🗳️ Voting_period_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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
| Proposal ⇒ Some 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
| Exploration ⇒ Some 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
| Cooldown ⇒ Some 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
| Promotion ⇒ Some 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
| Adoption ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Adoption)
].
Definition succ_kind (function_parameter : kind) : kind :=
match function_parameter with
| Proposal ⇒ Exploration
| Exploration ⇒ Cooldown
| Cooldown ⇒ Promotion
| Promotion ⇒ Adoption
| Adoption ⇒ Proposal
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
|}).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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
| Proposal ⇒ Some 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
| Exploration ⇒ Some 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
| Cooldown ⇒ Some 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
| Promotion ⇒ Some 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
| Adoption ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Adoption)
].
Definition succ_kind (function_parameter : kind) : kind :=
match function_parameter with
| Proposal ⇒ Exploration
| Exploration ⇒ Cooldown
| Cooldown ⇒ Promotion
| Promotion ⇒ Adoption
| Adoption ⇒ Proposal
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).
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).