Logic_Rel.hs revision 5406d70d63c7c843823cda85d3a3304c432e9f2a
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder{- |
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederDescription : Instance of class Logic for Rel
76647324ed70f33b95a881b536d883daccf9568dChristian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2008
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : luecke@informatik.uni-bremen.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : experimental
76647324ed70f33b95a881b536d883daccf9568dChristian MaederPortability : non-portable (imports Logic.Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederInstance of class Logic for RelationalSchemes
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-}
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedermodule RelationalScheme.Logic_Rel where
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Logic.Logic
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport RelationalScheme.AS
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maederimport RelationalScheme.Sign
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport RelationalScheme.ParseRS
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport RelationalScheme.ATC_RelationalScheme()
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport RelationalScheme.StaticAnalysis
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.DocUtils
d48085f765fca838c1d972d2123601997174583dChristian Maeder
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederdata Rel = Rel deriving (Show)
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance Language Rel where
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder description _ =
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder "Simple logic for Relational Schemes"
d48085f765fca838c1d972d2123601997174583dChristian Maeder
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- | Instance of Category for Rel
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance Category
d48085f765fca838c1d972d2123601997174583dChristian Maeder Rel -- lid
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Sign -- sign
d48085f765fca838c1d972d2123601997174583dChristian Maeder RSMorphism -- mor
05ae87b9efa19655024b0b6ac344d250b96567cdChristian Maeder where
d48085f765fca838c1d972d2123601997174583dChristian Maeder legal_obj Rel _ = False
d48085f765fca838c1d972d2123601997174583dChristian Maeder legal_mor Rel _ = False
d48085f765fca838c1d972d2123601997174583dChristian Maeder dom Rel = domain
d48085f765fca838c1d972d2123601997174583dChristian Maeder cod Rel = codomain
d48085f765fca838c1d972d2123601997174583dChristian Maeder ide Rel = idMor
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder comp Rel = comp_rst_mor
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder-- ^ Instance of Sentences for Rel
a39a820684c1974350f46593025e0bb279f41bc6Christian Maederinstance Sentences Rel Sentence Sign RSMorphism () where
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder -- there is nothing to leave out
d48085f765fca838c1d972d2123601997174583dChristian Maeder simplify_sen Rel _ form = form
d48085f765fca838c1d972d2123601997174583dChristian Maeder print_named _ = printAnnoted (pretty) . fromLabelledSen
d48085f765fca838c1d972d2123601997174583dChristian Maeder map_sen Rel = map_rel
d48085f765fca838c1d972d2123601997174583dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | Syntax of Rel
05ae87b9efa19655024b0b6ac344d250b96567cdChristian Maederinstance Syntax Rel RSScheme () () where
d48085f765fca838c1d972d2123601997174583dChristian Maeder parse_basic_spec Rel = Just parseRSScheme
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder parse_symb_items _ = Nothing
a716971174535184da7713ed308423e355a4aa66Christian Maeder parse_symb_map_items _ = Nothing
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder-- | Instance of Logic for Relational Schemes
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maederinstance Logic Rel
feab655b0275874012c3cf9859064c177860cc70Christian Maeder () -- Sublogics
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder RSScheme -- basic_spec
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder Sentence -- sentence
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder () -- symb_items
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder () -- symb_map_items
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder Sign -- sign
a716971174535184da7713ed308423e355a4aa66Christian Maeder RSMorphism -- morphism
a716971174535184da7713ed308423e355a4aa66Christian Maeder () -- symbol
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder RSRawSymbol -- raw_symbol
a716971174535184da7713ed308423e355a4aa66Christian Maeder () -- proof_tree
a716971174535184da7713ed308423e355a4aa66Christian Maeder where
a716971174535184da7713ed308423e355a4aa66Christian Maeder stability Rel = Experimental
a716971174535184da7713ed308423e355a4aa66Christian Maeder
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder-- | Static Analysis for Rel
793945d4ac7c0f22760589c87af8e71427c76118Christian Maederinstance StaticAnalysis Rel
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder RSScheme -- basic_spec
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder Sentence -- sentence
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder () -- symb_items
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder () -- symb_map_items
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder Sign -- sign
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder RSMorphism -- morphism
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder () -- symbol
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder RSRawSymbol -- raw_symbol
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder where
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder basic_analysis Rel = Just $ basic_Rel_analysis
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder empty_signature Rel = emptyRSSign
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder is_subsig Rel = isRSSubsig
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder inclusion Rel = rsInclusion
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder