Mercurial > urweb

comparison src/elab_util.sml @ 191:aa54250f58ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents 8e9f97508f0d
children ab86aa858e6c
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
394 S.bind2 (kind k, 394 S.bind2 (kind k,
395 fn k' => 395 fn k' =>
396 S.map2 (con ctx c, 396 S.map2 (con ctx c,
397 fn c' => 397 fn c' =>
398 (SgiCon (x, n, k', c'), loc))) 398 (SgiCon (x, n, k', c'), loc)))
399 | SgiDatatype (x, n, xncs) => 399 | SgiDatatype (x, n, xs, xncs) =>
400 S.map2 (ListUtil.mapfold (fn (x, n, c) => 400 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
401 case c of 401 case c of
402 NONE => S.return2 (x, n, c) 402 NONE => S.return2 (x, n, c)
403 | SOME c => 403 | SOME c =>
404 S.map2 (con ctx c, 404 S.map2 (con ctx c,
405 fn c' => (x, n, SOME c'))) xncs, 405 fn c' => (x, n, SOME c'))) xncs,
406 fn xncs' => 406 fn xncs' =>
407 (SgiDatatype (x, n, xncs'), loc)) 407 (SgiDatatype (x, n, xs, xncs'), loc))
408 | SgiDatatypeImp (x, n, m1, ms, s, xncs) => 408 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
409 S.map2 (ListUtil.mapfold (fn (x, n, c) => 409 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
410 case c of 410 case c of
411 NONE => S.return2 (x, n, c) 411 NONE => S.return2 (x, n, c)
412 | SOME c => 412 | SOME c =>
413 S.map2 (con ctx c, 413 S.map2 (con ctx c,
414 fn c' => (x, n, SOME c'))) xncs, 414 fn c' => (x, n, SOME c'))) xncs,
415 fn xncs' => 415 fn xncs' =>
416 (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc)) 416 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
417 | SgiVal (x, n, c) => 417 | SgiVal (x, n, c) =>
418 S.map2 (con ctx c, 418 S.map2 (con ctx c,
419 fn c' => 419 fn c' =>
420 (SgiVal (x, n, c'), loc)) 420 (SgiVal (x, n, c'), loc))
421 | SgiStr (x, n, s) => 421 | SgiStr (x, n, s) =>
443 (case #1 si of 443 (case #1 si of
444 SgiConAbs (x, _, k) => 444 SgiConAbs (x, _, k) =>
445 bind (ctx, NamedC (x, k)) 445 bind (ctx, NamedC (x, k))
446 | SgiCon (x, _, k, _) => 446 | SgiCon (x, _, k, _) =>
447 bind (ctx, NamedC (x, k)) 447 bind (ctx, NamedC (x, k))
448 | SgiDatatype (x, n, xncs) => 448 | SgiDatatype (x, n, _, xncs) =>
449 bind (ctx, NamedC (x, (KType, loc))) 449 bind (ctx, NamedC (x, (KType, loc)))
450 | SgiDatatypeImp (x, _, _, _, _, _) => 450 | SgiDatatypeImp (x, _, _, _, _, _, _) =>
451 bind (ctx, NamedC (x, (KType, loc))) 451 bind (ctx, NamedC (x, (KType, loc)))
452 | SgiVal _ => ctx 452 | SgiVal _ => ctx
453 | SgiStr (x, _, sgn) => 453 | SgiStr (x, _, sgn) =>
454 bind (ctx, Str (x, sgn)) 454 bind (ctx, Str (x, sgn))
455 | SgiSgn (x, _, sgn) => 455 | SgiSgn (x, _, sgn) =>
551 StrConst ds => 551 StrConst ds =>
552 S.map2 (ListUtil.mapfoldB (fn (ctx, d) => 552 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
553 (case #1 d of 553 (case #1 d of
554 DCon (x, _, k, _) => 554 DCon (x, _, k, _) =>
555 bind (ctx, NamedC (x, k)) 555 bind (ctx, NamedC (x, k))
556 | DDatatype (x, n, xncs) => 556 | DDatatype (x, n, xs, xncs) =>
557 let 557 let
558 val ctx = bind (ctx, NamedC (x, (KType, loc))) 558 val ctx = bind (ctx, NamedC (x, (KType, loc)))
559 in 559 in
560 foldl (fn ((x, _, co), ctx) => 560 foldl (fn ((x, _, co), ctx) =>
561 let 561 let
562 val t = 562 val t =
563 case co of 563 case co of
564 NONE => CNamed n 564 NONE => CNamed n
565 | SOME t => TFun (t, (CNamed n, loc)) 565 | SOME t => TFun (t, (CNamed n, loc))
566
567 val k = (KType, loc)
568 val t = (t, loc)
569 val t = foldr (fn (x, t) =>
570 (TCFun (Explicit,
571 x,
572 k,
573 t), loc))
574 t xs
566 in 575 in
567 bind (ctx, NamedE (x, (t, loc))) 576 bind (ctx, NamedE (x, t))
568 end) 577 end)
569 ctx xncs 578 ctx xncs
570 end 579 end
571 | DDatatypeImp (x, n, m, ms, x', _) => 580 | DDatatypeImp (x, n, m, ms, x', _, _) =>
572 bind (ctx, NamedC (x, (KType, loc))) 581 bind (ctx, NamedC (x, (KType, loc)))
573 | DVal (x, _, c, _) => 582 | DVal (x, _, c, _) =>
574 bind (ctx, NamedE (x, c)) 583 bind (ctx, NamedE (x, c))
575 | DValRec vis => 584 | DValRec vis =>
576 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis 585 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
614 S.bind2 (mfk k, 623 S.bind2 (mfk k,
615 fn k' => 624 fn k' =>
616 S.map2 (mfc ctx c, 625 S.map2 (mfc ctx c,
617 fn c' => 626 fn c' =>
618 (DCon (x, n, k', c'), loc))) 627 (DCon (x, n, k', c'), loc)))
619 | DDatatype (x, n, xncs) => 628 | DDatatype (x, n, xs, xncs) =>
620 S.map2 (ListUtil.mapfold (fn (x, n, c) => 629 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
621 case c of 630 case c of
622 NONE => S.return2 (x, n, c) 631 NONE => S.return2 (x, n, c)
623 | SOME c => 632 | SOME c =>
624 S.map2 (mfc ctx c, 633 S.map2 (mfc ctx c,
625 fn c' => (x, n, SOME c'))) xncs, 634 fn c' => (x, n, SOME c'))) xncs,
626 fn xncs' => 635 fn xncs' =>
627 (DDatatype (x, n, xncs'), loc)) 636 (DDatatype (x, n, xs, xncs'), loc))
628 | DDatatypeImp (x, n, m1, ms, s, xncs) => 637 | DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
629 S.map2 (ListUtil.mapfold (fn (x, n, c) => 638 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
630 case c of 639 case c of
631 NONE => S.return2 (x, n, c) 640 NONE => S.return2 (x, n, c)
632 | SOME c => 641 | SOME c =>
633 S.map2 (mfc ctx c, 642 S.map2 (mfc ctx c,
634 fn c' => (x, n, SOME c'))) xncs, 643 fn c' => (x, n, SOME c'))) xncs,
635 fn xncs' => 644 fn xncs' =>
636 (DDatatypeImp (x, n, m1, ms, s, xncs'), loc)) 645 (DDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
637 | DVal vi => 646 | DVal vi =>
638 S.map2 (mfvi ctx vi, 647 S.map2 (mfvi ctx vi,
639 fn vi' => 648 fn vi' =>
640 (DVal vi', loc)) 649 (DVal vi', loc))
641 | DValRec vis => 650 | DValRec vis =>