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 | |
parent | 627c93b9779f632bd8d90e7e2de26a5a9c197f08 (diff) |
Monoizing FFI transactions correctly
-rw-r--r-- | lib/basis.urs | 23 | ||||
-rw-r--r-- | src/corify.sml | 81 | ||||
-rw-r--r-- | src/mono_reduce.sml | 11 | ||||
-rw-r--r-- | tests/reqheader.ur | 5 | ||||
-rw-r--r-- | tests/reqheader.urp | 3 |
5 files changed, 99 insertions, 24 deletions
diff --git a/lib/basis.urs b/lib/basis.urs index ca81c95f..806a9623 100644 --- a/lib/basis.urs +++ b/lib/basis.urs @@ -69,6 +69,22 @@ val read_bool : read bool 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 @@ val sql_current_timestamp : sql_nfunc time (*** 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 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 diff --git a/src/mono_reduce.sml b/src/mono_reduce.sml index 07c7c5f5..57a9cc6d 100644 --- a/src/mono_reduce.sml +++ b/src/mono_reduce.sml @@ -352,10 +352,15 @@ fun exp env e = | 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 diff --git a/tests/reqheader.ur b/tests/reqheader.ur new file mode 100644 index 00000000..8b69cc3a --- /dev/null +++ b/tests/reqheader.ur @@ -0,0 +1,5 @@ +fun main () : transaction page = + ua <- requestHeader "UserAgent"; + case ua of + None => return <xml>Not found</xml> + | Some s => return <xml>UserAgent: {[s]}</xml> diff --git a/tests/reqheader.urp b/tests/reqheader.urp new file mode 100644 index 00000000..4541390f --- /dev/null +++ b/tests/reqheader.urp @@ -0,0 +1,3 @@ +debug + +reqheader |