🗂️ Indexable.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.Cache_memory_helpers.
Inductive index_only : Set :=
| Index_only : index_only.
Inductive value_only : Set :=
| Value_only : value_only.
Inductive unknown : Set :=
| Unknown : unknown.
Inductive t (a : Set) : Set :=
| Value : a → t a
| Hidden_value : a → t a
| Index : int32 → t a
| Hidden_index : int32 → t a.
Arguments Value {_}.
Arguments Hidden_value {_}.
Arguments Index {_}.
Arguments Hidden_index {_}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Inductive index_only : Set :=
| Index_only : index_only.
Inductive value_only : Set :=
| Value_only : value_only.
Inductive unknown : Set :=
| Unknown : unknown.
Inductive t (a : Set) : Set :=
| Value : a → t a
| Hidden_value : a → t a
| Index : int32 → t a
| Hidden_index : int32 → t a.
Arguments Value {_}.
Arguments Hidden_value {_}.
Arguments Index {_}.
Arguments Hidden_index {_}.
Init function; without side-effects in Coq
Definition init_module : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"indexable.index_cannot_be_negative" "Index of values cannot be negative"
"A negative integer cannot be used as an index for a value."
(Some
(fun (ppf : Format.formatter) ⇒
fun (wrong_id : int32) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" cannot be used as an index because it is negative."
CamlinternalFormatBasics.End_of_format))
"%ld cannot be used as an index because it is negative.") wrong_id))
(Data_encoding.obj1
(Data_encoding.req None None "wrong_index" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Index_cannot_be_negative" then
let wrong_id := cast int32 payload in
Some wrong_id
else None
end)
(fun (wrong_id : int32) ⇒
Build_extensible "Index_cannot_be_negative" int32 wrong_id).
Definition value (a : Set) : Set := t a.
Definition index (a : Set) : Set := t a.
Definition either (a : Set) : Set := t a.
Definition value_value {a : Set} (v_value : a) : value a := Value v_value.
Definition from_value {a : Set} (v_value : a) : either a :=
Hidden_value v_value.
Definition index_value {a : Set} (i_value : int32) : M? (index a) :=
if 0 ≤i32 i_value then
return? (Index i_value)
else
Error_monad.error_value
(Build_extensible "Index_cannot_be_negative" int32 i_value).
Definition from_index {a : Set} (i_value : int32) : M? (either a) :=
if 0 ≤i32 i_value then
return? (Hidden_index i_value)
else
Error_monad.error_value
(Build_extensible "Index_cannot_be_negative" int32 i_value).
Definition index_exn {a : Set} (i_value : int32) : index a :=
match index_value i_value with
| Pervasives.Ok x_value ⇒ x_value
| Pervasives.Error _ ⇒
Pervasives.raise
(Build_extensible "Invalid_argument" string "Indexable.index_exn")
end.
Definition from_index_exn {a : Set} (i_value : int32) : either a :=
match from_index i_value with
| Pervasives.Ok x_value ⇒ x_value
| Pervasives.Error _ ⇒
Pervasives.raise
(Build_extensible "Invalid_argument" string "Indexable.from_index_exn")
end.
Definition destruct {a : Set} (function_parameter : t a)
: Either.t (index a) a :=
match function_parameter with
| (Hidden_value x_value | Value x_value) ⇒ Either.Right x_value
| (Hidden_index x_value | Index x_value) ⇒ Either.Left (Index x_value)
end.
Definition forget {a : Set} (function_parameter : t a) : t a :=
match function_parameter with
| (Hidden_value x_value | Value x_value) ⇒ Hidden_value x_value
| (Hidden_index x_value | Index x_value) ⇒ Hidden_index x_value
end.
Definition to_int32 {A : Set} (function_parameter : t A) : int32 :=
match function_parameter with
| Index x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end.
Definition to_value {A : Set} (function_parameter : t A) : A :=
match function_parameter with
| Value x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end.
Definition is_value_e {trace a : Set} (error_value : trace) (v_value : t a)
: Pervasives.result a trace :=
match destruct v_value with
| Either.Left _ ⇒ Result.error_value error_value
| Either.Right v_value ⇒ Result.ok v_value
end.
Definition compact {A : Set} (val_encoding : Data_encoding.encoding A)
: Data_encoding.Compact.t (t A) :=
Data_encoding.Compact.conv None
(fun (function_parameter : t A) ⇒
match function_parameter with
| Hidden_index x_value ⇒ Either.Left x_value
| Hidden_value x_value ⇒ Either.Right x_value
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter : Either.t int32 A) ⇒
match function_parameter with
| Either.Left x_value ⇒ Hidden_index x_value
| Either.Right x_value ⇒ Hidden_value x_value
end) (Data_encoding.Compact.or_int32 "index" "value" None val_encoding).
Definition encoding {a : Set} (val_encoding : Data_encoding.t a)
: Data_encoding.t (either a) :=
Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
(compact val_encoding).
Definition pp {a : Set}
(ppv : Format.formatter → a → unit) (fmt : Format.formatter)
(function_parameter : t a) : unit :=
match function_parameter with
| (Hidden_index x_value | Index x_value) ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Char_literal "" % char
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)) "#%ld") x_value
| (Hidden_value x_value | Value x_value) ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
"%a") ppv x_value
end.
Definition in_memory_size {a : Set}
(ims : a → Cache_memory_helpers.sint) (function_parameter : t a)
: Cache_memory_helpers.sint :=
match function_parameter with
| (Hidden_value x_value | Value x_value) ⇒
Cache_memory_helpers.op_plusexclamation
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
Cache_memory_helpers.word_size) (ims x_value)
| (Hidden_index _ | Index _) ⇒
Cache_memory_helpers.op_plusexclamation
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
Cache_memory_helpers.word_size) Cache_memory_helpers.int32_size
end.
Definition size_value {a : Set} (s_value : a → int) (function_parameter : t a)
: int :=
match function_parameter with
| (Hidden_value x_value | Value x_value) ⇒ 1 +i (s_value x_value)
| (Hidden_index _ | Index _) ⇒ 1 +i 4
end.
Definition compare {a : Set}
(c_value : a → a → int) (x_value : t a) (y_value : t a) : int :=
match (x_value, y_value) with
|
((Hidden_index x_value | Index x_value),
(Hidden_index y_value | Index y_value)) ⇒
Compare.Int32.(Compare.S.compare) x_value y_value
|
((Hidden_value x_value | Value x_value),
(Hidden_value y_value | Value y_value)) ⇒ c_value x_value y_value
| ((Hidden_index _ | Index _), (Hidden_value _ | Value _)) ⇒ (-1)
| ((Hidden_value _ | Value _), (Hidden_index _ | Index _)) ⇒ 1
end.
Definition compare_values {a : Set}
(c_value : a → a → int) (x_value : value a) (y_value : value a) : int :=
match (x_value, y_value) with
| (Value x_value, Value y_value) ⇒ c_value x_value y_value
| _ ⇒ unreachable_gadt_branch
end.
Definition compare_indexes {a : Set} (x_value : index a) (y_value : index a)
: int :=
match (x_value, y_value) with
| (Index x_value, Index y_value) ⇒
Compare.Int32.(Compare.S.compare) x_value y_value
| _ ⇒ unreachable_gadt_branch
end.
Module VALUE.
Record signature {t : Set} : Set := {
t := t;
encoding : Data_encoding.t t;
compare : t → t → int;
pp : Format.formatter → t → unit;
}.
End VALUE.
Definition VALUE := @VALUE.signature.
Arguments VALUE {_}.
Module INDEXABLE.
Record signature {v_t : Set} : Set := {
v_t := v_t;
t := t v_t;
index := index v_t;
value := value v_t;
either := either v_t;
value_value : v_t → value;
index_value : int32 → M? index;
index_exn : int32 → index;
compact : Data_encoding.Compact.t either;
encoding : Data_encoding.t either;
index_encoding : Data_encoding.t index;
value_encoding : Data_encoding.t value;
compare : t → t → int;
compare_values : value → value → int;
compare_indexes : index → index → int;
pp : Format.formatter → t → unit;
}.
End INDEXABLE.
Definition INDEXABLE := @INDEXABLE.signature.
Arguments INDEXABLE {_}.
Module Make.
Class FArgs {V_t : Set} := {
V : VALUE (t := V_t);
}.
Arguments Build_FArgs {_}.
Definition t `{FArgs} : Set := t V.(VALUE.t).
Definition index `{FArgs} : Set := index V.(VALUE.t).
Definition value `{FArgs} : Set := value V.(VALUE.t).
Definition either `{FArgs} : Set := either V.(VALUE.t).
Definition value_value `{FArgs} : V.(VALUE.t) → value := value_value.
Definition index_value `{FArgs} : int32 → M? index := index_value.
Definition index_exn `{FArgs} : int32 → index := index_exn.
Definition compact `{FArgs} : Data_encoding.Compact.t either :=
compact V.(VALUE.encoding).
Definition encoding `{FArgs} : Data_encoding.t either :=
encoding V.(VALUE.encoding).
Definition index_encoding `{FArgs} : Data_encoding.t index :=
Data_encoding.conv
(fun (function_parameter : index) ⇒
match function_parameter with
| Index x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end) (fun (x_value : int32) ⇒ Index x_value) None
Data_encoding.int32_value.
Definition value_encoding `{FArgs} : Data_encoding.t value :=
Data_encoding.conv
(fun (function_parameter : value) ⇒
match function_parameter with
| Value x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end) (fun (x_value : V.(VALUE.t)) ⇒ Value x_value) None
V.(VALUE.encoding).
Definition pp `{FArgs} (fmt : Format.formatter) (x_value : t) : unit :=
pp V.(VALUE.pp) fmt x_value.
Definition compare_values `{FArgs} : value → value → int :=
compare_values V.(VALUE.compare).
Definition compare_indexes `{FArgs} : index → index → int :=
compare_indexes.
Definition compare `{FArgs} (x_value : t) (y_value : t) : int :=
compare V.(VALUE.compare) x_value y_value.
(* Make *)
Definition functor `{FArgs} :=
{|
INDEXABLE.value_value := value_value;
INDEXABLE.index_value := index_value;
INDEXABLE.index_exn := index_exn;
INDEXABLE.compact := compact;
INDEXABLE.encoding := encoding;
INDEXABLE.index_encoding := index_encoding;
INDEXABLE.value_encoding := value_encoding;
INDEXABLE.compare := compare;
INDEXABLE.compare_values := compare_values;
INDEXABLE.compare_indexes := compare_indexes;
INDEXABLE.pp := pp
|}.
End Make.
Definition Make {V_t : Set} (V : VALUE (t := V_t))
: INDEXABLE (v_t := V.(VALUE.t)) :=
let '_ := Make.Build_FArgs V in
Make.functor.
Error_monad.register_error_kind Error_monad.Permanent
"indexable.index_cannot_be_negative" "Index of values cannot be negative"
"A negative integer cannot be used as an index for a value."
(Some
(fun (ppf : Format.formatter) ⇒
fun (wrong_id : int32) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" cannot be used as an index because it is negative."
CamlinternalFormatBasics.End_of_format))
"%ld cannot be used as an index because it is negative.") wrong_id))
(Data_encoding.obj1
(Data_encoding.req None None "wrong_index" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Index_cannot_be_negative" then
let wrong_id := cast int32 payload in
Some wrong_id
else None
end)
(fun (wrong_id : int32) ⇒
Build_extensible "Index_cannot_be_negative" int32 wrong_id).
Definition value (a : Set) : Set := t a.
Definition index (a : Set) : Set := t a.
Definition either (a : Set) : Set := t a.
Definition value_value {a : Set} (v_value : a) : value a := Value v_value.
Definition from_value {a : Set} (v_value : a) : either a :=
Hidden_value v_value.
Definition index_value {a : Set} (i_value : int32) : M? (index a) :=
if 0 ≤i32 i_value then
return? (Index i_value)
else
Error_monad.error_value
(Build_extensible "Index_cannot_be_negative" int32 i_value).
Definition from_index {a : Set} (i_value : int32) : M? (either a) :=
if 0 ≤i32 i_value then
return? (Hidden_index i_value)
else
Error_monad.error_value
(Build_extensible "Index_cannot_be_negative" int32 i_value).
Definition index_exn {a : Set} (i_value : int32) : index a :=
match index_value i_value with
| Pervasives.Ok x_value ⇒ x_value
| Pervasives.Error _ ⇒
Pervasives.raise
(Build_extensible "Invalid_argument" string "Indexable.index_exn")
end.
Definition from_index_exn {a : Set} (i_value : int32) : either a :=
match from_index i_value with
| Pervasives.Ok x_value ⇒ x_value
| Pervasives.Error _ ⇒
Pervasives.raise
(Build_extensible "Invalid_argument" string "Indexable.from_index_exn")
end.
Definition destruct {a : Set} (function_parameter : t a)
: Either.t (index a) a :=
match function_parameter with
| (Hidden_value x_value | Value x_value) ⇒ Either.Right x_value
| (Hidden_index x_value | Index x_value) ⇒ Either.Left (Index x_value)
end.
Definition forget {a : Set} (function_parameter : t a) : t a :=
match function_parameter with
| (Hidden_value x_value | Value x_value) ⇒ Hidden_value x_value
| (Hidden_index x_value | Index x_value) ⇒ Hidden_index x_value
end.
Definition to_int32 {A : Set} (function_parameter : t A) : int32 :=
match function_parameter with
| Index x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end.
Definition to_value {A : Set} (function_parameter : t A) : A :=
match function_parameter with
| Value x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end.
Definition is_value_e {trace a : Set} (error_value : trace) (v_value : t a)
: Pervasives.result a trace :=
match destruct v_value with
| Either.Left _ ⇒ Result.error_value error_value
| Either.Right v_value ⇒ Result.ok v_value
end.
Definition compact {A : Set} (val_encoding : Data_encoding.encoding A)
: Data_encoding.Compact.t (t A) :=
Data_encoding.Compact.conv None
(fun (function_parameter : t A) ⇒
match function_parameter with
| Hidden_index x_value ⇒ Either.Left x_value
| Hidden_value x_value ⇒ Either.Right x_value
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter : Either.t int32 A) ⇒
match function_parameter with
| Either.Left x_value ⇒ Hidden_index x_value
| Either.Right x_value ⇒ Hidden_value x_value
end) (Data_encoding.Compact.or_int32 "index" "value" None val_encoding).
Definition encoding {a : Set} (val_encoding : Data_encoding.t a)
: Data_encoding.t (either a) :=
Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
(compact val_encoding).
Definition pp {a : Set}
(ppv : Format.formatter → a → unit) (fmt : Format.formatter)
(function_parameter : t a) : unit :=
match function_parameter with
| (Hidden_index x_value | Index x_value) ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Char_literal "" % char
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)) "#%ld") x_value
| (Hidden_value x_value | Value x_value) ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
"%a") ppv x_value
end.
Definition in_memory_size {a : Set}
(ims : a → Cache_memory_helpers.sint) (function_parameter : t a)
: Cache_memory_helpers.sint :=
match function_parameter with
| (Hidden_value x_value | Value x_value) ⇒
Cache_memory_helpers.op_plusexclamation
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
Cache_memory_helpers.word_size) (ims x_value)
| (Hidden_index _ | Index _) ⇒
Cache_memory_helpers.op_plusexclamation
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
Cache_memory_helpers.word_size) Cache_memory_helpers.int32_size
end.
Definition size_value {a : Set} (s_value : a → int) (function_parameter : t a)
: int :=
match function_parameter with
| (Hidden_value x_value | Value x_value) ⇒ 1 +i (s_value x_value)
| (Hidden_index _ | Index _) ⇒ 1 +i 4
end.
Definition compare {a : Set}
(c_value : a → a → int) (x_value : t a) (y_value : t a) : int :=
match (x_value, y_value) with
|
((Hidden_index x_value | Index x_value),
(Hidden_index y_value | Index y_value)) ⇒
Compare.Int32.(Compare.S.compare) x_value y_value
|
((Hidden_value x_value | Value x_value),
(Hidden_value y_value | Value y_value)) ⇒ c_value x_value y_value
| ((Hidden_index _ | Index _), (Hidden_value _ | Value _)) ⇒ (-1)
| ((Hidden_value _ | Value _), (Hidden_index _ | Index _)) ⇒ 1
end.
Definition compare_values {a : Set}
(c_value : a → a → int) (x_value : value a) (y_value : value a) : int :=
match (x_value, y_value) with
| (Value x_value, Value y_value) ⇒ c_value x_value y_value
| _ ⇒ unreachable_gadt_branch
end.
Definition compare_indexes {a : Set} (x_value : index a) (y_value : index a)
: int :=
match (x_value, y_value) with
| (Index x_value, Index y_value) ⇒
Compare.Int32.(Compare.S.compare) x_value y_value
| _ ⇒ unreachable_gadt_branch
end.
Module VALUE.
Record signature {t : Set} : Set := {
t := t;
encoding : Data_encoding.t t;
compare : t → t → int;
pp : Format.formatter → t → unit;
}.
End VALUE.
Definition VALUE := @VALUE.signature.
Arguments VALUE {_}.
Module INDEXABLE.
Record signature {v_t : Set} : Set := {
v_t := v_t;
t := t v_t;
index := index v_t;
value := value v_t;
either := either v_t;
value_value : v_t → value;
index_value : int32 → M? index;
index_exn : int32 → index;
compact : Data_encoding.Compact.t either;
encoding : Data_encoding.t either;
index_encoding : Data_encoding.t index;
value_encoding : Data_encoding.t value;
compare : t → t → int;
compare_values : value → value → int;
compare_indexes : index → index → int;
pp : Format.formatter → t → unit;
}.
End INDEXABLE.
Definition INDEXABLE := @INDEXABLE.signature.
Arguments INDEXABLE {_}.
Module Make.
Class FArgs {V_t : Set} := {
V : VALUE (t := V_t);
}.
Arguments Build_FArgs {_}.
Definition t `{FArgs} : Set := t V.(VALUE.t).
Definition index `{FArgs} : Set := index V.(VALUE.t).
Definition value `{FArgs} : Set := value V.(VALUE.t).
Definition either `{FArgs} : Set := either V.(VALUE.t).
Definition value_value `{FArgs} : V.(VALUE.t) → value := value_value.
Definition index_value `{FArgs} : int32 → M? index := index_value.
Definition index_exn `{FArgs} : int32 → index := index_exn.
Definition compact `{FArgs} : Data_encoding.Compact.t either :=
compact V.(VALUE.encoding).
Definition encoding `{FArgs} : Data_encoding.t either :=
encoding V.(VALUE.encoding).
Definition index_encoding `{FArgs} : Data_encoding.t index :=
Data_encoding.conv
(fun (function_parameter : index) ⇒
match function_parameter with
| Index x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end) (fun (x_value : int32) ⇒ Index x_value) None
Data_encoding.int32_value.
Definition value_encoding `{FArgs} : Data_encoding.t value :=
Data_encoding.conv
(fun (function_parameter : value) ⇒
match function_parameter with
| Value x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end) (fun (x_value : V.(VALUE.t)) ⇒ Value x_value) None
V.(VALUE.encoding).
Definition pp `{FArgs} (fmt : Format.formatter) (x_value : t) : unit :=
pp V.(VALUE.pp) fmt x_value.
Definition compare_values `{FArgs} : value → value → int :=
compare_values V.(VALUE.compare).
Definition compare_indexes `{FArgs} : index → index → int :=
compare_indexes.
Definition compare `{FArgs} (x_value : t) (y_value : t) : int :=
compare V.(VALUE.compare) x_value y_value.
(* Make *)
Definition functor `{FArgs} :=
{|
INDEXABLE.value_value := value_value;
INDEXABLE.index_value := index_value;
INDEXABLE.index_exn := index_exn;
INDEXABLE.compact := compact;
INDEXABLE.encoding := encoding;
INDEXABLE.index_encoding := index_encoding;
INDEXABLE.value_encoding := value_encoding;
INDEXABLE.compare := compare;
INDEXABLE.compare_values := compare_values;
INDEXABLE.compare_indexes := compare_indexes;
INDEXABLE.pp := pp
|}.
End Make.
Definition Make {V_t : Set} (V : VALUE (t := V_t))
: INDEXABLE (v_t := V.(VALUE.t)) :=
let '_ := Make.Build_FArgs V in
Make.functor.