🍬 Script_list.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

Module t.
  Record record {elt : Set} : Set := Build {
    elements : list elt;
    length : int;
  }.
  Arguments record : clear implicits.
  Definition with_elements {t_elt} elements (r : record t_elt) :=
    Build t_elt elements r.(length).
  Definition with_length {t_elt} length (r : record t_elt) :=
    Build t_elt r.(elements) length.
End t.
Definition t := t.record.

Definition of_list {A : Set} (l_value : list A) : t A :=
  {| t.elements := l_value; t.length := List.length l_value; |}.

Definition to_list {A : Set} (function_parameter : t A) : list A :=
  let '{| t.elements := elements; t.length := _ |} := function_parameter in
  elements.

Definition empty {a : Set} : t a := {| t.elements := nil; t.length := 0; |}.

Definition cons_value {a : Set} (elt_value : a) (l_value : t a) : t a :=
  {| t.elements := cons elt_value l_value.(t.elements);
    t.length := 1 +i l_value.(t.length); |}.

Definition length {A : Set} (function_parameter : t A) : int :=
  let '{| t.elements := _; t.length := length |} := function_parameter in
  length.

Definition uncons {A : Set} (function_parameter : t A) : option (A × t A) :=
  match function_parameter with
  | {| t.elements := []; t.length := _ |} ⇒ None
  | {| t.elements := cons hd tl; t.length := length |} ⇒
    Some (hd, {| t.elements := tl; t.length := length -i 1; |})
  end.

Definition rev {A : Set} (function_parameter : t A) : t A :=
  let '{| t.elements := elements; t.length := length |} := function_parameter in
  {| t.elements := List.rev elements; t.length := length; |}.