content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./CoCASL/Logic_CoCASL.hs
  Description :  Instance of class Logic for CoCASL
  Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  hausmann@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  portable
  
  Instance of class Logic for CoCASL.
  -}
  
  module CoCASL.Logic_CoCASL where
  
  import CoCASL.AS_CoCASL
  import CoCASL.ATC_CoCASL ()
  import CoCASL.CoCASLSign
  import CoCASL.Parse_AS
  import CoCASL.StatAna
  import CoCASL.Sublogic
  
  import CASL.AS_Basic_CASL
  import CASL.Logic_CASL
  import CASL.MapSentence
  import CASL.Morphism
  import CASL.Parse_AS_Basic
  import CASL.Sign
  import CASL.Sublogic
  import CASL.SymbolMapAnalysis
  import CASL.SymbolParser
  
  import Data.List
  import Common.DocUtils
  
  import Logic.Logic
  
  data CoCASL = CoCASL deriving Show
  
  instance Language CoCASL where
    description _ = "CoCASL is the coalgebraic extension of CASL."
  
  type CoCASLMor = Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
  type CoCASLFORMULA = FORMULA C_FORMULA
  
  instance SignExtension CoCASLSign where
    isSubSignExtension = isSubCoCASLSign
  
  instance Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
      parse_basic_spec CoCASL = Just $ basicSpec cocasl_reserved_words
      parse_symb_items CoCASL = Just . const $ symbItems cocasl_reserved_words
      parse_symb_map_items CoCASL = Just . const $ symbMapItems cocasl_reserved_words
  
  -- CoCASL logic
  
  map_C_FORMULA :: MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
  map_C_FORMULA mor frm = case frm of
             BoxOrDiamond b m f ps -> let
                newF = mapSen map_C_FORMULA mor f
                newM = case m of
                     Simple_mod _ -> m
                     Term_mod t -> Term_mod $ mapTerm map_C_FORMULA mor t
                in BoxOrDiamond b newM newF ps
             phi -> phi
  
  instance Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol where
        map_sen CoCASL m = return . mapSen map_C_FORMULA m
        sym_of CoCASL = symOf
        symKind CoCASL = show . pretty . symbolKind . symbType
        symmap_of CoCASL = morphismToSymbMap
        sym_name CoCASL = symName
  
  instance StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA
                 SYMB_ITEMS SYMB_MAP_ITEMS
                 CSign
                 CoCASLMor
                 Symbol RawSymbol where
           basic_analysis CoCASL = Just basicCoCASLAnalysis
           sen_analysis CoCASL = Just co_sen_analysis
           stat_symb_map_items CoCASL = statSymbMapItems
           stat_symb_items CoCASL = statSymbItems
  
           symbol_to_raw CoCASL = symbolToRaw
           id_to_raw CoCASL = idToRaw
           matches CoCASL = CASL.Morphism.matches
  
           empty_signature CoCASL = emptySign emptyCoCASLSign
           signature_union CoCASL s = return . addSig addCoCASLSign s
           intersection CoCASL s = return . interSig interCoCASLSign s
           morphism_union CoCASL = plainMorphismUnion addCoCASLSign
           final_union CoCASL = finalUnion addCoCASLSign
           is_subsig CoCASL = isSubSig isSubCoCASLSign
           subsig_inclusion CoCASL = sigInclusion emptyMorExt
           cogenerated_sign CoCASL = cogeneratedSign emptyMorExt
           generated_sign CoCASL = generatedSign emptyMorExt
           induced_from_morphism CoCASL = inducedFromMorphism emptyMorExt
           induced_from_to_morphism CoCASL =
               inducedFromToMorphism emptyMorExt isSubCoCASLSign diffCoCASLSign
  
  instance NameSL Bool where
      nameSL b = if b then "Co" else ""
  
  instance MinSL Bool C_FORMULA where
      minSL = minFormSublogic
  
  instance MinSL Bool C_SIG_ITEM where
      minSL = minCSigItem
  
  instance MinSL Bool C_BASIC_ITEM where
      minSL = minCBaseItem
  
  instance MinSL Bool CoCASLSign where
      minSL = const bottom
  
  instance ProjForm Bool C_FORMULA where
      projForm _ = Just . ExtFORMULA
  
  instance ProjSigItem Bool C_SIG_ITEM C_FORMULA where
      projSigItems _ s = (Just $ Ext_SIG_ITEMS s, [])
  
  instance ProjBasic Bool C_BASIC_ITEM C_SIG_ITEM C_FORMULA where
      projBasicItems _ b = (Just $ Ext_BASIC_ITEMS b, [])
  
  instance Logic CoCASL CoCASL_Sublogics
                 C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
                 CSign
                 CoCASLMor
                 Symbol RawSymbol () where
           parse_basic_sen CoCASL = Just $ const parseSen
           stability CoCASL = Testing
           proj_sublogic_epsilon CoCASL = pr_epsilon emptyMorExt
           all_sublogics CoCASL = sublogics_all [True]
           sublogicDimensions CoCASL = sDims [[True]]
           parseSublogic CoCASL = parseSL parseCo
           empty_proof_tree CoCASL = ()
  
  parseCo :: String -> Maybe (Bool, String)
  parseCo s = case stripPrefix "Co" s of
    Just r | not $ isPrefixOf "nd" r -> Just (True, r)
    _ -> Just (False, s)
  