1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaDescription : Abstract syntax for logic definitions
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaCopyright : (c) Kristina Sojakova, DFKI Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaMaintainer : k.sojakova@jacobs-university.de
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaStability : experimental
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaPortability : portable
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksatype NAME = IRI
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksatype SIG_NAME = IRI
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksatype MORPH_NAME = IRI
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakovatype PATTERN_NAME = Token
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata FRAM = LF | Isabelle | Maude deriving (Show, Eq, Ord, Typeable, Data)
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakovadata LogicDef = LogicDef
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova { -- the name of the object logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder newlogicName :: NAME,
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova -- the framework used for defining the object logic
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova {- name of the morphism specifying the sentences and truth judgement of the
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina Sojakova object logic -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder syntax :: MORPH_NAME,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- name of the morphism specifying the model category of the object logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder models :: MORPH_NAME,
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina Sojakova -- the foundation used to construct the model theory of the object logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder foundation :: SIG_NAME,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- name of the morphism specifying the proof category of the object logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder proofs :: MORPH_NAME,
3df50f2bdc19d6aa0d3ee0ecac5ad7ad785ddb45Kristina Sojakova -- name of the pattern specifying the signature category of the object logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder patterns :: PATTERN_NAME
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovdata ComorphismDef = ComorphismDef
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { -- the name of the comorphism
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov newcomorphismName :: NAME,
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- the framework used for defining the comorphism
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- name of the source logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder source :: SIG_NAME,
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov -- name of the target logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder target :: SIG_NAME,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- name of the morphism between the syntax of the source logic and
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov the syntax of the target logic -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder syntaxC :: MORPH_NAME,
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov {- name of the morphism between the model category of the source logic and
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov the model category of the target logic -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder modelC :: MORPH_NAME,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- name of the morphism between the proof category of the source logic and
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov the proof category of the target logic -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder proofC :: MORPH_NAME
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakovainstance GetRange LogicDef
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovinstance GetRange ComorphismDef
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakovainstance Pretty LogicDef where
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova pretty = printLogicDef
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovinstance Pretty ComorphismDef where
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pretty = printComorphismDef
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakovainstance Pretty FRAM where
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina Sojakova pretty = printFram
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina SojakovaprintLogicDef :: LogicDef -> Doc
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintLogicDef (LogicDef l ml s m f p pa) =
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova vcat [ text newlogicS <+> pretty l
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina Sojakova , text " " <+> text metaS <+> pretty ml
3df50f2bdc19d6aa0d3ee0ecac5ad7ad785ddb45Kristina Sojakova , text " " <+> text syntaxS <+> pretty s
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova , text " " <+> text modelsS <+> pretty m
109f89c82ec8769e9ec81bc967987b5deecdfd25Kristina Sojakova , text " " <+> text foundationS <+> pretty f
f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova , text " " <+> text proofsS <+> pretty p
3df50f2bdc19d6aa0d3ee0ecac5ad7ad785ddb45Kristina Sojakova , text " " <+> text patternsS <+> pretty pa
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovprintComorphismDef :: ComorphismDef -> Doc
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovprintComorphismDef (ComorphismDef c ml sl tl s m p) =
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov vcat [ text newcomorphismS <+> pretty c
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov , text " " <+> text metaS <+> pretty ml
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov , text " " <+> text sourceS <+> pretty sl
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov , text " " <+> text targetS <+> pretty tl
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov , text " " <+> text syntaxS <+> pretty s
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov , text " " <+> text modelsS <+> pretty m
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov , text " " <+> text proofsS <+> pretty p
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaprintFram :: FRAM -> Doc
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaprintFram LF = text "LF"
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaprintFram Isabelle = text "Isabelle"
bdc4fdc3b1e638eb2f5c0e08a577c9b1a042b506Kristina SojakovaprintFram Maude = text "Maude"