🗳️ Voting_services.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Module S.
Definition path : RPC_path.path Updater.rpc_context Updater.rpc_context :=
RPC_path.op_div RPC_path.open_root "votes".
Definition ballots
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
Alpha_context.Vote.ballots :=
RPC_service.get_service
(Some "Sum of ballots casted so far during a voting period.")
RPC_query.empty Alpha_context.Vote.ballots_encoding
(RPC_path.op_div path "ballots").
Definition ballot_list
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
(list (Signature.public_key_hash × Alpha_context.Vote.ballot)) :=
RPC_service.get_service
(Some "Ballots casted so far during a voting period.") RPC_query.empty
(Data_encoding.list_value None
(Data_encoding.obj2
(Data_encoding.req None None "pkh"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "ballot"
Alpha_context.Vote.ballot_encoding)))
(RPC_path.op_div path "ballot_list").
Definition current_period
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
Alpha_context.Voting_period.info :=
RPC_service.get_service
(Some
"Returns the voting period (index, kind, starting position) and related information (position, remaining) of the interrogated block.")
RPC_query.empty Alpha_context.Voting_period.info_encoding
(RPC_path.op_div path "current_period").
Definition successor_period
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
Alpha_context.Voting_period.info :=
RPC_service.get_service
(Some
"Returns the voting period (index, kind, starting position) and related information (position, remaining) of the next block.Useful to craft operations that will be valid in the next block.")
RPC_query.empty Alpha_context.Voting_period.info_encoding
(RPC_path.op_div path "successor_period").
Definition current_quorum
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
int32 :=
RPC_service.get_service (Some "Current expected quorum.") RPC_query.empty
Data_encoding.int32_value (RPC_path.op_div path "current_quorum").
Definition listings
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
(list (Alpha_context.public_key_hash × int64)) :=
RPC_service.get_service (Some "List of delegates with their voting power.")
RPC_query.empty Alpha_context.Vote.listings_encoding
(RPC_path.op_div path "listings").
Definition proposals
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
(Protocol_hash.Map.(S.INDEXES_MAP.t) int64) :=
RPC_service.get_service
(Some "List of proposals with number of supporters.") RPC_query.empty
(Protocol_hash.Map.(S.INDEXES_MAP.encoding) Data_encoding.int64_value)
(RPC_path.op_div path "proposals").
Definition current_proposal
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
(option Protocol_hash.t) :=
RPC_service.get_service (Some "Current proposal under evaluation.")
RPC_query.empty (Data_encoding.option_value Protocol_hash.encoding)
(RPC_path.op_div path "current_proposal").
Definition total_voting_power
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
int64 :=
RPC_service.get_service (Some "Total voting power in the voting listings.")
RPC_query.empty Data_encoding.int64_value
(RPC_path.op_div path "total_voting_power").
End S.
Definition register (function_parameter : unit) : unit :=
let '_ := function_parameter in
let '_ :=
Services_registration.register0 false S.ballots
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_ballots ctxt) in
let '_ :=
Services_registration.register0 true S.ballot_list
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_ballot_list ctxt) in
let '_ :=
Services_registration.register0 false S.current_period
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Voting_period.get_rpc_current_info ctxt) in
let '_ :=
Services_registration.register0 false S.successor_period
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Voting_period.get_rpc_succ_info ctxt) in
let '_ :=
Services_registration.register0 false S.current_quorum
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_current_quorum ctxt) in
let '_ :=
Services_registration.register0 true S.proposals
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_proposals ctxt) in
let '_ :=
Services_registration.register0 true S.listings
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_listings ctxt) in
let '_ :=
Services_registration.register0 false S.current_proposal
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.find_current_proposal ctxt) in
Services_registration.register0 false S.total_voting_power
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_total_voting_power_free ctxt).
Definition ballots {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult Alpha_context.Vote.ballots :=
RPC_context.make_call0 S.ballots ctxt block tt tt.
Definition ballot_list {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult
(list (Signature.public_key_hash × Alpha_context.Vote.ballot)) :=
RPC_context.make_call0 S.ballot_list ctxt block tt tt.
Definition current_period {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult Alpha_context.Voting_period.info :=
RPC_context.make_call0 S.current_period ctxt block tt tt.
Definition successor_period {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult Alpha_context.Voting_period.info :=
RPC_context.make_call0 S.successor_period ctxt block tt tt.
Definition current_quorum {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult int32 :=
RPC_context.make_call0 S.current_quorum ctxt block tt tt.
Definition listings {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult (list (Alpha_context.public_key_hash × int64)) :=
RPC_context.make_call0 S.listings ctxt block tt tt.
Definition proposals {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult (Protocol_hash.Map.(S.INDEXES_MAP.t) int64) :=
RPC_context.make_call0 S.proposals ctxt block tt tt.
Definition current_proposal {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult (option Protocol_hash.t) :=
RPC_context.make_call0 S.current_proposal ctxt block tt tt.
Definition total_voting_power {A : Set}
(ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult int64 :=
RPC_context.make_call0 S.total_voting_power ctxt block tt tt.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Module S.
Definition path : RPC_path.path Updater.rpc_context Updater.rpc_context :=
RPC_path.op_div RPC_path.open_root "votes".
Definition ballots
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
Alpha_context.Vote.ballots :=
RPC_service.get_service
(Some "Sum of ballots casted so far during a voting period.")
RPC_query.empty Alpha_context.Vote.ballots_encoding
(RPC_path.op_div path "ballots").
Definition ballot_list
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
(list (Signature.public_key_hash × Alpha_context.Vote.ballot)) :=
RPC_service.get_service
(Some "Ballots casted so far during a voting period.") RPC_query.empty
(Data_encoding.list_value None
(Data_encoding.obj2
(Data_encoding.req None None "pkh"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "ballot"
Alpha_context.Vote.ballot_encoding)))
(RPC_path.op_div path "ballot_list").
Definition current_period
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
Alpha_context.Voting_period.info :=
RPC_service.get_service
(Some
"Returns the voting period (index, kind, starting position) and related information (position, remaining) of the interrogated block.")
RPC_query.empty Alpha_context.Voting_period.info_encoding
(RPC_path.op_div path "current_period").
Definition successor_period
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
Alpha_context.Voting_period.info :=
RPC_service.get_service
(Some
"Returns the voting period (index, kind, starting position) and related information (position, remaining) of the next block.Useful to craft operations that will be valid in the next block.")
RPC_query.empty Alpha_context.Voting_period.info_encoding
(RPC_path.op_div path "successor_period").
Definition current_quorum
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
int32 :=
RPC_service.get_service (Some "Current expected quorum.") RPC_query.empty
Data_encoding.int32_value (RPC_path.op_div path "current_quorum").
Definition listings
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
(list (Alpha_context.public_key_hash × int64)) :=
RPC_service.get_service (Some "List of delegates with their voting power.")
RPC_query.empty Alpha_context.Vote.listings_encoding
(RPC_path.op_div path "listings").
Definition proposals
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
(Protocol_hash.Map.(S.INDEXES_MAP.t) int64) :=
RPC_service.get_service
(Some "List of proposals with number of supporters.") RPC_query.empty
(Protocol_hash.Map.(S.INDEXES_MAP.encoding) Data_encoding.int64_value)
(RPC_path.op_div path "proposals").
Definition current_proposal
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
(option Protocol_hash.t) :=
RPC_service.get_service (Some "Current proposal under evaluation.")
RPC_query.empty (Data_encoding.option_value Protocol_hash.encoding)
(RPC_path.op_div path "current_proposal").
Definition total_voting_power
: RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
int64 :=
RPC_service.get_service (Some "Total voting power in the voting listings.")
RPC_query.empty Data_encoding.int64_value
(RPC_path.op_div path "total_voting_power").
End S.
Definition register (function_parameter : unit) : unit :=
let '_ := function_parameter in
let '_ :=
Services_registration.register0 false S.ballots
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_ballots ctxt) in
let '_ :=
Services_registration.register0 true S.ballot_list
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_ballot_list ctxt) in
let '_ :=
Services_registration.register0 false S.current_period
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Voting_period.get_rpc_current_info ctxt) in
let '_ :=
Services_registration.register0 false S.successor_period
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Voting_period.get_rpc_succ_info ctxt) in
let '_ :=
Services_registration.register0 false S.current_quorum
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_current_quorum ctxt) in
let '_ :=
Services_registration.register0 true S.proposals
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_proposals ctxt) in
let '_ :=
Services_registration.register0 true S.listings
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_listings ctxt) in
let '_ :=
Services_registration.register0 false S.current_proposal
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.find_current_proposal ctxt) in
Services_registration.register0 false S.total_voting_power
(fun (ctxt : Alpha_context.t) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Alpha_context.Vote.get_total_voting_power_free ctxt).
Definition ballots {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult Alpha_context.Vote.ballots :=
RPC_context.make_call0 S.ballots ctxt block tt tt.
Definition ballot_list {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult
(list (Signature.public_key_hash × Alpha_context.Vote.ballot)) :=
RPC_context.make_call0 S.ballot_list ctxt block tt tt.
Definition current_period {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult Alpha_context.Voting_period.info :=
RPC_context.make_call0 S.current_period ctxt block tt tt.
Definition successor_period {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult Alpha_context.Voting_period.info :=
RPC_context.make_call0 S.successor_period ctxt block tt tt.
Definition current_quorum {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult int32 :=
RPC_context.make_call0 S.current_quorum ctxt block tt tt.
Definition listings {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult (list (Alpha_context.public_key_hash × int64)) :=
RPC_context.make_call0 S.listings ctxt block tt tt.
Definition proposals {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult (Protocol_hash.Map.(S.INDEXES_MAP.t) int64) :=
RPC_context.make_call0 S.proposals ctxt block tt tt.
Definition current_proposal {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult (option Protocol_hash.t) :=
RPC_context.make_call0 S.current_proposal ctxt block tt tt.
Definition total_voting_power {A : Set}
(ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult int64 :=
RPC_context.make_call0 S.total_voting_power ctxt block tt tt.