{-# LANGUAGE CPP, MultiParamTypeClasses #-}
{-
the following code is automatically generated by
static analysis is performed by MMT,
therefore static analysis functions are absent
-}
module PLpatt.Logic_PLpatt where
import Logic.Logic -- Logic and accompanying classes
import qualified PLpatt.Sign as Sign
import qualified PLpatt.Morphism as Morphism
import qualified PLpatt.AS_BASIC_PLpatt as AS
-- import qualified PLpatt.Tools as Tools -- TODO
import qualified MMT.Tools as Generic
-- import qualified PLpatt.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 PLpatt.Parse_PLpatt as LogicParse
import PLpatt.StaticAnaPLpatt
-- Logic ID lid
data PLpatt = PLpatt deriving Show
-- language
instance Language PLpatt 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 (Common.Id.GetRange AS.Bool') where
instance (Common.Id.GetRange AS.Symb) where
pretty a = DU.text $ show a
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
instance (AT.ShATermConvertible AS.Bool') where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
pretty a = DU.text $ show a
instance (AT.ShATermConvertible AS.Symb) where
toShATermAux = AT.toShATermAux
fromShATermAux = AT.fromShATermAux
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 $ case a of (AS.Basic_spec ls) -> unlines ls
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 PLpatt
AS.Basic_spec -- datatype for syntax trees - Generic.Tree?
()
()
where
empty_signature PLpatt = Sign.Sigs []
signatureDiff PLpatt = Sign.sigDiff
basic_analysis PLpatt = Just basicAna
instance Syntax PLpatt
AS.Basic_spec -- parse_basic_spec produces a syntax tree
()
()
where
parse_basic_spec _ = Just $ const 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 PLpatt
where
-- Logic instance, see Logic/Logic.hs:867
instance Logic PLpatt
() -- SL.Sublogic -- sublogic
AS.Basic_spec -- basic_spec
() -- 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
-}