Skip to main content

🚥 Bitset.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.

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