{-# LANGUAGE MultiParamTypeClasses, DeriveDataTypeable #-}
{- |
Module      :  ./ExtModal/MorphismExtension.hs
Description :  Morphism extension for modal signature morphisms
Copyright   :  DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  codruta.liliana@gmail.com
Stability   :  experimental
Portability :  portable

-}

module ExtModal.MorphismExtension where

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

import CASL.Morphism
import CASL.Sign
import CASL.MapSentence

import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Utils
import qualified Common.Lib.MapSet as MapSet

import ExtModal.ExtModalSign
import ExtModal.AS_ExtModal
import ExtModal.Print_AS ()

data MorphExtension = MorphExtension
        { MorphExtension -> Map Id Id
mod_map :: Map.Map Id Id
        , MorphExtension -> Map Id Id
nom_map :: Map.Map Id Id
        } deriving (Int -> MorphExtension -> ShowS
[MorphExtension] -> ShowS
MorphExtension -> String
(Int -> MorphExtension -> ShowS)
-> (MorphExtension -> String)
-> ([MorphExtension] -> ShowS)
-> Show MorphExtension
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MorphExtension] -> ShowS
$cshowList :: [MorphExtension] -> ShowS
show :: MorphExtension -> String
$cshow :: MorphExtension -> String
showsPrec :: Int -> MorphExtension -> ShowS
$cshowsPrec :: Int -> MorphExtension -> ShowS
Show, MorphExtension -> MorphExtension -> Bool
(MorphExtension -> MorphExtension -> Bool)
-> (MorphExtension -> MorphExtension -> Bool) -> Eq MorphExtension
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MorphExtension -> MorphExtension -> Bool
$c/= :: MorphExtension -> MorphExtension -> Bool
== :: MorphExtension -> MorphExtension -> Bool
$c== :: MorphExtension -> MorphExtension -> Bool
Eq, Eq MorphExtension
Eq MorphExtension =>
(MorphExtension -> MorphExtension -> Ordering)
-> (MorphExtension -> MorphExtension -> Bool)
-> (MorphExtension -> MorphExtension -> Bool)
-> (MorphExtension -> MorphExtension -> Bool)
-> (MorphExtension -> MorphExtension -> Bool)
-> (MorphExtension -> MorphExtension -> MorphExtension)
-> (MorphExtension -> MorphExtension -> MorphExtension)
-> Ord MorphExtension
MorphExtension -> MorphExtension -> Bool
MorphExtension -> MorphExtension -> Ordering
MorphExtension -> MorphExtension -> MorphExtension
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 :: MorphExtension -> MorphExtension -> MorphExtension
$cmin :: MorphExtension -> MorphExtension -> MorphExtension
max :: MorphExtension -> MorphExtension -> MorphExtension
$cmax :: MorphExtension -> MorphExtension -> MorphExtension
>= :: MorphExtension -> MorphExtension -> Bool
$c>= :: MorphExtension -> MorphExtension -> Bool
> :: MorphExtension -> MorphExtension -> Bool
$c> :: MorphExtension -> MorphExtension -> Bool
<= :: MorphExtension -> MorphExtension -> Bool
$c<= :: MorphExtension -> MorphExtension -> Bool
< :: MorphExtension -> MorphExtension -> Bool
$c< :: MorphExtension -> MorphExtension -> Bool
compare :: MorphExtension -> MorphExtension -> Ordering
$ccompare :: MorphExtension -> MorphExtension -> Ordering
$cp1Ord :: Eq MorphExtension
Ord, Typeable, Typeable MorphExtension
Constr
DataType
Typeable MorphExtension =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> MorphExtension -> c MorphExtension)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c MorphExtension)
-> (MorphExtension -> Constr)
-> (MorphExtension -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c MorphExtension))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c MorphExtension))
-> ((forall b. Data b => b -> b)
    -> MorphExtension -> MorphExtension)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> MorphExtension -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> MorphExtension -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> MorphExtension -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> MorphExtension -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> MorphExtension -> m MorphExtension)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> MorphExtension -> m MorphExtension)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> MorphExtension -> m MorphExtension)
