{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/Modal2CASL.hs
Copyright   :  (c) Klaus Luettich, Uni Bremen 2004, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt

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

The possible world encoding comorphism from ModalCASL to CASL.

   We use the Relational Translation by adding one extra parameter of
   type world to each predicate.

-}

module Comorphisms.Modal2CASL (Modal2CASL (..)) where

import Logic.Logic
import Logic.Comorphism

import Common.AS_Annotation
import Common.Id
import Common.ProofTree
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

-- CASL
import CASL.Logic_CASL
import CASL.Sublogic as SL
import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Morphism
import CASL.World

-- ModalCASL
import Modal.Logic_Modal
import Modal.AS_Modal
import Modal.ModalSign
import Modal.Utils

-- generated function
import Modal.ModalSystems

import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe

-- | The identity of the comorphism
data Modal2CASL = Modal2CASL deriving (Int -> Modal2CASL -> ShowS
[Modal2CASL] -> ShowS
Modal2CASL -> String
(Int -> Modal2CASL -> ShowS)
-> (Modal2CASL -> String)
-> ([Modal2CASL] -> ShowS)
-> Show Modal2CASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Modal2CASL] -> ShowS
$cshowList :: [Modal2CASL] -> ShowS
show :: Modal2CASL -> String
$cshow :: Modal2CASL -> String
showsPrec :: Int -> Modal2CASL -> ShowS
$cshowsPrec :: Int -> Modal2CASL -> ShowS
Show)

instance Language Modal2CASL -- default definition is okay

instance Comorphism Modal2CASL
               Modal ()
               M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               MSign
               ModalMor
               Symbol RawSymbol ()
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree where
    sourceLogic :: Modal2CASL -> Modal
sourceLogic Modal2CASL = Modal
Modal
    sourceSublogic :: Modal2CASL -> ()
sourceSublogic Modal2CASL = ()
    targetLogic :: Modal2CASL -> CASL
targetLogic Modal2CASL = CASL
CASL
    mapSublogic :: Modal2CASL -> () -> Maybe CASL_Sublogics
mapSublogic Modal2CASL _ = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop
      { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub
      , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
NoSortGen
      } -- to support going to SPASS
    map_theory :: Modal2CASL
