Skip to main content

🃏 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.Proto_alpha.Environment.

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).

Axiom split : ascii option int string list string.

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 xsloop (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_valuenb i 0
      | _false
      end) with
  | ([], _)nil
  | ((cons _ _) as l_value, true)l_value
  | (cons _ tl, _)remove_elem_from_list (nb -i 1) tl
  end.