-> Data MorphExtension
MorphExtension -> Constr
MorphExtension -> DataType
(forall b. Data b => b -> b) -> MorphExtension -> MorphExtension
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MorphExtension -> c MorphExtension
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MorphExtension
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> MorphExtension -> u
forall u. (forall d. Data d => d -> u) -> MorphExtension -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MorphExtension -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MorphExtension -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MorphExtension -> m MorphExtension
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MorphExtension -> m MorphExtension
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MorphExtension
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MorphExtension -> c MorphExtension
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MorphExtension)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MorphExtension)
$cMorphExtension :: Constr
$tMorphExtension :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> MorphExtension -> m MorphExtension
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MorphExtension -> m MorphExtension
gmapMp :: (forall d. Data d => d -> m d)
-> MorphExtension -> m MorphExtension
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MorphExtension -> m MorphExtension
gmapM :: (forall d. Data d => d -> m d)
-> MorphExtension -> m MorphExtension
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MorphExtension -> m MorphExtension
gmapQi :: Int -> (forall d. Data d => d -> u) -> MorphExtension -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> MorphExtension -> u
gmapQ :: (forall d. Data d => d -> u) -> MorphExtension -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> MorphExtension -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MorphExtension -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MorphExtension -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MorphExtension -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MorphExtension -> r
gmapT :: (forall b. Data b => b -> b) -> MorphExtension -> MorphExtension
$cgmapT :: (forall b. Data b => b -> b) -> MorphExtension -> MorphExtension
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MorphExtension)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MorphExtension)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c MorphExtension)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MorphExtension)
dataTypeOf :: MorphExtension -> DataType
$cdataTypeOf :: MorphExtension -> DataType
toConstr :: MorphExtension -> Constr
$ctoConstr :: MorphExtension -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MorphExtension
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MorphExtension
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MorphExtension -> c MorphExtension
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MorphExtension -> c MorphExtension
$cp1Data :: Typeable MorphExtension
Data)

emptyMorphExtension :: MorphExtension
emptyMorphExtension :: MorphExtension
emptyMorphExtension = Map Id Id -> Map Id Id -> MorphExtension
MorphExtension Map Id Id
forall k a. Map k a
Map.empty Map Id Id
forall k a. Map k a
Map.empty

instance Pretty MorphExtension where
        pretty :: MorphExtension -> Doc
pretty me :: MorphExtension
me = Map Id Id -> Doc
forall a. Pretty a => a -> Doc
pretty (MorphExtension -> Map Id Id
mod_map MorphExtension
me) Doc -> Doc -> Doc
$+$ Map Id Id -> Doc
forall a. Pretty a => a -> Doc
pretty (MorphExtension -> Map Id Id
nom_map MorphExtension
me)

instance MorphismExtension EModalSign MorphExtension where
        ideMorphismExtension :: EModalSign -> MorphExtension
ideMorphismExtension _ = MorphExtension
emptyMorphExtension
        composeMorphismExtension :: Morphism f EModalSign MorphExtension
-> Morphism f EModalSign MorphExtension -> Result MorphExtension
composeMorphismExtension fme1 :: Morphism f EModalSign MorphExtension
fme1 fme2 :: Morphism f EModalSign MorphExtension
fme2 = let
          me1 :: MorphExtension
me1 = Morphism f EModalSign MorphExtension -> MorphExtension
forall f e m. Morphism f e m -> m
extended_map Morphism f EModalSign MorphExtension
fme1
          me2 :: MorphExtension
me2 = Morphism f EModalSign MorphExtension -> MorphExtension
forall f e m. Morphism f e m -> m
extended_map Morphism f EModalSign MorphExtension
fme2
          src :: Sign f EModalSign
src = Morphism f EModalSign MorphExtension -> Sign f EModalSign
forall f e m. Morphism f e m -> Sign f e
msource Morphism f EModalSign MorphExtension
fme1
          mSrc :: EModalSign
mSrc = Sign f EModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo Sign f EModalSign
src
          in MorphExtension -> Result MorphExtension
forall (m :: * -> *) a. Monad m => a -> m a
return (MorphExtension -> Result MorphExtension)
-> MorphExtension -> Result MorphExtension
forall a b. (a -> b) -> a -> b
$ Map Id Id -> Map Id Id -> MorphExtension
MorphExtension
             (Map Id Id -> Map Id Id -> Map Id Id -> Map Id Id
forall a b. Ord a => Map a b -> Map a a -> Map a a -> Map a a
composeMap (Set Id -> Map Id Id
forall a. Ord a => Set a -> Map a a
MapSet.setToMap (Set Id -> Map Id Id) -> Set Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
modalities EModalSign
mSrc) (MorphExtension -> Map Id Id
mod_map MorphExtension
me1)
             (Map Id Id -> Map Id Id) -> Map Id Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ MorphExtension -> Map Id Id
mod_map MorphExtension
me2)
             (Map Id Id -> MorphExtension) -> Map Id Id -> MorphExtension
