Mercurial > urweb
view src/rpcify.sml @ 636:de8333ef1a0c
Coq README
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 26 Feb 2009 13:56:54 -0500 |
parents | c5991cdb0c4b |
children | 4a125bbc602d |
line wrap: on
line source
(* 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 = { cpsed : int IM.map, cps_decls : (string * int * con * exp * string) list, exported : IS.set, export_decls : decl 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) val tfuncs = foldl (fn ((d, _), tfuncs) => let fun doOne ((_, n, t, _, _), tfuncs) = let fun crawl (t, args) = case #1 t of CApp ((CFfi ("Basis", "transaction"), _), ran) => SOME (rev args, ran) | TFun (arg, rest) => crawl (rest, arg :: args) | _ => NONE in case crawl (t, []) of NONE => tfuncs | SOME sg => IM.insert (tfuncs, n, sg) end in case d of DVal vi => doOne (vi, tfuncs) | DValRec vis => foldl doOne tfuncs vis | _ => tfuncs end) IM.empty file 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, true) => 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, []) val (exported, export_decls) = if IS.member (#exported st, n) then (#exported st, #export_decls st) else (IS.add (#exported st, n), (DExport (Rpc, n), loc) :: #export_decls st) val st = {cpsed = #cpsed st, cps_decls = #cps_decls st, exported = exported, export_decls = export_decls} val ran = case IM.find (tfuncs, n) of NONE => (Print.prefaces "BAD" [("e", CorePrint.p_exp CoreEnv.empty (e, loc))]; raise Fail "Rpcify: Undetected transaction function") | SOME (_, ran) => ran in (EServerCall (n, args, trans2, ran), 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 (List.revAppend (case #cps_decls st of [] => [d] | ds => case d of (DValRec vis, loc) => [(DValRec (ds @ vis), loc)] | (_, loc) => [d, (DValRec ds, loc)], #export_decls st), {cpsed = #cpsed st, cps_decls = [], exported = #exported st, export_decls = []}) end val (file, _) = ListUtil.foldlMapConcat decl {cpsed = IM.empty, cps_decls = [], exported = IS.empty, export_decls = []} file in file end end