5592eb9fcfb498f454c45ee4b4b165a38bf4da40Christian Maeder{- |

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst SchulzModule : $Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : COL instance of class Logic

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst SchulzCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst SchulzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst SchulzMaintainer : till@informatik.uni-bremen.de

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst SchulzStability : provisional

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst SchulzPortability : non-portable (via Logic)

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulz

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst SchulzCOL instance of class Logic

1b353d403dbdb365ae93a568f32b3ebf5698cab5Ewaryst Schulz-}

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulz

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulzmodule COL.Logic_COL where

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulz

df0d1a7e7dfff3be40c24b25318a6a07c748be20Ewaryst Schulzimport COL.AS_COL

32e0cbe45839af0ec675bcff62a34ca3709f5588Ewaryst Schulzimport COL.COLSign

32e0cbe45839af0ec675bcff62a34ca3709f5588Ewaryst Schulzimport COL.ATC_COL()

8e2a5b3d7ccf6a7f03b54fbe6b410d49b9f1932cEwaryst Schulzimport COL.Parse_AS()

97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulzimport COL.StatAna

97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulzimport COL.Print_AS()

97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulzimport CASL.Sign

b1f2971b105e6da3f4722315e0a0e2abef96e66fcmaederimport CASL.StaticAna

97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulzimport CASL.MixfixParser

df0d1a7e7dfff3be40c24b25318a6a07c748be20Ewaryst Schulzimport CASL.Morphism

1a5414972199f27756b513d5cf515e4c0d688c08Ewaryst Schulzimport CASL.SymbolMapAnalysis

97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulzimport CASL.AS_Basic_CASL

0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulzimport CASL.Parse_AS_Basic

b524978df6a89e40139f2862ad9eb6f9f5c8a1b5Ewaryst Schulzimport CASL.MapSentence

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulzimport CASL.SymbolParser

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulzimport CASL.Logic_CASL ()

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulzimport Logic.Logic

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulz

99cb8518c038b6764ffef18cd734d2fc4e5c6f0bEwaryst Schulzdata COL = COL deriving Show

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulz

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulzinstance Language COL where

28f336e639eae9e0a940a673159198d9ef4e5613Ewaryst Schulz description _ =

5592eb9fcfb498f454c45ee4b4b165a38bf4da40Christian Maeder "COLCASL extends CASL by constructors and observers"

30f67f0a856f2018bf5559413be27f7c0ab5bbfbEwaryst Schulz

30f67f0a856f2018bf5559413be27f7c0ab5bbfbEwaryst Schulztype C_BASIC_SPEC = BASIC_SPEC () COL_SIG_ITEM ()

4af7799ec93fe75c6db8217c54d3d0656d104534Ewaryst Schulztype CSign = Sign () COLSign

8e2a5b3d7ccf6a7f03b54fbe6b410d49b9f1932cEwaryst Schulztype COLMor = Morphism () COLSign ()

30f67f0a856f2018bf5559413be27f7c0ab5bbfbEwaryst Schulztype COLFORMULA = FORMULA ()

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Syntax COL C_BASIC_SPEC

4869d2d404a494368f782e3446222461be4aede2Ewaryst Schulz SYMB_ITEMS SYMB_MAP_ITEMS

d1fddc394ac2af87a6210e7a3504bb565d088e7aEwaryst Schulz where

8e2a5b3d7ccf6a7f03b54fbe6b410d49b9f1932cEwaryst Schulz parse_basic_spec COL = Just $ basicSpec col_reserved_words

30f67f0a856f2018bf5559413be27f7c0ab5bbfbEwaryst Schulz parse_symb_items COL = Just $ symbItems col_reserved_words

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz parse_symb_map_items COL = Just $ symbMapItems col_reserved_words

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulzinstance Sentences COL COLFORMULA CSign COLMor Symbol where

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

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz parse_sentence COL = Nothing

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz sym_of COL = symOf

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz symmap_of COL = morphismToSymbMap

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz sym_name COL = symName

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulzinstance StaticAnalysis COL C_BASIC_SPEC COLFORMULA

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz SYMB_ITEMS SYMB_MAP_ITEMS

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz CSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz COLMor

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz Symbol RawSymbol where

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz basic_analysis COL = Just $ basicAnalysis (const return)

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz (const return) ana_COL_SIG_ITEM

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz emptyMix

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz stat_symb_map_items COL = statSymbMapItems

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz stat_symb_items COL = statSymbItems

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz symbol_to_raw COL = symbolToRaw

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz id_to_raw COL = idToRaw

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz matches COL = CASL.Morphism.matches

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz empty_signature COL = emptySign emptyCOLSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz signature_union COL sigma1 sigma2 =

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz return $ addSig addCOLSign sigma1 sigma2

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz morphism_union COL = morphismUnion (const id) addCOLSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz final_union COL = finalUnion addCOLSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz inclusion COL = sigInclusion () isSubCOLSign diffCOLSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz cogenerated_sign COL = cogeneratedSign () isSubCOLSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz generated_sign COL = generatedSign () isSubCOLSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz induced_from_morphism COL = inducedFromMorphism () isSubCOLSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz induced_from_to_morphism COL =

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz inducedFromToMorphism () isSubCOLSign diffCOLSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulzinstance Logic COL ()

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz CSign

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz COLMor

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz Symbol RawSymbol () where

1110f944e5455a3cd6461d296b373d19c0faa84eEwaryst Schulz empty_proof_tree _ = ()

30f67f0a856f2018bf5559413be27f7c0ab5bbfbEwaryst Schulz