Skip to main content

🗳️ Voting_period_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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Level_repr.

Inductive kind : Set :=
| Proposal : kind
| Exploration : kind
| Cooldown : kind
| Promotion : kind
| Adoption : kind.

Definition string_of_kind (function_parameter : kind) : string :=
  match function_parameter with
  | Proposal ⇒ "proposal"
  | Exploration ⇒ "exploration"
  | Cooldown ⇒ "cooldown"
  | Promotion ⇒ "promotion"
  | Adoption ⇒ "adoption"
  end.

Definition pp_kind (ppf : Format.formatter) (kind_value : kind) : unit :=
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
        CamlinternalFormatBasics.End_of_format) "%s")
    (string_of_kind kind_value).

Definition kind_encoding : Data_encoding.encoding kind :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "Proposal" None (Data_encoding.Tag 0)
        (Data_encoding.constant "proposal")
        (fun (function_parameter : kind) ⇒
          match function_parameter with
          | ProposalSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Proposal);
      Data_encoding.case_value "exploration" None (Data_encoding.Tag 1)
        (Data_encoding.constant "exploration")
        (fun (function_parameter : kind) ⇒
          match function_parameter with
          | ExplorationSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Exploration);
      Data_encoding.case_value "Cooldown" None (Data_encoding.Tag 2)
        (Data_encoding.constant "cooldown")
        (fun (function_parameter : kind) ⇒
          match function_parameter with
          | CooldownSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Cooldown);
      Data_encoding.case_value "Promotion" None (Data_encoding.Tag 3)
        (Data_encoding.constant "promotion")
        (fun (function_parameter : kind) ⇒
          match function_parameter with
          | PromotionSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Promotion);
      Data_encoding.case_value "Adoption" None (Data_encoding.Tag 4)
        (Data_encoding.constant "adoption")
        (fun (function_parameter : kind) ⇒
          match function_parameter with
          | AdoptionSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Adoption)
    ].

Definition succ_kind (function_parameter : kind) : kind :=
  match function_parameter with
  | ProposalExploration
  | ExplorationCooldown
  | CooldownPromotion
  | PromotionAdoption
  | AdoptionProposal
  end.

Module voting_period.
  Record record : Set := Build {
    index : int32;
    kind : kind;
    start_position : int32;
  }.
  Definition with_index index (r : record) :=
    Build index r.(kind) r.(start_position).
  Definition with_kind kind (r : record) :=
    Build r.(index) kind r.(start_position).
  Definition with_start_position start_position (r : record) :=
    Build r.(index) r.(kind) start_position.
End voting_period.
Definition voting_period := voting_period.record.

Definition t : Set := voting_period.

Module info.
  Record record : Set := Build {
    voting_period : t;
    position : int32;
    remaining : int32;
  }.
  Definition with_voting_period voting_period (r : record) :=
    Build voting_period r.(position) r.(remaining).
  Definition with_position position (r : record) :=
    Build r.(voting_period) position r.(remaining).
  Definition with_remaining remaining (r : record) :=
    Build r.(voting_period) r.(position) remaining.
End info.
Definition info := info.record.

Definition root_value (start_position : int32) : voting_period :=
  {| voting_period.index := 0; voting_period.kind := Proposal;
    voting_period.start_position := start_position; |}.

Definition pp (ppf : Format.formatter) (function_parameter : voting_period)
  : unit :=
  let '{|
    voting_period.index := index_value;
      voting_period.kind := kind_value;
      voting_period.start_position := start_position
      |} := function_parameter in
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_gen
        (CamlinternalFormatBasics.Open_box
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal "<hv 2>"
              CamlinternalFormatBasics.End_of_format) "<hv 2>"))
        (CamlinternalFormatBasics.String_literal "index: "
          (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
            CamlinternalFormatBasics.No_padding
            CamlinternalFormatBasics.No_precision
            (CamlinternalFormatBasics.Char_literal "," % char
              (CamlinternalFormatBasics.Formatting_lit
                (CamlinternalFormatBasics.Break "@ " 1 0)
                (CamlinternalFormatBasics.String_literal "kind:"
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal "," % char
                      (CamlinternalFormatBasics.Formatting_lit
                        (CamlinternalFormatBasics.Break "@ " 1 0)
                        (CamlinternalFormatBasics.String_literal
                          "start_position: "
                          (CamlinternalFormatBasics.Int32
                            CamlinternalFormatBasics.Int_d
                            CamlinternalFormatBasics.No_padding
                            CamlinternalFormatBasics.No_precision
                            (CamlinternalFormatBasics.Formatting_lit
                              CamlinternalFormatBasics.Close_box
                              CamlinternalFormatBasics.End_of_format))))))))))))
      "@[<hv 2>index: %ld,@ kind:%a,@ start_position: %ld@]") index_value
    pp_kind kind_value start_position.

