🔗 Skip_list_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Module S.
Record signature {cell : Set → Set → Set} : Set := {
cell := cell;
equal :
∀ {content ptr : Set},
(content → content → bool) → (ptr → ptr → 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;
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;
}.
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;
}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Module S.
Record signature {cell : Set → Set → Set} : Set := {
cell := cell;
equal :
∀ {content ptr : Set},
(content → content → bool) → (ptr → ptr → 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;
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;
}.
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_content : A → B → bool) (equal_ptr : C → C → bool)
(cell1 : cell A C) (cell2 : cell B C) : bool :=
let equal_back_pointers
(b1 : FallbackArray.t (option C)) (b2 : FallbackArray.t (option C))
: 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 C) ⇒
((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)) &&
((equal_back_pointers back_pointers cell2.(cell.back_pointers)) &&
(Compare.Int.equal index_value cell2.(cell.index))).
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 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 (fun (x_value : B) ⇒ Some x_value)
back_pointers in
{| cell.content := content; cell.back_pointers := back_pointers;
cell.index := index_value; |}.
#[bypass_check(guard)]
Definition best_skip `{FArgs} {A B : Set}
(cell_value : cell A B) (target_index : int) : option int :=
let index_value := cell_value.(cell.index) in
let fix aux
(idx : int) (pow : int) (best_idx : option int) (best_skip : option int)
{struct idx} : option int :=
if idx ≥i (FallbackArray.length cell_value.(cell.back_pointers)) then
best_idx
else
let idx_index := (index_value -i (Pervasives._mod index_value pow)) -i 1
in
let skip := index_value -i idx_index in
if
(idx_index <i target_index) ||
(Option.equal Compare.Int.equal (Some skip) best_skip)
then
best_idx
else
aux (idx +i 1) (Parameters.(S_Parameters.basis) ×i pow) (Some idx)
(Some skip) in
aux 0 1 None None.
#[bypass_check(guard)]
Definition back_path `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (list A) :=
let fix aux (path : list A) (ptr : A) {struct ptr} : option (list A) :=
let path := cons ptr path in
Option.bind (deref ptr)
(fun (cell_value : cell B A) ⇒
let index_value := cell_value.(cell.index) in
if target_index =i index_value then
Some (List.rev path)
else
if target_index >i index_value then
None
else
Option.bind (best_skip cell_value target_index)
(fun (best_idx : int) ⇒
Option.bind (back_pointer cell_value best_idx)
(fun (ptr : A) ⇒ aux path ptr))) in
aux nil cell_ptr.
#[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 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)
(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)).
(* Make *)
Definition functor `{FArgs} :=
{|
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.back_path _ _ := back_path;
S.valid_back_path _ _ := valid_back_path
|}.
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_content : A → B → bool) (equal_ptr : C → C → bool)
(cell1 : cell A C) (cell2 : cell B C) : bool :=
let equal_back_pointers
(b1 : FallbackArray.t (option C)) (b2 : FallbackArray.t (option C))
: 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 C) ⇒
((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)) &&
((equal_back_pointers back_pointers cell2.(cell.back_pointers)) &&
(Compare.Int.equal index_value cell2.(cell.index))).
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 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 (fun (x_value : B) ⇒ Some x_value)
back_pointers in
{| cell.content := content; cell.back_pointers := back_pointers;
cell.index := index_value; |}.
#[bypass_check(guard)]
Definition best_skip `{FArgs} {A B : Set}
(cell_value : cell A B) (target_index : int) : option int :=
let index_value := cell_value.(cell.index) in
let fix aux
(idx : int) (pow : int) (best_idx : option int) (best_skip : option int)
{struct idx} : option int :=
if idx ≥i (FallbackArray.length cell_value.(cell.back_pointers)) then
best_idx
else
let idx_index := (index_value -i (Pervasives._mod index_value pow)) -i 1
in
let skip := index_value -i idx_index in
if
(idx_index <i target_index) ||
(Option.equal Compare.Int.equal (Some skip) best_skip)
then
best_idx
else
aux (idx +i 1) (Parameters.(S_Parameters.basis) ×i pow) (Some idx)
(Some skip) in
aux 0 1 None None.
#[bypass_check(guard)]
Definition back_path `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (list A) :=
let fix aux (path : list A) (ptr : A) {struct ptr} : option (list A) :=
let path := cons ptr path in
Option.bind (deref ptr)
(fun (cell_value : cell B A) ⇒
let index_value := cell_value.(cell.index) in
if target_index =i index_value then
Some (List.rev path)
else
if target_index >i index_value then
None
else
Option.bind (best_skip cell_value target_index)
(fun (best_idx : int) ⇒
Option.bind (back_pointer cell_value best_idx)
(fun (ptr : A) ⇒ aux path ptr))) in
aux nil cell_ptr.
#[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 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)
(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)).
(* Make *)
Definition functor `{FArgs} :=
{|
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.back_path _ _ := back_path;
S.valid_back_path _ _ := valid_back_path
|}.
End Make.
Definition Make (Parameters : S_Parameters) : S (cell := _) :=
let '_ := Make.Build_FArgs Parameters in
Make.functor.