ExtModal2HasCASL.hs revision 97c21c29bf93e9fd1d0c4bdb6b9078034f013c3f
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
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian Maeder (mme, s) -> return (mme, 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
5bc55095489c7fb939535865b588b04957853446Christian MaederpredTy :: Type -> Type
5bc55095489c7fb939535865b588b04957853446Christian MaederpredTy = getFunType unitType HC.Partial . replicate 2
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaederisTransS :: String
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaederisTransS = "isTrans"
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaederisTransId :: Id
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaederisTransId = genName isTransS
5bc55095489c7fb939535865b588b04957853446Christian MaederisTransTy :: Type -> Type
5bc55095489c7fb939535865b588b04957853446Christian MaederisTransTy = predType nr . predTy
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaedercontainsS :: String
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaedercontainsS = "contains"
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian MaedercontainsId :: Id
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian MaedercontainsId = genName containsS
5bc55095489c7fb939535865b588b04957853446Christian MaedercontainsTy :: Type -> Type
5bc55095489c7fb939535865b588b04957853446Christian MaedercontainsTy = getFunType unitType HC.Partial . replicate 2 . predTy
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
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder $ OpInfo (simpleTypeScheme t) Set.empty $ NoOpDefn Fun
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder { assumps = foldr insF (assumps env)
ad06a3932c674dd1ebf566b8b5594d0df9e52cc0Christian Maeder [ (tauId, tauTy)
5bc55095489c7fb939535865b588b04957853446Christian Maeder , (isTransId, isTransTy nWorld)
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder , (containsId, containsTy nWorld)
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder , (transContainsId, containsTy nWorld)
5bc55095489c7fb939535865b588b04957853446Christian Maeder , typeMap = Map.insert nWorldId starTypeInfo $ typeMap env
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder , map (\ (s, t) -> makeNamed s $ Formula t)
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian Maeder [ (tauS, tauDef termMs $ Set.toList timeMs)
5bc55095489c7fb939535865b588b04957853446Christian Maeder , (isTransS, isTransDef nWorld)
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder , (containsS, containsDef nWorld)
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder , (transContainsS, transContainsDef nWorld)
5bc55095489c7fb939535865b588b04957853446Christian MaedervTrip :: Type -> [VarDecl]
5bc55095489c7fb939535865b588b04957853446Christian MaedervTrip w = map (\ n -> hcVarDecl (genNumVar "v" n) w) [1, 2, 3]
5bc55095489c7fb939535865b588b04957853446Christian MaedertripDs :: Type -> [GenVarDecl]
5bc55095489c7fb939535865b588b04957853446Christian MaedertripDs = map GenVarDecl . vTrip
5bc55095489c7fb939535865b588b04957853446Christian MaederpairDs :: Type -> [GenVarDecl]
5bc55095489c7fb939535865b588b04957853446Christian MaederpairDs = take 2 . tripDs
5bc55095489c7fb939535865b588b04957853446Christian MaedertTrip :: Type -> [Term]
5bc55095489c7fb939535865b588b04957853446Christian MaedertTrip = map QualVar . vTrip
5bc55095489c7fb939535865b588b04957853446Christian MaedertPair :: Type -> [Term]
5bc55095489c7fb939535865b588b04957853446Christian MaedertPair = take 2 . tTrip
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maedernr = nullRange
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian MaedertauDef :: Set.Set Id -> [Id] -> Term
5bc55095489c7fb939535865b588b04957853446Christian MaedertauDef termMs timeMs = let ts = tPair $ toType world in
5bc55095489c7fb939535865b588b04957853446Christian Maeder HC.mkForall (pairDs $ toType world)
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)
5bc55095489c7fb939535865b588b04957853446Christian MaederisTransDef :: Type -> Term
5bc55095489c7fb939535865b588b04957853446Christian MaederisTransDef w = let
5bc55095489c7fb939535865b588b04957853446Christian Maeder p = hcVarDecl (genToken "p") $ predTy w
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder pt = QualVar p
5bc55095489c7fb939535865b588b04957853446Christian Maeder [t1, t2, t3] = tTrip w
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder in HC.mkForall [GenVarDecl p]
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder . mkLogTerm eqvId nr
5bc55095489c7fb939535865b588b04957853446Christian Maeder (mkApplTerm (mkOp isTransId $ isTransTy 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]
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian MaederpAndQ :: Type -> [VarDecl]
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian MaederpAndQ w = map (\ c -> hcVarDecl (genToken [c]) $ predTy 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
5bc55095489c7fb939535865b588b04957853446Christian Maeder (mkApplTerm (mkOp containsId $ containsTy w) [pt, qt])
6a9f9db7e1bcd05068b156642fe4771f4e10bae7Christian Maeder . mkLogTerm implId nr
5bc55095489c7fb939535865b588b04957853446Christian Maeder (mkApplTerm pt ts)
5bc55095489c7fb939535865b588b04957853446Christian Maeder $ mkApplTerm qt ts
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian MaedertransContainsS :: String
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian MaedertransContainsS = "trans_contains"
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian MaedertransContainsId :: Id
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian MaedertransContainsId = genName transContainsS
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder-- transContainsTy = containsTy
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian MaedertransContainsDef :: Type -> Term
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian MaedertransContainsDef w = let -- q is transitive and contains p
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder ts@[_, qt] = map QualVar ps
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder in HC.mkForall (map GenVarDecl ps)
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder . mkLogTerm eqvId nr
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder (mkApplTerm (mkOp transContainsId $ containsTy w) ts)
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder . mkLogTerm andId nr
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder (mkApplTerm (mkOp isTransId $ isTransTy w) [qt])
97c21c29bf93e9fd1d0c4bdb6b9078034f013c3fChristian Maeder $ mkApplTerm (mkOp containsId $ containsTy w) ts
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
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertoSen :: ExtModalSign -> Env -> FORMULA EM_FORMULA -> Sentence
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertoSen msig env f = case f of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Sort_gen_ax cs b -> let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (sorts, ops, smap) = recover_Sort_gen_ax cs
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder genKind = if b then Free else Generated
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder mapPart :: OpKind -> Partiality
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder mapPart cp = case cp of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in DatatypeSen $ map ( \ s ->
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder DataEntry (Map.fromList smap) s genKind [] rStar
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ Set.fromList $ map ( \ (i, t) ->
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder let args = map toType $ opArgs t in
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Construct (if isInjName i then Nothing else Just i) args
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder (mapPart $ opKind t)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ map (\ a -> [Select Nothing a HC.Total]) args)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ filter ( \ (_, t) -> opRes t == s)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder $ map ( \ o -> case o of
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder Qual_op_name i t _ -> (trI i, toOpType t)
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> error "ExtModal2HasCASL.toSentence") ops) sorts
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder _ -> Formula $ transTop msig env f
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransTop :: ExtModalSign -> Env -> FORMULA EM_FORMULA -> Term
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian MaedertransTop msig env f = let
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder vt = varTerm (genNumVar "w" 1) world
8a94f9add1f11ef1b57be38c71b69f286b004acaChristian Maeder in mkEnvForall env
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
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
8181992e8fc9f2390d0542a5ba603cb807a8b05fChristian MaedermkExQ :: VarDecl -> Term -> Term
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder QuantifiedTerm HC.Existential [GenVarDecl vd] t nr
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
8166329c8bd64e1534c0a73c81d77fc50bd2dd75Christian Maeder a : r@(b : _) -> mkTerm notId notType [] nr
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