🦥 Lazy_storage_kind.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.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.Environment.V8.
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 → M? (option t);
path_length : M? 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} : M? int := return? 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)
: M? (option Z.t) :=
match function_parameter with
| ([] | cons _ (cons _ _)) ⇒ return? None
| cons z_value [] ⇒ return? (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 → M? (option t);
path_length : M? 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} : M? int := return? 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)
: M? (option Z.t) :=
match function_parameter with
| ([] | cons _ (cons _ _)) ⇒ return? None
| cons z_value [] ⇒ return? (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); |}.
Definition fresh {i : Set} (kind_value : kind) (temp_ids : t) : t × i :=
match kind_value with
| Big_map ⇒
cast (t × i)
(let big_map := Big_map.Temp_id.(TEMP_ID.next) temp_ids.(t.big_map) in
((t.with_big_map big_map temp_ids), temp_ids.(t.big_map)))
| Sapling_state ⇒
cast (t × i)
(let sapling_state :=
Sapling_state.Temp_id.(TEMP_ID.next) temp_ids.(t.sapling_state) in
((t.with_sapling_state sapling_state temp_ids), temp_ids.(t.sapling_state)))
end.
#[bypass_check(guard)]
Definition fold_s {acc i : Set}
(kind_value : kind) (f_value : acc → i → acc) (temp_ids : t)
(acc_value : acc) : acc :=
let helper {j : Set} (Temp_id : {_ : unit @ TEMP_ID (t := j)})
: j → (acc → j → acc) → acc :=
let 'existS _ _ Temp_id := Temp_id in
fun (last : j) ⇒
fun (f_value : acc → j → acc) ⇒
let fix aux (acc_value : acc) (id : j) {struct id} : acc :=
if Temp_id.(TEMP_ID.equal) id last then
acc_value
else
let acc_value := f_value acc_value id in
aux acc_value (Temp_id.(TEMP_ID.next) id) in
aux acc_value Temp_id.(TEMP_ID.init_value) in
match (kind_value, f_value) with
| (Big_map, f_value) ⇒
let f_value := cast (acc → Big_map.Id.(ID.t) → acc) f_value in
helper (existS (A := unit) (fun _ ⇒ _) tt Big_map.Temp_id)
temp_ids.(t.big_map)
(fun (acc_value : acc) ⇒
fun (temp_id : Big_map.Id.(ID.t)) ⇒ f_value acc_value temp_id)
| (Sapling_state, f_value) ⇒
let f_value := cast (acc → Sapling_state.Id.(ID.t) → acc) f_value in
helper (existS (A := unit) (fun _ ⇒ _) tt Sapling_state.Temp_id)
temp_ids.(t.sapling_state)
(fun (acc_value : acc) ⇒
fun (temp_id : Sapling_state.Id.(ID.t)) ⇒ f_value acc_value temp_id)
end.
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); |}.
Definition mem {i : Set} (kind_value : kind) (id : i) (set : t) : bool :=
match (kind_value, id, set) with
| (Big_map, id, {| t.big_map := big_map |}) ⇒
let '[big_map, id] :=
cast [Big_map.IdSet.(_Set.S.t) ** Big_map.Id.(ID.t)] [big_map, id] in
Big_map.IdSet.(_Set.S.mem) id big_map
| (Sapling_state, id, {| t.sapling_state := sapling_state |}) ⇒
let '[sapling_state, id] :=
cast [Sapling_state.IdSet.(_Set.S.t) ** Sapling_state.Id.(ID.t)]
[sapling_state, id] in
Sapling_state.IdSet.(_Set.S.mem) id sapling_state
end.
Definition add {i : Set} (kind_value : kind) (id : i) (set : t) : t :=
match (kind_value, id, set) with
| (Big_map, id, {| t.big_map := big_map |}) ⇒
let '[big_map, id] :=
cast [Big_map.IdSet.(_Set.S.t) ** Big_map.Id.(ID.t)] [big_map, id] in
let big_map := Big_map.IdSet.(_Set.S.add) id big_map in
t.with_big_map big_map set
| (Sapling_state, id, {| t.sapling_state := sapling_state |}) ⇒
let '[sapling_state, id] :=
cast [Sapling_state.IdSet.(_Set.S.t) ** Sapling_state.Id.(ID.t)]
[sapling_state, id] in
let sapling_state := Sapling_state.IdSet.(_Set.S.add) id sapling_state in
t.with_sapling_state sapling_state set
end.
Definition diff_value (set1 : t) (set2 : t) : t :=
let big_map :=
Big_map.IdSet.(_Set.S.diff_value) set1.(t.big_map) set2.(t.big_map) in
let sapling_state :=
Sapling_state.IdSet.(_Set.S.diff_value) set1.(t.sapling_state)
set2.(t.sapling_state) in
{| t.big_map := big_map; t.sapling_state := sapling_state; |}.
Definition fold {i acc : Set}
(kind_value : kind) (f_value : i → acc → acc) (set : t) (acc_value : acc)
: acc :=
match (kind_value, f_value, set) with
| (Big_map, f_value, {| t.big_map := big_map |}) ⇒
let '[big_map, f_value] :=
cast [Big_map.IdSet.(_Set.S.t) ** Big_map.Id.(ID.t) → acc → acc]
[big_map, f_value] in
Big_map.IdSet.(_Set.S.fold) f_value big_map acc_value
| (Sapling_state, f_value, {| t.sapling_state := sapling_state |}) ⇒
let '[sapling_state, f_value] :=
cast
[Sapling_state.IdSet.(_Set.S.t) **
Sapling_state.Id.(ID.t) → acc → acc] [sapling_state, f_value] in
Sapling_state.IdSet.(_Set.S.fold) f_value sapling_state acc_value
end.
Definition fold_all {A : Set} (f_value : fold_f A) (set : t) (acc_value : A)
: A :=
List.fold_left
(fun (acc_value : A) ⇒
fun (function_parameter : int × ex) ⇒
let '(_, Ex_Kind kind_value) := function_parameter in
let 'existT _ __Ex_Kind kind_value :=
cast_exists (Es := Set) (fun __Ex_Kind ⇒ kind) kind_value in
(fold (i := __Ex_Kind)) kind_value (f_value.(fold_f.f) kind_value) set
acc_value) acc_value all.
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); |}.
Definition fresh {i : Set} (kind_value : kind) (temp_ids : t) : t × i :=
match kind_value with
| Big_map ⇒
cast (t × i)
(let big_map := Big_map.Temp_id.(TEMP_ID.next) temp_ids.(t.big_map) in
((t.with_big_map big_map temp_ids), temp_ids.(t.big_map)))
| Sapling_state ⇒
cast (t × i)
(let sapling_state :=
Sapling_state.Temp_id.(TEMP_ID.next) temp_ids.(t.sapling_state) in
((t.with_sapling_state sapling_state temp_ids), temp_ids.(t.sapling_state)))
end.
#[bypass_check(guard)]
Definition fold_s {acc i : Set}
(kind_value : kind) (f_value : acc → i → acc) (temp_ids : t)
(acc_value : acc) : acc :=
let helper {j : Set} (Temp_id : {_ : unit @ TEMP_ID (t := j)})
: j → (acc → j → acc) → acc :=
let 'existS _ _ Temp_id := Temp_id in
fun (last : j) ⇒
fun (f_value : acc → j → acc) ⇒
let fix aux (acc_value : acc) (id : j) {struct id} : acc :=
if Temp_id.(TEMP_ID.equal) id last then
acc_value
else
let acc_value := f_value acc_value id in
aux acc_value (Temp_id.(TEMP_ID.next) id) in
aux acc_value Temp_id.(TEMP_ID.init_value) in
match (kind_value, f_value) with
| (Big_map, f_value) ⇒
let f_value := cast (acc → Big_map.Id.(ID.t) → acc) f_value in
helper (existS (A := unit) (fun _ ⇒ _) tt Big_map.Temp_id)
temp_ids.(t.big_map)
(fun (acc_value : acc) ⇒
fun (temp_id : Big_map.Id.(ID.t)) ⇒ f_value acc_value temp_id)
| (Sapling_state, f_value) ⇒
let f_value := cast (acc → Sapling_state.Id.(ID.t) → acc) f_value in
helper (existS (A := unit) (fun _ ⇒ _) tt Sapling_state.Temp_id)
temp_ids.(t.sapling_state)
(fun (acc_value : acc) ⇒
fun (temp_id : Sapling_state.Id.(ID.t)) ⇒ f_value acc_value temp_id)
end.
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); |}.
Definition mem {i : Set} (kind_value : kind) (id : i) (set : t) : bool :=
match (kind_value, id, set) with
| (Big_map, id, {| t.big_map := big_map |}) ⇒
let '[big_map, id] :=
cast [Big_map.IdSet.(_Set.S.t) ** Big_map.Id.(ID.t)] [big_map, id] in
Big_map.IdSet.(_Set.S.mem) id big_map
| (Sapling_state, id, {| t.sapling_state := sapling_state |}) ⇒
let '[sapling_state, id] :=
cast [Sapling_state.IdSet.(_Set.S.t) ** Sapling_state.Id.(ID.t)]
[sapling_state, id] in
Sapling_state.IdSet.(_Set.S.mem) id sapling_state
end.
Definition add {i : Set} (kind_value : kind) (id : i) (set : t) : t :=
match (kind_value, id, set) with
| (Big_map, id, {| t.big_map := big_map |}) ⇒
let '[big_map, id] :=
cast [Big_map.IdSet.(_Set.S.t) ** Big_map.Id.(ID.t)] [big_map, id] in
let big_map := Big_map.IdSet.(_Set.S.add) id big_map in
t.with_big_map big_map set
| (Sapling_state, id, {| t.sapling_state := sapling_state |}) ⇒
let '[sapling_state, id] :=
cast [Sapling_state.IdSet.(_Set.S.t) ** Sapling_state.Id.(ID.t)]
[sapling_state, id] in
let sapling_state := Sapling_state.IdSet.(_Set.S.add) id sapling_state in
t.with_sapling_state sapling_state set
end.
Definition diff_value (set1 : t) (set2 : t) : t :=
let big_map :=
Big_map.IdSet.(_Set.S.diff_value) set1.(t.big_map) set2.(t.big_map) in
let sapling_state :=
Sapling_state.IdSet.(_Set.S.diff_value) set1.(t.sapling_state)
set2.(t.sapling_state) in
{| t.big_map := big_map; t.sapling_state := sapling_state; |}.
Definition fold {i acc : Set}
(kind_value : kind) (f_value : i → acc → acc) (set : t) (acc_value : acc)
: acc :=
match (kind_value, f_value, set) with
| (Big_map, f_value, {| t.big_map := big_map |}) ⇒
let '[big_map, f_value] :=
cast [Big_map.IdSet.(_Set.S.t) ** Big_map.Id.(ID.t) → acc → acc]
[big_map, f_value] in
Big_map.IdSet.(_Set.S.fold) f_value big_map acc_value
| (Sapling_state, f_value, {| t.sapling_state := sapling_state |}) ⇒
let '[sapling_state, f_value] :=
cast
[Sapling_state.IdSet.(_Set.S.t) **
Sapling_state.Id.(ID.t) → acc → acc] [sapling_state, f_value] in
Sapling_state.IdSet.(_Set.S.fold) f_value sapling_state acc_value
end.
Definition fold_all {A : Set} (f_value : fold_f A) (set : t) (acc_value : A)
: A :=
List.fold_left
(fun (acc_value : A) ⇒
fun (function_parameter : int × ex) ⇒
let '(_, Ex_Kind kind_value) := function_parameter in
let 'existT _ __Ex_Kind kind_value :=
cast_exists (Es := Set) (fun __Ex_Kind ⇒ kind) kind_value in
(fold (i := __Ex_Kind)) kind_value (f_value.(fold_f.f) kind_value) set
acc_value) acc_value all.
End IdSet.