c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk{-# OPTIONS -fno-warn-missing-methods #-}

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk{- HetCATS/HasCASL/Logic_HasCASL.hs

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk $Id$

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk Authors: C. Maeder

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk Year: 2003

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk Here is the place where the class Logic is instantiated for HasCASL.

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk Also the instances for Syntax an Category.

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk todo:

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk - writing real functions

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk-}

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkmodule HasCASL.Logic_HasCASL where

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenk

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport HasCASL.As

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport HasCASL.Le

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport HasCASL.AsToLe

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport CASL.AS_Basic_CASL(SYMB_ITEMS, SYMB_MAP_ITEMS)

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport HasCASL.ParseItem

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport HasCASL.Merge

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport Common.Result

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport CASL.SymbolParser

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport Logic.ParsecInterface

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport Logic.Logic

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport Common.AnnoState(emptyAnnos)

c1350cf5bc50458ba79cc93ff9e0e5fe3f1aeeb0jeff.schenkimport Data.Dynamic

import Common.Lib.State

import HasCASL.Morphism

import qualified CASL.Sign

import qualified CASL.Static

import qualified CASL.Sublogics

import qualified CASL.Logic_CASL

type Sign = Env

type HasCASL_Sublogics = CASL.Sublogics.CASL_Sublogics

type Sentence = Formula

type Symbol = CASL.Sign.Symbol

type RawSymbol = CASL.Sign.RawSymbol

-- a dummy datatype for the LogicGraph and for identifying the right

-- instances

data HasCASL = HasCASL deriving (Show)

instance Language HasCASL -- default definition is okay

-- abstract syntax, parsing (and printing)

basicSpecTc :: TyCon

basicSpecTc = mkTyCon "HasCASL.As.BasicSpec"

signTc :: TyCon

signTc = mkTyCon "HasCASL.Le.Env"

sentenceTc :: TyCon

sentenceTc = mkTyCon "HasCASL.As.Formula"

instance Typeable BasicSpec where

typeOf _ = mkAppTy basicSpecTc []

instance Typeable Sign where

typeOf _ = mkAppTy signTc []

instance Typeable Sentence where

typeOf _ = mkAppTy sentenceTc []

instance Syntax HasCASL BasicSpec

SYMB_ITEMS SYMB_MAP_ITEMS

where

parse_basic_spec HasCASL = Just(toParseFun basicSpec emptyAnnos)

parse_symb_items HasCASL = Just(toParseFun symbItems ())

parse_symb_map_items HasCASL = Just(toParseFun symbMapItems ())

instance Category HasCASL Env Morphism where

ide HasCASL e = ideMor e

comp HasCASL m1 m2 = Just $ compMor m1 m2

dom HasCASL m = msource m

cod HasCASL m = mtarget m

legal_obj HasCASL e = legalEnv e

legal_mor HasCASL m = legalMor m

instance Sentences HasCASL Sentence () Sign Morphism Symbol

instance StaticAnalysis HasCASL BasicSpec Sentence ()

SYMB_ITEMS SYMB_MAP_ITEMS

Sign

Morphism

Symbol RawSymbol where

basic_analysis HasCASL = Just ( \ (b, e, _) ->

let ne = snd $ (runState (anaBasicSpec b)) e

in return (ne, initialEnv, []))

stat_symb_map_items HasCASL = CASL.Static.statSymbMapItems

stat_symb_items HasCASL = CASL.Static.statSymbItems

symbol_to_raw HasCASL = CASL.Static.symbolToRaw

id_to_raw HasCASL = CASL.Static.idToRaw

matches HasCASL = CASL.Static.matches

sym_name HasCASL = CASL.Static.symName

signature_union HasCASL = merge

empty_signature HasCASL = initialEnv

induced_from_to_morphism HasCASL _ e1 e2 = return $ mkMorphism e1 e2

induced_from_morphism HasCASL _ e = return $ ideMor e

morphism_union HasCASL m1 m2 = morphismUnion m1 m2

cogenerated_sign HasCASL _ e = return $ ideMor e

instance Logic HasCASL HasCASL_Sublogics

BasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS

Sign

Morphism

Symbol RawSymbol () where

sublogic_names HasCASL = CASL.Sublogics.sublogics_name

all_sublogics HasCASL = CASL.Sublogics.sublogics_all

is_in_symb_items HasCASL = CASL.Sublogics.in_symb_items

is_in_symb_map_items HasCASL = CASL.Sublogics.in_symb_map_items

is_in_symbol HasCASL = CASL.Sublogics.in_symbol

min_sublogic_symb_items HasCASL = CASL.Sublogics.sl_symb_items

min_sublogic_symb_map_items HasCASL = CASL.Sublogics.sl_symb_map_items

min_sublogic_symbol HasCASL = CASL.Sublogics.sl_symbol

proj_sublogic_symb_items HasCASL = CASL.Sublogics.pr_symb_items

proj_sublogic_symb_map_items HasCASL = CASL.Sublogics.pr_symb_map_items

proj_sublogic_symbol HasCASL = CASL.Sublogics.pr_symbol