44N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

44N/A{- |

44N/AModule : $Header$

44N/ACopyright : (c) Christian Maeder, DFKI 2012

44N/ALicense : GPLv2 or higher, see LICENSE.txt

44N/A

44N/AMaintainer : Christian.Maeder@dfki.de

44N/AStability : provisional

44N/APortability : non-portable (MPTC-FD)

44N/A-}

44N/A

44N/Amodule Comorphisms.ExtModal2CASL where

44N/A

44N/Aimport Logic.Logic

44N/Aimport Logic.Comorphism

44N/A

44N/Aimport Common.AS_Annotation

44N/Aimport Common.DocUtils

44N/Aimport Common.Id

44N/Aimport Common.ProofTree

75N/Aimport qualified Common.Lib.Rel as Rel

75N/Aimport qualified Common.Lib.MapSet as MapSet

5636N/A

44N/Aimport qualified Data.Set as Set

6895N/Aimport Data.Function

6895N/Aimport Data.Maybe

44N/A

44N/A-- CASL

44N/Aimport CASL.AS_Basic_CASL

491N/Aimport CASL.Fold

844N/Aimport CASL.Logic_CASL

844N/Aimport CASL.Morphism

44N/Aimport CASL.Overload

2899N/Aimport CASL.Quantification

2899N/Aimport CASL.Sign

5680N/Aimport CASL.Sublogic as SL

44N/Aimport CASL.World

515N/A

515N/A-- ExtModalCASL

515N/Aimport ExtModal.Logic_ExtModal

6895N/Aimport ExtModal.AS_ExtModal

6895N/Aimport ExtModal.ExtModalSign

6895N/Aimport ExtModal.Sublogic

6895N/A

44N/Adata ExtModal2CASL = ExtModal2CASL deriving (Show)

44N/Ainstance Language ExtModal2CASL

5680N/A

58N/Ainstance Comorphism ExtModal2CASL

44N/A ExtModal Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS

44N/A SYMB_MAP_ITEMS ExtModalSign ExtModalMorph

44N/A Symbol RawSymbol ()

44N/A CASL CASL_Sublogics

59N/A CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

6895N/A CASLSign

6895N/A CASLMor

6895N/A Symbol RawSymbol ProofTree where

6895N/A sourceLogic ExtModal2CASL = ExtModal

6895N/A sourceSublogic ExtModal2CASL = maxSublogic

6895N/A targetLogic ExtModal2CASL = CASL

44N/A mapSublogic ExtModal2CASL _ = Just SL.caslTop

5795N/A map_theory ExtModal2CASL (sig, sens) = case transSig sig of

5795N/A (mme, s) -> return (mme, s ++ map (mapNamed $ transTop sig mme) sens)

5795N/A {-

5795N/A map_morphism ExtModal2CASL = return . mapMor

5795N/A map_sentence ExtModal2CASL sig = return . transSen sig

3817N/A map_symbol ExtModal2CASL _ = Set.singleton . mapSym

3817N/A -}

5795N/A has_model_expansion ExtModal2CASL = True

3817N/A is_weakly_amalgamable ExtModal2CASL = True

3817N/A

nomName :: Id -> Id

nomName t = Id [genToken "N"] [t] $ rangeOfId t

nomOpType :: OpType

nomOpType = mkTotOpType [] world

-- | add world arguments to flexible ops and preds; and add relations

transSig :: ExtModalSign -> (CASLSign, [Named (FORMULA ())])

transSig sign = let

s1 = embedSign () sign

extInf = extendedInfo sign

flexibleOps = flexOps extInf

flexiblePreds = flexPreds extInf

flexOps' = addWorldOp world addPlace flexibleOps

flexPreds' = addWorldPred world addPlace flexiblePreds

rigOps' = diffOpMapSet (opMap sign) flexibleOps

rigPreds' = diffMapSet (predMap sign) flexiblePreds

noms = nominals extInf

noNomsPreds = Set.fold (`MapSet.delete` nomPType) rigPreds' noms

termMs = termMods extInf

