# HG changeset patch # User Adam Chlipala # Date 1234638476 18000 # Node ID 0dd40b6bfdf30b23721f7049dbc1e4a29ba2cf78 # Parent 5145181b02fa848b2a3df1e2c840c93d956b99ce Start of RPCification diff -r 5145181b02fa -r 0dd40b6bfdf3 demo/crud2.sql --- a/demo/crud2.sql Tue Jan 27 09:53:51 2009 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -CREATE TABLE uw_Crud2_t(uw_id int8 NOT NULL, uw_nam text NOT NULL, - uw_ready bool NOT NULL); - - CREATE SEQUENCE uw_Crud2_Crud_Make_seq; - - \ No newline at end of file diff -r 5145181b02fa -r 0dd40b6bfdf3 src/compiler.sig --- a/src/compiler.sig Tue Jan 27 09:53:51 2009 -0500 +++ b/src/compiler.sig Sat Feb 14 14:07:56 2009 -0500 @@ -66,6 +66,7 @@ val especialize : (Core.file, Core.file) phase val core_untangle : (Core.file, Core.file) phase val shake : (Core.file, Core.file) phase + val rpcify : (Core.file, Core.file) phase val tag : (Core.file, Core.file) phase val reduce : (Core.file, Core.file) phase val unpoly : (Core.file, Core.file) phase @@ -92,6 +93,7 @@ val toEspecialize : (string, Core.file) transform val toCore_untangle : (string, Core.file) transform val toShake1 : (string, Core.file) transform + val toRpcify : (string, Core.file) transform val toTag : (string, Core.file) transform val toReduce : (string, Core.file) transform val toUnpoly : (string, Core.file) transform diff -r 5145181b02fa -r 0dd40b6bfdf3 src/compiler.sml --- a/src/compiler.sml Tue Jan 27 09:53:51 2009 -0500 +++ b/src/compiler.sml Sat Feb 14 14:07:56 2009 -0500 @@ -446,12 +446,19 @@ val toShake1 = transform shake "shake1" o toCore_untangle +val rpcify = { + func = Rpcify.frob, + print = CorePrint.p_file CoreEnv.empty +} + +val toRpcify = transform rpcify "rpcify" o toShake1 + val tag = { func = Tag.tag, print = CorePrint.p_file CoreEnv.empty } -val toTag = transform tag "tag" o toShake1 +val toTag = transform tag "tag" o toRpcify val reduce = { func = Reduce.reduce, diff -r 5145181b02fa -r 0dd40b6bfdf3 src/core.sml --- a/src/core.sml Tue Jan 27 09:53:51 2009 -0500 +++ b/src/core.sml Sat Feb 14 14:07:56 2009 -0500 @@ -106,6 +106,8 @@ | ELet of string * con * exp * exp + | EServerCall of int * exp list * exp + withtype exp = exp' located datatype export_kind = diff -r 5145181b02fa -r 0dd40b6bfdf3 src/core_print.sml --- a/src/core_print.sml Tue Jan 27 09:53:51 2009 -0500 +++ b/src/core_print.sml Sat Feb 14 14:07:56 2009 -0500 @@ -394,6 +394,15 @@ newline, p_exp (E.pushERel env x t) e2] + | EServerCall (n, es, e) => box [string "Server(", + p_enamed env n, + string ",", + space, + p_list (p_exp env) es, + string ")[", + p_exp env e, + string "]"] + and p_exp env = p_exp' false env fun p_named x n = diff -r 5145181b02fa -r 0dd40b6bfdf3 src/core_util.sml --- a/src/core_util.sml Tue Jan 27 09:53:51 2009 -0500 +++ b/src/core_util.sml Sat Feb 14 14:07:56 2009 -0500 @@ -479,6 +479,13 @@ | (ELet (_, _, x1, e1), ELet (_, _, x2, e2)) => join (compare (x1, x2), fn () => compare (e1, e2)) + | (ELet _, _) => LESS + | (_, ELet _) => GREATER + + | (EServerCall (n1, es1, e1), EServerCall (n2, es2, e2)) => + join (Int.compare (n1, n2), + fn () => join (joinL compare (es1, es2), + fn () => compare (e1, e2))) datatype binder = RelC of string * kind @@ -653,6 +660,13 @@ fn e2' => (ELet (x, t', e1', e2'), loc)))) + | EServerCall (n, es, e) => + S.bind2 (ListUtil.mapfold (mfe ctx) es, + fn es' => + S.map2 (mfe ctx e, + fn e' => + (EServerCall (n, es', e'), loc))) + and mfp ctx (pAll as (p, loc)) = case p of PWild => S.return2 pAll diff -r 5145181b02fa -r 0dd40b6bfdf3 src/monoize.sml --- a/src/monoize.sml Tue Jan 27 09:53:51 2009 -0500 +++ b/src/monoize.sml Sat Feb 14 14:07:56 2009 -0500 @@ -2224,6 +2224,8 @@ in ((L'.ELet (x, t', e1, e2), loc), fm) end + + | L.EServerCall _ => raise Fail "Monoize EServerCall" end fun monoDecl (env, fm) (all as (d, loc)) = diff -r 5145181b02fa -r 0dd40b6bfdf3 src/reduce.sml --- a/src/reduce.sml Tue Jan 27 09:53:51 2009 -0500 +++ b/src/reduce.sml Sat Feb 14 14:07:56 2009 -0500 @@ -366,7 +366,9 @@ | EWrite e => (EWrite (exp env e), loc) | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) - | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)) + | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) + + | EServerCall (n, es, e) => (EServerCall (n, map (exp env) es, exp env e), loc)) in {con = con, exp = exp} end diff -r 5145181b02fa -r 0dd40b6bfdf3 src/reduce_local.sml --- a/src/reduce_local.sml Tue Jan 27 09:53:51 2009 -0500 +++ b/src/reduce_local.sml Sat Feb 14 14:07:56 2009 -0500 @@ -131,6 +131,8 @@ | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc) + | EServerCall (n, es, e) => (EServerCall (n, map (exp env) es, exp env e), loc) + fun reduce file = let fun doDecl (d as (_, loc)) = diff -r 5145181b02fa -r 0dd40b6bfdf3 src/rpcify.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/rpcify.sig Sat Feb 14 14:07:56 2009 -0500 @@ -0,0 +1,32 @@ +(* Copyright (c) 2009, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +signature RPCIFY = sig + + val frob : Core.file -> Core.file + +end diff -r 5145181b02fa -r 0dd40b6bfdf3 src/rpcify.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/rpcify.sml Sat Feb 14 14:07:56 2009 -0500 @@ -0,0 +1,149 @@ +(* Copyright (c) 2009, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +structure Rpcify :> RPCIFY = struct + +open Core + +structure U = CoreUtil +structure E = CoreEnv + +structure IS = IntBinarySet +structure IM = IntBinaryMap + +structure SS = BinarySetFn(struct + type ord_key = string + val compare = String.compare + end) + +val ssBasis = SS.addList (SS.empty, + ["requestHeader", + "query", + "dml", + "nextval"]) + +val csBasis = SS.addList (SS.empty, + ["source", + "get", + "set", + "alert"]) + +type state = { + exps : int IM.map, + decls : (string * int * con * exp * string) list +} + +fun frob file = + let + fun sideish (basis, ssids) = + U.Exp.exists {kind = fn _ => false, + con = fn _ => false, + exp = fn ENamed n => IS.member (ssids, n) + | EFfi ("Basis", x) => SS.member (basis, x) + | EFfiApp ("Basis", x, _) => SS.member (basis, x) + | _ => false} + + fun whichIds basis = + let + fun decl ((d, _), ssids) = + let + val impure = sideish (basis, ssids) + in + case d of + DVal (_, n, _, e, _) => if impure e then + IS.add (ssids, n) + else + ssids + | DValRec xes => if List.exists (fn (_, _, _, e, _) => impure e) xes then + foldl (fn ((_, n, _, _, _), ssids) => IS.add (ssids, n)) + ssids xes + else + ssids + | _ => ssids + end + in + foldl decl IS.empty file + end + + val ssids = whichIds ssBasis + val csids = whichIds csBasis + + val serverSide = sideish (ssBasis, ssids) + val clientSide = sideish (csBasis, csids) + + fun exp (e, st) = + case e of + EApp ( + (EApp + ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _), + (EFfi ("Basis", "transaction_monad"), _)), _), + trans1), _), + trans2) => + (case (serverSide trans1, clientSide trans1, serverSide trans2, clientSide trans2) of + (true, false, false, _) => + let + fun getApp (e, args) = + case #1 e of + ENamed n => (n, args) + | EApp (e1, e2) => getApp (e1, e2 :: args) + | _ => (ErrorMsg.errorAt loc "Mixed client/server code doesn't use a named function for server part"; + (0, [])) + + val (n, args) = getApp (trans1, []) + in + (EServerCall (n, args, trans2), st) + end + | _ => (e, st)) + | _ => (e, st) + + fun decl (d, st : state) = + let + val (d, st) = U.Decl.foldMap {kind = fn x => x, + con = fn x => x, + exp = exp, + decl = fn x => x} + st d + in + (case #decls st of + [] => [d] + | ds => + case d of + (DValRec vis, loc) => [(DValRec (ds @ vis), loc)] + | (_, loc) => [(DValRec ds, loc), d], + {decls = [], + exps = #exps st}) + end + + val (file, _) = ListUtil.foldlMapConcat decl + {decls = [], + exps = IM.empty} + file + in + file + end + +end diff -r 5145181b02fa -r 0dd40b6bfdf3 src/shake.sml --- a/src/shake.sml Tue Jan 27 09:53:51 2009 -0500 +++ b/src/shake.sml Sat Feb 14 14:07:56 2009 -0500 @@ -94,26 +94,31 @@ and shakeCon s = U.Con.fold {kind = kind, con = con} s fun exp (e, s) = - case e of - ENamed n => - if IS.member (#exp s, n) then - s - else - let - val s' = {exp = IS.add (#exp s, n), - con = #con s} - in - (*print ("Need " ^ Int.toString n ^ "\n");*) - case IM.find (edef, n) of - NONE => s' - | SOME (ns, t, e) => - let - val s' = shakeExp (shakeCon s' t) e - in - foldl (fn (n, s') => exp (ENamed n, s')) s' ns - end - end - | _ => s + let + fun check n = + if IS.member (#exp s, n) then + s + else + let + val s' = {exp = IS.add (#exp s, n), + con = #con s} + in + (*print ("Need " ^ Int.toString n ^ "\n");*) + case IM.find (edef, n) of + NONE => s' + | SOME (ns, t, e) => + let + val s' = shakeExp (shakeCon s' t) e + in + foldl (fn (n, s') => exp (ENamed n, s')) s' ns + end + end + in + case e of + ENamed n => check n + | EServerCall (n, _, _) => check n + | _ => s + end and shakeExp s = U.Exp.fold {kind = kind, con = con, exp = exp} s diff -r 5145181b02fa -r 0dd40b6bfdf3 src/sources --- a/src/sources Tue Jan 27 09:53:51 2009 -0500 +++ b/src/sources Sat Feb 14 14:07:56 2009 -0500 @@ -108,6 +108,9 @@ defunc.sig defunc.sml +rpcify.sig +rpcify.sml + tag.sig tag.sml diff -r 5145181b02fa -r 0dd40b6bfdf3 tests/rpc.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/rpc.ur Sat Feb 14 14:07:56 2009 -0500 @@ -0,0 +1,13 @@ +sequence s + +fun main () : transaction page = + let + fun getNext () = nextval s + in + s <- source 0; + return +