AS.hs revision b31d9d9838c96dff0effbfa224ee825fa492fd65
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederDescription : Abstract syntax for logical frameworks
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) Kristina Sojakova, DFKI Bremen 2010
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederMaintainer : k.sojakova@jacobs-university.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : experimental
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederPortability : portable
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedertype NAME = Token
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedertype SIG_NAME = Token
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maedertype MORPH_NAME = Token
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maedertype PATTERN_NAME = Token
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maederdata FRAM = LF | Isabelle | Maude deriving (Ord, Eq, Show)
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederdata BASIC_SPEC = Basic_spec
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder { -- name of the object logic
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder logicName :: NAME,
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder -- the framework used for defining the object logic
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder meta :: FRAM,
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder -- name of the signature specifying the syntax of the object logic
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder syntax :: SIG_NAME,
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder {- name of the morphism specifying the sentences and truth judgement of the
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder object logic -}
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder truth :: MORPH_NAME,
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder -- name of the pattern specifying the signature category of the object logic
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder signatures :: PATTERN_NAME,
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder -- name of the morphism specifying the model category of the object logic
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder models :: MORPH_NAME,
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder -- name of the morphism specifying the proof category of the object logic
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder proofs :: MORPH_NAME
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder } deriving (Ord, Eq, Show)
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maederinstance GetRange BASIC_SPEC