adam@1848: (* Copyright (c) 2009, 2012-2013, Adam Chlipala
adamc@607:  * All rights reserved.
adamc@607:  *
adamc@607:  * Redistribution and use in source and binary forms, with or without
adamc@607:  * modification, are permitted provided that the following conditions are met:
adamc@607:  *
adamc@607:  * - Redistributions of source code must retain the above copyright notice,
adamc@607:  *   this list of conditions and the following disclaimer.
adamc@607:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@607:  *   this list of conditions and the following disclaimer in the documentation
adamc@607:  *   and/or other materials provided with the distribution.
adamc@607:  * - The names of contributors may not be used to endorse or promote products
adamc@607:  *   derived from this software without specific prior written permission.
adamc@607:  *
adamc@607:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@607:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@607:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@607:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@607:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@607:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@607:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@607:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@607:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@607:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@607:  * POSSIBILITY OF SUCH DAMAGE.
adamc@607:  *)
adamc@607: 
adamc@607: structure Rpcify :> RPCIFY = struct
adamc@607: 
adamc@607: open Core
adamc@607: 
adamc@607: structure U = CoreUtil
adamc@607: structure E = CoreEnv
adamc@607: 
adamc@607: structure IS = IntBinarySet
adamc@607: structure IM = IntBinaryMap
adamc@607: 
adamc@607: type state = {
adamc@608:      exported : IS.set,
adamc@957:      export_decls : decl list
adamc@607: }
adamc@607: 
adamc@607: fun frob file =
adamc@607:     let
adam@1848:         val (rpcBaseIds, trpcBaseIds) =
adam@1848:             foldl (fn ((d, _), (rpcIds, trpcIds)) =>
adam@1848:                       case d of
adam@1848:                           DVal (_, n, _, (EFfi ("Basis", "rpc"), _), _) =>
adam@1848:                           (IS.add (rpcIds, n), trpcIds)
adam@1848:                         | DVal (_, n, _, (EFfi ("Basis", "tryRpc"), _), _) =>
adam@1848:                           (rpcIds, IS.add (trpcIds, n))
adam@1848:                         | DVal (_, n, _, (ENamed n', _), _) =>
adam@1848:                           if IS.member (rpcIds, n') then
adam@1848:                               (IS.add (rpcIds, n), trpcIds)
adam@1848:                           else if IS.member (trpcIds, n') then
adam@1848:                               (rpcIds, IS.add (trpcIds, n))
adam@1848:                           else
adam@1848:                               (rpcIds, trpcIds)
adam@1848:                         | _ => (rpcIds, trpcIds))
adam@1848:                   (IS.empty, IS.empty) file
adamc@607: 
adamc@609:         val tfuncs = foldl
adamc@609:                      (fn ((d, _), tfuncs) =>
adamc@609:                          let
adamc@642:                              fun doOne ((x, n, t, e, _), tfuncs) =
adamc@609:                                  let
adamc@642:                                      val loc = #2 e
adamc@642: 
adamc@642:                                      fun crawl (t, e, args) =
adamc@642:                                          case (#1 t, #1 e) of
adamc@642:                                              (CApp (_, ran), _) =>
adamc@642:                                              SOME (x, rev args, ran, e)
adamc@642:                                            | (TFun (arg, rest), EAbs (x, _, _, e)) =>
adamc@642:                                              crawl (rest, e, (x, arg) :: args)
adamc@642:                                            | (TFun (arg, rest), _) =>
adamc@642:                                              crawl (rest, (EApp (e, (ERel (length args), loc)), loc), ("x", arg) :: args)
adamc@609:                                            | _ => NONE
adamc@609:                                  in
adamc@642:                                      case crawl (t, e, []) of
adamc@609:                                          NONE => tfuncs
adamc@609:                                        | SOME sg => IM.insert (tfuncs, n, sg)
adamc@609:                                  end
adamc@609:                          in
adamc@609:                              case d of
adamc@609:                                  DVal vi => doOne (vi, tfuncs)
adamc@609:                                | DValRec vis => foldl doOne tfuncs vis
adamc@609:                                | _ => tfuncs
adamc@609:                          end)
adamc@609:                      IM.empty file
adamc@609:                              
adamc@607:         fun exp (e, st) =
adamc@649:             let
adamc@649:                 fun getApp (e', args) =
adamc@908:                     case e' of
adamc@908:                         ENamed n => SOME (n, args)
adamc@908:                       | EApp (e1, e2) => getApp (#1 e1, e2 :: args)
adamc@908:                       | _ => NONE
adamc@642: 
adam@1848:                 fun newRpc (trans : exp, st : state, fm) =
adamc@908:                     case getApp (#1 trans, []) of
adamc@908:                         NONE => (ErrorMsg.errorAt (#2 trans)
adamc@908:                                                   "RPC code doesn't use a named function or transaction";
adam@1677:                                  (*Print.preface ("Expression",
adam@1677:                                                 CorePrint.p_exp CoreEnv.empty trans);*)
adamc@908:                                  (#1 trans, st))
adamc@908:                       | SOME (n, args) =>
adamc@908:                         case IM.find (tfuncs, n) of
adamc@908:                             NONE => ((*Print.prefaces "BAD" [("e", CorePrint.p_exp CoreEnv.empty (e, loc))];*)
adamc@908:                                      raise Fail ("Rpcify: Undetected transaction function " ^ Int.toString n))
adamc@908:                           | SOME (_, _, ran, _) =>
adamc@908:                             let
adamc@908:                                 val loc = #2 trans
adamc@642: 
adamc@908:                                 val (exported, export_decls) =
adamc@908:                                     if IS.member (#exported st, n) then
adamc@908:                                         (#exported st, #export_decls st)
adamc@908:                                     else
adamc@908:                                         (IS.add (#exported st, n),
adamc@1104:                                          (DExport (Rpc ReadWrite, n, false), loc) :: #export_decls st)
adamc@642: 
adamc@908:                                 val st = {exported = exported,
adamc@957:                                           export_decls = export_decls}
adamc@642: 
adam@1848:                                 val e' = EServerCall (n, args, ran, fm)
adamc@651:                             in
adamc@908:                                 (e', st)
adamc@651:                             end
adamc@649:             in
adamc@649:                 case e of
adam@1848:                     EApp ((ECApp ((EFfi ("Basis", "rpc"), _), ran), _), trans) => newRpc (trans, st, None)
adam@1848:                   | EApp ((ECApp ((EFfi ("Basis", "tryRpc"), _), ran), _), trans) => newRpc (trans, st, Error)
adamc@908:                   | EApp ((ECApp ((ENamed n, _), ran), _), trans) =>
adamc@908:                     if IS.member (rpcBaseIds, n) then
adam@1848:                         newRpc (trans, st, None)
adam@1848:                     else if IS.member (trpcBaseIds, n) then
adam@1848:                         newRpc (trans, st, Error)
adamc@908:                     else
adamc@908:                         (e, st)
adamc@642: 
adamc@649:                   | _ => (e, st)
adamc@649:             end
adamc@607: 
adamc@642:         and doExp (e, st) = U.Exp.foldMap {kind = fn x => x,
adamc@642:                                            con = fn x => x,
adamc@642:                                            exp = exp} st (ReduceLocal.reduceExp e)
adamc@642: 
adamc@607:         fun decl (d, st : state) =
adamc@607:             let
adamc@607:                 val (d, st) = U.Decl.foldMap {kind = fn x => x,
adamc@607:                                               con = fn x => x,
adamc@607:                                               exp = exp,
adamc@607:                                               decl = fn x => x}
adamc@607:                               st d
adamc@607:             in
adam@1695:                 (d :: #export_decls st,
adamc@908:                  {exported = #exported st,
adamc@957:                   export_decls = []})
adamc@607:             end
adamc@607: 
adamc@607:         val (file, _) = ListUtil.foldlMapConcat decl
adamc@908:                         {exported = IS.empty,
adamc@957:                          export_decls = []}
adamc@607:                         file
adamc@607:     in
adamc@607:         file
adamc@607:     end
adamc@607: 
adamc@607: end