Mercurial > urweb
comparison 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 |
comparison
equal
deleted
inserted
replaced
1271:503d4ec93494 | 1272:56bd4a4f6e66 |
---|---|
427 | PCon (_, _, _, NONE) => ctx | 427 | PCon (_, _, _, NONE) => ctx |
428 | PCon (_, _, _, SOME p) => pb (p, ctx) | 428 | PCon (_, _, _, SOME p) => pb (p, ctx) |
429 | PRecord xps => foldl (fn ((_, p, _), ctx) => | 429 | PRecord xps => foldl (fn ((_, p, _), ctx) => |
430 pb (p, ctx)) ctx xps | 430 pb (p, ctx)) ctx xps |
431 in | 431 in |
432 S.map2 (mfe (pb (p, ctx)) e, | 432 S.bind2 (mfp ctx p, |
433 fn e' => (p, e')) | 433 fn p' => |
434 S.map2 (mfe (pb (p', ctx)) e, | |
435 fn e' => (p', e'))) | |
434 end) pes, | 436 end) pes, |
435 fn pes' => | 437 fn pes' => |
436 S.bind2 (mfc ctx disc, | 438 S.bind2 (mfc ctx disc, |
437 fn disc' => | 439 fn disc' => |
438 S.map2 (mfc ctx result, | 440 S.map2 (mfc ctx result, |
479 S.bind2 (mfe ctx e, | 481 S.bind2 (mfe ctx e, |
480 fn e' => | 482 fn e' => |
481 S.map2 (mfk ctx k, | 483 S.map2 (mfk ctx k, |
482 fn k' => | 484 fn k' => |
483 (EKApp (e', k'), loc))) | 485 (EKApp (e', k'), loc))) |
486 | |
487 and mfp ctx (pAll as (p, loc)) = | |
488 case p of | |
489 PWild => S.return2 pAll | |
490 | PVar (x, t) => | |
491 S.map2 (mfc ctx t, | |
492 fn t' => | |
493 (PVar (x, t'), loc)) | |
494 | PPrim _ => S.return2 pAll | |
495 | PCon (dk, pc, args, po) => | |
496 S.bind2 (ListUtil.mapfold (mfc ctx) args, | |
497 fn args' => | |
498 S.map2 ((case po of | |
499 NONE => S.return2 NONE | |
500 | SOME p => S.map2 (mfp ctx p, SOME)), | |
501 fn po' => | |
502 (PCon (dk, pc, args', po'), loc))) | |
503 | PRecord xps => | |
504 S.map2 (ListUtil.mapfold (fn (x, p, c) => | |
505 S.bind2 (mfp ctx p, | |
506 fn p' => | |
507 S.map2 (mfc ctx c, | |
508 fn c' => | |
509 (x, p', c')))) xps, | |
510 fn xps' => | |
511 (PRecord xps', loc)) | |
484 | 512 |
485 and mfed ctx (dAll as (d, loc)) = | 513 and mfed ctx (dAll as (d, loc)) = |
486 case d of | 514 case d of |
487 EDVal (p, t, e) => | 515 EDVal (p, t, e) => |
488 S.bind2 (mfc ctx t, | 516 S.bind2 (mfc ctx t, |