{-# 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

import qualified MMT.Tools as Generic

-- import qualified PLpatt.Sublogic as SL

import Common.Id

import Common.DocUtils

-- import Common.Lib.Pretty

import ATerm.Conversion

-- import Common.Consistency

-- import ATC.AS_Annotation

import Data.Typeable.Internal

import qualified Common.DocUtils as DU

import qualified ATerm.Conversion as AT

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

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

instance (Pretty Sign.Sigs) where

pretty = DU.pretty

instance (ShATermConvertible Sign.Sigs) where

toShATermAux = AT.toShATermAux

fromShATermAux = AT.fromShATermAux

instance (ShATermConvertible Generic.Tree) where

instance (Ord Generic.Tree) where

instance (Eq Generic.Tree) where

instance (Data.Typeable.Internal.Typeable Generic.Tree) where

instance (Show Sign.Sigs) where

instance (ShATermConvertible Morphism.Morphism) where

instance (Pretty Morphism.Morphism) where

instance (ShATermConvertible AS.Form) where

instance (Pretty AS.Form) where

instance (ShATermConvertible AS.Symb) where

instance (Pretty AS.Symb) where

instance (Show Morphism.Morphism) where

instance (Show AS.Form) where

instance (Show AS.Symb) where

instance (Typeable Sign.Sigs) where

instance (Typeable Morphism.Morphism) where

instance (Typeable AS.Form) where

instance (Typeable AS.Symb) where

-- static analysis should in fact be performed by MMT

instance StaticAnalysis PLpatt

()

AS.Form

()

()

Sign.Sigs

Morphism.Morphism

AS.Symb

AS.Symb

where

instance Syntax PLpatt () () () where

-- instance of category

instance Category Sign.Sigs Morphism.Morphism where

--TODO place Morphism functions here

instance Sentences PLpatt

AS.Form Sign.Sigs Morphism.Morphism

AS.Symb

where

--TODO

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

instance Logic PLpatt

() -- SL.Sublogic -- sublogic

() -- basic_spec

AS.Form

() -- symb_items

() -- symb_map_items

Sign.Sigs -- sign

Morphism.Morphism -- sentence

AS.Symb -- Symb

AS.Symb -- raw Symb

Generic.Tree -- 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

-}