timeMs = timeMods extInf

rels = Set.fold (\ m ->

insertModPred world (Set.member m timeMs) (Set.member m termMs) m)

MapSet.empty $ modalities extInf

nomOps = Set.fold (\ n -> addOpTo (nomName n) nomOpType) rigOps' noms

vds = map (\ n -> mkVarDecl (genNumVar "v" n) world) [1, 2]

ts = map toQualVar vds

in (s1

{ sortRel = Rel.insertKey world $ sortRel sign

, opMap = addOpMapSet flexOps' nomOps

, assocOps = diffOpMapSet (assocOps sign) flexibleOps

, predMap = (if Set.null timeMs then id else MapSet.insert tauId tauTy)

. addMapSet rels

$ addMapSet flexPreds' noNomsPreds

} , if Set.null timeMs then [] else

[makeNamed "tau" . mkForall vds . mkEqv

(mkPredication (mkQualPred tauId $ toPRED_TYPE tauTy) ts)

. disjunct . map (\ tm ->

let v = mkVarDecl (genNumVar "t" 0) tm

term = Set.member tm termMs

in (if term then mkExist [v] else id) $ mkPredication

(mkQualPred (relOfMod True term tm)

. toPRED_TYPE $ modPredType world term tm)

$ if term then toQualVar v : ts else ts) $ Set.toList timeMs])

data Args = Args

{ currentW :: TERM ()

, nextW, freeC :: Int -- world variables

, boundNoms :: [(Id, TERM ())]

, modSig :: ExtModalSign

}

transTop :: ExtModalSign -> CASLSign -> FORMULA EM_FORMULA -> FORMULA ()

transTop msig csig = let

vd = mkVarDecl (genNumVar "w" 1) world

vt = toQualVar vd

in stripQuant csig . mkForall [vd]

. transMF (Args vt 1 1 [] msig)

getTermOfNom :: Args -> Id -> TERM ()

getTermOfNom as i = fromMaybe (mkNomAppl i) . lookup i $ boundNoms as

tauId :: Id

tauId = genName "Tau"

tauTy :: PredType

tauTy = PredType [world, world]

-- TODO: check that constructors are not flexible!

mkNomAppl :: Id -> TERM ()

mkNomAppl pn = mkAppl (mkQualOp (nomName pn) $ toOP_TYPE nomOpType) []

transRecord :: Args -> Record EM_FORMULA (FORMULA ()) (TERM ())

transRecord as = let

extInf = extendedInfo $ modSig as

currW = currentW as

in (mapRecord $ const ())

{ foldPredication = \ _ ps args r -> case ps of

Qual_pred_name pn pTy@(Pred_type srts q) p

| MapSet.member pn (toPredType pTy) $ flexPreds extInf

-> Predication

(Qual_pred_name (addPlace pn) (Pred_type (world : srts) q) p)

(currW : args) r

| null srts && Set.member pn (nominals extInf)

-> mkStEq currW $ getTermOfNom as pn

_ -> Predication ps args r

, foldExtFORMULA = \ _ f -> transEMF as f

, foldApplication = \ _ os args r -> case os of

Qual_op_name opn oTy@(Op_type ok srts res q) p

| MapSet.member opn (toOpType oTy) $ flexOps extInf

-> Application

(Qual_op_name (addPlace opn) (Op_type ok (world : srts) res q) p)

(currW : args) r

_ -> Application os args r

}

transMF :: Args -> FORMULA EM_FORMULA -> FORMULA ()

transMF = foldFormula . transRecord

disjointVars :: [VAR_DECL] -> [FORMULA ()]

disjointVars vs = case vs of

a : r@(b : _) -> mkNeg (on mkStEq toQualVar a b) : disjointVars r

_ -> []

transEMF :: Args -> EM_FORMULA -> FORMULA ()

transEMF as emf = case emf of

PrefixForm pf f r -> let

fW = freeC as

in case pf of

BoxOrDiamond bOp m gEq i -> let

ex = bOp == Diamond

l = [fW + 1 .. fW + i]

