Mercurial > urweb
changeset 1181:618f9f458da9
Got split1 working, but noticed a nasty type inference bug with transplanted unification variables
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 06 Mar 2010 19:14:48 -0500 |
| parents | ac3dbbc85c6e |
| children | 0b1d666bddb4 |
| files | lib/ur/incl.ur lib/ur/incl.urs src/compiler.sig src/compiler.sml src/especialize.sml src/reduce.sml |
| diffstat | 6 files changed, 61 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/incl.ur Sat Mar 06 16:15:26 2010 -0500 +++ b/lib/ur/incl.ur Sat Mar 06 19:14:48 2010 -0500 @@ -21,7 +21,7 @@ i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !)) -fun inv2 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] +fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] (i : incl ([nm = t] ++ r) r') = i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) => @@ -35,6 +35,6 @@ (i : tf []) (fl : folder r) = @Top.fold [fn r' => incl r' r -> tf r'] (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i => - f [nm] [v] [r'] ! i (acc (inv2 [nm] [r'] [r] i))) + f [nm] [v] [r'] ! i (acc (inv2 [nm] [v] [r'] [r] i))) (fn _ => i) fl (incl [r] [[]])
--- a/lib/ur/incl.urs Sat Mar 06 16:15:26 2010 -0500 +++ b/lib/ur/incl.urs Sat Mar 06 19:14:48 2010 -0500 @@ -9,7 +9,7 @@ -> incl ([nm = t] ++ r) r' -> (nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) -> f nm t r' -val inv2 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K} +val inv2 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K} -> [[nm] ~ r] => incl ([nm = t] ++ r) r' -> incl r r'
--- a/src/compiler.sig Sat Mar 06 16:15:26 2010 -0500 +++ b/src/compiler.sig Sat Mar 06 19:14:48 2010 -0500 @@ -120,12 +120,13 @@ val toRpcify : (string, Core.file) transform val toCore_untangle2 : (string, Core.file) transform val toShake2 : (string, Core.file) transform + val toUnpoly1 : (string, Core.file) transform val toEspecialize1 : (string, Core.file) transform val toCore_untangle3 : (string, Core.file) transform val toShake3 : (string, Core.file) transform val toTag : (string, Core.file) transform val toReduce : (string, Core.file) transform - val toUnpoly : (string, Core.file) transform + val toUnpoly2 : (string, Core.file) transform val toSpecialize : (string, Core.file) transform val toShake4 : (string, Core.file) transform val toEspecialize2 : (string, Core.file) transform
--- a/src/compiler.sml Sat Mar 06 16:15:26 2010 -0500 +++ b/src/compiler.sml Sat Mar 06 19:14:48 2010 -0500 @@ -955,7 +955,16 @@ val toCore_untangle2 = transform core_untangle "core_untangle2" o toRpcify val toShake2 = transform shake "shake2" o toCore_untangle2 -val toEspecialize1 = transform especialize "especialize1" o toShake2 + +val unpoly = { + func = Unpoly.unpoly, + print = CorePrint.p_file CoreEnv.empty +} + +val toUnpoly1 = transform unpoly "unpoly1" o toShake2 + +val toEspecialize1 = transform especialize "especialize1" o toUnpoly1 + val toCore_untangle3 = transform core_untangle "core_untangle3" o toEspecialize1 val toShake3 = transform shake "shake3" o toCore_untangle3 @@ -973,19 +982,14 @@ val toReduce = transform reduce "reduce" o toTag -val unpoly = { - func = Unpoly.unpoly, - print = CorePrint.p_file CoreEnv.empty -} - -val toUnpoly = transform unpoly "unpoly" o toReduce +val toUnpoly2 = transform unpoly "unpoly2" o toReduce val specialize = { func = Specialize.specialize, print = CorePrint.p_file CoreEnv.empty } -val toSpecialize = transform specialize "specialize" o toUnpoly +val toSpecialize = transform specialize "specialize" o toUnpoly2 val toShake4 = transform shake "shake4" o toSpecialize
--- a/src/especialize.sml Sat Mar 06 16:15:26 2010 -0500 +++ b/src/especialize.sml Sat Mar 06 19:14:48 2010 -0500 @@ -43,6 +43,13 @@ structure IM = IntBinaryMap structure IS = IntBinarySet +val isOpen = U.Exp.exists {kind = fn _ => false, + con = fn c => + case c of + CRel _ => true + | _ => false, + exp = fn _ => false} + val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs, con = fn (_, _, xs) => xs, exp = fn (bound, e, xs) => @@ -221,7 +228,12 @@ in ((ECApp (e, c), loc), st) end - | ECAbs _ => (e, st) + | ECAbs (x, k, e) => + let + val (e, st) = exp (env, e, st) + in + ((ECAbs (x, k, e), loc), st) + end | EKAbs _ => (e, st) | EKApp (e, k) => let @@ -349,6 +361,7 @@ if not fin orelse List.all (fn (ERel _, _) => true | _ => false) fxs' + orelse List.exists isOpen fxs' orelse (IS.numItems fvs >= length fxs andalso IS.exists (fn n => functionInside (#2 (List.nth (env, n)))) fvs) then ((*Print.prefaces "No" [("name", Print.PD.string name),
--- a/src/reduce.sml Sat Mar 06 16:15:26 2010 -0500 +++ b/src/reduce.sml Sat Mar 06 19:14:48 2010 -0500 @@ -423,7 +423,15 @@ in case #1 e1 of EAbs (_, _, _, b) => - exp (KnownE e2 :: env') b + let + val r = exp (KnownE e2 :: env') b + in + (*Print.prefaces "eapp" [("b", CorePrint.p_exp CoreEnv.empty b), + ("env", Print.PD.string (e2s env')), + ("e2", CorePrint.p_exp CoreEnv.empty e2), + ("r", CorePrint.p_exp CoreEnv.empty r)];*) + r + end | _ => (EApp (e1, e2), loc) end @@ -435,7 +443,17 @@ val c = con env c in case #1 e of - ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b + ECAbs (_, _, b) => + let + val r = exp (KnownC c :: deKnown env) b + in + (*Print.prefaces "csub" [("l", Print.PD.string (ErrorMsg.spanToString loc)), + ("env", Print.PD.string (e2s (deKnown env))), + ("b", CorePrint.p_exp CoreEnv.empty b), + ("c", CorePrint.p_con CoreEnv.empty c), + ("r", CorePrint.p_exp CoreEnv.empty r)];*) + r + end | _ => (ECApp (e, c), loc) end @@ -446,7 +464,16 @@ val e = exp env e in case #1 e of - EKAbs (_, b) => exp (KnownK k :: deKnown env) b + EKAbs (_, b) => + let + val r = exp (KnownK k :: deKnown env) b + in + (*Print.prefaces "ksub" [("l", Print.PD.string (ErrorMsg.spanToString loc)), + ("b", CorePrint.p_exp CoreEnv.empty b), + ("k", CorePrint.p_kind CoreEnv.empty k), + ("r", CorePrint.p_exp CoreEnv.empty r)];*) + r + end | _ => (EKApp (e, kind env k), loc) end