forall a b. (a -> b) -> a -> b
$ Map Id Id -> Map Id Id -> Map Id Id -> Map Id Id
forall a b. Ord a => Map a b -> Map a a -> Map a a -> Map a a
composeMap (Set Id -> Map Id Id
forall a. Ord a => Set a -> Map a a
MapSet.setToMap (Set Id -> Map Id Id) -> Set Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
nominals EModalSign
mSrc) (MorphExtension -> Map Id Id
nom_map MorphExtension
me1)
             (Map Id Id -> Map Id Id) -> Map Id Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ MorphExtension -> Map Id Id
nom_map MorphExtension
me2
        -- ignore inverses
        isInclusionMorphismExtension :: MorphExtension -> Bool
isInclusionMorphismExtension me :: MorphExtension
me =
                Map Id Id -> Bool
forall k a. Map k a -> Bool
Map.null (MorphExtension -> Map Id Id
mod_map MorphExtension
me) Bool -> Bool -> Bool
&& Map Id Id -> Bool
forall k a. Map k a -> Bool
Map.null (MorphExtension -> Map Id Id
nom_map MorphExtension
me)

inducedEMsign :: InducedSign EM_FORMULA EModalSign MorphExtension EModalSign
inducedEMsign :: InducedSign EM_FORMULA EModalSign MorphExtension EModalSign
inducedEMsign sm :: Map Id Id
sm om :: Op_map
om pm :: Pred_map
pm m :: MorphExtension
m sig :: Sign EM_FORMULA EModalSign
sig =
  let ms :: EModalSign
ms = Sign EM_FORMULA EModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo Sign EM_FORMULA EModalSign
sig
      mods :: Map Id Id
mods = MorphExtension -> Map Id Id
mod_map MorphExtension
m
      tmods :: Set Id
tmods = EModalSign -> Set Id
termMods EModalSign
ms
      msm :: Id -> Id
msm i :: Id
i = Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i
        (Map Id Id -> Id) -> Map Id Id -> Id
forall a b. (a -> b) -> a -> b
$ if Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i Set Id
tmods then Map Id Id
sm else Map Id Id
mods
  in EModalSign
