Mercurial > urweb

comparison src/elab_util.sml @ 805:e2780d2f4afc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Elaborate
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:14:17 -0400
parents d20d6afc1206
children 7f871c03e3a1
comparison
equal deleted inserted replaced
804:10fe57e4a8c2 805:e2780d2f4afc
566 S.bind2 (kind ctx k, 566 S.bind2 (kind ctx k,
567 fn k' => 567 fn k' =>
568 S.map2 (con ctx c, 568 S.map2 (con ctx c,
569 fn c' => 569 fn c' =>
570 (SgiCon (x, n, k', c'), loc))) 570 (SgiCon (x, n, k', c'), loc)))
571 | SgiDatatype (x, n, xs, xncs) => 571 | SgiDatatype dts =>
572 S.map2 (ListUtil.mapfold (fn (x, n, c) => 572 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
573 case c of 573 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
574 NONE => S.return2 (x, n, c) 574 case c of
575 | SOME c => 575 NONE => S.return2 (x, n, c)
576 S.map2 (con ctx c, 576 | SOME c =>
577 fn c' => (x, n, SOME c'))) xncs, 577 S.map2 (con ctx c,
578 fn xncs' => 578 fn c' => (x, n, SOME c'))) xncs,
579 (SgiDatatype (x, n, xs, xncs'), loc)) 579 fn xncs' => (x, n, xs, xncs'))) dts,
580 fn dts' =>
581 (SgiDatatype dts', loc))
580 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => 582 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
581 S.map2 (ListUtil.mapfold (fn (x, n, c) => 583 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
582 case c of 584 case c of
583 NONE => S.return2 (x, n, c) 585 NONE => S.return2 (x, n, c)
584 | SOME c => 586 | SOME c =>
625 (case #1 si of 627 (case #1 si of
626 SgiConAbs (x, n, k) => 628 SgiConAbs (x, n, k) =>
627 bind (ctx, NamedC (x, n, k, NONE)) 629 bind (ctx, NamedC (x, n, k, NONE))
628 | SgiCon (x, n, k, c) => 630 | SgiCon (x, n, k, c) =>
629 bind (ctx, NamedC (x, n, k, SOME c)) 631 bind (ctx, NamedC (x, n, k, SOME c))
630 | SgiDatatype (x, n, _, xncs) => 632 | SgiDatatype dts =>
631 bind (ctx, NamedC (x, n, (KType, loc), NONE)) 633 foldl (fn ((x, n, ks, _), ctx) =>
634 let
635 val k' = (KType, loc)
636 val k = foldl (fn (_, k) => (KArrow (k', k), loc))
637 k' ks
638 in
639 bind (ctx, NamedC (x, n, k, NONE))
640 end) ctx dts
632 | SgiDatatypeImp (x, n, m1, ms, s, _, _) => 641 | SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
633 bind (ctx, NamedC (x, n, (KType, loc), 642 bind (ctx, NamedC (x, n, (KType, loc),
634 SOME (CModProj (m1, ms, s), loc))) 643 SOME (CModProj (m1, ms, s), loc)))
635 | SgiVal _ => ctx 644 | SgiVal _ => ctx
636 | SgiStr (x, n, sgn) => 645 | SgiStr (x, n, sgn) =>
751 StrConst ds => 760 StrConst ds =>
752 S.map2 (ListUtil.mapfoldB (fn (ctx, d) => 761 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
753 (case #1 d of 762 (case #1 d of
754 DCon (x, n, k, c) => 763 DCon (x, n, k, c) =>
755 bind (ctx, NamedC (x, n, k, SOME c)) 764 bind (ctx, NamedC (x, n, k, SOME c))
756 | DDatatype (x, n, xs, xncs) => 765 | DDatatype dts =>
757 let 766 let
758 val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE)) 767 fun doOne ((x, n, xs, xncs), ctx) =
768 let
769 val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
770 in
771 foldl (fn ((x, _, co), ctx) =>
772 let
773 val t =
774 case co of
775 NONE => CNamed n
776 | SOME t => TFun (t, (CNamed n, loc))
777
778 val k = (KType, loc)
779 val t = (t, loc)
780 val t = foldr (fn (x, t) =>
781 (TCFun (Explicit,
782 x,
783 k,
784 t), loc))
785 t xs
786 in
787 bind (ctx, NamedE (x, t))
788 end)
789 ctx xncs
790 end
759 in 791 in
760 foldl (fn ((x, _, co), ctx) => 792 foldl doOne ctx dts
761 let
762 val t =
763 case co of
764 NONE => CNamed n
765 | SOME t => TFun (t, (CNamed n, loc))
766
767 val k = (KType, loc)
768 val t = (t, loc)
769 val t = foldr (fn (x, t) =>
770 (TCFun (Explicit,
771 x,
772 k,
773 t), loc))
774 t xs
775 in
776 bind (ctx, NamedE (x, t))
777 end)
778 ctx xncs
779 end 793 end
780 | DDatatypeImp (x, n, m, ms, x', _, _) => 794 | DDatatypeImp (x, n, m, ms, x', _, _) =>
781 bind (ctx, NamedC (x, n, (KType, loc), 795 bind (ctx, NamedC (x, n, (KType, loc),
782 SOME (CModProj (m, ms, x'), loc))) 796 SOME (CModProj (m, ms, x'), loc)))
783 | DVal (x, _, c, _) => 797 | DVal (x, _, c, _) =>
849 S.bind2 (mfk ctx k, 863 S.bind2 (mfk ctx k,
850 fn k' => 864 fn k' =>
851 S.map2 (mfc ctx c, 865 S.map2 (mfc ctx c,
852 fn c' => 866 fn c' =>
853 (DCon (x, n, k', c'), loc))) 867 (DCon (x, n, k', c'), loc)))
854 | DDatatype (x, n, xs, xncs) => 868 | DDatatype dts =>
855 S.map2 (ListUtil.mapfold (fn (x, n, c) => 869 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
856 case c of 870 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
857 NONE => S.return2 (x, n, c) 871 case c of
858 | SOME c => 872 NONE => S.return2 (x, n, c)
859 S.map2 (mfc ctx c, 873 | SOME c =>
860 fn c' => (x, n, SOME c'))) xncs, 874 S.map2 (mfc ctx c,
861 fn xncs' => 875 fn c' => (x, n, SOME c'))) xncs,
862 (DDatatype (x, n, xs, xncs'), loc)) 876 fn xncs' =>
877 (x, n, xs, xncs'))) dts,
878 fn dts' =>
879 (DDatatype dts', loc))
863 | DDatatypeImp (x, n, m1, ms, s, xs, xncs) => 880 | DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
864 S.map2 (ListUtil.mapfold (fn (x, n, c) => 881 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
865 case c of 882 case c of
866 NONE => S.return2 (x, n, c) 883 NONE => S.return2 (x, n, c)
867 | SOME c => 884 | SOME c =>
1057 fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds 1074 fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds
1058 1075
1059 and maxNameDecl (d, _) = 1076 and maxNameDecl (d, _) =
1060 case d of 1077 case d of
1061 DCon (_, n, _, _) => n 1078 DCon (_, n, _, _) => n
1062 | DDatatype (_, n, _, ns) => 1079 | DDatatype dts =>
1080 foldl (fn ((_, n, _, ns), max) =>
1063 foldl (fn ((_, n', _), m) => Int.max (n', m)) 1081 foldl (fn ((_, n', _), m) => Int.max (n', m))
1064 n ns 1082 (Int.max (n, max)) ns) 0 dts
1065 | DDatatypeImp (_, n1, n2, _, _, _, ns) => 1083 | DDatatypeImp (_, n1, n2, _, _, _, ns) =>
1066 foldl (fn ((_, n', _), m) => Int.max (n', m)) 1084 foldl (fn ((_, n', _), m) => Int.max (n', m))
1067 (Int.max (n1, n2)) ns 1085 (Int.max (n1, n2)) ns
1068 | DVal (_, n, _, _) => n 1086 | DVal (_, n, _, _) => n
1069 | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis 1087 | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis
1099 1117
1100 and maxNameSgi (sgi, _) = 1118 and maxNameSgi (sgi, _) =
1101 case sgi of 1119 case sgi of
1102 SgiConAbs (_, n, _) => n 1120 SgiConAbs (_, n, _) => n
1103 | SgiCon (_, n, _, _) => n 1121 | SgiCon (_, n, _, _) => n
1104 | SgiDatatype (_, n, _, ns) => 1122 | SgiDatatype dts =>
1105 foldl (fn ((_, n', _), m) => Int.max (n', m)) 1123 foldl (fn ((_, n, _, ns), max) =>
1106 n ns 1124 foldl (fn ((_, n', _), m) => Int.max (n', m))
1125 (Int.max (n, max)) ns) 0 dts
1107 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) => 1126 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
1108 foldl (fn ((_, n', _), m) => Int.max (n', m)) 1127 foldl (fn ((_, n', _), m) => Int.max (n', m))
1109 (Int.max (n1, n2)) ns 1128 (Int.max (n1, n2)) ns
1110 | SgiVal (_, n, _) => n 1129 | SgiVal (_, n, _) => n
1111 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1130 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)