diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-11-06 09:21:34 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-06 09:21:34 -0500 |
| commit | 1841f3b75ec441d16d289cb768526c374f16960a (patch) | |
| tree | ba523b94cf3cd06fdc212a16b0ae735ad2d11aa9 /src/corify.sml | |
| parent | 627c93b9779f632bd8d90e7e2de26a5a9c197f08 (diff) | |
Monoizing FFI transactions correctly
Diffstat (limited to 'src/corify.sml')
| -rw-r--r-- | src/corify.sml | 81 |
1 files changed, 67 insertions, 14 deletions
diff --git a/src/corify.sml b/src/corify.sml index 0ec98c69..8b72f9f8 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -540,11 +540,31 @@ fun corifyExp st (e, loc) = | _ => (all, rev args) val (result, args) = getArgs (t, []) + val (isTransaction, result) = + case result of + (L'.CApp ((L'.CFfi ("Basis", "transaction"), _), + result), _) => (true, result) + | _ => (false, result) - val (actuals, _) = foldr (fn (_, (actuals, n)) => - ((L'.ERel n, loc) :: actuals, - n + 1)) ([], 0) args - val app = (L'.EFfiApp (m, x, actuals), loc) + fun makeApp n = + let + val (actuals, _) = foldr (fn (_, (actuals, n)) => + ((L'.ERel n, loc) :: actuals, + n + 1)) ([], n) args + in + (L'.EFfiApp (m, x, actuals), loc) + end + val unit = (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc) + val (result, app) = + if isTransaction then + ((L'.TFun (unit, result), loc), + (L'.EAbs ("_", + unit, + result, + makeApp 1), loc)) + else + (result, makeApp 0) + val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => ((L'.EAbs ("arg" ^ Int.toString n, t, @@ -734,17 +754,24 @@ fun corifyDecl mods ((d, loc : EM.span), st) = (case sgn of L.SgnConst sgis => let - val (ds, cmap, conmap, st) = - foldl (fn ((sgi, _), (ds, cmap, conmap, st)) => + val (ds, cmap, conmap, st, _) = + foldl (fn ((sgi, _), (ds, cmap, conmap, st, trans)) => case sgi of L.SgiConAbs (x, n, k) => let val (st, n') = St.bindCon st x n + + val trans = + if x = "transaction" then + SOME n + else + trans in ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, cmap, conmap, - st) + st, + trans) end | L.SgiCon (x, n, k, _) => let @@ -753,7 +780,8 @@ fun corifyDecl mods ((d, loc : EM.span), st) = ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, cmap, conmap, - st) + st, + trans) end | L.SgiDatatype (x, n, xs, xnts) => @@ -815,15 +843,40 @@ fun corifyDecl mods ((d, loc : EM.span), st) = (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds, cmap, conmap, - st) + st, + trans) end | L.SgiVal (x, _, c) => - (ds, - SM.insert (cmap, x, corifyCon st c), - conmap, - st) - | _ => (ds, cmap, conmap, st)) ([], SM.empty, SM.empty, st) sgis + let + val c = + case trans of + NONE => corifyCon st c + | SOME trans => + let + fun transactify (all as (c, loc)) = + case c of + L.TFun (dom, ran) => + (L'.TFun (corifyCon st dom, transactify ran), loc) + | L.CApp ((L.CNamed trans', _), t) => + if trans' = trans then + (L'.CApp ((L'.CFfi (m, "transaction"), loc), + corifyCon st t), loc) + else + corifyCon st all + | _ => corifyCon st all + in + transactify c + end + in + (ds, + SM.insert (cmap, x, c), + conmap, + st, + trans) + end + | _ => (ds, cmap, conmap, st, trans)) + ([], SM.empty, SM.empty, st, NONE) sgis val st = St.bindStr st m n (St.ffi m cmap conmap) in |