📜 Bounded_history_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Module NAME.
Record signature : Set := {
name : string;
_sig_NAME : unit;
}.
End NAME.
Definition NAME := NAME.signature.
Module KEY.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
pp : Format.formatter → t → unit;
encoding : Data_encoding.t t;
_sig_KEY : unit;
}.
End KEY.
Definition KEY := @KEY.signature.
Arguments KEY {_}.
Module VALUE.
Record signature {t : Set} : Set := {
t := t;
equal : t → t → bool;
pp : Format.formatter → t → unit;
encoding : Data_encoding.t t;
}.
End VALUE.
Definition VALUE := @VALUE.signature.
Arguments VALUE {_}.
Module S.
Record signature {t key value : Set} : Set := {
t := t;
key := key;
value := value;
empty : int64 → t;
encoding : Data_encoding.t t;
pp : Format.formatter → t → unit;
find : key → t → option value;
remember : key → value → t → M? t;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _}.
Module Make.
Class FArgs {Key_t Value_t : Set} := {
Name : NAME;
Key : KEY (t := Key_t);
Value : VALUE (t := Value_t);
}.
Arguments Build_FArgs {_ _}.
Definition key `{FArgs} : Set := Key.(KEY.t).
Definition value `{FArgs} : Set := Value.(VALUE.t).
Definition Int64_map `{FArgs} :=
Map.Make
{|
Compare.COMPARABLE.compare := Int64.compare
|}.
Definition Map `{FArgs} :=
Map.Make
{|
Compare.COMPARABLE.compare := Key.(KEY.compare)
|}.
Module t.
Record record `{FArgs} : Set := Build {
events : Map.(Map.S.t) value;
sequence : Int64_map.(Map.S.t) key;
capacity : int64;
next_index : int64;
oldest_index : int64;
size : int64;
}.
Definition with_events `{FArgs} events (r : record) :=
Build _ _ _ events r.(sequence) r.(capacity) r.(next_index)
r.(oldest_index) r.(size).
Definition with_sequence `{FArgs} sequence (r : record) :=
Build _ _ _ r.(events) sequence r.(capacity) r.(next_index)
r.(oldest_index) r.(size).
Definition with_capacity `{FArgs} capacity (r : record) :=
Build _ _ _ r.(events) r.(sequence) capacity r.(next_index)
r.(oldest_index) r.(size).
Definition with_next_index `{FArgs} next_index (r : record) :=
Build _ _ _ r.(events) r.(sequence) r.(capacity) next_index
r.(oldest_index) r.(size).
Definition with_oldest_index `{FArgs} oldest_index (r : record) :=
Build _ _ _ r.(events) r.(sequence) r.(capacity) r.(next_index)
oldest_index r.(size).
Definition with_size `{FArgs} size (r : record) :=
Build _ _ _ r.(events) r.(sequence) r.(capacity) r.(next_index)
r.(oldest_index) size.
End t.
Definition t `{FArgs} := t.record.
Definition encoding `{FArgs} : Data_encoding.t t :=
let events_encoding :=
Data_encoding.conv Map.(Map.S.bindings)
(fun (l_value : list (Key.(KEY.t) × Value.(VALUE.t))) ⇒
Map.(Map.S.add_seq) (List.to_seq l_value) Map.(Map.S.empty)) None
(Data_encoding.list_value None
(Data_encoding.tup2 Key.(KEY.encoding) Value.(VALUE.encoding))) in
let sequence_encoding :=
Data_encoding.conv Int64_map.(Map.S.bindings)
(List.fold_left
(fun (m_value : Int64_map.(Map.S.t) Key.(KEY.t)) ⇒
fun (function_parameter : Int64.t × Key.(KEY.t)) ⇒
let '(k_value, v_value) := function_parameter in
Int64_map.(Map.S.add) k_value v_value m_value)
Int64_map.(Map.S.empty)) None
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.int64_value Key.(KEY.encoding))) in
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.events := events;
t.sequence := sequence_value;
t.capacity := capacity;
t.next_index := next_index;
t.oldest_index := oldest_index;
t.size := size_value
|} := function_parameter in
(events, sequence_value, capacity, next_index, oldest_index, size_value))
(fun (function_parameter :
Map.(Map.S.t) value × Int64_map.(Map.S.t) key × int64 × int64 × int64 ×
int64) ⇒
let
'(events, sequence_value, capacity, next_index, oldest_index,
size_value) := function_parameter in
{| t.events := events; t.sequence := sequence_value;
t.capacity := capacity; t.next_index := next_index;
t.oldest_index := oldest_index; t.size := size_value; |}) None
(Data_encoding.obj6 (Data_encoding.req None None "events" events_encoding)
(Data_encoding.req None None "sequence" sequence_encoding)
(Data_encoding.req None None "capacity" Data_encoding.int64_value)
(Data_encoding.req None None "next_index" Data_encoding.int64_value)
(Data_encoding.req None None "oldest_index" Data_encoding.int64_value)
(Data_encoding.req None None "size" Data_encoding.int64_value)).
Definition pp `{FArgs} (fmt : Format.formatter) (function_parameter : t)
: unit :=
let '{|
t.events := events;
t.sequence := sequence_value;
t.capacity := capacity;
t.next_index := next_index;
t.oldest_index := oldest_index;
t.size := size_value
|} := function_parameter in
(fun (bindings : list (Key.(KEY.t) × value)) ⇒
(fun (sequence_bindings : list (Int64.t × key)) ⇒
let pp_binding
(fmt : Format.formatter)
(function_parameter : Key.(KEY.t) × Value.(VALUE.t)) : unit :=
let '(hash_value, history_proof) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " -> "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))
"@[%a -> %a@;@]") Key.(KEY.pp) hash_value Value.(VALUE.pp)
history_proof in
let pp_sequence_binding
(fmt : Format.formatter) (function_parameter : int64 × Key.(KEY.t))
: unit :=
let '(counter, hash_value) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " -> "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))
"@[%s -> %a@;@]") (Int64.to_string counter) Key.(KEY.pp)
hash_value in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hov 2>"
CamlinternalFormatBasics.End_of_format) "<hov 2>"))
(CamlinternalFormatBasics.String_literal "History:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal " { capacity: "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
" current size: "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
" oldest index: "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal
";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1
0)
(CamlinternalFormatBasics.String_literal
" next_index : "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal
";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1 0)
(CamlinternalFormatBasics.String_literal
" bindings: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal
";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1 0)
(CamlinternalFormatBasics.String_literal
" sequence: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
"; }"
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))))))))))))))))))))))
"@[<hov 2>History:@; { capacity: %Ld;@; current size: %Ld;@; oldest index: %Ld;@; next_index : %Ld;@; bindings: %a;@; sequence: %a; }@]")
capacity size_value oldest_index next_index
(Format.pp_print_list None pp_binding) bindings
(Format.pp_print_list None pp_sequence_binding) sequence_bindings)
(Int64_map.(Map.S.bindings) sequence_value))
(Map.(Map.S.bindings) events).
Definition empty `{FArgs} (capacity : int64) : t :=
let next_index := 0 in
{| t.events := Map.(Map.S.empty); t.sequence := Int64_map.(Map.S.empty);
t.capacity := capacity; t.next_index := next_index;
t.oldest_index := next_index; t.size := 0; |}.
Module Key_bound_to_different_value.
Record record `{FArgs} : Set := Build {
key : key;
existing_value : value;
given_value : value;
}.
Definition with_key `{FArgs} key (r : record) :=
Build _ _ _ key r.(existing_value) r.(given_value).
Definition with_existing_value `{FArgs} existing_value (r : record) :=
Build _ _ _ r.(key) existing_value r.(given_value).
Definition with_given_value `{FArgs} given_value (r : record) :=
Build _ _ _ r.(key) r.(existing_value) given_value.
End Key_bound_to_different_value.
Definition Key_bound_to_different_value `{FArgs} :=
Key_bound_to_different_value.record.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Module NAME.
Record signature : Set := {
name : string;
_sig_NAME : unit;
}.
End NAME.
Definition NAME := NAME.signature.
Module KEY.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
pp : Format.formatter → t → unit;
encoding : Data_encoding.t t;
_sig_KEY : unit;
}.
End KEY.
Definition KEY := @KEY.signature.
Arguments KEY {_}.
Module VALUE.
Record signature {t : Set} : Set := {
t := t;
equal : t → t → bool;
pp : Format.formatter → t → unit;
encoding : Data_encoding.t t;
}.
End VALUE.
Definition VALUE := @VALUE.signature.
Arguments VALUE {_}.
Module S.
Record signature {t key value : Set} : Set := {
t := t;
key := key;
value := value;
empty : int64 → t;
encoding : Data_encoding.t t;
pp : Format.formatter → t → unit;
find : key → t → option value;
remember : key → value → t → M? t;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _}.
Module Make.
Class FArgs {Key_t Value_t : Set} := {
Name : NAME;
Key : KEY (t := Key_t);
Value : VALUE (t := Value_t);
}.
Arguments Build_FArgs {_ _}.
Definition key `{FArgs} : Set := Key.(KEY.t).
Definition value `{FArgs} : Set := Value.(VALUE.t).
Definition Int64_map `{FArgs} :=
Map.Make
{|
Compare.COMPARABLE.compare := Int64.compare
|}.
Definition Map `{FArgs} :=
Map.Make
{|
Compare.COMPARABLE.compare := Key.(KEY.compare)
|}.
Module t.
Record record `{FArgs} : Set := Build {
events : Map.(Map.S.t) value;
sequence : Int64_map.(Map.S.t) key;
capacity : int64;
next_index : int64;
oldest_index : int64;
size : int64;
}.
Definition with_events `{FArgs} events (r : record) :=
Build _ _ _ events r.(sequence) r.(capacity) r.(next_index)
r.(oldest_index) r.(size).
Definition with_sequence `{FArgs} sequence (r : record) :=
Build _ _ _ r.(events) sequence r.(capacity) r.(next_index)
r.(oldest_index) r.(size).
Definition with_capacity `{FArgs} capacity (r : record) :=
Build _ _ _ r.(events) r.(sequence) capacity r.(next_index)
r.(oldest_index) r.(size).
Definition with_next_index `{FArgs} next_index (r : record) :=
Build _ _ _ r.(events) r.(sequence) r.(capacity) next_index
r.(oldest_index) r.(size).
Definition with_oldest_index `{FArgs} oldest_index (r : record) :=
Build _ _ _ r.(events) r.(sequence) r.(capacity) r.(next_index)
oldest_index r.(size).
Definition with_size `{FArgs} size (r : record) :=
Build _ _ _ r.(events) r.(sequence) r.(capacity) r.(next_index)
r.(oldest_index) size.
End t.
Definition t `{FArgs} := t.record.
Definition encoding `{FArgs} : Data_encoding.t t :=
let events_encoding :=
Data_encoding.conv Map.(Map.S.bindings)
(fun (l_value : list (Key.(KEY.t) × Value.(VALUE.t))) ⇒
Map.(Map.S.add_seq) (List.to_seq l_value) Map.(Map.S.empty)) None
(Data_encoding.list_value None
(Data_encoding.tup2 Key.(KEY.encoding) Value.(VALUE.encoding))) in
let sequence_encoding :=
Data_encoding.conv Int64_map.(Map.S.bindings)
(List.fold_left
(fun (m_value : Int64_map.(Map.S.t) Key.(KEY.t)) ⇒
fun (function_parameter : Int64.t × Key.(KEY.t)) ⇒
let '(k_value, v_value) := function_parameter in
Int64_map.(Map.S.add) k_value v_value m_value)
Int64_map.(Map.S.empty)) None
(Data_encoding.list_value None
(Data_encoding.tup2 Data_encoding.int64_value Key.(KEY.encoding))) in
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.events := events;
t.sequence := sequence_value;
t.capacity := capacity;
t.next_index := next_index;
t.oldest_index := oldest_index;
t.size := size_value
|} := function_parameter in
(events, sequence_value, capacity, next_index, oldest_index, size_value))
(fun (function_parameter :
Map.(Map.S.t) value × Int64_map.(Map.S.t) key × int64 × int64 × int64 ×
int64) ⇒
let
'(events, sequence_value, capacity, next_index, oldest_index,
size_value) := function_parameter in
{| t.events := events; t.sequence := sequence_value;
t.capacity := capacity; t.next_index := next_index;
t.oldest_index := oldest_index; t.size := size_value; |}) None
(Data_encoding.obj6 (Data_encoding.req None None "events" events_encoding)
(Data_encoding.req None None "sequence" sequence_encoding)
(Data_encoding.req None None "capacity" Data_encoding.int64_value)
(Data_encoding.req None None "next_index" Data_encoding.int64_value)
(Data_encoding.req None None "oldest_index" Data_encoding.int64_value)
(Data_encoding.req None None "size" Data_encoding.int64_value)).
Definition pp `{FArgs} (fmt : Format.formatter) (function_parameter : t)
: unit :=
let '{|
t.events := events;
t.sequence := sequence_value;
t.capacity := capacity;
t.next_index := next_index;
t.oldest_index := oldest_index;
t.size := size_value
|} := function_parameter in
(fun (bindings : list (Key.(KEY.t) × value)) ⇒
(fun (sequence_bindings : list (Int64.t × key)) ⇒
let pp_binding
(fmt : Format.formatter)
(function_parameter : Key.(KEY.t) × Value.(VALUE.t)) : unit :=
let '(hash_value, history_proof) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " -> "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))
"@[%a -> %a@;@]") Key.(KEY.pp) hash_value Value.(VALUE.pp)
history_proof in
let pp_sequence_binding
(fmt : Format.formatter) (function_parameter : int64 × Key.(KEY.t))
: unit :=
let '(counter, hash_value) := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " -> "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format))))))
"@[%s -> %a@;@]") (Int64.to_string counter) Key.(KEY.pp)
hash_value in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<hov 2>"
CamlinternalFormatBasics.End_of_format) "<hov 2>"))
(CamlinternalFormatBasics.String_literal "History:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal " { capacity: "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
" current size: "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal ";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.String_literal
" oldest index: "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal
";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1
0)
(CamlinternalFormatBasics.String_literal
" next_index : "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal
";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1 0)
(CamlinternalFormatBasics.String_literal
" bindings: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal
";" % char
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break
"@;" 1 0)
(CamlinternalFormatBasics.String_literal
" sequence: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
"; }"
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))))))))))))))))))))))
"@[<hov 2>History:@; { capacity: %Ld;@; current size: %Ld;@; oldest index: %Ld;@; next_index : %Ld;@; bindings: %a;@; sequence: %a; }@]")
capacity size_value oldest_index next_index
(Format.pp_print_list None pp_binding) bindings
(Format.pp_print_list None pp_sequence_binding) sequence_bindings)
(Int64_map.(Map.S.bindings) sequence_value))
(Map.(Map.S.bindings) events).
Definition empty `{FArgs} (capacity : int64) : t :=
let next_index := 0 in
{| t.events := Map.(Map.S.empty); t.sequence := Int64_map.(Map.S.empty);
t.capacity := capacity; t.next_index := next_index;
t.oldest_index := next_index; t.size := 0; |}.
Module Key_bound_to_different_value.
Record record `{FArgs} : Set := Build {
key : key;
existing_value : value;
given_value : value;
}.
Definition with_key `{FArgs} key (r : record) :=
Build _ _ _ key r.(existing_value) r.(given_value).
Definition with_existing_value `{FArgs} existing_value (r : record) :=
Build _ _ _ r.(key) existing_value r.(given_value).
Definition with_given_value `{FArgs} given_value (r : record) :=
Build _ _ _ r.(key) r.(existing_value) given_value.
End Key_bound_to_different_value.
Definition Key_bound_to_different_value `{FArgs} :=
Key_bound_to_different_value.record.
Init function; without side-effects in Coq
Definition init_module_repr `{FArgs} : unit :=
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (Pervasives.not (String.equal Name.(NAME.name) "")) in
Error_monad.register_error_kind Error_monad.Temporary
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Bounded_history_repr."
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
".key_bound_to_different_value"
CamlinternalFormatBasics.End_of_format)))
"Bounded_history_repr.%s.key_bound_to_different_value")
Name.(NAME.name))
(Pervasives.op_caret Name.(NAME.name)
": Key already bound to a different value.")
(Pervasives.op_caret Name.(NAME.name)
(": Remember called with a key that is already bound to a different" ++
String.String "010" " value.")) None
(Data_encoding.obj3 (Data_encoding.req None None "key" Key.(KEY.encoding))
(Data_encoding.req None None "existing_value" Value.(VALUE.encoding))
(Data_encoding.req None None "given_value" Value.(VALUE.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Key_bound_to_different_value" then
let '{|
Key_bound_to_different_value.key := key_value;
Key_bound_to_different_value.existing_value := existing_value;
Key_bound_to_different_value.given_value := given_value
|} := cast Key_bound_to_different_value payload in
Some (key_value, existing_value, given_value)
else None
end)
(fun (function_parameter : key × value × value) ⇒
let '(key_value, existing_value, given_value) := function_parameter in
Build_extensible "Key_bound_to_different_value"
Key_bound_to_different_value
{| Key_bound_to_different_value.key := key_value;
Key_bound_to_different_value.existing_value := existing_value;
Key_bound_to_different_value.given_value := given_value; |}).
Definition remember `{FArgs}
(key_value : Key.(KEY.t)) (value_value : value) (t_value : t) : M? t :=
if t_value.(t.capacity) ≤i64 0 then
return? t_value
else
match
((Map.(Map.S.find) key_value t_value.(t.events)),
match Map.(Map.S.find) key_value t_value.(t.events) with
| Some value' ⇒
Pervasives.not (Value.(VALUE.equal) value_value value')
| _ ⇒ false
end) with
| (Some value', true) ⇒
Error_monad.error_value
(Build_extensible "Key_bound_to_different_value"
Key_bound_to_different_value
{| Key_bound_to_different_value.key := key_value;
Key_bound_to_different_value.existing_value := value';
Key_bound_to_different_value.given_value := value_value; |})
| (_, _) ⇒
let events := Map.(Map.S.add) key_value value_value t_value.(t.events)
in
let current_index := t_value.(t.next_index) in
let next_index := Int64.succ current_index in
let t_value :=
{| t.events := events;
t.sequence :=
Int64_map.(Map.S.add) current_index key_value t_value.(t.sequence);
t.capacity := t_value.(t.capacity); t.next_index := next_index;
t.oldest_index := t_value.(t.oldest_index);
t.size := Int64.succ t_value.(t.size); |} in
if
(t_value.(t.size) >i64 0) &&
(t_value.(t.size) ≤i64 t_value.(t.capacity))
then
return? t_value
else
let l_value := t_value.(t.oldest_index) in
match Int64_map.(Map.S.find) l_value t_value.(t.sequence) with
| None ⇒
Error_monad.error_value (Build_extensible "Asserted" unit tt)
| Some h_value ⇒
let sequence_value :=
Int64_map.(Map.S.remove) l_value t_value.(t.sequence) in
let events := Map.(Map.S.remove) h_value events in
return?
{| t.events := events; t.sequence := sequence_value;
t.capacity := t_value.(t.capacity);
t.next_index := t_value.(t.next_index);
t.oldest_index := Int64.succ t_value.(t.oldest_index);
t.size := t_value.(t.capacity); |}
end
end.
Definition find `{FArgs} (key_value : Key.(KEY.t)) (t_value : t)
: option value := Map.(Map.S.find_opt) key_value t_value.(t.events).
(* Make *)
Definition functor `{FArgs} :=
{|
S.empty := empty;
S.encoding := encoding;
S.pp := pp;
S.find := find;
S.remember := remember
|}.
End Make.
Definition Make {Key_t Value_t : Set}
(Name : NAME) (Key : KEY (t := Key_t)) (Value : VALUE (t := Value_t))
: S (t := _) (key := Key.(KEY.t)) (value := Value.(VALUE.t)) :=
let '_ := Make.Build_FArgs Name Key Value in
Make.functor.
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (Pervasives.not (String.equal Name.(NAME.name) "")) in
Error_monad.register_error_kind Error_monad.Temporary
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Bounded_history_repr."
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
".key_bound_to_different_value"
CamlinternalFormatBasics.End_of_format)))
"Bounded_history_repr.%s.key_bound_to_different_value")
Name.(NAME.name))
(Pervasives.op_caret Name.(NAME.name)
": Key already bound to a different value.")
(Pervasives.op_caret Name.(NAME.name)
(": Remember called with a key that is already bound to a different" ++
String.String "010" " value.")) None
(Data_encoding.obj3 (Data_encoding.req None None "key" Key.(KEY.encoding))
(Data_encoding.req None None "existing_value" Value.(VALUE.encoding))
(Data_encoding.req None None "given_value" Value.(VALUE.encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Key_bound_to_different_value" then
let '{|
Key_bound_to_different_value.key := key_value;
Key_bound_to_different_value.existing_value := existing_value;
Key_bound_to_different_value.given_value := given_value
|} := cast Key_bound_to_different_value payload in
Some (key_value, existing_value, given_value)
else None
end)
(fun (function_parameter : key × value × value) ⇒
let '(key_value, existing_value, given_value) := function_parameter in
Build_extensible "Key_bound_to_different_value"
Key_bound_to_different_value
{| Key_bound_to_different_value.key := key_value;
Key_bound_to_different_value.existing_value := existing_value;
Key_bound_to_different_value.given_value := given_value; |}).
Definition remember `{FArgs}
(key_value : Key.(KEY.t)) (value_value : value) (t_value : t) : M? t :=
if t_value.(t.capacity) ≤i64 0 then
return? t_value
else
match
((Map.(Map.S.find) key_value t_value.(t.events)),
match Map.(Map.S.find) key_value t_value.(t.events) with
| Some value' ⇒
Pervasives.not (Value.(VALUE.equal) value_value value')
| _ ⇒ false
end) with
| (Some value', true) ⇒
Error_monad.error_value
(Build_extensible "Key_bound_to_different_value"
Key_bound_to_different_value
{| Key_bound_to_different_value.key := key_value;
Key_bound_to_different_value.existing_value := value';
Key_bound_to_different_value.given_value := value_value; |})
| (_, _) ⇒
let events := Map.(Map.S.add) key_value value_value t_value.(t.events)
in
let current_index := t_value.(t.next_index) in
let next_index := Int64.succ current_index in
let t_value :=
{| t.events := events;
t.sequence :=
Int64_map.(Map.S.add) current_index key_value t_value.(t.sequence);
t.capacity := t_value.(t.capacity); t.next_index := next_index;
t.oldest_index := t_value.(t.oldest_index);
t.size := Int64.succ t_value.(t.size); |} in
if
(t_value.(t.size) >i64 0) &&
(t_value.(t.size) ≤i64 t_value.(t.capacity))
then
return? t_value
else
let l_value := t_value.(t.oldest_index) in
match Int64_map.(Map.S.find) l_value t_value.(t.sequence) with
| None ⇒
Error_monad.error_value (Build_extensible "Asserted" unit tt)
| Some h_value ⇒
let sequence_value :=
Int64_map.(Map.S.remove) l_value t_value.(t.sequence) in
let events := Map.(Map.S.remove) h_value events in
return?
{| t.events := events; t.sequence := sequence_value;
t.capacity := t_value.(t.capacity);
t.next_index := t_value.(t.next_index);
t.oldest_index := Int64.succ t_value.(t.oldest_index);
t.size := t_value.(t.capacity); |}
end
end.
Definition find `{FArgs} (key_value : Key.(KEY.t)) (t_value : t)
: option value := Map.(Map.S.find_opt) key_value t_value.(t.events).
(* Make *)
Definition functor `{FArgs} :=
{|
S.empty := empty;
S.encoding := encoding;
S.pp := pp;
S.find := find;
S.remember := remember
|}.
End Make.
Definition Make {Key_t Value_t : Set}
(Name : NAME) (Key : KEY (t := Key_t)) (Value : VALUE (t := Value_t))
: S (t := _) (key := Key.(KEY.t)) (value := Value.(VALUE.t)) :=
let '_ := Make.Build_FArgs Name Key Value in
Make.functor.