summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-14 09:11:58 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-14 09:11:58 -0400
commit9e6bd5dd1394c99f0a9b29369a4957c958e0830c (patch)
tree40c991c6a8032bc73433e5d3f9c1db78a98674ef /src
parent22b407de7cf9ee5cc5947369372d9ca8373134a6 (diff)
Fix a nasty binding bug in CoreUtil
Diffstat (limited to 'src')
-rw-r--r--src/core_print.sml10
-rw-r--r--src/core_util.sml8
-rw-r--r--src/expl_print.sml16
-rw-r--r--src/unpoly.sml9
4 files changed, 29 insertions, 14 deletions
diff --git a/src/core_print.sml b/src/core_print.sml
index 971aa4b4..e9d8951e 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -198,12 +198,18 @@ fun p_con_named env n =
fun p_patCon env pc =
case pc of
PConVar n => p_con_named env n
- | PConFfi {mod = m, con, arg, ...} =>
+ | PConFfi {mod = m, con, arg, params, ...} =>
if !debug then
box [string "FFIC[",
case arg of
NONE => box []
- | SOME t => p_con env t,
+ | SOME t =>
+ let
+ val k = (KType, ErrorMsg.dummySpan)
+ val env' = foldl (fn (x, env) => E.pushCRel env x k) env params
+ in
+ p_con env' t
+ end,
string "](",
string m,
string ".",
diff --git a/src/core_util.sml b/src/core_util.sml
index ae956121..e3ec8a1d 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -772,7 +772,13 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
| PConFfi {mod = m, datatyp, params, con, arg, kind} =>
S.map2 ((case arg of
NONE => S.return2 NONE
- | SOME c => S.map2 (mfc ctx c, SOME)),
+ | SOME c =>
+ let
+ val k = (KType, ErrorMsg.dummySpan)
+ val ctx' = foldl (fn (x, ctx) => bind (ctx, RelC (x, k))) ctx params
+ in
+ S.map2 (mfc ctx' c, SOME)
+ end),
fn arg' =>
PConFfi {mod = m, datatyp = datatyp, params = params,
con = con, arg = arg', kind = kind})
diff --git a/src/expl_print.sml b/src/expl_print.sml
index e6b28fea..7aa36c6d 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -219,9 +219,19 @@ fun p_pat' par env (p, _) =
| PVar (s, _) => string s
| PPrim p => Prim.p_t p
| PCon (_, pc, _, NONE) => p_patCon env pc
- | PCon (_, pc, _, SOME p) => parenIf par (box [p_patCon env pc,
- space,
- p_pat' true env p])
+ | PCon (_, pc, cs, SOME p) =>
+ if !debug then
+ parenIf par (box [p_patCon env pc,
+ string "[",
+ p_list (p_con env) cs,
+ string "]",
+ space,
+ p_pat' true env p])
+ else
+ parenIf par (box [p_patCon env pc,
+ space,
+ p_pat' true env p])
+
| PRecord xps =>
box [string "{",
p_list_sep (box [string ",", space]) (fn (x, p, _) =>
diff --git a/src/unpoly.sml b/src/unpoly.sml
index 56406636..6f838392 100644
--- a/src/unpoly.sml
+++ b/src/unpoly.sml
@@ -138,14 +138,7 @@ fun exp (e, st : state) =
in
trim (t, e, cargs)
end
- | (_, _, []) =>
- (*let
- val e = foldl (fn ((_, n, n_old, _, _, _), e) =>
- unpolyNamed (n_old, ENamed n) e)
- e vis
- in*)
- SOME (t, e)
- (*end*)
+ | (_, _, []) => SOME (t, e)
| _ => NONE
in
(*Print.prefaces "specialize"