Skip to main content

🏪 Services_registration.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
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_levelblock_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_valuec_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).