🔫 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.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.

Inductive t : Set :=
| Tx_rollup_bond_id : Tx_rollup_repr.t → t
| Sc_rollup_bond_id : Sc_rollup_repr.t → t.

Definition Compare_Make_include :=
  Compare.Make
    (let t : Set := t in
    let compare (id1 : t) (id2 : t) : int :=
      match (id1, id2) with
      | (Tx_rollup_bond_id id1, Tx_rollup_bond_id id2) ⇒
        Tx_rollup_repr.compare id1 id2
      | (Sc_rollup_bond_id id1, Sc_rollup_bond_id id2) ⇒
        Sc_rollup_repr.Address.compare id1 id2
      | (Tx_rollup_bond_id _, Sc_rollup_bond_id _) ⇒ (-1)
      | (Sc_rollup_bond_id _, Tx_rollup_bond_id _) ⇒ 1
      end 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 :=
  Data_encoding.def "bond_id" None None
    (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) ⇒
            match function_parameter with
            | Tx_rollup_bond_id id ⇒ Some id
            | _ ⇒ None
            end) (fun (id : Tx_rollup_repr.t) ⇒ Tx_rollup_bond_id id);
        Data_encoding.case_value "Sc_rollup_bond_id" None (Data_encoding.Tag 1)
          (Data_encoding.obj1
            (Data_encoding.req None None "sc_rollup"
              Sc_rollup_repr.encoding))
          (fun (function_parameter : t) ⇒
            match function_parameter with
            | Sc_rollup_bond_id id ⇒ Some id
            | _ ⇒ None
            end) (fun (id : Sc_rollup_repr.t) ⇒ Sc_rollup_bond_id id)
      ]).

Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
  match function_parameter with
  | Tx_rollup_bond_id id ⇒ Tx_rollup_repr.pp ppf id
  | Sc_rollup_bond_id id ⇒ Sc_rollup_repr.pp ppf id
  end.

#[bypass_check(guard)]
Definition destruct (id : string) : Pervasives.result t string :=
  let starts_with (prefix : string) (s_value : string) : bool :=
    let len_s : int :=
      String.length s_value
    in let len_pre : int :=
      String.length prefix in
    let fix aux (i_value : int) {struct i_value} : bool :=
      if i_value =i len_pre then
        true
      else
        if
          Compare.Char.(Compare.S.op_ltgt) (String.get s_value i_value)
            (String.get prefix i_value)
        then
          false
        else
          aux (i_value +i 1) in
    (len_s ≥i len_pre) && (aux 0) in
  if
    starts_with Tx_rollup_prefixes.rollup_address.(Tx_rollup_prefixes.t.prefix)
      id
  then
    match Tx_rollup_repr.of_b58check_opt id with
    | Some id ⇒ Result.ok (Tx_rollup_bond_id id)
    | None ⇒ Result.error_value "Cannot parse transaction rollup id"
    end
  else
    if starts_with Sc_rollup_repr.Address.prefix id then
      match Sc_rollup_repr.Address.of_b58check_opt id with
      | Some id ⇒ Result.ok (Sc_rollup_bond_id id)
      | None ⇒ Result.error_value "Cannot parse smart contract rollup id"
      end
    else
      Result.error_value "Cannot parse rollup id".

Definition construct (function_parameter : t) : string :=
  match function_parameter with
  | Tx_rollup_bond_id id ⇒ Tx_rollup_repr.to_b58check id
  | Sc_rollup_bond_id id ⇒ Sc_rollup_repr.Address.to_b58check id
  end.

Definition rpc_arg : RPC_arg.arg t :=
  RPC_arg.make (Some "A bond identifier.") "bond_id" destruct construct tt.

Module Internal_for_test.
  Definition destruct : string → Pervasives.result t string := destruct.

  Definition construct : t → string := construct.
End Internal_for_test.

Module Index.
  Definition t : Set := t.

  Definition path_length : M? int := return? 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) : M? (option t) :=
    match function_parameter with
    | cons key_value [] ⇒
      return?
        (Option.bind (Hex.to_bytes (Hex.Hex key_value))
          (Data_encoding.Binary.of_bytes_opt encoding))
    | _ ⇒ return? 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.