Skip to main content

🔗 Skip_list_repr.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.V7.

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;
    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 ptrcons 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 ptrptr
    | 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 back_path `{FArgs} {A B : Set}
    (deref : A option (cell B A)) (cell_ptr : A) (target_index : int)
    : option (list A) :=
    Option.bind (deref cell_ptr)
      (fun (cell_value : cell B A) ⇒
        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
          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 powers)
                    (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
        | Noneaux (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
    | Nonefalse
    | Some x_valuef_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_ptrcandidate_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_ptrcandidate_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.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.