Mercurial > urweb

comparison src/corify.sml @ 456:1a4fa157fedd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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