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

Definition t : Set := Z.t.

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

Definition empty : Z.t :=

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 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.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
    (fun (i_value : int) ⇒ Build_extensible "Invalid_position" int i_value).