{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
module Comorphisms.ExtModal2ExtModalTotal where
import Logic.Logic
import Logic.Comorphism
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.MapSet as MapSet
import Common.AS_Annotation
import Common.ProofUtils
import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Morphism
import CASL.Sign
import CASL.Simplify
import CASL.Sublogic
import CASL.Utils
import ExtModal.Logic_ExtModal
import ExtModal.AS_ExtModal
import ExtModal.ExtModalSign
import ExtModal.StatAna
import ExtModal.Sublogic as EM
import Comorphisms.CASL2SubCFOL
data ExtModal2ExtModalTotal = ExtModal2ExtModalTotal deriving Int -> ExtModal2ExtModalTotal -> ShowS
[ExtModal2ExtModalTotal] -> ShowS
ExtModal2ExtModalTotal -> String
(Int -> ExtModal2ExtModalTotal -> ShowS)
-> (ExtModal2ExtModalTotal -> String)
-> ([ExtModal2ExtModalTotal] -> ShowS)
-> Show ExtModal2ExtModalTotal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtModal2ExtModalTotal] -> ShowS
$cshowList :: [ExtModal2ExtModalTotal] -> ShowS
show :: ExtModal2ExtModalTotal -> String
$cshow :: ExtModal2ExtModalTotal -> String
showsPrec :: Int -> ExtModal2ExtModalTotal -> ShowS
$cshowsPrec :: Int -> ExtModal2ExtModalTotal -> ShowS
Show
instance Language ExtModal2ExtModalTotal
instance Comorphism ExtModal2ExtModalTotal
ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
Symbol RawSymbol ()
ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
Symbol RawSymbol () where
sourceLogic :: ExtModal2ExtModalTotal -> ExtModal
sourceLogic ExtModal2ExtModalTotal = ExtModal
ExtModal
sourceSublogic :: ExtModal2ExtModalTotal -> ExtModalSL
sourceSublogic ExtModal2ExtModalTotal = Sublogic -> ExtModalSL
forall a. a -> CASL_SL a
mkTop Sublogic
maxSublogic
targetLogic :: ExtModal2ExtModalTotal -> ExtModal
targetLogic ExtModal2ExtModalTotal = ExtModal
ExtModal
mapSublogic :: ExtModal2ExtModalTotal -> ExtModalSL -> Maybe ExtModalSL
mapSublogic ExtModal2ExtModalTotal sl :: ExtModalSL
sl = ExtModalSL -> Maybe ExtModalSL
forall a. a -> Maybe a
Just
(ExtModalSL -> Maybe ExtModalSL) -> ExtModalSL -> Maybe ExtModalSL
forall a b. (a -> b) -> a -> b
$ if ExtModalSL -> Bool
forall a. CASL_SL a -> Bool
has_part ExtModalSL
sl then ExtModalSL
sl
{ has_part :: Bool
has_part = Bool
False
, has_pred :: Bool
has_pred = Bool
True
, which_logic :: CASL_Formulas
which_logic = CASL_Formulas -> CASL_Formulas -> CASL_Formulas
forall a. Ord a => a -> a -> a
max CASL_Formulas
Horn (CASL_Formulas -> CASL_Formulas) -> CASL_Formulas -> CASL_Formulas
forall a b. (a -> b) -> a -> b
$ ExtModalSL -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic ExtModalSL
sl
, has_eq :: Bool
has_eq = Bool
True} else ExtModalSL
sl
map_theory :: ExtModal2ExtModalTotal
-> (ExtModalSign, [Named ExtModalFORMULA])
-> Result (ExtModalSign, [Named ExtModalFORMULA])
map_theory ExtModal2ExtModalTotal (sig :: ExtModalSign
sig, sens :: [Named ExtModalFORMULA]
sens) = let
bsrts :: Set SORT
bsrts = ExtModalSign -> Set SORT
forall f e. Sign f e -> Set SORT
emsortsWithBottom ExtModalSign
sig
sens1 :: [Named ExtModalFORMULA]
sens1 = Bool -> Set SORT -> ExtModalSign -> [Named ExtModalFORMULA]
forall f e.
(Ord f, TermExtension f) =>
Bool -> Set SORT -> Sign f e -> [Named (FORMULA f)]
generateAxioms Bool
True Set SORT
bsrts ExtModalSign
sig
sens2 :: [Named ExtModalFORMULA]
sens2 = (Named ExtModalFORMULA -> Named ExtModalFORMULA)
-> [Named ExtModalFORMULA] -> [Named ExtModalFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((ExtModalFORMULA -> ExtModalFORMULA)
-> Named ExtModalFORMULA -> Named ExtModalFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (ExtModalFORMULA -> ExtModalFORMULA
noCondsEMFormula (ExtModalFORMULA -> ExtModalFORMULA)
-> (ExtModalFORMULA -> ExtModalFORMULA)
-> ExtModalFORMULA
-> ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtModalFORMULA -> ExtModalFORMULA
simplifyEMFormula
(ExtModalFORMULA -> ExtModalFORMULA)
-> (ExtModalFORMULA -> ExtModalFORMULA)
-> ExtModalFORMULA
-> ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> ExtModalFORMULA -> ExtModalFORMULA
codeEMFormula Set SORT
bsrts)) [Named ExtModalFORMULA]
sens
in (ExtModalSign, [Named ExtModalFORMULA])
-> Result (ExtModalSign, [Named ExtModalFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return
( Set SORT -> ExtModalSign -> ExtModalSign
forall f. Set SORT -> Sign f EModalSign -> Sign f EModalSign
emEncodeSig Set SORT
bsrts ExtModalSign
sig
, [Named ExtModalFORMULA] -> [Named ExtModalFORMULA]
forall a. [Named a] -> [Named a]
nameAndDisambiguate ([Named ExtModalFORMULA] -> [Named ExtModalFORMULA])
-> [Named ExtModalFORMULA] -> [Named ExtModalFORMULA]
forall a b. (a -> b) -> a -> b
$ [Named ExtModalFORMULA]
sens1 [Named ExtModalFORMULA]
-> [Named ExtModalFORMULA] -> [Named ExtModalFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named ExtModalFORMULA]
sens2)
map_morphism :: ExtModal2ExtModalTotal -> ExtModalMorph -> Result ExtModalMorph
map_morphism ExtModal2ExtModalTotal mor :: ExtModalMorph
mor@Morphism
{msource :: forall f e m. Morphism f e m -> Sign f e
msource = ExtModalSign
src, mtarget :: forall f e m. Morphism f e m -> Sign f e
mtarget = ExtModalSign
tar}
= ExtModalMorph -> Result ExtModalMorph
forall (m :: * -> *) a. Monad m => a -> m a
return
ExtModalMorph
mor { msource :: ExtModalSign
msource = Set SORT -> ExtModalSign -> ExtModalSign
forall f. Set SORT -> Sign f EModalSign -> Sign f EModalSign
emEncodeSig (ExtModalSign -> Set SORT
forall f e. Sign f e -> Set SORT
emsortsWithBottom ExtModalSign
src) ExtModalSign
src
, mtarget :: ExtModalSign
mtarget = Set SORT -> ExtModalSign -> ExtModalSign
forall f. Set SORT -> Sign f EModalSign -> Sign f EModalSign
emEncodeSig (ExtModalSign -> Set SORT
forall f e. Sign f e -> Set SORT
emsortsWithBottom ExtModalSign
tar) ExtModalSign
tar
, op_map :: Op_map
op_map = ((SORT, OpKind) -> (SORT, OpKind)) -> Op_map -> Op_map
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (i :: SORT
i, _) -> (SORT
i, OpKind
Total)) (Op_map -> Op_map) -> Op_map -> Op_map
forall a b. (a -> b) -> a -> b
$ ExtModalMorph -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map ExtModalMorph
mor }
map_sentence :: ExtModal2ExtModalTotal
-> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA
map_sentence ExtModal2ExtModalTotal sig :: ExtModalSign
sig sen :: ExtModalFORMULA
sen = let
bsrts :: Set SORT
bsrts = ExtModalSign -> Set SORT
forall f e. Sign f e -> Set SORT
emsortsWithBottom ExtModalSign
sig
in ExtModalFORMULA -> Result ExtModalFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtModalFORMULA -> Result ExtModalFORMULA)
-> ExtModalFORMULA -> Result ExtModalFORMULA
forall a b. (a -> b) -> a -> b
$ ExtModalFORMULA -> ExtModalFORMULA
simplifyEMFormula (ExtModalFORMULA -> ExtModalFORMULA)
-> ExtModalFORMULA -> ExtModalFORMULA
forall a b. (a -> b) -> a -> b
$ Set SORT -> ExtModalFORMULA -> ExtModalFORMULA
codeEMFormula Set SORT
bsrts ExtModalFORMULA
sen
map_symbol :: ExtModal2ExtModalTotal -> ExtModalSign -> Symbol -> Set Symbol
map_symbol ExtModal2ExtModalTotal _ s :: Symbol
s =
Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton Symbol
s { symbType :: SymbType
symbType = SymbType -> SymbType
totalizeSymbType (SymbType -> SymbType) -> SymbType -> SymbType
forall a b. (a -> b) -> a -> b
$ Symbol -> SymbType
symbType Symbol
s }
has_model_expansion :: ExtModal2ExtModalTotal -> Bool
has_model_expansion ExtModal2ExtModalTotal = Bool
True
is_weakly_amalgamable :: ExtModal2ExtModalTotal -> Bool
is_weakly_amalgamable ExtModal2ExtModalTotal = Bool
True
emEncodeSig :: Set.Set SORT -> Sign f EModalSign -> Sign f EModalSign
emEncodeSig :: Set SORT -> Sign f EModalSign -> Sign f EModalSign
emEncodeSig bsrts :: Set SORT
bsrts sig :: Sign f EModalSign
sig = (Set SORT -> Sign f EModalSign -> Sign f EModalSign
forall f e. Set SORT -> Sign f e -> Sign f e
encodeSig Set SORT
bsrts Sign f EModalSign
sig)
{ extendedInfo :: EModalSign
extendedInfo = let extInfo :: EModalSign
extInfo = Sign f EModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo Sign f EModalSign
sig in
EModalSign
extInfo { flexOps :: OpMap
flexOps = (OpType -> OpType) -> OpMap -> OpMap
forall b c a.
(Ord b, Ord c) =>
(b -> c) -> MapSet a b -> MapSet a c
MapSet.map OpType -> OpType
mkTotal (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> OpMap
flexOps EModalSign
extInfo }}
emsortsWithBottom :: Sign f e -> Set.Set SORT
emsortsWithBottom :: Sign f e -> Set SORT
emsortsWithBottom sig :: Sign f e
sig = FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
sortsWithBottom FormulaTreatment
NoMembershipOrCast Sign f e
sig Set SORT
forall a. Set a
Set.empty
simplifyEM :: EM_FORMULA -> EM_FORMULA
simplifyEM :: EM_FORMULA -> EM_FORMULA
simplifyEM = (ExtModalFORMULA -> ExtModalFORMULA) -> EM_FORMULA -> EM_FORMULA
mapExtForm ExtModalFORMULA -> ExtModalFORMULA
simplifyEMFormula
simplifyEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
simplifyEMFormula :: ExtModalFORMULA -> ExtModalFORMULA
simplifyEMFormula = (EM_FORMULA -> EM_FORMULA) -> ExtModalFORMULA -> ExtModalFORMULA
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula EM_FORMULA -> EM_FORMULA
simplifyEM
noCondsEM :: EM_FORMULA -> EM_FORMULA
noCondsEM :: EM_FORMULA -> EM_FORMULA
noCondsEM = (ExtModalFORMULA -> ExtModalFORMULA) -> EM_FORMULA -> EM_FORMULA
mapExtForm ExtModalFORMULA -> ExtModalFORMULA
noCondsEMFormula
noCondsEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
noCondsEMFormula :: ExtModalFORMULA -> ExtModalFORMULA
noCondsEMFormula = (EM_FORMULA -> EM_FORMULA) -> ExtModalFORMULA -> ExtModalFORMULA
forall f. Eq f => (f -> f) -> FORMULA f -> FORMULA f
codeOutConditionalF EM_FORMULA -> EM_FORMULA
noCondsEM
codeEM :: Set.Set SORT -> EM_FORMULA -> EM_FORMULA
codeEM :: Set SORT -> EM_FORMULA -> EM_FORMULA
codeEM = (ExtModalFORMULA -> ExtModalFORMULA) -> EM_FORMULA -> EM_FORMULA
mapExtForm ((ExtModalFORMULA -> ExtModalFORMULA) -> EM_FORMULA -> EM_FORMULA)
-> (Set SORT -> ExtModalFORMULA -> ExtModalFORMULA)
-> Set SORT
-> EM_FORMULA
-> EM_FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> ExtModalFORMULA -> ExtModalFORMULA
codeEMFormula
codeEMFormula :: Set.Set SORT -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA
codeEMFormula :: Set SORT -> ExtModalFORMULA -> ExtModalFORMULA
codeEMFormula bsrts :: Set SORT
bsrts = Record EM_FORMULA ExtModalFORMULA (TERM EM_FORMULA)
-> ExtModalFORMULA -> ExtModalFORMULA
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Bool
-> Set SORT
-> (EM_FORMULA -> EM_FORMULA)
-> Record EM_FORMULA ExtModalFORMULA (TERM EM_FORMULA)
forall f.
TermExtension f =>
Bool -> Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)
codeRecord Bool
True Set SORT
bsrts ((EM_FORMULA -> EM_FORMULA)
-> Record EM_FORMULA ExtModalFORMULA (TERM EM_FORMULA))
-> (EM_FORMULA -> EM_FORMULA)
-> Record EM_FORMULA ExtModalFORMULA (TERM EM_FORMULA)
forall a b. (a -> b) -> a -> b
$ Set SORT -> EM_FORMULA -> EM_FORMULA
codeEM Set SORT
bsrts)