Definition pp_info (ppf : Format.formatter) (function_parameter : info)
  : unit :=
  let '{|
    info.voting_period := voting_period;
      info.position := position;
      info.remaining := remaining
      |} := function_parameter in
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_gen
        (CamlinternalFormatBasics.Open_box
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal "<hv 2>"
              CamlinternalFormatBasics.End_of_format) "<hv 2>"))
        (CamlinternalFormatBasics.String_literal "voting_period: "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Char_literal "," % char
              (CamlinternalFormatBasics.Formatting_lit
                (CamlinternalFormatBasics.Break "@ " 1 0)
                (CamlinternalFormatBasics.String_literal "position:"
                  (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.No_precision
                    (CamlinternalFormatBasics.Char_literal "," % char
                      (CamlinternalFormatBasics.Formatting_lit
                        (CamlinternalFormatBasics.Break "@ " 1 0)
                        (CamlinternalFormatBasics.String_literal "remaining: "
                          (CamlinternalFormatBasics.Int32
                            CamlinternalFormatBasics.Int_d
                            CamlinternalFormatBasics.No_padding
                            CamlinternalFormatBasics.No_precision
                            (CamlinternalFormatBasics.Formatting_lit
                              CamlinternalFormatBasics.Close_box
                              CamlinternalFormatBasics.End_of_format))))))))))))
      "@[<hv 2>voting_period: %a,@ position:%ld,@ remaining: %ld@]") pp
    voting_period position remaining.

Definition encoding : Data_encoding.encoding voting_period :=
  Data_encoding.conv
    (fun (function_parameter : voting_period) ⇒
      let '{|
        voting_period.index := index_value;
          voting_period.kind := kind_value;
          voting_period.start_position := start_position
          |} := function_parameter in
      (index_value, kind_value, start_position))
    (fun (function_parameter : int32 × kind × int32) ⇒
      let '(index_value, kind_value, start_position) := function_parameter in
      {| voting_period.index := index_value; voting_period.kind := kind_value;
        voting_period.start_position := start_position; |}) None
    (Data_encoding.obj3
      (Data_encoding.req None
        (Some
          "The voting period's index. Starts at 0 with the first block of the Alpha family of protocols.")
        "index" Data_encoding.int32_value)
      (Data_encoding.req None
        (Some "One of the several kinds of periods in the voting procedure.")
        "kind" kind_encoding)
      (Data_encoding.req None
        (Some
          "The relative position of the first level of the period with respect to the first level of the Alpha family of protocols.")
        "start_position" Data_encoding.int32_value)).

Definition info_encoding : Data_encoding.encoding info :=
  Data_encoding.conv
    (fun (function_parameter : info) ⇒
      let '{|
        info.voting_period := voting_period;
          info.position := position;
          info.remaining := remaining
          |} := function_parameter in
      (voting_period, position, remaining))
    (fun (function_parameter : t × int32 × int32) ⇒
      let '(voting_period, position, remaining) := function_parameter in
      {| info.voting_period := voting_period; info.position := position;
        info.remaining := remaining; |}) None
    (Data_encoding.obj3
      (Data_encoding.req None
        (Some "The voting period to which the block belongs.") "voting_period"
        encoding)
      (Data_encoding.req None
        (Some "The position of the block within the voting period.") "position"
        Data_encoding.int32_value)
      (Data_encoding.req None
        (Some
          "The number of blocks remaining till the end of the voting period.")
        "remaining" Data_encoding.int32_value)).

Definition Compare_Make_include :=
  Compare.Make
    (let t : Set := t in
    let compare (p_value : voting_period) (p' : voting_period) : int :=
      Compare.Int32.(Compare.S.compare) p_value.(voting_period.index)
        p'.(voting_period.index) in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Inclusion of the module [Compare_Make_include]
Definition op_eq := Compare_Make_include.(Compare.S.op_eq).

Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).

Definition op_lt := Compare_Make_include.(Compare.S.op_lt).

Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).

Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).

Definition op_gt := Compare_Make_include.(Compare.S.op_gt).

Definition compare := Compare_Make_include.(Compare.S.compare).

Definition equal := Compare_Make_include.(Compare.S.equal).

Definition max := Compare_Make_include.(Compare.S.max).

Definition min := Compare_Make_include.(Compare.S.min).

Definition raw_reset (period : voting_period) (start_position : int32)
  : voting_period :=
  let index_value := Int32.succ period.(voting_period.index) in
  let kind_value := Proposal in
  {| voting_period.index := index_value; voting_period.kind := kind_value;
    voting_period.start_position := start_position; |}.

Definition raw_succ (period : voting_period) (start_position : int32)
  : voting_period :=
  let index_value := Int32.succ period.(voting_period.index) in
  let kind_value := succ_kind period.(voting_period.kind) in
  {| voting_period.index := index_value; voting_period.kind := kind_value;
    voting_period.start_position := start_position; |}.

Definition position_since (level : Level_repr.t) (voting_period : t) : int32 :=
  level.(Level_repr.t.level_position) -i32
  voting_period.(voting_period.start_position).

Definition remaining_blocks
  (level : Level_repr.t) (voting_period : t) (blocks_per_voting_period : int32)
  : int32 :=
  let position := position_since level voting_period in
  blocks_per_voting_period -i32 (Int32.succ position).