ExtModal2CASL.hs revision 1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Christian Maeder, DFKI 2012
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Christian.Maeder@dfki.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : non-portable (MPTC-FD)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedermodule Comorphisms.ExtModal2CASL (ExtModal2CASL (..)) where
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Common.Lib.Rel as Rel
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Common.Lib.MapSet as MapSet
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Data.Set as Set
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- ExtModalCASL
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata ExtModal2CASL = ExtModal2CASL deriving (Show)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederinstance Language ExtModal2CASL
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederinstance Comorphism ExtModal2CASL
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Symbol RawSymbol ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder CASL CASL_Sublogics
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Symbol RawSymbol ProofTree where
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder sourceLogic ExtModal2CASL = ExtModal
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder sourceSublogic ExtModal2CASL = mkTop foleml
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder targetLogic ExtModal2CASL = CASL
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder mapSublogic ExtModal2CASL s = Just s { ext_features = () }
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder map_theory ExtModal2CASL (sig, sens) = case transSig sig of
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder mme -> return (mme, map (mapNamed $ transTop sig mme) sens)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder map_morphism ExtModal2CASL = return . mapMor
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder map_sentence ExtModal2CASL sig = return . transSen sig
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder map_symbol ExtModal2CASL _ = Set.singleton . mapSym
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder has_model_expansion ExtModal2CASL = True
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder is_weakly_amalgamable ExtModal2CASL = True
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaedernomName :: Id -> Id
ad270004874ce1d0697fb30d7309f180553bb315Christian MaedernomName t = Id [genToken "N"] [t] $ rangeOfId t
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedernomOpType :: OpType
5e46b572ed576c0494768998b043d9d340594122Till MossakowskinomOpType = mkTotOpType [] world
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder-- | add world arguments to flexible ops and preds; and add relations
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaedertransSig :: ExtModalSign -> CASLSign
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaedertransSig sign = let
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder s1 = embedSign () sign
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang extInf = extendedInfo sign
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder flexibleOps = flexOps extInf
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder flexiblePreds = flexPreds extInf
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder flexOps' = addWorldOp world addPlace flexibleOps
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder flexPreds' = addWorldPred world addPlace flexiblePreds
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski rigOps' = diffOpMapSet (opMap sign) flexibleOps
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder rigPreds' = diffMapSet (predMap sign) flexiblePreds
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder noms = nominals extInf
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder noNomsPreds = Set.fold (`MapSet.delete` nomPType) rigPreds' noms
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder termMs = termMods extInf
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder rels = Set.fold (\ m ->
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich insertModPred world False (Set.member m termMs) m)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder MapSet.empty $ modalities extInf
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich nomOps = Set.fold (\ n -> addOpTo (nomName n) nomOpType) rigOps' noms
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { sortRel = Rel.insertKey world $ sortRel sign
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , opMap = addOpMapSet flexOps' nomOps
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu , assocOps = diffOpMapSet (assocOps sign) flexibleOps
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , predMap = addMapSet rels $ addMapSet flexPreds' noNomsPreds
8e80792f474d154ff11762fac081a422e34f1accChristian Maederdata Args = Args
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { currentW :: TERM ()
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , nextW, freeC :: Int -- world variables
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , boundNoms :: [(Id, TERM ())]
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , modSig :: ExtModalSign
16e124196c6b204769042028c74f533509c9b5d3Christian MaedertransTop :: ExtModalSign -> CASLSign -> FORMULA EM_FORMULA -> FORMULA ()
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaedertransTop msig csig = let
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder vd = mkVarDecl (genNumVar "w" 1) world
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder vt = toQualVar vd
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder in stripQuant csig . mkForall [vd]
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder . transMF (Args vt 1 1 [] msig)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaedergetTermOfNom :: Args -> Id -> TERM ()
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaedergetTermOfNom as i = fromMaybe (mkNomAppl i) . lookup i $ boundNoms as
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaedermkNomAppl :: Id -> TERM ()
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaedermkNomAppl pn = mkAppl (mkQualOp (nomName pn) $ toOP_TYPE nomOpType) []
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedertransRecord :: Args -> Record EM_FORMULA (FORMULA ()) (TERM ())
e6dccba746efe07338d3107fed512e713fd50b28Christian MaedertransRecord as = let
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder extInf = extendedInfo $ modSig as
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder currW = currentW as
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder in (mapRecord $ const ())
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder { foldPredication = \ _ ps args r -> case ps of
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Qual_pred_name pn pTy@(Pred_type srts q) p
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder | MapSet.member pn (toPredType pTy) $ flexPreds extInf
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -> Predication
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (Qual_pred_name (addPlace pn) (Pred_type (world : srts) q) p)
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder (currW : args) r
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder | null srts && Set.member pn (nominals extInf)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder -> mkStEq currW $ getTermOfNom as pn
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder _ -> Predication ps args r
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder , foldExtFORMULA = \ _ f -> transEMF as f
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder , foldApplication = \ _ os args r -> case os of
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder Qual_op_name opn oTy@(Op_type ok srts res q) p
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder | MapSet.member opn (toOpType oTy) $ flexOps extInf
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder -> Application
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (Qual_op_name (addPlace opn) (Op_type ok (world : srts) res q) p)
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder (currW : args) r
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder _ -> Application os args r
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaedertransMF :: Args -> FORMULA EM_FORMULA -> FORMULA ()
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaedertransMF = foldFormula . transRecord
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederdisjointVars :: [VAR_DECL] -> [FORMULA ()]
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederdisjointVars vs = case vs of
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder a : r@(b : _) -> mkNeg (on mkStEq toQualVar a b) : disjointVars r
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedertransEMF :: Args -> EM_FORMULA -> FORMULA ()
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedertransEMF as emf = case emf of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder PrefixForm pf f r -> let
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder fW = freeC as
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder in case pf of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder BoxOrDiamond bOp m gEq i -> let
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ex = bOp == Diamond
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder l = [fW + 1 .. fW + i]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder vds = map (\ n -> mkVarDecl (genNumVar "w" n) world) l
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder nAs = as { freeC = fW + i }
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder tf n = transMF nAs { currentW = mkVarTerm (genNumVar "w" n) world } f
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder tM n = transMod nAs { nextW = n } m
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder conjF = conjunct $ map tM l ++ map tf l ++ disjointVars vds
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder diam = BoxOrDiamond Diamond m True
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder tr b = transEMF as $ PrefixForm (BoxOrDiamond b m gEq i) f r
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder in if gEq && i > 0 && (i == 1 || ex) then case bOp of
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder Diamond -> mkExist vds conjF
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Box -> mkForall vds conjF
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder EBox -> conjunct [mkExist vds conjF, mkForall vds conjF]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else if i <= 0 && ex && gEq then trueForm
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder else if bOp == EBox then conjunct $ map tr [Diamond, Box]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else if ex -- lEq
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski then transMF as . mkNeg . ExtFORMULA $ PrefixForm
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (diam $ i + 1) f r
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder else if gEq -- Box
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder then transMF as . mkNeg . ExtFORMULA $ PrefixForm
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (diam i) (mkNeg f) r
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder else transMF as . ExtFORMULA $ PrefixForm
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (diam $ i + 1) (mkNeg f) r
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Hybrid at i -> let ni = simpleIdToId i in
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder if at then transMF as { currentW = getTermOfNom as ni } f else let
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder vi = mkVarDecl (genNumVar "i" $ fW + 1) world
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ti = toQualVar vi
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder in mkExist [vi] $ conjunct
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder [ mkStEq ti $ currentW as
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , transMF as { boundNoms = (ni, ti) : boundNoms as
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , currentW = ti
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , freeC = fW + 1 } f ]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> transMF as f
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder UntilSince _isUntil f1 f2 r -> conjunctRange [transMF as f1, transMF as f2] r
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ModForm _ -> trueForm
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedertransMod :: Args -> MODALITY -> FORMULA ()
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedertransMod as md = let
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder t1 = currentW as
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder t2 = mkVarTerm (genNumVar "w" $ nextW as) world
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder vts = [t1, t2]
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder msig = modSig as
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder extInf = extendedInfo msig
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in case md of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder SimpleMod i -> let ri = simpleIdToId i in mkPredication
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (mkQualPred (relOfMod False False ri)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder . toPRED_TYPE $ modPredType world False ri) vts
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder TermMod t -> case optTermSort t of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just srt -> case keepMinimals msig id . Set.toList
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder . Set.intersection (termMods extInf) . Set.insert srt
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ supersortsOf srt msig of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder [] -> error $ "transMod1: " ++ showDoc t ""
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder st : _ -> mkPredication
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (mkQualPred (relOfMod False True st)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder . toPRED_TYPE $ modPredType world True st)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder $ foldTerm (transRecord as) t : vts
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder _ -> error $ "transMod2: " ++ showDoc t ""
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Guard f -> conjunct [mkExEq t1 t2, transMF as f]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder ModOp mOp m1 m2 -> case mOp of
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Composition -> let
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder nW = freeC as + 1
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder nAs = as { freeC = nW }
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz vd = mkVarDecl (genNumVar "w" nW) world
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder in mkExist [vd] $ conjunct
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder [ transMod nAs { nextW = nW } m1
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz , transMod nAs { currentW = toQualVar vd } m2 ]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Intersection -> conjunct [transMod as m1, transMod as m2] -- parallel?
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Union -> disjunct [transMod as m1, transMod as m2]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder OrElse -> disjunct . transOrElse [] as $ flatOrElse md
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder TransClos m -> transMod as m -- ignore transitivity for now
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederflatOrElse :: MODALITY -> [MODALITY]
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian MaederflatOrElse md = case md of
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian Maeder ModOp OrElse m1 m2 -> flatOrElse m1 ++ flatOrElse m2
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulztransOrElse :: [FORMULA EM_FORMULA] -> Args -> [MODALITY] -> [FORMULA ()]
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulztransOrElse nFs as ms = case ms of
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz md : r -> case md of
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz Guard f -> transMod as (Guard . conjunct $ f : nFs)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder : transOrElse (mkNeg f : nFs) as r
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ -> transMod as md : transOrElse nFs as r