🎰 Slot_repr.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.

Init function; without side-effects in Coq

Definition init_module_repr : unit :=
  Error_monad.register_error_kind Error_monad.Permanent "slot.invalid_slot"
    "invalid slot" "Invalid slot"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (x_value : int) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "invalid slot: "
                (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  CamlinternalFormatBasics.End_of_format)) "invalid slot: %d")
            x_value))
    (Data_encoding.obj1
      (Data_encoding.req None None "bad_slot" Data_encoding.int31))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Invalid_slot" then
          let x_value := cast int payload in
          Some x_value
        else None
      end) (fun (x_value : int) ⇒ Build_extensible "Invalid_slot" int x_value).

Include Compare.Int.

Definition slot : Set := t.

Definition encoding : Data_encoding.encoding int := Data_encoding.uint16.

Definition pp : Format.formatter → int → unit := Format.pp_print_int.

Definition zero : int := 0.

Definition to_int {A : Set} (x_value : A) : A := x_value.

Definition max_value : int := (Pervasives.lsl 1 16) -i 1.

Definition of_int_do_not_use_except_for_parameters {A : Set} (i_value : A)
  : A := i_value.

Definition of_int (i_value : int) : M? int :=
  if (i_value <i 0) || (i_value >i max_value) then
    Error_monad.error_value (Build_extensible "Invalid_slot" int i_value)
  else
    return? i_value.

Definition succ (slot : int) : M? int := of_int (slot +i 1).

Definition Map :=
  Map.Make
    {|
      Compare.COMPARABLE.compare := Compare.Int.compare
    |}.

Definition _Set :=
  _Set.Make
    {|
      Compare.COMPARABLE.compare := Compare.Int.compare
    |}.

Module Range.

Records for the constructor parameters

  Module ConstructorRecords_t.
    Module t.
      Module Interval.
        Record record {lo hi : Set} : Set := Build {
          lo : lo;
          hi : hi;
        }.
        Arguments record : clear implicits.
        Definition with_lo {t_lo t_hi} lo (r : record t_lo t_hi) :=
          Build t_lo t_hi lo r.(hi).
        Definition with_hi {t_lo t_hi} hi (r : record t_lo t_hi) :=
          Build t_lo t_hi r.(lo) hi.
      End Interval.
      Definition Interval_skeleton := Interval.record.
    End t.
  End ConstructorRecords_t.
  Import ConstructorRecords_t.

  Reserved Notation "'t.Interval".

  Inductive t : Set :=
  | Interval : 't.Interval → t
  
  where "'t.Interval" := (t.Interval_skeleton int int).

  Module t.
    Include ConstructorRecords_t.t.
    Definition Interval := 't.Interval.
  End t.

  Definition create (min : int) (count : int) : M? t :=
    let? '_ :=
      Error_monad.error_when (op_lt min 0)
        (Build_extensible "Invalid_slot" int min) in
    let? '_ :=
      Error_monad.error_when (op_gt min max_value)
        (Build_extensible "Invalid_slot" int min) in
    let? '_ :=
      Error_monad.error_when (op_lt count 1)
        (Build_extensible "Invalid_slot" int count) in
    let? '_ :=
      Error_monad.error_when (op_gt count max_value)
        (Build_extensible "Invalid_slot" int count) in
    let max := (min +i count) -i 1 in
    let? '_ :=
      Error_monad.error_when (op_gt max max_value)
        (Build_extensible "Invalid_slot" int max) in
    return? (Interval {| t.Interval.lo := min; t.Interval.hi := max; |}).

  #[bypass_check(guard)]
  Definition fold {A : Set}
    (f_value : A → int → A) (init_value : A) (function_parameter : t) : A :=
    let 'Interval {| t.Interval.lo := lo; t.Interval.hi := hi |} :=
      function_parameter in
    let fix loop (acc_value : A) (next : int) {struct next} : A :=
      if next >i hi then
        acc_value
      else
        loop (f_value acc_value next) (next +i 1) in
    loop (f_value init_value lo) (lo +i 1).

  #[bypass_check(guard)]
  Definition fold_es {A B : Set}
    (f_value : A → int → Pervasives.result A B) (init_value : A)
    (function_parameter : t) : Pervasives.result A B :=
    let 'Interval {| t.Interval.lo := lo; t.Interval.hi := hi |} :=
      function_parameter in
    let fix loop (acc_value : A) (next : int) {struct next}
      : Pervasives.result A B :=
      if next >i hi then
        return? acc_value
      else
        let? acc_value := f_value acc_value next in
        loop acc_value (next +i 1) in
    let? acc_value := f_value init_value lo in
    loop acc_value (lo +i 1).

  #[bypass_check(guard)]
  Definition rev_fold_es {A B : Set}
    (f_value : A → int → Pervasives.result A B) (init_value : A)
    (function_parameter : t) : Pervasives.result A B :=
    let 'Interval {| t.Interval.lo := lo; t.Interval.hi := hi |} :=
      function_parameter in
    let fix loop (acc_value : A) (next : int) {struct next}
      : Pervasives.result A B :=
      if next <i lo then
        return? acc_value
      else
        let? acc_value := f_value acc_value next in
        loop acc_value (next -i 1) in
    let? acc_value := f_value init_value hi in
    loop acc_value (hi -i 1).
End Range.