🚥 Bitset.v

Translated OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.

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

Init function; without side-effects in Coq

Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "bitfield_invalid_position" "Invalid bitfield\226\128\153s 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).