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



open Global
open Pi
open Crypto
open Data
open Prins
open Proxy_protocol

let debug_impl = debug "impl"

type var_c = C of principal
type var_p = P of principal
type var_w = W of principal
type var_q = Q of string
type var_x = X of string
type var_d = D of string
type var_o = O of string

(* Proxy function for c *)

type result_c = string

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

let rec c_cpwqRequest : store -> msg1 -> result_c = fun st handlers ->
  let r = receiveWired_c_cpwqRequest st in
  match r with
  | Wired_in_c_cpwqRequest_of_w_xReply_dResume_cpwqRequest_x__p_Resume_dDetails_cpwqRequest_d__ ((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
  | Wired_in_c_cpwqRequest_of_w_xReply_odResume_cpwqRequest_x__p_Resume_odDetails_cpwqRequest_od__ ((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
  | Wired_in_c_cpwqRequest_of_w_xReply_Forward_cpwqRequest_x__p_Forward_cpwqRequest___ ((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, P p, W w, Q q,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Request(c,st.header.sid,ts1,c,p,w,q)) in
    let newSt = sendWired_Request_c_start c p w q st in
    c_cpwqRequest 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 p *)

type result_p = string

type msg3 = {
   hRequest : (var_c * var_p * var_w * var_q -> msg4)}
and msg4 = 
   Forward of (result_p)
 | Audit of (msg6)
and msg6 = {
   hDetails : (var_d -> msg7)}
and msg7 = 
   Retry of (var_o * msg6)
 | Resume of (result_p)

let rec p_oRetry_dDetails_cpwqRequest : store -> msg6 -> result_p = fun st handlers ->
  let r = receiveWired_p_oRetry_dDetails_cpwqRequest st in
  match r with
  | Wired_in_p_oRetry_dDetails_cpwqRequest_of_w_dDetails_oRetry_cpwqRequest_d__ ((d), newSt) ->
    let () = assume (Recv_Details(newSt.vars.p,newSt.header.sid,newSt.header.ts,newSt.vars.d)) in
    let next = handlers.hDetails (D d) in
    p_dDetails_oRetry_cpwqRequest newSt next
and p_Audit_cpwqRequest : store -> msg6 -> result_p = fun st handlers ->
  let r = receiveWired_p_Audit_cpwqRequest st in
  match r with
  | Wired_in_p_Audit_cpwqRequest_of_w_dDetails_Audit_cpwqRequest_d__ ((d), newSt) ->
    let () = assume (Recv_Details(newSt.vars.p,newSt.header.sid,newSt.header.ts,newSt.vars.d)) in
    let next = handlers.hDetails (D d) in
    p_dDetails_Audit_cpwqRequest newSt next
and p_start : store -> msg3 -> result_p = fun st handlers ->
  let r = receiveWired_p_start st in
  match r with
  | Wired_in_p_start_of_c_cpwqRequest_cpwq__ ((c, p, w, q), newSt) ->
    let () = assume (Recv_Request(newSt.vars.p,newSt.header.sid,newSt.header.ts,newSt.vars.c,newSt.vars.p,newSt.vars.w,newSt.vars.q)) in
    let next = handlers.hRequest (C c, P p, W w, Q q) in
    p_cpwqRequest newSt next
and p_cpwqRequest : store -> msg4 -> result_p = fun st -> function
  | Audit(next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Audit(st.vars.p,st.header.sid,ts1)) in
    let newSt = sendWired_Audit_p_cpwqRequest st in
    p_Audit_cpwqRequest newSt next
  | Forward(next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Forward(st.vars.p,st.header.sid,ts1)) in
    let _ = sendWired_Forward_p_cpwqRequest st in
    next
and p_dDetails_oRetry_cpwqRequest : store -> msg7 -> result_p = fun st -> function
  | Resume(next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Resume(st.vars.p,st.header.sid,ts1)) in
    let _ = sendWired_Resume_p_dDetails_oRetry_cpwqRequest st in
    next
  | Retry(O o,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Retry(st.vars.p,st.header.sid,ts1,o)) in
    let newSt = sendWired_Retry_p_dDetails_oRetry_cpwqRequest o st in
    p_oRetry_dDetails_cpwqRequest newSt next
and p_dDetails_Audit_cpwqRequest : store -> msg7 -> result_p = fun st -> function
  | Resume(next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Resume(st.vars.p,st.header.sid,ts1)) in
    let _ = sendWired_Resume_p_dDetails_Audit_cpwqRequest st in
    next
  | Retry(O o,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Retry(st.vars.p,st.header.sid,ts1,o)) in
    let newSt = sendWired_Retry_p_dDetails_Audit_cpwqRequest o st in
    p_oRetry_dDetails_cpwqRequest newSt next


let p (host:principal) (user_input:msg3) =
  let empty_store = empty_store_p host false in
  let () = bind host in
  debug_impl ("Executing role p ...");
  let result = p_start empty_store user_input in (*close();*)
  result

(* Proxy function for w *)

type result_w = string

type msg9 = {
   hForward : (var_c * var_p * var_w * var_q -> msg10) ;
   hAudit : (var_c * var_p * var_w -> msg12)}
and msg10 = 
   Reply of (var_x * result_w)
and msg12 = 
   Details of (var_d * msg13)
and msg13 = {
   hRetry : (var_o -> msg12) ;
   hResume : (var_q -> msg10)}

let rec w_start : store -> msg9 -> result_w = fun st handlers ->
  let r = receiveWired_w_start st in
  match r with
  | Wired_in_w_start_of_p_Audit_cpwqRequest___c_cpwqRequest_cpwq__ ((c, p, w), newSt) ->
    let () = assume (Recv_Audit(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.c,newSt.vars.p,newSt.vars.w)) in
    let next = handlers.hAudit (C c, P p, W w) in
    w_Audit_cpwqRequest newSt next
  | Wired_in_w_start_of_p_Forward_cpwqRequest___c_cpwqRequest_cpwq__ ((c, p, w, q), newSt) ->
    let () = assume (Recv_Forward(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.c,newSt.vars.p,newSt.vars.w,newSt.vars.q)) in
    let next = handlers.hForward (C c, P p, W w, Q q) in
    w_Forward_cpwqRequest newSt next
and w_dDetails_oRetry_cpwqRequest : store -> msg13 -> result_w = fun st handlers ->
  let r = receiveWired_w_dDetails_oRetry_cpwqRequest st in
  match r with
  | Wired_in_w_dDetails_oRetry_cpwqRequest_of_p_Resume_odDetails_cpwqRequest___ ((q), newSt) ->
    let () = assume (Recv_Resume(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.q)) in
    let next = handlers.hResume (Q q) in
    w_Resume_odDetails_cpwqRequest newSt next
  | Wired_in_w_dDetails_oRetry_cpwqRequest_of_p_oRetry_dDetails_cpwqRequest_o__ ((o), newSt) ->
    let () = assume (Recv_Retry(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.o)) in
    let next = handlers.hRetry (O o) in
    w_oRetry_dDetails_cpwqRequest newSt next
and w_dDetails_Audit_cpwqRequest : store -> msg13 -> result_w = fun st handlers ->
  let r = receiveWired_w_dDetails_Audit_cpwqRequest st in
  match r with
  | Wired_in_w_dDetails_Audit_cpwqRequest_of_p_Resume_dDetails_cpwqRequest___ ((q), newSt) ->
    let () = assume (Recv_Resume(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.q)) in
    let next = handlers.hResume (Q q) in
    w_Resume_dDetails_cpwqRequest newSt next
  | Wired_in_w_dDetails_Audit_cpwqRequest_of_p_oRetry_dDetails_cpwqRequest_o__ ((o), newSt) ->
    let () = assume (Recv_Retry(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.o)) in
    let next = handlers.hRetry (O o) in
    w_oRetry_dDetails_cpwqRequest newSt next
and w_Forward_cpwqRequest : store -> msg10 -> 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_Forward_cpwqRequest x st in
    next
and w_Resume_odDetails_cpwqRequest : store -> msg10 -> 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_Resume_odDetails_cpwqRequest x st in
    next
and w_oRetry_dDetails_cpwqRequest : store -> msg12 -> result_w = fun st -> function
  | Details(D d,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Details(st.vars.w,st.header.sid,ts1,d)) in
    let newSt = sendWired_Details_w_oRetry_dDetails_cpwqRequest d st in
    w_dDetails_oRetry_cpwqRequest newSt next
and w_Resume_dDetails_cpwqRequest : store -> msg10 -> 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_Resume_dDetails_cpwqRequest x st in
    next
and w_Audit_cpwqRequest : store -> msg12 -> result_w = fun st -> function
  | Details(D d,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Details(st.vars.w,st.header.sid,ts1,d)) in
    let newSt = sendWired_Details_w_Audit_cpwqRequest d st in
    w_dDetails_Audit_cpwqRequest newSt next


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