AS.hs revision 2cb6df4f21c52732336579a79f7e5d28299b3500
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$
2dc26996d32244796c48c71fe44413c8ebf8bbc9Christian MaederDescription : Abstract syntax for logic definitions
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederCopyright : (c) Kristina Sojakova, DFKI Bremen 2010
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : k.sojakova@jacobs-university.de
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : experimental
a0e24c863b78669b05797ff8ce635995a9bede44Christian MaederPortability : portable
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedertype NAME = Token
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedertype SIG_NAME = Token
ad270004874ce1d0697fb30d7309f180553bb315Christian Maedertype MORPH_NAME = Token
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maedertype PATTERN_NAME = Token
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederdata FRAM = LF | Isabelle | Maude deriving (Ord, Eq, Show)
2dc26996d32244796c48c71fe44413c8ebf8bbc9Christian Maederdata LogicDef = LogicDef
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder { -- the name of the object logic
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder newlogicName :: NAME,
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder -- the framework used for defining the object logic
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder meta :: FRAM,
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder {- name of the morphism specifying the sentences and truth judgement of the
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder object logic -}
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder syntax :: MORPH_NAME,
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -- name of the morphism specifying the model category of the object logic
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder models :: MORPH_NAME,
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -- the foundation used to construct the model theory of the object logic
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder foundation :: SIG_NAME,
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -- name of the morphism specifying the proof category of the object logic
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder proofs :: MORPH_NAME,
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -- name of the pattern specifying the signature category of the object logic
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder patterns :: PATTERN_NAME
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder } deriving (Ord, Eq, Show)
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederdata ComorphismDef = ComorphismDef
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder { --the name of the comorphism
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder newcomorphismName :: NAME,
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- the framework used for defining the comorphism
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder metaC :: FRAM,
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- name of the source logic
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder source :: SIG_NAME,
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -- name of the target logic
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder target :: SIG_NAME,
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder {- name of the morphism between the syntax of the source logic and
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder the syntax of the target logic -}
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder syntaxC :: MORPH_NAME,
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder {- name of the morphism between the model category of the source logic and
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder the model category of the target logic -}
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder modelC :: MORPH_NAME,
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder {- name of the morphism between the proof category of the source logic and
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder the proof category of the target logic -}
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder proofC :: MORPH_NAME
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder } deriving (Ord, Eq, Show)
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maederinstance GetRange LogicDef
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederinstance GetRange ComorphismDef
7feac39f792f587cffdc8b63b0e7c5a7d2de292eChristian Maederinstance Pretty LogicDef where
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder pretty = printLogicDef
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederinstance Pretty ComorphismDef where
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder pretty = printComorphismDef
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maederinstance Pretty FRAM where
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder pretty = printFram
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederprintLogicDef :: LogicDef -> Doc
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederprintLogicDef (LogicDef l ml s m f p pa) =
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder vcat [ text newlogicS <+> pretty l
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , text " " <+> text metaS <+> pretty ml
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , text " " <+> text syntaxS <+> pretty s
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , text " " <+> text modelsS <+> pretty m
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , text " " <+> text foundationS <+> pretty f
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder , text " " <+> text proofsS <+> pretty p
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , text " " <+> text patternsS <+> pretty pa
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederprintComorphismDef :: ComorphismDef -> Doc
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederprintComorphismDef (ComorphismDef c ml sl tl s m p) =
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder vcat [ text newcomorphismS <+> pretty c
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , text " " <+> text metaS <+> pretty ml
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , text " " <+> text sourceS <+> pretty sl
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder , text " " <+> text targetS <+> pretty tl
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder , text " " <+> text syntaxS <+> pretty s
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder , text " " <+> text modelsS <+> pretty m
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder , text " " <+> text proofsS <+> pretty p
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederprintFram :: FRAM -> Doc
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaederprintFram LF = text "LF"
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaederprintFram Isabelle = text "Isabelle"
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaederprintFram Maude = text "Maude"