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,