ExtModal2HasCASL.hs revision a284d9c8a1a6b2134a7ae900f247eda10e1687c0
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
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder sourceSublogic ExtModal2HasCASL = maxSublogic { hasTransClos = False }
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)]
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder ++ s ++ map (mapNamed $ toSen sig) 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
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkOp :: Id -> Type -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkOp i = mkOpTerm i . simpleTypeScheme
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkNomAppl :: Id -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkNomAppl pn = mkOp (nomName pn) $ trOp nomOpType
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedereqWorld :: Id -> Term -> Term -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedereqWorld i = mkEqTerm i (toType world) nr
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedereqW :: Term -> Term -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedereqW = eqWorld eqId
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkNot :: Term -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkNot = mkTerm notId notType [] nr
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkConj :: [Term] -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkConj l = toBinJunctor andId l nr
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkDisj :: [Term] -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian Maeder (if null l then unitTerm falseId else toBinJunctor orId l) nr
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkExQs :: [GenVarDecl] -> Term -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian Maeder QuantifiedTerm HC.Existential vs t nr
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkExQ :: VarDecl -> Term -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkExQ vd = mkExQs [GenVarDecl vd]
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkExConj :: VarDecl -> [Term] -> Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian MaedermkExConj vd = mkExQ vd . mkConj
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)
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder , (pathId, 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)
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder , (pathS, pathDef)
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
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian 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)
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaederrAndQ :: Type -> [VarDecl]
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaederrAndQ w = map (\ c -> hcVarDecl (genToken [c]) $ binPredTy w) "RQ"
5bc55095489c7fb939535865b588b04957853446Christian MaedercontainsDef :: Type -> Term
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaedercontainsDef w = let -- q contains r
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder ts@[pt, qt] = map QualVar ps
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian Maeder in HC.mkForall (map GenVarDecl ps)
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian Maeder . mkLogTerm eqvId nr
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder (mkApplTerm (mkOp containsId $ transTy w) ts)
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder $ containsDefAux False implId pt qt w
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaedercontainsDefAux :: Bool -> Id -> Term -> Term -> Type -> Term
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaedercontainsDefAux neg op pt qt w = let ts = tPair w in
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder HC.mkForall (pairDs w) . (if neg then mkNot else id)
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder . mkLogTerm op nr (mkApplTerm pt ts) $ mkApplTerm qt ts
08fa7405566a83131a773e82e9514d67e30233c9Christian MaedersomeContainsDef :: (Term -> Term) -> Type -> Term -> Term -> Term
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaedersomeContainsDef sPred w pt qt = let -- q fulfills sPred and contains r
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
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaedersomeDef dId op w = let -- q is the (smallest) something containing r
94e228feb6eb06e1b1564146d00d54734b8e3307Christian Maeder ts@[pt, qt] = map QualVar ps
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 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]
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian MaederzeroT = mkOp zero natTy
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederhasSuccessorDef :: Term
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian MaederhasSuccessorDef = let
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]
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian MaederpairWorld :: Term -> Term -> Term
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian MaederpairWorld t1 t2 = mkApplTerm (mkOp nWorldId nWorldTy) [t1, t2]
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian MaedersucTy = altToTy natId sucAlt
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian MaedersucTerm :: Term -> Term
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian MaedersucTerm t = mkApplTerm (mkOp sucId sucTy) [t]
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
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder pw = pairWorld xt0 nT
9ad3eca7ffa4b65d03bf9443f5b85b274a038d1aChristian Maeder in (mkExQ x tauAppl, pw,
aab870997808945ad279711662d457a225c53011Christian Maeder . mkLogTerm andId nr tauAppl
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder $ mkApplTerm pt [pw, pairWorld xt $ sucTerm 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]
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaederpathS :: String
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaederpathS = "path"
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaederpathId = genName pathS
28bbcefa89149db601a9910612f743e95388da2bChristian MaederpathAppl :: [Term] -> Term
28bbcefa89149db601a9910612f743e95388da2bChristian MaederpathAppl = mkApplTerm $ mkOp pathId hasSuccessorTy
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian MaederpathDef :: Term
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder vs = xZeroAndP
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder [rv, qv] = rAndQ nWorld
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder [rt, qt] = map QualVar [rv, qv]
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder ts@[x0, pt] = map QualVar vs
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder in HC.mkForall (map GenVarDecl vs)
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder . mkLogTerm eqvId nr
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder (pathAppl ts)
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder [ mkApplTerm (mkOp superpathId hasSuccessorTy) [x0, rt]
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder , mkApplTerm (mkOp transReflexId $ transTy nWorld) [rt, pt]
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder , HC.mkForall [GenVarDecl qv]
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder . mkLogTerm implId nr
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder (mkApplTerm (mkOp superpathId hasSuccessorTy) [x0, qt])
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder . mkLogTerm orId nr
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder (containsDefAux True implId qt rt nWorld)
2a074c93e61ad37e0747e134fbba9471a14c18c1Christian Maeder $ containsDefAux False eqvId qt rt nWorld
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian MaedertoSen :: ExtModalSign -> FORMULA EM_FORMULA -> Sentence
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian MaedertoSen msig 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
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder ExtFORMULA (ModForm _) -> Formula $ unitTerm trueId nr
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder _ -> Formula $ transTop msig f
d7e22970811b439073fdecd4f35803f4e415bc78Christian Maederdata Args = Args
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder { sourceW, targetW, targetN :: Term
d7e22970811b439073fdecd4f35803f4e415bc78Christian Maeder , nextW, freeC :: Int -- world variables
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder , freeZ :: Int -- path variable
d7e22970811b439073fdecd4f35803f4e415bc78Christian Maeder , boundNoms :: [(Id, Term)]
d7e22970811b439073fdecd4f35803f4e415bc78Christian Maeder , modSig :: ExtModalSign
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian MaederstartArgs :: ExtModalSign -> Args
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian MaederstartArgs msig = let
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder vt = varTerm (genNumVar "w" 1) world
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder { sourceW = vt
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder , targetW = vt
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder , targetN = zeroT
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder , boundNoms = []
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder , modSig = msig
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian MaederzDecl :: Args -> VarDecl
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian MaederzDecl as = hcVarDecl (genNumVar "Z" $ freeZ as) $ binPredTy nWorld
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian MaedertransTop :: ExtModalSign -> FORMULA EM_FORMULA -> Term
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian MaedertransTop msig f = let
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder as = startArgs msig
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder vs = [hcVarDecl (genNumVar "w" 1) worldTy, zDecl as]
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder in HC.mkForall (map GenVarDecl vs)
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder . mkLogTerm implId nr
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder (pathAppl $ map QualVar vs)
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder $ transMF as f
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedergetTermOfNom :: Args -> Id -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedergetTermOfNom as i = fromMaybe (mkNomAppl i) . lookup i $ boundNoms as
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian MaedermkZPath :: Term -> Term -> Args -> Term
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian MaedermkZPath v n as = mkApplTerm (QualVar $ zDecl as)
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder [pairWorld v n, pairWorld (targetW as) $ targetN as]
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian MaederzPath :: Args -> Term
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian MaederzPath as = mkZPath (sourceW as) zeroT as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertrRecord :: Args -> String -> Record EM_FORMULA Term Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertrRecord as str = let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder extInf = extendedInfo $ modSig as
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder currW = targetW as
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder andPath = mkLogTerm andId nr $ zPath as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in (transRecord str)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder { foldPredication = \ _ ps args _ -> let
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder Qual_pred_name pn pTy@(Pred_type srts q) _ = ps
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder $ 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
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder , foldEquation = \ o t1 e t2 ps ->
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder let Equation c1 _ _ _ = o in
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder andPath $ mkEqTerm (if e == Existl then exEq else eqId)
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder (typeOfTerm c1) ps t1 t2
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder , foldDefinedness = \ o t ps ->
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder let Definedness c _ = o in
525d42e964a41b6c2cbaec4e6b211e9c6d6b64a2Christian Maeder andPath $ mkTerm defId defType [typeOfTerm c] ps t
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
28bbcefa89149db601a9910612f743e95388da2bChristian MaederpathAppl2 :: Term -> VarDecl -> Term
28bbcefa89149db601a9910612f743e95388da2bChristian MaederpathAppl2 t v = pathAppl [t, QualVar v]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransEMF :: Args -> EM_FORMULA -> Term
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian MaedertransEMF as emf = let
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder fW = freeC as
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder pathAppl3 t = mkLogTerm implId nr . pathAppl2 t
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder is i = [fW + 1 .. fW + i]
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder vds = map (\ n -> varDecl (genNumVar "w" n) world) . is
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder gvs = map GenVarDecl . vds
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder in case emf of
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder PrefixForm pf f r -> case pf of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder BoxOrDiamond bOp m gEq i -> let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder ex = bOp == Diamond
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder nAs = as { freeC = fW + i }
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder vt = varTerm (genNumVar "w" n) world
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder newAs = nAs { freeZ = n }
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder zd = zDecl newAs
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder in HC.mkForall [GenVarDecl zd]
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder . pathAppl3 vt zd
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder $ transMF (resetArgs vt newAs) f
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder tM n = transMod nAs { nextW = n } m
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder conjF = mkConj $ map tM l ++ map tf l ++ disjointVars (vds i)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder diam = BoxOrDiamond Diamond m True
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder tr b = transEMF as $ PrefixForm (BoxOrDiamond b m gEq i) f r
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder f1 = QuantifiedTerm HC.Existential gs 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
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder if at then let
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder ti = getTermOfNom as ni
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder nAs = as { freeC = fW + 1, freeZ = fW + 1 }
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder zd = zDecl nAs
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder [ zPath as, HC.mkForall [GenVarDecl zd]
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder . pathAppl3 ti zd $ transMF (resetArgs ti as) f ]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder vi = varDecl (genNumVar "i" $ fW + 1) world
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder ti = QualVar vi
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder in mkExConj vi
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder [ eqW ti $ targetW as
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder , transMF as { boundNoms = (ni, ti) : boundNoms as
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder , targetW = ti
fb690a2fb0173d53f695a5d43f83abf5c955250cChristian Maeder , freeC = fW + 1 } f ]
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> transMF as f
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder UntilSince isUntil f1 f2 r -> let
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder nAs = as { freeC = fW + 2 }
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder vt0 = targetW as
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder nt0 = targetN as
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder [v1, v2] = vds 2
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder [n1, n2] = map (\ n -> varDecl (genNumVar "n" n) natId) l
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder [vt1, vt2, nt1, nt2] = map QualVar [v1, v2, n1, n2]
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder as1 = nAs { targetW = vt1, targetN = nt1 }
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder as2 = nAs { targetW = vt2, targetN = nt2 }
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder in mkLogTerm andId r (zPath as)
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder . mkExQs (map GenVarDecl [v1, n1])
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder [ if isUntil then mkZPath vt0 nt0 as1 else mkZPath vt1 nt1 as
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder , transMF as1 f2
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder , HC.mkForall (map GenVarDecl [v2, n2])
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder . mkLogTerm orId r
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder [ mkLogTerm orId r
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder (if isUntil then mkZPath vt0 nt0 as2 else mkZPath vt2 nt2 as)
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder . mkLogTerm andId r (eqW vt0 vt2)
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder $ mkEqTerm eqId natTy r nt0 nt2
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder , if isUntil then mkZPath vt2 nt2 as1 else mkZPath vt1 nt1 as2 ])
a284d9c8a1a6b2134a7ae900f247eda10e1687c0Christian Maeder $ transMF as2 f1 ]
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder ModForm _ -> unitTerm trueId nr
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian MaederresetArgs :: Term -> Args -> Args
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian MaederresetArgs t as = as
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder { sourceW = t
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder , targetW = t
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder , targetN = zeroT }
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransMod :: Args -> MODALITY -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransMod as md = let
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder t1 = targetW 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)
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder $ foldTerm (trRecord (resetArgs t1 as) $ showDoc t "") t : vts
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> error $ "transMod2: " ++ showDoc t ""
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder Guard f -> let
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder nf = freeC as + 1
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder newAs = as { freeC = nf, freeZ = nf }
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder zd = zDecl newAs
5565b8dc5860317884e01b59e11b7a171b3eabe5Christian Maeder in mkConj [eqWorld exEq t1 t2, HC.mkForall [GenVarDecl zd] $ mkConj
28bbcefa89149db601a9910612f743e95388da2bChristian Maeder [ pathAppl2 t1 zd, transMF (resetArgs t1 newAs) 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
e41d5ebab1cc75c958b7c2e5521d4d83a4136bf9Christian Maeder , transMod nAs { targetW = 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