๐ช Services_registration.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Module rpc_context.
Record record : Set := Build {
block_hash : Block_hash.t;
block_header : Alpha_context.Block_header.shell_header;
context : Alpha_context.t;
}.
Definition with_block_hash block_hash (r : record) :=
Build block_hash r.(block_header) r.(context).
Definition with_block_header block_header (r : record) :=
Build r.(block_hash) block_header r.(context).
Definition with_context context (r : record) :=
Build r.(block_hash) r.(block_header) context.
End rpc_context.
Definition rpc_context := rpc_context.record.
Inductive level : Set :=
| Head_level : level
| Successor_level : level.
Definition rpc_init (function_parameter : Updater.rpc_context)
: level โ M? rpc_context :=
let '{|
Updater.rpc_context.block_hash := block_hash;
Updater.rpc_context.block_header := block_header;
Updater.rpc_context.context := context_value
|} := function_parameter in
fun (mode : level) โ
let timestamp := block_header.(Block_header.shell_header.timestamp) in
let level :=
match mode with
| Head_level โ block_header.(Block_header.shell_header.level)
| Successor_level โ
Int32.succ block_header.(Block_header.shell_header.level)
end in
let? '(context_value, _, _) :=
Alpha_context.prepare context_value level timestamp timestamp in
return?
{| rpc_context.block_hash := block_hash;
rpc_context.block_header := block_header;
rpc_context.context := context_value; |}.
Definition rpc_services
: Pervasives.ref (RPC_directory.t Updater.rpc_context) :=
Pervasives.ref_value RPC_directory.empty.
Definition register0_fullctxt {A B C : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context Updater.rpc_context A B C)
(f_value : rpc_context โ A โ B โ M? C) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (ctxt : Updater.rpc_context) โ
fun (q_value : A) โ
fun (i_value : B) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt q_value i_value)).
Definition register0 {A B C : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context Updater.rpc_context A B C)
(f_value : Alpha_context.t โ A โ B โ M? C) : unit :=
register0_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
f_value context_value).
Definition register0_noctxt {A B C D : Set}
(chunked : bool) (s_value : RPC_service.t Updater.rpc_context A B C D)
(f_value : B โ C โ M? D) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : A) โ
let '_ := function_parameter in
fun (q_value : B) โ fun (i_value : C) โ f_value q_value i_value)).
Definition register1_fullctxt {A B C D : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context (Updater.rpc_context ร A) B C D)
(f_value : rpc_context โ A โ B โ C โ M? D) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : Updater.rpc_context ร A) โ
let '(ctxt, arg) := function_parameter in
fun (q_value : B) โ
fun (i_value : C) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt arg q_value i_value)).
Definition register1 {A B C D : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context (Updater.rpc_context ร A) B C D)
(f_value : Alpha_context.t โ A โ B โ C โ M? D) : unit :=
register1_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
fun (x_value : A) โ f_value context_value x_value).
Definition register2_fullctxt {A B C D E : Set}
(chunked : bool)
(s_value :
RPC_service.t Updater.rpc_context ((Updater.rpc_context ร A) ร B) C D E)
(f_value : rpc_context โ A โ B โ C โ D โ M? E) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : (Updater.rpc_context ร A) ร B) โ
let '((ctxt, arg1), arg2) := function_parameter in
fun (q_value : C) โ
fun (i_value : D) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt arg1 arg2 q_value i_value)).
Definition register2 {A B C D E : Set}
(chunked : bool)
(s_value :
RPC_service.t Updater.rpc_context ((Updater.rpc_context ร A) ร B) C D E)
(f_value : Alpha_context.t โ A โ B โ C โ D โ M? E) : unit :=
register2_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
fun (a1 : A) โ
fun (a2 : B) โ
fun (q_value : C) โ
fun (i_value : D) โ f_value context_value a1 a2 q_value i_value).
Definition opt_register0_fullctxt {A B C : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context Updater.rpc_context A B C)
(f_value : rpc_context โ A โ B โ M? (option C)) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.opt_register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (ctxt : Updater.rpc_context) โ
fun (q_value : A) โ
fun (i_value : B) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt q_value i_value)).
Definition opt_register0 {A B C : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context Updater.rpc_context A B C)
(f_value : Alpha_context.t โ A โ B โ M? (option C)) : unit :=
opt_register0_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
f_value context_value).
Definition opt_register1_fullctxt {A B C D : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context (Updater.rpc_context ร A) B C D)
(f_value : rpc_context โ A โ B โ C โ M? (option D)) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.opt_register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : Updater.rpc_context ร A) โ
let '(ctxt, arg) := function_parameter in
fun (q_value : B) โ
fun (i_value : C) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt arg q_value i_value)).
Definition opt_register1 {A B C D : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context (Updater.rpc_context ร A) B C D)
(f_value : Alpha_context.t โ A โ B โ C โ M? (option D)) : unit :=
opt_register1_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
fun (x_value : A) โ f_value context_value x_value).
Definition opt_register2_fullctxt {A B C D E : Set}
(chunked : bool)
(s_value :
RPC_service.t Updater.rpc_context ((Updater.rpc_context ร A) ร B) C D E)
(f_value : rpc_context โ A โ B โ C โ D โ M? (option E)) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.opt_register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : (Updater.rpc_context ร A) ร B) โ
let '((ctxt, arg1), arg2) := function_parameter in
fun (q_value : C) โ
fun (i_value : D) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt arg1 arg2 q_value i_value)).
Definition opt_register2 {A B C D E : Set}
(chunked : bool)
(s_value :
RPC_service.t Updater.rpc_context ((Updater.rpc_context ร A) ร B) C D E)
(f_value : Alpha_context.t โ A โ B โ C โ D โ M? (option E)) : unit :=
opt_register2_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
fun (a1 : A) โ
fun (a2 : B) โ
fun (q_value : C) โ
fun (i_value : D) โ f_value context_value a1 a2 q_value i_value).
Definition get_rpc_services (function_parameter : unit)
: RPC_directory.directory Updater.rpc_context :=
let '_ := function_parameter in
let p_value :=
RPC_directory.map
(fun (c_value : Updater.rpc_context) โ
let function_parameter := rpc_init c_value Head_level in
match function_parameter with
| Pervasives.Error t_value โ
Pervasives.raise
(Build_extensible "Failure" string
(Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format) "%a")
Error_monad.pp_trace t_value))
| Pervasives.Ok c_value โ c_value.(rpc_context.context)
end) (Storage_description.build_directory Alpha_context.description) in
RPC_directory.register_dynamic_directory None
(Pervasives.op_exclamation rpc_services)
(RPC_path.op_div
(RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "raw")
"json")
(fun (function_parameter : Updater.rpc_context) โ
let '_ := function_parameter in
p_value).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Module rpc_context.
Record record : Set := Build {
block_hash : Block_hash.t;
block_header : Alpha_context.Block_header.shell_header;
context : Alpha_context.t;
}.
Definition with_block_hash block_hash (r : record) :=
Build block_hash r.(block_header) r.(context).
Definition with_block_header block_header (r : record) :=
Build r.(block_hash) block_header r.(context).
Definition with_context context (r : record) :=
Build r.(block_hash) r.(block_header) context.
End rpc_context.
Definition rpc_context := rpc_context.record.
Inductive level : Set :=
| Head_level : level
| Successor_level : level.
Definition rpc_init (function_parameter : Updater.rpc_context)
: level โ M? rpc_context :=
let '{|
Updater.rpc_context.block_hash := block_hash;
Updater.rpc_context.block_header := block_header;
Updater.rpc_context.context := context_value
|} := function_parameter in
fun (mode : level) โ
let timestamp := block_header.(Block_header.shell_header.timestamp) in
let level :=
match mode with
| Head_level โ block_header.(Block_header.shell_header.level)
| Successor_level โ
Int32.succ block_header.(Block_header.shell_header.level)
end in
let? '(context_value, _, _) :=
Alpha_context.prepare context_value level timestamp timestamp in
return?
{| rpc_context.block_hash := block_hash;
rpc_context.block_header := block_header;
rpc_context.context := context_value; |}.
Definition rpc_services
: Pervasives.ref (RPC_directory.t Updater.rpc_context) :=
Pervasives.ref_value RPC_directory.empty.
Definition register0_fullctxt {A B C : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context Updater.rpc_context A B C)
(f_value : rpc_context โ A โ B โ M? C) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (ctxt : Updater.rpc_context) โ
fun (q_value : A) โ
fun (i_value : B) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt q_value i_value)).
Definition register0 {A B C : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context Updater.rpc_context A B C)
(f_value : Alpha_context.t โ A โ B โ M? C) : unit :=
register0_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
f_value context_value).
Definition register0_noctxt {A B C D : Set}
(chunked : bool) (s_value : RPC_service.t Updater.rpc_context A B C D)
(f_value : B โ C โ M? D) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : A) โ
let '_ := function_parameter in
fun (q_value : B) โ fun (i_value : C) โ f_value q_value i_value)).
Definition register1_fullctxt {A B C D : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context (Updater.rpc_context ร A) B C D)
(f_value : rpc_context โ A โ B โ C โ M? D) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : Updater.rpc_context ร A) โ
let '(ctxt, arg) := function_parameter in
fun (q_value : B) โ
fun (i_value : C) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt arg q_value i_value)).
Definition register1 {A B C D : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context (Updater.rpc_context ร A) B C D)
(f_value : Alpha_context.t โ A โ B โ C โ M? D) : unit :=
register1_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
fun (x_value : A) โ f_value context_value x_value).
Definition register2_fullctxt {A B C D E : Set}
(chunked : bool)
(s_value :
RPC_service.t Updater.rpc_context ((Updater.rpc_context ร A) ร B) C D E)
(f_value : rpc_context โ A โ B โ C โ D โ M? E) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : (Updater.rpc_context ร A) ร B) โ
let '((ctxt, arg1), arg2) := function_parameter in
fun (q_value : C) โ
fun (i_value : D) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt arg1 arg2 q_value i_value)).
Definition register2 {A B C D E : Set}
(chunked : bool)
(s_value :
RPC_service.t Updater.rpc_context ((Updater.rpc_context ร A) ร B) C D E)
(f_value : Alpha_context.t โ A โ B โ C โ D โ M? E) : unit :=
register2_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
fun (a1 : A) โ
fun (a2 : B) โ
fun (q_value : C) โ
fun (i_value : D) โ f_value context_value a1 a2 q_value i_value).
Definition opt_register0_fullctxt {A B C : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context Updater.rpc_context A B C)
(f_value : rpc_context โ A โ B โ M? (option C)) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.opt_register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (ctxt : Updater.rpc_context) โ
fun (q_value : A) โ
fun (i_value : B) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt q_value i_value)).
Definition opt_register0 {A B C : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context Updater.rpc_context A B C)
(f_value : Alpha_context.t โ A โ B โ M? (option C)) : unit :=
opt_register0_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
f_value context_value).
Definition opt_register1_fullctxt {A B C D : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context (Updater.rpc_context ร A) B C D)
(f_value : rpc_context โ A โ B โ C โ M? (option D)) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.opt_register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : Updater.rpc_context ร A) โ
let '(ctxt, arg) := function_parameter in
fun (q_value : B) โ
fun (i_value : C) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt arg q_value i_value)).
Definition opt_register1 {A B C D : Set}
(chunked : bool)
(s_value : RPC_service.t Updater.rpc_context (Updater.rpc_context ร A) B C D)
(f_value : Alpha_context.t โ A โ B โ C โ M? (option D)) : unit :=
opt_register1_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
fun (x_value : A) โ f_value context_value x_value).
Definition opt_register2_fullctxt {A B C D E : Set}
(chunked : bool)
(s_value :
RPC_service.t Updater.rpc_context ((Updater.rpc_context ร A) ร B) C D E)
(f_value : rpc_context โ A โ B โ C โ D โ M? (option E)) : unit :=
Pervasives.op_coloneq rpc_services
(RPC_directory.opt_register chunked (Pervasives.op_exclamation rpc_services)
s_value
(fun (function_parameter : (Updater.rpc_context ร A) ร B) โ
let '((ctxt, arg1), arg2) := function_parameter in
fun (q_value : C) โ
fun (i_value : D) โ
let? ctxt := rpc_init ctxt Head_level in
f_value ctxt arg1 arg2 q_value i_value)).
Definition opt_register2 {A B C D E : Set}
(chunked : bool)
(s_value :
RPC_service.t Updater.rpc_context ((Updater.rpc_context ร A) ร B) C D E)
(f_value : Alpha_context.t โ A โ B โ C โ D โ M? (option E)) : unit :=
opt_register2_fullctxt chunked s_value
(fun (function_parameter : rpc_context) โ
let '{| rpc_context.context := context_value |} := function_parameter in
fun (a1 : A) โ
fun (a2 : B) โ
fun (q_value : C) โ
fun (i_value : D) โ f_value context_value a1 a2 q_value i_value).
Definition get_rpc_services (function_parameter : unit)
: RPC_directory.directory Updater.rpc_context :=
let '_ := function_parameter in
let p_value :=
RPC_directory.map
(fun (c_value : Updater.rpc_context) โ
let function_parameter := rpc_init c_value Head_level in
match function_parameter with
| Pervasives.Error t_value โ
Pervasives.raise
(Build_extensible "Failure" string
(Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format) "%a")
Error_monad.pp_trace t_value))
| Pervasives.Ok c_value โ c_value.(rpc_context.context)
end) (Storage_description.build_directory Alpha_context.description) in
RPC_directory.register_dynamic_directory None
(Pervasives.op_exclamation rpc_services)
(RPC_path.op_div
(RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "raw")
"json")
(fun (function_parameter : Updater.rpc_context) โ
let '_ := function_parameter in
p_value).