{-# LANGUAGE CPP, MultiParamTypeClasses #-}

{-

the following code is automatically generated by

MMT/hets-mmt-standalone.jar

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

instance (DU.Pretty Sign.Sigs) 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

instance (DU.Pretty AS.Bool') where

pretty a = DU.text $ show a

instance (AT.ShATermConvertible AS.Symb) where

toShATermAux = AT.toShATermAux

fromShATermAux = AT.fromShATermAux

instance (DU.Pretty AS.Symb) where

pretty a = DU.text $ show $ AS.sname a

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 []

mappend (AS.Basic_spec bs1) (AS.Basic_spec bs2) = AS.Basic_spec $ bs1 ++ bs2

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?

AS.Bool'

()

()

Sign.Sigs

Morphism.Morphism

AS.Symb

AS.Symb

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

AS.Symb

()

()

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 PLpatt

AS.Bool'

Sign.Sigs

Morphism.Morphism

AS.Symb

where

-- Logic instance, see Logic/Logic.hs:867

instance Logic PLpatt

() -- SL.Sublogic -- sublogic

AS.Basic_spec -- basic_spec

AS.Bool'

() -- 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

-}