🦥 Lazy_storage_kind.v
Translated 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.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Module TEMP_ID.
Record signature {t : Set} : Set := {
t := t;
equal : t → t → bool;
init_value : t;
next : t → t;
}.
End TEMP_ID.
Definition TEMP_ID := @TEMP_ID.signature.
Arguments TEMP_ID {_}.
Module ID.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
encoding : Data_encoding.t t;
rpc_arg : RPC_arg.arg t;
init_value : t;
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Module TEMP_ID.
Record signature {t : Set} : Set := {
t := t;
equal : t → t → bool;
init_value : t;
next : t → t;
}.
End TEMP_ID.
Definition TEMP_ID := @TEMP_ID.signature.
Arguments TEMP_ID {_}.
Module ID.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
encoding : Data_encoding.t t;
rpc_arg : RPC_arg.arg t;
init_value : t;
In the protocol, to be used in parse_data only
In the protocol, to be used in unparse_data only
unparse_to_z : t → Z.t;
next : t → t;
is_temp : t → bool;
of_legacy_USE_ONLY_IN_Legacy_big_map_diff : Z.t → t;
to_legacy_USE_ONLY_IN_Legacy_big_map_diff : t → Z.t;
to_path : t → list string → list string;
of_path : list string → option t;
path_length : int;
}.
End ID.
Definition ID := @ID.signature.
Arguments ID {_}.
Module Title.
Record signature : Set := {
title : string;
}.
End Title.
Definition Title := Title.signature.
Module TitleWithId.
Record signature {Id_t IdSet_t : Set} : Set := {
title : string;
Id : ID (t := Id_t);
Temp_id : TEMP_ID (t := Id.(ID.t));
IdSet : _Set.S (elt := Id.(ID.t)) (t := IdSet_t);
}.
End TitleWithId.
Definition TitleWithId := @TitleWithId.signature.
Arguments TitleWithId {_ _}.
Module MakeId.
Class FArgs := {
Title : Title;
}.
Definition title `{FArgs} : string := Title.(Title.title).
Definition title_words `{FArgs} : string :=
String.map
(fun (function_parameter : ascii) ⇒
match function_parameter with
| "_" % char ⇒ " " % char
| c_value ⇒ c_value
end) title.
Definition rpc_arg_error `{FArgs} : string :=
Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Cannot parse "
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " id"
CamlinternalFormatBasics.End_of_format))) "Cannot parse %s id")
title_words.
Definition description `{FArgs} : string :=
Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A "
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " identifier"
CamlinternalFormatBasics.End_of_format))) "A %s identifier")
title_words.
Definition name `{FArgs} : string := Pervasives.op_caret title "_id".
Definition encoding_title `{FArgs} : string :=
Pervasives.op_caret (String.capitalize_ascii title_words) " identifier".
Module Id.
Definition t `{FArgs} : Set := Z.t.
Definition compare `{FArgs} : Z.t → Z.t → int := Z.compare.
Definition encoding `{FArgs} : Data_encoding.encoding Z.t :=
Data_encoding.def name (Some encoding_title) (Some description)
Data_encoding.z_value.
Definition rpc_arg `{FArgs} : RPC_arg.arg Z.t :=
let construct := Z.to_string in
let destruct (hash_value : string) : Pervasives.result Z.t string :=
Result.catch_f None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Z.of_string hash_value)
(fun (function_parameter : extensible_type) ⇒
let '_ := function_parameter in
rpc_arg_error) in
RPC_arg.make (Some description) name destruct construct tt.
Definition init_value `{FArgs} : Z.t := Z.zero.
Definition parse_z `{FArgs} (z_value : Z.t) : t := z_value.
Definition unparse_to_z `{FArgs} (z_value : t) : Z.t := z_value.
Definition next `{FArgs} : Z.t → Z.t := Z.succ.
Definition of_legacy_USE_ONLY_IN_Legacy_big_map_diff `{FArgs}
(z_value : Z.t) : t := z_value.
Definition to_legacy_USE_ONLY_IN_Legacy_big_map_diff `{FArgs} (z_value : t)
: Z.t := z_value.
Definition is_temp `{FArgs} (z_value : Z.t) : bool := z_value <Z Z.zero.
Definition path_length `{FArgs} : int := 1.
Definition to_path `{FArgs} (z_value : Z.t) (l_value : list string)
: list string := cons (Z.to_string z_value) l_value.
Definition of_path `{FArgs} (function_parameter : list string)
: option Z.t :=
match function_parameter with
| ([] | cons _ (cons _ _)) ⇒ None
| cons z_value [] ⇒ Some (Z.of_string z_value)
end.
(* Id *)
Definition module `{FArgs} :=
{|
ID.compare := compare;
ID.encoding := encoding;
ID.rpc_arg := rpc_arg;
ID.init_value := init_value;
ID.parse_z := parse_z;
ID.unparse_to_z := unparse_to_z;
ID.next := next;
ID.of_legacy_USE_ONLY_IN_Legacy_big_map_diff :=
of_legacy_USE_ONLY_IN_Legacy_big_map_diff;
ID.to_legacy_USE_ONLY_IN_Legacy_big_map_diff :=
to_legacy_USE_ONLY_IN_Legacy_big_map_diff;
ID.is_temp := is_temp;
ID.path_length := path_length;
ID.to_path := to_path;
ID.of_path := of_path
|}.
End Id.
Definition Id `{FArgs} := Id.module.
Module Temp_id.
Definition t `{FArgs} : Set := Z.t.
Definition equal `{FArgs} : Z.t → Z.t → bool := Z.equal.
Definition init_value `{FArgs} : Z.t :=
Z.of_int (Pervasives.op_tildeminus 1).
Definition next `{FArgs} (z_value : Z.t) : Z.t := z_value -Z Z.one.
(* Temp_id *)
Definition module `{FArgs} :=
{|
TEMP_ID.equal := equal;
TEMP_ID.init_value := init_value;
TEMP_ID.next := next
|}.
End Temp_id.
Definition Temp_id `{FArgs} := Temp_id.module.
Definition IdSet `{FArgs} :=
_Set.Make
{|
Compare.COMPARABLE.compare := Id.(ID.compare)
|}.
(* MakeId *)
Definition functor `{FArgs} :=
{|
TitleWithId.title := title;
TitleWithId.Id := Id;
TitleWithId.Temp_id := Temp_id;
TitleWithId.IdSet := IdSet
|}.
End MakeId.
Definition MakeId (Title : Title) : TitleWithId (Id_t := _) (IdSet_t := _) :=
let '_ := MakeId.Build_FArgs Title in
MakeId.functor.
Module Big_map.
Definition MakeId_include :=
MakeId
(let title := "big_map" in
{|
Title.title := title
|}).
next : t → t;
is_temp : t → bool;
of_legacy_USE_ONLY_IN_Legacy_big_map_diff : Z.t → t;
to_legacy_USE_ONLY_IN_Legacy_big_map_diff : t → Z.t;
to_path : t → list string → list string;
of_path : list string → option t;
path_length : int;
}.
End ID.
Definition ID := @ID.signature.
Arguments ID {_}.
Module Title.
Record signature : Set := {
title : string;
}.
End Title.
Definition Title := Title.signature.
Module TitleWithId.
Record signature {Id_t IdSet_t : Set} : Set := {
title : string;
Id : ID (t := Id_t);
Temp_id : TEMP_ID (t := Id.(ID.t));
IdSet : _Set.S (elt := Id.(ID.t)) (t := IdSet_t);
}.
End TitleWithId.
Definition TitleWithId := @TitleWithId.signature.
Arguments TitleWithId {_ _}.
Module MakeId.
Class FArgs := {
Title : Title;
}.
Definition title `{FArgs} : string := Title.(Title.title).
Definition title_words `{FArgs} : string :=
String.map
(fun (function_parameter : ascii) ⇒
match function_parameter with
| "_" % char ⇒ " " % char
| c_value ⇒ c_value
end) title.
Definition rpc_arg_error `{FArgs} : string :=
Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Cannot parse "
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " id"
CamlinternalFormatBasics.End_of_format))) "Cannot parse %s id")
title_words.
Definition description `{FArgs} : string :=
Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A "
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " identifier"
CamlinternalFormatBasics.End_of_format))) "A %s identifier")
title_words.
Definition name `{FArgs} : string := Pervasives.op_caret title "_id".
Definition encoding_title `{FArgs} : string :=
Pervasives.op_caret (String.capitalize_ascii title_words) " identifier".
Module Id.
Definition t `{FArgs} : Set := Z.t.
Definition compare `{FArgs} : Z.t → Z.t → int := Z.compare.
Definition encoding `{FArgs} : Data_encoding.encoding Z.t :=
Data_encoding.def name (Some encoding_title) (Some description)
Data_encoding.z_value.
Definition rpc_arg `{FArgs} : RPC_arg.arg Z.t :=
let construct := Z.to_string in
let destruct (hash_value : string) : Pervasives.result Z.t string :=
Result.catch_f None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Z.of_string hash_value)
(fun (function_parameter : extensible_type) ⇒
let '_ := function_parameter in
rpc_arg_error) in
RPC_arg.make (Some description) name destruct construct tt.
Definition init_value `{FArgs} : Z.t := Z.zero.
Definition parse_z `{FArgs} (z_value : Z.t) : t := z_value.
Definition unparse_to_z `{FArgs} (z_value : t) : Z.t := z_value.
Definition next `{FArgs} : Z.t → Z.t := Z.succ.
Definition of_legacy_USE_ONLY_IN_Legacy_big_map_diff `{FArgs}
(z_value : Z.t) : t := z_value.
Definition to_legacy_USE_ONLY_IN_Legacy_big_map_diff `{FArgs} (z_value : t)
: Z.t := z_value.
Definition is_temp `{FArgs} (z_value : Z.t) : bool := z_value <Z Z.zero.
Definition path_length `{FArgs} : int := 1.
Definition to_path `{FArgs} (z_value : Z.t) (l_value : list string)
: list string := cons (Z.to_string z_value) l_value.
Definition of_path `{FArgs} (function_parameter : list string)
: option Z.t :=
match function_parameter with
| ([] | cons _ (cons _ _)) ⇒ None
| cons z_value [] ⇒ Some (Z.of_string z_value)
end.
(* Id *)
Definition module `{FArgs} :=
{|
ID.compare := compare;
ID.encoding := encoding;
ID.rpc_arg := rpc_arg;
ID.init_value := init_value;
ID.parse_z := parse_z;
ID.unparse_to_z := unparse_to_z;
ID.next := next;
ID.of_legacy_USE_ONLY_IN_Legacy_big_map_diff :=
of_legacy_USE_ONLY_IN_Legacy_big_map_diff;
ID.to_legacy_USE_ONLY_IN_Legacy_big_map_diff :=
to_legacy_USE_ONLY_IN_Legacy_big_map_diff;
ID.is_temp := is_temp;
ID.path_length := path_length;
ID.to_path := to_path;
ID.of_path := of_path
|}.
End Id.
Definition Id `{FArgs} := Id.module.
Module Temp_id.
Definition t `{FArgs} : Set := Z.t.
Definition equal `{FArgs} : Z.t → Z.t → bool := Z.equal.
Definition init_value `{FArgs} : Z.t :=
Z.of_int (Pervasives.op_tildeminus 1).
Definition next `{FArgs} (z_value : Z.t) : Z.t := z_value -Z Z.one.
(* Temp_id *)
Definition module `{FArgs} :=
{|
TEMP_ID.equal := equal;
TEMP_ID.init_value := init_value;
TEMP_ID.next := next
|}.
End Temp_id.
Definition Temp_id `{FArgs} := Temp_id.module.
Definition IdSet `{FArgs} :=
_Set.Make
{|
Compare.COMPARABLE.compare := Id.(ID.compare)
|}.
(* MakeId *)
Definition functor `{FArgs} :=
{|
TitleWithId.title := title;
TitleWithId.Id := Id;
TitleWithId.Temp_id := Temp_id;
TitleWithId.IdSet := IdSet
|}.
End MakeId.
Definition MakeId (Title : Title) : TitleWithId (Id_t := _) (IdSet_t := _) :=
let '_ := MakeId.Build_FArgs Title in
MakeId.functor.
Module Big_map.
Definition MakeId_include :=
MakeId
(let title := "big_map" in
{|
Title.title := title
|}).
Inclusion of the module [MakeId_include]
Definition title := MakeId_include.(TitleWithId.title).
Definition Id := MakeId_include.(TitleWithId.Id).
Definition Temp_id := MakeId_include.(TitleWithId.Temp_id).
Definition IdSet := MakeId_include.(TitleWithId.IdSet).
Module alloc.
Record record : Set := Build {
key_type : Script_repr.expr;
value_type : Script_repr.expr;
}.
Definition with_key_type key_type (r : record) :=
Build key_type r.(value_type).
Definition with_value_type value_type (r : record) :=
Build r.(key_type) value_type.
End alloc.
Definition alloc := alloc.record.
Module update.
Record record : Set := Build {
key : Script_repr.expr;
key_hash : Script_expr_hash.t;
value : option Script_repr.expr;
}.
Definition with_key key (r : record) :=
Build key r.(key_hash) r.(value).
Definition with_key_hash key_hash (r : record) :=
Build r.(key) key_hash r.(value).
Definition with_value value (r : record) :=
Build r.(key) r.(key_hash) value.
End update.
Definition update := update.record.
Definition updates : Set := list update.
Definition alloc_encoding : Data_encoding.encoding alloc :=
Data_encoding.conv
(fun (function_parameter : alloc) ⇒
let '{| alloc.key_type := key_type; alloc.value_type := value_type |} :=
function_parameter in
(key_type, value_type))
(fun (function_parameter : Script_repr.expr × Script_repr.expr) ⇒
let '(key_type, value_type) := function_parameter in
{| alloc.key_type := key_type; alloc.value_type := value_type; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "key_type" Script_repr.expr_encoding)
(Data_encoding.req None None "value_type" Script_repr.expr_encoding)).
Definition update_encoding : Data_encoding.encoding update :=
Data_encoding.conv
(fun (function_parameter : update) ⇒
let '{|
update.key := key_value;
update.key_hash := key_hash;
update.value := value_value
|} := function_parameter in
(key_hash, key_value, value_value))
(fun (function_parameter :
Script_expr_hash.t × Script_repr.expr × option Script_repr.expr) ⇒
let '(key_hash, key_value, value_value) := function_parameter in
{| update.key := key_value; update.key_hash := key_hash;
update.value := value_value; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "key_hash" Script_expr_hash.encoding)
(Data_encoding.req None None "key" Script_repr.expr_encoding)
(Data_encoding.opt None None "value" Script_repr.expr_encoding)).
Definition updates_encoding : Data_encoding.encoding (list update) :=
Data_encoding.list_value None update_encoding.
End Big_map.
Module Sapling_state.
Definition MakeId_include :=
MakeId
(let title := "sapling_state" in
{|
Title.title := title
|}).
Definition Id := MakeId_include.(TitleWithId.Id).
Definition Temp_id := MakeId_include.(TitleWithId.Temp_id).
Definition IdSet := MakeId_include.(TitleWithId.IdSet).
Module alloc.
Record record : Set := Build {
key_type : Script_repr.expr;
value_type : Script_repr.expr;
}.
Definition with_key_type key_type (r : record) :=
Build key_type r.(value_type).
Definition with_value_type value_type (r : record) :=
Build r.(key_type) value_type.
End alloc.
Definition alloc := alloc.record.
Module update.
Record record : Set := Build {
key : Script_repr.expr;
key_hash : Script_expr_hash.t;
value : option Script_repr.expr;
}.
Definition with_key key (r : record) :=
Build key r.(key_hash) r.(value).
Definition with_key_hash key_hash (r : record) :=
Build r.(key) key_hash r.(value).
Definition with_value value (r : record) :=
Build r.(key) r.(key_hash) value.
End update.
Definition update := update.record.
Definition updates : Set := list update.
Definition alloc_encoding : Data_encoding.encoding alloc :=
Data_encoding.conv
(fun (function_parameter : alloc) ⇒
let '{| alloc.key_type := key_type; alloc.value_type := value_type |} :=
function_parameter in
(key_type, value_type))
(fun (function_parameter : Script_repr.expr × Script_repr.expr) ⇒
let '(key_type, value_type) := function_parameter in
{| alloc.key_type := key_type; alloc.value_type := value_type; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "key_type" Script_repr.expr_encoding)
(Data_encoding.req None None "value_type" Script_repr.expr_encoding)).
Definition update_encoding : Data_encoding.encoding update :=
Data_encoding.conv
(fun (function_parameter : update) ⇒
let '{|
update.key := key_value;
update.key_hash := key_hash;
update.value := value_value
|} := function_parameter in
(key_hash, key_value, value_value))
(fun (function_parameter :
Script_expr_hash.t × Script_repr.expr × option Script_repr.expr) ⇒
let '(key_hash, key_value, value_value) := function_parameter in
{| update.key := key_value; update.key_hash := key_hash;
update.value := value_value; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "key_hash" Script_expr_hash.encoding)
(Data_encoding.req None None "key" Script_repr.expr_encoding)
(Data_encoding.opt None None "value" Script_repr.expr_encoding)).
Definition updates_encoding : Data_encoding.encoding (list update) :=
Data_encoding.list_value None update_encoding.
End Big_map.
Module Sapling_state.
Definition MakeId_include :=
MakeId
(let title := "sapling_state" in
{|
Title.title := title
|}).
Inclusion of the module [MakeId_include]
Definition title := MakeId_include.(TitleWithId.title).
Definition Id := MakeId_include.(TitleWithId.Id).
Definition Temp_id := MakeId_include.(TitleWithId.Temp_id).
Definition IdSet := MakeId_include.(TitleWithId.IdSet).
Module alloc.
Record record : Set := Build {
memo_size : Sapling_repr.Memo_size.t;
}.
Definition with_memo_size memo_size (r : record) :=
Build memo_size.
End alloc.
Definition alloc := alloc.record.
Definition updates : Set := Sapling_repr.diff.
Definition alloc_encoding : Data_encoding.encoding alloc :=
Data_encoding.conv
(fun (function_parameter : alloc) ⇒
let '{| alloc.memo_size := memo_size |} := function_parameter in
memo_size)
(fun (memo_size : Sapling_repr.Memo_size.t) ⇒
{| alloc.memo_size := memo_size; |}) None
(Data_encoding.obj1
(Data_encoding.req None None "memo_size" Sapling_repr.Memo_size.encoding)).
Definition updates_encoding : Data_encoding.encoding Sapling_repr.diff :=
Sapling_repr.diff_encoding.
End Sapling_state.
Inductive t : Set :=
| Big_map : t
| Sapling_state : t.
Inductive ex : Set :=
| Ex_Kind : t → ex.
Definition all : list (int × ex) :=
[ (0, (Ex_Kind Big_map)); (1, (Ex_Kind Sapling_state)) ].
Inductive cmp : Set :=
| Eq : cmp
| Neq : cmp.
Definition equal (k1 : t) (k2 : t) : cmp :=
match (k1, k2) with
| (Big_map, Big_map) ⇒ Eq
| (Sapling_state, Sapling_state) ⇒ Eq
| (Big_map, _) ⇒ Neq
| (_, Big_map) ⇒ Neq
end.
Definition kind : Set := t.
Module Temp_ids.
Module t.
Record record : Set := Build {
big_map : Big_map.Id.(ID.t);
sapling_state : Sapling_state.Id.(ID.t);
}.
Definition with_big_map big_map (r : record) :=
Build big_map r.(sapling_state).
Definition with_sapling_state sapling_state (r : record) :=
Build r.(big_map) sapling_state.
End t.
Definition t := t.record.
Definition init_value : t :=
{| t.big_map := Big_map.Temp_id.(TEMP_ID.init_value);
t.sapling_state := Sapling_state.Temp_id.(TEMP_ID.init_value); |}.
Axiom fresh : ∀ {i : Set}, kind → t → t × i.
Axiom fold_s : ∀ {acc i : Set},
kind → (acc → i → acc) → t → acc → acc.
End Temp_ids.
Module IdSet.
Module t.
Record record : Set := Build {
big_map : Big_map.IdSet.(_Set.S.t);
sapling_state : Sapling_state.IdSet.(_Set.S.t);
}.
Definition with_big_map big_map (r : record) :=
Build big_map r.(sapling_state).
Definition with_sapling_state sapling_state (r : record) :=
Build r.(big_map) sapling_state.
End t.
Definition t := t.record.
Module fold_f.
Record record {acc : Set} : Set := Build {
f : ∀ {i : Set}, kind → i → acc → acc;
}.
Arguments record : clear implicits.
Definition with_f {t_acc} f (r : record t_acc) :=
Build t_acc f.
End fold_f.
Definition fold_f := fold_f.record.
Definition empty : t :=
{| t.big_map := Big_map.IdSet.(_Set.S.empty);
t.sapling_state := Sapling_state.IdSet.(_Set.S.empty); |}.
Axiom mem : ∀ {i : Set}, kind → i → t → bool.
Axiom add : ∀ {i : Set}, kind → i → t → t.
Axiom diff_value : t → t → t.
Axiom fold : ∀ {i acc : Set},
kind → (i → acc → acc) → t → acc → acc.
Axiom fold_all : ∀ {A : Set}, fold_f A → t → A → A.
End IdSet.
Definition Id := MakeId_include.(TitleWithId.Id).
Definition Temp_id := MakeId_include.(TitleWithId.Temp_id).
Definition IdSet := MakeId_include.(TitleWithId.IdSet).
Module alloc.
Record record : Set := Build {
memo_size : Sapling_repr.Memo_size.t;
}.
Definition with_memo_size memo_size (r : record) :=
Build memo_size.
End alloc.
Definition alloc := alloc.record.
Definition updates : Set := Sapling_repr.diff.
Definition alloc_encoding : Data_encoding.encoding alloc :=
Data_encoding.conv
(fun (function_parameter : alloc) ⇒
let '{| alloc.memo_size := memo_size |} := function_parameter in
memo_size)
(fun (memo_size : Sapling_repr.Memo_size.t) ⇒
{| alloc.memo_size := memo_size; |}) None
(Data_encoding.obj1
(Data_encoding.req None None "memo_size" Sapling_repr.Memo_size.encoding)).
Definition updates_encoding : Data_encoding.encoding Sapling_repr.diff :=
Sapling_repr.diff_encoding.
End Sapling_state.
Inductive t : Set :=
| Big_map : t
| Sapling_state : t.
Inductive ex : Set :=
| Ex_Kind : t → ex.
Definition all : list (int × ex) :=
[ (0, (Ex_Kind Big_map)); (1, (Ex_Kind Sapling_state)) ].
Inductive cmp : Set :=
| Eq : cmp
| Neq : cmp.
Definition equal (k1 : t) (k2 : t) : cmp :=
match (k1, k2) with
| (Big_map, Big_map) ⇒ Eq
| (Sapling_state, Sapling_state) ⇒ Eq
| (Big_map, _) ⇒ Neq
| (_, Big_map) ⇒ Neq
end.
Definition kind : Set := t.
Module Temp_ids.
Module t.
Record record : Set := Build {
big_map : Big_map.Id.(ID.t);
sapling_state : Sapling_state.Id.(ID.t);
}.
Definition with_big_map big_map (r : record) :=
Build big_map r.(sapling_state).
Definition with_sapling_state sapling_state (r : record) :=
Build r.(big_map) sapling_state.
End t.
Definition t := t.record.
Definition init_value : t :=
{| t.big_map := Big_map.Temp_id.(TEMP_ID.init_value);
t.sapling_state := Sapling_state.Temp_id.(TEMP_ID.init_value); |}.
Axiom fresh : ∀ {i : Set}, kind → t → t × i.
Axiom fold_s : ∀ {acc i : Set},
kind → (acc → i → acc) → t → acc → acc.
End Temp_ids.
Module IdSet.
Module t.
Record record : Set := Build {
big_map : Big_map.IdSet.(_Set.S.t);
sapling_state : Sapling_state.IdSet.(_Set.S.t);
}.
Definition with_big_map big_map (r : record) :=
Build big_map r.(sapling_state).
Definition with_sapling_state sapling_state (r : record) :=
Build r.(big_map) sapling_state.
End t.
Definition t := t.record.
Module fold_f.
Record record {acc : Set} : Set := Build {
f : ∀ {i : Set}, kind → i → acc → acc;
}.
Arguments record : clear implicits.
Definition with_f {t_acc} f (r : record t_acc) :=
Build t_acc f.
End fold_f.
Definition fold_f := fold_f.record.
Definition empty : t :=
{| t.big_map := Big_map.IdSet.(_Set.S.empty);
t.sapling_state := Sapling_state.IdSet.(_Set.S.empty); |}.
Axiom mem : ∀ {i : Set}, kind → i → t → bool.
Axiom add : ∀ {i : Set}, kind → i → t → t.
Axiom diff_value : t → t → t.
Axiom fold : ∀ {i acc : Set},
kind → (i → acc → acc) → t → acc → acc.
Axiom fold_all : ∀ {A : Set}, fold_f A → t → A → A.
End IdSet.