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



open Global
open Pi
open Crypto
open Data
open Prins
open Fwd_protocol

let debug_impl = debug "impl"

type var_c = C of principal
type var_w = W of principal
type var_r = R of principal
type var_q = Q of int

(* Proxy function for c *)

type result_c = string

type msg0 = 
   Commit of (var_q * var_c * var_w * var_r * result_c)

let rec c_start : store -> msg0 -> result_c = fun st -> function
  | Commit(Q q, C c, W w, R r,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Commit(c,st.header.sid,ts1,q,c,w,r)) in
    let _ = sendWired_Commit_c_start q c w r st in
    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 msg2 = {
   hCommit : (var_q * var_c * var_w * var_r -> msg3)}
and msg3 = 
   Fwd of (result_w)

let rec w_start : store -> msg2 -> result_w = fun st handlers ->
  let r = receiveWired_w_start st in
  match r with
  | Wired_in_w_start_of_c_qcwrCommit_qcwr__ ((q, c, w, r), newSt) ->
    let () = assume (Recv_Commit(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.q,newSt.vars.c,newSt.vars.w,newSt.vars.r)) in
    let next = handlers.hCommit (Q q, C c, W w, R r) in
    w_qcwrCommit newSt next
and w_qcwrCommit : store -> msg3 -> result_w = fun st -> function
  | Fwd(next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Fwd(st.vars.w,st.header.sid,ts1)) in
    let _ = sendWired_Fwd_w_qcwrCommit st in
    next


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

(* Proxy function for r *)

type result_r = string

type msg5 = {
   hFwd : (var_q * var_c * var_w * var_r -> result_r)}

let rec r_start : store -> msg5 -> result_r = fun st handlers ->
  let r = receiveWired_r_start st in
  match r with
  | Wired_in_r_start_of_w_Fwd_qcwrCommit___c_qcwrCommit_qcwr__ ((q, c, w, r), newSt) ->
    let () = assume (Recv_Fwd(newSt.vars.r,newSt.header.sid,newSt.header.ts,newSt.vars.q,newSt.vars.c,newSt.vars.w,newSt.vars.r)) in
    let next = handlers.hFwd (Q q, C c, W w, R r) in
    next


let r (host:principal) (user_input:msg5) =
  let empty_store = empty_store_r host false in
  let () = bind host in
  debug_impl ("Executing role r ...");
  let result = r_start empty_store user_input in (*close();*)
  result