ExtModal2HasCASL.hs revision 8a94f9add1f11ef1b57be38c71b69f286b004aca
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederModule : $Header$
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederCopyright : (c) Christian Maeder, DFKI 2012
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederMaintainer : Christian.Maeder@dfki.de
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederStability : provisional
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederPortability : non-portable (MPTC-FD)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport qualified Common.Lib.Rel as Rel
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport qualified Common.Lib.MapSet as MapSet
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maederimport qualified Data.Map as Map
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maederimport qualified Data.Set as Set
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederdata ExtModal2HasCASL = ExtModal2HasCASL deriving (Show)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederinstance Language ExtModal2HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederinstance Comorphism ExtModal2HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder ExtModal EM.Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder BasicSpec Sentence SymbItems SymbMapItems
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Env HC.Morphism HC.Symbol HC.RawSymbol () where
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder sourceLogic ExtModal2HasCASL = ExtModal
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder sourceSublogic ExtModal2HasCASL = maxSublogic
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder targetLogic ExtModal2HasCASL = HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder mapSublogic ExtModal2HasCASL _ = Just HC.caslLogic { which_logic = HOL }
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder map_theory ExtModal2HasCASL (sig, sens) = case transSig sig sens of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder mme -> return (mme, map (mapNamed $ toSen sig mme) sens)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_morphism ExtModal2HasCASL = return . mapMor
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_sentence ExtModal2HasCASL sig = return . transSen sig
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_symbol ExtModal2HasCASL _ = Set.singleton . mapSym
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder has_model_expansion ExtModal2HasCASL = True
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder is_weakly_amalgamable ExtModal2HasCASL = True
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomName :: Id -> Id
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomName t = Id [genToken "N"] [t] $ rangeOfId t
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomOpType :: OpType
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomOpType = mkTotOpType [] world
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertauId = genName "Tau"
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertauTy :: PredType
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertauTy = PredType [world, world]
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder-- | mixfix names work for tuples and are lost after currying
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrI :: Id -> Id
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrI i = if isMixfix i then Id [genToken "C"] [i] $ rangeOfId i else i
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrOpSyn :: OP_TYPE -> Type
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrOpSyn (Op_type ok args res _) = let
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder (partial, total) = case ok of
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder resTy = toType res
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder in if null args then if total then resTy else mkLazyType resTy
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder else getFunType resTy partial $ map toType args
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrOp :: OpType -> TypeScheme
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrOp = simpleTypeScheme . trOpSyn . toOP_TYPE
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrPrSyn :: PRED_TYPE -> Type
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrPrSyn (Pred_type args ps) = let u = unitTypeWithRange ps in
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder if null args then mkLazyType u else
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder getFunType u HC.Partial $ map toType args
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrPr :: PredType -> TypeScheme
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrPr = simpleTypeScheme . trPrSyn . toPRED_TYPE
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder-- | add world arguments to flexible ops and preds; and add relations
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertransSig :: ExtModalSign -> [Named (FORMULA EM_FORMULA)] -> Env
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertransSig sign sens = let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder s1 = embedSign () sign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder extInf = extendedInfo sign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder flexibleOps = flexOps extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder flexiblePreds = flexPreds extInf
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder flexOps' = addWorldOp world id flexibleOps
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder flexPreds' = addWorldPred world id flexiblePreds
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder rigOps' = diffOpMapSet (opMap sign) flexibleOps
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder rigPreds' = diffMapSet (predMap sign) flexiblePreds
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder noms = nominals extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder noNomsPreds = Set.fold (`MapSet.delete` nomPType) rigPreds' noms
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder termMs = termMods extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder timeMs = timeMods extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder rels = Set.fold (\ m ->
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder insertModPred world (Set.member m timeMs) (Set.member m termMs) m)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder MapSet.empty $ modalities extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder nomOps = Set.fold (\ n -> addOpTo (nomName n) nomOpType) rigOps' noms
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder { sortRel = Rel.insertKey world $ sortRel sign
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder , opMap = addOpMapSet flexOps' nomOps
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder , predMap = (if Set.null timeMs then id else MapSet.insert tauId tauTy)
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder . addMapSet rels $ addMapSet flexPreds' noNomsPreds
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder in mapSigAux trI trOp trPr (getConstructors sens) s2
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maederdata Args = Args
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder { currentW :: Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , nextW, freeC :: Int -- world variables
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , boundNoms :: [(Id, Term)]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , modSig :: ExtModalSign
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedervarDecl :: Token -> SORT -> VarDecl
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedervarDecl i s = VarDecl (simpleIdToId i) (toType s) Other nullRange
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedergenVarDecl :: Token -> SORT -> GenVarDecl
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedergenVarDecl i = GenVarDecl . varDecl i
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedervarTerm :: Token -> SORT -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedervarTerm i = QualVar . varDecl i
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertoSen :: ExtModalSign -> Env -> FORMULA EM_FORMULA -> Sentence
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertoSen msig env f = case f of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Sort_gen_ax cs b -> let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (sorts, ops, smap) = recover_Sort_gen_ax cs
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder genKind = if b then Free else Generated
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder mapPart :: OpKind -> Partiality
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder mapPart cp = case cp of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in DatatypeSen $ map ( \ s ->
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder DataEntry (Map.fromList smap) s genKind [] rStar
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ Set.fromList $ map ( \ (i, t) ->
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder let args = map toType $ opArgs t in
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Construct (if isInjName i then Nothing else Just i) args
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (mapPart $ opKind t)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ map (\ a -> [Select Nothing a HC.Total]) args)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ filter ( \ (_, t) -> opRes t == s)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ map ( \ o -> case o of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Qual_op_name i t _ -> (trI i, toOpType t)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> error "ExtModal2HasCASL.toSentence") ops) sorts
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> Formula $ transTop msig env f
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransTop :: ExtModalSign -> Env -> FORMULA EM_FORMULA -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransTop msig env f = let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder vt = varTerm (genNumVar "w" 1) world
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in mkEnvForall env
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (transMF (Args vt 1 1 [] msig) f) nullRange
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedergetTermOfNom :: Args -> Id -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedergetTermOfNom as i = fromMaybe (mkNomAppl i) . lookup i $ boundNoms as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedermkNomAppl :: Id -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedermkNomAppl pn = mkOpTerm (nomName pn) $ trOp nomOpType
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertrRecord :: Args -> String -> Record EM_FORMULA Term Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertrRecord as str = let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder extInf = extendedInfo $ modSig as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder currW = currentW as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in (transRecord str)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder { foldPredication = \ _ ps args _ -> let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Qual_pred_name pn pTy@(Pred_type srts q) p = ps
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in if MapSet.member pn (toPredType pTy) $ flexPreds extInf
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder then mkApplTerm
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (mkOpTerm (trI pn) . simpleTypeScheme . trPrSyn
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ Pred_type (world : srts) q) $ currW : args
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else if null srts && Set.member pn (nominals extInf)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder then mkEqTerm eqId (toType world) p currW $ getTermOfNom as pn
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else mkApplTerm
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (mkOpTerm (trI pn) . simpleTypeScheme $ trPrSyn pTy) args
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , foldExtFORMULA = \ _ f -> transEMF as f
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , foldApplication = \ _ os args _ -> let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Qual_op_name opn oTy@(Op_type ok srts res q) _ = os
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in if MapSet.member opn (toOpType oTy) $ flexOps extInf
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder then mkApplTerm
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (mkOpTerm (trI opn) . simpleTypeScheme . trOpSyn
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ Op_type ok (world : srts) res q) $ currW : args
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else mkApplTerm
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (mkOpTerm (trI opn) . simpleTypeScheme $ trOpSyn oTy) args
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransMF :: Args -> FORMULA EM_FORMULA -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransMF a f = foldFormula (trRecord a $ showDoc f "") f
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaederdisjointVars :: [VarDecl] -> [Term]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaederdisjointVars vs = case vs of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder a : r@(b : _) -> mkTerm notId notType [] nullRange
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (on (mkEqTerm eqId (toType world) nullRange) QualVar a b) : disjointVars r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransEMF :: Args -> EM_FORMULA -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransEMF as emf = case emf of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder PrefixForm pf f r -> let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder fW = freeC as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in case pf of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder BoxOrDiamond bOp m gEq i -> let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder ex = bOp == Diamond
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder l = [fW + 1 .. fW + i]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder vds = map (\ n -> varDecl (genNumVar "w" n) world) l
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder gvs = map GenVarDecl vds
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder nAs = as { freeC = fW + i }
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder tf n = transMF nAs { currentW = varTerm (genNumVar "w" n) world } f
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder tM n = transMod nAs { nextW = n } m
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder conjF = toBinJunctor andId
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (map tM l ++ map tf l ++ disjointVars vds) r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder diam = BoxOrDiamond Diamond m True
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder tr b = transEMF as $ PrefixForm (BoxOrDiamond b m gEq i) f r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder f1 = QuantifiedTerm HC.Existential gvs conjF r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in if gEq && i > 0 && (i == 1 || ex) then case bOp of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Diamond -> f1
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder EBox -> toBinJunctor andId [f1, f2] r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else if i <= 0 && ex && gEq then unitTerm trueId r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else if bOp == EBox then toBinJunctor andId (map tr [Diamond, Box]) r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else if ex -- lEq
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder then transMF as . mkNeg . ExtFORMULA $ PrefixForm
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (diam $ i + 1) f r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else if gEq -- Box
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder then transMF as . mkNeg . ExtFORMULA $ PrefixForm
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (diam i) (mkNeg f) r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else transMF as . ExtFORMULA $ PrefixForm
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (diam $ i + 1) (mkNeg f) r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Hybrid at i -> let ni = simpleIdToId i in
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder if at then transMF as { currentW = getTermOfNom as ni } f else let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder vi = varDecl (genNumVar "i" $ fW + 1) world
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder ti = QualVar vi
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in QuantifiedTerm HC.Existential [GenVarDecl vi]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (toBinJunctor andId
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder [ mkEqTerm eqId (toType world) r ti $ currentW as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , transMF as { boundNoms = (ni, ti) : boundNoms as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , currentW = ti
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , freeC = fW + 1 } f ] r) r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> transMF as f
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder UntilSince _isUntil f1 f2 r ->
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder toBinJunctor andId [transMF as f1, transMF as f2] r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder ModForm _ -> unitTerm trueId nullRange
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransMod :: Args -> MODALITY -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransMod as md = let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder t1 = currentW as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder t2 = varTerm (genNumVar "w" $ nextW as) world
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder vts = [t1, t2]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder msig = modSig as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder extInf = extendedInfo msig
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder timeMs = timeMods extInf
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in case md of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder SimpleMod i -> let ri = simpleIdToId i in mkApplTerm
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (mkOpTerm (relOfMod (Set.member ri timeMs) False ri)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder . trPr $ modPredType world False ri) vts
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder TermMod t -> case optTermSort t of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Just srt -> case keepMinimals msig id . Set.toList
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder . Set.intersection (termMods extInf) . Set.insert srt
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ supersortsOf srt msig of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder [] -> error $ "transMod1: " ++ showDoc t ""
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder st : _ -> mkApplTerm
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (mkOpTerm (relOfMod (Set.member st timeMs) True st)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder . trPr $ modPredType world True st)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ foldTerm (trRecord as $ showDoc t "") t : vts
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> error $ "transMod2: " ++ showDoc t ""
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Guard f -> toBinJunctor andId
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder [mkEqTerm exEq (toType world) nullRange t1 t2, transMF as f] nullRange
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder ModOp mOp m1 m2 -> case mOp of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Composition -> let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder nW = freeC as + 1
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder nAs = as { freeC = nW }
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder vd = varDecl (genNumVar "w" nW) world
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in QuantifiedTerm HC.Existential [GenVarDecl vd] (toBinJunctor andId
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder [ transMod nAs { nextW = nW } m1
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , transMod nAs { currentW = QualVar vd } m2 ] nullRange)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Intersection -> toBinJunctor andId [transMod as m1, transMod as m2]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Union -> toBinJunctor orId [transMod as m1, transMod as m2] nullRange
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder OrElse -> toBinJunctor orId (transOrElse [] as $ flatOrElse md) nullRange
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder TransClos m -> transMod as m -- ignore transitivity for now
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaederflatOrElse :: MODALITY -> [MODALITY]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaederflatOrElse md = case md of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder ModOp OrElse m1 m2 -> flatOrElse m1 ++ flatOrElse m2
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransOrElse :: [FORMULA EM_FORMULA] -> Args -> [MODALITY] -> [Term]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransOrElse nFs as ms = case ms of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder md : r -> case md of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Guard f -> transMod as (Guard . conjunct $ f : nFs)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder : transOrElse (mkNeg f : nFs) as r
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> transMod as md : transOrElse nFs as r