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



open Global
open Pi
open Crypto
open Data
open Prins
open Login_protocol

let debug_impl = debug "impl"

type var_c = C of principal
type var_w = W of principal
type var_p = P of principal
type var_d = D of principal
type var_q = Q of string
type var_r = R of int

(* Proxy function for c *)

type result_c = string

type msg0 = 
   Login of (var_c * var_p * var_d * var_q * msg1)
and msg1 = {
   hRedirect : (var_w -> msg2) ;
   hBasicreply : (var_r -> result_c)}
and msg2 = 
   Request of (var_q * msg3)
and msg3 = {
   hReply : (var_r -> msg4) ;
   hFault : (unit -> result_c)}
and msg4 = 
   Extra of (var_q * msg3)

let rec c_qExtra_rReply_cpdwRedirect : store -> msg3 -> result_c = fun st handlers ->
  let r = receiveWired_c_qExtra_rReply_cpdwRedirect st in
  match r with
  | Wired_in_c_qExtra_rReply_cpdwRedirect_of_w_rReply_qExtra_cpdwRedirect_r__ ((r), newSt) ->
    let () = assume (Recv_Reply(newSt.vars.c,newSt.header.sid,newSt.header.ts,newSt.vars.r)) in
    let next = handlers.hReply (R r) in
    c_rReply_qExtra_cpdwRedirect newSt next
  | Wired_in_c_qExtra_rReply_cpdwRedirect_of_w_Fault_rqExtra_cpdwRedirect___ ((), newSt) ->
    let () = assume (Recv_Fault(newSt.vars.c,newSt.header.sid,newSt.header.ts)) in
    let next = handlers.hFault () in
    next
and c_qRequest_cpdwRedirect : store -> msg3 -> result_c = fun st handlers ->
  let r = receiveWired_c_qRequest_cpdwRedirect st in
  match r with
  | Wired_in_c_qRequest_cpdwRedirect_of_w_Fault_qRequest_cpdwRedirect___ ((), newSt) ->
    let () = assume (Recv_Fault(newSt.vars.c,newSt.header.sid,newSt.header.ts)) in
    let next = handlers.hFault () in
    next
  | Wired_in_c_qRequest_cpdwRedirect_of_w_rReply_qRequest_cpdwRedirect_r__ ((r), newSt) ->
    let () = assume (Recv_Reply(newSt.vars.c,newSt.header.sid,newSt.header.ts,newSt.vars.r)) in
    let next = handlers.hReply (R r) in
    c_rReply_qRequest_cpdwRedirect newSt next
and c_cpdqLogin : store -> msg1 -> result_c = fun st handlers ->
  let r = receiveWired_c_cpdqLogin st in
  match r with
  | Wired_in_c_cpdqLogin_of_d_rBasicreply_Reject_cpdqLogin_r__p_Reject_cpdqLogin___ ((r), newSt) ->
    let () = assume (Recv_Basicreply(newSt.vars.c,newSt.header.sid,newSt.header.ts,newSt.vars.r)) in
    let next = handlers.hBasicreply (R r) in
    next
  | Wired_in_c_cpdqLogin_of_p_wRedirect_cpdqLogin_w__ ((w), newSt) ->
    let () = assume (Recv_Redirect(newSt.vars.c,newSt.header.sid,newSt.header.ts,newSt.vars.w)) in
    let next = handlers.hRedirect (W w) in
    c_wRedirect_cpdqLogin newSt next
and c_rReply_qExtra_cpdwRedirect : store -> msg4 -> result_c = fun st -> function
  | Extra(Q q,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Extra(st.vars.c,st.header.sid,ts1,q)) in
    let newSt = sendWired_Extra_c_rReply_qExtra_cpdwRedirect q st in
    c_qExtra_rReply_cpdwRedirect newSt next
and c_rReply_qRequest_cpdwRedirect : store -> msg4 -> result_c = fun st -> function
  | Extra(Q q,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Extra(st.vars.c,st.header.sid,ts1,q)) in
    let newSt = sendWired_Extra_c_rReply_qRequest_cpdwRedirect q st in
    c_qExtra_rReply_cpdwRedirect newSt next
and c_wRedirect_cpdqLogin : store -> msg2 -> result_c = fun st -> function
  | Request(Q q,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Request(st.vars.c,st.header.sid,ts1,q)) in
    let newSt = sendWired_Request_c_wRedirect_cpdqLogin q st in
    c_qRequest_cpdwRedirect newSt next
and c_start : store -> msg0 -> result_c = fun st -> function
  | Login(C c, P p, D d, Q q,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Login(c,st.header.sid,ts1,c,p,d,q)) in
    let newSt = sendWired_Login_c_start c p d q st in
    c_cpdqLogin 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 msg7 = {
   hRequest : (var_c * var_p * var_w * var_q -> msg8)}
and msg8 = 
   Reply of (var_r * msg9)
 | Fault of (result_w)
and msg9 = {
   hExtra : (var_q -> msg8)}

