{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./ExtModal/Logic_ExtModal.hs
Description :  Instance of class Logic for ExtModal
Copyright   :  DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  non-portable (imports Logic)

Instance of class Logic for ExtModal
-}

module ExtModal.Logic_ExtModal where

import ExtModal.AS_ExtModal
import ExtModal.ExtModalSign
import ExtModal.ATC_ExtModal ()
import ExtModal.Parse_AS
import ExtModal.StatAna
import ExtModal.MorphismExtension
import ExtModal.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.SimplifySen
import CASL.Sublogic
import CASL.SymbolMapAnalysis
import CASL.SymbolParser
import CASL.Taxonomy
import CASL.ToDoc

import Logic.Logic

import Common.DocUtils
import qualified Common.Lib.MapSet as MapSet
import qualified Data.Set as Set

data ExtModal = ExtModal deriving Int -> ExtModal -> ShowS
[ExtModal] -> ShowS
ExtModal -> String
(Int -> ExtModal -> ShowS)
-> (ExtModal -> String) -> ([ExtModal] -> ShowS) -> Show ExtModal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtModal] -> ShowS
$cshowList :: [ExtModal] -> ShowS
show :: ExtModal -> String
$cshow :: ExtModal -> String
showsPrec :: Int -> ExtModal -> ShowS
$cshowsPrec :: Int -> ExtModal -> ShowS
Show

instance Language ExtModal where
        description :: ExtModal -> String
description _ = [String] -> String
unlines
         [ "ExtModal is the 'extended modal logic' extension of CASL. "
         , "Syntax for ordinary modalities, multi-modal logic, dynamic "
         , "logic, graded modal logic, hybrid logic, CTL* and mu-calculus  "
         , "is provided. Specific modal logics can be obtained via "
         , "restrictions to sublanguages."
         ]

type ExtModalSign = Sign EM_FORMULA EModalSign
type ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension
type ExtModalFORMULA = FORMULA EM_FORMULA

instance SignExtension EModalSign where
        isSubSignExtension :: EModalSign -> EModalSign -> Bool
isSubSignExtension = EModalSign -> EModalSign -> Bool
isSubEModalSign

instance Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
        parse_basic_spec :: ExtModal -> Maybe (PrefixMap -> AParser st EM_BASIC_SPEC)
parse_basic_spec ExtModal = (PrefixMap -> AParser st EM_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st EM_BASIC_SPEC)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st EM_BASIC_SPEC)
 -> Maybe (PrefixMap -> AParser st EM_BASIC_SPEC))
