{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/ExtModal2CASL.hs
Copyright   :  (c) Christian Maeder, DFKI 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (MPTC-FD)
-}

module Comorphisms.ExtModal2CASL (ExtModal2CASL (..)) where

import Logic.Logic
import Logic.Comorphism

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

import qualified Data.Set as Set
import Data.Function
import Data.Maybe

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

-- ExtModalCASL
import ExtModal.Logic_ExtModal
import ExtModal.AS_ExtModal
import ExtModal.ExtModalSign
import ExtModal.Sublogic

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

instance Comorphism ExtModal2CASL
               ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
               SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
               Symbol RawSymbol ()
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree where
    sourceLogic :: ExtModal2CASL -> ExtModal
sourceLogic ExtModal2CASL = ExtModal
ExtModal
    sourceSublogic :: ExtModal2CASL -> ExtModalSL
sourceSublogic ExtModal2CASL = Sublogic -> ExtModalSL
forall a. a -> CASL_SL a
mkTop Sublogic
foleml
    targetLogic :: ExtModal2CASL -> CASL
targetLogic ExtModal2CASL = CASL
CASL
    mapSublogic :: ExtModal2CASL -> ExtModalSL -> Maybe CASL_Sublogics
mapSublogic ExtModal2CASL s :: ExtModalSL
s = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just ExtModalSL
s { ext_features :: ()
ext_features = () }
    map_theory :: ExtModal2CASL
