1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederCopyright : (c) Christian Maeder, DFKI 2012
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela TurcuLicense : GPLv2 or higher, see LICENSE.txt
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederMaintainer : Christian.Maeder@dfki.de
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederStability : provisional
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederPortability : non-portable (MPTC-FD)
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maedermodule Comorphisms.ExtModal2CASL (ExtModal2CASL (..)) where
3f5d611a1388ce3cd33f86da3f1e9b7ad68d087cMihaela Turcuimport qualified Common.Lib.Rel as Rel
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maederimport qualified Common.Lib.MapSet as MapSet
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maederimport qualified Data.Set as Set
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu-- ExtModalCASL
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcudata ExtModal2CASL = ExtModal2CASL deriving (Show)
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcuinstance Language ExtModal2CASL
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcuinstance Comorphism ExtModal2CASL
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu Symbol RawSymbol ()
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu CASL CASL_Sublogics
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu Symbol RawSymbol ProofTree where
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu sourceLogic ExtModal2CASL = ExtModal
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder sourceSublogic ExtModal2CASL = mkTop foleml
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu targetLogic ExtModal2CASL = CASL
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder mapSublogic ExtModal2CASL s = Just s { ext_features = () }
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder map_theory ExtModal2CASL (sig, sens) = case transSig sig of
a62775006ae39677af366c0f7b599924243cc65bChristian Maeder mme -> return (mme, map (mapNamed $ transTop sig mme) sens)
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu map_morphism ExtModal2CASL = return . mapMor
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu map_sentence ExtModal2CASL sig = return . transSen sig
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu map_symbol ExtModal2CASL _ = Set.singleton . mapSym
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu has_model_expansion ExtModal2CASL = True
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu is_weakly_amalgamable ExtModal2CASL = True
d20b265a2765e843986ceed6bf0055582981bf0fChristian MaedernomName :: Id -> Id
d20b265a2765e843986ceed6bf0055582981bf0fChristian MaedernomName t = Id [genToken "N"] [t] $ rangeOfId t
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian MaedernomOpType :: OpType
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian MaedernomOpType = mkTotOpType [] world
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder-- | add world arguments to flexible ops and preds; and add relations
a62775006ae39677af366c0f7b599924243cc65bChristian MaedertransSig :: ExtModalSign -> CASLSign
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaedertransSig sign = let
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder s1 = embedSign () sign
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder extInf = extendedInfo sign
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder flexibleOps = flexOps extInf
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder flexiblePreds = flexPreds extInf
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder flexOps' = addWorldOp world addPlace flexibleOps
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder flexPreds' = addWorldPred world addPlace flexiblePreds
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder rigOps' = diffOpMapSet (opMap sign) flexibleOps
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder rigPreds' = diffMapSet (predMap sign) flexiblePreds
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian Maeder noms = nominals extInf
d20b265a2765e843986ceed6bf0055582981bf0fChristian Maeder noNomsPreds = Set.fold (`MapSet.delete` nomPType) rigPreds' noms
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder termMs = termMods extInf
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder rels = Set.fold (\ m ->
84c0c21396b0ebd663607b9eb745753a628f7de1Christian Maeder insertModPred world False (Set.member m termMs) m)
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder MapSet.empty $ modalities extInf
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian Maeder nomOps = Set.fold (\ n -> addOpTo (nomName n) nomOpType) rigOps' noms
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder { sortRel = Rel.insertKey world $ sortRel sign
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian Maeder , opMap = addOpMapSet flexOps' nomOps
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder , assocOps = diffOpMapSet (assocOps sign) flexibleOps
a62775006ae39677af366c0f7b599924243cc65bChristian Maeder , predMap = addMapSet rels $ addMapSet flexPreds' noNomsPreds
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maederdata Args = Args
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder { currentW :: TERM ()
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder , nextW, freeC :: Int -- world variables
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder , boundNoms :: [(Id, TERM ())]
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder , modSig :: ExtModalSign
d12f7a58b996457c25e12d674153346a4e21930eChristian MaedertransTop :: ExtModalSign -> CASLSign -> FORMULA EM_FORMULA -> FORMULA ()
d12f7a58b996457c25e12d674153346a4e21930eChristian MaedertransTop msig csig = let
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder vd = mkVarDecl (genNumVar "w" 1) world
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder vt = toQualVar vd
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder in stripQuant csig . mkForall [vd]
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder . transMF (Args vt 1 1 [] msig)
d12f7a58b996457c25e12d674153346a4e21930eChristian MaedergetTermOfNom :: Args -> Id -> TERM ()
d12f7a58b996457c25e12d674153346a4e21930eChristian MaedergetTermOfNom as i = fromMaybe (mkNomAppl i) . lookup i $ boundNoms as
398f02e814574f163278b28b5c78cd213493f7ccChristian MaedermkNomAppl :: Id -> TERM ()
398f02e814574f163278b28b5c78cd213493f7ccChristian MaedermkNomAppl pn = mkAppl (mkQualOp (nomName pn) $ toOP_TYPE nomOpType) []
16779ccfe622e9db869898f724bc0132b90cb7d7Christian MaedertransRecord :: Args -> Record EM_FORMULA (FORMULA ()) (TERM ())
16779ccfe622e9db869898f724bc0132b90cb7d7Christian MaedertransRecord as = let
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder extInf = extendedInfo $ modSig as
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder currW = currentW as
16779ccfe622e9db869898f724bc0132b90cb7d7Christian Maeder in (mapRecord $ const ())
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder { foldPredication = \ _ ps args r -> case ps of
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder Qual_pred_name pn pTy@(Pred_type srts q) p
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder | MapSet.member pn (toPredType pTy) $ flexPreds extInf
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder -> Predication
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder (Qual_pred_name (addPlace pn) (Pred_type (world : srts) q) p)
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder (currW : args) r
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder | null srts && Set.member pn (nominals extInf)
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder -> mkStEq currW $ getTermOfNom as pn
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder _ -> Predication ps args r
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder , foldExtFORMULA = \ _ f -> transEMF as f
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder , foldApplication = \ _ os args r -> case os of
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder Qual_op_name opn oTy@(Op_type ok srts res q) p
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder | MapSet.member opn (toOpType oTy) $ flexOps extInf
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder -> Application
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder (Qual_op_name (addPlace opn) (Op_type ok (world : srts) res q) p)
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder (currW : args) r
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder _ -> Application os args r
16779ccfe622e9db869898f724bc0132b90cb7d7Christian MaedertransMF :: Args -> FORMULA EM_FORMULA -> FORMULA ()
16779ccfe622e9db869898f724bc0132b90cb7d7Christian MaedertransMF = foldFormula . transRecord
3397210aac34a94e9ae85faacf7f6a02a808097eChristian MaederdisjointVars :: [VAR_DECL] -> [FORMULA ()]
3397210aac34a94e9ae85faacf7f6a02a808097eChristian MaederdisjointVars vs = case vs of
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder a : r@(b : _) -> mkNeg (on mkStEq toQualVar a b) : disjointVars r
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian MaedertransEMF :: Args -> EM_FORMULA -> FORMULA ()
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian MaedertransEMF as emf = case emf of
398f02e814574f163278b28b5c78cd213493f7ccChristian Maeder PrefixForm pf f r -> let
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder fW = freeC as
398f02e814574f163278b28b5c78cd213493f7ccChristian Maeder in case pf of
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder BoxOrDiamond bOp m gEq i -> let
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder ex = bOp == Diamond
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder l = [fW + 1 .. fW + i]
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder vds = map (\ n -> mkVarDecl (genNumVar "w" n) world) l
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder nAs = as { freeC = fW + i }
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder tf n = transMF nAs { currentW = mkVarTerm (genNumVar "w" n) world } f
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder tM n = transMod nAs { nextW = n } m
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder conjF = conjunct $ map tM l ++ map tf l ++ disjointVars vds
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder diam = BoxOrDiamond Diamond m True
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder tr b = transEMF as $ PrefixForm (BoxOrDiamond b m gEq i) f r
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder in if gEq && i > 0 && (i == 1 || ex) then case bOp of
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder Diamond -> mkExist vds conjF
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder Box -> mkForall vds conjF
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder EBox -> conjunct [mkExist vds conjF, mkForall vds conjF]
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder else if i <= 0 && ex && gEq then trueForm
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder else if bOp == EBox then conjunct $ map tr [Diamond, Box]
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder else if ex -- lEq
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder then transMF as . mkNeg . ExtFORMULA $ PrefixForm
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder (diam $ i + 1) f r
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder else if gEq -- Box
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder then transMF as . mkNeg . ExtFORMULA $ PrefixForm
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder (diam i) (mkNeg f) r
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder else transMF as . ExtFORMULA $ PrefixForm
3397210aac34a94e9ae85faacf7f6a02a808097eChristian Maeder (diam $ i + 1) (mkNeg f) r
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder Hybrid at i -> let ni = simpleIdToId i in
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder if at then transMF as { currentW = getTermOfNom as ni } f else let
a2cc771b106f5792a02348fd36475550b8731792Christian Maeder vi = mkVarDecl (genNumVar "i" $ fW + 1) world
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder ti = toQualVar vi
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder in mkExist [vi] $ conjunct
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder [ mkStEq ti $ currentW as
a2cc771b106f5792a02348fd36475550b8731792Christian Maeder , transMF as { boundNoms = (ni, ti) : boundNoms as
a2cc771b106f5792a02348fd36475550b8731792Christian Maeder , currentW = ti
a2cc771b106f5792a02348fd36475550b8731792Christian Maeder , freeC = fW + 1 } f ]
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder _ -> transMF as f
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder UntilSince _isUntil f1 f2 r -> conjunctRange [transMF as f1, transMF as f2] r
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder ModForm _ -> trueForm
3397210aac34a94e9ae85faacf7f6a02a808097eChristian MaedertransMod :: Args -> MODALITY -> FORMULA ()
16779ccfe622e9db869898f724bc0132b90cb7d7Christian MaedertransMod as md = let
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder t1 = currentW as
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder t2 = mkVarTerm (genNumVar "w" $ nextW as) world
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder vts = [t1, t2]
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder msig = modSig as
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder extInf = extendedInfo msig
16779ccfe622e9db869898f724bc0132b90cb7d7Christian Maeder in case md of
16779ccfe622e9db869898f724bc0132b90cb7d7Christian Maeder SimpleMod i -> let ri = simpleIdToId i in mkPredication
84c0c21396b0ebd663607b9eb745753a628f7de1Christian Maeder (mkQualPred (relOfMod False False ri)
16779ccfe622e9db869898f724bc0132b90cb7d7Christian Maeder . toPRED_TYPE $ modPredType world False ri) vts
16779ccfe622e9db869898f724bc0132b90cb7d7Christian Maeder TermMod t -> case optTermSort t of
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder Just srt -> case keepMinimals msig id . Set.toList
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder . Set.intersection (termMods extInf) . Set.insert srt
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder $ supersortsOf srt msig of
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder [] -> error $ "transMod1: " ++ showDoc t ""
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder st : _ -> mkPredication
84c0c21396b0ebd663607b9eb745753a628f7de1Christian Maeder (mkQualPred (relOfMod False True st)
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder . toPRED_TYPE $ modPredType world True st)
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder $ foldTerm (transRecord as) t : vts
c55f9e48a7d93c41ebfe7a3216ed305165346e2fChristian Maeder _ -> error $ "transMod2: " ++ showDoc t ""
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder Guard f -> conjunct [mkExEq t1 t2, transMF as f]
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder ModOp mOp m1 m2 -> case mOp of
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder Composition -> let
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder nW = freeC as + 1
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder nAs = as { freeC = nW }
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder vd = mkVarDecl (genNumVar "w" nW) world
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder in mkExist [vd] $ conjunct
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder [ transMod nAs { nextW = nW } m1
d12f7a58b996457c25e12d674153346a4e21930eChristian Maeder , transMod nAs { currentW = toQualVar vd } m2 ]
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder Intersection -> conjunct [transMod as m1, transMod as m2] -- parallel?
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder Union -> disjunct [transMod as m1, transMod as m2]
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder OrElse -> disjunct . transOrElse [] as $ flatOrElse md
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder TransClos m -> transMod as m -- ignore transitivity for now
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian MaederflatOrElse :: MODALITY -> [MODALITY]
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian MaederflatOrElse md = case md of
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder ModOp OrElse m1 m2 -> flatOrElse m1 ++ flatOrElse m2
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian MaedertransOrElse :: [FORMULA EM_FORMULA] -> Args -> [MODALITY] -> [FORMULA ()]
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian MaedertransOrElse nFs as ms = case ms of
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder md : r -> case md of
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder Guard f -> transMod as (Guard . conjunct $ f : nFs)
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder : transOrElse (mkNeg f : nFs) as r
c5ddf41fe430a758733dbc46db25d5910c85ab8cChristian Maeder _ -> transMod as md : transOrElse nFs as r