🎛️ Constants_services.v

Translated OCaml

See proofs, Gitlab , 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.Services_registration.

Definition custom_root : RPC_path.context RPC_context.t :=
  RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "constants".

Module S.
  Definition errors
    : RPC_service.service RPC_context.t RPC_context.t unit unit
      Data_encoding.json_schema :=
    RPC_service.get_service
      (Some "Schema for all the RPC errors from this protocol version")
      RPC_query.empty Data_encoding.json_schema_value
      (RPC_path.op_div custom_root "errors").

  Definition all
    : RPC_service.service RPC_context.t RPC_context.t unit unit
      Alpha_context.Constants.t :=
    RPC_service.get_service (Some "All constants") RPC_query.empty
      Alpha_context.Constants.encoding custom_root.

  Definition parametric_value
    : RPC_service.service RPC_context.t RPC_context.t unit unit
      Alpha_context.Constants.Parametric.t :=
    RPC_service.get_service (Some "Parametric constants") RPC_query.empty
      Alpha_context.Constants.Parametric.encoding
      (RPC_path.op_div custom_root "parametric").
End S.

Definition register (function_parameter : unit) : unit :=
  let '_ := function_parameter in
  let '_ :=
    Services_registration.register0_noctxt true S.errors
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          return? (Data_encoding.Json.schema None Error_monad.error_encoding))
    in
  let '_ :=
    Services_registration.register0 false S.all
      (fun (ctxt : Alpha_context.t) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            return? (Alpha_context.Constants.all ctxt)) in
  Services_registration.register0 false S.parametric_value
    (fun (ctxt : Alpha_context.t) ⇒
      fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          return? (Alpha_context.Constants.parametric_value ctxt)).

Definition errors {A : Set} (ctxt : RPC_context.simple A) (block : A)
  : Error_monad.shell_tzresult Data_encoding.json_schema :=
  RPC_context.make_call0 S.errors ctxt block tt tt.

Definition all {A : Set} (ctxt : RPC_context.simple A) (block : A)
  : Error_monad.shell_tzresult Alpha_context.Constants.t :=
  RPC_context.make_call0 S.all ctxt block tt tt.

Definition parametric_value {A : Set} (ctxt : RPC_context.simple A) (block : A)
  : Error_monad.shell_tzresult Alpha_context.Constants.Parametric.t :=
  RPC_context.make_call0 S.parametric_value ctxt block tt tt.