Mercurial > urweb

comparison src/elab_util.sml @ 826:78504d97410b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix EDLet elab_util bug
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 May 2009 12:40:55 -0400
parents 7f871c03e3a1
children b2413e4dd109
comparison
equal deleted inserted replaced
825:7f871c03e3a1 826:78504d97410b
436 | EUnif (ref (SOME e)) => mfe ctx e 436 | EUnif (ref (SOME e)) => mfe ctx e
437 | EUnif _ => S.return2 eAll 437 | EUnif _ => S.return2 eAll
438 438
439 | ELet (des, e, t) => 439 | ELet (des, e, t) =>
440 let 440 let
441 val (des, ctx) = foldl (fn (ed, (des, ctx)) => 441 val (des, ctx') = foldl (fn (ed, (des, ctx)) =>
442 let 442 let
443 val ctx' = 443 val ctx' =
444 case #1 ed of 444 case #1 ed of
445 EDVal (p, _, _) => doVars (p, ctx) 445 EDVal (p, _, _) => doVars (p, ctx)
446 | EDValRec vis => 446 | EDValRec vis =>
447 foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis 447 foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t)))
448 in 448 ctx vis
449 (S.bind2 (des, 449 in
450 fn des' => 450 (S.bind2 (des,
451 S.map2 (mfed ctx ed, 451 fn des' =>
452 fn ed' => des' @ [ed'])), 452 S.map2 (mfed ctx ed,
453 ctx') 453 fn ed' => ed' :: des')),
454 end) 454 ctx')
455 end)
455 (S.return2 [], ctx) des 456 (S.return2 [], ctx) des
456 in 457 in
457 S.bind2 (des, 458 S.bind2 (des,
458 fn des' => 459 fn des' =>
459 S.bind2 (mfe ctx e, 460 S.bind2 (mfe ctx' e,
460 fn e' => 461 fn e' =>
461 S.map2 (mfc ctx t, 462 S.map2 (mfc ctx t,
462 fn t' => 463 fn t' =>
463 (ELet (des', e', t'), loc)))) 464 (ELet (rev des', e', t'), loc))))
464 end 465 end
465 466
466 | EKAbs (x, e) => 467 | EKAbs (x, e) =>
467 S.map2 (mfe (bind (ctx, RelK x)) e, 468 S.map2 (mfe (bind (ctx, RelK x)) e,
468 fn e' => 469 fn e' =>
477 and mfed ctx (dAll as (d, loc)) = 478 and mfed ctx (dAll as (d, loc)) =
478 case d of 479 case d of
479 EDVal (p, t, e) => 480 EDVal (p, t, e) =>
480 S.bind2 (mfc ctx t, 481 S.bind2 (mfc ctx t,
481 fn t' => 482 fn t' =>
482 S.map2 (mfe (doVars (p, ctx)) e, 483 S.map2 (mfe ctx e,
483 fn e' => 484 fn e' =>
484 (EDVal (p, t', e'), loc))) 485 (EDVal (p, t', e'), loc)))
485 | EDValRec vis => 486 | EDValRec vis =>
486 let 487 let
487 val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis 488 val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis