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

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

instance (DU.Pretty AS.Symb) where

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

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

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

()

()

Sign.Sigs

Morphism.Morphism

AS.Symb

AS.Symb

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

Sign.Sigs

Morphism.Morphism

AS.Symb

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

-}