Skip to main content

🔫 Bond_id_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.

Inductive t : Set :=
| Tx_rollup_bond_id : Tx_rollup_repr.t t.

Definition Compare_Make_include :=
  Compare.Make
    (let t : Set := t in
    let compare (id1 : t) (id2 : t) : int :=
      let '(Tx_rollup_bond_id id1, Tx_rollup_bond_id id2) := (id1, id2) in
      Tx_rollup_repr.compare id1 id2 in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Inclusion of the module [Compare_Make_include]
Definition op_eq := Compare_Make_include.(Compare.S.op_eq).

Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).

Definition op_lt := Compare_Make_include.(Compare.S.op_lt).

Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).

Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).

Definition op_gt := Compare_Make_include.(Compare.S.op_gt).

Definition compare := Compare_Make_include.(Compare.S.compare).

Definition equal := Compare_Make_include.(Compare.S.equal).

Definition max := Compare_Make_include.(Compare.S.max).

Definition min := Compare_Make_include.(Compare.S.min).

Definition encoding : Data_encoding.encoding t :=
  (let arg := Data_encoding.def "bond_id" in
  fun (eta : Data_encoding.encoding t) ⇒ arg None None eta)
    (Data_encoding.union None
      [
        Data_encoding.case_value "Tx_rollup_bond_id" None (Data_encoding.Tag 0)
          (Data_encoding.obj1
            (Data_encoding.req None None "tx_rollup"
              Tx_rollup_repr.encoding))
          (fun (function_parameter : t) ⇒
            let 'Tx_rollup_bond_id id := function_parameter in
            Some id)
          (fun (id : Tx_rollup_repr.t) ⇒ Tx_rollup_bond_id id)
      ]).

Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
  let 'Tx_rollup_bond_id id := function_parameter in
  Tx_rollup_repr.pp ppf id.

Definition rpc_arg : RPC_arg.arg t :=
  let construct (function_parameter : t) : string :=
    let 'Tx_rollup_bond_id id := function_parameter in
    Tx_rollup_repr.to_b58check id in
  let destruct (id : string) : Pervasives.result t string :=
    Result.map_error
      (fun (function_parameter : Error_monad.trace Error_monad._error) ⇒
        let '_ := function_parameter in
        "Cannot parse tx rollup id")
      (let? id := Tx_rollup_repr.of_b58check id in
      return? (Tx_rollup_bond_id id)) in
  RPC_arg.make (Some "A bond identifier.") "bond_id" destruct construct tt.

Module Index.
  Definition t : Set := t.

  Definition path_length : int := 1.

  Definition to_path (c_value : t) (l_value : list string) : list string :=
    let raw_key := Data_encoding.Binary.to_bytes_exn None encoding c_value in
    let 'Hex.Hex key_value := Hex.of_bytes None raw_key in
    cons key_value l_value.

  Definition of_path (function_parameter : list string) : option t :=
    match function_parameter with
    | cons key_value []
      Option.bind (Hex.to_bytes (Hex.Hex key_value))
        (Data_encoding.Binary.of_bytes_opt encoding)
    | _None
    end.

  Definition rpc_arg : RPC_arg.arg t := rpc_arg.

  Definition encoding : Data_encoding.encoding t := encoding.

  Definition compare : t t int := compare.

  (* Index *)
  Definition module :=
    {|
      Storage_description.INDEX.path_length := path_length;
      Storage_description.INDEX.to_path := to_path;
      Storage_description.INDEX.of_path := of_path;
      Storage_description.INDEX.rpc_arg := rpc_arg;
      Storage_description.INDEX.encoding := encoding;
      Storage_description.INDEX.compare := compare
    |}.
End Index.
Definition Index := Index.module.