6133N/A{- |

6133N/AModule : $Header$

6133N/ADescription : COL instance of class Logic

6133N/ACopyright : (c) Till Mossakowski, Uni Bremen 2002-2004

6133N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

6133N/A

6133N/AMaintainer : till@informatik.uni-bremen.de

6133N/AStability : provisional

6133N/APortability : non-portable (via Logic)

6133N/A

6133N/ACOL instance of class Logic

6133N/A-}

6133N/A

6133N/Amodule COL.Logic_COL where

6133N/A

6133N/Aimport COL.AS_COL

6133N/Aimport COL.COLSign

6133N/Aimport COL.ATC_COL()

6133N/Aimport COL.Parse_AS()

6133N/Aimport COL.StatAna

6133N/Aimport COL.Print_AS()

6133N/Aimport CASL.Sign

6133N/Aimport CASL.StaticAna

6133N/Aimport CASL.MixfixParser

6133N/Aimport CASL.Morphism

6133N/Aimport CASL.SymbolMapAnalysis

6133N/Aimport CASL.AS_Basic_CASL

6133N/Aimport CASL.Parse_AS_Basic

6133N/Aimport CASL.MapSentence

6133N/Aimport CASL.SymbolParser

6147N/Aimport Logic.Logic

6147N/A

6147N/Adata COL = COL deriving Show

6147N/A

6147N/Ainstance Language COL where

6147N/A description _ =

6133N/A "COLCASL extends CASL by constructors and observers"

6147N/A

6147N/Atype C_BASIC_SPEC = BASIC_SPEC () COL_SIG_ITEM ()

6147N/Atype CSign = Sign () COLSign

6147N/Atype COLMor = Morphism () COLSign ()

6147N/Atype COLFORMULA = FORMULA ()

6147N/A

6133N/Ainstance Category COL CSign COLMor

6147N/A where

6147N/A -- ide :: id -> object -> morphism

6147N/A ide COL = idMor ()

6133N/A -- comp :: id -> morphism -> morphism -> Maybe morphism

6147N/A comp COL = compose (const id)

6147N/A -- dom, cod :: id -> morphism -> object

6147N/A dom COL = msource

6147N/A cod COL = mtarget

6133N/A -- legal_obj :: id -> object -> Bool

6133N/A legal_obj COL = legalSign

6133N/A -- legal_mor :: id -> morphism -> Bool

6133N/A legal_mor COL = legalMor

-- abstract syntax, parsing (and printing)

instance Syntax COL C_BASIC_SPEC

SYMB_ITEMS SYMB_MAP_ITEMS

where

parse_basic_spec COL = Just $ basicSpec col_reserved_words

parse_symb_items COL = Just $ symbItems col_reserved_words

parse_symb_map_items COL = Just $ symbMapItems col_reserved_words

-- COL logic

instance Sentences COL COLFORMULA CSign COLMor Symbol where

map_sen COL m = return . mapSen (\ _ -> id) m

parse_sentence COL = Nothing

sym_of COL = symOf

symmap_of COL = morphismToSymbMap

sym_name COL = symName

instance StaticAnalysis COL C_BASIC_SPEC COLFORMULA

SYMB_ITEMS SYMB_MAP_ITEMS

CSign

COLMor

Symbol RawSymbol where

basic_analysis COL = Just $ basicAnalysis (const return)

(const return) ana_COL_SIG_ITEM

emptyMix

stat_symb_map_items COL = statSymbMapItems

stat_symb_items COL = statSymbItems

ensures_amalgamability COL _ =

fail "COL: ensures_amalgamability nyi" -- ???

sign_to_basic_spec COL _sigma _sens = Basic_spec [] -- ???

symbol_to_raw COL = symbolToRaw

id_to_raw COL = idToRaw

matches COL = CASL.Morphism.matches

empty_signature COL = emptySign emptyCOLSign

signature_union COL sigma1 sigma2 =

return $ addSig addCOLSign sigma1 sigma2

morphism_union COL = morphismUnion (const id) addCOLSign

final_union COL = finalUnion addCOLSign

inclusion COL = sigInclusion () isSubCOLSign diffCOLSign

cogenerated_sign COL = cogeneratedSign ()

generated_sign COL = generatedSign ()

induced_from_morphism COL = inducedFromMorphism ()

induced_from_to_morphism COL =

inducedFromToMorphism () isSubCOLSign diffCOLSign

instance Logic COL ()

C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CSign

COLMor

Symbol RawSymbol () where

empty_proof_tree _ = ()