Mercurial > urweb

comparison src/corify.sml @ 807:61a1f5c5ae2c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Effectize
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:45:12 -0400
parents 0e554bfd6d6a
children 7b380e2b9e68
comparison
equal deleted inserted replaced
806:0e554bfd6d6a 807:61a1f5c5ae2c
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 _ => raise Fail "Corify DDatatype" 624 | L.DDatatype dts =>
625 (*| L.DDatatype (x, n, xs, xncs) => 625 let
626 let 626 val (dts, st) = ListUtil.foldlMap (fn ((x, n, xs, xncs), st) =>
627 val (st, n) = St.bindCon st x n 627 let
628 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 628 val (st, n) = St.bindCon st x n
629 let 629 in
630 val st = St.bindConstructor st x n (L'.PConVar n) 630 ((x, n, xs, xncs), st)
631 val st = St.bindConstructorVal st x n 631 end)
632 val co = Option.map (corifyCon st) co 632 st dts
633 in 633
634 ((x, n, co), st) 634 val (dts, (st, dcons)) =
635 end) st xncs 635 ListUtil.foldlMap
636 636 (fn ((x, n, xs, xncs), (st, dcons)) =>
637 val dk = ElabUtil.classifyDatatype xncs 637 let
638 val t = (L'.CNamed n, loc) 638 val (xncs, st) = ListUtil.foldlMap
639 val nxs = length xs - 1 639 (fn ((x, n, co), st) =>
640 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs 640 let
641 val k = (L'.KType, loc) 641 val st = St.bindConstructor st x n (L'.PConVar n)
642 val dcons = map (fn (x, n, to) => 642 val st = St.bindConstructorVal st x n
643 let 643 val co = Option.map (corifyCon st) co
644 val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs 644 in
645 val (e, t) = 645 ((x, n, co), st)
646 case to of 646 end) st xncs
647 NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) 647
648 | SOME t' => ((L'.EAbs ("x", t', t, 648 val dk = ElabUtil.classifyDatatype xncs
649 (L'.ECon (dk, L'.PConVar n, args, 649 val t = (L'.CNamed n, loc)
650 SOME (L'.ERel 0, loc)), 650 val nxs = length xs - 1
651 loc)), 651 val t = ListUtil.foldli
652 loc), 652 (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
653 (L'.TFun (t', t), loc)) 653 val k = (L'.KType, loc)
654 654 val dcons' = map (fn (x, n, to) =>
655 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs 655 let
656 val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs 656 val args = ListUtil.mapi
657 in 657 (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
658 (L'.DVal (x, n, t, e, ""), loc) 658 val (e, t) =
659 end) xncs 659 case to of
660 in 660 NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE),
661 ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st) 661 loc), t)
662 end*) 662 | SOME t' => ((L'.EAbs ("x", t', t,
663 (L'.ECon (dk, L'.PConVar n,
664 args,
665 SOME (L'.ERel 0,
666 loc)),
667 loc)),
668 loc),
669 (L'.TFun (t', t), loc))
670
671 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
672 val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
673 in
674 (L'.DVal (x, n, t, e, ""), loc)
675 end) xncs
676 in
677 ((x, n, xs, xncs), (st, dcons' @ dcons))
678 end)
679 (st, []) dts
680 in
681 ((L'.DDatatype dts, loc) :: dcons, st)
682 end
663 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => 683 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
664 let 684 let
665 val (st, n) = St.bindCon st x n 685 val (st, n) = St.bindCon st x n
666 val c = corifyCon st (L.CModProj (m1, ms, s), loc) 686 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
667 687
794 conmap, 814 conmap,
795 st, 815 st,
796 trans) 816 trans)
797 end 817 end
798 818
799 | L.SgiDatatype _ => raise Fail "Corify SgiDatatype" 819 | L.SgiDatatype dts =>
800 (*| L.SgiDatatype (x, n, xs, xnts) =>
801 let 820 let
802 val k = (L'.KType, loc) 821 val k = (L'.KType, loc)
803 val dk = ElabUtil.classifyDatatype xnts 822
804 val (st, n') = St.bindCon st x n 823 val (dts, (ds', st, cmap, conmap)) =
805 val (xnts, (ds', st, cmap, conmap)) =
806 ListUtil.foldlMap 824 ListUtil.foldlMap
807 (fn ((x', n, to), (ds', st, cmap, conmap)) => 825 (fn ((x, n, xs, xnts), (ds', st, cmap, conmap)) =>
808 let 826 let
809 val dt = (L'.CNamed n', loc) 827 val dk = ElabUtil.classifyDatatype xnts
810 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs 828 val (st, n') = St.bindCon st x n
811 829 val (xnts, (ds', st, cmap, conmap)) =
812 val to = Option.map (corifyCon st) to 830 ListUtil.foldlMap
813 831 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
814 val pc = L'.PConFfi {mod = m, 832 let
815 datatyp = x, 833 val dt = (L'.CNamed n', loc)
816 params = xs, 834 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
817 con = x', 835
818 arg = to, 836 val to = Option.map (corifyCon st) to
819 kind = dk} 837
820 838 val pc = L'.PConFfi {mod = m,
821 fun wrapT t = 839 datatyp = x,
822 foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs 840 params = xs,
823 fun wrapE e = 841 con = x',
824 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs 842 arg = to,
825 843 kind = dk}
826 val (cmap, d) = 844
827 case to of 845 fun wrapT t =
828 NONE => (SM.insert (cmap, x', wrapT dt), 846 foldr (fn (x, t) => (L'.TCFun (x, k, t), loc))
829 (L'.DVal (x', n, wrapT dt, 847 t xs
830 wrapE 848 fun wrapE e =
831 (L'.ECon (dk, pc, args, NONE), 849 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc))
832 loc), 850 e xs
833 ""), loc)) 851
834 | SOME t => 852 val (cmap, d) =
835 let 853 case to of
836 val tf = (L'.TFun (t, dt), loc) 854 NONE => (SM.insert (cmap, x', wrapT dt),
837 val e = wrapE (L'.EAbs ("x", t, tf, 855 (L'.DVal (x', n, wrapT dt,
838 (L'.ECon (dk, pc, args, 856 wrapE
839 SOME (L'.ERel 0, 857 (L'.ECon (dk, pc,
840 loc)), 858 args,
841 loc)), loc) 859 NONE),
842 val d = (L'.DVal (x', n, wrapT tf, 860 loc),
843 e, ""), loc) 861 ""), loc))
844 in 862 | SOME t =>
845 (SM.insert (cmap, x', wrapT tf), d) 863 let
846 end 864 val tf = (L'.TFun (t, dt), loc)
847 865 val e = wrapE
848 val st = St.bindConstructor st x' n pc 866 (L'.EAbs ("x", t, tf,
849 867 (L'.ECon (dk,
850 val conmap = SM.insert (conmap, x', (x, xs, to, dk)) 868 pc,
869 args,
870 SOME
871 (L'.ERel 0,
872 loc)),
873 loc)), loc)
874 val d = (L'.DVal (x', n, wrapT tf,
875 e, ""), loc)
876 in
877 (SM.insert (cmap, x', wrapT tf), d)
878 end
879
880 val st = St.bindConstructor st x' n pc
881
882 val conmap = SM.insert (conmap, x',
883 (x, xs, to, dk))
884 in
885 ((x', n, to),
886 (d :: ds', st, cmap, conmap))
887 end) (ds', st, cmap, conmap) xnts
851 in 888 in
852 ((x', n, to), 889 ((x, n', xs, xnts), (ds', st, cmap, conmap))
853 (d :: ds', st, cmap, conmap)) 890 end)
854 end) ([], st, cmap, conmap) xnts 891 ([], st, cmap, conmap) dts
855 in 892 in
856 (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds, 893 (ds' @ (L'.DDatatype dts, loc) :: ds,
857 cmap, 894 cmap,
858 conmap, 895 conmap,
859 st, 896 st,
860 trans) 897 trans)
861 end*) 898 end
862 899
863 | L.SgiVal (x, _, c) => 900 | L.SgiVal (x, _, c) =>
864 let 901 let
865 val c = 902 val c =
866 case trans of 903 case trans of