-> (PrefixMap -> AParser st EM_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st EM_BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ [String] -> PrefixMap -> AParser st EM_BASIC_SPEC
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [String]
ext_modal_reserved_words
        parse_symb_items :: ExtModal -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items ExtModal = (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]
ext_modal_reserved_words
        parse_symb_map_items :: ExtModal -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items ExtModal =
             (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]
ext_modal_reserved_words

-- Simplification of formulas - simplifySen for ExtFORMULA
simEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
simEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
simEMSen sign :: Sign EM_FORMULA EModalSign
sign = (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> EM_FORMULA -> EM_FORMULA
mapExtForm (Min EM_FORMULA EModalSign
-> (Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA)
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> FORMULA EM_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 EM_FORMULA EModalSign
frmTypeAna Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
simEMSen Sign EM_FORMULA EModalSign
sign)

correctTarget :: Morphism f EModalSign m -> Morphism f EModalSign m
correctTarget :: Morphism f EModalSign m -> Morphism f EModalSign m
correctTarget m :: Morphism f EModalSign m
m = Morphism f EModalSign m
m
  { mtarget :: Sign f EModalSign
mtarget = Sign f EModalSign -> Sign f EModalSign
forall f. Sign f EModalSign -> Sign f EModalSign
correctSign (Sign f EModalSign -> Sign f EModalSign)
-> Sign f EModalSign -> Sign f EModalSign
forall a b. (a -> b) -> a -> b
$ Morphism f EModalSign m -> Sign f EModalSign
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f EModalSign m
m
  , msource :: Sign f EModalSign
msource = Sign f EModalSign -> Sign f EModalSign
forall f. Sign f EModalSign -> Sign f EModalSign
correctSign (Sign f EModalSign -> Sign f EModalSign)
-> Sign f EModalSign -> Sign f EModalSign
forall a b. (a -> b) -> a -> b
$ Morphism f EModalSign m -> Sign f EModalSign
forall f e m. Morphism f e m -> Sign f e
msource Morphism f EModalSign m
m }

instance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol
    where
        map_sen :: ExtModal
-> ExtModalMorph
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
map_sen ExtModal morph :: ExtModalMorph
morph = FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA))
-> (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen EM_FORMULA EModalSign MorphExtension
-> ExtModalMorph -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen EM_FORMULA EModalSign MorphExtension
mapEMform ExtModalMorph
morph
        simplify_sen :: ExtModal
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> FORMULA EM_FORMULA
simplify_sen ExtModal = Min EM_FORMULA EModalSign
-> (Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA)
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> FORMULA EM_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 EM_FORMULA EModalSign
frmTypeAna Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
simEMSen (Sign EM_FORMULA EModalSign
 -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> (Sign EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign)
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> FORMULA EM_FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign
forall f e. Sign f e -> Sign f e
setRevSortRel
        print_named :: ExtModal -> Named (FORMULA EM_FORMULA) -> Doc
print_named ExtModal = Named (FORMULA EM_FORMULA) -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula
        print_sign :: ExtModal -> Sign EM_FORMULA EModalSign -> Doc
print_sign ExtModal sig :: Sign EM_FORMULA EModalSign
sig = let e :: EModalSign
e = Sign EM_FORMULA EModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo Sign EM_FORMULA EModalSign
sig in Sign EM_FORMULA EModalSign -> Doc
forall a. Pretty a => a -> Doc
pretty Sign EM_FORMULA EModalSign
sig
          { opMap :: OpMap
opMap = OpMap -> OpMap -> OpMap
diffOpMapSet (Sign EM_FORMULA EModalSign -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign EM_FORMULA EModalSign
sig) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> OpMap
flexOps EModalSign
e
          , predMap :: PredMap
predMap = (Id -> PredMap -> PredMap) -> PredMap -> Set Id -> PredMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Id -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
`MapSet.delete` PredType
nomPType)
            (PredMap -> PredMap -> PredMap
diffMapSet (Sign EM_FORMULA EModalSign -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign EM_FORMULA EModalSign
sig) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> PredMap
flexPreds EModalSign
e) (Set Id -> PredMap) -> Set Id -> PredMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
nominals EModalSign
e
          }
        sym_of :: ExtModal -> Sign EM_FORMULA EModalSign -> [Set Symbol]
sym_of ExtModal = Sign EM_FORMULA EModalSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
        symKind :: ExtModal -> Symbol -> String
symKind ExtModal = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Symbol -> Doc) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SYMB_KIND -> Doc
forall a. Pretty a => a -> Doc
pretty (SYMB_KIND -> Doc) -> (Symbol -> SYMB_KIND) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbType -> SYMB_KIND
symbolKind (SymbType -> SYMB_KIND)
-> (Symbol -> SymbType) -> Symbol -> SYMB_KIND
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbType
symbType
        symmap_of :: ExtModal -> ExtModalMorph -> EndoMap Symbol
symmap_of ExtModal = ExtModalMorph -> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
        sym_name :: ExtModal -> Symbol -> Id
sym_name ExtModal = Symbol -> Id
symName

instance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
    SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol where
        basic_analysis :: ExtModal
-> Maybe
     ((EM_BASIC_SPEC, Sign EM_FORMULA EModalSign, GlobalAnnos)
      -> Result
           (EM_BASIC_SPEC, ExtSign (Sign EM_FORMULA EModalSign) Symbol,
            [Named (FORMULA EM_FORMULA)]))
basic_analysis ExtModal = ((EM_BASIC_SPEC, Sign EM_FORMULA EModalSign, GlobalAnnos)
 -> Result
      (EM_BASIC_SPEC, ExtSign (Sign EM_FORMULA EModalSign) Symbol,
       [Named (FORMULA EM_FORMULA)]))
-> Maybe
     ((EM_BASIC_SPEC, Sign EM_FORMULA EModalSign, GlobalAnnos)
      -> Result
           (EM_BASIC_SPEC, ExtSign (Sign EM_FORMULA EModalSign) Symbol,
            [Named (FORMULA EM_FORMULA)]))
forall a. a -> Maybe a
Just (EM_BASIC_SPEC, Sign EM_FORMULA EModalSign, GlobalAnnos)
-> Result
     (EM_BASIC_SPEC, ExtSign (Sign EM_FORMULA EModalSign) Symbol,
      [Named (FORMULA EM_FORMULA)])
basicEModalAnalysis
        stat_symb_map_items :: ExtModal
