ExtModal2HasCASL.hs revision 9ad3eca7ffa4b65d03bf9443f5b85b274a038d1a
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)
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maedermodule Comorphisms.ExtModal2HasCASL (ExtModal2HasCASL (..)) where
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
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder (mme, s) -> return
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder (mme, map (\ (n, d) -> makeNamed n $ DatatypeSen [d])
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder [("natural numbers", natType), ("numbered worlds", worldType)]
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder ++ s ++ 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
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaedertauS :: String
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaedertauId = genName tauS
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedertauCaslTy :: PredType
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedertauCaslTy = PredType [world, world]
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedertauTy = trPrSyn $ toPRED_TYPE tauCaslTy
5bc55095489c7fb939535865b588b04957853446Christian Maeder{- | we now consider numbered worlds:
5bc55095489c7fb939535865b588b04957853446Christian Maeder free type WN ::= WN World Nat -}
5bc55095489c7fb939535865b588b04957853446Christian MaedernWorldId :: SORT
5bc55095489c7fb939535865b588b04957853446Christian MaedernWorldId = genName "WN"
5bc55095489c7fb939535865b588b04957853446Christian MaedernWorld :: Type
5bc55095489c7fb939535865b588b04957853446Christian MaedernWorld = toType nWorldId
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederbinPredTy :: Type -> Type
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederbinPredTy = getFunType unitType HC.Partial . replicate 2
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaederisTransS :: String
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaederisTransS = "isTrans"
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaederisTransId :: Id
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaederisTransId = genName isTransS
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederprOfBinPrTy :: Type -> Type
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederprOfBinPrTy = predType nr . binPredTy
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederprOfNwPrTy :: Type
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederprOfNwPrTy = prOfBinPrTy nWorld
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaedercontainsS :: String
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaedercontainsS = "contains"
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedercontainsId :: Id
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaedercontainsId = genName containsS
94e228feb6eb06e1b1564146d00d54734b8e3307Christian MaedertransTy :: Type -> Type
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaedertransTy = getFunType unitType HC.Partial . replicate 2 . binPredTy
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
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedertrOp :: OpType -> Type
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedertrOp = 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
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedertrPr :: PredType -> Type
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedertrPr = trPrSyn . toPRED_TYPE
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder-- | add world arguments to flexible ops and preds; and add relations
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian MaedertransSig :: ExtModalSign -> [Named (FORMULA EM_FORMULA)]
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian Maeder -> (Env, [Named Sentence])
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
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder , predMap = addMapSet rels $ addMapSet flexPreds' noNomsPreds
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder env = mapSigAux trI trOp trPr (getConstructors sens) s2
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder mkOpInfo t = Set.singleton . OpInfo (simpleTypeScheme t) Set.empty
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder insF (i, t) = insOpInfo i . mkOpInfo t $ NoOpDefn Fun
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder { assumps = foldr (uncurry insOpInfo)
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder (foldr insF (assumps env)
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder [ (tauId, tauTy)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder , (isTransId, prOfNwPrTy)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder , (reflexId, prOfNwPrTy)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder , (irreflexId, prOfNwPrTy)
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder , (containsId, transTy nWorld)
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder , (transId, transTy nWorld)
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder , (transReflexId, transTy nWorld)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder , (transLinearOrderId, prOfNwPrTy)
a7f28197b52180ffd32affa3625ac742338158f8Christian Maeder , (hasSuccessorId, hasSuccessorTy)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder , (subsetOfTauId, prOfNwPrTy)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder , (hasTauSucId, prOfNwPrTy)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder , (superpathId, hasSuccessorTy)
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder [ altToOpInfo natId zeroAlt
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder , altToOpInfo natId sucAlt
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder , altToOpInfo nWorldId worldAlt
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder , selWorldInfo getWorldSel
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder , selWorldInfo numSel
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder , typeMap = Map.insert nWorldId starTypeInfo
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder { typeDefn = DatatypeDefn worldType }
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder . Map.insert natId starTypeInfo
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder { typeDefn = DatatypeDefn natType }
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder $ typeMap env
0825423cb8c7ce148f77681f932425701cade405Christian Maeder , makeNamed "nat_induction" (Formula $ inductionScheme [natType])
0825423cb8c7ce148f77681f932425701cade405Christian Maeder : makeDataSelEqs (toDataPat worldType) [worldAlt]
0825423cb8c7ce148f77681f932425701cade405Christian Maeder ++ map (\ (s, t) -> makeNamed s $ Formula t)
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian Maeder [ (tauS, tauDef termMs $ Set.toList timeMs)
5bc55095489c7fb939535865b588b04957853446Christian Maeder , (isTransS, isTransDef nWorld)
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder , (reflexS, reflexDef True nWorld)
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder , (irreflexS, reflexDef False nWorld)
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder , (containsS, containsDef nWorld)
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder , (transS, someDef transId (transContainsDef nWorld) nWorld)
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder , (transReflexS, someDef transReflexId
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder (transReflexContainsDef nWorld) nWorld)
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder , (transLinearOrderS, transLinearOrderDef nWorld)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder , (hasSuccessorS, hasSuccessorDef)
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder , (subsetOfTauS, subsetOfTauDef)
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder , (hasTauSucS, hasTauSucDefAny)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder , (superpathS, superpathDef)
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedervQuad :: Type -> [VarDecl]
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedervQuad w = map (\ n -> hcVarDecl (genNumVar "v" n) w) [1, 2, 3, 4]
afe70330421b8b596e0c880d910cb9857053f3afChristian MaederquadDs :: Type -> [GenVarDecl]
afe70330421b8b596e0c880d910cb9857053f3afChristian MaederquadDs = map GenVarDecl . vQuad
5bc55095489c7fb939535865b588b04957853446Christian MaedertripDs :: Type -> [GenVarDecl]
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertripDs = take 3 . quadDs
5bc55095489c7fb939535865b588b04957853446Christian MaederpairDs :: Type -> [GenVarDecl]
5bc55095489c7fb939535865b588b04957853446Christian MaederpairDs = take 2 . tripDs
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertQuad :: Type -> [Term]
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertQuad = map QualVar . vQuad
5bc55095489c7fb939535865b588b04957853446Christian MaedertTrip :: Type -> [Term]
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertTrip = take 3 . tQuad
5bc55095489c7fb939535865b588b04957853446Christian MaedertPair :: Type -> [Term]
5bc55095489c7fb939535865b588b04957853446Christian MaedertPair = take 2 . tTrip
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maedernr = nullRange
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederworldTy :: Type
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederworldTy = toType world
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian MaedertauDef :: Set.Set Id -> [Id] -> Term
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedertauDef termMs timeMs = let ts = tPair worldTy in
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder HC.mkForall (pairDs worldTy)
a9ba344f36a2ee2d25c7c2bcbf46ba710de736eaChristian Maeder . mkLogTerm eqvId nr
5bc55095489c7fb939535865b588b04957853446Christian Maeder (mkApplTerm (mkOp tauId tauTy) ts)
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder $ map (\ tm ->
a9ba344f36a2ee2d25c7c2bcbf46ba710de736eaChristian Maeder let v = varDecl (genToken "t") tm
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian Maeder term = Set.member tm termMs
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian Maeder in (if term then mkExQ v else id) $ mkApplTerm
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder (mkOp (relOfMod True term tm)
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian Maeder . trPr $ modPredType world term tm)
5bc55095489c7fb939535865b588b04957853446Christian Maeder $ if term then QualVar v : ts else ts)
08fa7405566a83131a773e82e9514d67e30233c9Christian MaederpVar :: Type -> VarDecl
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederpVar = hcVarDecl (genToken "p") . binPredTy
5bc55095489c7fb939535865b588b04957853446Christian MaederisTransDef :: Type -> Term
5bc55095489c7fb939535865b588b04957853446Christian MaederisTransDef w = let
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder pt = QualVar p
5bc55095489c7fb939535865b588b04957853446Christian Maeder [t1, t2, t3] = tTrip w
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder in HC.mkForall [GenVarDecl p]
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder . mkLogTerm eqvId nr
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder (mkApplTerm (mkOp isTransId $ prOfBinPrTy w) [pt])
a9ba344f36a2ee2d25c7c2bcbf46ba710de736eaChristian Maeder . mkLogTerm implId nr
a9ba344f36a2ee2d25c7c2bcbf46ba710de736eaChristian Maeder (mkLogTerm andId nr
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder (mkApplTerm pt [t1, t2])
a9ba344f36a2ee2d25c7c2bcbf46ba710de736eaChristian Maeder $ mkApplTerm pt [t2, t3])
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder $ mkApplTerm pt [t1, t3]
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertrichotomyDef :: Type -> Term -> Term -> Term -> Term
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertrichotomyDef w pt t1 t2 = mkLogTerm orId nr
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder (dichotomyDef pt t1 t2)
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder $ mkEqTerm eqId w nr t1 t2
afe70330421b8b596e0c880d910cb9857053f3afChristian MaederdichotomyDef :: Term -> Term -> Term -> Term
afe70330421b8b596e0c880d910cb9857053f3afChristian MaederdichotomyDef pt t1 t2 = mkLogTerm orId nr
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder (mkApplTerm pt [t1, t2])
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder $ mkApplTerm pt [t2, t1]
afe70330421b8b596e0c880d910cb9857053f3afChristian MaederlinearOrderDef :: Type -> Term -> Term
afe70330421b8b596e0c880d910cb9857053f3afChristian MaederlinearOrderDef w pt = let
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder [t1, t2, t3, t4] = tQuad w
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder . mkLogTerm implId nr
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder (mkExQs (drop 2 $ quadDs w)
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder . mkLogTerm andId nr
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder (dichotomyDef pt t1 t3)
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder $ dichotomyDef pt t2 t4)
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder $ trichotomyDef w pt t1 t2
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertransLinearOrderS :: String
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertransLinearOrderS = "trans_linear_order"
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertransLinearOrderId :: Id
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertransLinearOrderId = genName transLinearOrderS
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertransLinearOrderDef :: Type -> Term
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedertransLinearOrderDef w = let
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder [pv, qv] = map GenVarDecl ps
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder ts@[pt, qt] = map QualVar ps
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder . mkLogTerm eqvId nr
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder (mkApplTerm (mkOp transLinearOrderId $ prOfBinPrTy w) [pt])
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder . mkExQs [qv]
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder . mkLogTerm andId nr
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder (mkApplTerm (mkOp transId $ transTy w) ts)
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder $ linearOrderDef w qt
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedernatId = stringToId "Nat"
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedernatTy = toType natId
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedersucId = stringToId "suc"
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maederzero = stringToId "0"
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedernatType :: DataEntry
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder DataEntry Map.empty natId Free [] rStar
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder $ Set.fromList [zeroAlt, sucAlt]
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederzeroAlt :: AltDefn
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederzeroAlt = Construct (Just zero) [] HC.Total []
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedersucAlt :: AltDefn
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedersucAlt = Construct (Just sucId) [natTy] HC.Total [typeToSelector Nothing natTy]
aab870997808945ad279711662d457a225c53011Christian MaederaltToTy :: Id -> AltDefn -> Type
aab870997808945ad279711662d457a225c53011Christian MaederaltToTy i (Construct _ ts p _) = getFunType (toType i) p ts
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederaltToOpInfo :: Id -> AltDefn -> (Id, Set.Set OpInfo)
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederaltToOpInfo i c@(Construct m _ _ _) = let Just n = m in
aab870997808945ad279711662d457a225c53011Christian Maeder OpInfo (simpleTypeScheme $ altToTy i c) Set.empty
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder $ ConstructData i)
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedergetWorldId :: Id
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedergetWorldId = genName "getWorld"
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedernumId = genName "num"
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederworldType :: DataEntry
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederworldType = DataEntry Map.empty nWorldId Free [] rStar $ Set.singleton worldAlt
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederworldAlt :: AltDefn
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederworldAlt = Construct (Just nWorldId) [worldTy, natTy] HC.Total
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder [getWorldSel, numSel]
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedergetWorldSel :: [Selector]
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedergetWorldSel = typeToSelector (Just getWorldId) worldTy
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedernumSel :: [Selector]
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedernumSel = typeToSelector (Just numId) natTy
aab870997808945ad279711662d457a225c53011Christian MaedernWorldTy :: Type
aab870997808945ad279711662d457a225c53011Christian MaedernWorldTy = altToTy nWorldId worldAlt
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederselWorldInfo :: [Selector] -> (Id, Set.Set OpInfo)
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederselWorldInfo = selToOpInfo nWorldId . Set.singleton . ConstrInfo nWorldId
aab870997808945ad279711662d457a225c53011Christian Maeder $ simpleTypeScheme nWorldTy
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaederselToTy :: Id -> [Selector] -> (Id, Type)
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaederselToTy i s = let [Select (Just n) t p] = s in
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder (n, getFunType t p [toType i])
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaederselToOpInfo :: Id -> Set.Set ConstrInfo -> [Selector] -> (Id, Set.Set OpInfo)
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaederselToOpInfo i c s = let (n, ty) = selToTy i s in
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder (n, Set.singleton . OpInfo (simpleTypeScheme ty) Set.empty
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder $ SelectData c i)
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian MaederpAndQ :: Type -> [VarDecl]
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederpAndQ w = map (\ c -> hcVarDecl (genToken [c]) $ binPredTy w) "pq"
5bc55095489c7fb939535865b588b04957853446Christian MaedercontainsDef :: Type -> Term
5bc55095489c7fb939535865b588b04957853446Christian MaedercontainsDef w = let -- q contains p
5bc55095489c7fb939535865b588b04957853446Christian Maeder [pt, qt] = map QualVar ps
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian Maeder in HC.mkForall (map GenVarDecl ps)
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian Maeder . mkLogTerm eqvId nr
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder (mkApplTerm (mkOp containsId $ transTy w) [pt, qt])
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian Maeder . mkLogTerm implId nr
5bc55095489c7fb939535865b588b04957853446Christian Maeder (mkApplTerm pt ts)
5bc55095489c7fb939535865b588b04957853446Christian Maeder $ mkApplTerm qt ts
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedersomeContainsDef :: (Term -> Term) -> Type -> Term -> Term -> Term
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedersomeContainsDef sPred w pt qt = let -- q fulfills sPred and contains p
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder ts = [pt, qt]
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder in mkLogTerm andId nr (sPred qt)
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder $ mkApplTerm (mkOp containsId $ transTy w) ts
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedertransContainsDef :: Type -> Term -> Term -> Term
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedertransContainsDef w = someContainsDef
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder (\ qt -> mkApplTerm (mkOp isTransId $ prOfBinPrTy w) [qt]) w
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedertransReflexContainsDef :: Type -> Term -> Term -> Term
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedertransReflexContainsDef w = someContainsDef
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder (\ qt -> mkLogTerm andId nr
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder (mkApplTerm (mkOp isTransId $ prOfBinPrTy w) [qt])
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder $ mkApplTerm (mkOp reflexId $ prOfBinPrTy w) [qt]) w
94e228feb6eb06e1b1564146d00d54734b8e3307Christian MaedertransS :: String
94e228feb6eb06e1b1564146d00d54734b8e3307Christian MaedertransS = "trans"
94e228feb6eb06e1b1564146d00d54734b8e3307Christian MaedertransId = genName transS
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedertransReflexS :: String
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedertransReflexS = "trans_reflex"
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedertransReflexId :: Id
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedertransReflexId = genName transReflexS
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedersomeDef :: Id -> (Term -> Term -> Term) -> Type -> Term
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedersomeDef dId op w = let -- q is the (smallest) something containing p
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder ts@[pt, qt] = map QualVar ps
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder z = hcVarDecl (genToken "Z") $ binPredTy w
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder zt = QualVar z
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder in HC.mkForall (map GenVarDecl ps)
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder . mkLogTerm eqvId nr
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder (mkApplTerm (mkOp dId $ transTy w) ts)
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder . mkLogTerm andId nr (op pt qt)
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder . HC.mkForall [GenVarDecl z]
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder . mkLogTerm implId nr (op pt zt)
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder $ mkApplTerm (mkOp containsId $ transTy w) [qt, zt]
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederreflexS :: String
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederreflexS = "reflex"
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederirreflexS :: String
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederirreflexS = "irreflex"
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederreflexId :: Id
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederreflexId = genName reflexS
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederirreflexId :: Id
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederirreflexId = genName irreflexS
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederreflexDef :: Bool -> Type -> Term
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaederreflexDef refl w = let
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian Maeder x = hcVarDecl (genToken "x") w
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian Maeder pt = QualVar p
08fa7405566a83131a773e82e9514d67e30233c9Christian Maeder in HC.mkForall [GenVarDecl p]
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian Maeder . mkLogTerm eqvId nr
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian Maeder (mkApplTerm (mkOp (if refl then reflexId else irreflexId)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder $ prOfBinPrTy w) [pt])
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian Maeder . HC.mkForall [GenVarDecl x]
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian Maeder . (if refl then id else mkNot)
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian Maeder . mkApplTerm pt . replicate 2 $ QualVar x
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
a9ba344f36a2ee2d25c7c2bcbf46ba710de736eaChristian MaedervarDecl i = hcVarDecl i . toType
a9ba344f36a2ee2d25c7c2bcbf46ba710de736eaChristian MaederhcVarDecl :: Token -> Type -> VarDecl
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian MaederhcVarDecl i t = VarDecl (simpleIdToId i) t Other nr
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedervarTerm :: Token -> SORT -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedervarTerm i = QualVar . varDecl i
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedertypeToSelector :: Maybe Id -> Type -> [Selector]
05db707eaa7d8694e909a090d96ace73d686ad31Christian MaedertypeToSelector m a = [Select m a HC.Total]
a7f28197b52180ffd32affa3625ac742338158f8Christian MaederhasSuccessorS :: String
a7f28197b52180ffd32affa3625ac742338158f8Christian MaederhasSuccessorS = "has_successor"
a7f28197b52180ffd32affa3625ac742338158f8Christian MaederhasSuccessorId :: Id
a7f28197b52180ffd32affa3625ac742338158f8Christian MaederhasSuccessorId = genName hasSuccessorS
a7f28197b52180ffd32affa3625ac742338158f8Christian MaederhasSuccessorTy :: Type
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederhasSuccessorTy = getFunType unitType HC.Partial [worldTy, binPredTy nWorld]
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedertauApplTerm :: Term -> Term -> Term
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedertauApplTerm t1 t2 = mkApplTerm (mkOp tauId tauTy) [t1, t2]
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederhasSuccessorDef :: Term
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederhasSuccessorDef = let
8e450d61efe94923fa5f977e2fd490601f5251eeChristian Maeder zeroT = mkOp zero natTy
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder [x0, p] = xZeroAndP
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder (tT, _, rT) = hasTauSucDefAux zeroT
8e450d61efe94923fa5f977e2fd490601f5251eeChristian Maeder in HC.mkForall (map GenVarDecl [x0, p])
8e450d61efe94923fa5f977e2fd490601f5251eeChristian Maeder . mkLogTerm eqvId nr
a7f28197b52180ffd32affa3625ac742338158f8Christian Maeder (mkApplTerm (mkOp hasSuccessorId hasSuccessorTy) $ map QualVar [x0, p])
8e450d61efe94923fa5f977e2fd490601f5251eeChristian Maeder $ mkLogTerm implId nr tT rT
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederxZeroAndP :: [VarDecl]
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederxZeroAndP = [hcVarDecl (genNumVar "x" 0) worldTy, pVar nWorld]
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederhasTauSucDefAux :: Term -> (Term, Term, Term)
8e450d61efe94923fa5f977e2fd490601f5251eeChristian MaederhasTauSucDefAux nT = let
aab870997808945ad279711662d457a225c53011Christian Maeder x = hcVarDecl (genToken "x") worldTy
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder vs = xZeroAndP
8e450d61efe94923fa5f977e2fd490601f5251eeChristian Maeder [xt, xt0, pt] = map QualVar $ x : vs
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder tauAppl = tauApplTerm xt0 xt
aab870997808945ad279711662d457a225c53011Christian Maeder pairWorld = mkApplTerm $ mkOp nWorldId nWorldTy
aab870997808945ad279711662d457a225c53011Christian Maeder sucTy = altToTy natId sucAlt
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder pw = pairWorld [xt0, nT]
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder in (mkExQ x tauAppl, pw,
aab870997808945ad279711662d457a225c53011Christian Maeder . mkLogTerm andId nr tauAppl
aab870997808945ad279711662d457a225c53011Christian Maeder $ mkApplTerm pt
8e450d61efe94923fa5f977e2fd490601f5251eeChristian Maeder [ pairWorld [xt0, nT]
8e450d61efe94923fa5f977e2fd490601f5251eeChristian Maeder , pairWorld [xt, mkApplTerm (mkOp sucId sucTy) [nT]]])
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian MaederhasTauSucS :: String
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian MaederhasTauSucS = "has_tau_suc"
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian MaederhasTauSucId :: Id
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian MaederhasTauSucId = genName hasTauSucS
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian MaederhasTauSucDefAny :: Term
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian MaederhasTauSucDefAny = let
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder nv = hcVarDecl (genToken "n") natTy
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder nt = QualVar nv
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder [x0, p] = xZeroAndP
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder (tT, pw, rT) = hasTauSucDefAux nt
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder y = hcVarDecl (genToken "y") nWorld
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder in HC.mkForall [GenVarDecl p]
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder . mkLogTerm eqvId nr
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder (mkApplTerm (mkOp hasTauSucId prOfNwPrTy) [QualVar p])
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder . HC.mkForall (map GenVarDecl [x0, nv])
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder $ mkLogTerm implId nr
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder (mkLogTerm andId nr
bca57e47ab660e5c458c9e1a3e52800b0715520eChristian Maeder (mkExQ y $ mkApplTerm (QualVar p) [QualVar y, pw])
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedersubsetOfTauS :: String
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedersubsetOfTauS = "subset_of_tau"
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedersubsetOfTauId :: Id
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedersubsetOfTauId = genName subsetOfTauS
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedergetWorld :: Term -> Term
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedergetWorld t = mkApplTerm (uncurry mkOp $ selToTy nWorldId getWorldSel) [t]
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedersubsetOfTauDef :: Term
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian MaedersubsetOfTauDef = let
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder p = pVar nWorld
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder pt = QualVar p
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder ts@[xt, yt] = tPair nWorld
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder in HC.mkForall [GenVarDecl p]
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder . mkLogTerm eqvId nr
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder (mkApplTerm (mkOp subsetOfTauId prOfNwPrTy) [pt])
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder . HC.mkForall (pairDs nWorld)
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder . mkLogTerm implId nr
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder (mkApplTerm pt ts)
fe8c6bddfe2edfc7651808af0ee0a3574b36a9ceChristian Maeder . tauApplTerm (getWorld xt) $ getWorld yt
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaedersuperpathS :: String
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaedersuperpathS = "superpath"
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaedersuperpathId :: Id
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaedersuperpathId = genName superpathS
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaedersuperpathDef :: Term
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaedersuperpathDef = let
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder vs = xZeroAndP
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder ts@[_, pt] = map QualVar vs
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder in HC.mkForall (map GenVarDecl vs)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder . mkLogTerm eqvId nr
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder (mkApplTerm (mkOp superpathId hasSuccessorTy) ts)
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder $ mkApplTerm (mkOp hasSuccessorId hasSuccessorTy) ts
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder : map (\ i -> mkApplTerm (mkOp i prOfNwPrTy) [pt])
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder [irreflexId, subsetOfTauId, hasTauSucId, transLinearOrderId]
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)
05db707eaa7d8694e909a090d96ace73d686ad31Christian Maeder $ map (typeToSelector Nothing) 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
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder (transMF (Args vt 1 1 [] msig) f) nr
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedergetTermOfNom :: Args -> Id -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedergetTermOfNom as i = fromMaybe (mkNomAppl i) . lookup i $ boundNoms as
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedermkOp :: Id -> Type -> Term
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedermkOp i = mkOpTerm i . simpleTypeScheme
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedermkNomAppl :: Id -> Term
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedermkNomAppl pn = mkOp (nomName pn) $ trOp nomOpType
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian MaedereqWorld :: Id -> Term -> Term -> Term
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian MaedereqWorld i = mkEqTerm i (toType world) nr
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian MaedereqW :: Term -> Term -> Term
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian MaedereqW = eqWorld eqId
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaedermkNot :: Term -> Term
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian MaedermkNot = mkTerm notId notType [] nr
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian MaedermkConj :: [Term] -> Term
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian MaedermkConj l = toBinJunctor andId l nr
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian MaedermkDisj :: [Term] -> Term
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder (if null l then unitTerm falseId else toBinJunctor orId l) nr
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedermkExQs :: [GenVarDecl] -> Term -> Term
afe70330421b8b596e0c880d910cb9857053f3afChristian Maeder QuantifiedTerm HC.Existential vs t nr
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian MaedermkExQ :: VarDecl -> Term -> Term
afe70330421b8b596e0c880d910cb9857053f3afChristian MaedermkExQ vd = mkExQs [GenVarDecl vd]
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian MaedermkExConj :: VarDecl -> [Term] -> Term
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian MaedermkExConj vd = mkExQ vd . mkConj
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
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder Qual_pred_name pn pTy@(Pred_type srts q) _ = ps
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in if MapSet.member pn (toPredType pTy) $ flexPreds extInf
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder then mkApplTerm
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder (mkOp (trI pn) . trPrSyn
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ Pred_type (world : srts) q) $ currW : args
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else if null srts && Set.member pn (nominals extInf)
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder then eqW currW $ getTermOfNom as pn
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else mkApplTerm
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder (mkOp (trI pn) $ 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
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder (mkOp (trI opn) . trOpSyn
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ Op_type ok (world : srts) res q) $ currW : args
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else mkApplTerm
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder (mkOp (trI opn) $ 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
dbddf62bfe7f08b1fa0993c8ed944c047758d96cChristian Maeder a : r@(b : _) -> mkNot
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder (on eqW 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
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder conjF = mkConj $ map tM l ++ map tf l ++ disjointVars vds
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
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder EBox -> mkConj [f1, f2]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder else if i <= 0 && ex && gEq then unitTerm trueId r
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder else if bOp == EBox then mkConj $ map tr [Diamond, Box]
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
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder in mkExConj vi
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder [ eqW ti $ currentW as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , transMF as { boundNoms = (ni, ti) : boundNoms as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , currentW = ti
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder , freeC = fW + 1 } f ]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> transMF as f
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder UntilSince _isUntil f1 f2 _ -> mkConj [transMF as f1, transMF as f2]
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder ModForm _ -> unitTerm trueId nr
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
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder (mkOp (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
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder (mkOp (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 ""
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder Guard f -> mkConj [eqWorld exEq t1 t2, transMF as f]
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian 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
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder in mkExConj vd
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder [ transMod nAs { nextW = nW } m1
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder , transMod nAs { currentW = QualVar vd } m2 ]
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder Intersection -> mkConj [transMod as m1, transMod as m2]
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder Union -> mkDisj [transMod as m1, transMod as m2]
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder OrElse -> mkDisj $ transOrElse [] as $ flatOrElse md
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