summaryrefslogtreecommitdiff
path: root/src/elab_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-06-03 13:04:37 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-06-03 13:04:37 -0400
commit63f77395df8d7e78c21437876ce585b01517f0cc (patch)
tree370066a96da7c7aff61371c96f82804cde02fa75 /src/elab_util.sml
parent4c67cd1d61cb79224bbe90dbdb229e0d9b58d3c9 (diff)
Some serious bug-fix work to get HTML example to compile; this includes fixing a bug with 'val' patterns in Unnest and the need for more local reduction in Especialize
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml32
1 files changed, 30 insertions, 2 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 8345e3f3..ec6c51ba 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -429,8 +429,10 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
| PRecord xps => foldl (fn ((_, p, _), ctx) =>
pb (p, ctx)) ctx xps
in
- S.map2 (mfe (pb (p, ctx)) e,
- fn e' => (p, e'))
+ S.bind2 (mfp ctx p,
+ fn p' =>
+ S.map2 (mfe (pb (p', ctx)) e,
+ fn e' => (p', e')))
end) pes,
fn pes' =>
S.bind2 (mfc ctx disc,
@@ -482,6 +484,32 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
fn k' =>
(EKApp (e', k'), loc)))
+ and mfp ctx (pAll as (p, loc)) =
+ case p of
+ PWild => S.return2 pAll
+ | PVar (x, t) =>
+ S.map2 (mfc ctx t,
+ fn t' =>
+ (PVar (x, t'), loc))
+ | PPrim _ => S.return2 pAll
+ | PCon (dk, pc, args, po) =>
+ S.bind2 (ListUtil.mapfold (mfc ctx) args,
+ fn args' =>
+ S.map2 ((case po of
+ NONE => S.return2 NONE
+ | SOME p => S.map2 (mfp ctx p, SOME)),
+ fn po' =>
+ (PCon (dk, pc, args', po'), loc)))
+ | PRecord xps =>
+ S.map2 (ListUtil.mapfold (fn (x, p, c) =>
+ S.bind2 (mfp ctx p,
+ fn p' =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (x, p', c')))) xps,
+ fn xps' =>
+ (PRecord xps', loc))
+
and mfed ctx (dAll as (d, loc)) =
case d of
EDVal (p, t, e) =>