-> Sign EM_FORMULA EModalSign
-> Maybe (Sign EM_FORMULA EModalSign)
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items ExtModal = Sign EM_FORMULA EModalSign
-> Maybe (Sign EM_FORMULA EModalSign)
-> [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 :: ExtModal
-> Sign EM_FORMULA EModalSign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items ExtModal = Sign EM_FORMULA EModalSign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems

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

        empty_signature :: ExtModal -> Sign EM_FORMULA EModalSign
empty_signature ExtModal = EModalSign -> Sign EM_FORMULA EModalSign
forall e f. e -> Sign f e
emptySign EModalSign
emptyEModalSign
        signature_union :: ExtModal
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Result (Sign EM_FORMULA EModalSign)
signature_union ExtModal sgn :: Sign EM_FORMULA EModalSign
sgn = Sign EM_FORMULA EModalSign -> Result (Sign EM_FORMULA EModalSign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign EM_FORMULA EModalSign -> Result (Sign EM_FORMULA EModalSign))
-> (Sign EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign)
-> Sign EM_FORMULA EModalSign
-> Result (Sign EM_FORMULA EModalSign)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EModalSign -> EModalSign -> EModalSign)
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig EModalSign -> EModalSign -> EModalSign
addEModalSign Sign EM_FORMULA EModalSign
sgn
        intersection :: ExtModal
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Result (Sign EM_FORMULA EModalSign)
intersection ExtModal sgn :: Sign EM_FORMULA EModalSign
sgn = Sign EM_FORMULA EModalSign -> Result (Sign EM_FORMULA EModalSign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign EM_FORMULA EModalSign -> Result (Sign EM_FORMULA EModalSign))
-> (Sign EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign)
-> Sign EM_FORMULA EModalSign
-> Result (Sign EM_FORMULA EModalSign)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EModalSign -> EModalSign -> EModalSign)
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
interSig EModalSign -> EModalSign -> EModalSign
interEModalSign Sign EM_FORMULA EModalSign
sgn
        signatureDiff :: ExtModal
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Result (Sign EM_FORMULA EModalSign)
signatureDiff ExtModal sgn :: Sign EM_FORMULA EModalSign
sgn = Sign EM_FORMULA EModalSign -> Result (Sign EM_FORMULA EModalSign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign EM_FORMULA EModalSign -> Result (Sign EM_FORMULA EModalSign))
-> (Sign EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign)
-> Sign EM_FORMULA EModalSign
-> Result (Sign EM_FORMULA EModalSign)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EModalSign -> EModalSign -> EModalSign)
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig EModalSign -> EModalSign -> EModalSign
diffEModalSign Sign EM_FORMULA EModalSign
sgn
        final_union :: ExtModal
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Result (Sign EM_FORMULA EModalSign)
final_union ExtModal = (EModalSign -> EModalSign -> EModalSign)
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Result (Sign EM_FORMULA EModalSign)
forall e f.
(e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion EModalSign -> EModalSign -> EModalSign
addEModalSign
        morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph
morphism_union ExtModal = (EModalSign -> EModalSign -> EModalSign)
-> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph
forall e f m.
(e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion EModalSign -> EModalSign -> EModalSign
addEModalSign
        is_subsig :: ExtModal
-> Sign EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign -> Bool
is_subsig ExtModal = (EModalSign -> EModalSign -> Bool)
-> Sign EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig EModalSign -> EModalSign -> Bool
isSubEModalSign
        subsig_inclusion :: ExtModal
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Result ExtModalMorph
subsig_inclusion ExtModal = MorphExtension
-> Sign EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> Result ExtModalMorph
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion MorphExtension
emptyMorphExtension
        generated_sign :: ExtModal
-> Set Symbol -> Sign EM_FORMULA EModalSign -> Result ExtModalMorph
generated_sign ExtModal s :: Set Symbol
s = (ExtModalMorph -> ExtModalMorph)
-> Result ExtModalMorph -> Result ExtModalMorph
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ExtModalMorph -> ExtModalMorph
forall f m. Morphism f EModalSign m -> Morphism f EModalSign m
correctTarget
          (Result ExtModalMorph -> Result ExtModalMorph)
-> (Sign EM_FORMULA EModalSign -> Result ExtModalMorph)
-> Sign EM_FORMULA EModalSign
-> Result ExtModalMorph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MorphExtension
-> Set Symbol -> Sign EM_FORMULA EModalSign -> Result ExtModalMorph
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign MorphExtension
emptyMorphExtension Set Symbol
s
        cogenerated_sign :: ExtModal
-> Set Symbol -> Sign EM_FORMULA EModalSign -> Result ExtModalMorph
cogenerated_sign ExtModal s :: Set Symbol
s = (ExtModalMorph -> ExtModalMorph)
-> Result ExtModalMorph -> Result ExtModalMorph
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ExtModalMorph -> ExtModalMorph
forall f m. Morphism f EModalSign m -> Morphism f EModalSign m
correctTarget
          (Result ExtModalMorph -> Result ExtModalMorph)
-> (Sign EM_FORMULA EModalSign -> Result ExtModalMorph)
-> Sign EM_FORMULA EModalSign
-> Result ExtModalMorph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MorphExtension
-> Set Symbol -> Sign EM_FORMULA EModalSign -> Result ExtModalMorph
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign MorphExtension
emptyMorphExtension Set Symbol
s
        induced_from_morphism :: ExtModal
-> EndoMap RawSymbol
-> Sign EM_FORMULA EModalSign
-> Result ExtModalMorph
induced_from_morphism ExtModal =
          InducedSign EM_FORMULA EModalSign MorphExtension EModalSign
-> InducedMorphism EModalSign MorphExtension
-> EndoMap RawSymbol
-> Sign EM_FORMULA EModalSign
-> Result ExtModalMorph
forall e f m.
(Pretty e, Show f) =>
InducedSign f e m e
-> InducedMorphism e m
-> EndoMap RawSymbol
-> Sign f e
-> Result (Morphism f e m)
inducedFromMorphismExt InducedSign EM_FORMULA EModalSign MorphExtension EModalSign
inducedEMsign
          (MorphExtension -> InducedMorphism EModalSign MorphExtension
forall m e. m -> InducedMorphism e m
constMorphExt MorphExtension
emptyMorphExtension)
        induced_from_to_morphism :: ExtModal
-> EndoMap RawSymbol
-> ExtSign (Sign EM_FORMULA EModalSign) Symbol
-> ExtSign (Sign EM_FORMULA EModalSign) Symbol
-> Result ExtModalMorph
induced_from_to_morphism ExtModal =
          InducedSign EM_FORMULA EModalSign MorphExtension EModalSign
-> InducedMorphism EModalSign MorphExtension
-> (ExtModalMorph -> ExtModalMorph -> Result MorphExtension)
-> (EModalSign -> EModalSign -> Bool)
-> (EModalSign -> EModalSign -> EModalSign)
-> EndoMap RawSymbol
-> ExtSign (Sign EM_FORMULA EModalSign) Symbol
-> ExtSign (Sign EM_FORMULA EModalSign) Symbol
-> Result ExtModalMorph
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
InducedSign f e m e
-> InducedMorphism e m
-> (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Bool)
-> (e -> e -> e)
-> EndoMap RawSymbol
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphismExt InducedSign EM_FORMULA EModalSign MorphExtension EModalSign
inducedEMsign
          (MorphExtension -> InducedMorphism EModalSign MorphExtension
forall m e. m -> InducedMorphism e m
constMorphExt MorphExtension
emptyMorphExtension)
          (\ _ _ -> MorphExtension -> Result MorphExtension
forall (m :: * -> *) a. Monad m => a -> m a
return MorphExtension
emptyMorphExtension) EModalSign -> EModalSign -> Bool
isSubEModalSign EModalSign -> EModalSign -> EModalSign
diffEModalSign
        theory_to_taxonomy :: ExtModal
-> TaxoGraphKind
-> MMiSSOntology
-> Sign EM_FORMULA EModalSign
-> [Named (FORMULA EM_FORMULA)]
-> Result MMiSSOntology
theory_to_taxonomy ExtModal = TaxoGraphKind
-> MMiSSOntology
-> Sign EM_FORMULA EModalSign
-> [Named (FORMULA EM_FORMULA)]
-> Result MMiSSOntology
forall f e.
TaxoGraphKind
-> MMiSSOntology
-> Sign f e
-> [Named (FORMULA f)]
-> Result MMiSSOntology
convTaxo

instance Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
    SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () where
        stability :: ExtModal -> Stability
stability ExtModal = Stability
Testing
        all_sublogics :: ExtModal -> [ExtModalSL]
all_sublogics ExtModal = [Sublogic] -> [ExtModalSL]
forall a. Lattice a => [a] -> [CASL_SL a]
sublogics_all ([Sublogic] -> [ExtModalSL]) -> [Sublogic] -> [ExtModalSL]
forall a b. (a -> b) -> a -> b
$ Sublogic
foleml Sublogic -> [Sublogic] -> [Sublogic]
forall a. a -> [a] -> [a]
: [[Sublogic]] -> [Sublogic]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Sublogic]]
sublogicsDim
        sublogicDimensions :: ExtModal -> [[ExtModalSL]]
