AS.hs revision 36b9e4cf34070e81d93765f129044abc5dbcf678
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : Abstract syntax for logical frameworks
81ec673ac5ab1493568d9ef7798b752ab8ee0e61Felix Gabriel ManceCopyright : (c) Kristina Sojakova, DFKI Bremen 2010
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : k.sojakova@jacobs-university.de
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceStability : experimental
5d801400993c9671010d244646936d8fd435638cChristian MaederPortability : portable
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mancetype NAME = Token
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancetype SIG_NAME = Token
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maedertype MORPH_NAME = Token
090c663fcc1593c66f39a0972326799a672760d5Christian Maedertype PATTERN_NAME = Token
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescudata FRAM = LF | Isabelle | Maude deriving (Ord, Eq, Show)
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescudata BASIC_SPEC = Basic_spec
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu { -- name of the object logic
feab1106bbee4f2ea2fd48bca7106dd041e4211dFelix Gabriel Mance logicName :: NAME,
18ff56829e5e99383ee6106584d55bcbd8ed45e7Felix Gabriel Mance -- the framework used for defining the object logic
b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder -- name of the signature specifying the syntax of the object logic
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder syntax :: SIG_NAME,
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance {- name of the morphism specifying the sentences and truth judgement of the
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance object logic -}
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance truth :: MORPH_NAME,
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder -- name of the pattern specifying the signature category of the object logic
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance signatures :: PATTERN_NAME,
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance -- name of the morphism specifying the model category of the object logic
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder models :: MORPH_NAME,
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance -- name of the morphism specifying the proof category of the object logic
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance proofs :: MORPH_NAME
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance } deriving (Ord, Eq, Show)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceinstance GetRange BASIC_SPEC
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceinstance Pretty BASIC_SPEC where
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance pretty = printBasicSpec
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceinstance Pretty FRAM where
0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Mance pretty = printFram
852bd6145634dc2832b61c44678fe539bc1682d5Christian MaederprintBasicSpec :: BASIC_SPEC -> Doc
1a38107941725211e7c3f051f7a8f5e12199f03acmaederprintBasicSpec (Basic_spec l f sy t si m p) =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance vcat [ text "logic" <+> pretty l <+> text "="
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , text " " <+> text "meta" <+> pretty f
6033265e7b4ae660eff78e944213286863304903Mihai Codescu , text " " <+> text "syntax" <+> pretty sy
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , text " " <+> text "truth" <+> pretty t
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , text " " <+> text "signatures" <+> pretty si
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , text " " <+> text "models" <+> pretty m
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , text " " <+> text "proofs" <+> pretty p
68de80eb2800338cbd16512106fcadab79325d8bChristian MaederprintFram :: FRAM -> Doc
68de80eb2800338cbd16512106fcadab79325d8bChristian MaederprintFram LF = text "LF"
68de80eb2800338cbd16512106fcadab79325d8bChristian MaederprintFram Isabelle = text "Isabelle"
68de80eb2800338cbd16512106fcadab79325d8bChristian MaederprintFram Maude = text "Maude"