ms
  { flexOps :: OpMap
flexOps = Map Id Id -> Op_map -> OpMap -> OpMap
inducedOpMap Map Id Id
sm Op_map
om (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> OpMap
flexOps EModalSign
ms
  , flexPreds :: PredMap
flexPreds = Map Id Id -> Pred_map -> PredMap -> PredMap
inducedPredMap Map Id Id
sm Pred_map
pm (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> PredMap
flexPreds EModalSign
ms
  , modalities :: Set Id
modalities = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Id
msm (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
modalities EModalSign
ms
  , timeMods :: Set Id
timeMods = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Id
msm (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
timeMods EModalSign
ms
  , termMods :: Set Id
termMods = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ i :: Id
i -> Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i Map Id Id
sm) Set Id
tmods
  , nominals :: Set Id
nominals = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ i :: Id
i -> Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i (Map Id Id -> Id) -> Map Id Id -> Id
forall a b. (a -> b) -> a -> b
$ MorphExtension -> Map Id Id
nom_map MorphExtension
m)
    (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
nominals EModalSign
ms
  }

mapEMmod :: Morphism EM_FORMULA EModalSign MorphExtension -> MODALITY
  -> MODALITY
mapEMmod :: Morphism EM_FORMULA EModalSign MorphExtension
-> MODALITY -> MODALITY
mapEMmod morph :: Morphism EM_FORMULA EModalSign MorphExtension
morph tm :: MODALITY
tm = case MODALITY
tm of
  SimpleMod sm :: SIMPLE_ID
sm -> case Id -> Map Id Id -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SIMPLE_ID -> Id
simpleIdToId SIMPLE_ID
sm) (Map Id Id -> Maybe Id) -> Map Id Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ MorphExtension -> Map Id Id
mod_map
      (MorphExtension -> Map Id Id) -> MorphExtension -> Map Id Id
forall a b. (a -> b) -> a -> b
$ Morphism EM_FORMULA EModalSign MorphExtension -> MorphExtension
forall f e m. Morphism f e m -> m
extended_map Morphism EM_FORMULA EModalSign MorphExtension
morph of
    Just ni :: Id
ni -> SIMPLE_ID -> MODALITY
SimpleMod (SIMPLE_ID -> MODALITY) -> SIMPLE_ID -> MODALITY
forall a b. (a -> b) -> a -> b
$ Id -> SIMPLE_ID
idToSimpleId Id
ni
    Nothing -> MODALITY
tm
  ModOp o :: ModOp
o tm1 :: MODALITY
tm1 tm2 :: MODALITY
tm2 -> ModOp -> MODALITY -> MODALITY -> MODALITY
ModOp ModOp
o (Morphism EM_FORMULA EModalSign MorphExtension
-> MODALITY -> MODALITY
mapEMmod Morphism EM_FORMULA EModalSign MorphExtension
morph MODALITY
tm1) (MODALITY -> MODALITY) -> MODALITY -> MODALITY
forall a b. (a -> b) -> a -> b
$ Morphism EM_FORMULA EModalSign MorphExtension
-> MODALITY -> MODALITY
mapEMmod Morphism EM_FORMULA EModalSign MorphExtension
morph MODALITY
tm2
  TransClos tm1 :: MODALITY
tm1 -> MODALITY -> MODALITY
TransClos (MODALITY -> MODALITY) -> MODALITY -> MODALITY
forall a b. (a -> b) -> a -> b
$ Morphism EM_FORMULA EModalSign MorphExtension
-> MODALITY -> MODALITY
mapEMmod Morphism EM_FORMULA EModalSign MorphExtension
morph MODALITY
tm1
  Guard frm :: FORMULA EM_FORMULA
frm -> FORMULA EM_FORMULA -> MODALITY
Guard (FORMULA EM_FORMULA -> MODALITY) -> FORMULA EM_FORMULA -> MODALITY
forall a b. (a -> b) -> a -> b
$ MapSen EM_FORMULA EModalSign MorphExtension
-> Morphism EM_FORMULA EModalSign MorphExtension
-> 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 Morphism EM_FORMULA EModalSign MorphExtension
morph FORMULA EM_FORMULA
frm
  TermMod trm :: TERM EM_FORMULA
trm -> TERM EM_FORMULA -> MODALITY
TermMod (TERM EM_FORMULA -> MODALITY) -> TERM EM_FORMULA -> MODALITY
forall a b. (a -> b) -> a -> b
$ MapSen EM_FORMULA EModalSign MorphExtension
-> Morphism EM_FORMULA EModalSign MorphExtension
-> TERM EM_FORMULA
-> TERM EM_FORMULA
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
mapTerm MapSen EM_FORMULA EModalSign MorphExtension
mapEMform Morphism EM_FORMULA EModalSign MorphExtension
morph TERM EM_FORMULA
trm

mapEMprefix :: Morphism EM_FORMULA EModalSign MorphExtension -> FormPrefix
  -> FormPrefix
mapEMprefix :: Morphism EM_FORMULA EModalSign MorphExtension
-> FormPrefix -> FormPrefix
mapEMprefix morph :: Morphism EM_FORMULA EModalSign MorphExtension
morph pf :: FormPrefix
pf = case FormPrefix
pf of
  BoxOrDiamond choice :: BoxOp
choice tm :: MODALITY
tm leq_geq :: Bool
leq_geq num :: Int
num ->
    BoxOp -> MODALITY -> Bool -> Int -> FormPrefix
BoxOrDiamond BoxOp
choice (Morphism EM_FORMULA EModalSign MorphExtension
-> MODALITY -> MODALITY
mapEMmod Morphism EM_FORMULA EModalSign MorphExtension
morph MODALITY
tm) Bool
leq_geq Int
num
  _ -> FormPrefix
pf

-- Modal formula mapping via signature morphism
mapEMform :: MapSen EM_FORMULA EModalSign MorphExtension
mapEMform :: MapSen EM_FORMULA EModalSign MorphExtension
mapEMform morph :: Morphism EM_FORMULA EModalSign MorphExtension
morph frm :: EM_FORMULA
frm =
  let rmapf :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
rmapf = MapSen EM_FORMULA EModalSign MorphExtension
-> Morphism EM_FORMULA EModalSign MorphExtension
-> 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 Morphism EM_FORMULA EModalSign MorphExtension
morph
      em :: MorphExtension
em = Morphism EM_FORMULA EModalSign MorphExtension -> MorphExtension
forall f e m. Morphism f e m -> m
extended_map Morphism EM_FORMULA EModalSign MorphExtension
morph
  in case EM_FORMULA
frm of
  PrefixForm p :: FormPrefix
p f :: FORMULA EM_FORMULA
f pos :: Range
pos -> FormPrefix -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
PrefixForm (Morphism EM_FORMULA EModalSign MorphExtension
-> FormPrefix -> FormPrefix
mapEMprefix Morphism EM_FORMULA EModalSign MorphExtension
morph FormPrefix
p) (FORMULA EM_FORMULA -> FORMULA EM_FORMULA
rmapf FORMULA EM_FORMULA
f) Range
pos
  UntilSince choice :: Bool
choice f1 :: FORMULA EM_FORMULA
f1 f2 :: FORMULA EM_FORMULA
f2 pos :: Range
pos -> Bool
-> FORMULA EM_FORMULA -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
UntilSince Bool
choice (FORMULA EM_FORMULA -> FORMULA EM_FORMULA
rmapf FORMULA EM_FORMULA
f1) (FORMULA EM_FORMULA -> FORMULA EM_FORMULA
rmapf FORMULA EM_FORMULA
f2) Range
pos
  ModForm (ModDefn ti :: Bool
ti te :: Bool
te is :: [Annoted Id]
is fs :: [Annoted FrameForm]
fs pos :: Range
pos) -> ModDefn -> EM_FORMULA
ModForm (ModDefn -> EM_FORMULA) -> ModDefn -> EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool -> [Annoted Id] -> [Annoted FrameForm] -> Range -> ModDefn
ModDefn Bool
ti Bool
te
    ((Annoted Id -> Annoted Id) -> [Annoted Id] -> [Annoted Id]
forall a b. (a -> b) -> [a] -> [b]
map ((Id -> Id) -> Annoted Id -> Annoted Id
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Id -> Id) -> Annoted Id -> Annoted Id)
-> (Id -> Id) -> Annoted Id -> Annoted Id
forall a b. (a -> b) -> a -> b
$ \ i :: Id
i -> Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i Id
i
         (Map Id Id -> Id) -> Map Id Id -> Id
forall a b. (a -> b) -> a -> b
$ if Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ Sign EM_FORMULA EModalSign -> Set Id
forall f e. Sign f e -> Set Id
sortSet (Sign EM_FORMULA EModalSign -> Set Id)
-> Sign EM_FORMULA EModalSign -> Set Id
forall a b. (a -> b) -> a -> b
$ Morphism EM_FORMULA EModalSign MorphExtension
-> Sign EM_FORMULA EModalSign
forall f e m. Morphism f e m -> Sign f e
msource Morphism EM_FORMULA EModalSign MorphExtension
morph then
         Morphism EM_FORMULA EModalSign MorphExtension -> Map Id Id
forall f e m. Morphism f e m -> Map Id Id
sort_map Morphism EM_FORMULA EModalSign MorphExtension
morph else MorphExtension -> Map Id Id
mod_map MorphExtension
em) [Annoted Id]
is)
    ((Annoted FrameForm -> Annoted FrameForm)
-> [Annoted FrameForm] -> [Annoted FrameForm]
forall a b. (a -> b) -> [a] -> [b]
map ((FrameForm -> FrameForm) -> Annoted FrameForm -> Annoted FrameForm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FrameForm -> FrameForm)
 -> Annoted FrameForm -> Annoted FrameForm)
