Skip to main content

🗳️ Vote_repr.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 proposal : Set := Protocol_hash.t.

Inductive ballot : Set :=
| Yay : ballot
| Nay : ballot
| Pass : ballot.

Definition ballot_encoding : Data_encoding.encoding ballot :=
  let of_int8 (function_parameter : int) : Pervasives.result ballot string :=
    match function_parameter with
    | 0 ⇒ Pervasives.Ok Yay
    | 1 ⇒ Pervasives.Ok Nay
    | 2 ⇒ Pervasives.Ok Pass
    | _Pervasives.Error "ballot_of_int8"
    end in
  let to_int8 (function_parameter : ballot) : int :=
    match function_parameter with
    | Yay ⇒ 0
    | Nay ⇒ 1
    | Pass ⇒ 2
    end in
  Data_encoding.splitted
    (Data_encoding.string_enum [ ("yay", Yay); ("nay", Nay); ("pass", Pass) ])
    (Data_encoding.conv_with_guard to_int8 of_int8 None Data_encoding.int8).

Definition equal_ballot (a_value : ballot) (b_value : ballot) : bool :=
  match (a_value, b_value) with
  | ((Yay, Yay) | (Nay, Nay) | (Pass, Pass)) ⇒ true
  | _false
  end.

Definition pp_ballot (ppf : Format.formatter) (function_parameter : ballot)
  : unit :=
  match function_parameter with
  | Yay
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "yay"
          CamlinternalFormatBasics.End_of_format) "yay")
  | Nay
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "nay"
          CamlinternalFormatBasics.End_of_format) "nay")
  | Pass
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "pass"
          CamlinternalFormatBasics.End_of_format) "pass")
  end.