Logic.tmpl revision 0413c36cba625f74f193961c19826a5424c45c1d
{-# LANGUAGE CPP, MultiParamTypeClasses #-}
{-
the following code is automatically generated by
static analysis is performed by MMT,
therefore static analysis functions are absent
-}
module <LogicName>.Logic_<LogicName> where
import Logic.Logic -- Logic and accompanying classes
import qualified <LogicName>.Sign as Sign
import qualified <LogicName>.Morphism as Morphism
import qualified <LogicName>.AS_BASIC_<LogicName> as AS
-- import qualified <LogicName>.Tools as Tools -- TODO
import qualified MMT.Tools as Generic
-- import qualified <LogicName>.Sublogic as SL -- TODO
import Common.Id
import qualified Common.DocUtils as DU
import qualified ATerm.Conversion as AT
import qualified Data.Typeable.Internal as Tp
import Common.Result
import Data.Monoid
-- Logic ID lid
data <LogicName> = <LogicName> deriving Show
-- language
instance Language <LogicName> where
description _ = "This is some logic generated by MMT\n"
instance (Ord Sign.Sigs) where
instance (Eq Sign.Sigs) where
instance (Ord Morphism.Morphism) where
instance (Eq Morphism.Morphism) where
instance (Ord AS.<Form>) where
instance (Eq AS.<Form>) where
instance (Ord AS.Symb) where
instance (Eq AS.Symb) where
instance (Common.Id.GetRange AS.<Form>) where
instance (Common.Id.GetRange AS.Symb) where
pretty = DU.pretty
instance (AT.ShATermConvertible Sign.Sigs) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
instance (AT.ShATermConvertible Generic.Tree) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
instance (Ord Generic.Tree) where
instance (Eq Generic.Tree) where
instance (Tp.Typeable Generic.Tree) where
typeOf = Tp.typeOf
instance (Show Sign.Sigs) where
instance (AT.ShATermConvertible Morphism.Morphism) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
instance (DU.Pretty Morphism.Morphism) where
pretty = DU.pretty
instance (AT.ShATermConvertible AS.<Form>) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
instance (DU.Pretty AS.<Form>) where
pretty = DU.pretty
instance (AT.ShATermConvertible AS.Symb) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
pretty = DU.pretty
instance (Show Morphism.Morphism) where
instance (Show AS.<Form>) where
instance (Show AS.Symb) where
instance (Tp.Typeable Sign.Sigs) where
typeOf = Tp.typeOf
instance (Tp.Typeable Morphism.Morphism) where
typeOf = Tp.typeOf
instance (Tp.Typeable AS.<Form>) where
typeOf = Tp.typeOf
instance (Tp.Typeable AS.Symb) where
typeOf = Tp.typeOf
-- instances required for newtype Basic_spec
instance (DU.Pretty AS.Basic_spec) where
pretty = DU.pretty
instance (GetRange AS.Basic_spec) where
instance (Data.Monoid.Monoid AS.Basic_spec) where
mempty = AS.Basic_spec []
instance (Show AS.Basic_spec) where
instance (AT.ShATermConvertible AS.Basic_spec) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
instance (Tp.Typeable AS.Basic_spec) where
typeOf = Tp.typeOf
-- static analysis should in fact be performed by MMT
instance StaticAnalysis <LogicName>
AS.Basic_spec -- datatype for syntax trees - Generic.Tree?
AS.<Form>
()
()
where
empty_signature <LogicName> = Sign.Sigs []
instance Syntax <LogicName>
AS.Basic_spec -- parse_basic_spec produces a syntax tree
()
()
where
-- parse_basic_spec lid = Just (\pm -> parser) -- Text.CombinatorParses.Parsec
-- basic_analysis lid = Just (\ .. )
-- instance of category
instance Category Sign.Sigs Morphism.Morphism where
ide sgn = Morphism.Morphism sgn sgn
composeMorphisms mor1 _ = Result [] (Just mor1) -- TODO
dom = Morphism.source
cod = Morphism.target
instance Sentences <LogicName>
AS.<Form>
where
-- TODO
-- Logic instance, see Logic/Logic.hs:867
instance Logic <LogicName>
() -- SL.Sublogic -- sublogic
AS.Basic_spec -- basic_spec
AS.<Form>
() -- symb_items
() -- symb_map_items
Sign.Sigs -- sign
Morphism.Morphism -- sentence
AS.Symb -- Symb
AS.Symb -- raw Symb
() -- proof tree
where
{-
logic_name = show
id lid = Morphism.id
comp lid = Morphism.comp
parse_basic_spec lid = Generic.parseSpec
map_sen lid = Morphism.mapSen
basic_analysis lid = Tools.theo_from_pt
stat_symb_map lid = Tools.mor_from_pt
minSublogic lid = SL.minSublogic
-}