sublogicDimensions ExtModal = [[Sublogic]] -> [[ExtModalSL]]
forall a. Lattice a => [[a]] -> [[CASL_SL a]]
sDims [[Sublogic]]
sublogicsDim
        parseSublogic :: ExtModal -> String -> Maybe ExtModalSL
parseSublogic ExtModal = (String -> Maybe (Sublogic, String)) -> String -> Maybe ExtModalSL
forall a.
(String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a)
parseSL ((String -> Maybe (Sublogic, String))
 -> String -> Maybe ExtModalSL)
-> (String -> Maybe (Sublogic, String))
-> String
-> Maybe ExtModalSL
forall a b. (a -> b) -> a -> b
$ (Sublogic, String) -> Maybe (Sublogic, String)
forall a. a -> Maybe a
Just ((Sublogic, String) -> Maybe (Sublogic, String))
-> (String -> (Sublogic, String))
-> String
-> Maybe (Sublogic, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> (Sublogic, String)
parseSublog
        empty_proof_tree :: ExtModal -> ()
empty_proof_tree ExtModal = ()

instance MinSL Sublogic EM_FORMULA where
    minSL :: EM_FORMULA -> ExtModalSL
minSL = EM_FORMULA -> ExtModalSL
minSublogicOfEM

instance ProjForm Sublogic EM_FORMULA where
    projForm :: ExtModalSL -> EM_FORMULA -> Maybe (FORMULA EM_FORMULA)
projForm _ = FORMULA EM_FORMULA -> Maybe (FORMULA EM_FORMULA)
forall a. a -> Maybe a
Just (FORMULA EM_FORMULA -> Maybe (FORMULA EM_FORMULA))
-> (EM_FORMULA -> FORMULA EM_FORMULA)
-> EM_FORMULA
-> Maybe (FORMULA EM_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EM_FORMULA -> FORMULA EM_FORMULA
forall f. f -> FORMULA f
ExtFORMULA

instance ProjSigItem Sublogic EM_SIG_ITEM EM_FORMULA where
    projSigItems :: ExtModalSL
-> EM_SIG_ITEM -> (Maybe (SIG_ITEMS EM_SIG_ITEM EM_FORMULA), [Id])
projSigItems _ s :: EM_SIG_ITEM
s = (SIG_ITEMS EM_SIG_ITEM EM_FORMULA
-> Maybe (SIG_ITEMS EM_SIG_ITEM EM_FORMULA)
forall a. a -> Maybe a
Just (SIG_ITEMS EM_SIG_ITEM EM_FORMULA
 -> Maybe (SIG_ITEMS EM_SIG_ITEM EM_FORMULA))
-> SIG_ITEMS EM_SIG_ITEM EM_FORMULA
-> Maybe (SIG_ITEMS EM_SIG_ITEM EM_FORMULA)
forall a b. (a -> b) -> a -> b
$ EM_SIG_ITEM -> SIG_ITEMS EM_SIG_ITEM EM_FORMULA
forall s f. s -> SIG_ITEMS s f
Ext_SIG_ITEMS EM_SIG_ITEM
s, [])

instance ProjBasic Sublogic EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA where
    projBasicItems :: ExtModalSL
-> EM_BASIC_ITEM
-> (Maybe (BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA), [Id])
projBasicItems _ b :: EM_BASIC_ITEM
b = (BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA
-> Maybe (BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA)
forall a. a -> Maybe a
Just (BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA
 -> Maybe (BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA))
-> BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA
-> Maybe (BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA)
forall a b. (a -> b) -> a -> b
$ EM_BASIC_ITEM -> BASIC_ITEMS EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA
forall b s f. b -> BASIC_ITEMS b s f
Ext_BASIC_ITEMS EM_BASIC_ITEM
b, [])

instance MinSL Sublogic EM_SIG_ITEM where
    minSL :: EM_SIG_ITEM -> ExtModalSL
minSL = [ExtModalSL] -> ExtModalSL
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([ExtModalSL] -> ExtModalSL)
-> (EM_SIG_ITEM -> [ExtModalSL]) -> EM_SIG_ITEM -> ExtModalSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EM_SIG_ITEM -> [ExtModalSL]
minSLExtSigItem

instance MinSL Sublogic EM_BASIC_ITEM where
    minSL :: EM_BASIC_ITEM -> ExtModalSL
minSL = EM_BASIC_ITEM -> ExtModalSL
minSublogicEMBasic

instance MinSL Sublogic EModalSign where
    minSL :: EModalSign -> ExtModalSL
minSL = EModalSign -> ExtModalSL
minSublogicEMSign

instance NameSL Sublogic where
    nameSL :: Sublogic -> String
nameSL = Sublogic -> String
sublogName