🔥 Carbonated_map.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.Carbonated_map_costs.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Module S.
Record signature {t : Set → Set} {key context : Set} : Set := {
t := t;
key := key;
context := context;
empty : ∀ {a : Set}, t a;
singleton : ∀ {a : Set}, key → a → t a;
size_value : ∀ {a : Set}, t a → int;
find : ∀ {a : Set}, context → key → t a → M? (option a × context);
update :
∀ {a : Set},
context → key → (context → option a → M? (option a × context)) →
t a → M? (t a × context);
to_list : ∀ {a : Set}, context → t a → M? (list (key × a) × context);
of_list :
∀ {a : Set},
context → (context → a → a → M? (a × context)) → list (key × a) →
M? (t a × context);
merge :
∀ {a : Set},
context → (context → a → a → M? (a × context)) → t a → t a →
M? (t a × context);
map_e :
∀ {a b : Set},
context → (context → key → a → M? (b × context)) → t a →
M? (t b × context);
fold_e :
∀ {state value : Set},
context → (context → state → key → value → M? (state × context)) →
state → t value → M? (state × context);
fold_es :
∀ {state value : Set},
context → (context → state → key → value → M? (state × context)) →
state → t value → M? (state × context);
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _}.
Module GAS.
Record signature {context : Set} : Set := {
context := context;
consume : context → Saturation_repr.t → M? context;
}.
End GAS.
Definition GAS := @GAS.signature.
Arguments GAS {_}.
Module COMPARABLE.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Carbonated_map_costs.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Module S.
Record signature {t : Set → Set} {key context : Set} : Set := {
t := t;
key := key;
context := context;
empty : ∀ {a : Set}, t a;
singleton : ∀ {a : Set}, key → a → t a;
size_value : ∀ {a : Set}, t a → int;
find : ∀ {a : Set}, context → key → t a → M? (option a × context);
update :
∀ {a : Set},
context → key → (context → option a → M? (option a × context)) →
t a → M? (t a × context);
to_list : ∀ {a : Set}, context → t a → M? (list (key × a) × context);
of_list :
∀ {a : Set},
context → (context → a → a → M? (a × context)) → list (key × a) →
M? (t a × context);
merge :
∀ {a : Set},
context → (context → a → a → M? (a × context)) → t a → t a →
M? (t a × context);
map_e :
∀ {a b : Set},
context → (context → key → a → M? (b × context)) → t a →
M? (t b × context);
fold_e :
∀ {state value : Set},
context → (context → state → key → value → M? (state × context)) →
state → t value → M? (state × context);
fold_es :
∀ {state value : Set},
context → (context → state → key → value → M? (state × context)) →
state → t value → M? (state × context);
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _}.
Module GAS.
Record signature {context : Set} : Set := {
context := context;
consume : context → Saturation_repr.t → M? context;
}.
End GAS.
Definition GAS := @GAS.signature.
Arguments GAS {_}.
Module COMPARABLE.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
[compare_cost k] returns the cost of comparing the given key [k] with
another value of the same type.
compare_cost : t → Saturation_repr.t;
}.
End COMPARABLE.
Definition COMPARABLE := @COMPARABLE.signature.
Arguments COMPARABLE {_}.
Module S_builder.
Record signature {t : Set → Set} {key : Set} : Set := {
t := t;
key := key;
Make :
∀ {G_context : Set},
∀ (G : GAS (context := G_context)),
S (t := fun (a : Set) ⇒ t a) (key := key) (context := G.(GAS.context));
}.
End S_builder.
Definition S_builder := @S_builder.signature.
Arguments S_builder {_ _}.
Module Make_builder.
Class FArgs {C_t : Set} := {
C : COMPARABLE (t := C_t);
}.
Arguments Build_FArgs {_}.
Definition M `{FArgs} :=
Map.Make
{|
Compare.COMPARABLE.compare := C.(COMPARABLE.compare)
|}.
Module t.
Record record `{FArgs} {a : Set} : Set := Build {
map : M.(Map.S.t) a;
size : int;
}.
Arguments record {_ _}.
Definition with_map `{FArgs} {t_a} map (r : record t_a) :=
Build _ _ t_a map r.(size).
Definition with_size `{FArgs} {t_a} size (r : record t_a) :=
Build _ _ t_a r.(map) size.
End t.
Definition t `{FArgs} := t.record.
Module Make.
Class FArgs `{FArgs} {G_context : Set} := {
G : GAS (context := G_context);
}.
Arguments Build_FArgs {_ _ _}.
Definition key `{FArgs} : Set := C.(COMPARABLE.t).
Definition context `{FArgs} : Set := G.(GAS.context).
Definition empty `{FArgs} {A : Set} : t A :=
{| t.map := M.(Map.S.empty); t.size := 0; |}.
Definition singleton `{FArgs} {A : Set}
(key_value : C.(COMPARABLE.t)) (value_value : A) : t A :=
{| t.map := M.(Map.S.singleton) key_value value_value; t.size := 1; |}.
Definition size_value `{FArgs} {A : Set} (function_parameter : t A) : int :=
let '{| t.size := size_value |} := function_parameter in
size_value.
Definition find_cost `{FArgs}
(key_value : C.(COMPARABLE.t)) (size_value : int)
: Carbonated_map_costs.cost :=
Carbonated_map_costs.find_cost (C.(COMPARABLE.compare_cost) key_value)
size_value.
Definition update_cost `{FArgs}
(key_value : C.(COMPARABLE.t)) (size_value : int)
: Carbonated_map_costs.cost :=
Carbonated_map_costs.update_cost (C.(COMPARABLE.compare_cost) key_value)
size_value.
Definition find `{FArgs} {A : Set}
(ctxt : G.(GAS.context)) (key_value : C.(COMPARABLE.t))
(function_parameter : t A) : M? (option A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt := G.(GAS.consume) ctxt (find_cost key_value size_value) in
return? ((M.(Map.S.find) key_value map), ctxt).
Definition update `{FArgs} {A : Set}
(ctxt : G.(GAS.context)) (key_value : C.(COMPARABLE.t))
(f_value : G.(GAS.context) → option A → M? (option A × G.(GAS.context)))
(function_parameter : t A) : M? (t A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let find_cost := find_cost key_value size_value in
let update_cost := update_cost key_value size_value in
let? ctxt := G.(GAS.consume) ctxt find_cost in
let old_val_opt := M.(Map.S.find) key_value map in
let? '(new_val_opt, ctxt) := f_value ctxt old_val_opt in
match (old_val_opt, new_val_opt) with
| (Some _, Some new_val) ⇒
let? ctxt := G.(GAS.consume) ctxt update_cost in
return?
({| t.map := M.(Map.S.add) key_value new_val map;
t.size := size_value; |}, ctxt)
| (Some _, None) ⇒
let? ctxt := G.(GAS.consume) ctxt update_cost in
return?
({| t.map := M.(Map.S.remove) key_value map;
t.size := size_value -i 1; |}, ctxt)
| (None, Some new_val) ⇒
let? ctxt := G.(GAS.consume) ctxt update_cost in
return?
({| t.map := M.(Map.S.add) key_value new_val map;
t.size := size_value +i 1; |}, ctxt)
| (None, None) ⇒
return? ({| t.map := map; t.size := size_value; |}, ctxt)
end.
Definition to_list `{FArgs} {A : Set}
(ctxt : G.(GAS.context)) (function_parameter : t A)
: M? (list (C.(COMPARABLE.t) × A) × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt :=
G.(GAS.consume) ctxt (Carbonated_map_costs.fold_cost size_value) in
return? ((M.(Map.S.bindings) map), ctxt).
Definition add `{FArgs} {A : Set}
(ctxt : G.(GAS.context))
(merge_overlap : G.(GAS.context) → A → A → M? (A × G.(GAS.context)))
(key_value : C.(COMPARABLE.t)) (value_value : A)
(function_parameter : t A) : M? (t A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt := G.(GAS.consume) ctxt (find_cost key_value size_value) in
let? ctxt := G.(GAS.consume) ctxt (update_cost key_value size_value) in
match M.(Map.S.find) key_value map with
| Some old_val ⇒
let? '(new_value, ctxt) := merge_overlap ctxt old_val value_value in
return?
({| t.map := M.(Map.S.add) key_value new_value map;
t.size := size_value; |}, ctxt)
| None ⇒
Pervasives.Ok
({| t.map := M.(Map.S.add) key_value value_value map;
t.size := size_value +i 1; |}, ctxt)
end.
Definition add_key_values_to_map `{FArgs} {A : Set}
(ctxt : G.(GAS.context))
(merge_overlap : G.(GAS.context) → A → A → M? (A × G.(GAS.context)))
(map : t A) (key_values : list (C.(COMPARABLE.t) × A))
: M? (t A × G.(GAS.context)) :=
let accum (function_parameter : t A × G.(GAS.context))
: C.(COMPARABLE.t) × A → M? (t A × G.(GAS.context)) :=
let '(map, ctxt) := function_parameter in
fun (function_parameter : C.(COMPARABLE.t) × A) ⇒
let '(key_value, value_value) := function_parameter in
add ctxt merge_overlap key_value value_value map in
List.fold_left_e accum (map, ctxt) key_values.
Definition of_list `{FArgs} {A : Set}
(ctxt : G.(GAS.context))
(merge_overlap : G.(GAS.context) → A → A → M? (A × G.(GAS.context)))
: list (C.(COMPARABLE.t) × A) → M? (t A × G.(GAS.context)) :=
add_key_values_to_map ctxt merge_overlap empty.
Definition merge `{FArgs} {A : Set}
(ctxt : G.(GAS.context))
(merge_overlap : G.(GAS.context) → A → A → M? (A × G.(GAS.context)))
(map1 : t A) (function_parameter : t A) : M? (t A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt :=
G.(GAS.consume) ctxt (Carbonated_map_costs.fold_cost size_value) in
M.(Map.S.fold_e)
(fun (key_value : C.(COMPARABLE.t)) ⇒
fun (value_value : A) ⇒
fun (function_parameter : t A × G.(GAS.context)) ⇒
let '(map, ctxt) := function_parameter in
add ctxt merge_overlap key_value value_value map) map (map1, ctxt).
Definition fold_e `{FArgs} {A B : Set}
(ctxt : G.(GAS.context))
(f_value :
G.(GAS.context) → A → C.(COMPARABLE.t) → B →
M? (A × G.(GAS.context))) (empty : A) (function_parameter : t B)
: M? (A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt :=
G.(GAS.consume) ctxt (Carbonated_map_costs.fold_cost size_value) in
M.(Map.S.fold_e)
(fun (key_value : C.(COMPARABLE.t)) ⇒
fun (value_value : B) ⇒
fun (function_parameter : A × G.(GAS.context)) ⇒
let '(acc_value, ctxt) := function_parameter in
f_value ctxt acc_value key_value value_value) map (empty, ctxt).
Definition fold_es `{FArgs} {A B : Set}
(ctxt : G.(GAS.context))
(f_value :
G.(GAS.context) → A → C.(COMPARABLE.t) → B →
M? (A × G.(GAS.context))) (empty : A) (function_parameter : t B)
: M? (A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt :=
G.(GAS.consume) ctxt (Carbonated_map_costs.fold_cost size_value) in
M.(Map.S.fold_es)
(fun (key_value : C.(COMPARABLE.t)) ⇒
fun (value_value : B) ⇒
fun (function_parameter : A × G.(GAS.context)) ⇒
let '(acc_value, ctxt) := function_parameter in
f_value ctxt acc_value key_value value_value) map (empty, ctxt).
Definition map_e `{FArgs} {A B : Set}
(ctxt : G.(GAS.context))
(f_value :
G.(GAS.context) → C.(COMPARABLE.t) → A → M? (B × G.(GAS.context)))
(function_parameter : t A) : M? (t B × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? '(map, ctxt) :=
fold_e ctxt
(fun (ctxt : G.(GAS.context)) ⇒
fun (map : M.(Map.S.t) B) ⇒
fun (key_value : C.(COMPARABLE.t)) ⇒
fun (value_value : A) ⇒
let? '(value_value, ctxt) :=
f_value ctxt key_value value_value in
let? ctxt :=
G.(GAS.consume) ctxt (update_cost key_value size_value) in
return? ((M.(Map.S.add) key_value value_value map), ctxt))
M.(Map.S.empty) {| t.map := map; t.size := size_value; |} in
return? ({| t.map := map; t.size := size_value; |}, ctxt).
(* Make *)
Definition functor `{FArgs} :=
{|
S.empty _ := empty;
S.singleton _ := singleton;
S.size_value _ := size_value;
S.find _ := find;
S.update _ := update;
S.to_list _ := to_list;
S.of_list _ := of_list;
S.merge _ := merge;
S.map_e _ _ := map_e;
S.fold_e _ _ := fold_e;
S.fold_es _ _ := fold_es
|}.
End Make.
Definition Make `{FArgs} {G_context : Set} (G : GAS (context := G_context))
: S (t := fun (a : Set) ⇒ t a) (key := C.(COMPARABLE.t))
(context := G.(GAS.context)) :=
let '_ := Make.Build_FArgs G in
Make.functor.
(* Make_builder *)
Definition functor `{FArgs} :=
{|
S_builder.Make _ := Make
|}.
End Make_builder.
Definition Make_builder {C_t : Set} (C : COMPARABLE (t := C_t))
: S_builder (t := _) (key := C.(COMPARABLE.t)) :=
let '_ := Make_builder.Build_FArgs C in
Make_builder.functor.
Module Make.
Class FArgs {G_context C_t : Set} := {
G : GAS (context := G_context);
C : COMPARABLE (t := C_t);
}.
Arguments Build_FArgs {_ _}.
Definition M `{FArgs} := Make_builder C.
Definition t `{FArgs} (a : Set) : Set := M.(S_builder.t) a.
Definition M_Make_include `{FArgs} := M.(S_builder.Make) G.
}.
End COMPARABLE.
Definition COMPARABLE := @COMPARABLE.signature.
Arguments COMPARABLE {_}.
Module S_builder.
Record signature {t : Set → Set} {key : Set} : Set := {
t := t;
key := key;
Make :
∀ {G_context : Set},
∀ (G : GAS (context := G_context)),
S (t := fun (a : Set) ⇒ t a) (key := key) (context := G.(GAS.context));
}.
End S_builder.
Definition S_builder := @S_builder.signature.
Arguments S_builder {_ _}.
Module Make_builder.
Class FArgs {C_t : Set} := {
C : COMPARABLE (t := C_t);
}.
Arguments Build_FArgs {_}.
Definition M `{FArgs} :=
Map.Make
{|
Compare.COMPARABLE.compare := C.(COMPARABLE.compare)
|}.
Module t.
Record record `{FArgs} {a : Set} : Set := Build {
map : M.(Map.S.t) a;
size : int;
}.
Arguments record {_ _}.
Definition with_map `{FArgs} {t_a} map (r : record t_a) :=
Build _ _ t_a map r.(size).
Definition with_size `{FArgs} {t_a} size (r : record t_a) :=
Build _ _ t_a r.(map) size.
End t.
Definition t `{FArgs} := t.record.
Module Make.
Class FArgs `{FArgs} {G_context : Set} := {
G : GAS (context := G_context);
}.
Arguments Build_FArgs {_ _ _}.
Definition key `{FArgs} : Set := C.(COMPARABLE.t).
Definition context `{FArgs} : Set := G.(GAS.context).
Definition empty `{FArgs} {A : Set} : t A :=
{| t.map := M.(Map.S.empty); t.size := 0; |}.
Definition singleton `{FArgs} {A : Set}
(key_value : C.(COMPARABLE.t)) (value_value : A) : t A :=
{| t.map := M.(Map.S.singleton) key_value value_value; t.size := 1; |}.
Definition size_value `{FArgs} {A : Set} (function_parameter : t A) : int :=
let '{| t.size := size_value |} := function_parameter in
size_value.
Definition find_cost `{FArgs}
(key_value : C.(COMPARABLE.t)) (size_value : int)
: Carbonated_map_costs.cost :=
Carbonated_map_costs.find_cost (C.(COMPARABLE.compare_cost) key_value)
size_value.
Definition update_cost `{FArgs}
(key_value : C.(COMPARABLE.t)) (size_value : int)
: Carbonated_map_costs.cost :=
Carbonated_map_costs.update_cost (C.(COMPARABLE.compare_cost) key_value)
size_value.
Definition find `{FArgs} {A : Set}
(ctxt : G.(GAS.context)) (key_value : C.(COMPARABLE.t))
(function_parameter : t A) : M? (option A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt := G.(GAS.consume) ctxt (find_cost key_value size_value) in
return? ((M.(Map.S.find) key_value map), ctxt).
Definition update `{FArgs} {A : Set}
(ctxt : G.(GAS.context)) (key_value : C.(COMPARABLE.t))
(f_value : G.(GAS.context) → option A → M? (option A × G.(GAS.context)))
(function_parameter : t A) : M? (t A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let find_cost := find_cost key_value size_value in
let update_cost := update_cost key_value size_value in
let? ctxt := G.(GAS.consume) ctxt find_cost in
let old_val_opt := M.(Map.S.find) key_value map in
let? '(new_val_opt, ctxt) := f_value ctxt old_val_opt in
match (old_val_opt, new_val_opt) with
| (Some _, Some new_val) ⇒
let? ctxt := G.(GAS.consume) ctxt update_cost in
return?
({| t.map := M.(Map.S.add) key_value new_val map;
t.size := size_value; |}, ctxt)
| (Some _, None) ⇒
let? ctxt := G.(GAS.consume) ctxt update_cost in
return?
({| t.map := M.(Map.S.remove) key_value map;
t.size := size_value -i 1; |}, ctxt)
| (None, Some new_val) ⇒
let? ctxt := G.(GAS.consume) ctxt update_cost in
return?
({| t.map := M.(Map.S.add) key_value new_val map;
t.size := size_value +i 1; |}, ctxt)
| (None, None) ⇒
return? ({| t.map := map; t.size := size_value; |}, ctxt)
end.
Definition to_list `{FArgs} {A : Set}
(ctxt : G.(GAS.context)) (function_parameter : t A)
: M? (list (C.(COMPARABLE.t) × A) × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt :=
G.(GAS.consume) ctxt (Carbonated_map_costs.fold_cost size_value) in
return? ((M.(Map.S.bindings) map), ctxt).
Definition add `{FArgs} {A : Set}
(ctxt : G.(GAS.context))
(merge_overlap : G.(GAS.context) → A → A → M? (A × G.(GAS.context)))
(key_value : C.(COMPARABLE.t)) (value_value : A)
(function_parameter : t A) : M? (t A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt := G.(GAS.consume) ctxt (find_cost key_value size_value) in
let? ctxt := G.(GAS.consume) ctxt (update_cost key_value size_value) in
match M.(Map.S.find) key_value map with
| Some old_val ⇒
let? '(new_value, ctxt) := merge_overlap ctxt old_val value_value in
return?
({| t.map := M.(Map.S.add) key_value new_value map;
t.size := size_value; |}, ctxt)
| None ⇒
Pervasives.Ok
({| t.map := M.(Map.S.add) key_value value_value map;
t.size := size_value +i 1; |}, ctxt)
end.
Definition add_key_values_to_map `{FArgs} {A : Set}
(ctxt : G.(GAS.context))
(merge_overlap : G.(GAS.context) → A → A → M? (A × G.(GAS.context)))
(map : t A) (key_values : list (C.(COMPARABLE.t) × A))
: M? (t A × G.(GAS.context)) :=
let accum (function_parameter : t A × G.(GAS.context))
: C.(COMPARABLE.t) × A → M? (t A × G.(GAS.context)) :=
let '(map, ctxt) := function_parameter in
fun (function_parameter : C.(COMPARABLE.t) × A) ⇒
let '(key_value, value_value) := function_parameter in
add ctxt merge_overlap key_value value_value map in
List.fold_left_e accum (map, ctxt) key_values.
Definition of_list `{FArgs} {A : Set}
(ctxt : G.(GAS.context))
(merge_overlap : G.(GAS.context) → A → A → M? (A × G.(GAS.context)))
: list (C.(COMPARABLE.t) × A) → M? (t A × G.(GAS.context)) :=
add_key_values_to_map ctxt merge_overlap empty.
Definition merge `{FArgs} {A : Set}
(ctxt : G.(GAS.context))
(merge_overlap : G.(GAS.context) → A → A → M? (A × G.(GAS.context)))
(map1 : t A) (function_parameter : t A) : M? (t A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt :=
G.(GAS.consume) ctxt (Carbonated_map_costs.fold_cost size_value) in
M.(Map.S.fold_e)
(fun (key_value : C.(COMPARABLE.t)) ⇒
fun (value_value : A) ⇒
fun (function_parameter : t A × G.(GAS.context)) ⇒
let '(map, ctxt) := function_parameter in
add ctxt merge_overlap key_value value_value map) map (map1, ctxt).
Definition fold_e `{FArgs} {A B : Set}
(ctxt : G.(GAS.context))
(f_value :
G.(GAS.context) → A → C.(COMPARABLE.t) → B →
M? (A × G.(GAS.context))) (empty : A) (function_parameter : t B)
: M? (A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt :=
G.(GAS.consume) ctxt (Carbonated_map_costs.fold_cost size_value) in
M.(Map.S.fold_e)
(fun (key_value : C.(COMPARABLE.t)) ⇒
fun (value_value : B) ⇒
fun (function_parameter : A × G.(GAS.context)) ⇒
let '(acc_value, ctxt) := function_parameter in
f_value ctxt acc_value key_value value_value) map (empty, ctxt).
Definition fold_es `{FArgs} {A B : Set}
(ctxt : G.(GAS.context))
(f_value :
G.(GAS.context) → A → C.(COMPARABLE.t) → B →
M? (A × G.(GAS.context))) (empty : A) (function_parameter : t B)
: M? (A × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? ctxt :=
G.(GAS.consume) ctxt (Carbonated_map_costs.fold_cost size_value) in
M.(Map.S.fold_es)
(fun (key_value : C.(COMPARABLE.t)) ⇒
fun (value_value : B) ⇒
fun (function_parameter : A × G.(GAS.context)) ⇒
let '(acc_value, ctxt) := function_parameter in
f_value ctxt acc_value key_value value_value) map (empty, ctxt).
Definition map_e `{FArgs} {A B : Set}
(ctxt : G.(GAS.context))
(f_value :
G.(GAS.context) → C.(COMPARABLE.t) → A → M? (B × G.(GAS.context)))
(function_parameter : t A) : M? (t B × G.(GAS.context)) :=
let '{| t.map := map; t.size := size_value |} := function_parameter in
let? '(map, ctxt) :=
fold_e ctxt
(fun (ctxt : G.(GAS.context)) ⇒
fun (map : M.(Map.S.t) B) ⇒
fun (key_value : C.(COMPARABLE.t)) ⇒
fun (value_value : A) ⇒
let? '(value_value, ctxt) :=
f_value ctxt key_value value_value in
let? ctxt :=
G.(GAS.consume) ctxt (update_cost key_value size_value) in
return? ((M.(Map.S.add) key_value value_value map), ctxt))
M.(Map.S.empty) {| t.map := map; t.size := size_value; |} in
return? ({| t.map := map; t.size := size_value; |}, ctxt).
(* Make *)
Definition functor `{FArgs} :=
{|
S.empty _ := empty;
S.singleton _ := singleton;
S.size_value _ := size_value;
S.find _ := find;
S.update _ := update;
S.to_list _ := to_list;
S.of_list _ := of_list;
S.merge _ := merge;
S.map_e _ _ := map_e;
S.fold_e _ _ := fold_e;
S.fold_es _ _ := fold_es
|}.
End Make.
Definition Make `{FArgs} {G_context : Set} (G : GAS (context := G_context))
: S (t := fun (a : Set) ⇒ t a) (key := C.(COMPARABLE.t))
(context := G.(GAS.context)) :=
let '_ := Make.Build_FArgs G in
Make.functor.
(* Make_builder *)
Definition functor `{FArgs} :=
{|
S_builder.Make _ := Make
|}.
End Make_builder.
Definition Make_builder {C_t : Set} (C : COMPARABLE (t := C_t))
: S_builder (t := _) (key := C.(COMPARABLE.t)) :=
let '_ := Make_builder.Build_FArgs C in
Make_builder.functor.
Module Make.
Class FArgs {G_context C_t : Set} := {
G : GAS (context := G_context);
C : COMPARABLE (t := C_t);
}.
Arguments Build_FArgs {_ _}.
Definition M `{FArgs} := Make_builder C.
Definition t `{FArgs} (a : Set) : Set := M.(S_builder.t) a.
Definition M_Make_include `{FArgs} := M.(S_builder.Make) G.
Inclusion of the module [M_Make_include]
Definition key `{FArgs} := M_Make_include.(S.key).
Definition context `{FArgs} := M_Make_include.(S.context).
Definition empty `{FArgs} {a : Set} := M_Make_include.(S.empty) (a := a).
Definition singleton `{FArgs} {a : Set} :=
M_Make_include.(S.singleton) (a := a).
Definition size_value `{FArgs} {a : Set} :=
M_Make_include.(S.size_value) (a := a).
Definition find `{FArgs} {a : Set} := M_Make_include.(S.find) (a := a).
Definition update `{FArgs} {a : Set} := M_Make_include.(S.update) (a := a).
Definition to_list `{FArgs} {a : Set} := M_Make_include.(S.to_list) (a := a).
Definition of_list `{FArgs} {a : Set} := M_Make_include.(S.of_list) (a := a).
Definition merge `{FArgs} {a : Set} := M_Make_include.(S.merge) (a := a).
Definition map_e `{FArgs} {a b : Set} :=
M_Make_include.(S.map_e) (a := a) (b := b).
Definition fold_e `{FArgs} {state value : Set} :=
M_Make_include.(S.fold_e) (state := state) (value := value).
Definition fold_es `{FArgs} {state value : Set} :=
M_Make_include.(S.fold_es) (state := state) (value := value).
(* Make *)
Definition functor `{FArgs} :=
{|
S.empty _ := empty;
S.singleton _ := singleton;
S.size_value _ := size_value;
S.find _ := find;
S.update _ := update;
S.to_list _ := to_list;
S.of_list _ := of_list;
S.merge _ := merge;
S.map_e _ _ := map_e;
S.fold_e _ _ := fold_e;
S.fold_es _ _ := fold_es
|}.
End Make.
Definition Make {G_context C_t : Set}
(G : GAS (context := G_context)) (C : COMPARABLE (t := C_t))
: S (t := _) (key := C.(COMPARABLE.t)) (context := G.(GAS.context)) :=
let '_ := Make.Build_FArgs G C in
Make.functor.
Definition context `{FArgs} := M_Make_include.(S.context).
Definition empty `{FArgs} {a : Set} := M_Make_include.(S.empty) (a := a).
Definition singleton `{FArgs} {a : Set} :=
M_Make_include.(S.singleton) (a := a).
Definition size_value `{FArgs} {a : Set} :=
M_Make_include.(S.size_value) (a := a).
Definition find `{FArgs} {a : Set} := M_Make_include.(S.find) (a := a).
Definition update `{FArgs} {a : Set} := M_Make_include.(S.update) (a := a).
Definition to_list `{FArgs} {a : Set} := M_Make_include.(S.to_list) (a := a).
Definition of_list `{FArgs} {a : Set} := M_Make_include.(S.of_list) (a := a).
Definition merge `{FArgs} {a : Set} := M_Make_include.(S.merge) (a := a).
Definition map_e `{FArgs} {a b : Set} :=
M_Make_include.(S.map_e) (a := a) (b := b).
Definition fold_e `{FArgs} {state value : Set} :=
M_Make_include.(S.fold_e) (state := state) (value := value).
Definition fold_es `{FArgs} {state value : Set} :=
M_Make_include.(S.fold_es) (state := state) (value := value).
(* Make *)
Definition functor `{FArgs} :=
{|
S.empty _ := empty;
S.singleton _ := singleton;
S.size_value _ := size_value;
S.find _ := find;
S.update _ := update;
S.to_list _ := to_list;
S.of_list _ := of_list;
S.merge _ := merge;
S.map_e _ _ := map_e;
S.fold_e _ _ := fold_e;
S.fold_es _ _ := fold_es
|}.
End Make.
Definition Make {G_context C_t : Set}
(G : GAS (context := G_context)) (C : COMPARABLE (t := C_t))
: S (t := _) (key := C.(COMPARABLE.t)) (context := G.(GAS.context)) :=
let '_ := Make.Build_FArgs G C in
Make.functor.