hets/COL/Logic_COL.hs

2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnell{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnell{- |
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellModule      :  ./COL/Logic_COL.hs
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellDescription :  COL instance of class Logic
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellCopyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellLicense     :  GPLv2 or higher, see LICENSE.txt
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnell
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellMaintainer  :  till@informatik.uni-bremen.de
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellStability   :  provisional
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellPortability :  non-portable (via Logic)
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnell
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellCOL instance of class Logic
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnell-}
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnell
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellmodule COL.Logic_COL where
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnell
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellimport COL.AS_COL
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellimport COL.COLSign
415243fbc81341293a852ff6aa14e9608d08685cCraig McDonnellimport COL.ATC_COL ()
fb63998ce7684bddab24e10c0b593809df1b7bffCraig McDonnellimport COL.Parse_AS ()
916ef74523ecddc8140815c084ab6971ee366bcfCraig McDonnellimport COL.StatAna
916ef74523ecddc8140815c084ab6971ee366bcfCraig McDonnellimport COL.Print_AS ()
916ef74523ecddc8140815c084ab6971ee366bcfCraig McDonnellimport CASL.Sign
916ef74523ecddc8140815c084ab6971ee366bcfCraig McDonnellimport CASL.StaticAna
916ef74523ecddc8140815c084ab6971ee366bcfCraig McDonnellimport CASL.MixfixParser
916ef74523ecddc8140815c084ab6971ee366bcfCraig McDonnellimport CASL.Morphism
916ef74523ecddc8140815c084ab6971ee366bcfCraig McDonnellimport CASL.SymbolMapAnalysis
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellimport CASL.AS_Basic_CASL
fb63998ce7684bddab24e10c0b593809df1b7bffCraig McDonnellimport CASL.Parse_AS_Basic
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellimport CASL.MapSentence
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellimport CASL.SymbolParser
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnellimport CASL.Logic_CASL ()
fb63998ce7684bddab24e10c0b593809df1b7bffCraig McDonnellimport Logic.Logic
415243fbc81341293a852ff6aa14e9608d08685cCraig McDonnell
fb63998ce7684bddab24e10c0b593809df1b7bffCraig McDonnellimport Common.DocUtils
415243fbc81341293a852ff6aa14e9608d08685cCraig McDonnell
fb63998ce7684bddab24e10c0b593809df1b7bffCraig McDonnelldata COL = COL deriving Show
2229ffbfe08c2cd606c305f8934e627548002c9eCraig McDonnell
instance Language COL where
 description _ =
  "COLCASL extends CASL by constructors and observers"

type C_BASIC_SPEC = BASIC_SPEC () COL_SIG_ITEM ()
type CSign = Sign () COLSign
type COLMor = Morphism () COLSign (DefMorExt COLSign)
type COLFORMULA = FORMULA ()

instance SignExtension COLSign where
  isSubSignExtension = isSubCOLSign

instance Syntax COL C_BASIC_SPEC
                Symbol 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

instance Sentences COL COLFORMULA CSign COLMor Symbol where
      map_sen COL m = return . mapSen (const id) m
      sym_of COL = symOf
      symKind COL = show . pretty . symbolKind . symbType
      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

         symbol_to_raw COL = symbolToRaw
         id_to_raw COL = idToRaw
         matches COL = CASL.Morphism.matches

         empty_signature COL = emptySign emptyCOLSign
         signature_union COL sigma1 =
           return . addSig addCOLSign sigma1
         morphism_union COL = plainMorphismUnion addCOLSign
         final_union COL = finalUnion addCOLSign
         is_subsig COL = isSubSig isSubCOLSign
         subsig_inclusion COL = sigInclusion emptyMorExt
         cogenerated_sign COL = cogeneratedSign emptyMorExt
         generated_sign COL = generatedSign emptyMorExt
         induced_from_morphism COL = inducedFromMorphism emptyMorExt
         induced_from_to_morphism COL =
             inducedFromToMorphism emptyMorExt isSubCOLSign diffCOLSign

instance Logic COL ()
               C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CSign
               COLMor
               Symbol RawSymbol () where
         empty_proof_tree _ = ()