TypeRel.hs revision 9e5c10805bd50b5baaf6bf1f6a3f085c7afb17d8
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : compute subtype dependencies
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : experimental
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskicompute subtype dependencies
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport qualified Common.Lib.Rel as Rel
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport qualified Data.Map as Map
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maederimport qualified Data.Set as Set
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedertypeRel :: TypeMap -> Rel.Rel Id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitypeRel = Rel.transReduce . Rel.irreflex . Rel.transClosure
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Set.fold (Rel.insert i) r $ superTypes ti) Rel.empty
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian MaedergetRawKind :: TypeMap -> Id -> RawKind
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian MaedergetRawKind tm i = typeKind $
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Map.findWithDefault (error $ showId i " not found in type map") i tm
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich-- | make a polymorphic function from a to b
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichmkInjOrProjType :: Arrow -> TypeScheme
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermkInjOrProjType arr =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder TypeScheme [aTypeArg, bTypeArg] (mkFunArrType aType arr bType) nullRange
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederinjType :: TypeScheme
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederinjType = mkInjOrProjType FunArr
c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuprojType :: TypeScheme
986d3f255182539098a97ac86da9eeee5b7a72e3Christian MaederprojType = mkInjOrProjType PFunArr
986d3f255182539098a97ac86da9eeee5b7a72e3Christian MaedermkInjOrProj :: Arrow -> Set.Set OpInfo
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermkInjOrProj arr = Set.singleton OpInfo
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder { opType = mkInjOrProjType arr
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder , opDefn = NoOpDefn Fun }
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedersubtRelName :: Id
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian MaedersubtRelName = mkId [genToken "subt"]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedersubtRelType :: TypeScheme
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedersubtRelType = TypeScheme [aTypeArg, bTypeArg]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (mkFunArrType (mkProductType [aType, bType]) PFunArr unitType) nullRange
d79e02625778d20a5458078f979ff74aac67db61Christian MaedersubtRel :: Set.Set OpInfo
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder { opType = subtRelType
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder , opDefn = NoOpDefn Fun }
d79e02625778d20a5458078f979ff74aac67db61Christian MaedersubtAxioms :: TypeMap -> [Named Sentence]
d79e02625778d20a5458078f979ff74aac67db61Christian MaedersubtAxioms tm =
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder let tr = typeRel tm in
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder if Rel.null tr then [] else subtReflex : subtTrans : subtInjProj : injTrans
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder : map (subtAx tm) (Rel.toList tr)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maedernr = nullRange
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedergetKindAppl :: RawKind -> [Variance]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedergetKindAppl rk = case rk of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ClassKind () -> []
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder FunKind v _ r _ -> v : getKindAppl r
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermkTypeArg :: Id -> Int -> TypeArg
5e46b572ed576c0494768998b043d9d340594122Till MossakowskimkTypeArg i c = TypeArg i NonVar (VarKind universe) rStar c Other nr
5e46b572ed576c0494768998b043d9d340594122Till MossakowskisubtAx :: TypeMap -> (Id, Id) -> Named Sentence
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedersubtAx tm (i1, i2) = let
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Map.findWithDefault (error "TypeRel.subtAx") i bTypes) i tm
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder e1 = findType i1
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder e2 = findType i2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder txt = shows i1 "_<_" ++ show i2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder l1 = getKindAppl $ typeKind e1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder l2 = getKindAppl $ typeKind e2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder l3 = zipWith minVariance l1 l2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder l4 = foldr (\ v (((tl, vl), pl), fl) ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let c = length pl + 1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder a = simpleIdToId $ genNumVar "a" c
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ta = mkTypeArg a (- (length tl + 1))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski b = simpleIdToId $ genNumVar "b" c
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski tb = mkTypeArg b (- (length tl + 2))
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder x = stringToId $ 'x' : show c
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder y = stringToId $ 'y' : show c
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder tx = typeArgToType ta
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ty = typeArgToType tb
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder vx = mkVarDecl x tx
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder vy = mkVarDecl y ty
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder in (case v of
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder NonVar -> ((ta : tl, vx : vl), (tx, tx) : pl)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> (([ta, tb] ++ tl, [vx, vy] ++ vl), (tx, ty) : pl)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder CoVar -> mkSubtTerm tx ty vx vy : fl
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ContraVar -> mkSubtTerm ty tx vy vx : fl
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder _ -> fl)) ((([], []), []), []) l3
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (args, fs) = l4
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (gens, acts) = args
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (act1, act2) = unzip acts
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (tyargs, vargs) = gens
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder t1 = mkTypeAppl (toType i1) act1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder t2 = mkTypeAppl (toType i2) act2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder x1 = stringToId "x"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder x2 = stringToId "y"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder v1 = mkVarDecl x1 t1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder v2 = mkVarDecl x2 t2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in makeNamed ("ga_subt_" ++ txt) $ Formula
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $ mkForall (map GenTypeVarDecl tyargs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ++ map GenVarDecl (vargs ++ [v1, v2]))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $ (if null fs then id else
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder mkLogTerm implId nr (foldr1 (mkLogTerm andId nr) fs))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $ mkSubtTerm t1 t2 v1 v2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermkSubtTerm :: Type -> Type -> VarDecl -> VarDecl -> Term
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermkSubtTerm t1 t2 v1 v2 = mkTerm subtRelName subtRelType [t1, t2] nr
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ TupleTerm [QualVar v1, QualVar v2] nr
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedersubtReflex :: Named Sentence
5e46b572ed576c0494768998b043d9d340594122Till MossakowskisubtReflex = let
74d9a385499bf903b24848dff450a153f525bda7Christian Maeder v1 = mkVarDecl (stringToId "x") aType
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder v2 = mkVarDecl (stringToId "y") aType
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in makeNamed "ga_subt_reflexive" $ Formula
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ mkForall (GenTypeVarDecl aTypeArg : map GenVarDecl [v1, v2])
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ mkSubtTerm aType aType v1 v2
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedersubtTrans :: Named Sentence
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedersubtTrans = let
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder v1 = mkVarDecl (stringToId "x") aType
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder v2 = mkVarDecl (stringToId "y") bType
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder v3 = mkVarDecl (stringToId "z") cType
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in makeNamed "ga_subt_transitive" $ Formula
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg, cTypeArg]
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder ++ map GenVarDecl [v1, v2, v3])
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkLogTerm implId nr
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder (mkLogTerm andId nr
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder (mkSubtTerm aType bType v1 v2)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkSubtTerm bType cType v2 v3)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkSubtTerm aType cType v1 v3
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedermkInjTerm :: Type -> Type -> Term -> Term
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedermkInjTerm t1 t2 = mkTerm injName injType [t1, t2] nr
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedermkInjEq :: Type -> Type -> VarDecl -> VarDecl -> Term
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedermkInjEq t1 t2 v1 v2 =
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder mkEqTerm eqId t2 nr (QualVar v2)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkInjTerm t1 t2 $ QualVar v1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisubtInjProj :: Named Sentence
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedersubtInjProj = let
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder v1 = mkVarDecl (stringToId "x") aType
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder v2 = mkVarDecl (stringToId "y") bType
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in makeNamed "ga_subt_inj_proj" $ Formula
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg]
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder ++ map GenVarDecl [v1, v2])
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkLogTerm implId nr
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder (mkSubtTerm aType bType v1 v2)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkLogTerm eqvId nr (mkInjEq aType bType v1 v2)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkEqTerm eqId aType nr (QualVar v1)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ mkTerm projName projType [bType, aType] nr
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederinjTrans :: Named Sentence
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederinjTrans = let
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder v1 = mkVarDecl (stringToId "x") aType
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder v2 = mkVarDecl (stringToId "y") bType
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder v3 = mkVarDecl (stringToId "z") cType
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder in makeNamed "ga_inj_transitive" $ Formula
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg, cTypeArg]
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder ++ map GenVarDecl [v1, v2, v3])
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkLogTerm implId nr
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder (mkLogTerm andId nr (mkSubtTerm aType bType v1 v2)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkLogTerm andId nr (mkSubtTerm bType cType v2 v3)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder $ mkInjEq aType bType v1 v2)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $ mkLogTerm eqvId nr (mkInjEq aType cType v1 v3)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ mkInjEq bType cType v2 v3
03136b84a0c70d877e227444f0875e209506b9e4Christian Maedermonos :: Env -> [Named Sentence]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maedermonos e = concatMap (makeMonos e) . Map.toList $ assumps e
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedermakeMonos :: Env -> (Id, Set.Set OpInfo) -> [Named Sentence]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedermakeMonos e (i, s) = makeEquivMonos e i . map opType $ Set.toList s
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermakeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermakeEquivMonos e i l = case l of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder t : r -> mapMaybe (makeEquivMono e i t) r ++ makeEquivMonos e i r
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimakeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermakeEquivMono e i s1 s2 = case getCommonSupertype e s1 s2 of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just (ty1, l1, ty2, l2, args, nTy) ->
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Just $ makeNamed "ga_monotonicity"
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder $ Formula $ mkForall (map GenTypeVarDecl args)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ mkEqTerm eqId nTy nr
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (mkInjTerm ty1 nTy
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ QualOp Op (PolyId i [] nr) s1 l1 UserGiven nr)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $ mkInjTerm ty2 nTy
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $ QualOp Op (PolyId i [] nr) s2 l2 UserGiven nr
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> Nothing