🔫 Bond_id_repr.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.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
|}).
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.
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.