vds = map (\ n -> mkVarDecl (genNumVar "w" n) world) l

nAs = as { freeC = fW + i }

tf n = transMF nAs { currentW = mkVarTerm (genNumVar "w" n) world } f

tM n = transMod nAs { nextW = n } m

conjF = conjunct $ map tM l ++ map tf l ++ disjointVars vds

diam = BoxOrDiamond Diamond m True

tr b = transEMF as $ PrefixForm (BoxOrDiamond b m gEq i) f r

in if gEq && i > 0 && (i == 1 || ex) then case bOp of

Diamond -> mkExist vds conjF

Box -> mkForall vds conjF

EBox -> conjunct [mkExist vds conjF, mkForall vds conjF]

else if i <= 0 && ex && gEq then trueForm

else if bOp == EBox then conjunct $ map tr [Diamond, Box]

else if ex -- lEq

then transMF as . mkNeg . ExtFORMULA $ PrefixForm

(diam $ i + 1) f r

else if gEq -- Box

then transMF as . mkNeg . ExtFORMULA $ PrefixForm

(diam i) (mkNeg f) r

else transMF as . ExtFORMULA $ PrefixForm

(diam $ i + 1) (mkNeg f) r

Hybrid at i -> let ni = simpleIdToId i in

if at then transMF as { currentW = getTermOfNom as ni } f else let

vi = mkVarDecl (genNumVar "i" fW) world

ti = toQualVar vi

in mkExist [vi] $ conjunct

[ mkStEq ti $ currentW as

, transMF as { boundNoms = (ni, ti) : boundNoms as } f ]

_ -> transMF as f

UntilSince _isUntil f1 f2 r -> conjunctRange [transMF as f1, transMF as f2] r

ModForm _ -> trueForm

transMod :: Args -> MODALITY -> FORMULA ()

transMod as md = let

t1 = currentW as

t2 = mkVarTerm (genNumVar "w" $ nextW as) world

vts = [t1, t2]

msig = modSig as

extInf = extendedInfo msig

timeMs = timeMods extInf

in case md of

SimpleMod i -> let ri = simpleIdToId i in mkPredication

(mkQualPred (relOfMod (Set.member ri timeMs) False ri)

. toPRED_TYPE $ modPredType world False ri) vts

TermMod t -> case optTermSort t of

Just srt -> case keepMinimals msig id . Set.toList

. Set.intersection (termMods extInf) . Set.insert srt

$ supersortsOf srt msig of

[] -> error $ "transMod1: " ++ showDoc t ""

st : _ -> mkPredication

(mkQualPred (relOfMod (Set.member st timeMs) True st)

. toPRED_TYPE $ modPredType world True st)

$ foldTerm (transRecord as) t : vts

_ -> error $ "transMod2: " ++ showDoc t ""

Guard f -> conjunct [mkExEq t1 t2, transMF as f]

ModOp mOp m1 m2 -> case mOp of

Composition -> let

nW = freeC as + 1

nAs = as { freeC = nW }

vd = mkVarDecl (genNumVar "w" nW) world

in mkExist [vd] $ conjunct

[ transMod nAs { nextW = nW } m1

, transMod nAs { currentW = toQualVar vd } m2 ]

Intersection -> conjunct [transMod as m1, transMod as m2] -- parallel?

Union -> disjunct [transMod as m1, transMod as m2]

OrElse -> disjunct . transOrElse [] as $ flatOrElse md

TransClos m -> transMod as m -- ignore transitivity for now

flatOrElse :: MODALITY -> [MODALITY]

flatOrElse md = case md of

ModOp OrElse m1 m2 -> flatOrElse m1 ++ flatOrElse m2

_ -> [md]

transOrElse :: [FORMULA EM_FORMULA] -> Args -> [MODALITY] -> [FORMULA ()]

transOrElse nFs as ms = case ms of

[] -> []

md : r -> case md of

Guard f -> transMod as (Guard . conjunct $ f : nFs)

: transOrElse (mkNeg f : nFs) as r

_ -> transMod as md : transOrElse nFs as r