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



open Global
open Pi
open Crypto
open Data
open Prins
open Commit_protocol

let debug_impl = debug "impl"

type var_c = C of principal
type var_w = W 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 * msg1)
and msg1 = {
   hAck : (unit -> msg2)}
and msg2 = 
   Reveal of (result_c)

let rec c_qcwCommit : store -> msg1 -> result_c = fun st handlers ->
  let r = receiveWired_c_qcwCommit st in
  match r with
  | Wired_in_c_qcwCommit_of_w_Ack_qcwCommit___ ((), newSt) ->
    let () = assume (Recv_Ack(newSt.vars.c,newSt.header.sid,newSt.header.ts)) in
    let next = handlers.hAck () in
    c_Ack_qcwCommit newSt next
and c_Ack_qcwCommit : store -> msg2 -> result_c = fun st -> function
  | Reveal(next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Reveal(st.vars.c,st.header.sid,ts1)) in
    let _ = sendWired_Reveal_c_Ack_qcwCommit st in
    next
and c_start : store -> msg0 -> result_c = fun st -> function
  | Commit(Q q, C c, W w,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Commit(c,st.header.sid,ts1,q,c,w)) in
    let newSt = sendWired_Commit_c_start q c w st in
    c_qcwCommit 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 = {
   hCommit : (var_c * var_w -> msg5)}
and msg5 = 
   Ack of (msg6)
and msg6 = {
   hReveal : (var_q -> result_w)}

let rec w_Ack_qcwCommit : store -> msg6 -> result_w = fun st handlers ->
  let r = receiveWired_w_Ack_qcwCommit st in
  match r with
  | Wired_in_w_Ack_qcwCommit_of_c_Reveal_qcwAck___ ((q), newSt) ->
    let () = assume (Recv_Reveal(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.q)) in
    let next = handlers.hReveal (Q q) in
    next
and 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_qcwCommit_qcw__ ((c, w), newSt) ->
    let () = assume (Recv_Commit(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.c,newSt.vars.w)) in
    let next = handlers.hCommit (C c, W w) in
    w_qcwCommit newSt next
and w_qcwCommit : store -> msg5 -> result_w = fun st -> function
  | Ack(next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Ack(st.vars.w,st.header.sid,ts1)) in
    let newSt = sendWired_Ack_w_qcwCommit st in
    w_Ack_qcwCommit newSt 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