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



open Global
open Pi
open Crypto
open Data
open Prins
open Ws_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 = unit

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

let rec c_cwqRequest : store -> msg1 -> result_c = fun st handlers ->
  let r = receiveWired_c_cwqRequest st in
  match r with
  | Wired_in_c_cwqRequest_of_w_Fault_cwqRequest___ ((), newSt) ->
    let () = assume (Recv_Fault(newSt.vars.c,newSt.header.sid,newSt.header.ts)) in
    let next = handlers.hFault () in
    next
  | Wired_in_c_cwqRequest_of_w_xReply_cwqRequest_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
  | Request(C c, W w, Q q,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Request(c,st.header.sid,ts1,c,w,q)) in
    let newSt = sendWired_Request_c_start c w q st in
    c_cwqRequest 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 msg4 = {
   hRequest : (var_c * var_w * var_q -> msg5)}
and msg5 = 
   Reply of (var_x * result_w)
 | Fault of (result_w)

let rec w_start : store -> msg4 -> result_w = fun st handlers ->
  let r = receiveWired_w_start st in
  match r with
  | Wired_in_w_start_of_c_cwqRequest_cwq__ ((c, w, q), newSt) ->
    let () = assume (Recv_Request(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.c,newSt.vars.w,newSt.vars.q)) in
    let next = handlers.hRequest (C c, W w, Q q) in
    w_cwqRequest newSt next
and w_cwqRequest : store -> msg5 -> result_w = fun st -> function
  | Fault(next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Fault(st.vars.w,st.header.sid,ts1)) in
    let _ = sendWired_Fault_w_cwqRequest st in
    next
  | 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_cwqRequest x st in
    next


let w (host:principal) (user_input:msg4) =
  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