-> (MSign, [Named ModalFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory (Modal2CASL
Modal2CASL) (sig :: MSign
sig, sens :: [Named ModalFORMULA]
sens) = case MSign -> ModMapEnv
transSig MSign
sig of
      mme :: ModMapEnv
mme -> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (ModMapEnv -> CASLSign
caslSign ModMapEnv
mme, ModMapEnv -> [Named CASLFORMULA]
relFormulas ModMapEnv
mme
                     [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ (Named ModalFORMULA -> Named CASLFORMULA)
-> [Named ModalFORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((ModalFORMULA -> CASLFORMULA)
-> Named ModalFORMULA -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((ModalFORMULA -> CASLFORMULA)
 -> Named ModalFORMULA -> Named CASLFORMULA)
-> (ModalFORMULA -> CASLFORMULA)
-> Named ModalFORMULA
-> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ MSign -> ModalFORMULA -> CASLFORMULA
transSen MSign
sig) [Named ModalFORMULA]
sens)
    map_morphism :: Modal2CASL -> ModalMor -> Result CASLMor
map_morphism Modal2CASL = CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLMor -> Result CASLMor)
-> (ModalMor -> CASLMor) -> ModalMor -> Result CASLMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModalMor -> CASLMor
mapMor
    map_sentence :: Modal2CASL -> MSign -> ModalFORMULA -> Result CASLFORMULA
map_sentence Modal2CASL sig :: MSign
sig = CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> (ModalFORMULA -> CASLFORMULA)
-> ModalFORMULA
-> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MSign -> ModalFORMULA -> CASLFORMULA
transSen MSign
sig
    map_symbol :: Modal2CASL -> MSign -> Symbol -> Set Symbol
map_symbol Modal2CASL _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
mapSym
    has_model_expansion :: Modal2CASL -> Bool
has_model_expansion Modal2CASL = Bool
True
    is_weakly_amalgamable :: Modal2CASL -> Bool
is_weakly_amalgamable Modal2CASL = Bool
True

data ModName = SimpleM SIMPLE_ID
             | SortM SORT
               deriving (Int -> ModName -> ShowS
[ModName] -> ShowS
ModName -> String
(Int -> ModName -> ShowS)
-> (ModName -> String) -> ([ModName] -> ShowS) -> Show ModName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModName] -> ShowS
$cshowList :: [ModName] -> ShowS
show :: ModName -> String
$cshow :: ModName -> String
showsPrec :: Int -> ModName -> ShowS
$cshowsPrec :: Int -> ModName -> ShowS
Show, Eq ModName
Eq ModName =>
(ModName -> ModName -> Ordering)
-> (ModName -> ModName -> Bool)
-> (ModName -> ModName -> Bool)
-> (ModName -> ModName -> Bool)
-> (ModName -> ModName -> Bool)
-> (ModName -> ModName -> ModName)
-> (ModName -> ModName -> ModName)
-> Ord ModName
ModName -> ModName -> Bool
ModName -> ModName -> Ordering
ModName -> ModName -> ModName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ModName -> ModName -> ModName
$cmin :: ModName -> ModName -> ModName
max :: ModName -> ModName -> ModName
$cmax :: ModName -> ModName -> ModName
>= :: ModName -> ModName -> Bool
$c>= :: ModName -> ModName -> Bool
> :: ModName -> ModName -> Bool
$c> :: ModName -> ModName -> Bool
<= :: ModName -> ModName -> Bool
$c<= :: ModName -> ModName -> Bool
< :: ModName -> ModName -> Bool
$c< :: ModName -> ModName -> Bool
compare :: ModName -> ModName -> Ordering
$ccompare :: ModName -> ModName -> Ordering
$cp1Ord :: Eq ModName
Ord, ModName -> ModName -> Bool
(ModName -> ModName -> Bool)
-> (ModName -> ModName -> Bool) -> Eq ModName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModName -> ModName -> Bool
$c/= :: ModName -> ModName -> Bool
== :: ModName -> ModName -> Bool
$c== :: ModName -> ModName -> Bool
Eq)

-- | relations on possible worlds
type ModalityRelMap = Map.Map ModName PRED_NAME

data ModMapEnv = MME
    { ModMapEnv -> CASLSign
caslSign :: CASLSign
    , ModMapEnv -> SORT
worldSort :: SORT
    , ModMapEnv -> ModalityRelMap
modalityRelMap :: ModalityRelMap
    , ModMapEnv -> OpMap
flexiOps :: OpMap
    , ModMapEnv -> PredMap
flexiPreds :: PredMap
    , ModMapEnv -> [Named CASLFORMULA]
relFormulas :: [Named CASLFORMULA] }

transSig :: MSign -> ModMapEnv
transSig :: MSign -> ModMapEnv
transSig sign :: MSign
sign =
   let extInf :: ModalSign
extInf = MSign -> ModalSign
forall f e. Sign f e -> e
extendedInfo MSign
sign
       flexibleOps :: OpMap
flexibleOps = ModalSign -> OpMap
flexOps ModalSign
extInf
       flexiblePreds :: PredMap
flexiblePreds = ModalSign -> PredMap
flexPreds ModalSign
extInf
       fws :: SORT
fws = SORT
world
       flexOps' :: OpMap
flexOps' = SORT -> (SORT -> SORT) -> OpMap -> OpMap
addWorldOp SORT
fws SORT -> SORT
addPlace OpMap
flexibleOps
       flexPreds' :: PredMap
flexPreds' = Map SORT (Set PredType) -> PredMap
forall a b. Ord a => Map a (Set b) -> MapSet a b
MapSet.fromMap (Map SORT (Set PredType) -> PredMap)
-> (PredMap -> Map SORT (Set PredType)) -> PredMap -> PredMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> ModalityRelMap
-> Map SORT (Set PredType)
-> Map SORT (Set PredType)
forall k.
Bool
-> Map k SORT -> Map SORT (Set PredType) -> Map SORT (Set PredType)
addWorldRels Bool
True ModalityRelMap
relsTermMod
                    (Map SORT (Set PredType) -> Map SORT (Set PredType))
-> (PredMap -> Map SORT (Set PredType))
-> PredMap
-> Map SORT (Set PredType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> ModalityRelMap
-> Map SORT (Set PredType)
-> Map SORT (Set PredType)
forall k.
Bool
-> Map k SORT -> Map SORT (Set PredType) -> Map SORT (Set PredType)
addWorldRels Bool
False ModalityRelMap
relsMod (Map SORT (Set PredType) -> Map SORT (Set PredType))
-> (PredMap -> Map SORT (Set PredType))
-> PredMap
-> Map SORT (Set PredType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredMap -> Map SORT (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap
                    (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ SORT -> (SORT -> SORT) -> PredMap -> PredMap
addWorldPred SORT
fws SORT -> SORT
addPlace PredMap
flexiblePreds
       rigOps' :: OpMap
rigOps' = OpMap -> OpMap -> OpMap
diffOpMapSet (MSign -> OpMap
forall f e. Sign f e -> OpMap
opMap MSign
sign) OpMap
flexibleOps
       rigPreds' :: PredMap
rigPreds' = PredMap -> PredMap -> PredMap
diffMapSet (MSign -> PredMap
forall f e. Sign f e -> PredMap
predMap MSign
sign) PredMap
flexiblePreds
       relations :: ModalityRelMap
relations = ModalityRelMap -> ModalityRelMap -> ModalityRelMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ModalityRelMap
relsMod ModalityRelMap
relsTermMod
       genRels :: (t -> Map k a -> Map k a) -> Map t a -> Map k a
genRels f :: t -> Map k a -> Map k a
f = (t -> a -> Map k a -> Map k a) -> Map k a -> Map t a -> Map k a
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ me :: t
me _ nm :: Map k a
nm -> t -> Map k a -> Map k a
f t
me Map k a
nm) Map k a
forall k a. Map k a
Map.empty
       relSymbS :: SIMPLE_ID -> SORT
relSymbS = Bool -> SORT -> SORT
relName Bool
False (SORT -> SORT) -> (SIMPLE_ID -> SORT) -> SIMPLE_ID -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> SORT
simpleIdToId
       relSymbT :: SORT -> SORT
relSymbT = Bool -> SORT -> SORT
relName Bool
True
       genModFrms :: (k -> a -> [a] -> [a]) -> Map k a -> [a]
genModFrms f :: k -> a -> [a] -> [a]
f = (k -> a -> [a] -> [a]) -> [a] -> Map k a -> [a]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey k -> a -> [a] -> [a]
f []
       modiesInf :: Map SIMPLE_ID [AnModFORM]
modiesInf = ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
extInf
       trmMods :: Map SORT [AnModFORM]
trmMods = ModalSign -> Map SORT [AnModFORM]
termModies ModalSign
extInf
       relsMod :: ModalityRelMap
relsMod = (SIMPLE_ID -> ModalityRelMap -> ModalityRelMap)
-> Map SIMPLE_ID [AnModFORM] -> ModalityRelMap
forall t k a a. (t -> Map k a -> Map k a) -> Map t a -> Map k a
genRels (\ me :: SIMPLE_ID
me nm :: ModalityRelMap
nm -> ModName -> SORT -> ModalityRelMap -> ModalityRelMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SIMPLE_ID -> ModName
SimpleM SIMPLE_ID
me) (SIMPLE_ID -> SORT
relSymbS SIMPLE_ID
me) ModalityRelMap
nm)
                         Map SIMPLE_ID [AnModFORM]
modiesInf
       relsTermMod :: ModalityRelMap
relsTermMod = (SORT -> ModalityRelMap -> ModalityRelMap)
-> Map SORT [AnModFORM] -> ModalityRelMap
forall t k a a. (t -> Map k a -> Map k a) -> Map t a -> Map k a
genRels (\ me :: SORT
me nm :: ModalityRelMap
nm ->
                                  ModName -> SORT -> ModalityRelMap -> ModalityRelMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT -> ModName
SortM SORT
me) (SORT -> SORT
relSymbT SORT
me) ModalityRelMap
nm)
                             Map SORT [AnModFORM]
trmMods
       relModFrms :: [Named CASLFORMULA]
relModFrms = (SIMPLE_ID
 -> [AnModFORM] -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> Map SIMPLE_ID [AnModFORM] -> [Named CASLFORMULA]
forall k a a. (k -> a -> [a] -> [a]) -> Map k a -> [a]
genModFrms (\ me :: SIMPLE_ID
me frms :: [AnModFORM]
frms trFrms :: [Named CASLFORMULA]
trFrms -> [Named CASLFORMULA]
trFrms [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++
                                         ModMapEnv -> SORT -> SORT -> [AnModFORM] -> [Named CASLFORMULA]
transSchemaMFormulas ModMapEnv
partMME
                                                  SORT
fws (SIMPLE_ID -> SORT
relSymbS SIMPLE_ID
me) [AnModFORM]
frms)
                               Map SIMPLE_ID [AnModFORM]
modiesInf
       relTermModFrms :: [Named CASLFORMULA]
relTermModFrms = (SORT -> [AnModFORM] -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> Map SORT [AnModFORM] -> [Named CASLFORMULA]
forall k a a. (k -> a -> [a] -> [a]) -> Map k a -> [a]
genModFrms (\ me :: SORT
me frms :: [AnModFORM]
frms trFrms :: [Named CASLFORMULA]
trFrms -> [Named CASLFORMULA]
trFrms [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++
                                         ModMapEnv -> SORT -> SORT -> [AnModFORM] -> [Named CASLFORMULA]
transSchemaMFormulas ModMapEnv
partMME
                                                  SORT
fws (SORT -> SORT
relSymbT SORT
me) [AnModFORM]
frms)
                               Map SORT [AnModFORM]
trmMods
       addWorldRels :: Bool
-> Map k SORT -> Map SORT (Set PredType) -> Map SORT (Set PredType)
addWorldRels isTermMod :: Bool
isTermMod rels :: Map k SORT
rels mp :: Map SORT (Set PredType)
mp =
              let argSorts :: SORT -> [SORT]
argSorts rs :: SORT
rs = if Bool
isTermMod
                             then [SORT -> SORT
getModTermSort SORT
rs, SORT
fws, SORT
fws]
                             else [SORT
fws, SORT
fws] in
               (SORT -> Map SORT (Set PredType) -> Map SORT (Set PredType))
-> Map SORT (Set PredType) -> Map k SORT -> Map SORT (Set PredType)
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (\ rs :: SORT
rs nm :: Map SORT (Set PredType)
nm -> SORT
-> Set PredType
-> Map SORT (Set PredType)
-> Map SORT (Set PredType)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SORT
rs
                                              (PredType -> Set PredType
forall a. a -> Set a
Set.singleton (PredType -> Set PredType) -> PredType -> Set PredType
forall a b. (a -> b) -> a -> b
$
                                                    [SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ SORT -> [SORT]
argSorts SORT
rs)
                                              Map SORT (Set PredType)
nm)
                        Map SORT (Set PredType)
mp Map k SORT
rels
       partMME :: ModMapEnv
partMME = MME :: CASLSign
-> SORT
-> ModalityRelMap
-> OpMap
-> PredMap
-> [Named CASLFORMULA]
-> ModMapEnv
MME {caslSign :: CASLSign
caslSign =
            (() -> CASLSign
forall e f. e -> Sign f e
emptySign ())
               { sortRel :: Rel SORT
sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
fws (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ MSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel MSign
sign
               , opMap :: OpMap
opMap = OpMap -> OpMap -> OpMap
addOpMapSet OpMap
flexOps' OpMap
rigOps'
               , assocOps :: OpMap
assocOps = OpMap -> OpMap -> OpMap
diffOpMapSet (MSign -> OpMap
forall f e. Sign f e -> OpMap
assocOps MSign
sign) OpMap
flexibleOps
               , predMap :: PredMap
predMap = PredMap -> PredMap -> PredMap
addMapSet PredMap
flexPreds' PredMap
rigPreds'},
         worldSort :: SORT
worldSort = SORT
fws,
         modalityRelMap :: ModalityRelMap
modalityRelMap = ModalityRelMap
relations,
         flexiOps :: OpMap
flexiOps = OpMap
flexibleOps,
         flexiPreds :: PredMap
flexiPreds = PredMap
flexiblePreds,
         relFormulas :: [Named CASLFORMULA]
relFormulas = []}
      in ModMapEnv
partMME { relFormulas :: [Named CASLFORMULA]
relFormulas = [Named CASLFORMULA]
relModFrms [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
relTermModFrms}

mapMor :: ModalMor -> CASLMor
mapMor :: ModalMor -> CASLMor
mapMor m :: ModalMor
m = (() -> CASLSign -> CASLSign -> CASLMor
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism ()
    (ModMapEnv -> CASLSign
caslSign (ModMapEnv -> CASLSign) -> ModMapEnv -> CASLSign
forall a b. (a -> b) -> a -> b
$ MSign -> ModMapEnv
transSig (MSign -> ModMapEnv) -> MSign -> ModMapEnv
forall a b. (a -> b) -> a -> b
$ ModalMor -> MSign
forall f e m. Morphism f e m -> Sign f e
msource ModalMor
m)
    (CASLSign -> CASLMor) -> CASLSign -> CASLMor
forall a b. (a -> b) -> a -> b
$ ModMapEnv -> CASLSign
caslSign (ModMapEnv -> CASLSign) -> ModMapEnv -> CASLSign
forall a b. (a -> b) -> a -> b
$ MSign -> ModMapEnv
transSig (MSign -> ModMapEnv) -> MSign -> ModMapEnv
forall a b. (a -> b) -> a -> b
$ ModalMor -> MSign
forall f e m. Morphism f e m -> Sign f e
mtarget ModalMor
m)
  { sort_map :: Sort_map
sort_map = ModalMor -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map ModalMor
m
  , op_map :: Op_map
op_map = ModalMor -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map ModalMor
m
  , pred_map :: Pred_map
pred_map = ModalMor -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map ModalMor
m }

mapSym :: Symbol -> Symbol
mapSym :: Symbol -> Symbol
mapSym = Symbol -> Symbol
forall a. a -> a
id  -- needs to be changed once modal symbols are added

transSchemaMFormulas :: ModMapEnv -> SORT -> PRED_NAME
                     -> [AnModFORM] -> [Named CASLFORMULA]
transSchemaMFormulas :: ModMapEnv -> SORT -> SORT -> [AnModFORM] -> [Named CASLFORMULA]
transSchemaMFormulas mapEnv :: ModMapEnv
mapEnv fws :: SORT
fws relSymb :: SORT
relSymb =
    (AnModFORM -> Maybe (Named CASLFORMULA))
-> [AnModFORM] -> [Named CASLFORMULA]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (([SIMPLE_ID] -> TERM M_FORMULA -> TERM ())
-> SORT
-> SORT
-> [SIMPLE_ID]
-> AnModFORM
-> Maybe (Named CASLFORMULA)
transSchemaMFormula (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv) SORT
fws SORT
relSymb [SIMPLE_ID]
worldVars)

transSen :: MSign -> ModalFORMULA -> CASLFORMULA
transSen :: MSign -> ModalFORMULA -> CASLFORMULA
transSen msig :: MSign
msig = ModMapEnv -> ModalFORMULA -> CASLFORMULA
mapSenTop (MSign -> ModMapEnv
transSig MSign
msig)

mapSenTop :: ModMapEnv -> ModalFORMULA -> CASLFORMULA
mapSenTop :: ModMapEnv -> ModalFORMULA -> CASLFORMULA
mapSenTop mapEnv :: ModMapEnv
mapEnv@(MME {worldSort :: ModMapEnv -> SORT
worldSort = SORT
fws}) f :: ModalFORMULA
f =
    case ModalFORMULA
f of
    Quantification q :: QUANTIFIER
q@QUANTIFIER
Universal vs :: [VAR_DECL]
vs frm :: ModalFORMULA
frm ps :: Range
ps ->
        QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q (VAR_DECL
qwv VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
vs) (ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen ModMapEnv
mapEnv [SIMPLE_ID]
wvs ModalFORMULA
frm) Range
ps
    f1 :: ModalFORMULA
f1 -> [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
qwv] (ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen ModMapEnv
mapEnv [SIMPLE_ID]
wvs ModalFORMULA
f1)
    where qwv :: VAR_DECL
qwv = SIMPLE_ID -> SORT -> VAR_DECL
mkVarDecl SIMPLE_ID
v1 SORT
fws
          wvs :: [SIMPLE_ID]
wvs@(v1 :: SIMPLE_ID
v1 : _) = [SIMPLE_ID]
worldVars


-- head [VAR] is always the current world variable (for predication)
mapSen :: ModMapEnv -> [VAR] -> ModalFORMULA -> CASLFORMULA
mapSen :: ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen mapEnv :: ModMapEnv
mapEnv@(MME {worldSort :: ModMapEnv -> SORT
worldSort = SORT
fws, flexiPreds :: ModMapEnv -> PredMap
flexiPreds = PredMap
fPreds}) vars :: [SIMPLE_ID]
vars
       f :: ModalFORMULA
f = case ModalFORMULA
f of
           Quantification q :: QUANTIFIER
q vs :: [VAR_DECL]
vs frm :: ModalFORMULA
frm ps :: Range
ps ->
                  QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vs (ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen ModMapEnv
mapEnv [SIMPLE_ID]
vars ModalFORMULA
frm) Range
ps
           Junction j :: Junctor
j fs :: [ModalFORMULA]
fs ps :: Range
ps ->
               Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j ((ModalFORMULA -> CASLFORMULA) -> [ModalFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen ModMapEnv
mapEnv [SIMPLE_ID]
vars) [ModalFORMULA]
fs) Range
ps
           Relation f1 :: ModalFORMULA
f1 c :: Relation
c f2 :: ModalFORMULA
f2 ps :: Range
ps ->
               CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen ModMapEnv
mapEnv [SIMPLE_ID]
vars ModalFORMULA
f1) Relation
c (ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen ModMapEnv
mapEnv [SIMPLE_ID]
vars ModalFORMULA
f2) Range
ps
           Negation frm :: ModalFORMULA
frm ps :: Range
ps -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen ModMapEnv
mapEnv [SIMPLE_ID]
vars ModalFORMULA
frm) Range
ps
           Atom b :: Bool
b ps :: Range
ps -> Bool -> Range -> CASLFORMULA
forall f. Bool -> Range -> FORMULA f
Atom Bool
b Range
ps
           Equation t1 :: TERM M_FORMULA
t1 e :: Equality
e t2 :: TERM M_FORMULA
t2 ps :: Range
ps -> TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
               (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars TERM M_FORMULA
t1) Equality
e (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars TERM M_FORMULA
t2) Range
ps
           Predication pn :: PRED_SYMB
pn as :: [TERM M_FORMULA]
as qs :: Range
qs ->
               let as' :: [TERM ()]
as' = (TERM M_FORMULA -> TERM ()) -> [TERM M_FORMULA] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars) [TERM M_FORMULA]
as
                   fwsTerm :: TERM f
fwsTerm = SIMPLE_ID -> SORT -> TERM f
forall f. SIMPLE_ID -> SORT -> TERM f
mkVarTerm ([SIMPLE_ID] -> SIMPLE_ID
forall a. [a] -> a
head [SIMPLE_ID]
vars) SORT
fws
                   (pn' :: PRED_SYMB
pn', as'' :: [TERM ()]
as'') =
                       case PRED_SYMB
pn of
                       Pred_name _ -> String -> (PRED_SYMB, [TERM ()])
forall a. HasCallStack => String -> a
error "Modal2CASL: untyped predication"
                       Qual_pred_name prn :: SORT
prn pType :: PRED_TYPE
pType@(Pred_type sorts :: [SORT]
sorts pps :: Range
pps) ps :: Range
ps ->
                         let addTup :: (PRED_SYMB, [TERM ()])
addTup = (SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name (SORT -> SORT
addPlace SORT
prn)
                                             ([SORT] -> Range -> PRED_TYPE
Pred_type (SORT
fws SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT]
sorts) Range
pps) Range
ps,
                                       TERM ()
forall f. TERM f
fwsTerm TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: [TERM ()]
as')
                             defTup :: (PRED_SYMB, [TERM ()])
defTup = (PRED_SYMB
pn, [TERM ()]
as') in
                                 if PredType -> Set PredType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (PRED_TYPE -> PredType
toPredType PRED_TYPE
pType)
                                     (Set PredType -> Bool) -> Set PredType -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> PredMap -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
prn PredMap
fPreds
                                     then (PRED_SYMB, [TERM ()])
addTup
                                     else (PRED_SYMB, [TERM ()])
defTup
               in PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
pn' [TERM ()]
as'' Range
qs
           Definedness t :: TERM M_FORMULA
t ps :: Range
ps -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Range -> FORMULA f
Definedness (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars TERM M_FORMULA
t) Range
ps
           Membership t :: TERM M_FORMULA
t ty :: SORT
ty ps :: Range
ps -> TERM () -> SORT -> Range -> CASLFORMULA
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars TERM M_FORMULA
t) SORT
ty Range
ps
           Sort_gen_ax constrs :: [Constraint]
constrs isFree :: Bool
isFree -> [Constraint] -> Bool -> CASLFORMULA
forall f. [Constraint] -> Bool -> FORMULA f
Sort_gen_ax [Constraint]
constrs Bool
isFree
           ExtFORMULA mf :: M_FORMULA
mf -> ModMapEnv -> [SIMPLE_ID] -> M_FORMULA -> CASLFORMULA
mapMSen ModMapEnv
mapEnv [SIMPLE_ID]
vars M_FORMULA
mf
           _ -> String -> CASLFORMULA
forall a. HasCallStack => String -> a
error "Modal2CASL.transSen->mapSen"

mapMSen :: ModMapEnv -> [VAR] -> M_FORMULA -> CASLFORMULA
mapMSen :: ModMapEnv -> [SIMPLE_ID] -> M_FORMULA -> CASLFORMULA
mapMSen mapEnv :: ModMapEnv
mapEnv@(MME {worldSort :: ModMapEnv -> SORT
worldSort = SORT
fws, modalityRelMap :: ModMapEnv -> ModalityRelMap
modalityRelMap = ModalityRelMap
pwRelMap}) vars :: [SIMPLE_ID]
vars f :: M_FORMULA
f
   = let w1 :: SIMPLE_ID
w1 : w2 :: SIMPLE_ID
w2 : tl :: [SIMPLE_ID]
tl = [SIMPLE_ID]
vars
         getRel :: MODALITY -> Map ModName a -> a
getRel mo :: MODALITY
mo =
              a -> ModName -> Map ModName a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                    (String -> a
forall a. HasCallStack => String -> a
error ("Modal2CASL: Undefined modality " String -> ShowS
forall a. [a] -> [a] -> [a]
++ MODALITY -> String
forall a. Show a => a -> String
show MODALITY
mo))
                    (MODALITY -> ModName
modalityToModName MODALITY
mo)
         vw1 :: VAR_DECL
vw1 = SIMPLE_ID -> SORT -> VAR_DECL
mkVarDecl SIMPLE_ID
w1 SORT
fws
         vw2 :: VAR_DECL
vw2 = SIMPLE_ID -> SORT -> VAR_DECL
mkVarDecl SIMPLE_ID
w2 SORT
fws
         mkPredType :: [SORT] -> PRED_TYPE
mkPredType ts :: [SORT]
ts = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
ts Range
nullRange
         joinPreds :: Bool -> FORMULA f -> FORMULA f -> FORMULA f
joinPreds b :: Bool
b t1 :: FORMULA f
t1 t2 :: FORMULA f
t2 = if Bool
b then FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl FORMULA f
t1 FORMULA f
t2 else [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f
t1, FORMULA f
t2]
     in
     case M_FORMULA
f of
     BoxOrDiamond b :: Bool
b moda :: MODALITY
moda f1 :: ModalFORMULA
f1 _ ->
       let rel :: SORT
rel = MODALITY -> ModalityRelMap -> SORT
forall a. MODALITY -> Map ModName a -> a
getRel MODALITY
moda ModalityRelMap
pwRelMap
       in (if Bool
b then [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall else [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist) [VAR_DECL
vw2] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Bool -> CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. Bool -> FORMULA f -> FORMULA f -> FORMULA f
joinPreds Bool
b
       (case MODALITY
moda of
        Simple_mod _ -> PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication
            (SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
rel (PRED_TYPE -> PRED_SYMB) -> PRED_TYPE -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ [SORT] -> PRED_TYPE
mkPredType [SORT
fws, SORT
fws])
            [VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vw1, VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vw2]
        Term_mod t :: TERM M_FORMULA
t -> PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication
            (SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
rel (PRED_TYPE -> PRED_SYMB) -> PRED_TYPE -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ [SORT] -> PRED_TYPE
mkPredType [SORT -> SORT
getModTermSort SORT
rel, SORT
fws, SORT
fws])
            [ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv (SIMPLE_ID
w1 SIMPLE_ID -> [SIMPLE_ID] -> [SIMPLE_ID]
forall a. a -> [a] -> [a]
: [SIMPLE_ID]
tl) TERM M_FORMULA
t, VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vw1, VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vw2]
       ) (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen ModMapEnv
mapEnv (SIMPLE_ID
w2 SIMPLE_ID -> [SIMPLE_ID] -> [SIMPLE_ID]
forall a. a -> [a] -> [a]
: [SIMPLE_ID]
tl) ModalFORMULA
f1

-- head [VAR] is always the current world variable (for Application)
mapTERM :: ModMapEnv -> [VAR] -> TERM M_FORMULA -> TERM ()
mapTERM :: ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM mapEnv :: ModMapEnv
mapEnv@(MME {worldSort :: ModMapEnv -> SORT
worldSort = SORT
fws, flexiOps :: ModMapEnv -> OpMap
flexiOps = OpMap
fOps}) vars :: [SIMPLE_ID]
vars t :: TERM M_FORMULA
t = case TERM M_FORMULA
t of
    Qual_var v :: SIMPLE_ID
v ty :: SORT
ty ps :: Range
ps -> SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
v SORT
ty Range
ps
    Application opsym :: OP_SYMB
opsym as :: [TERM M_FORMULA]
as qs :: Range
qs ->
        let as' :: [TERM ()]
as' = (TERM M_FORMULA -> TERM ()) -> [TERM M_FORMULA] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars) [TERM M_FORMULA]
as
            fwsTerm :: TERM f
fwsTerm = SIMPLE_ID -> SORT -> TERM f
forall f. SIMPLE_ID -> SORT -> TERM f
mkVarTerm ([SIMPLE_ID] -> SIMPLE_ID
forall a. [a] -> a
head [SIMPLE_ID]
vars) SORT
fws
            addFws :: OP_TYPE -> OP_TYPE
addFws (Op_type k :: OpKind
k sorts :: [SORT]
sorts res :: SORT
res pps :: Range
pps) =
                OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
k (SORT
fws SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT]
sorts) SORT
res Range
pps
            (opsym' :: OP_SYMB
opsym', as'' :: [TERM ()]
as'') =
                case OP_SYMB
opsym of
                Op_name _ -> String -> (OP_SYMB, [TERM ()])
forall a. HasCallStack => String -> a
error "Modal2CASL: untyped prdication"
                Qual_op_name on :: SORT
on opType :: OP_TYPE
opType ps :: Range
ps ->
                    let addTup :: (OP_SYMB, [TERM ()])
addTup = (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (SORT -> SORT
addPlace SORT
on)
                                               (OP_TYPE -> OP_TYPE
addFws OP_TYPE
opType) Range
ps,
                                  TERM ()
forall f. TERM f
fwsTerm TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: [TERM ()]
as')
                        defTup :: (OP_SYMB, [TERM ()])
defTup = (OP_SYMB
opsym, [TERM ()]
as') in
                            if OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (OP_TYPE -> OpType
toOpType OP_TYPE
opType)
                                (Set OpType -> Bool) -> Set OpType -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> OpMap -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
on OpMap
fOps
                                then (OP_SYMB, [TERM ()])
addTup
                                else (OP_SYMB, [TERM ()])
defTup
        in OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
opsym' [TERM ()]
as'' Range
qs
    Sorted_term trm :: TERM M_FORMULA
trm ty :: SORT
ty ps :: Range
ps -> TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars TERM M_FORMULA
trm) SORT
ty Range
ps
    Cast trm :: TERM M_FORMULA
trm ty :: SORT
ty ps :: Range
ps -> TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Cast (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars TERM M_FORMULA
trm) SORT
ty Range
ps
    Conditional t1 :: TERM M_FORMULA
t1 f :: ModalFORMULA
f t2 :: TERM M_FORMULA
t2 ps :: Range
ps ->
       TERM () -> CASLFORMULA -> TERM () -> Range -> TERM ()
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars TERM M_FORMULA
t1)
                   (ModMapEnv -> [SIMPLE_ID] -> ModalFORMULA -> CASLFORMULA
mapSen ModMapEnv
mapEnv [SIMPLE_ID]
vars ModalFORMULA
f)
                   (ModMapEnv -> [SIMPLE_ID] -> TERM M_FORMULA -> TERM ()
mapTERM ModMapEnv
mapEnv [SIMPLE_ID]
vars TERM M_FORMULA
t2) Range
ps
    _ -> String -> TERM ()
forall a. HasCallStack => String -> a
error "Modal2CASL.mapTERM"

modalityToModName :: MODALITY -> ModName
modalityToModName :: MODALITY -> ModName
modalityToModName (Simple_mod sid :: SIMPLE_ID
sid) = SIMPLE_ID -> ModName
SimpleM SIMPLE_ID
sid
modalityToModName (Term_mod t :: TERM M_FORMULA
t) =
    case TERM M_FORMULA -> Maybe SORT
forall f. TermExtension f => f -> Maybe SORT
optTermSort TERM M_FORMULA
t of
    Just srt :: SORT
srt -> SORT -> ModName
SortM SORT
srt
    Nothing -> String -> ModName
forall a. HasCallStack => String -> a
error ("Modal2CASL: modalityToModName: Wrong term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TERM M_FORMULA -> String
forall a. Show a => a -> String
show TERM M_FORMULA
t)

-- List of variables for worlds
worldVars :: [SIMPLE_ID]
worldVars :: [SIMPLE_ID]
worldVars = (Int -> SIMPLE_ID) -> [Int] -> [SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int -> SIMPLE_ID
genNumVar "w") [1 ..]