TypeRel.hs revision bc994dca195712fe9143e074ed479077f9bab75d
ce8d7a0627c0f246376cccd980463f8250a6a97ebjhModule : $Header$
cb5d3f2f217d457dada4883addb1dc9f3f17bb85fieldingDescription : compute subtype dependencies
6ca0e6973c8176100f4a426444823ae5e777e28fsaschaCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
6ded37e63424e43b00ca7c9055d355e071d6a444rbbLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5a65270617de7ed4d14b193fdd6deb2d4890e1a6jortonMaintainer : Christian.Maeder@dfki.de
65d743d7fbb53143636ee2dec8fe8d8a1a581a6bjerenkrantzStability : experimental
6ca0e6973c8176100f4a426444823ae5e777e28fsaschaPortability : portable
6ca0e6973c8176100f4a426444823ae5e777e28fsaschacompute subtype dependencies
1fb1fa8713de956400293b715f191ae8675bfaf1fieldingimport qualified Common.Lib.Rel as Rel
6ca0e6973c8176100f4a426444823ae5e777e28fsaschaimport qualified Data.Map as Map
1ddf25b77b03f7f4fd7a7676b62755da90cd3e0crbbimport qualified Data.Set as Set
6ca0e6973c8176100f4a426444823ae5e777e28fsaschatypeRel :: TypeMap -> Rel.Rel Id
aa01f2bd8a4fc8a417b77d6fab108174f9ee1458jortontypeRel = Rel.transReduce . Rel.irreflex . Rel.transClosure
aa01f2bd8a4fc8a417b77d6fab108174f9ee1458jorton . Map.foldWithKey ( \ i ti r ->
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregamesgetRawKind :: TypeMap -> Id -> RawKind
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregamesgetRawKind tm i = typeKind $
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregames Map.findWithDefault (error $ showId i " not found in type map") i tm
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregames-- | make a polymorphic function from a to b
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregamesmkInjOrProjType :: Arrow -> TypeScheme
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregamesmkInjOrProjType arr =
e34761145134f5cfce7821fb60a06ec82b3b9650rjung TypeScheme [aTypeArg, bTypeArg] (mkFunArrType aType arr bType) nullRange
92c4ce31c526bc9e6272bc1157b496132c13d848rbbinjType :: TypeScheme
92c4ce31c526bc9e6272bc1157b496132c13d848rbbinjType = mkInjOrProjType FunArr
92c4ce31c526bc9e6272bc1157b496132c13d848rbbprojType :: TypeScheme
92c4ce31c526bc9e6272bc1157b496132c13d848rbbprojType = mkInjOrProjType PFunArr
92c4ce31c526bc9e6272bc1157b496132c13d848rbbmkInjOrProj :: Arrow -> Set.Set OpInfo
92c4ce31c526bc9e6272bc1157b496132c13d848rbbmkInjOrProj arr = Set.singleton OpInfo
92c4ce31c526bc9e6272bc1157b496132c13d848rbb { opType = mkInjOrProjType arr
92c4ce31c526bc9e6272bc1157b496132c13d848rbb , opAttrs = Set.empty
92c4ce31c526bc9e6272bc1157b496132c13d848rbb , opDefn = NoOpDefn Fun }
9ed3fee22fa1888a70ac42b7b6b8ea475fad0a6dfuankgsubtRelName :: Id
92c4ce31c526bc9e6272bc1157b496132c13d848rbbsubtRelName = mkId [genToken "subt"]
2b1f314755d8bf35d3e734339c8363c1cb57b3a3rjungsubtRelType :: TypeScheme
2b1f314755d8bf35d3e734339c8363c1cb57b3a3rjungsubtRelType = TypeScheme [aTypeArg, bTypeArg]
2b1f314755d8bf35d3e734339c8363c1cb57b3a3rjung (mkFunArrType (mkProductType [aType, bType]) PFunArr unitType) nullRange
2b1f314755d8bf35d3e734339c8363c1cb57b3a3rjungsubtRel :: Set.Set OpInfo
2b1f314755d8bf35d3e734339c8363c1cb57b3a3rjungsubtRel = Set.singleton OpInfo
2b1f314755d8bf35d3e734339c8363c1cb57b3a3rjung { opType = subtRelType
2b1f314755d8bf35d3e734339c8363c1cb57b3a3rjung , opDefn = NoOpDefn Fun }
92c4ce31c526bc9e6272bc1157b496132c13d848rbbsubtAxioms :: TypeMap -> [Named Sentence]
92c4ce31c526bc9e6272bc1157b496132c13d848rbbsubtAxioms tm =
dc12feb05fcd9f7afbe6c5d830898f028370cafbsf let tr = typeRel tm in
fb333f30ae01a1f14b2afaa8a92c99192abf883erjung if Rel.null tr then [] else subtReflex : subtTrans : subtInjProj : injTrans
0a2212da6843659e65c378c5201e6612be625731sf : map (subtAx tm) (Rel.toList tr)
0a2212da6843659e65c378c5201e6612be625731sfnr :: Range
fb333f30ae01a1f14b2afaa8a92c99192abf883erjungnr = nullRange
fb333f30ae01a1f14b2afaa8a92c99192abf883erjunggetKindAppl :: RawKind -> [Variance]
c9e0a2dddde6e561c529fa5ac3c384c136781570rjunggetKindAppl rk = case rk of
c9e0a2dddde6e561c529fa5ac3c384c136781570rjung ClassKind () -> []
c9e0a2dddde6e561c529fa5ac3c384c136781570rjung FunKind v _ r _ -> v : getKindAppl r
c9e0a2dddde6e561c529fa5ac3c384c136781570rjungmkTypeArg :: Id -> Int -> TypeArg
c9e0a2dddde6e561c529fa5ac3c384c136781570rjungmkTypeArg i c = TypeArg i NonVar (VarKind universe) rStar c Other nr
c9e0a2dddde6e561c529fa5ac3c384c136781570rjungsubtAx :: TypeMap -> (Id, Id) -> Named Sentence
c9e0a2dddde6e561c529fa5ac3c384c136781570rjungsubtAx tm (i1, i2) = let
c9e0a2dddde6e561c529fa5ac3c384c136781570rjung e1 = Map.findWithDefault (error "TypeRel.subtAx1") i1 tm
c9e0a2dddde6e561c529fa5ac3c384c136781570rjung e2 = Map.findWithDefault (error "TypeRel.subtAx2") i2 tm
c9e0a2dddde6e561c529fa5ac3c384c136781570rjung txt = shows i1 "_<_" ++ show i2
92c4ce31c526bc9e6272bc1157b496132c13d848rbb l1 = getKindAppl $ typeKind e1
92c4ce31c526bc9e6272bc1157b496132c13d848rbb l2 = getKindAppl $ typeKind e2
92c4ce31c526bc9e6272bc1157b496132c13d848rbb l3 = zipWith minVariance l1 l2
92c4ce31c526bc9e6272bc1157b496132c13d848rbb l4 = foldr (\ v (((tl, vl), pl), fl) ->
92c4ce31c526bc9e6272bc1157b496132c13d848rbb let c = length pl + 1
9ed3fee22fa1888a70ac42b7b6b8ea475fad0a6dfuankg a = simpleIdToId $ genNumVar "a" c
92c4ce31c526bc9e6272bc1157b496132c13d848rbb ta = mkTypeArg a (- (length tl + 1))
92c4ce31c526bc9e6272bc1157b496132c13d848rbb b = simpleIdToId $ genNumVar "b" c
945a9b081610f2b57759231e4cfad7aed62c9326slive tb = mkTypeArg b (- (length tl + 2))
945a9b081610f2b57759231e4cfad7aed62c9326slive x = stringToId $ 'x' : show c
8e5d996e323397bbcc56710e856475911930a93bjerenkrantz y = stringToId $ 'y' : show c
945a9b081610f2b57759231e4cfad7aed62c9326slive tx = typeArgToType ta
945a9b081610f2b57759231e4cfad7aed62c9326slive ty = typeArgToType tb
92c4ce31c526bc9e6272bc1157b496132c13d848rbb vx = mkVarDecl x tx
d15c3a0e8c77973008a6357eef9e87eae3c0137aslive vy = mkVarDecl y ty
945a9b081610f2b57759231e4cfad7aed62c9326slive in (case v of
92c4ce31c526bc9e6272bc1157b496132c13d848rbb NonVar -> ((ta : tl, vx : vl), (tx, tx) : pl)
8e5d996e323397bbcc56710e856475911930a93bjerenkrantz _ -> (([ta, tb] ++ tl, [vx, vy] ++ vl), (tx, ty) : pl)
92c4ce31c526bc9e6272bc1157b496132c13d848rbb , case v of
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregames CoVar -> mkSubtTerm tx ty vx vy : fl
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregames ContraVar -> mkSubtTerm ty tx vy vx : fl
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregames _ -> fl)) ((([], []), []), []) l3
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregames (args, fs) = l4
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregames (gens, acts) = args
49f79e02c1ca9aaf51f0c1fb06eeb1aa72cb1843gregames (act1, act2) = unzip acts
d472f67198d6b15dd1270136f180cca9c9263243trawick (tyargs, vargs) = gens
6ca0e6973c8176100f4a426444823ae5e777e28fsascha t1 = mkTypeAppl (toType i1) act1
51b88347f3bdf1a6b561aa7bbf18148459976e8ejorton t2 = mkTypeAppl (toType i2) act2
51b88347f3bdf1a6b561aa7bbf18148459976e8ejorton x1 = stringToId "x"
51b88347f3bdf1a6b561aa7bbf18148459976e8ejorton x2 = stringToId "y"
51b88347f3bdf1a6b561aa7bbf18148459976e8ejorton v1 = mkVarDecl x1 t1
51b88347f3bdf1a6b561aa7bbf18148459976e8ejorton v2 = mkVarDecl x2 t2
1acdb106aad7f32757afa07281b80e292229c3a8sf in makeNamed ("ga_subt_" ++ txt) $ Formula
1acdb106aad7f32757afa07281b80e292229c3a8sf $ mkForall (map GenTypeVarDecl tyargs
1acdb106aad7f32757afa07281b80e292229c3a8sf ++ map GenVarDecl (vargs ++ [v1, v2]))
1acdb106aad7f32757afa07281b80e292229c3a8sf $ (if null fs then id else
1acdb106aad7f32757afa07281b80e292229c3a8sf mkLogTerm implId nr (foldr1 (mkLogTerm andId nr) fs))
1acdb106aad7f32757afa07281b80e292229c3a8sf $ mkSubtTerm t1 t2 v1 v2
1acdb106aad7f32757afa07281b80e292229c3a8sfmkSubtTerm :: Type -> Type -> VarDecl -> VarDecl -> Term
51b88347f3bdf1a6b561aa7bbf18148459976e8ejortonmkSubtTerm t1 t2 v1 v2 = mkTerm subtRelName subtRelType [t1, t2] nr
51b88347f3bdf1a6b561aa7bbf18148459976e8ejorton $ TupleTerm [QualVar v1, QualVar v2] nr
ef0665105781ee79245fd5014fbc8569730c47a9rbbsubtReflex :: Named Sentence
de2aecd8da21eeae4394088cca196dfcb491de84rbbsubtReflex = let
f03dbdf787054ac7bb3ba5aa78c654e4c1b113d2pquerna v1 = mkVarDecl (stringToId "x") aType
f03dbdf787054ac7bb3ba5aa78c654e4c1b113d2pquerna v2 = mkVarDecl (stringToId "y") aType
294204c69c5ad7a76406907d780b01d80ea00d8cpquerna in makeNamed "ga_subt_reflexive" $ Formula
f03dbdf787054ac7bb3ba5aa78c654e4c1b113d2pquerna $ mkForall (GenTypeVarDecl aTypeArg : map GenVarDecl [v1, v2])
f03dbdf787054ac7bb3ba5aa78c654e4c1b113d2pquerna $ mkSubtTerm aType aType v1 v2
f03dbdf787054ac7bb3ba5aa78c654e4c1b113d2pquernasubtTrans :: Named Sentence
26d4668b602c703d63655271b1caaa420bf7a572rbbsubtTrans = let
bd7ee7eef7ad1988ff4d11aca3b0f9fc7beb4d97sf v1 = mkVarDecl (stringToId "x") aType
bd7ee7eef7ad1988ff4d11aca3b0f9fc7beb4d97sf v2 = mkVarDecl (stringToId "y") bType
bd7ee7eef7ad1988ff4d11aca3b0f9fc7beb4d97sf v3 = mkVarDecl (stringToId "z") cType
bd7ee7eef7ad1988ff4d11aca3b0f9fc7beb4d97sf in makeNamed "ga_subt_transitive" $ Formula
bd7ee7eef7ad1988ff4d11aca3b0f9fc7beb4d97sf $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg, cTypeArg]
bd7ee7eef7ad1988ff4d11aca3b0f9fc7beb4d97sf ++ map GenVarDecl [v1, v2, v3])
bd7ee7eef7ad1988ff4d11aca3b0f9fc7beb4d97sf $ mkLogTerm implId nr
bd7ee7eef7ad1988ff4d11aca3b0f9fc7beb4d97sf (mkLogTerm andId nr
f03dbdf787054ac7bb3ba5aa78c654e4c1b113d2pquerna (mkSubtTerm aType bType v1 v2)
ef0665105781ee79245fd5014fbc8569730c47a9rbb $ mkSubtTerm bType cType v2 v3)
759f4a24d09e28c4eaca9f97311b497fc15cb5c7ben $ mkSubtTerm aType cType v1 v3
92c4ce31c526bc9e6272bc1157b496132c13d848rbbmkInjEq :: Type -> Type -> VarDecl -> VarDecl -> Term
92c4ce31c526bc9e6272bc1157b496132c13d848rbbmkInjEq t1 t2 v1 v2 =
92c4ce31c526bc9e6272bc1157b496132c13d848rbb mkEqTerm eqId t2 nr (QualVar v2)
ebc7a477cfdf05bc87fce40c5886e02aa1c63e57trawick $ mkTerm injName injType [t1, t2] nr
92c4ce31c526bc9e6272bc1157b496132c13d848rbb $ QualVar v1
9db19053d8158d96abd6934678c012e0d59d59edjerenkrantzsubtInjProj :: Named Sentence
9db19053d8158d96abd6934678c012e0d59d59edjerenkrantzsubtInjProj = let
9db19053d8158d96abd6934678c012e0d59d59edjerenkrantz v1 = mkVarDecl (stringToId "x") aType
9db19053d8158d96abd6934678c012e0d59d59edjerenkrantz v2 = mkVarDecl (stringToId "y") bType
9db19053d8158d96abd6934678c012e0d59d59edjerenkrantz in makeNamed "ga_subt_inj_proj" $ Formula
92c4ce31c526bc9e6272bc1157b496132c13d848rbb $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg]
6ca0e6973c8176100f4a426444823ae5e777e28fsascha ++ map GenVarDecl [v1, v2])
b20fd88fb62a14780223a39488dba735d3643fdcwrowe $ mkLogTerm implId nr
92c4ce31c526bc9e6272bc1157b496132c13d848rbb (mkSubtTerm aType bType v1 v2)
92c4ce31c526bc9e6272bc1157b496132c13d848rbb $ mkLogTerm eqvId nr (mkInjEq aType bType v1 v2)
92c4ce31c526bc9e6272bc1157b496132c13d848rbb $ mkEqTerm eqId aType nr (QualVar v1)
ebc7a477cfdf05bc87fce40c5886e02aa1c63e57trawick $ mkTerm projName projType [bType, aType] nr
92c4ce31c526bc9e6272bc1157b496132c13d848rbb $ QualVar v2
ee0a58b4f00271d965403b2ed65b8aace6dee4c6pquernainjTrans :: Named Sentence
92c4ce31c526bc9e6272bc1157b496132c13d848rbbinjTrans = let
b20fd88fb62a14780223a39488dba735d3643fdcwrowe v1 = mkVarDecl (stringToId "x") aType
6ca0e6973c8176100f4a426444823ae5e777e28fsascha v2 = mkVarDecl (stringToId "y") bType
92c4ce31c526bc9e6272bc1157b496132c13d848rbb v3 = mkVarDecl (stringToId "z") cType
92c4ce31c526bc9e6272bc1157b496132c13d848rbb in makeNamed "ga_inj_transitive" $ Formula
92c4ce31c526bc9e6272bc1157b496132c13d848rbb $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg, cTypeArg]
ebc7a477cfdf05bc87fce40c5886e02aa1c63e57trawick ++ map GenVarDecl [v1, v2, v3])
92c4ce31c526bc9e6272bc1157b496132c13d848rbb $ mkLogTerm implId nr
ebc7a477cfdf05bc87fce40c5886e02aa1c63e57trawick (mkLogTerm andId nr (mkSubtTerm aType bType v1 v2)
ee0a58b4f00271d965403b2ed65b8aace6dee4c6pquerna $ mkLogTerm andId nr (mkSubtTerm bType cType v2 v3)
92c4ce31c526bc9e6272bc1157b496132c13d848rbb $ mkInjEq aType bType v1 v2)
6ca0e6973c8176100f4a426444823ae5e777e28fsascha $ mkLogTerm eqvId nr (mkInjEq aType cType v1 v3)
6ca0e6973c8176100f4a426444823ae5e777e28fsascha $ mkInjEq bType cType v2 v3
92c4ce31c526bc9e6272bc1157b496132c13d848rbbmonos :: Env -> [Named Sentence]
92c4ce31c526bc9e6272bc1157b496132c13d848rbbmonos e = concatMap (makeMonos e) . Map.toList $ assumps e
92c4ce31c526bc9e6272bc1157b496132c13d848rbbmakeMonos :: Env -> (Id, Set.Set OpInfo) -> [Named Sentence]
ebc7a477cfdf05bc87fce40c5886e02aa1c63e57trawickmakeMonos e (i, s) = makeEquivMonos e i . map opType $ Set.toList s
92c4ce31c526bc9e6272bc1157b496132c13d848rbbmakeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence]
2a67190265146d3e80b1b0c9ef04f181c8db7f64rbbmakeEquivMonos e i l = case l of
4b34d6a5b70303010612df6c87da3ee91ae86078rbb t : r -> mapMaybe (makeEquivMono e i t) r ++ makeEquivMonos e i r
6cb7893a671cebe32dd0455ba79781a4834e141egregamesmakeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)
6cb7893a671cebe32dd0455ba79781a4834e141egregamesmakeEquivMono e i s1 s2 = case getCommonSupertype e s1 s2 of
6cb7893a671cebe32dd0455ba79781a4834e141egregames Just (TypeScheme args nTy _) ->
4b34d6a5b70303010612df6c87da3ee91ae86078rbb Just $ makeNamed "ga_monotonicity"
6cb7893a671cebe32dd0455ba79781a4834e141egregames $ Formula $ mkForall (map GenTypeVarDecl args)
9b43e5d0e78f3f273d8d3f99398267f282ba293ftrawick $ mkEqTerm eqId nTy nr
cdb58be93a9cbeaba1ebc759b48aa8ed519675a9bjh (TypedTerm
cdb58be93a9cbeaba1ebc759b48aa8ed519675a9bjh (QualOp Op (PolyId i [] nr) s1 [] Infer nr)
4b34d6a5b70303010612df6c87da3ee91ae86078rbb OfType nTy nr)
cdb58be93a9cbeaba1ebc759b48aa8ed519675a9bjh $ TypedTerm
6ca0e6973c8176100f4a426444823ae5e777e28fsascha (QualOp Op (PolyId i [] nr) s2 [] Infer nr)
aa01f2bd8a4fc8a417b77d6fab108174f9ee1458jorton OfType nTy nr
aa01f2bd8a4fc8a417b77d6fab108174f9ee1458jorton Nothing -> Nothing