{-# 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 Common.Doc as DU
import qualified ATerm.Conversion as AT
import qualified Data.Typeable.Internal as Tp
import Common.Result
import Data.Monoid
import qualified <LogicName>.Parse_<LogicName> as LogicParse
import <LogicName>.StaticAna<LogicName>
-- 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
_ == _ = True
instance (Ord AS.Symb) where
_ <= _ = True
instance (Eq AS.Symb) where
_ == _ = True
instance (Common.Id.GetRange AS.<Form>) where
instance (Common.Id.GetRange AS.Symb) where
pretty a = DU.text $ show a--DU.empty--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
_ <= _ = True
instance (Eq Generic.Tree) where
_ == _ = True
instance (AT.ShATermConvertible Morphism.Morphism) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
instance (DU.Pretty Morphism.Morphism) where
pretty a = DU.text $ show a --DU.empty--DU.pretty
instance (AT.ShATermConvertible AS.<Form>) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
instance (DU.Pretty AS.<Form>) where
pretty a = DU.text $ show a
instance (AT.ShATermConvertible AS.Symb) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
pretty a = DU.text $ show a--DU.empty--DU.pretty
instance (Show Morphism.Morphism) where
instance (Tp.Typeable Morphism.Morphism) where
typeOf = Tp.typeOf
instance (DU.Pretty AS.Basic_spec) where
pretty a = DU.text $ show a --DU.empty--DU.pretty
instance (GetRange AS.Basic_spec) where
instance (Data.Monoid.Monoid AS.Basic_spec) where
mempty = AS.Basic_spec []
instance (AT.ShATermConvertible AS.Basic_spec) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
-- 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 []
signatureDiff <LogicName> = Sign.sigDiff
basic_analysis <LogicName> = Just basicAna
instance Syntax <LogicName>
AS.Basic_spec -- parse_basic_spec produces a syntax tree
()
()
where
parse_basic_spec _ = Just (\ _ -> LogicParse.parse1)
-- 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
-- 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
-}