🃏 Misc.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Unset Positivity Checking.

Require Import TezosOfOCaml.Environment.V8.

Definition Public_key_map :=
  Map.Make
    {|
      Compare.COMPARABLE.compare :=
        Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.compare)
    |}.

Definition lazyt (a : Set) : Set := unit → a.

Inductive lazy_list_t (a : Set) : Set :=
| LCons : a → lazyt (M? (lazy_list_t a)) → lazy_list_t a.

Arguments LCons {_}.

Definition lazy_list (a : Set) : Set := M? (lazy_list_t a).

#[bypass_check(guard)]
Fixpoint op_minusminusgt (i_value : int) (j_value : int) {struct i_value}
  : list int :=
  if i_value >i j_value then
    nil
  else
    cons i_value (op_minusminusgt (Pervasives.succ i_value) j_value).

#[bypass_check(guard)]
Fixpoint op_ltminusminus (i_value : int) (j_value : int) {struct j_value}
  : list int :=
  if i_value >i j_value then
    nil
  else
    cons j_value (op_ltminusminus i_value (Pervasives.pred j_value)).

#[bypass_check(guard)]
Fixpoint op_minusminusminusgt (i_value : int32) (j_value : int32)
  {struct i_value} : list int32 :=
  if i_value >i32 j_value then
    nil
  else
    cons i_value (op_minusminusminusgt (Int32.succ i_value) j_value).

Module Split.
  #[bypass_check(guard)]
  Fixpoint do_slashes
    (env : ascii × string × int) (acc_value : list string) (limit : int)
    (i_value : int) {struct i_value} : list string :=
    let '(delim, path, l_value) := env in
    if i_value ≥i l_value then
      List.rev acc_value
    else
      if Compare.Char.(Compare.S.op_eq) (String.get path i_value) delim then
        do_slashes env acc_value limit (i_value +i 1)
      else
        do_split env acc_value limit i_value
  
  with do_split
    (env : ascii × string × int) (acc_value : list string) (limit : int)
    (i_value : int) {struct limit} : list string :=
    let '(_, path, l_value) := env in
    if limit ≤i 0 then
      if i_value =i l_value then
        List.rev acc_value
      else
        List.rev (cons (String.sub path i_value (l_value -i i_value)) acc_value)
    else
      do_component env acc_value (Pervasives.pred limit) i_value i_value
  
  with do_component
    (env : ascii × string × int) (acc_value : list string) (limit : int)
    (i_value : int) (j_value : int) {struct j_value} : list string :=
    let '(delim, path, l_value) := env in
    if j_value ≥i l_value then
      if i_value =i j_value then
        List.rev acc_value
      else
        List.rev (cons (String.sub path i_value (j_value -i i_value)) acc_value)
    else
      if Compare.Char.(Compare.S.op_eq) (String.get path j_value) delim then
        do_slashes env
          (cons (String.sub path i_value (j_value -i i_value)) acc_value) limit
          j_value
      else
        do_component env acc_value limit i_value (j_value +i 1).
End Split.

Definition split (delim : ascii) (op_staroptstar : option int)
  : string → list string :=
  let limit :=
    match op_staroptstar with
    | Some op_starsthstar ⇒ op_starsthstar
    | None ⇒ Pervasives.max_int
    end in
  fun (path : string) ⇒
    let l_value := String.length path in
    let env := (delim, path, l_value) in
    if limit >i 0 then
      Split.do_slashes env nil limit 0
    else
      [ path ].

Definition pp_print_paragraph (ppf : Format.formatter) (description : string)
  : unit :=
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_gen
        (CamlinternalFormatBasics.Open_box
          (CamlinternalFormatBasics.Format
            CamlinternalFormatBasics.End_of_format ""))
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.Formatting_lit
            CamlinternalFormatBasics.Close_box
            CamlinternalFormatBasics.End_of_format))) "@[%a@]")
    (Format.pp_print_list (Some Format.pp_print_space) Format.pp_print_string)
    (split " " % char None description).

Definition take {A : Set} (n_value : int) (l_value : list A)
  : option (list A × list A) :=
  let fix loop {B : Set} (acc_value : list B) (n_value : int) (xs : list B)
    : option (list B × list B) :=
    if n_value ≤i 0 then
      Some ((List.rev acc_value), xs)
    else
      match xs with
      | [] ⇒ None
      | cons x_value xs ⇒ loop (cons x_value acc_value) (n_value -i 1) xs
      end in
  loop nil n_value l_value.

Definition remove_prefix (prefix : string) (s_value : string) : option string :=
  let x_value := String.length prefix in
  let n_value := String.length s_value in
  if
    (n_value ≥i x_value) &&
    (Compare.String.(Compare.S.op_eq) (String.sub s_value 0 x_value) prefix)
  then
    Some (String.sub s_value x_value (n_value -i x_value))
  else
    None.

Fixpoint remove_elem_from_list {A : Set}
  (nb : int) (function_parameter : list A) : list A :=
  match
    (function_parameter,
      match function_parameter with
      | (cons _ _) as l_value ⇒ nb ≤i 0
      | _ ⇒ false
      end) with
  | ([], _) ⇒ nil
  | ((cons _ _) as l_value, true) ⇒ l_value
  | (cons _ tl, _) ⇒ remove_elem_from_list (nb -i 1) tl
  end.