-> (FrameForm -> FrameForm)
-> Annoted FrameForm
-> Annoted FrameForm
forall a b. (a -> b) -> a -> b
$ Morphism EM_FORMULA EModalSign MorphExtension
-> FrameForm -> FrameForm
mapEMframe Morphism EM_FORMULA EModalSign MorphExtension
morph) [Annoted FrameForm]
fs) Range
pos

mapEMframe :: Morphism EM_FORMULA EModalSign MorphExtension -> FrameForm
  -> FrameForm
mapEMframe :: Morphism EM_FORMULA EModalSign MorphExtension
-> FrameForm -> FrameForm
mapEMframe morph :: Morphism EM_FORMULA EModalSign MorphExtension
morph (FrameForm vs :: [VAR_DECL]
vs fs :: [Annoted (FORMULA EM_FORMULA)]
fs r :: Range
r) =
    [VAR_DECL] -> [Annoted (FORMULA EM_FORMULA)] -> Range -> FrameForm
FrameForm [VAR_DECL]
vs ((Annoted (FORMULA EM_FORMULA) -> Annoted (FORMULA EM_FORMULA))
-> [Annoted (FORMULA EM_FORMULA)] -> [Annoted (FORMULA EM_FORMULA)]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> Annoted (FORMULA EM_FORMULA) -> Annoted (FORMULA EM_FORMULA)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
 -> Annoted (FORMULA EM_FORMULA) -> Annoted (FORMULA EM_FORMULA))
-> (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> Annoted (FORMULA EM_FORMULA)
-> Annoted (FORMULA EM_FORMULA)
forall a b. (a -> b) -> a -> b
$ MapSen EM_FORMULA EModalSign MorphExtension
-> Morphism EM_FORMULA EModalSign MorphExtension
-> 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 Morphism EM_FORMULA EModalSign MorphExtension
morph) [Annoted (FORMULA EM_FORMULA)]
fs) Range
r