From df76c398867ef66c583e5d481bdb33e046acfc09 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 6 Mar 2010 19:14:48 -0500 Subject: Got split1 working, but noticed a nasty type inference bug with transplanted unification variables --- lib/ur/incl.ur | 4 ++-- lib/ur/incl.urs | 2 +- src/compiler.sig | 3 ++- src/compiler.sml | 20 ++++++++++++-------- src/especialize.sml | 15 ++++++++++++++- src/reduce.sml | 33 ++++++++++++++++++++++++++++++--- 6 files changed, 61 insertions(+), 16 deletions(-) diff --git a/lib/ur/incl.ur b/lib/ur/incl.ur index d0f4b521..ebf7acef 100644 --- a/lib/ur/incl.ur +++ b/lib/ur/incl.ur @@ -21,7 +21,7 @@ fun inv1 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] 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 @@ fun fold [K] [tf :: {K} -> Type] [r ::: {K}] (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] [[]]) diff --git a/lib/ur/incl.urs b/lib/ur/incl.urs index d0d78b36..2c77369f 100644 --- a/lib/ur/incl.urs +++ b/lib/ur/incl.urs @@ -9,7 +9,7 @@ val inv1 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K} -> 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' diff --git a/src/compiler.sig b/src/compiler.sig index 63da4e5c..6be2b22f 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -120,12 +120,13 @@ signature COMPILER = sig 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 diff --git a/src/compiler.sml b/src/compiler.sml index 63b28fb7..237cad08 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -955,7 +955,16 @@ val toRpcify = transform rpcify "rpcify" o toShake1 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 reduce = { 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 diff --git a/src/especialize.sml b/src/especialize.sml index 4936cc61..b0a4a8c2 100644 --- a/src/especialize.sml +++ b/src/especialize.sml @@ -43,6 +43,13 @@ structure KM = BinaryMapFn(K) 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 @@ fun specialize' (funcs, specialized) file = 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 @@ fun specialize' (funcs, specialized) file = 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), diff --git a/src/reduce.sml b/src/reduce.sml index 150e0bad..b7ad567a 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -423,7 +423,15 @@ fun kindConAndExp (namedC, namedE) = 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 @@ fun kindConAndExp (namedC, namedE) = 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 @@ fun kindConAndExp (namedC, namedE) = 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 -- cgit v1.2.3