ExtModal2CASL.hs revision d12f7a58b996457c25e12d674153346a4e21930e
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
137edd3944aacd150d60af8977de962113ead859Felix Gabriel ManceModule : $Header$
137edd3944aacd150d60af8977de962113ead859Felix Gabriel ManceCopyright : (c) Christian Maeder, DFKI 2012
137edd3944aacd150d60af8977de962113ead859Felix Gabriel ManceLicense : GPLv2 or higher, see LICENSE.txt
137edd3944aacd150d60af8977de962113ead859Felix Gabriel ManceMaintainer : Christian.Maeder@dfki.de
137edd3944aacd150d60af8977de962113ead859Felix Gabriel ManceStability : provisional
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancePortability : non-portable (MPTC-FD)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Manceimport qualified Common.Lib.Rel as Rel
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Manceimport qualified Common.Lib.MapSet as MapSet
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Manceimport qualified Data.Set as Set
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance-- ExtModalCASL
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mancedata ExtModal2CASL = ExtModal2CASL deriving (Show)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Manceinstance Language ExtModal2CASL
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Manceinstance Comorphism ExtModal2CASL
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance ExtModal Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Symbol RawSymbol ()
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance CASL CASL_Sublogics
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Symbol RawSymbol ProofTree where
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance sourceLogic ExtModal2CASL = ExtModal
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance sourceSublogic ExtModal2CASL = maxSublogic
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance targetLogic ExtModal2CASL = CASL
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance mapSublogic ExtModal2CASL _ = Just SL.caslTop
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance map_theory ExtModal2CASL (sig, sens) = case transSig sig of
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (mme, s) -> return (mme, s ++ map (mapNamed $ transTop sig mme) sens)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance map_morphism ExtModal2CASL = return . mapMor
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance map_sentence ExtModal2CASL sig = return . transSen sig
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance map_symbol ExtModal2CASL _ = Set.singleton . mapSym
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance has_model_expansion ExtModal2CASL = True
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance is_weakly_amalgamable ExtModal2CASL = True
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancenomName :: Id -> Id
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancenomName t = Id [genToken "N"] [t] $ rangeOfId t
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancenomOpType :: OpType
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancenomOpType = mkTotOpType [] world
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance-- | add world arguments to flexible ops and preds; and add relations
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransSig :: ExtModalSign -> (CASLSign, [Named (FORMULA ())])
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransSig sign = let
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance s1 = embedSign () sign
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance extInf = extendedInfo sign
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance flexibleOps = flexOps extInf
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance flexiblePreds = flexPreds extInf
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance flexOps' = addWorldOp world addPlace flexibleOps
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance flexPreds' = addWorldPred world addPlace flexiblePreds
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance rigOps' = diffOpMapSet (opMap sign) flexibleOps
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance rigPreds' = diffMapSet (predMap sign) flexiblePreds
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance noms = nominals extInf
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance noNomsPreds = Set.fold (`MapSet.delete` nomPType) rigPreds' noms
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance termMs = termMods extInf
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance timeMs = timeMods extInf
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance insertModPred world (Set.member m timeMs) (Set.member m termMs) m)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance MapSet.empty $ modalities extInf
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance nomOps = Set.fold (\ n -> addOpTo (nomName n) nomOpType) rigOps' noms
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance vds = map (\ n -> mkVarDecl (genNumVar "v" n) world) [1, 2]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance ts = map toQualVar vds
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance { sortRel = Rel.insertKey world $ sortRel sign
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance , opMap = addOpMapSet flexOps' nomOps
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance , assocOps = diffOpMapSet (assocOps sign) flexibleOps
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance , predMap = (if Set.null timeMs then id else MapSet.insert tauId tauTy)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance . addMapSet rels
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance $ addMapSet flexPreds' noNomsPreds
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance } , if Set.null timeMs then [] else
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance [makeNamed "tau" . mkForall vds . mkEqv
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (mkPredication (mkQualPred tauId $ toPRED_TYPE tauTy) ts)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance . disjunct . map (\ tm ->
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance let v = mkVarDecl (genNumVar "t" 0) tm
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance term = Set.member tm termMs
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance in (if term then mkExist [v] else id) $ mkPredication
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (mkQualPred (relOfMod True term tm)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance . toPRED_TYPE $ modPredType world term tm)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance $ if term then toQualVar v : ts else ts) $ Set.toList timeMs])
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mancedata Args = Args
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance { currentW :: TERM ()
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance , nextW, freeC :: Int -- world variables
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance , boundNoms :: [(Id, TERM ())]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance , modSig :: ExtModalSign
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransTop :: ExtModalSign -> CASLSign -> FORMULA EM_FORMULA -> FORMULA ()
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransTop msig csig = let
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance vd = mkVarDecl (genNumVar "w" 1) world
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance vt = toQualVar vd
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance in stripQuant csig . mkForall [vd]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance . transMF (Args vt 1 1 [] msig)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancegetTermOfNom :: Args -> Id -> TERM ()
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancegetTermOfNom as i = fromMaybe (mkNomAppl i) . lookup i $ boundNoms as
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetauId = genName "Tau"
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetauTy :: PredType
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetauTy = PredType [world, world]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance-- TODO: check that constructors are not flexible!
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancemkNomAppl :: Id -> TERM ()
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancemkNomAppl pn = mkAppl (mkQualOp (nomName pn) $ toOP_TYPE nomOpType) []
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransRecord :: Args -> Record EM_FORMULA (FORMULA ()) (TERM ())
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransRecord as = let
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance extInf = extendedInfo $ modSig as
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance currW = currentW as
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance in (mapRecord $ const ())
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance { foldPredication = \ _ ps args r -> case ps of
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Qual_pred_name pn pTy@(Pred_type srts q) p
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance | MapSet.member pn (toPredType pTy) $ flexPreds extInf
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance -> Predication
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (Qual_pred_name (addPlace pn) (Pred_type (world : srts) q) p)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (currW : args) r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance | null srts && Set.member pn (nominals extInf)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance -> mkStEq currW $ getTermOfNom as pn
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance _ -> Predication ps args r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance , foldExtFORMULA = \ _ f -> transEMF as f
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance , foldApplication = \ _ os args r -> case os of
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Qual_op_name opn oTy@(Op_type ok srts res q) p
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance | MapSet.member opn (toOpType oTy) $ flexOps extInf
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance -> Application
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (Qual_op_name (addPlace opn) (Op_type ok (world : srts) res q) p)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (currW : args) r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance _ -> Application os args r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransMF :: Args -> FORMULA EM_FORMULA -> FORMULA ()
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransMF = foldFormula . transRecord
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancedisjointVars :: [VAR_DECL] -> [FORMULA ()]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancedisjointVars vs = case vs of
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance a : r@(b : _) -> mkNeg (on mkStEq toQualVar a b) : disjointVars r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransEMF :: Args -> EM_FORMULA -> FORMULA ()
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransEMF as emf = case emf of
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance PrefixForm pf f r -> let
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance BoxOrDiamond bOp m gEq i -> let
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance ex = bOp == Diamond
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance l = [fW + 1 .. fW + i]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance vds = map (\ n -> mkVarDecl (genNumVar "w" n) world) l
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance nAs = as { freeC = fW + i }
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance tf n = transMF nAs { currentW = mkVarTerm (genNumVar "w" n) world } f
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance tM n = transMod nAs { nextW = n } m
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance conjF = conjunct $ map tM l ++ map tf l ++ disjointVars vds
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance diam = BoxOrDiamond Diamond m True
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance tr b = transEMF as $ PrefixForm (BoxOrDiamond b m gEq i) f r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance in if gEq && i > 0 && (i == 1 || ex) then case bOp of
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Diamond -> mkExist vds conjF
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Box -> mkForall vds conjF
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance EBox -> conjunct [mkExist vds conjF, mkForall vds conjF]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance else if i <= 0 && ex && gEq then trueForm
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance else if bOp == EBox then conjunct $ map tr [Diamond, Box]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance else if ex -- lEq
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance then transMF as . mkNeg . ExtFORMULA $ PrefixForm
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (diam $ i + 1) f r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance else if gEq -- Box
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance then transMF as . mkNeg . ExtFORMULA $ PrefixForm
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (diam i) (mkNeg f) r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance else transMF as . ExtFORMULA $ PrefixForm
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (diam $ i + 1) (mkNeg f) r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Hybrid at i -> let ni = simpleIdToId i in
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance if at then transMF as { currentW = getTermOfNom as ni } f else let
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance vi = mkVarDecl (genNumVar "i" fW) world
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance ti = toQualVar vi
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance in mkExist [vi] $ conjunct
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance [ mkStEq ti $ currentW as
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance , transMF as { boundNoms = (ni, ti) : boundNoms as } f ]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance _ -> transMF as f
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance UntilSince _isUntil f1 f2 r -> conjunctRange [transMF as f1, transMF as f2] r
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance ModForm _ -> trueForm
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransMod :: Args -> MODALITY -> FORMULA ()
137edd3944aacd150d60af8977de962113ead859Felix Gabriel MancetransMod as md = let
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance t1 = currentW as
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance t2 = mkVarTerm (genNumVar "w" $ nextW as) world
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance vts = [t1, t2]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance msig = modSig as
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance extInf = extendedInfo msig
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance timeMs = timeMods extInf
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance SimpleMod i -> let ri = simpleIdToId i in mkPredication
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (mkQualPred (relOfMod (Set.member ri timeMs) False ri)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance . toPRED_TYPE $ modPredType world False ri) vts
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance TermMod t -> case optTermSort t of
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Just srt -> case keepMinimals msig id . Set.toList
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance . Set.intersection (termMods extInf) . Set.insert srt
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance $ supersortsOf srt msig of
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance [] -> error $ "transMod1: " ++ showDoc t ""
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance st : _ -> mkPredication
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance (mkQualPred (relOfMod (Set.member st timeMs) True st)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance . toPRED_TYPE $ modPredType world True st)
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance $ foldTerm (transRecord as) t : vts
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance _ -> error $ "transMod2: " ++ showDoc t ""
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Guard f -> conjunct [mkExEq t1 t2, transMF as f]
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance ModOp mOp m1 m2 -> case mOp of
137edd3944aacd150d60af8977de962113ead859Felix Gabriel Mance Composition -> let