🚥 Bitset.v

Translated OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.

Definition t : Set := Z.t.

Definition encoding : Data_encoding.encoding Z.t := Data_encoding.z_value.

Definition empty : Z.t := Z.zero.

Definition mem (field_value : Z.t) (pos : int) : M ? bool :=
  let ? '_ :=
    Error_monad.error_when (pos <i 0)
      (Build_extensible "Invalid_position" int pos) in
  return ? (Z.testbit field_value pos ).

Definition add (field_value : Z.t) (pos : int) : M ? Z.t :=
  let ? '_ :=
    Error_monad.error_when (pos <i 0)
      (Build_extensible "Invalid_position" int pos) in
  return ? (Z.logor field_value (Z.shift_left Z.one pos)).

Definition from_list (positions : list int) : M ? Z.t :=
  List.fold_left_e add empty positions.

Definition fill (length : int) : M ? Z.t :=
  let ? '_ :=
    Error_monad.error_when (length <i 0)
      (Build_extensible "Invalid_position" int length) in
  return ? (Z.pred (Z.shift_left Z.one length)).

Definition inter : Z.t → Z.t → Z.t := Z.logand.

Definition diff_value (b1 : Z.t) (b2 : Z.t) : Z.t := Z.logand b1 (Z.lognot b2).

Init function; without side-effects in Coq

Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "bitfield_invalid_position"
    ("Invalid bitfield" ++
      String.String "226"
        (String.String "128" (String.String "153" "s position")))
    "Bitfields does not accept negative positions" None
    (Data_encoding.obj1
      (Data_encoding.req None None "position" Data_encoding.int31))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Invalid_position" then
          let i_value := cast int payload in
          Some i_value
        else None
      end)
    (fun (i_value : int) ⇒ Build_extensible "Invalid_position" int i_value).

Definition occupied_size_in_bits : Z.t → int := Z.numbits.