Mercurial > urweb
diff src/elab_util.sml @ 1272:56bd4a4f6e66
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
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 03 Jun 2010 13:04:37 -0400 |
| parents | c316ca3c9ec6 |
| children | b4480a56cab7 |
line wrap: on
line diff
--- a/src/elab_util.sml Tue Jun 01 15:46:24 2010 -0400 +++ b/src/elab_util.sml Thu Jun 03 13:04:37 2010 -0400 @@ -429,8 +429,10 @@ | 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 @@ 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) =>