summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/ur/incl.ur4
-rw-r--r--lib/ur/incl.urs2
-rw-r--r--src/compiler.sig3
-rw-r--r--src/compiler.sml20
-rw-r--r--src/especialize.sml15
-rw-r--r--src/reduce.sml33
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 09:56:34 +0000