{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/ExtModal2ExtModalTotal.hs
Description :  coding out subsorting
Copyright   :  (c) C. Maeder DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

Coding out subsorting (SubPCFOL= -> PCFOL=),
   following Chap. III:3.1 of the CASL Reference Manual
-}

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

-- CASL
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

-- | The identity of the comorphism
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 -- default definition is okay

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 -- partiality is coded out
        , 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)