Mercurial > urweb

comparison src/corify.sml @ 806:0e554bfd6d6a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Corify
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:22:05 -0400
parents 3b7e46790fa7
children 61a1f5c5ae2c
comparison
equal deleted inserted replaced
805:e2780d2f4afc 806:0e554bfd6d6a
619 let 619 let
620 val (st, n) = St.bindCon st x n 620 val (st, n) = St.bindCon st x n
621 in 621 in
622 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) 622 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
623 end 623 end
624 | L.DDatatype (x, n, xs, xncs) => 624 | L.DDatatype _ => raise Fail "Corify DDatatype"
625 (*| L.DDatatype (x, n, xs, xncs) =>
625 let 626 let
626 val (st, n) = St.bindCon st x n 627 val (st, n) = St.bindCon st x n
627 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 628 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
628 let 629 let
629 val st = St.bindConstructor st x n (L'.PConVar n) 630 val st = St.bindConstructor st x n (L'.PConVar n)
656 in 657 in
657 (L'.DVal (x, n, t, e, ""), loc) 658 (L'.DVal (x, n, t, e, ""), loc)
658 end) xncs 659 end) xncs
659 in 660 in
660 ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st) 661 ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st)
661 end 662 end*)
662 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => 663 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
663 let 664 let
664 val (st, n) = St.bindCon st x n 665 val (st, n) = St.bindCon st x n
665 val c = corifyCon st (L.CModProj (m1, ms, s), loc) 666 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
666 667
793 conmap, 794 conmap,
794 st, 795 st,
795 trans) 796 trans)
796 end 797 end
797 798
798 | L.SgiDatatype (x, n, xs, xnts) => 799 | L.SgiDatatype _ => raise Fail "Corify SgiDatatype"
800 (*| L.SgiDatatype (x, n, xs, xnts) =>
799 let 801 let
800 val k = (L'.KType, loc) 802 val k = (L'.KType, loc)
801 val dk = ElabUtil.classifyDatatype xnts 803 val dk = ElabUtil.classifyDatatype xnts
802 val (st, n') = St.bindCon st x n 804 val (st, n') = St.bindCon st x n
803 val (xnts, (ds', st, cmap, conmap)) = 805 val (xnts, (ds', st, cmap, conmap)) =
854 (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds, 856 (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds,
855 cmap, 857 cmap,
856 conmap, 858 conmap,
857 st, 859 st,
858 trans) 860 trans)
859 end 861 end*)
860 862
861 | L.SgiVal (x, _, c) => 863 | L.SgiVal (x, _, c) =>
862 let 864 let
863 val c = 865 val c =
864 case trans of 866 case trans of
1059 end 1061 end
1060 1062
1061 fun maxName ds = foldl (fn ((d, _), n) => 1063 fun maxName ds = foldl (fn ((d, _), n) =>
1062 case d of 1064 case d of
1063 L.DCon (_, n', _, _) => Int.max (n, n') 1065 L.DCon (_, n', _, _) => Int.max (n, n')
1064 | L.DDatatype (_, n', _, _) => Int.max (n, n') 1066 | L.DDatatype dts => foldl (fn ((_, n', _, _), n) => Int.max (n, n')) n dts
1065 | L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n') 1067 | L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n')
1066 | L.DVal (_, n', _, _) => Int.max (n, n') 1068 | L.DVal (_, n', _, _) => Int.max (n, n')
1067 | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis 1069 | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis
1068 | L.DSgn (_, n', _) => Int.max (n, n') 1070 | L.DSgn (_, n', _) => Int.max (n, n')
1069 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str)) 1071 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))