{-# 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)

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 $ symbItems modal_reserved_words
    parse_symb_map_items Modal = Just $ 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
               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 ()
               Symbol RawSymbol () where
         stability _ = Testing
         empty_proof_tree _ = ()