content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Modal/Logic_Modal.hs
  Description :  Instance of class Logic for Modal CASL
  Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  luecke@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  portable
  
  Instance of class Logic for modal logic.
  -}
  
  module Modal.Logic_Modal where
  
  import Logic.Logic
  
  import Modal.AS_Modal
  import Modal.ModalSign
  import Modal.ATC_Modal ()
  import Modal.Parse_AS
  import Modal.Print_AS
  import Modal.StatAna
  
  import CASL.Sign
  import CASL.Morphism
  import CASL.SymbolMapAnalysis
  import CASL.AS_Basic_CASL
  import CASL.Parse_AS_Basic
  import CASL.MapSentence
  import CASL.SimplifySen
  import CASL.SymbolParser
  import CASL.Taxonomy
  import CASL.ToDoc
  import CASL.Logic_CASL ()
  
  data Modal = Modal deriving Show
  
  instance Language Modal where
   description _ = unlines
    [ "ModalCASL extends CASL by modal operators."
    , "Syntax for ordinary"
    , "modalities, multi-modal logics as well as  term-modal"
    , "logic (also covering dynamic logic) is provided."
    , "Specific modal logics can be obtained via restrictions to"
    , "sublanguages." ]
  
  type MSign = Sign M_FORMULA ModalSign
  type ModalMor = Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
  type ModalFORMULA = FORMULA M_FORMULA
  
  instance SignExtension ModalSign where
    isSubSignExtension = isSubModalSign
  
  instance Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
      parse_basic_spec Modal = Just $ basicSpec modal_reserved_words
      parse_symb_items Modal = Just . const $ symbItems modal_reserved_words
      parse_symb_map_items Modal = Just . const $ symbMapItems modal_reserved_words
  
  -- Modal logic
  
  map_M_FORMULA :: MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
  map_M_FORMULA mor (BoxOrDiamond b m f ps) =
      let newM = case m of
                     Simple_mod _ -> m
                     Term_mod t -> let newT = mapTerm map_M_FORMULA mor t
                                   in Term_mod newT
          newF = mapSen map_M_FORMULA mor f
      in BoxOrDiamond b newM newF ps
  
  instance Sentences Modal ModalFORMULA MSign ModalMor Symbol where
        map_sen Modal m = return . mapSen map_M_FORMULA m
        sym_of Modal = symOf
        symmap_of Modal = morphismToSymbMap
        sym_name Modal = symName
        simplify_sen Modal = simplifySen minExpForm simModal
        print_sign Modal sig = printSign
            (printModalSign $ simplifySen minExpForm simModal sig) sig
        print_named Modal = printTheoryFormula
  
  -- simplifySen for ExtFORMULA
  simModal :: Sign M_FORMULA ModalSign -> M_FORMULA -> M_FORMULA
  simModal sign (BoxOrDiamond b md form pos) =
      let mod' = case md of
                          Term_mod term -> Term_mod $ rmTypesT minExpForm
                                           simModal sign term
                          t -> t
      in BoxOrDiamond b mod'
                   (simplifySen minExpForm simModal sign form) pos
  
  rmTypesExt :: a -> b -> b
  rmTypesExt _ f = f
  
  instance StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA
                 SYMB_ITEMS SYMB_MAP_ITEMS
                 MSign
                 ModalMor
                 Symbol RawSymbol where
           basic_analysis Modal = Just basicModalAnalysis
           stat_symb_map_items Modal = statSymbMapItems
           stat_symb_items Modal = statSymbItems
  
           symbol_to_raw Modal = symbolToRaw
           id_to_raw Modal = idToRaw
           matches Modal = CASL.Morphism.matches
  
           empty_signature Modal = emptySign emptyModalSign
           signature_union Modal s = return . addSig addModalSign s
           intersection Modal s = return . interSig interModalSign s
           morphism_union Modal = plainMorphismUnion addModalSign
           final_union Modal = finalUnion addModalSign
           is_subsig Modal = isSubSig isSubModalSign
           subsig_inclusion Modal = sigInclusion emptyMorExt
           cogenerated_sign Modal = cogeneratedSign emptyMorExt
           generated_sign Modal = generatedSign emptyMorExt
           induced_from_morphism Modal = inducedFromMorphism emptyMorExt
           induced_from_to_morphism Modal =
               inducedFromToMorphism emptyMorExt isSubModalSign diffModalSign
           theory_to_taxonomy Modal = convTaxo
  
  instance Logic Modal ()
                 M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
                 MSign
                 ModalMor
                 Symbol RawSymbol () where
           stability _ = Testing
           empty_proof_tree _ = ()
  