(*******************)
(* Proxy functions *)
(*******************)



open Global
open Pi
open Crypto
open Data
open Prins
open Rpc_protocol

let debug_impl = debug "impl"

type var_c = C of principal
type var_w = W of principal
type var_q = Q of string
type var_x = X of int

(* Proxy function for c *)

type result_c = string

type msg0 = 
   Query of (var_q * var_c * var_w * msg1)
and msg1 = {
   hReply : (var_x -> result_c)}

let rec c_qcwQuery : store -> msg1 -> result_c = fun st handlers ->
  let r = receiveWired_c_qcwQuery st in
  match r with
  | Wired_in_c_qcwQuery_of_w_xReply_qcwQuery_x__ ((x), newSt) ->
    let () = assume (Recv_Reply(newSt.vars.c,newSt.header.sid,newSt.header.ts,newSt.vars.x)) in
    let next = handlers.hReply (X x) in
    next
and c_start : store -> msg0 -> result_c = fun st -> function
  | Query(Q q, C c, W w,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Query(c,st.header.sid,ts1,q,c,w)) in
    let newSt = sendWired_Query_c_start q c w st in
    c_qcwQuery newSt next


let c (host:principal) (user_input:msg0) =
  let empty_store = empty_store_c host true in
  let () = bind host in
  debug_impl ("Executing role c ...");
  let result = c_start empty_store user_input in (*close();*)
  result

(* Proxy function for w *)

type result_w = string

type msg3 = {
   hQuery : (var_q * var_c * var_w -> msg4)}
and msg4 = 
   Reply of (var_x * result_w)

let rec w_start : store -> msg3 -> result_w = fun st handlers ->
  let r = receiveWired_w_start st in
  match r with
  | Wired_in_w_start_of_c_qcwQuery_qcw__ ((q, c, w), newSt) ->
    let () = assume (Recv_Query(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.q,newSt.vars.c,newSt.vars.w)) in
    let next = handlers.hQuery (Q q, C c, W w) in
    w_qcwQuery newSt next
and w_qcwQuery : store -> msg4 -> result_w = fun st -> function
  | Reply(X x,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Reply(st.vars.w,st.header.sid,ts1,x)) in
    let _ = sendWired_Reply_w_qcwQuery x st in
    next


let w (host:principal) (user_input:msg3) =
  let empty_store = empty_store_w host false in
  let () = bind host in
  debug_impl ("Executing role w ...");
  let result = w_start empty_store user_input in (*close();*)
  result