Mercurial > urweb
comparison src/corify.sml @ 456:1a4fa157fedd
Monoizing FFI transactions correctly
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 06 Nov 2008 09:21:34 -0500 |
parents | 07f6576aeb0a |
children | 5c9606deacb6 |
comparison
equal
deleted
inserted
replaced
455:d4a81273d4b1 | 456:1a4fa157fedd |
---|---|
538 case t of | 538 case t of |
539 L'.TFun (dom, ran) => getArgs (ran, dom :: args) | 539 L'.TFun (dom, ran) => getArgs (ran, dom :: args) |
540 | _ => (all, rev args) | 540 | _ => (all, rev args) |
541 | 541 |
542 val (result, args) = getArgs (t, []) | 542 val (result, args) = getArgs (t, []) |
543 | 543 val (isTransaction, result) = |
544 val (actuals, _) = foldr (fn (_, (actuals, n)) => | 544 case result of |
545 ((L'.ERel n, loc) :: actuals, | 545 (L'.CApp ((L'.CFfi ("Basis", "transaction"), _), |
546 n + 1)) ([], 0) args | 546 result), _) => (true, result) |
547 val app = (L'.EFfiApp (m, x, actuals), loc) | 547 | _ => (false, result) |
548 | |
549 fun makeApp n = | |
550 let | |
551 val (actuals, _) = foldr (fn (_, (actuals, n)) => | |
552 ((L'.ERel n, loc) :: actuals, | |
553 n + 1)) ([], n) args | |
554 in | |
555 (L'.EFfiApp (m, x, actuals), loc) | |
556 end | |
557 val unit = (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc) | |
558 val (result, app) = | |
559 if isTransaction then | |
560 ((L'.TFun (unit, result), loc), | |
561 (L'.EAbs ("_", | |
562 unit, | |
563 result, | |
564 makeApp 1), loc)) | |
565 else | |
566 (result, makeApp 0) | |
567 | |
548 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => | 568 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => |
549 ((L'.EAbs ("arg" ^ Int.toString n, | 569 ((L'.EAbs ("arg" ^ Int.toString n, |
550 t, | 570 t, |
551 ran, | 571 ran, |
552 abs), loc), | 572 abs), loc), |
732 | 752 |
733 | L.DFfiStr (m, n, (sgn, _)) => | 753 | L.DFfiStr (m, n, (sgn, _)) => |
734 (case sgn of | 754 (case sgn of |
735 L.SgnConst sgis => | 755 L.SgnConst sgis => |
736 let | 756 let |
737 val (ds, cmap, conmap, st) = | 757 val (ds, cmap, conmap, st, _) = |
738 foldl (fn ((sgi, _), (ds, cmap, conmap, st)) => | 758 foldl (fn ((sgi, _), (ds, cmap, conmap, st, trans)) => |
739 case sgi of | 759 case sgi of |
740 L.SgiConAbs (x, n, k) => | 760 L.SgiConAbs (x, n, k) => |
741 let | 761 let |
742 val (st, n') = St.bindCon st x n | 762 val (st, n') = St.bindCon st x n |
763 | |
764 val trans = | |
765 if x = "transaction" then | |
766 SOME n | |
767 else | |
768 trans | |
743 in | 769 in |
744 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, | 770 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, |
745 cmap, | 771 cmap, |
746 conmap, | 772 conmap, |
747 st) | 773 st, |
774 trans) | |
748 end | 775 end |
749 | L.SgiCon (x, n, k, _) => | 776 | L.SgiCon (x, n, k, _) => |
750 let | 777 let |
751 val (st, n') = St.bindCon st x n | 778 val (st, n') = St.bindCon st x n |
752 in | 779 in |
753 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, | 780 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, |
754 cmap, | 781 cmap, |
755 conmap, | 782 conmap, |
756 st) | 783 st, |
784 trans) | |
757 end | 785 end |
758 | 786 |
759 | L.SgiDatatype (x, n, xs, xnts) => | 787 | L.SgiDatatype (x, n, xs, xnts) => |
760 let | 788 let |
761 val k = (L'.KType, loc) | 789 val k = (L'.KType, loc) |
813 end) ([], st, cmap, conmap) xnts | 841 end) ([], st, cmap, conmap) xnts |
814 in | 842 in |
815 (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds, | 843 (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds, |
816 cmap, | 844 cmap, |
817 conmap, | 845 conmap, |
818 st) | 846 st, |
847 trans) | |
819 end | 848 end |
820 | 849 |
821 | L.SgiVal (x, _, c) => | 850 | L.SgiVal (x, _, c) => |
822 (ds, | 851 let |
823 SM.insert (cmap, x, corifyCon st c), | 852 val c = |
824 conmap, | 853 case trans of |
825 st) | 854 NONE => corifyCon st c |
826 | _ => (ds, cmap, conmap, st)) ([], SM.empty, SM.empty, st) sgis | 855 | SOME trans => |
856 let | |
857 fun transactify (all as (c, loc)) = | |
858 case c of | |
859 L.TFun (dom, ran) => | |
860 (L'.TFun (corifyCon st dom, transactify ran), loc) | |
861 | L.CApp ((L.CNamed trans', _), t) => | |
862 if trans' = trans then | |
863 (L'.CApp ((L'.CFfi (m, "transaction"), loc), | |
864 corifyCon st t), loc) | |
865 else | |
866 corifyCon st all | |
867 | _ => corifyCon st all | |
868 in | |
869 transactify c | |
870 end | |
871 in | |
872 (ds, | |
873 SM.insert (cmap, x, c), | |
874 conmap, | |
875 st, | |
876 trans) | |
877 end | |
878 | _ => (ds, cmap, conmap, st, trans)) | |
879 ([], SM.empty, SM.empty, st, NONE) sgis | |
827 | 880 |
828 val st = St.bindStr st m n (St.ffi m cmap conmap) | 881 val st = St.bindStr st m n (St.ffi m cmap conmap) |
829 in | 882 in |
830 (rev ds, St.basisIs (st, n)) | 883 (rev ds, St.basisIs (st, n)) |
831 end | 884 end |