Mercurial > urweb

comparison src/elab_util.sml @ 825:7f871c03e3a1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Destructing local let, to the point where demo compiles
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 May 2009 12:07:05 -0400
parents e2780d2f4afc
children 78504d97410b
comparison
equal deleted inserted replaced
824:be0988e46336 825:7f871c03e3a1
303 | Con.NamedC x => NamedC x 303 | Con.NamedC x => NamedC x
304 in 304 in
305 bind (ctx, b') 305 bind (ctx, b')
306 end 306 end
307 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} 307 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
308
309 fun doVars ((p, _), ctx) =
310 case p of
311 PWild => ctx
312 | PVar xt => bind (ctx, RelE xt)
313 | PPrim _ => ctx
314 | PCon (_, _, _, NONE) => ctx
315 | PCon (_, _, _, SOME p) => doVars (p, ctx)
316 | PRecord xpcs =>
317 foldl (fn ((_, p, _), ctx) => doVars (p, ctx))
318 ctx xpcs
308 319
309 fun mfe ctx e acc = 320 fun mfe ctx e acc =
310 S.bindP (mfe' ctx e acc, fe ctx) 321 S.bindP (mfe' ctx e acc, fe ctx)
311 322
312 and mfe' ctx (eAll as (e, loc)) = 323 and mfe' ctx (eAll as (e, loc)) =
423 434
424 | EError => S.return2 eAll 435 | EError => S.return2 eAll
425 | EUnif (ref (SOME e)) => mfe ctx e 436 | EUnif (ref (SOME e)) => mfe ctx e
426 | EUnif _ => S.return2 eAll 437 | EUnif _ => S.return2 eAll
427 438
428 | ELet (des, e) => 439 | ELet (des, e, t) =>
429 let 440 let
430 val (des, ctx) = foldl (fn (ed, (des, ctx)) => 441 val (des, ctx) = foldl (fn (ed, (des, ctx)) =>
431 let 442 let
432 val ctx' = 443 val ctx' =
433 case #1 ed of 444 case #1 ed of
434 EDVal (x, t, _) => bind (ctx, RelE (x, t)) 445 EDVal (p, _, _) => doVars (p, ctx)
435 | EDValRec vis => 446 | EDValRec vis =>
436 foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis 447 foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
437 in 448 in
438 (S.bind2 (des, 449 (S.bind2 (des,
439 fn des' => 450 fn des' =>
443 end) 454 end)
444 (S.return2 [], ctx) des 455 (S.return2 [], ctx) des
445 in 456 in
446 S.bind2 (des, 457 S.bind2 (des,
447 fn des' => 458 fn des' =>
448 S.map2 (mfe ctx e, 459 S.bind2 (mfe ctx e,
449 fn e' => 460 fn e' =>
450 (ELet (des', e'), loc))) 461 S.map2 (mfc ctx t,
462 fn t' =>
463 (ELet (des', e', t'), loc))))
451 end 464 end
452 465
453 | EKAbs (x, e) => 466 | EKAbs (x, e) =>
454 S.map2 (mfe (bind (ctx, RelK x)) e, 467 S.map2 (mfe (bind (ctx, RelK x)) e,
455 fn e' => 468 fn e' =>
461 fn k' => 474 fn k' =>
462 (EKApp (e', k'), loc))) 475 (EKApp (e', k'), loc)))
463 476
464 and mfed ctx (dAll as (d, loc)) = 477 and mfed ctx (dAll as (d, loc)) =
465 case d of 478 case d of
466 EDVal vi => 479 EDVal (p, t, e) =>
467 S.map2 (mfvi ctx vi, 480 S.bind2 (mfc ctx t,
468 fn vi' => 481 fn t' =>
469 (EDVal vi', loc)) 482 S.map2 (mfe (doVars (p, ctx)) e,
483 fn e' =>
484 (EDVal (p, t', e'), loc)))
470 | EDValRec vis => 485 | EDValRec vis =>
471 let 486 let
472 val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis 487 val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
473 in 488 in
474 S.map2 (ListUtil.mapfold (mfvi ctx) vis, 489 S.map2 (ListUtil.mapfold (mfvi ctx) vis,