let rec w_rReply_qExtra_cpdwRedirect : store -> msg9 -> result_w = fun st handlers ->
  let r = receiveWired_w_rReply_qExtra_cpdwRedirect st in
  match r with
  | Wired_in_w_rReply_qExtra_cpdwRedirect_of_c_qExtra_rReply_cpdwRedirect_q__ ((q), newSt) ->
    let () = assume (Recv_Extra(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.q)) in
    let next = handlers.hExtra (Q q) in
    w_qExtra_rReply_cpdwRedirect newSt next
and w_rReply_qRequest_cpdwRedirect : store -> msg9 -> result_w = fun st handlers ->
  let r = receiveWired_w_rReply_qRequest_cpdwRedirect st in
  match r with
  | Wired_in_w_rReply_qRequest_cpdwRedirect_of_c_qExtra_rReply_cpdwRedirect_q__ ((q), newSt) ->
    let () = assume (Recv_Extra(newSt.vars.w,newSt.header.sid,newSt.header.ts,newSt.vars.q)) in
    let next = handlers.hExtra (Q q) in
    w_qExtra_rReply_cpdwRedirect newSt next
and w_start : store -> msg7 -> result_w = fun st handlers ->
  let r = receiveWired_w_start st in
  match r with
  | Wired_in_w_start_of_c_qRequest_cpdwRedirect_q__p_wRedirect_cpdqLogin_cpdw__ ((c, p, w, q), newSt) ->
    let () = assume (Recv_Request(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.hRequest (C c, P p, W w, Q q) in
    w_qRequest_cpdwRedirect newSt next
and w_qExtra_rReply_cpdwRedirect : store -> msg8 -> result_w = fun st -> function
  | Reply(R r,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Reply(st.vars.w,st.header.sid,ts1,r)) in
    let newSt = sendWired_Reply_w_qExtra_rReply_cpdwRedirect r st in
    w_rReply_qExtra_cpdwRedirect newSt next
  | 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_qExtra_rReply_cpdwRedirect st in
    next
and w_qRequest_cpdwRedirect : store -> msg8 -> 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_qRequest_cpdwRedirect st in
    next
  | Reply(R r,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Reply(st.vars.w,st.header.sid,ts1,r)) in
    let newSt = sendWired_Reply_w_qRequest_cpdwRedirect r st in
    w_rReply_qRequest_cpdwRedirect newSt next


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

type result_p = string

type msg11 = {
   hLogin : (var_p * var_d * var_c * var_q -> msg12)}
and msg12 = 
   Redirect of (var_w * result_p)
 | Reject of (result_p)

let rec p_start : store -> msg11 -> result_p = fun st handlers ->
  let r = receiveWired_p_start st in
  match r with
  | Wired_in_p_start_of_c_cpdqLogin_cpdq__ ((p, d, c, q), newSt) ->
    let () = assume (Recv_Login(newSt.vars.p,newSt.header.sid,newSt.header.ts,newSt.vars.p,newSt.vars.d,newSt.vars.c,newSt.vars.q)) in
    let next = handlers.hLogin (P p, D d, C c, Q q) in
    p_cpdqLogin newSt next
and p_cpdqLogin : store -> msg12 -> result_p = fun st -> function
  | Reject(next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Reject(st.vars.p,st.header.sid,ts1)) in
    let _ = sendWired_Reject_p_cpdqLogin st in
    next
  | Redirect(W w,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Redirect(st.vars.p,st.header.sid,ts1,w)) in
    let _ = sendWired_Redirect_p_cpdqLogin w st in
    next


let p (host:principal) (user_input:msg11) =
  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 d *)

type result_d = string

type msg15 = {
   hReject : (var_p * var_d * var_c -> msg16)}
and msg16 = 
   Basicreply of (var_r * result_d)

let rec d_start : store -> msg15 -> result_d = fun st handlers ->
  let r = receiveWired_d_start st in
  match r with
  | Wired_in_d_start_of_p_Reject_cpdqLogin___c_cpdqLogin_cpdq__ ((p, d, c), newSt) ->
    let () = assume (Recv_Reject(newSt.vars.d,newSt.header.sid,newSt.header.ts,newSt.vars.p,newSt.vars.d,newSt.vars.c)) in
    let next = handlers.hReject (P p, D d, C c) in
    d_Reject_cpdqLogin newSt next
and d_Reject_cpdqLogin : store -> msg16 -> result_d = fun st -> function
  | Basicreply(R r,next) ->
    let ts1 = st.header.ts+1 in
    let () = assume (Send_Basicreply(st.vars.d,st.header.sid,ts1,r)) in
    let _ = sendWired_Basicreply_d_Reject_cpdqLogin r st in
    next


let d (host:principal) (user_input:msg15) =
  let empty_store = empty_store_d host false in
  let () = bind host in
  debug_impl ("Executing role d ...");
  let result = d_start empty_store user_input in (*close();*)
  result