🔗 Skip_list_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Records for the constructor parameters
Module ConstructorRecords_search_cell_result.
Module search_cell_result.
Module Nearest.
Record record {lower upper : Set} : Set := Build {
lower : lower;
upper : upper;
}.
Arguments record : clear implicits.
Definition with_lower {t_lower t_upper} lower
(r : record t_lower t_upper) :=
Build t_lower t_upper lower r.(upper).
Definition with_upper {t_lower t_upper} upper
(r : record t_lower t_upper) :=
Build t_lower t_upper r.(lower) upper.
End Nearest.
Definition Nearest_skeleton := Nearest.record.
End search_cell_result.
End ConstructorRecords_search_cell_result.
Import ConstructorRecords_search_cell_result.
Reserved Notation "'search_cell_result.Nearest".
Inductive search_cell_result (cell : Set) : Set :=
| Found : cell → search_cell_result cell
| Nearest : 'search_cell_result.Nearest cell → search_cell_result cell
| No_exact_or_lower_ptr : search_cell_result cell
| Deref_returned_none : search_cell_result cell
where "'search_cell_result.Nearest" :=
(fun (t_cell : Set) ⇒ search_cell_result.Nearest_skeleton t_cell
(option t_cell)).
Module search_cell_result.
Include ConstructorRecords_search_cell_result.search_cell_result.
Definition Nearest := 'search_cell_result.Nearest.
End search_cell_result.
Arguments Found {_}.
Arguments Nearest {_}.
Arguments No_exact_or_lower_ptr {_}.
Arguments Deref_returned_none {_}.
Module search_result.
Record record {cell : Set} : Set := Build {
rev_path : list cell;
last_cell : search_cell_result cell;
}.
Arguments record : clear implicits.
Definition with_rev_path {t_cell} rev_path (r : record t_cell) :=
Build t_cell rev_path r.(last_cell).
Definition with_last_cell {t_cell} last_cell (r : record t_cell) :=
Build t_cell r.(rev_path) last_cell.
End search_result.
Definition search_result := search_result.record.
Module S.
Record signature {cell : Set → Set → Set} : Set := {
cell := cell;
pp :
∀ {content ptr : Set},
(Format.formatter → ptr → unit) →
(Format.formatter → content → unit) → Format.formatter →
cell content ptr → unit;
equal :
∀ {content ptr : Set},
(ptr → ptr → bool) → (content → content → bool) →
cell content ptr → cell content ptr → bool;
encoding :
∀ {content ptr : Set},
Data_encoding.t ptr → Data_encoding.t content →
Data_encoding.t (cell content ptr);
index_value : ∀ {content ptr : Set}, cell content ptr → int;
content : ∀ {content ptr : Set}, cell content ptr → content;
back_pointer :
∀ {content ptr : Set}, cell content ptr → int → option ptr;
back_pointers : ∀ {content ptr : Set}, cell content ptr → list ptr;
genesis : ∀ {content ptr : Set}, content → cell content ptr;
next :
∀ {content ptr : Set},
cell content ptr → ptr → content → cell content ptr;
find :
∀ {content ptr : Set},
(ptr → option (cell content ptr)) → ptr → int →
option (cell content ptr);
back_path :
∀ {content ptr : Set},
(ptr → option (cell content ptr)) → ptr → int → option (list ptr);
valid_back_path :
∀ {content ptr : Set},
(ptr → ptr → bool) → (ptr → option (cell content ptr)) → ptr →
ptr → list ptr → bool;
search_cell_result :=
fun (ptr content : Set) ⇒ search_cell_result (cell content ptr);
search_result :=
fun (ptr content : Set) ⇒ search_result (cell ptr content);
pp_search_result :
∀ {content ptr : Set},
(Format.formatter → cell ptr content → unit) → Format.formatter →
search_result ptr content → unit;
search :
∀ {content ptr : Set},
(ptr → option (cell content ptr)) → (content → int) →
cell content ptr → search_result content ptr;
}.
End S.
Definition S := @S.signature.
Arguments S {_}.
Module S_Parameters.
Record signature : Set := {
basis : int;
}.
End S_Parameters.
Definition S_Parameters := S_Parameters.signature.
Module Make.
Class FArgs := {
Parameters : S_Parameters;
}.
Module search_cell_result.
Module Nearest.
Record record {lower upper : Set} : Set := Build {
lower : lower;
upper : upper;
}.
Arguments record : clear implicits.
Definition with_lower {t_lower t_upper} lower
(r : record t_lower t_upper) :=
Build t_lower t_upper lower r.(upper).
Definition with_upper {t_lower t_upper} upper
(r : record t_lower t_upper) :=
Build t_lower t_upper r.(lower) upper.
End Nearest.
Definition Nearest_skeleton := Nearest.record.
End search_cell_result.
End ConstructorRecords_search_cell_result.
Import ConstructorRecords_search_cell_result.
Reserved Notation "'search_cell_result.Nearest".
Inductive search_cell_result (cell : Set) : Set :=
| Found : cell → search_cell_result cell
| Nearest : 'search_cell_result.Nearest cell → search_cell_result cell
| No_exact_or_lower_ptr : search_cell_result cell
| Deref_returned_none : search_cell_result cell
where "'search_cell_result.Nearest" :=
(fun (t_cell : Set) ⇒ search_cell_result.Nearest_skeleton t_cell
(option t_cell)).
Module search_cell_result.
Include ConstructorRecords_search_cell_result.search_cell_result.
Definition Nearest := 'search_cell_result.Nearest.
End search_cell_result.
Arguments Found {_}.
Arguments Nearest {_}.
Arguments No_exact_or_lower_ptr {_}.
Arguments Deref_returned_none {_}.
Module search_result.
Record record {cell : Set} : Set := Build {
rev_path : list cell;
last_cell : search_cell_result cell;
}.
Arguments record : clear implicits.
Definition with_rev_path {t_cell} rev_path (r : record t_cell) :=
Build t_cell rev_path r.(last_cell).
Definition with_last_cell {t_cell} last_cell (r : record t_cell) :=
Build t_cell r.(rev_path) last_cell.
End search_result.
Definition search_result := search_result.record.
Module S.
Record signature {cell : Set → Set → Set} : Set := {
cell := cell;
pp :
∀ {content ptr : Set},
(Format.formatter → ptr → unit) →
(Format.formatter → content → unit) → Format.formatter →
cell content ptr → unit;
equal :
∀ {content ptr : Set},
(ptr → ptr → bool) → (content → content → bool) →
cell content ptr → cell content ptr → bool;
encoding :
∀ {content ptr : Set},
Data_encoding.t ptr → Data_encoding.t content →
Data_encoding.t (cell content ptr);
index_value : ∀ {content ptr : Set}, cell content ptr → int;
content : ∀ {content ptr : Set}, cell content ptr → content;
back_pointer :
∀ {content ptr : Set}, cell content ptr → int → option ptr;
back_pointers : ∀ {content ptr : Set}, cell content ptr → list ptr;
genesis : ∀ {content ptr : Set}, content → cell content ptr;
next :
∀ {content ptr : Set},
cell content ptr → ptr → content → cell content ptr;
find :
∀ {content ptr : Set},
(ptr → option (cell content ptr)) → ptr → int →
option (cell content ptr);
back_path :
∀ {content ptr : Set},
(ptr → option (cell content ptr)) → ptr → int → option (list ptr);
valid_back_path :
∀ {content ptr : Set},
(ptr → ptr → bool) → (ptr → option (cell content ptr)) → ptr →
ptr → list ptr → bool;
search_cell_result :=
fun (ptr content : Set) ⇒ search_cell_result (cell content ptr);
search_result :=
fun (ptr content : Set) ⇒ search_result (cell ptr content);
pp_search_result :
∀ {content ptr : Set},
(Format.formatter → cell ptr content → unit) → Format.formatter →
search_result ptr content → unit;
search :
∀ {content ptr : Set},
(ptr → option (cell content ptr)) → (content → int) →
cell content ptr → search_result content ptr;
}.
End S.
Definition S := @S.signature.
Arguments S {_}.
Module S_Parameters.
Record signature : Set := {
basis : int;
}.
End S_Parameters.
Definition S_Parameters := S_Parameters.signature.
Module Make.
Class FArgs := {
Parameters : S_Parameters;
}.
Init function; without side-effects in Coq
Definition init_module_repr `{FArgs} : unit :=
(* ❌ Assert instruction is not handled. *)
assert unit (Parameters.(S_Parameters.basis) ≥i 2).
Module cell.
Record record `{FArgs} {content ptr : Set} : Set := Build {
content : content;
back_pointers : FallbackArray.t (option ptr);
index : int;
}.
Arguments record {_}.
Definition with_content `{FArgs} {t_content t_ptr} content
(r : record t_content t_ptr) :=
Build _ t_content t_ptr content r.(back_pointers) r.(index).
Definition with_back_pointers `{FArgs} {t_content t_ptr} back_pointers
(r : record t_content t_ptr) :=
Build _ t_content t_ptr r.(content) back_pointers r.(index).
Definition with_index `{FArgs} {t_content t_ptr} index
(r : record t_content t_ptr) :=
Build _ t_content t_ptr r.(content) r.(back_pointers) index.
End cell.
Definition cell `{FArgs} := cell.record.
Definition equal `{FArgs} {A B C : Set}
(equal_ptr : A → A → bool) (equal_content : B → C → bool)
(cell1 : cell B A) (cell2 : cell C A) : bool :=
let equal_back_pointers
(b1 : FallbackArray.t (option A)) (b2 : FallbackArray.t (option A))
: bool :=
((FallbackArray.length b1) =i (FallbackArray.length b2)) &&
(Pervasives.fst
(FallbackArray.fold
(fun (function_parameter : bool × int) ⇒
let '(equal, i_value) := function_parameter in
fun (h1 : option A) ⇒
((equal &&
(Option.equal equal_ptr h1 (FallbackArray.get b2 i_value))),
(i_value +i 1))) b1 (true, 0))) in
let '{|
cell.content := content;
cell.back_pointers := back_pointers;
cell.index := index_value
|} := cell1 in
(equal_content content cell2.(cell.content)) &&
((Compare.Int.equal index_value cell2.(cell.index)) &&
(equal_back_pointers back_pointers cell2.(cell.back_pointers))).
Definition index_value `{FArgs} {A B : Set} (cell_value : cell A B) : int :=
cell_value.(cell.index).
Definition back_pointers_to_list `{FArgs} {A : Set}
(a_value : FallbackArray.t (option A)) : list A :=
List.rev
(FallbackArray.fold
(fun (l_value : list A) ⇒
fun (function_parameter : option A) ⇒
match function_parameter with
| Some ptr ⇒ cons ptr l_value
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (list _) false
end) a_value nil).
Definition pp `{FArgs} {A B : Set}
(pp_ptr : Format.formatter → A → unit)
(pp_content : Format.formatter → B → unit) (fmt : Format.formatter)
(function_parameter : cell B A) : unit :=
let '{|
cell.content := content;
cell.back_pointers := back_pointers;
cell.index := index_value
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
(String.String "010" " content = ")
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
(String.String "010" " index = ")
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
(String.String "010" " back_pointers = ")
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
(String.String "010" " ")
CamlinternalFormatBasics.End_of_format)))))))
(String.String "010"
(" content = %a" ++
String.String "010"
(" index = %d" ++
String.String "010"
(" back_pointers = %a" ++ String.String "010" " ")))))
pp_content content index_value (Format.pp_print_list None pp_ptr)
(back_pointers_to_list back_pointers).
Definition encoding `{FArgs} {A B : Set}
(ptr_encoding : Data_encoding.encoding A)
(content_encoding : Data_encoding.encoding B)
: Data_encoding.encoding (cell B A) :=
let of_list :=
FallbackArray.of_list None (fun (c_value : A) ⇒ Some c_value) in
let to_list {C : Set} : FallbackArray.t (option C) → list C :=
back_pointers_to_list in
Data_encoding.conv
(fun (function_parameter : cell B A) ⇒
let '{|
cell.content := content;
cell.back_pointers := back_pointers;
cell.index := index_value
|} := function_parameter in
(index_value, content, (to_list back_pointers)))
(fun (function_parameter : int × B × list A) ⇒
let '(index_value, content, back_pointers) := function_parameter in
{| cell.content := content; cell.back_pointers := of_list back_pointers;
cell.index := index_value; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "index" Data_encoding.int31)
(Data_encoding.req None None "content" content_encoding)
(Data_encoding.req None None "back_pointers"
(Data_encoding.list_value None ptr_encoding))).
Definition content `{FArgs} {A B : Set} (cell_value : cell A B) : A :=
cell_value.(cell.content).
Definition back_pointers `{FArgs} {A B : Set} (cell_value : cell A B)
: list B := back_pointers_to_list cell_value.(cell.back_pointers).
Definition genesis `{FArgs} {A B : Set} (content : A) : cell A B :=
{| cell.content := content; cell.back_pointers := FallbackArray.make 0 None;
cell.index := 0; |}.
Definition back_pointer `{FArgs} {A B : Set}
(cell_value : cell A B) (i_value : int) : option B :=
FallbackArray.get cell_value.(cell.back_pointers) i_value.
Definition back_pointer_unsafe `{FArgs} {A B : Set}
(cell_value : cell A B) (i_value : int) : B :=
match FallbackArray.get cell_value.(cell.back_pointers) i_value with
| Some ptr ⇒ ptr
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert _ false
end.
#[bypass_check(guard)]
Definition next `{FArgs} {A B C : Set}
(prev_cell : cell A B) (prev_cell_ptr : B) (content : C) : cell C B :=
let index_value := prev_cell.(cell.index) +i 1 in
let back_pointers :=
let fix aux (power : int) (accu_value : list B) (i_value : int)
{struct power} : list B :=
if index_value <i power then
List.rev accu_value
else
let back_pointer_i :=
if (Pervasives._mod index_value power) =i 0 then
prev_cell_ptr
else
back_pointer_unsafe prev_cell i_value in
let accu_value := cons back_pointer_i accu_value in
aux (power ×i Parameters.(S_Parameters.basis)) accu_value
(i_value +i 1) in
aux 1 nil 0 in
let back_pointers := FallbackArray.of_list None Option.some back_pointers in
{| cell.content := content; cell.back_pointers := back_pointers;
cell.index := index_value; |}.
#[bypass_check(guard)]
Definition list_powers `{FArgs} {A B : Set} (cell_value : cell A B)
: FallbackArray.t int :=
let fix aux (n_value : int) (prev : int) (p_value : list int)
{struct n_value} : list int :=
if n_value ≤i 0 then
List.rev p_value
else
aux (n_value -i 1) (Parameters.(S_Parameters.basis) ×i prev)
(cons prev p_value) in
FallbackArray.of_list 0 (fun (x_value : int) ⇒ x_value)
(aux (FallbackArray.length cell_value.(cell.back_pointers)) 1 nil).
#[bypass_check(guard)]
Definition best_skip `{FArgs} {A B : Set}
(cell_value : cell A B) (target_index : int) (powers : FallbackArray.t int)
: option int :=
let pointed_cell_index (i_value : int) : int :=
(cell_value.(cell.index) -i
(Pervasives._mod cell_value.(cell.index)
(FallbackArray.get powers i_value))) -i 1 in
let fix binary_search (start_idx : int) (end_idx : int) {struct start_idx}
: option int :=
if start_idx ≥i end_idx then
Some start_idx
else
let mid_idx := start_idx +i ((end_idx -i start_idx) /i 2) in
let mid_cell_index := pointed_cell_index mid_idx in
if mid_cell_index =i target_index then
Some mid_idx
else
if mid_cell_index <i target_index then
binary_search start_idx (mid_idx -i 1)
else
let prev_mid_cell_index := pointed_cell_index (mid_idx +i 1) in
if prev_mid_cell_index =i target_index then
Some (mid_idx +i 1)
else
if prev_mid_cell_index <i target_index then
Some mid_idx
else
binary_search (mid_idx +i 1) end_idx in
binary_search 0
((FallbackArray.length cell_value.(cell.back_pointers)) -i 1).
#[bypass_check(guard)]
Definition rev_back_path `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (list A) :=
let× cell_value := deref cell_ptr in
let powers := list_powers cell_value in
let fix aux (path : list A) (ptr : A) {struct ptr} : option (list A) :=
let path := cons ptr path in
let× cell_value := deref ptr in
let index_value := cell_value.(cell.index) in
if target_index =i index_value then
return× path
else
if target_index >i index_value then
Error_monad.Option_syntax.fail
else
let× best_idx := best_skip cell_value target_index powers in
let× ptr := back_pointer cell_value best_idx in
aux path ptr in
aux nil cell_ptr.
Definition find `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (cell B A) :=
let× rev_back_path := rev_back_path deref cell_ptr target_index in
let× cell_ptr := List.hd rev_back_path in
deref cell_ptr.
Definition back_path `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (list A) :=
Error_monad.Option_syntax.op_letplus
(rev_back_path deref cell_ptr target_index)
(fun rev_back_path ⇒ List.rev rev_back_path).
#[bypass_check(guard)]
Definition mem `{FArgs} {A B : Set}
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B)) : bool :=
let n_value := FallbackArray.length l_value in
let fix aux (idx : int) {struct idx} : bool :=
if idx ≥i n_value then
false
else
match FallbackArray.get l_value idx with
| None ⇒ aux (idx +i 1)
| Some y_value ⇒
if equal x_value y_value then
true
else
aux (idx +i 1)
end in
aux 0.
Definition assume_some `{FArgs} {A : Set}
(o_value : option A) (f_value : A → bool) : bool :=
match o_value with
| None ⇒ false
| Some x_value ⇒ f_value x_value
end.
#[bypass_check(guard)]
Definition valid_back_path `{FArgs} {A B : Set}
(equal_ptr : A → A → bool) (deref : A → option (cell B A)) (cell_ptr : A)
(target_ptr : A) (path : list A) : bool :=
assume_some (deref target_ptr)
(fun (target : cell B A) ⇒
assume_some (deref cell_ptr)
(fun (cell_value : cell B A) ⇒
let target_index : int :=
index_value target
in let cell_index : int :=
index_value cell_value
in let powers : FallbackArray.t int :=
list_powers cell_value in
let fix valid_path
(index_value : int) (cell_ptr : A) (path : list A) {struct path}
: bool :=
match (cell_ptr, path) with
| (final_cell, []) ⇒
(equal_ptr target_ptr final_cell) &&
(index_value =i target_index)
| (cell_ptr, cons cell_ptr' path) ⇒
assume_some (deref cell_ptr)
(fun (cell_value : cell B A) ⇒
assume_some (deref cell_ptr')
(fun (cell' : cell B A) ⇒
(mem equal_ptr cell_ptr' cell_value.(cell.back_pointers))
&&
(assume_some (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
assume_some (back_pointer cell_value best_idx)
(fun (best_ptr : A) ⇒
let minimal := equal_ptr best_ptr cell_ptr' in
let index' := cell'.(cell.index) in
minimal && (valid_path index' cell_ptr' path))))))
end in
match path with
| [] ⇒ false
| cons first_cell_ptr path ⇒
(equal_ptr first_cell_ptr cell_ptr) &&
(valid_path cell_index cell_ptr path)
end)).
Definition search_cell_result `{FArgs} (ptr content : Set) : Set :=
search_cell_result (cell content ptr).
Definition search_result `{FArgs} (ptr content : Set) : Set :=
search_result (cell ptr content).
Definition pp_rev_path `{FArgs} {A : Set}
(pp_cell : Format.formatter → A → unit)
: Format.formatter → list A → unit :=
Format.pp_print_list (Some Format.pp_print_space) pp_cell.
Definition pp_search_cell_result `{FArgs} {A B : Set}
(pp_cell : Format.formatter → cell A B → unit) (fmt : Format.formatter)
(function_parameter : search_cell_result B A) : unit :=
match function_parameter with
| Found ptr ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Found("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))) "Found(%a)") pp_cell
ptr
|
Nearest {|
search_cell_result.Nearest.lower := lower;
search_cell_result.Nearest.upper := upper
|} ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Nearest(lower="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ";upper="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"Nearest(lower=%a;upper=%a)") pp_cell lower
(Format.pp_print_option None pp_cell) upper
| No_exact_or_lower_ptr ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "No_exact_or_lower_ptr"
CamlinternalFormatBasics.End_of_format) "No_exact_or_lower_ptr")
| Deref_returned_none ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Deref_returned_none"
CamlinternalFormatBasics.End_of_format) "Deref_returned_none")
end.
Definition pp_search_result `{FArgs} {A B : Set}
(pp_cell : Format.formatter → cell A B → unit) (fmt : Format.formatter)
(function_parameter : search_result A B) : unit :=
let '{|
search_result.rev_path := rev_path;
search_result.last_cell := last_cell
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "{rev_path = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "; last_point = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "}" % char
CamlinternalFormatBasics.End_of_format)))))
"{rev_path = %a; last_point = %a}") (pp_rev_path pp_cell) rev_path
(pp_search_cell_result pp_cell) last_cell.
#[bypass_check(guard)]
Definition search `{FArgs} {ptr content : Set}
(deref : ptr → option (cell content ptr)) (compare : content → int)
(cell_value : cell content ptr) : search_result content ptr :=
let '(op_eq, op_lt, op_gt) :=
(Compare.Int.op_eq, Compare.Int.op_lt, Compare.Int.op_gt) in
let fix aux
(rev_path : list (cell content ptr)) (cell_value : cell content ptr)
(ix : int) {struct ix} : search_result content ptr :=
let back_pointers_length :=
FallbackArray.length cell_value.(cell.back_pointers) in
if op_eq back_pointers_length 0 then
{| search_result.rev_path := rev_path;
search_result.last_cell := No_exact_or_lower_ptr; |}
else
let candidate_ptr :=
match back_pointer cell_value ix with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert ptr false
| Some candidate_ptr ⇒ candidate_ptr
end in
match deref candidate_ptr with
| None ⇒
{| search_result.rev_path := rev_path;
search_result.last_cell := Deref_returned_none; |}
| Some next_cell ⇒
let comparison := compare next_cell.(cell.content) in
if op_eq comparison 0 then
let rev_path := cons next_cell rev_path in
{| search_result.rev_path := rev_path;
search_result.last_cell := Found next_cell; |}
else
if op_gt comparison 0 then
if op_lt ix (back_pointers_length -i 1) then
aux rev_path cell_value (ix +i 1)
else
let rev_path := cons next_cell rev_path in
aux rev_path next_cell 0
else
if op_eq ix 0 then
let rev_path := cons next_cell rev_path in
{| search_result.rev_path := rev_path;
search_result.last_cell :=
Nearest
{| search_cell_result.Nearest.lower := next_cell;
search_cell_result.Nearest.upper := Some cell_value; |};
|}
else
let good_candidate_ptr :=
match back_pointer cell_value (ix -i 1) with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert ptr false
| Some candidate_ptr ⇒ candidate_ptr
end in
match deref good_candidate_ptr with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (search_result content ptr) false
| Some good_next_cell ⇒
let rev_path := cons good_next_cell rev_path in
aux rev_path good_next_cell 0
end
end in
let comparison := compare cell_value.(cell.content) in
if comparison =i 0 then
{| search_result.rev_path := [ cell_value ];
search_result.last_cell := Found cell_value; |}
else
if comparison <i 0 then
{| search_result.rev_path := [ cell_value ];
search_result.last_cell :=
Nearest
{| search_cell_result.Nearest.lower := cell_value;
search_cell_result.Nearest.upper := None; |}; |}
else
aux [ cell_value ] cell_value 0.
(* Make *)
Definition functor `{FArgs} :=
{|
S.pp _ _ := pp;
S.equal _ _ := equal;
S.encoding _ _ := encoding;
S.index_value _ _ := index_value;
S.content _ _ := content;
S.back_pointer _ _ := back_pointer;
S.back_pointers _ _ := back_pointers;
S.genesis _ _ := genesis;
S.next _ _ := next;
S.find _ _ := find;
S.back_path _ _ := back_path;
S.valid_back_path _ _ := valid_back_path;
S.pp_search_result _ _ := pp_search_result;
S.search _ _ := search
|}.
End Make.
Definition Make (Parameters : S_Parameters) : S (cell := _) :=
let '_ := Make.Build_FArgs Parameters in
Make.functor.
(* ❌ Assert instruction is not handled. *)
assert unit (Parameters.(S_Parameters.basis) ≥i 2).
Module cell.
Record record `{FArgs} {content ptr : Set} : Set := Build {
content : content;
back_pointers : FallbackArray.t (option ptr);
index : int;
}.
Arguments record {_}.
Definition with_content `{FArgs} {t_content t_ptr} content
(r : record t_content t_ptr) :=
Build _ t_content t_ptr content r.(back_pointers) r.(index).
Definition with_back_pointers `{FArgs} {t_content t_ptr} back_pointers
(r : record t_content t_ptr) :=
Build _ t_content t_ptr r.(content) back_pointers r.(index).
Definition with_index `{FArgs} {t_content t_ptr} index
(r : record t_content t_ptr) :=
Build _ t_content t_ptr r.(content) r.(back_pointers) index.
End cell.
Definition cell `{FArgs} := cell.record.
Definition equal `{FArgs} {A B C : Set}
(equal_ptr : A → A → bool) (equal_content : B → C → bool)
(cell1 : cell B A) (cell2 : cell C A) : bool :=
let equal_back_pointers
(b1 : FallbackArray.t (option A)) (b2 : FallbackArray.t (option A))
: bool :=
((FallbackArray.length b1) =i (FallbackArray.length b2)) &&
(Pervasives.fst
(FallbackArray.fold
(fun (function_parameter : bool × int) ⇒
let '(equal, i_value) := function_parameter in
fun (h1 : option A) ⇒
((equal &&
(Option.equal equal_ptr h1 (FallbackArray.get b2 i_value))),
(i_value +i 1))) b1 (true, 0))) in
let '{|
cell.content := content;
cell.back_pointers := back_pointers;
cell.index := index_value
|} := cell1 in
(equal_content content cell2.(cell.content)) &&
((Compare.Int.equal index_value cell2.(cell.index)) &&
(equal_back_pointers back_pointers cell2.(cell.back_pointers))).
Definition index_value `{FArgs} {A B : Set} (cell_value : cell A B) : int :=
cell_value.(cell.index).
Definition back_pointers_to_list `{FArgs} {A : Set}
(a_value : FallbackArray.t (option A)) : list A :=
List.rev
(FallbackArray.fold
(fun (l_value : list A) ⇒
fun (function_parameter : option A) ⇒
match function_parameter with
| Some ptr ⇒ cons ptr l_value
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (list _) false
end) a_value nil).
Definition pp `{FArgs} {A B : Set}
(pp_ptr : Format.formatter → A → unit)
(pp_content : Format.formatter → B → unit) (fmt : Format.formatter)
(function_parameter : cell B A) : unit :=
let '{|
cell.content := content;
cell.back_pointers := back_pointers;
cell.index := index_value
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
(String.String "010" " content = ")
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
(String.String "010" " index = ")
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
(String.String "010" " back_pointers = ")
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
(String.String "010" " ")
CamlinternalFormatBasics.End_of_format)))))))
(String.String "010"
(" content = %a" ++
String.String "010"
(" index = %d" ++
String.String "010"
(" back_pointers = %a" ++ String.String "010" " ")))))
pp_content content index_value (Format.pp_print_list None pp_ptr)
(back_pointers_to_list back_pointers).
Definition encoding `{FArgs} {A B : Set}
(ptr_encoding : Data_encoding.encoding A)
(content_encoding : Data_encoding.encoding B)
: Data_encoding.encoding (cell B A) :=
let of_list :=
FallbackArray.of_list None (fun (c_value : A) ⇒ Some c_value) in
let to_list {C : Set} : FallbackArray.t (option C) → list C :=
back_pointers_to_list in
Data_encoding.conv
(fun (function_parameter : cell B A) ⇒
let '{|
cell.content := content;
cell.back_pointers := back_pointers;
cell.index := index_value
|} := function_parameter in
(index_value, content, (to_list back_pointers)))
(fun (function_parameter : int × B × list A) ⇒
let '(index_value, content, back_pointers) := function_parameter in
{| cell.content := content; cell.back_pointers := of_list back_pointers;
cell.index := index_value; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "index" Data_encoding.int31)
(Data_encoding.req None None "content" content_encoding)
(Data_encoding.req None None "back_pointers"
(Data_encoding.list_value None ptr_encoding))).
Definition content `{FArgs} {A B : Set} (cell_value : cell A B) : A :=
cell_value.(cell.content).
Definition back_pointers `{FArgs} {A B : Set} (cell_value : cell A B)
: list B := back_pointers_to_list cell_value.(cell.back_pointers).
Definition genesis `{FArgs} {A B : Set} (content : A) : cell A B :=
{| cell.content := content; cell.back_pointers := FallbackArray.make 0 None;
cell.index := 0; |}.
Definition back_pointer `{FArgs} {A B : Set}
(cell_value : cell A B) (i_value : int) : option B :=
FallbackArray.get cell_value.(cell.back_pointers) i_value.
Definition back_pointer_unsafe `{FArgs} {A B : Set}
(cell_value : cell A B) (i_value : int) : B :=
match FallbackArray.get cell_value.(cell.back_pointers) i_value with
| Some ptr ⇒ ptr
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert _ false
end.
#[bypass_check(guard)]
Definition next `{FArgs} {A B C : Set}
(prev_cell : cell A B) (prev_cell_ptr : B) (content : C) : cell C B :=
let index_value := prev_cell.(cell.index) +i 1 in
let back_pointers :=
let fix aux (power : int) (accu_value : list B) (i_value : int)
{struct power} : list B :=
if index_value <i power then
List.rev accu_value
else
let back_pointer_i :=
if (Pervasives._mod index_value power) =i 0 then
prev_cell_ptr
else
back_pointer_unsafe prev_cell i_value in
let accu_value := cons back_pointer_i accu_value in
aux (power ×i Parameters.(S_Parameters.basis)) accu_value
(i_value +i 1) in
aux 1 nil 0 in
let back_pointers := FallbackArray.of_list None Option.some back_pointers in
{| cell.content := content; cell.back_pointers := back_pointers;
cell.index := index_value; |}.
#[bypass_check(guard)]
Definition list_powers `{FArgs} {A B : Set} (cell_value : cell A B)
: FallbackArray.t int :=
let fix aux (n_value : int) (prev : int) (p_value : list int)
{struct n_value} : list int :=
if n_value ≤i 0 then
List.rev p_value
else
aux (n_value -i 1) (Parameters.(S_Parameters.basis) ×i prev)
(cons prev p_value) in
FallbackArray.of_list 0 (fun (x_value : int) ⇒ x_value)
(aux (FallbackArray.length cell_value.(cell.back_pointers)) 1 nil).
#[bypass_check(guard)]
Definition best_skip `{FArgs} {A B : Set}
(cell_value : cell A B) (target_index : int) (powers : FallbackArray.t int)
: option int :=
let pointed_cell_index (i_value : int) : int :=
(cell_value.(cell.index) -i
(Pervasives._mod cell_value.(cell.index)
(FallbackArray.get powers i_value))) -i 1 in
let fix binary_search (start_idx : int) (end_idx : int) {struct start_idx}
: option int :=
if start_idx ≥i end_idx then
Some start_idx
else
let mid_idx := start_idx +i ((end_idx -i start_idx) /i 2) in
let mid_cell_index := pointed_cell_index mid_idx in
if mid_cell_index =i target_index then
Some mid_idx
else
if mid_cell_index <i target_index then
binary_search start_idx (mid_idx -i 1)
else
let prev_mid_cell_index := pointed_cell_index (mid_idx +i 1) in
if prev_mid_cell_index =i target_index then
Some (mid_idx +i 1)
else
if prev_mid_cell_index <i target_index then
Some mid_idx
else
binary_search (mid_idx +i 1) end_idx in
binary_search 0
((FallbackArray.length cell_value.(cell.back_pointers)) -i 1).
#[bypass_check(guard)]
Definition rev_back_path `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (list A) :=
let× cell_value := deref cell_ptr in
let powers := list_powers cell_value in
let fix aux (path : list A) (ptr : A) {struct ptr} : option (list A) :=
let path := cons ptr path in
let× cell_value := deref ptr in
let index_value := cell_value.(cell.index) in
if target_index =i index_value then
return× path
else
if target_index >i index_value then
Error_monad.Option_syntax.fail
else
let× best_idx := best_skip cell_value target_index powers in
let× ptr := back_pointer cell_value best_idx in
aux path ptr in
aux nil cell_ptr.
Definition find `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (cell B A) :=
let× rev_back_path := rev_back_path deref cell_ptr target_index in
let× cell_ptr := List.hd rev_back_path in
deref cell_ptr.
Definition back_path `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (list A) :=
Error_monad.Option_syntax.op_letplus
(rev_back_path deref cell_ptr target_index)
(fun rev_back_path ⇒ List.rev rev_back_path).
#[bypass_check(guard)]
Definition mem `{FArgs} {A B : Set}
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B)) : bool :=
let n_value := FallbackArray.length l_value in
let fix aux (idx : int) {struct idx} : bool :=
if idx ≥i n_value then
false
else
match FallbackArray.get l_value idx with
| None ⇒ aux (idx +i 1)
| Some y_value ⇒
if equal x_value y_value then
true
else
aux (idx +i 1)
end in
aux 0.
Definition assume_some `{FArgs} {A : Set}
(o_value : option A) (f_value : A → bool) : bool :=
match o_value with
| None ⇒ false
| Some x_value ⇒ f_value x_value
end.
#[bypass_check(guard)]
Definition valid_back_path `{FArgs} {A B : Set}
(equal_ptr : A → A → bool) (deref : A → option (cell B A)) (cell_ptr : A)
(target_ptr : A) (path : list A) : bool :=
assume_some (deref target_ptr)
(fun (target : cell B A) ⇒
assume_some (deref cell_ptr)
(fun (cell_value : cell B A) ⇒
let target_index : int :=
index_value target
in let cell_index : int :=
index_value cell_value
in let powers : FallbackArray.t int :=
list_powers cell_value in
let fix valid_path
(index_value : int) (cell_ptr : A) (path : list A) {struct path}
: bool :=
match (cell_ptr, path) with
| (final_cell, []) ⇒
(equal_ptr target_ptr final_cell) &&
(index_value =i target_index)
| (cell_ptr, cons cell_ptr' path) ⇒
assume_some (deref cell_ptr)
(fun (cell_value : cell B A) ⇒
assume_some (deref cell_ptr')
(fun (cell' : cell B A) ⇒
(mem equal_ptr cell_ptr' cell_value.(cell.back_pointers))
&&
(assume_some (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
assume_some (back_pointer cell_value best_idx)
(fun (best_ptr : A) ⇒
let minimal := equal_ptr best_ptr cell_ptr' in
let index' := cell'.(cell.index) in
minimal && (valid_path index' cell_ptr' path))))))
end in
match path with
| [] ⇒ false
| cons first_cell_ptr path ⇒
(equal_ptr first_cell_ptr cell_ptr) &&
(valid_path cell_index cell_ptr path)
end)).
Definition search_cell_result `{FArgs} (ptr content : Set) : Set :=
search_cell_result (cell content ptr).
Definition search_result `{FArgs} (ptr content : Set) : Set :=
search_result (cell ptr content).
Definition pp_rev_path `{FArgs} {A : Set}
(pp_cell : Format.formatter → A → unit)
: Format.formatter → list A → unit :=
Format.pp_print_list (Some Format.pp_print_space) pp_cell.
Definition pp_search_cell_result `{FArgs} {A B : Set}
(pp_cell : Format.formatter → cell A B → unit) (fmt : Format.formatter)
(function_parameter : search_cell_result B A) : unit :=
match function_parameter with
| Found ptr ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Found("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format))) "Found(%a)") pp_cell
ptr
|
Nearest {|
search_cell_result.Nearest.lower := lower;
search_cell_result.Nearest.upper := upper
|} ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Nearest(lower="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ";upper="
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))
"Nearest(lower=%a;upper=%a)") pp_cell lower
(Format.pp_print_option None pp_cell) upper
| No_exact_or_lower_ptr ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "No_exact_or_lower_ptr"
CamlinternalFormatBasics.End_of_format) "No_exact_or_lower_ptr")
| Deref_returned_none ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Deref_returned_none"
CamlinternalFormatBasics.End_of_format) "Deref_returned_none")
end.
Definition pp_search_result `{FArgs} {A B : Set}
(pp_cell : Format.formatter → cell A B → unit) (fmt : Format.formatter)
(function_parameter : search_result A B) : unit :=
let '{|
search_result.rev_path := rev_path;
search_result.last_cell := last_cell
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "{rev_path = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal "; last_point = "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "}" % char
CamlinternalFormatBasics.End_of_format)))))
"{rev_path = %a; last_point = %a}") (pp_rev_path pp_cell) rev_path
(pp_search_cell_result pp_cell) last_cell.
#[bypass_check(guard)]
Definition search `{FArgs} {ptr content : Set}
(deref : ptr → option (cell content ptr)) (compare : content → int)
(cell_value : cell content ptr) : search_result content ptr :=
let '(op_eq, op_lt, op_gt) :=
(Compare.Int.op_eq, Compare.Int.op_lt, Compare.Int.op_gt) in
let fix aux
(rev_path : list (cell content ptr)) (cell_value : cell content ptr)
(ix : int) {struct ix} : search_result content ptr :=
let back_pointers_length :=
FallbackArray.length cell_value.(cell.back_pointers) in
if op_eq back_pointers_length 0 then
{| search_result.rev_path := rev_path;
search_result.last_cell := No_exact_or_lower_ptr; |}
else
let candidate_ptr :=
match back_pointer cell_value ix with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert ptr false
| Some candidate_ptr ⇒ candidate_ptr
end in
match deref candidate_ptr with
| None ⇒
{| search_result.rev_path := rev_path;
search_result.last_cell := Deref_returned_none; |}
| Some next_cell ⇒
let comparison := compare next_cell.(cell.content) in
if op_eq comparison 0 then
let rev_path := cons next_cell rev_path in
{| search_result.rev_path := rev_path;
search_result.last_cell := Found next_cell; |}
else
if op_gt comparison 0 then
if op_lt ix (back_pointers_length -i 1) then
aux rev_path cell_value (ix +i 1)
else
let rev_path := cons next_cell rev_path in
aux rev_path next_cell 0
else
if op_eq ix 0 then
let rev_path := cons next_cell rev_path in
{| search_result.rev_path := rev_path;
search_result.last_cell :=
Nearest
{| search_cell_result.Nearest.lower := next_cell;
search_cell_result.Nearest.upper := Some cell_value; |};
|}
else
let good_candidate_ptr :=
match back_pointer cell_value (ix -i 1) with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert ptr false
| Some candidate_ptr ⇒ candidate_ptr
end in
match deref good_candidate_ptr with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert (search_result content ptr) false
| Some good_next_cell ⇒
let rev_path := cons good_next_cell rev_path in
aux rev_path good_next_cell 0
end
end in
let comparison := compare cell_value.(cell.content) in
if comparison =i 0 then
{| search_result.rev_path := [ cell_value ];
search_result.last_cell := Found cell_value; |}
else
if comparison <i 0 then
{| search_result.rev_path := [ cell_value ];
search_result.last_cell :=
Nearest
{| search_cell_result.Nearest.lower := cell_value;
search_cell_result.Nearest.upper := None; |}; |}
else
aux [ cell_value ] cell_value 0.
(* Make *)
Definition functor `{FArgs} :=
{|
S.pp _ _ := pp;
S.equal _ _ := equal;
S.encoding _ _ := encoding;
S.index_value _ _ := index_value;
S.content _ _ := content;
S.back_pointer _ _ := back_pointer;
S.back_pointers _ _ := back_pointers;
S.genesis _ _ := genesis;
S.next _ _ := next;
S.find _ _ := find;
S.back_path _ _ := back_path;
S.valid_back_path _ _ := valid_back_path;
S.pp_search_result _ _ := pp_search_result;
S.search _ _ := search
|}.
End Make.
Definition Make (Parameters : S_Parameters) : S (cell := _) :=
let '_ := Make.Build_FArgs Parameters in
Make.functor.