{-# 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 Int -> Modal -> ShowS
[Modal] -> ShowS
Modal -> String
(Int -> Modal -> ShowS)
-> (Modal -> String) -> ([Modal] -> ShowS) -> Show Modal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Modal] -> ShowS
$cshowList :: [Modal] -> ShowS
show :: Modal -> String
$cshow :: Modal -> String
showsPrec :: Int -> Modal -> ShowS
$cshowsPrec :: Int -> Modal -> ShowS
Show

instance Language Modal where
 description :: Modal -> String
description _ = [String] -> String
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 :: ModalSign -> ModalSign -> Bool
isSubSignExtension = ModalSign -> ModalSign -> Bool
isSubModalSign

instance Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
    parse_basic_spec :: Modal -> Maybe (PrefixMap -> AParser st M_BASIC_SPEC)
parse_basic_spec Modal = (PrefixMap -> AParser st M_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st M_BASIC_SPEC)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st M_BASIC_SPEC)
 -> Maybe (PrefixMap -> AParser st M_BASIC_SPEC))
-> (PrefixMap -> AParser st M_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st M_BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ [String] -> PrefixMap -> AParser st M_BASIC_SPEC
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [String]
modal_reserved_words
    parse_symb_items :: Modal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items Modal = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_ITEMS
forall st. [String] -> AParser st SYMB_ITEMS
symbItems [String]
modal_reserved_words
    parse_symb_map_items :: Modal -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items Modal = (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_MAP_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
    -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_MAP_ITEMS
forall st. [String] -> AParser st SYMB_MAP_ITEMS
symbMapItems [String]
modal_reserved_words

-- Modal logic

map_M_FORMULA :: MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
map_M_FORMULA :: MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
map_M_FORMULA mor :: Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
mor (BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA M_FORMULA
f ps :: Range
ps) =
    let newM :: MODALITY
newM = case MODALITY
m of
                   Simple_mod _ -> MODALITY
m
                   Term_mod t :: TERM M_FORMULA
t -> let newT :: TERM M_FORMULA
newT = MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
-> Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> TERM M_FORMULA
-> TERM M_FORMULA
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
mapTerm MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
map_M_FORMULA Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
mor TERM M_FORMULA
t
                                 in TERM M_FORMULA -> MODALITY
Term_mod TERM M_FORMULA
newT
        newF :: FORMULA M_FORMULA
newF = MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
-> Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> FORMULA M_FORMULA
-> FORMULA M_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
map_M_FORMULA Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
mor FORMULA M_FORMULA
f
    in Bool -> MODALITY -> FORMULA M_FORMULA -> Range -> M_FORMULA
BoxOrDiamond Bool
b MODALITY
newM FORMULA M_FORMULA
newF Range
ps

instance Sentences Modal ModalFORMULA MSign ModalMor Symbol where
      map_sen :: Modal
-> Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> FORMULA M_FORMULA
-> Result (FORMULA M_FORMULA)
map_sen Modal m :: Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
m = FORMULA M_FORMULA -> Result (FORMULA M_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA M_FORMULA -> Result (FORMULA M_FORMULA))
-> (FORMULA M_FORMULA -> FORMULA M_FORMULA)
-> FORMULA M_FORMULA
-> Result (FORMULA M_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
-> Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> FORMULA M_FORMULA
-> FORMULA M_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
map_M_FORMULA Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
m
      sym_of :: Modal -> MSign -> [Set Symbol]
sym_of Modal = MSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
      symmap_of :: Modal
-> Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> EndoMap Symbol
symmap_of Modal = Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
      sym_name :: Modal -> Symbol -> Id
sym_name Modal = Symbol -> Id
symName
      simplify_sen :: Modal -> MSign -> FORMULA M_FORMULA -> FORMULA M_FORMULA
simplify_sen Modal = Min M_FORMULA ModalSign
-> (MSign -> M_FORMULA -> M_FORMULA)
-> MSign
-> FORMULA M_FORMULA
-> FORMULA M_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min M_FORMULA ModalSign
minExpForm MSign -> M_FORMULA -> M_FORMULA
simModal
      print_sign :: Modal -> MSign -> Doc
print_sign Modal sig :: MSign
sig = (ModalSign -> Doc) -> MSign -> Doc
forall e f. (e -> Doc) -> Sign f e -> Doc
printSign
          ((FORMULA M_FORMULA -> FORMULA M_FORMULA) -> ModalSign -> Doc
printModalSign ((FORMULA M_FORMULA -> FORMULA M_FORMULA) -> ModalSign -> Doc)
-> (FORMULA M_FORMULA -> FORMULA M_FORMULA) -> ModalSign -> Doc
forall a b. (a -> b) -> a -> b
$ Min M_FORMULA ModalSign
-> (MSign -> M_FORMULA -> M_FORMULA)
-> MSign
-> FORMULA M_FORMULA
-> FORMULA M_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min M_FORMULA ModalSign
minExpForm MSign -> M_FORMULA -> M_FORMULA
simModal MSign
sig) MSign
sig
      print_named :: Modal -> Named (FORMULA M_FORMULA) -> Doc
print_named Modal = Named (FORMULA M_FORMULA) -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula

-- simplifySen for ExtFORMULA
simModal :: Sign M_FORMULA ModalSign -> M_FORMULA -> M_FORMULA
simModal :: MSign -> M_FORMULA -> M_FORMULA
simModal sign :: MSign
sign (BoxOrDiamond b :: Bool
b md :: MODALITY
md form :: FORMULA M_FORMULA
form pos :: Range
pos) =
    let mod' :: MODALITY
mod' = case MODALITY
md of
                        Term_mod term :: TERM M_FORMULA
term -> TERM M_FORMULA -> MODALITY
Term_mod (TERM M_FORMULA -> MODALITY) -> TERM M_FORMULA -> MODALITY
forall a b. (a -> b) -> a -> b
$ Min M_FORMULA ModalSign
-> (MSign -> M_FORMULA -> M_FORMULA)
-> MSign
-> TERM M_FORMULA
-> TERM M_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
rmTypesT Min M_FORMULA ModalSign
minExpForm
                                         MSign -> M_FORMULA -> M_FORMULA
simModal MSign
sign TERM M_FORMULA
term
                        t :: MODALITY
t -> MODALITY
t
    in Bool -> MODALITY -> FORMULA M_FORMULA -> Range -> M_FORMULA
BoxOrDiamond Bool
b MODALITY
mod'
                 (Min M_FORMULA ModalSign
-> (MSign -> M_FORMULA -> M_FORMULA)
-> MSign
-> FORMULA M_FORMULA
-> FORMULA M_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min M_FORMULA ModalSign
minExpForm MSign -> M_FORMULA -> M_FORMULA
simModal MSign
sign FORMULA M_FORMULA
form) Range
pos

rmTypesExt :: a -> b -> b
rmTypesExt :: a -> b -> b
rmTypesExt _ f :: b
f = b
f

instance StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               MSign
               ModalMor
               Symbol RawSymbol where
         basic_analysis :: Modal
-> Maybe
     ((M_BASIC_SPEC, MSign, GlobalAnnos)
      -> Result
           (M_BASIC_SPEC, ExtSign MSign Symbol, [Named (FORMULA M_FORMULA)]))
basic_analysis Modal = ((M_BASIC_SPEC, MSign, GlobalAnnos)
 -> Result
      (M_BASIC_SPEC, ExtSign MSign Symbol, [Named (FORMULA M_FORMULA)]))
-> Maybe
     ((M_BASIC_SPEC, MSign, GlobalAnnos)
      -> Result
           (M_BASIC_SPEC, ExtSign MSign Symbol, [Named (FORMULA M_FORMULA)]))
forall a. a -> Maybe a
Just (M_BASIC_SPEC, MSign, GlobalAnnos)
-> Result
     (M_BASIC_SPEC, ExtSign MSign Symbol, [Named (FORMULA M_FORMULA)])
basicModalAnalysis
         stat_symb_map_items :: Modal
-> MSign
-> Maybe MSign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items Modal = MSign
-> Maybe MSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol)
forall f e.
Sign f e
-> Maybe (Sign f e)
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
statSymbMapItems
         stat_symb_items :: Modal -> MSign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items Modal = MSign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems

         symbol_to_raw :: Modal -> Symbol -> RawSymbol
symbol_to_raw Modal = Symbol -> RawSymbol
symbolToRaw
         id_to_raw :: Modal -> Id -> RawSymbol
id_to_raw Modal = Id -> RawSymbol
idToRaw
         matches :: Modal -> Symbol -> RawSymbol -> Bool
matches Modal = Symbol -> RawSymbol -> Bool
CASL.Morphism.matches

         empty_signature :: Modal -> MSign
empty_signature Modal = ModalSign -> MSign
forall e f. e -> Sign f e
emptySign ModalSign
emptyModalSign
         signature_union :: Modal -> MSign -> MSign -> Result MSign
signature_union Modal s :: MSign
s = MSign -> Result MSign
forall (m :: * -> *) a. Monad m => a -> m a
return (MSign -> Result MSign)
-> (MSign -> MSign) -> MSign -> Result MSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModalSign -> ModalSign -> ModalSign) -> MSign -> MSign -> MSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig ModalSign -> ModalSign -> ModalSign
addModalSign MSign
s
         intersection :: Modal -> MSign -> MSign -> Result MSign
intersection Modal s :: MSign
s = MSign -> Result MSign
forall (m :: * -> *) a. Monad m => a -> m a
return (MSign -> Result MSign)
-> (MSign -> MSign) -> MSign -> Result MSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModalSign -> ModalSign -> ModalSign) -> MSign -> MSign -> MSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
interSig ModalSign -> ModalSign -> ModalSign
interModalSign MSign
s
         morphism_union :: Modal
-> Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
morphism_union Modal = (ModalSign -> ModalSign -> ModalSign)
-> Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
forall e f m.
(e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion ModalSign -> ModalSign -> ModalSign
addModalSign
         final_union :: Modal -> MSign -> MSign -> Result MSign
final_union Modal = (ModalSign -> ModalSign -> ModalSign)
-> MSign -> MSign -> Result MSign
forall e f.
(e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion ModalSign -> ModalSign -> ModalSign
addModalSign
         is_subsig :: Modal -> MSign -> MSign -> Bool
is_subsig Modal = (ModalSign -> ModalSign -> Bool) -> MSign -> MSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig ModalSign -> ModalSign -> Bool
isSubModalSign
         subsig_inclusion :: Modal
-> MSign
-> MSign
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
subsig_inclusion Modal = DefMorExt ModalSign
-> MSign
-> MSign
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion DefMorExt ModalSign
forall e. DefMorExt e
emptyMorExt
         cogenerated_sign :: Modal
-> Set Symbol
-> MSign
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
cogenerated_sign Modal = DefMorExt ModalSign
-> Set Symbol
-> MSign
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign DefMorExt ModalSign
forall e. DefMorExt e
emptyMorExt
         generated_sign :: Modal
-> Set Symbol
-> MSign
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
generated_sign Modal = DefMorExt ModalSign
-> Set Symbol
-> MSign
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign DefMorExt ModalSign
forall e. DefMorExt e
emptyMorExt
         induced_from_morphism :: Modal
-> EndoMap RawSymbol
-> MSign
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
induced_from_morphism Modal = DefMorExt ModalSign
-> EndoMap RawSymbol
-> MSign
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
forall e f m.
(Pretty e, Show f) =>
m -> EndoMap RawSymbol -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism DefMorExt ModalSign
forall e. DefMorExt e
emptyMorExt
         induced_from_to_morphism :: Modal
-> EndoMap RawSymbol
-> ExtSign MSign Symbol
-> ExtSign MSign Symbol
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
induced_from_to_morphism Modal =
             DefMorExt ModalSign
-> (ModalSign -> ModalSign -> Bool)
-> (ModalSign -> ModalSign -> ModalSign)
-> EndoMap RawSymbol
-> ExtSign MSign Symbol
-> ExtSign MSign Symbol
-> Result (Morphism M_FORMULA ModalSign (DefMorExt ModalSign))
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
m
-> (e -> e -> Bool)
-> (e -> e -> e)
-> EndoMap RawSymbol
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphism DefMorExt ModalSign
forall e. DefMorExt e
emptyMorExt ModalSign -> ModalSign -> Bool
isSubModalSign ModalSign -> ModalSign -> ModalSign
diffModalSign
         theory_to_taxonomy :: Modal
-> TaxoGraphKind
-> MMiSSOntology
-> MSign
-> [Named (FORMULA M_FORMULA)]
-> Result MMiSSOntology
theory_to_taxonomy Modal = TaxoGraphKind
-> MMiSSOntology
-> MSign
-> [Named (FORMULA M_FORMULA)]
-> Result MMiSSOntology
forall f e.
TaxoGraphKind
-> MMiSSOntology
-> Sign f e
-> [Named (FORMULA f)]
-> Result MMiSSOntology
convTaxo

instance Logic Modal ()
               M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               MSign
               ModalMor
               Symbol RawSymbol () where
         stability :: Modal -> Stability
stability _ = Stability
Testing
         empty_proof_tree :: Modal -> ()
empty_proof_tree _ = ()