-> (ExtModalSign, [Named ExtModalFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory ExtModal2CASL (sig :: ExtModalSign
sig, sens :: [Named ExtModalFORMULA]
sens) = case ExtModalSign -> CASLSign
transSig ExtModalSign
sig of
      mme :: CASLSign
mme -> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
mme, (Named ExtModalFORMULA -> Named CASLFORMULA)
-> [Named ExtModalFORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((ExtModalFORMULA -> CASLFORMULA)
-> Named ExtModalFORMULA -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((ExtModalFORMULA -> CASLFORMULA)
 -> Named ExtModalFORMULA -> Named CASLFORMULA)
-> (ExtModalFORMULA -> CASLFORMULA)
-> Named ExtModalFORMULA
-> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ ExtModalSign -> CASLSign -> ExtModalFORMULA -> CASLFORMULA
transTop ExtModalSign
sig CASLSign
mme) [Named ExtModalFORMULA]
sens)
    {-
    map_morphism ExtModal2CASL = return . mapMor
    map_sentence ExtModal2CASL sig = return . transSen sig
    map_symbol ExtModal2CASL _ = Set.singleton . mapSym
    -}
    has_model_expansion :: ExtModal2CASL -> Bool
has_model_expansion ExtModal2CASL = Bool
True
    is_weakly_amalgamable :: ExtModal2CASL -> Bool
is_weakly_amalgamable ExtModal2CASL = Bool
True

nomName :: Id -> Id
nomName :: Id -> Id
nomName t :: Id
t = [Token] -> [Id] -> Range -> Id
Id [String -> Token
genToken "N"] [Id
t] (Range -> Id) -> Range -> Id
forall a b. (a -> b) -> a -> b
$ Id -> Range
rangeOfId Id
t

nomOpType :: OpType
nomOpType :: OpType
nomOpType = [Id] -> Id -> OpType
mkTotOpType [] Id
world

-- | add world arguments to flexible ops and preds; and add relations
transSig :: ExtModalSign -> CASLSign
transSig :: ExtModalSign -> CASLSign
transSig sign :: ExtModalSign
sign = let
    s1 :: Sign f ()
s1 = () -> ExtModalSign -> Sign f ()
forall e f1 e1 f. e -> Sign f1 e1 -> Sign f e
embedSign () ExtModalSign
sign
    extInf :: EModalSign
extInf = ExtModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo ExtModalSign
sign
    flexibleOps :: OpMap
flexibleOps = EModalSign -> OpMap
flexOps EModalSign
extInf
    flexiblePreds :: PredMap
flexiblePreds = EModalSign -> PredMap
flexPreds EModalSign
extInf
    flexOps' :: OpMap
flexOps' = Id -> (Id -> Id) -> OpMap -> OpMap
addWorldOp Id
world Id -> Id
addPlace OpMap
flexibleOps
    flexPreds' :: PredMap
flexPreds' = Id -> (Id -> Id) -> PredMap -> PredMap
addWorldPred Id
world Id -> Id
addPlace PredMap
flexiblePreds
    rigOps' :: OpMap
rigOps' = OpMap -> OpMap -> OpMap
diffOpMapSet (ExtModalSign -> OpMap
forall f e. Sign f e -> OpMap
opMap ExtModalSign
sign) OpMap
flexibleOps
    rigPreds' :: PredMap
rigPreds' = PredMap -> PredMap -> PredMap
diffMapSet (ExtModalSign -> PredMap
forall f e. Sign f e -> PredMap
predMap ExtModalSign
sign) PredMap
flexiblePreds
    noms :: Set Id
noms = EModalSign -> Set Id
nominals EModalSign
extInf
    noNomsPreds :: PredMap
noNomsPreds = (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
rigPreds' Set Id
noms
    termMs :: Set Id
termMs = EModalSign -> Set Id
termMods EModalSign
extInf
    rels :: PredMap
rels = (Id -> PredMap -> PredMap) -> PredMap -> Set Id -> PredMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ m :: Id
m ->
      Id -> Bool -> Bool -> Id -> PredMap -> PredMap
insertModPred Id
world Bool
False (Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
m Set Id
termMs) Id
m)
      PredMap
forall a b. MapSet a b
MapSet.empty (Set Id -> PredMap) -> Set Id -> PredMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
modalities EModalSign
extInf
    nomOps :: OpMap
nomOps = (Id -> OpMap -> OpMap) -> OpMap -> Set Id -> OpMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ n :: Id
n -> Id -> OpType -> OpMap -> OpMap
addOpTo (Id -> Id
nomName Id
n) OpType
nomOpType) OpMap
rigOps' Set Id
noms
    in CASLSign
forall f. Sign f ()
s1
    { sortRel :: Rel Id
sortRel = Id -> Rel Id -> Rel Id
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey Id
world (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ ExtModalSign -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel ExtModalSign
sign
    , opMap :: OpMap
opMap = OpMap -> OpMap -> OpMap
addOpMapSet OpMap
flexOps' OpMap
nomOps
    , assocOps :: OpMap
assocOps = OpMap -> OpMap -> OpMap
diffOpMapSet (ExtModalSign -> OpMap
forall f e. Sign f e -> OpMap
assocOps ExtModalSign
sign) OpMap
flexibleOps
    , predMap :: PredMap
predMap = PredMap -> PredMap -> PredMap
addMapSet PredMap
rels (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ PredMap -> PredMap -> PredMap
addMapSet PredMap
flexPreds' PredMap
noNomsPreds
    }

data Args = Args
  { Args -> TERM ()
currentW :: TERM ()
  , Args -> Int
nextW, Args -> Int
freeC :: Int  -- world variables
  , Args -> [(Id, TERM ())]
boundNoms :: [(Id, TERM ())]
  , Args -> ExtModalSign
modSig :: ExtModalSign
  }

transTop :: ExtModalSign -> CASLSign -> FORMULA EM_FORMULA -> FORMULA ()
transTop :: ExtModalSign -> CASLSign -> ExtModalFORMULA -> CASLFORMULA
transTop msig :: ExtModalSign
msig csig :: CASLSign
csig = let
    vd :: VAR_DECL
vd = Token -> Id -> VAR_DECL
mkVarDecl (String -> Int -> Token
genNumVar "w" 1) Id
world
    vt :: TERM f
vt = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vd
    in CASLSign -> CASLFORMULA -> CASLFORMULA
forall f e. TermExtension f => Sign f e -> FORMULA f -> FORMULA f
stripQuant CASLSign
csig (CASLFORMULA -> CASLFORMULA)
-> (ExtModalFORMULA -> CASLFORMULA)
-> ExtModalFORMULA
-> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vd]
           (CASLFORMULA -> CASLFORMULA)
-> (ExtModalFORMULA -> CASLFORMULA)
-> ExtModalFORMULA
-> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Args -> ExtModalFORMULA -> CASLFORMULA
transMF (TERM () -> Int -> Int -> [(Id, TERM ())] -> ExtModalSign -> Args
Args TERM ()
forall f. TERM f
vt 1 1 [] ExtModalSign
msig)

getTermOfNom :: Args -> Id -> TERM ()
getTermOfNom :: Args -> Id -> TERM ()
getTermOfNom as :: Args
as i :: Id
i = TERM () -> Maybe (TERM ()) -> TERM ()
forall a. a -> Maybe a -> a
fromMaybe (Id -> TERM ()
mkNomAppl Id
i) (Maybe (TERM ()) -> TERM ())
-> ([(Id, TERM ())] -> Maybe (TERM ()))
-> [(Id, TERM ())]
-> TERM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> [(Id, TERM ())] -> Maybe (TERM ())
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Id
i ([(Id, TERM ())] -> TERM ()) -> [(Id, TERM ())] -> TERM ()
forall a b. (a -> b) -> a -> b
$ Args -> [(Id, TERM ())]
boundNoms Args
as

mkNomAppl :: Id -> TERM ()
mkNomAppl :: Id -> TERM ()
mkNomAppl pn :: Id
pn = OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (Id -> OP_TYPE -> OP_SYMB
mkQualOp (Id -> Id
nomName Id
pn) (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
nomOpType) []

transRecord :: Args -> Record EM_FORMULA (FORMULA ()) (TERM ())
transRecord :: Args -> Record EM_FORMULA CASLFORMULA (TERM ())
transRecord as :: Args
as = let
    extInf :: EModalSign
extInf = ExtModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo (ExtModalSign -> EModalSign) -> ExtModalSign -> EModalSign
forall a b. (a -> b) -> a -> b
$ Args -> ExtModalSign
modSig Args
as
    currW :: TERM ()
currW = Args -> TERM ()
currentW Args
as
    in ((EM_FORMULA -> ()) -> Record EM_FORMULA CASLFORMULA (TERM ())
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord ((EM_FORMULA -> ()) -> Record EM_FORMULA CASLFORMULA (TERM ()))
-> (EM_FORMULA -> ()) -> Record EM_FORMULA CASLFORMULA (TERM ())
forall a b. (a -> b) -> a -> b
$ () -> EM_FORMULA -> ()
forall a b. a -> b -> a
const ())
  { foldPredication :: ExtModalFORMULA -> PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
foldPredication = \ _ ps :: PRED_SYMB
ps args :: [TERM ()]
args r :: Range
r -> case PRED_SYMB
ps of
      Qual_pred_name pn :: Id
pn pTy :: PRED_TYPE
pTy@(Pred_type srts :: [Id]
srts q :: Range
q) p :: Range
p
        | Id -> PredType -> PredMap -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member Id
pn (PRED_TYPE -> PredType
toPredType PRED_TYPE
pTy) (PredMap -> Bool) -> PredMap -> Bool
forall a b. (a -> b) -> a -> b
$ EModalSign -> PredMap
flexPreds EModalSign
extInf
          -> PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
            (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name (Id -> Id
addPlace Id
pn) ([Id] -> Range -> PRED_TYPE
Pred_type (Id
world Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
srts) Range
q) Range
p)
            (TERM ()
currW TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: [TERM ()]
args) Range
r
        | [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
srts Bool -> Bool -> Bool
&& Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
pn (EModalSign -> Set Id
nominals EModalSign
extInf)
          -> TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM ()
currW (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Args -> Id -> TERM ()
getTermOfNom Args
as Id
pn
      _ -> PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
ps [TERM ()]
args Range
r
  , foldExtFORMULA :: ExtModalFORMULA -> EM_FORMULA -> CASLFORMULA
foldExtFORMULA = \ _ f :: EM_FORMULA
f -> Args -> EM_FORMULA -> CASLFORMULA
transEMF Args
as EM_FORMULA
f
  , foldApplication :: TERM EM_FORMULA -> OP_SYMB -> [TERM ()] -> Range -> TERM ()
foldApplication = \ _ os :: OP_SYMB
os args :: [TERM ()]
args r :: Range
r -> case OP_SYMB
os of
      Qual_op_name opn :: Id
opn oTy :: OP_TYPE
oTy@(Op_type ok :: OpKind
ok srts :: [Id]
srts res :: Id
res q :: Range
q) p :: Range
p
        | Id -> OpType -> OpMap -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member Id
opn (OP_TYPE -> OpType
toOpType OP_TYPE
oTy) (OpMap -> Bool) -> OpMap -> Bool
forall a b. (a -> b) -> a -> b
$ EModalSign -> OpMap
flexOps EModalSign
extInf
          -> OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
            (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (Id -> Id
addPlace Id
opn) (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
ok (Id
world Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
srts) Id
res Range
q) Range
p)
            (TERM ()
currW TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: [TERM ()]
args) Range
r
      _ -> OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
os [TERM ()]
args Range
r
  }

transMF :: Args -> FORMULA EM_FORMULA -> FORMULA ()
transMF :: Args -> ExtModalFORMULA -> CASLFORMULA
transMF = Record EM_FORMULA CASLFORMULA (TERM ())
-> ExtModalFORMULA -> CASLFORMULA
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record EM_FORMULA CASLFORMULA (TERM ())
 -> ExtModalFORMULA -> CASLFORMULA)
-> (Args -> Record EM_FORMULA CASLFORMULA (TERM ()))
-> Args
-> ExtModalFORMULA
-> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Args -> Record EM_FORMULA CASLFORMULA (TERM ())
transRecord

disjointVars :: [VAR_DECL] -> [FORMULA ()]
disjointVars :: [VAR_DECL] -> [CASLFORMULA]
disjointVars vs :: [VAR_DECL]
vs = case [VAR_DECL]
vs of
  a :: VAR_DECL
a : r :: [VAR_DECL]
r@(b :: VAR_DECL
b : _) -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg ((TERM () -> TERM () -> CASLFORMULA)
-> (VAR_DECL -> TERM ()) -> VAR_DECL -> VAR_DECL -> CASLFORMULA
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
a VAR_DECL
b) CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [VAR_DECL] -> [CASLFORMULA]
disjointVars [VAR_DECL]
r
  _ -> []

transEMF :: Args -> EM_FORMULA -> FORMULA ()
transEMF :: Args -> EM_FORMULA -> CASLFORMULA
transEMF as :: Args
as emf :: EM_FORMULA
emf = case EM_FORMULA
emf of
  PrefixForm pf :: FormPrefix
pf f :: ExtModalFORMULA
f r :: Range
r -> let
    fW :: Int
fW = Args -> Int
freeC Args
as
    in case FormPrefix
pf of
    BoxOrDiamond bOp :: BoxOp
bOp m :: MODALITY
m gEq :: Bool
gEq i :: Int
i -> let
      ex :: Bool
ex = BoxOp
bOp BoxOp -> BoxOp -> Bool
forall a. Eq a => a -> a -> Bool
== BoxOp
Diamond
      l :: [Int]
l = [Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 .. Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i]
      vds :: [VAR_DECL]
vds = (Int -> VAR_DECL) -> [Int] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: Int
n -> Token -> Id -> VAR_DECL
mkVarDecl (String -> Int -> Token
genNumVar "w" Int
n) Id
world) [Int]
l
      nAs :: Args
nAs = Args
as { freeC :: Int
freeC = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i }
      tf :: Int -> CASLFORMULA
tf n :: Int
n = Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
nAs { currentW :: TERM ()
currentW = Token -> Id -> TERM ()
forall f. Token -> Id -> TERM f
mkVarTerm (String -> Int -> Token
genNumVar "w" Int
n) Id
world } ExtModalFORMULA
f
      tM :: Int -> CASLFORMULA
tM n :: Int
n = Args -> MODALITY -> CASLFORMULA
transMod Args
nAs { nextW :: Int
nextW = Int
n } MODALITY
m
      conjF :: CASLFORMULA
conjF = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (Int -> CASLFORMULA) -> [Int] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map Int -> CASLFORMULA
tM [Int]
l [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ (Int -> CASLFORMULA) -> [Int] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map Int -> CASLFORMULA
tf [Int]
l [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [VAR_DECL] -> [CASLFORMULA]
disjointVars [VAR_DECL]
vds
      diam :: Int -> FormPrefix
diam = BoxOp -> MODALITY -> Bool -> Int -> FormPrefix
BoxOrDiamond BoxOp
Diamond MODALITY
m Bool
True
      tr :: BoxOp -> CASLFORMULA
tr b :: BoxOp
b = Args -> EM_FORMULA -> CASLFORMULA
transEMF Args
as (EM_FORMULA -> CASLFORMULA) -> EM_FORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ FormPrefix -> ExtModalFORMULA -> Range -> EM_FORMULA
PrefixForm (BoxOp -> MODALITY -> Bool -> Int -> FormPrefix
BoxOrDiamond BoxOp
b MODALITY
m Bool
gEq Int
i) ExtModalFORMULA
f Range
r
      in if Bool
gEq Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
&& (Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 Bool -> Bool -> Bool
|| Bool
ex) then case BoxOp
bOp of
           Diamond -> [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL]
vds CASLFORMULA
conjF
           Box -> [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vds CASLFORMULA
conjF
           EBox -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [[VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL]
vds CASLFORMULA
conjF, [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vds CASLFORMULA
conjF]
         else if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 Bool -> Bool -> Bool
&& Bool
ex Bool -> Bool -> Bool
&& Bool
gEq then CASLFORMULA
forall f. FORMULA f
trueForm
         else if BoxOp
bOp BoxOp -> BoxOp -> Bool
forall a. Eq a => a -> a -> Bool
== BoxOp
EBox then [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (BoxOp -> CASLFORMULA) -> [BoxOp] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map BoxOp -> CASLFORMULA
tr [BoxOp
Diamond, BoxOp
Box]
         else if Bool
ex -- lEq
              then Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
as (ExtModalFORMULA -> CASLFORMULA)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg (ExtModalFORMULA -> ExtModalFORMULA)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EM_FORMULA -> ExtModalFORMULA
forall f. f -> FORMULA f
ExtFORMULA (EM_FORMULA -> CASLFORMULA) -> EM_FORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ FormPrefix -> ExtModalFORMULA -> Range -> EM_FORMULA
PrefixForm
                       (Int -> FormPrefix
diam (Int -> FormPrefix) -> Int -> FormPrefix
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) ExtModalFORMULA
f Range
r
         else if Bool
gEq -- Box
              then Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
as (ExtModalFORMULA -> CASLFORMULA)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg (ExtModalFORMULA -> ExtModalFORMULA)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EM_FORMULA -> ExtModalFORMULA
forall f. f -> FORMULA f
ExtFORMULA (EM_FORMULA -> CASLFORMULA) -> EM_FORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ FormPrefix -> ExtModalFORMULA -> Range -> EM_FORMULA
PrefixForm
                       (Int -> FormPrefix
diam Int
i) (ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg ExtModalFORMULA
f) Range
r
              else Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
as (ExtModalFORMULA -> CASLFORMULA)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EM_FORMULA -> ExtModalFORMULA
forall f. f -> FORMULA f
ExtFORMULA (EM_FORMULA -> CASLFORMULA) -> EM_FORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ FormPrefix -> ExtModalFORMULA -> Range -> EM_FORMULA
PrefixForm
                       (Int -> FormPrefix
diam (Int -> FormPrefix) -> Int -> FormPrefix
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg ExtModalFORMULA
f) Range
r
    Hybrid at :: Bool
at i :: Token
i -> let ni :: Id
ni = Token -> Id
simpleIdToId Token
i in
      if Bool
at then Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
as { currentW :: TERM ()
currentW = Args -> Id -> TERM ()
getTermOfNom Args
as Id
ni } ExtModalFORMULA
f else let
      vi :: VAR_DECL
vi = Token -> Id -> VAR_DECL
mkVarDecl (String -> Int -> Token
genNumVar "i" (Int -> Token) -> Int -> Token
forall a b. (a -> b) -> a -> b
$ Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Id
world
      ti :: TERM f
ti = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vi
      in [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL
vi] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct
           [ TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM ()
forall f. TERM f
ti (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Args -> TERM ()
currentW Args
as
           , Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
as { boundNoms :: [(Id, TERM ())]
boundNoms = (Id
ni, TERM ()
forall f. TERM f
ti) (Id, TERM ()) -> [(Id, TERM ())] -> [(Id, TERM ())]
forall a. a -> [a] -> [a]
: Args -> [(Id, TERM ())]
boundNoms Args
as
                        , currentW :: TERM ()
currentW = TERM ()
forall f. TERM f
ti
                        , freeC :: Int
freeC = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 } ExtModalFORMULA
f ]
    _ -> Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
as ExtModalFORMULA
f
  UntilSince _isUntil :: Bool
_isUntil f1 :: ExtModalFORMULA
f1 f2 :: ExtModalFORMULA
f2 r :: Range
r -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. [FORMULA f] -> Range -> FORMULA f
conjunctRange [Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
as ExtModalFORMULA
f1, Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
as ExtModalFORMULA
f2] Range
r
  ModForm _ -> CASLFORMULA
forall f. FORMULA f
trueForm

transMod :: Args -> MODALITY -> FORMULA ()
transMod :: Args -> MODALITY -> CASLFORMULA
transMod as :: Args
as md :: MODALITY
md = let
  t1 :: TERM ()
t1 = Args -> TERM ()
currentW Args
as
  t2 :: TERM f
t2 = Token -> Id -> TERM f
forall f. Token -> Id -> TERM f
mkVarTerm (String -> Int -> Token
genNumVar "w" (Int -> Token) -> Int -> Token
forall a b. (a -> b) -> a -> b
$ Args -> Int
nextW Args
as) Id
world
  vts :: [TERM ()]
vts = [TERM ()
t1, TERM ()
forall f. TERM f
t2]
  msig :: ExtModalSign
msig = Args -> ExtModalSign
modSig Args
as
  extInf :: EModalSign
extInf = ExtModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo ExtModalSign
msig
  in case MODALITY
md of
  SimpleMod i :: Token
i -> let ri :: Id
ri = Token -> Id
simpleIdToId Token
i in PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication
    (Id -> PRED_TYPE -> PRED_SYMB
mkQualPred (Bool -> Bool -> Id -> Id
relOfMod Bool
False Bool
False Id
ri)
                    (PRED_TYPE -> PRED_SYMB)
-> (PredType -> PRED_TYPE) -> PredType -> PRED_SYMB
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> PRED_TYPE
toPRED_TYPE (PredType -> PRED_SYMB) -> PredType -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ Id -> Bool -> Id -> PredType
modPredType Id
world Bool
False Id
ri) [TERM ()]
vts
  TermMod t :: TERM EM_FORMULA
t -> case TERM EM_FORMULA -> Maybe Id
forall f. TermExtension f => f -> Maybe Id
optTermSort TERM EM_FORMULA
t of
    Just srt :: Id
srt -> case ExtModalSign -> (Id -> Id) -> [Id] -> [Id]
forall f e a. Sign f e -> (a -> Id) -> [a] -> [a]
keepMinimals ExtModalSign
msig Id -> Id
forall a. a -> a
id ([Id] -> [Id]) -> (Set Id -> [Id]) -> Set Id -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> [Id]
forall a. Set a -> [a]
Set.toList
      (Set Id -> [Id]) -> (Set Id -> Set Id) -> Set Id -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (EModalSign -> Set Id
termMods EModalSign
extInf) (Set Id -> Set Id) -> (Set Id -> Set Id) -> Set Id -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
srt
      (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ Id -> ExtModalSign -> Set Id
forall f e. Id -> Sign f e -> Set Id
supersortsOf Id
srt ExtModalSign
msig of
      [] -> String -> CASLFORMULA
forall a. HasCallStack => String -> a
error (String -> CASLFORMULA) -> String -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "transMod1: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TERM EM_FORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TERM EM_FORMULA
t ""
      st :: Id
st : _ -> PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication
        (Id -> PRED_TYPE -> PRED_SYMB
mkQualPred (Bool -> Bool -> Id -> Id
relOfMod Bool
False Bool
True Id
st)
         (PRED_TYPE -> PRED_SYMB)
-> (PredType -> PRED_TYPE) -> PredType -> PRED_SYMB
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> PRED_TYPE
toPRED_TYPE (PredType -> PRED_SYMB) -> PredType -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ Id -> Bool -> Id -> PredType
modPredType Id
world Bool
True Id
st)
        ([TERM ()] -> CASLFORMULA) -> [TERM ()] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Record EM_FORMULA CASLFORMULA (TERM ())
-> TERM EM_FORMULA -> TERM ()
forall f a b. Record f a b -> TERM f -> b
foldTerm (Args -> Record EM_FORMULA CASLFORMULA (TERM ())
transRecord Args
as) TERM EM_FORMULA
t TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: [TERM ()]
vts
    _ -> String -> CASLFORMULA
forall a. HasCallStack => String -> a
error (String -> CASLFORMULA) -> String -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "transMod2: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TERM EM_FORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TERM EM_FORMULA
t ""
  Guard f :: ExtModalFORMULA
f -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkExEq TERM ()
t1 TERM ()
forall f. TERM f
t2, Args -> ExtModalFORMULA -> CASLFORMULA
transMF Args
as ExtModalFORMULA
f]
  ModOp mOp :: ModOp
mOp m1 :: MODALITY
m1 m2 :: MODALITY
m2 -> case ModOp
mOp of
    Composition -> let
      nW :: Int
nW = Args -> Int
freeC Args
as Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
      nAs :: Args
nAs = Args
as { freeC :: Int
freeC = Int
nW }
      vd :: VAR_DECL
vd = Token -> Id -> VAR_DECL
mkVarDecl (String -> Int -> Token
genNumVar "w" Int
nW) Id
world
      in [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL
vd] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct
           [ Args -> MODALITY -> CASLFORMULA
transMod Args
nAs { nextW :: Int
nextW = Int
nW } MODALITY
m1
           , Args -> MODALITY -> CASLFORMULA
transMod Args
nAs { currentW :: TERM ()
currentW = VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vd } MODALITY
m2 ]
    Intersection -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [Args -> MODALITY -> CASLFORMULA
transMod Args
as MODALITY
m1, Args -> MODALITY -> CASLFORMULA
transMod Args
as MODALITY
m2] -- parallel?
    Union -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct [Args -> MODALITY -> CASLFORMULA
transMod Args
as MODALITY
m1, Args -> MODALITY -> CASLFORMULA
transMod Args
as MODALITY
m2]
    OrElse -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct ([CASLFORMULA] -> CASLFORMULA)
-> ([MODALITY] -> [CASLFORMULA]) -> [MODALITY] -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExtModalFORMULA] -> Args -> [MODALITY] -> [CASLFORMULA]
transOrElse [] Args
as ([MODALITY] -> CASLFORMULA) -> [MODALITY] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ MODALITY -> [MODALITY]
flatOrElse MODALITY
md
  TransClos m :: MODALITY
m -> Args -> MODALITY -> CASLFORMULA
transMod Args
as MODALITY
m -- ignore transitivity for now

flatOrElse :: MODALITY -> [MODALITY]
flatOrElse :: MODALITY -> [MODALITY]
flatOrElse md :: MODALITY
md = case MODALITY
md of
  ModOp OrElse m1 :: MODALITY
m1 m2 :: MODALITY
m2 -> MODALITY -> [MODALITY]
flatOrElse MODALITY
m1 [MODALITY] -> [MODALITY] -> [MODALITY]
forall a. [a] -> [a] -> [a]
++ MODALITY -> [MODALITY]
flatOrElse MODALITY
m2
  _ -> [MODALITY
md]

transOrElse :: [FORMULA EM_FORMULA] -> Args -> [MODALITY] -> [FORMULA ()]
transOrElse :: [ExtModalFORMULA] -> Args -> [MODALITY] -> [CASLFORMULA]
transOrElse nFs :: [ExtModalFORMULA]
nFs as :: Args
as ms :: [MODALITY]
ms = case [MODALITY]
ms of
  [] -> []
  md :: MODALITY
md : r :: [MODALITY]
r -> case MODALITY
md of
    Guard f :: ExtModalFORMULA
f -> Args -> MODALITY -> CASLFORMULA
transMod Args
as (ExtModalFORMULA -> MODALITY
Guard (ExtModalFORMULA -> MODALITY)
-> ([ExtModalFORMULA] -> ExtModalFORMULA)
-> [ExtModalFORMULA]
-> MODALITY
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExtModalFORMULA] -> ExtModalFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([ExtModalFORMULA] -> MODALITY) -> [ExtModalFORMULA] -> MODALITY
forall a b. (a -> b) -> a -> b
$ ExtModalFORMULA
f ExtModalFORMULA -> [ExtModalFORMULA] -> [ExtModalFORMULA]
forall a. a -> [a] -> [a]
: [ExtModalFORMULA]
nFs)
      CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [ExtModalFORMULA] -> Args -> [MODALITY] -> [CASLFORMULA]
transOrElse (ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg ExtModalFORMULA
f ExtModalFORMULA -> [ExtModalFORMULA] -> [ExtModalFORMULA]
forall a. a -> [a] -> [a]
: [ExtModalFORMULA]
nFs) Args
as [MODALITY]
r
    _ -> Args -> MODALITY -> CASLFORMULA
transMod Args
as MODALITY
md CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [ExtModalFORMULA] -> Args -> [MODALITY] -> [CASLFORMULA]
transOrElse [ExtModalFORMULA]
nFs Args
as [MODALITY]
r