Got split1 working, but noticed a nasty type inference bug with transplanted unification variables

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