{-# OPTIONS -fno-warn-missing-methods #-}

{- HetCATS/HasCASL/Logic_HasCASL.hs

$Id$

Authors: C. Maeder

Year: 2003

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

Also the instances for Syntax an Category.

todo:

- writing real functions

-}

module HasCASL.Logic_HasCASL where

import HasCASL.As

import HasCASL.Le

import HasCASL.AsToLe

import CASL.AS_Basic_CASL(SYMB_ITEMS, SYMB_MAP_ITEMS)

import HasCASL.ParseItem

import HasCASL.Merge

import Common.Result

import CASL.SymbolParser

import Logic.ParsecInterface

import Logic.Logic

import Common.AnnoState(emptyAnnos)

import Data.Dynamic

import Common.Lib.State

import HasCASL.Morphism

import qualified CASL.Sign

import qualified CASL.Static

import qualified CASL.SymbolAnalysis

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.SymbolAnalysis.statSymbMapItems

stat_symb_items HasCASL = CASL.SymbolAnalysis.statSymbItems

symbol_to_raw HasCASL = CASL.SymbolAnalysis.symbolToRaw

id_to_raw HasCASL = CASL.SymbolAnalysis.idToRaw

matches HasCASL = CASL.SymbolAnalysis.matches

sym_name HasCASL = CASL.SymbolAnalysis.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