diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2010-06-03 13:04:37 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2010-06-03 13:04:37 -0400 |
| commit | b1d29df128dd1fa879e24f0eb3f5cdc1b74e16b7 (patch) | |
| tree | 370066a96da7c7aff61371c96f82804cde02fa75 /src/elab_util.sml | |
| parent | ccc3c126378aaa53765f8d69c267c6ffee666acf (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.sml | 32 |
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) => |