Mercurial > urweb

comparison src/elab_util.sml @ 792:d20d6afc1206

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Improvements while working on Graftid
author Adam Chlipala <adamc@hcoop.net>
date Tue, 12 May 2009 18:02:25 -0400
parents 8688e01ae469
children e2780d2f4afc
comparison
equal deleted inserted replaced
791:5368deb3764b 792:d20d6afc1206
111 structure Con = struct 111 structure Con = struct
112 112
113 datatype binder = 113 datatype binder =
114 RelK of string 114 RelK of string
115 | RelC of string * Elab.kind 115 | RelC of string * Elab.kind
116 | NamedC of string * int * Elab.kind 116 | NamedC of string * int * Elab.kind * Elab.con option
117 117
118 fun mapfoldB {kind = fk, con = fc, bind} = 118 fun mapfoldB {kind = fk, con = fc, bind} =
119 let 119 let
120 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, s) => bind (ctx, RelK s)} 120 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, s) => bind (ctx, RelK s)}
121 121
285 structure Exp = struct 285 structure Exp = struct
286 286
287 datatype binder = 287 datatype binder =
288 RelK of string 288 RelK of string
289 | RelC of string * Elab.kind 289 | RelC of string * Elab.kind
290 | NamedC of string * int * Elab.kind 290 | NamedC of string * int * Elab.kind * Elab.con option
291 | RelE of string * Elab.con 291 | RelE of string * Elab.con
292 | NamedE of string * Elab.con 292 | NamedE of string * Elab.con
293 293
294 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = 294 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
295 let 295 let
532 structure Sgn = struct 532 structure Sgn = struct
533 533
534 datatype binder = 534 datatype binder =
535 RelK of string 535 RelK of string
536 | RelC of string * Elab.kind 536 | RelC of string * Elab.kind
537 | NamedC of string * int * Elab.kind 537 | NamedC of string * int * Elab.kind * Elab.con option
538 | Str of string * Elab.sgn 538 | Str of string * int * Elab.sgn
539 | Sgn of string * Elab.sgn 539 | Sgn of string * int * Elab.sgn
540 540
541 fun mapfoldB {kind, con, sgn_item, sgn, bind} = 541 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
542 let 542 let
543 fun bind' (ctx, b) = 543 fun bind' (ctx, b) =
544 let 544 let
622 case s of 622 case s of
623 SgnConst sgis => 623 SgnConst sgis =>
624 S.map2 (ListUtil.mapfoldB (fn (ctx, si) => 624 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
625 (case #1 si of 625 (case #1 si of
626 SgiConAbs (x, n, k) => 626 SgiConAbs (x, n, k) =>
627 bind (ctx, NamedC (x, n, k)) 627 bind (ctx, NamedC (x, n, k, NONE))
628 | SgiCon (x, n, k, _) => 628 | SgiCon (x, n, k, c) =>
629 bind (ctx, NamedC (x, n, k)) 629 bind (ctx, NamedC (x, n, k, SOME c))
630 | SgiDatatype (x, n, _, xncs) => 630 | SgiDatatype (x, n, _, xncs) =>
631 bind (ctx, NamedC (x, n, (KType, loc))) 631 bind (ctx, NamedC (x, n, (KType, loc), NONE))
632 | SgiDatatypeImp (x, n, _, _, _, _, _) => 632 | SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
633 bind (ctx, NamedC (x, n, (KType, loc))) 633 bind (ctx, NamedC (x, n, (KType, loc),
634 SOME (CModProj (m1, ms, s), loc)))
634 | SgiVal _ => ctx 635 | SgiVal _ => ctx
635 | SgiStr (x, _, sgn) => 636 | SgiStr (x, n, sgn) =>
636 bind (ctx, Str (x, sgn)) 637 bind (ctx, Str (x, n, sgn))
637 | SgiSgn (x, _, sgn) => 638 | SgiSgn (x, n, sgn) =>
638 bind (ctx, Sgn (x, sgn)) 639 bind (ctx, Sgn (x, n, sgn))
639 | SgiConstraint _ => ctx 640 | SgiConstraint _ => ctx
640 | SgiClassAbs (x, n, k) => 641 | SgiClassAbs (x, n, k) =>
641 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))) 642 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), NONE))
642 | SgiClass (x, n, k, _) => 643 | SgiClass (x, n, k, c) =>
643 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))), 644 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c)),
644 sgi ctx si)) ctx sgis, 645 sgi ctx si)) ctx sgis,
645 fn sgis' => 646 fn sgis' =>
646 (SgnConst sgis', loc)) 647 (SgnConst sgis', loc))
647 648
648 | SgnVar _ => S.return2 sAll 649 | SgnVar _ => S.return2 sAll
649 | SgnFun (m, n, s1, s2) => 650 | SgnFun (m, n, s1, s2) =>
650 S.bind2 (sg ctx s1, 651 S.bind2 (sg ctx s1,
651 fn s1' => 652 fn s1' =>
652 S.map2 (sg (bind (ctx, Str (m, s1'))) s2, 653 S.map2 (sg (bind (ctx, Str (m, n, s1'))) s2,
653 fn s2' => 654 fn s2' =>
654 (SgnFun (m, n, s1', s2'), loc))) 655 (SgnFun (m, n, s1', s2'), loc)))
655 | SgnProj _ => S.return2 sAll 656 | SgnProj _ => S.return2 sAll
656 | SgnWhere (sgn, x, c) => 657 | SgnWhere (sgn, x, c) =>
657 S.bind2 (sg ctx sgn, 658 S.bind2 (sg ctx sgn,
669 con = fn () => con, 670 con = fn () => con,
670 sgn_item = fn () => sgn_item, 671 sgn_item = fn () => sgn_item,
671 sgn = fn () => sgn, 672 sgn = fn () => sgn,
672 bind = fn ((), _) => ()} () 673 bind = fn ((), _) => ()} ()
673 674
675 fun mapB {kind, con, sgn_item, sgn, bind} ctx s =
676 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
677 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
678 sgn_item = fn ctx => fn sgi => fn () => S.Continue (sgn_item ctx sgi, ()),
679 sgn = fn ctx => fn s => fn () => S.Continue (sgn ctx s, ()),
680 bind = bind} ctx s () of
681 S.Continue (s, ()) => s
682 | S.Return _ => raise Fail "ElabUtil.Sgn.mapB: Impossible"
683
674 fun map {kind, con, sgn_item, sgn} s = 684 fun map {kind, con, sgn_item, sgn} s =
675 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), 685 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
676 con = fn c => fn () => S.Continue (con c, ()), 686 con = fn c => fn () => S.Continue (con c, ()),
677 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()), 687 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
678 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of 688 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
684 structure Decl = struct 694 structure Decl = struct
685 695
686 datatype binder = 696 datatype binder =
687 RelK of string 697 RelK of string
688 | RelC of string * Elab.kind 698 | RelC of string * Elab.kind
689 | NamedC of string * int * Elab.kind 699 | NamedC of string * int * Elab.kind * Elab.con option
690 | RelE of string * Elab.con 700 | RelE of string * Elab.con
691 | NamedE of string * Elab.con 701 | NamedE of string * Elab.con
692 | Str of string * Elab.sgn 702 | Str of string * Elab.sgn
693 | Sgn of string * Elab.sgn 703 | Sgn of string * Elab.sgn
694 704
724 let 734 let
725 val b' = case b of 735 val b' = case b of
726 Sgn.RelK x => RelK x 736 Sgn.RelK x => RelK x
727 | Sgn.RelC x => RelC x 737 | Sgn.RelC x => RelC x
728 | Sgn.NamedC x => NamedC x 738 | Sgn.NamedC x => NamedC x
729 | Sgn.Sgn x => Sgn x 739 | Sgn.Sgn (x, _, y) => Sgn (x, y)
730 | Sgn.Str x => Str x 740 | Sgn.Str (x, _, y) => Str (x, y)
731 in 741 in
732 bind (ctx, b') 742 bind (ctx, b')
733 end 743 end
734 val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'} 744 val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
735 745
739 and mfst' ctx (strAll as (str, loc)) = 749 and mfst' ctx (strAll as (str, loc)) =
740 case str of 750 case str of
741 StrConst ds => 751 StrConst ds =>
742 S.map2 (ListUtil.mapfoldB (fn (ctx, d) => 752 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
743 (case #1 d of 753 (case #1 d of
744 DCon (x, n, k, _) => 754 DCon (x, n, k, c) =>
745 bind (ctx, NamedC (x, n, k)) 755 bind (ctx, NamedC (x, n, k, SOME c))
746 | DDatatype (x, n, xs, xncs) => 756 | DDatatype (x, n, xs, xncs) =>
747 let 757 let
748 val ctx = bind (ctx, NamedC (x, n, (KType, loc))) 758 val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
749 in 759 in
750 foldl (fn ((x, _, co), ctx) => 760 foldl (fn ((x, _, co), ctx) =>
751 let 761 let
752 val t = 762 val t =
753 case co of 763 case co of
766 bind (ctx, NamedE (x, t)) 776 bind (ctx, NamedE (x, t))
767 end) 777 end)
768 ctx xncs 778 ctx xncs
769 end 779 end
770 | DDatatypeImp (x, n, m, ms, x', _, _) => 780 | DDatatypeImp (x, n, m, ms, x', _, _) =>
771 bind (ctx, NamedC (x, n, (KType, loc))) 781 bind (ctx, NamedC (x, n, (KType, loc),
782 SOME (CModProj (m, ms, x'), loc)))
772 | DVal (x, _, c, _) => 783 | DVal (x, _, c, _) =>
773 bind (ctx, NamedE (x, c)) 784 bind (ctx, NamedE (x, c))
774 | DValRec vis => 785 | DValRec vis =>
775 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis 786 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
776 | DSgn (x, _, sgn) => 787 | DSgn (x, _, sgn) =>
796 val ct = (CModProj (n, [], "sql_view"), loc) 807 val ct = (CModProj (n, [], "sql_view"), loc)
797 val ct = (CApp (ct, c), loc) 808 val ct = (CApp (ct, c), loc)
798 in 809 in
799 bind (ctx, NamedE (x, ct)) 810 bind (ctx, NamedE (x, ct))
800 end 811 end
801 | DClass (x, n, k, _) => 812 | DClass (x, n, k, c) =>
802 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))) 813 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c))
803 | DDatabase _ => ctx 814 | DDatabase _ => ctx
804 | DCookie (tn, x, n, c) => 815 | DCookie (tn, x, n, c) =>
805 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc), 816 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
806 c), loc))) 817 c), loc)))
807 | DStyle (tn, x, n) => 818 | DStyle (tn, x, n) =>