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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/reqheader.ur	Thu Nov 06 09:21:34 2008 -0500
@@ -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>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/reqheader.urp	Thu Nov 06 09:21:34 2008 -0500
@@ -0,0 +1,3 @@
+debug
+
+reqheader