2509N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
0N/ADescription : Instances of Logic and other classes for the logic Framework
0N/ACopyright : (c) Kristina Sojakova, DFKI Bremen 2009
0N/AMaintainer : k.sojakova@jacobs-university.de
0N/AStability : experimental
0N/APortability : portable
0N/A Signatures of this logic are composed of a logical framework name
0N/A (currently one of LF, Isabelle, or Maude) to be used as a meta-logic,
0N/A and a tuple of signature and morphism names which determine
0N/A the object logic. As such the logic Framework does not have any
0N/A sentences and only identity signature morphisms.
2362N/A For reference see Integrating Logical Frameworks in Hets by M. Codescu et al
0N/Atype Morphism = DefaultMorphism LogicDef
0N/A-- lid for logical frameworks
1178N/Adata Framework = Framework deriving Show
0N/Ainstance Language Framework where
0N/A description _ = "A framework allowing to add logics dynamically."
0N/A-- syntax for Framework
0N/Ainstance Syntax Framework LogicDef () ()
0N/A-- sentences for Framework
0N/Ainstance Sentences Framework () LogicDef Morphism ()
0N/A-- static analysis for Framework
0N/Ainstance StaticAnalysis Framework LogicDef () () ()
0N/A LogicDef Morphism () () where
0N/A empty_signature Framework = error
0N/A "Logic Framework does not have an empty signature."
0N/A-- instance of logic for Framework
0N/Ainstance Logic Framework () LogicDef () () () LogicDef Morphism () () ()