Mercurial > urweb
changeset 456:1a4fa157fedd
Monoizing FFI transactions correctly
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 06 Nov 2008 09:21:34 -0500 |
| parents | d4a81273d4b1 |
| children | 360cbc202756 |
| files | lib/basis.urs src/corify.sml src/mono_reduce.sml tests/reqheader.ur tests/reqheader.urp |
| diffstat | 5 files changed, 99 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/basis.urs Tue Nov 04 09:33:35 2008 -0500 +++ b/lib/basis.urs Thu Nov 06 09:21:34 2008 -0500 @@ -69,6 +69,22 @@ val read_time : read time +(** * Transactions *) + +con transaction :: Type -> Type + +val return : t ::: Type + -> t -> transaction t +val bind : t1 ::: Type -> t2 ::: Type + -> transaction t1 -> (t1 -> transaction t2) + -> transaction t2 + + +(** HTTP operations *) + +val requestHeader : string -> transaction (option string) + + (** SQL *) con sql_table :: {Type} -> Type @@ -233,13 +249,6 @@ (*** Executing queries *) -con transaction :: Type -> Type -val return : t ::: Type - -> t -> transaction t -val bind : t1 ::: Type -> t2 ::: Type - -> transaction t1 -> (t1 -> transaction t2) - -> transaction t2 - val query : tables ::: {{Type}} -> exps ::: {Type} -> fn [tables ~ exps] => state ::: Type
--- a/src/corify.sml Tue Nov 04 09:33:35 2008 -0500 +++ b/src/corify.sml Thu Nov 06 09:21:34 2008 -0500 @@ -540,11 +540,31 @@ | _ => (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 @@ (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 @@ ((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 @@ (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
--- a/src/mono_reduce.sml Tue Nov 04 09:33:35 2008 -0500 +++ b/src/mono_reduce.sml Thu Nov 06 09:21:34 2008 -0500 @@ -352,10 +352,15 @@ | ELet (x, t, e', b) => let + fun doSub () = #1 (reduceExp env (subExpInExp (0, e') b)) + fun trySub () = - case e' of - (ECase _, _) => e - | _ => #1 (reduceExp env (subExpInExp (0, e') b)) + case t of + (TFfi ("Basis", "string"), _) => doSub () + | _ => + case e' of + (ECase _, _) => e + | _ => doSub () in if impure e' then let