✒️ Contract_services.v
Translated 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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Sapling_services.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Definition custom_root : RPC_path.context RPC_context.t :=
RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "contracts".
Definition big_map_root : RPC_path.context RPC_context.t :=
RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "big_maps".
Module info.
Record record : Set := Build {
balance : Alpha_context.Tez.t;
delegate : option Alpha_context.public_key_hash;
counter : option Alpha_context.counter;
script : option Alpha_context.Script.t;
}.
Definition with_balance balance (r : record) :=
Build balance r.(delegate) r.(counter) r.(script).
Definition with_delegate delegate (r : record) :=
Build r.(balance) delegate r.(counter) r.(script).
Definition with_counter counter (r : record) :=
Build r.(balance) r.(delegate) counter r.(script).
Definition with_script script (r : record) :=
Build r.(balance) r.(delegate) r.(counter) script.
End info.
Definition info := info.record.
Definition info_encoding : Data_encoding.encoding info :=
(let arg :=
Data_encoding.conv
(fun (function_parameter : info) ⇒
let '{|
info.balance := balance;
info.delegate := delegate;
info.counter := counter;
info.script := script
|} := function_parameter in
(balance, delegate, script, counter))
(fun (function_parameter :
Alpha_context.Tez.t × option Alpha_context.public_key_hash ×
option Alpha_context.Script.t × option Alpha_context.counter) ⇒
let '(balance, delegate, script, counter) := function_parameter in
{| info.balance := balance; info.delegate := delegate;
info.counter := counter; info.script := script; |}) in
fun (eta :
Data_encoding.encoding
(Alpha_context.Tez.t × option Alpha_context.public_key_hash ×
option Alpha_context.Script.t × option Alpha_context.counter)) ⇒
arg None eta)
(Data_encoding.obj4
(Data_encoding.req None None "balance" Alpha_context.Tez.encoding)
(Data_encoding.opt None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.opt None None "script" Alpha_context.Script.encoding)
(Data_encoding.opt None None "counter" Data_encoding.n_value)).
Module S.
Definition balance
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Tez.t :=
RPC_service.get_service
(Some
"Access the spendable balance of a contract, excluding frozen bonds.")
RPC_query.empty Alpha_context.Tez.encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"balance").
Definition frozen_bonds
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Tez.t :=
RPC_service.get_service (Some "Access the frozen bonds of a contract.")
RPC_query.empty Alpha_context.Tez.encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"frozen_bonds").
Definition balance_and_frozen_bonds
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Tez.t :=
RPC_service.get_service
(Some
"Access the sum of the spendable balance and frozen bonds of a contract. This sum is part of the contract's stake, and it is exactly the contract's stake if the contract is not a delegate.")
RPC_query.empty Alpha_context.Tez.encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"balance_and_frozen_bonds").
Definition manager_key
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
(option Signature.public_key) :=
RPC_service.get_service (Some "Access the manager of a contract.")
RPC_query.empty
(Data_encoding.option_value
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"manager_key").
Definition delegate
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Signature.public_key_hash :=
RPC_service.get_service (Some "Access the delegate of a contract, if any.")
RPC_query.empty
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"delegate").
Definition counter
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit Z.t :=
RPC_service.get_service (Some "Access the counter of a contract, if any.")
RPC_query.empty Data_encoding.z_value
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"counter").
Definition script
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Script.t :=
RPC_service.get_service (Some "Access the code and data of the contract.")
RPC_query.empty Alpha_context.Script.encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"script").
Definition storage_value
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Script.expr :=
RPC_service.get_service (Some "Access the data of the contract.")
RPC_query.empty Alpha_context.Script.expr_encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"storage").
Module normalize_types_query.
Record record : Set := Build {
normalize_types : bool;
}.
Definition with_normalize_types normalize_types (r : record) :=
Build normalize_types.
End normalize_types_query.
Definition normalize_types_query := normalize_types_query.record.
Definition normalize_types_query_value : RPC_query.t normalize_types_query :=
RPC_query.seal
(RPC_query.op_pipeplus
(RPC_query.query_value
(fun (normalize_types : bool) ⇒
{| normalize_types_query.normalize_types := normalize_types; |}))
(RPC_query.flag
(Some
"Whether types should be normalized (annotations removed, combs flattened) or kept as they appeared in the original script.")
"normalize_types"
(fun (t_value : normalize_types_query) ⇒
t_value.(normalize_types_query.normalize_types)))).
Definition entrypoint_type
: RPC_service.service RPC_context.t
((RPC_context.t × Alpha_context.Contract.contract) ×
Alpha_context.Entrypoint.t) normalize_types_query unit
Alpha_context.Script.expr :=
RPC_service.get_service
(Some "Return the type of the given entrypoint of the contract")
normalize_types_query_value Alpha_context.Script.expr_encoding
(RPC_path.op_divcolon
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"entrypoints") Alpha_context.Entrypoint.rpc_arg).
Definition list_entrypoints
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) normalize_types_query
unit
(list (list Michelson_v1_primitives.prim) ×
list (string × Alpha_context.Script.expr)) :=
RPC_service.get_service
(Some "Return the list of entrypoints of the contract")
normalize_types_query_value
(Data_encoding.obj2
(Data_encoding.dft None None "unreachable"
(Data_encoding.list_value None
(Data_encoding.obj1
(Data_encoding.req None None "path"
(Data_encoding.list_value None
Michelson_v1_primitives.prim_encoding)))) nil)
(Data_encoding.req None None "entrypoints"
(Data_encoding.assoc Alpha_context.Script.expr_encoding)))
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"entrypoints").
Definition contract_big_map_get_opt
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit
(Alpha_context.Script.expr × Alpha_context.Script.expr)
(option Alpha_context.Script.expr) :=
RPC_service.post_service
(Some
"Access the value associated with a key in a big map of the contract (deprecated).")
RPC_query.empty
(Data_encoding.obj2
(Data_encoding.req None None "key" Alpha_context.Script.expr_encoding)
(Data_encoding.req None None "type" Alpha_context.Script.expr_encoding))
(Data_encoding.option_value Alpha_context.Script.expr_encoding)
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"big_map_get").
Definition big_map_get
: RPC_service.service RPC_context.t
((RPC_context.t × Alpha_context.Big_map.Id.t) × Script_expr_hash.t) unit
unit Alpha_context.Script.expr :=
RPC_service.get_service
(Some "Access the value associated with a key in a big map.")
RPC_query.empty Alpha_context.Script.expr_encoding
(RPC_path.op_divcolon
(RPC_path.op_divcolon big_map_root Alpha_context.Big_map.Id.rpc_arg)
Script_expr_hash.rpc_arg).
Module big_map_get_all_query.
Record record : Set := Build {
offset : option int;
length : option int;
}.
Definition with_offset offset (r : record) :=
Build offset r.(length).
Definition with_length length (r : record) :=
Build r.(offset) length.
End big_map_get_all_query.
Definition big_map_get_all_query := big_map_get_all_query.record.
Definition rpc_arg_uint : RPC_arg.t int :=
let int_of_string (s_value : string) : Pervasives.result int string :=
let? i_value :=
Option.to_result
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot parse integer value "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Cannot parse integer value %s") s_value)
(Pervasives.int_of_string_opt s_value) in
if i_value <i 0 then
Pervasives.Error
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Negative integer: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))
"Negative integer: %d") i_value)
else
Pervasives.Ok i_value in
RPC_arg.make (Some "A non-negative integer (greater than or equal to 0).")
"uint" int_of_string Pervasives.string_of_int tt.
Definition big_map_get_all_query_value : RPC_query.t big_map_get_all_query :=
RPC_query.seal
(RPC_query.op_pipeplus
(RPC_query.op_pipeplus
(RPC_query.query_value
(fun (offset : option int) ⇒
fun (length : option int) ⇒
{| big_map_get_all_query.offset := offset;
big_map_get_all_query.length := length; |}))
(RPC_query.opt_field
(Some
"Skip the first [offset] values. Useful in combination with [length] for pagination.")
"offset" rpc_arg_uint
(fun (t_value : big_map_get_all_query) ⇒
t_value.(big_map_get_all_query.offset))))
(RPC_query.opt_field
(Some
"Only retrieve [length] values. Useful in combination with [offset] for pagination.")
"length" rpc_arg_uint
(fun (t_value : big_map_get_all_query) ⇒
t_value.(big_map_get_all_query.length)))).
Definition big_map_get_all
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Big_map.Id.t) big_map_get_all_query unit
(list Alpha_context.Script.expr) :=
RPC_service.get_service
(Some
"Get the (optionally paginated) list of values in a big map. Order of values is unspecified, but is guaranteed to be consistent.")
big_map_get_all_query_value
(Data_encoding.list_value None Alpha_context.Script.expr_encoding)
(RPC_path.op_divcolon big_map_root Alpha_context.Big_map.Id.rpc_arg).
Definition info_value
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) normalize_types_query
unit info :=
RPC_service.get_service (Some "Access the complete status of a contract.")
normalize_types_query_value info_encoding
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg).
Definition list_value
: RPC_service.service RPC_context.t RPC_context.t unit unit
(list Alpha_context.Contract.t) :=
RPC_service.get_service
(Some "All existing contracts (including non-empty default contracts).")
RPC_query.empty
(Data_encoding.list_value None Alpha_context.Contract.encoding)
custom_root.
Module Sapling.
Definition single_sapling_get_id
(ctxt : Alpha_context.context)
(contract_id : Alpha_context.Contract.contract)
: M? (option Alpha_context.Sapling.Id.t × Alpha_context.context) :=
let? '(ctxt, script) := Alpha_context.Contract.get_script ctxt contract_id
in
match script with
| None ⇒ return? (None, ctxt)
| Some script ⇒
let ctxt := Alpha_context.Gas.set_unlimited ctxt in
let tzresult :=
Script_ir_translator.parse_script None ctxt true true script in
let?
'(Script_ir_translator.Ex_script (Script_typed_ir.Script script), ctxt) :=
tzresult in
Script_ir_translator.get_single_sapling_state ctxt
script.(Script_typed_ir.script.Script.storage_type)
script.(Script_typed_ir.script.Script.storage)
end.
Definition make_service {A B : Set}
(function_parameter : Sapling_services.S.Args.t A B)
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) A unit B ×
(Alpha_context.context → Alpha_context.Contract.contract → A →
unit → M? (option B)) :=
let '{|
Sapling_services.S.Args.t.name := name;
Sapling_services.S.Args.t.description := description;
Sapling_services.S.Args.t.query := query_value;
Sapling_services.S.Args.t.output := output;
Sapling_services.S.Args.t.f := f_value
|} := function_parameter in
let name := Pervasives.op_caret "single_sapling_" name in
let path :=
RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg) name
in
let service :=
RPC_service.get_service (Some description) query_value output path in
(service,
(fun (ctxt : Alpha_context.context) ⇒
fun (contract_id : Alpha_context.Contract.contract) ⇒
fun (q_value : A) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
let? '(sapling_id, ctxt) :=
single_sapling_get_id ctxt contract_id in
Option.map_es
(fun (sapling_id : Alpha_context.Sapling.Id.t) ⇒
f_value ctxt sapling_id q_value) sapling_id)).
Definition get_diff
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract)
Sapling_services.diff_query unit
(Alpha_context.Sapling.root × Alpha_context.Sapling.diff) ×
(Alpha_context.context → Alpha_context.Contract.contract →
Sapling_services.diff_query → unit →
M? (option (Alpha_context.Sapling.root × Alpha_context.Sapling.diff))) :=
make_service Sapling_services.S.Args.get_diff.
Definition register (function_parameter : unit) : unit :=
let '_ := function_parameter in
let reg {A B C D : Set}
(chunked : bool)
(function_parameter :
RPC_service.t Updater.rpc_context (Updater.rpc_context × A) B C D ×
(Alpha_context.t → A → B → C → M? (option D))) : unit :=
let '(service, f_value) := function_parameter in
Services_registration.opt_register1 chunked service f_value in
reg false get_diff.
Definition mk_call1 {A B C D E : Set}
(function_parameter :
RPC_service.t RPC_context.t (RPC_context.t × A) B unit C × D)
: RPC_context.simple E → E → A → B → Error_monad.shell_tzresult C :=
let '(service, _f) := function_parameter in
fun (ctxt : RPC_context.simple E) ⇒
fun (block : E) ⇒
fun (id : A) ⇒
fun (q_value : B) ⇒
RPC_context.make_call1 service ctxt block id q_value tt.
End Sapling.
End S.
Axiom register : unit → unit.
Definition list_value {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult (list Alpha_context.Contract.t) :=
RPC_context.make_call0 S.list_value ctxt block tt tt.
Definition info_value {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract) (normalize_types : bool)
: Error_monad.shell_tzresult info :=
RPC_context.make_call1 S.info_value ctxt block contract
{| S.normalize_types_query.normalize_types := normalize_types; |} tt.
Definition balance {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Tez.t :=
RPC_context.make_call1 S.balance ctxt block contract tt tt.
Definition frozen_bonds {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Tez.t :=
RPC_context.make_call1 S.frozen_bonds ctxt block contract tt tt.
Definition balance_and_frozen_bonds {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Tez.t :=
RPC_context.make_call1 S.balance_and_frozen_bonds ctxt block contract tt tt.
Definition manager_key {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(mgr : Alpha_context.public_key_hash)
: Error_monad.shell_tzresult (option Signature.public_key) :=
RPC_context.make_call1 S.manager_key ctxt block
(Alpha_context.Contract.implicit_contract mgr) tt tt.
Definition delegate {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Signature.public_key_hash :=
RPC_context.make_call1 S.delegate ctxt block contract tt tt.
Definition delegate_opt {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult (option Signature.public_key_hash) :=
RPC_context.make_opt_call1 S.delegate ctxt block contract tt tt.
Definition counter {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(mgr : Alpha_context.public_key_hash) : Error_monad.shell_tzresult Z.t :=
RPC_context.make_call1 S.counter ctxt block
(Alpha_context.Contract.implicit_contract mgr) tt tt.
Definition script {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Script.t :=
RPC_context.make_call1 S.script ctxt block contract tt tt.
Definition script_opt {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult (option Alpha_context.Script.t) :=
RPC_context.make_opt_call1 S.script ctxt block contract tt tt.
Definition storage_value {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Script.expr :=
RPC_context.make_call1 S.storage_value ctxt block contract tt tt.
Definition entrypoint_type {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
(entrypoint : Alpha_context.Entrypoint.t) (normalize_types : bool)
: Error_monad.shell_tzresult Alpha_context.Script.expr :=
RPC_context.make_call2 S.entrypoint_type ctxt block contract entrypoint
{| S.normalize_types_query.normalize_types := normalize_types; |} tt.
Definition list_entrypoints {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract) (normalize_types : bool)
: Error_monad.shell_tzresult
(list (list Michelson_v1_primitives.prim) ×
list (string × Alpha_context.Script.expr)) :=
RPC_context.make_call1 S.list_entrypoints ctxt block contract
{| S.normalize_types_query.normalize_types := normalize_types; |} tt.
Definition storage_opt {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult (option Alpha_context.Script.expr) :=
RPC_context.make_opt_call1 S.storage_value ctxt block contract tt tt.
Definition big_map_get {A : Set}
(ctxt : RPC_context.simple A) (block : A) (id : Alpha_context.Big_map.Id.t)
(key_value : Script_expr_hash.t)
: Error_monad.shell_tzresult Alpha_context.Script.expr :=
RPC_context.make_call2 S.big_map_get ctxt block id key_value tt tt.
Definition contract_big_map_get_opt {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
(key_value : Alpha_context.Script.expr × Alpha_context.Script.expr)
: Error_monad.shell_tzresult (option Alpha_context.Script.expr) :=
RPC_context.make_call1 S.contract_big_map_get_opt ctxt block contract tt
key_value.
Definition single_sapling_get_diff {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(id : Alpha_context.Contract.contract) (offset_commitment : option Int64.t)
(offset_nullifier : option Int64.t) (function_parameter : unit)
: Error_monad.shell_tzresult
(Alpha_context.Sapling.root × Alpha_context.Sapling.diff) :=
let '_ := function_parameter in
S.Sapling.mk_call1 S.Sapling.get_diff ctxt block id
{| Sapling_services.diff_query.offset_commitment := offset_commitment;
Sapling_services.diff_query.offset_nullifier := offset_nullifier; |}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Sapling_services.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Definition custom_root : RPC_path.context RPC_context.t :=
RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "contracts".
Definition big_map_root : RPC_path.context RPC_context.t :=
RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "big_maps".
Module info.
Record record : Set := Build {
balance : Alpha_context.Tez.t;
delegate : option Alpha_context.public_key_hash;
counter : option Alpha_context.counter;
script : option Alpha_context.Script.t;
}.
Definition with_balance balance (r : record) :=
Build balance r.(delegate) r.(counter) r.(script).
Definition with_delegate delegate (r : record) :=
Build r.(balance) delegate r.(counter) r.(script).
Definition with_counter counter (r : record) :=
Build r.(balance) r.(delegate) counter r.(script).
Definition with_script script (r : record) :=
Build r.(balance) r.(delegate) r.(counter) script.
End info.
Definition info := info.record.
Definition info_encoding : Data_encoding.encoding info :=
(let arg :=
Data_encoding.conv
(fun (function_parameter : info) ⇒
let '{|
info.balance := balance;
info.delegate := delegate;
info.counter := counter;
info.script := script
|} := function_parameter in
(balance, delegate, script, counter))
(fun (function_parameter :
Alpha_context.Tez.t × option Alpha_context.public_key_hash ×
option Alpha_context.Script.t × option Alpha_context.counter) ⇒
let '(balance, delegate, script, counter) := function_parameter in
{| info.balance := balance; info.delegate := delegate;
info.counter := counter; info.script := script; |}) in
fun (eta :
Data_encoding.encoding
(Alpha_context.Tez.t × option Alpha_context.public_key_hash ×
option Alpha_context.Script.t × option Alpha_context.counter)) ⇒
arg None eta)
(Data_encoding.obj4
(Data_encoding.req None None "balance" Alpha_context.Tez.encoding)
(Data_encoding.opt None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.opt None None "script" Alpha_context.Script.encoding)
(Data_encoding.opt None None "counter" Data_encoding.n_value)).
Module S.
Definition balance
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Tez.t :=
RPC_service.get_service
(Some
"Access the spendable balance of a contract, excluding frozen bonds.")
RPC_query.empty Alpha_context.Tez.encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"balance").
Definition frozen_bonds
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Tez.t :=
RPC_service.get_service (Some "Access the frozen bonds of a contract.")
RPC_query.empty Alpha_context.Tez.encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"frozen_bonds").
Definition balance_and_frozen_bonds
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Tez.t :=
RPC_service.get_service
(Some
"Access the sum of the spendable balance and frozen bonds of a contract. This sum is part of the contract's stake, and it is exactly the contract's stake if the contract is not a delegate.")
RPC_query.empty Alpha_context.Tez.encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"balance_and_frozen_bonds").
Definition manager_key
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
(option Signature.public_key) :=
RPC_service.get_service (Some "Access the manager of a contract.")
RPC_query.empty
(Data_encoding.option_value
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"manager_key").
Definition delegate
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Signature.public_key_hash :=
RPC_service.get_service (Some "Access the delegate of a contract, if any.")
RPC_query.empty
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"delegate").
Definition counter
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit Z.t :=
RPC_service.get_service (Some "Access the counter of a contract, if any.")
RPC_query.empty Data_encoding.z_value
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"counter").
Definition script
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Script.t :=
RPC_service.get_service (Some "Access the code and data of the contract.")
RPC_query.empty Alpha_context.Script.encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"script").
Definition storage_value
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit unit
Alpha_context.Script.expr :=
RPC_service.get_service (Some "Access the data of the contract.")
RPC_query.empty Alpha_context.Script.expr_encoding
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"storage").
Module normalize_types_query.
Record record : Set := Build {
normalize_types : bool;
}.
Definition with_normalize_types normalize_types (r : record) :=
Build normalize_types.
End normalize_types_query.
Definition normalize_types_query := normalize_types_query.record.
Definition normalize_types_query_value : RPC_query.t normalize_types_query :=
RPC_query.seal
(RPC_query.op_pipeplus
(RPC_query.query_value
(fun (normalize_types : bool) ⇒
{| normalize_types_query.normalize_types := normalize_types; |}))
(RPC_query.flag
(Some
"Whether types should be normalized (annotations removed, combs flattened) or kept as they appeared in the original script.")
"normalize_types"
(fun (t_value : normalize_types_query) ⇒
t_value.(normalize_types_query.normalize_types)))).
Definition entrypoint_type
: RPC_service.service RPC_context.t
((RPC_context.t × Alpha_context.Contract.contract) ×
Alpha_context.Entrypoint.t) normalize_types_query unit
Alpha_context.Script.expr :=
RPC_service.get_service
(Some "Return the type of the given entrypoint of the contract")
normalize_types_query_value Alpha_context.Script.expr_encoding
(RPC_path.op_divcolon
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"entrypoints") Alpha_context.Entrypoint.rpc_arg).
Definition list_entrypoints
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) normalize_types_query
unit
(list (list Michelson_v1_primitives.prim) ×
list (string × Alpha_context.Script.expr)) :=
RPC_service.get_service
(Some "Return the list of entrypoints of the contract")
normalize_types_query_value
(Data_encoding.obj2
(Data_encoding.dft None None "unreachable"
(Data_encoding.list_value None
(Data_encoding.obj1
(Data_encoding.req None None "path"
(Data_encoding.list_value None
Michelson_v1_primitives.prim_encoding)))) nil)
(Data_encoding.req None None "entrypoints"
(Data_encoding.assoc Alpha_context.Script.expr_encoding)))
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"entrypoints").
Definition contract_big_map_get_opt
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) unit
(Alpha_context.Script.expr × Alpha_context.Script.expr)
(option Alpha_context.Script.expr) :=
RPC_service.post_service
(Some
"Access the value associated with a key in a big map of the contract (deprecated).")
RPC_query.empty
(Data_encoding.obj2
(Data_encoding.req None None "key" Alpha_context.Script.expr_encoding)
(Data_encoding.req None None "type" Alpha_context.Script.expr_encoding))
(Data_encoding.option_value Alpha_context.Script.expr_encoding)
(RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg)
"big_map_get").
Definition big_map_get
: RPC_service.service RPC_context.t
((RPC_context.t × Alpha_context.Big_map.Id.t) × Script_expr_hash.t) unit
unit Alpha_context.Script.expr :=
RPC_service.get_service
(Some "Access the value associated with a key in a big map.")
RPC_query.empty Alpha_context.Script.expr_encoding
(RPC_path.op_divcolon
(RPC_path.op_divcolon big_map_root Alpha_context.Big_map.Id.rpc_arg)
Script_expr_hash.rpc_arg).
Module big_map_get_all_query.
Record record : Set := Build {
offset : option int;
length : option int;
}.
Definition with_offset offset (r : record) :=
Build offset r.(length).
Definition with_length length (r : record) :=
Build r.(offset) length.
End big_map_get_all_query.
Definition big_map_get_all_query := big_map_get_all_query.record.
Definition rpc_arg_uint : RPC_arg.t int :=
let int_of_string (s_value : string) : Pervasives.result int string :=
let? i_value :=
Option.to_result
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot parse integer value "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Cannot parse integer value %s") s_value)
(Pervasives.int_of_string_opt s_value) in
if i_value <i 0 then
Pervasives.Error
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Negative integer: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))
"Negative integer: %d") i_value)
else
Pervasives.Ok i_value in
RPC_arg.make (Some "A non-negative integer (greater than or equal to 0).")
"uint" int_of_string Pervasives.string_of_int tt.
Definition big_map_get_all_query_value : RPC_query.t big_map_get_all_query :=
RPC_query.seal
(RPC_query.op_pipeplus
(RPC_query.op_pipeplus
(RPC_query.query_value
(fun (offset : option int) ⇒
fun (length : option int) ⇒
{| big_map_get_all_query.offset := offset;
big_map_get_all_query.length := length; |}))
(RPC_query.opt_field
(Some
"Skip the first [offset] values. Useful in combination with [length] for pagination.")
"offset" rpc_arg_uint
(fun (t_value : big_map_get_all_query) ⇒
t_value.(big_map_get_all_query.offset))))
(RPC_query.opt_field
(Some
"Only retrieve [length] values. Useful in combination with [offset] for pagination.")
"length" rpc_arg_uint
(fun (t_value : big_map_get_all_query) ⇒
t_value.(big_map_get_all_query.length)))).
Definition big_map_get_all
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Big_map.Id.t) big_map_get_all_query unit
(list Alpha_context.Script.expr) :=
RPC_service.get_service
(Some
"Get the (optionally paginated) list of values in a big map. Order of values is unspecified, but is guaranteed to be consistent.")
big_map_get_all_query_value
(Data_encoding.list_value None Alpha_context.Script.expr_encoding)
(RPC_path.op_divcolon big_map_root Alpha_context.Big_map.Id.rpc_arg).
Definition info_value
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) normalize_types_query
unit info :=
RPC_service.get_service (Some "Access the complete status of a contract.")
normalize_types_query_value info_encoding
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg).
Definition list_value
: RPC_service.service RPC_context.t RPC_context.t unit unit
(list Alpha_context.Contract.t) :=
RPC_service.get_service
(Some "All existing contracts (including non-empty default contracts).")
RPC_query.empty
(Data_encoding.list_value None Alpha_context.Contract.encoding)
custom_root.
Module Sapling.
Definition single_sapling_get_id
(ctxt : Alpha_context.context)
(contract_id : Alpha_context.Contract.contract)
: M? (option Alpha_context.Sapling.Id.t × Alpha_context.context) :=
let? '(ctxt, script) := Alpha_context.Contract.get_script ctxt contract_id
in
match script with
| None ⇒ return? (None, ctxt)
| Some script ⇒
let ctxt := Alpha_context.Gas.set_unlimited ctxt in
let tzresult :=
Script_ir_translator.parse_script None ctxt true true script in
let?
'(Script_ir_translator.Ex_script (Script_typed_ir.Script script), ctxt) :=
tzresult in
Script_ir_translator.get_single_sapling_state ctxt
script.(Script_typed_ir.script.Script.storage_type)
script.(Script_typed_ir.script.Script.storage)
end.
Definition make_service {A B : Set}
(function_parameter : Sapling_services.S.Args.t A B)
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract) A unit B ×
(Alpha_context.context → Alpha_context.Contract.contract → A →
unit → M? (option B)) :=
let '{|
Sapling_services.S.Args.t.name := name;
Sapling_services.S.Args.t.description := description;
Sapling_services.S.Args.t.query := query_value;
Sapling_services.S.Args.t.output := output;
Sapling_services.S.Args.t.f := f_value
|} := function_parameter in
let name := Pervasives.op_caret "single_sapling_" name in
let path :=
RPC_path.op_div
(RPC_path.op_divcolon custom_root Alpha_context.Contract.rpc_arg) name
in
let service :=
RPC_service.get_service (Some description) query_value output path in
(service,
(fun (ctxt : Alpha_context.context) ⇒
fun (contract_id : Alpha_context.Contract.contract) ⇒
fun (q_value : A) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
let? '(sapling_id, ctxt) :=
single_sapling_get_id ctxt contract_id in
Option.map_es
(fun (sapling_id : Alpha_context.Sapling.Id.t) ⇒
f_value ctxt sapling_id q_value) sapling_id)).
Definition get_diff
: RPC_service.service RPC_context.t
(RPC_context.t × Alpha_context.Contract.contract)
Sapling_services.diff_query unit
(Alpha_context.Sapling.root × Alpha_context.Sapling.diff) ×
(Alpha_context.context → Alpha_context.Contract.contract →
Sapling_services.diff_query → unit →
M? (option (Alpha_context.Sapling.root × Alpha_context.Sapling.diff))) :=
make_service Sapling_services.S.Args.get_diff.
Definition register (function_parameter : unit) : unit :=
let '_ := function_parameter in
let reg {A B C D : Set}
(chunked : bool)
(function_parameter :
RPC_service.t Updater.rpc_context (Updater.rpc_context × A) B C D ×
(Alpha_context.t → A → B → C → M? (option D))) : unit :=
let '(service, f_value) := function_parameter in
Services_registration.opt_register1 chunked service f_value in
reg false get_diff.
Definition mk_call1 {A B C D E : Set}
(function_parameter :
RPC_service.t RPC_context.t (RPC_context.t × A) B unit C × D)
: RPC_context.simple E → E → A → B → Error_monad.shell_tzresult C :=
let '(service, _f) := function_parameter in
fun (ctxt : RPC_context.simple E) ⇒
fun (block : E) ⇒
fun (id : A) ⇒
fun (q_value : B) ⇒
RPC_context.make_call1 service ctxt block id q_value tt.
End Sapling.
End S.
Axiom register : unit → unit.
Definition list_value {A : Set} (ctxt : RPC_context.simple A) (block : A)
: Error_monad.shell_tzresult (list Alpha_context.Contract.t) :=
RPC_context.make_call0 S.list_value ctxt block tt tt.
Definition info_value {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract) (normalize_types : bool)
: Error_monad.shell_tzresult info :=
RPC_context.make_call1 S.info_value ctxt block contract
{| S.normalize_types_query.normalize_types := normalize_types; |} tt.
Definition balance {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Tez.t :=
RPC_context.make_call1 S.balance ctxt block contract tt tt.
Definition frozen_bonds {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Tez.t :=
RPC_context.make_call1 S.frozen_bonds ctxt block contract tt tt.
Definition balance_and_frozen_bonds {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Tez.t :=
RPC_context.make_call1 S.balance_and_frozen_bonds ctxt block contract tt tt.
Definition manager_key {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(mgr : Alpha_context.public_key_hash)
: Error_monad.shell_tzresult (option Signature.public_key) :=
RPC_context.make_call1 S.manager_key ctxt block
(Alpha_context.Contract.implicit_contract mgr) tt tt.
Definition delegate {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Signature.public_key_hash :=
RPC_context.make_call1 S.delegate ctxt block contract tt tt.
Definition delegate_opt {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult (option Signature.public_key_hash) :=
RPC_context.make_opt_call1 S.delegate ctxt block contract tt tt.
Definition counter {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(mgr : Alpha_context.public_key_hash) : Error_monad.shell_tzresult Z.t :=
RPC_context.make_call1 S.counter ctxt block
(Alpha_context.Contract.implicit_contract mgr) tt tt.
Definition script {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Script.t :=
RPC_context.make_call1 S.script ctxt block contract tt tt.
Definition script_opt {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult (option Alpha_context.Script.t) :=
RPC_context.make_opt_call1 S.script ctxt block contract tt tt.
Definition storage_value {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult Alpha_context.Script.expr :=
RPC_context.make_call1 S.storage_value ctxt block contract tt tt.
Definition entrypoint_type {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
(entrypoint : Alpha_context.Entrypoint.t) (normalize_types : bool)
: Error_monad.shell_tzresult Alpha_context.Script.expr :=
RPC_context.make_call2 S.entrypoint_type ctxt block contract entrypoint
{| S.normalize_types_query.normalize_types := normalize_types; |} tt.
Definition list_entrypoints {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract) (normalize_types : bool)
: Error_monad.shell_tzresult
(list (list Michelson_v1_primitives.prim) ×
list (string × Alpha_context.Script.expr)) :=
RPC_context.make_call1 S.list_entrypoints ctxt block contract
{| S.normalize_types_query.normalize_types := normalize_types; |} tt.
Definition storage_opt {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
: Error_monad.shell_tzresult (option Alpha_context.Script.expr) :=
RPC_context.make_opt_call1 S.storage_value ctxt block contract tt tt.
Definition big_map_get {A : Set}
(ctxt : RPC_context.simple A) (block : A) (id : Alpha_context.Big_map.Id.t)
(key_value : Script_expr_hash.t)
: Error_monad.shell_tzresult Alpha_context.Script.expr :=
RPC_context.make_call2 S.big_map_get ctxt block id key_value tt tt.
Definition contract_big_map_get_opt {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(contract : Alpha_context.Contract.contract)
(key_value : Alpha_context.Script.expr × Alpha_context.Script.expr)
: Error_monad.shell_tzresult (option Alpha_context.Script.expr) :=
RPC_context.make_call1 S.contract_big_map_get_opt ctxt block contract tt
key_value.
Definition single_sapling_get_diff {A : Set}
(ctxt : RPC_context.simple A) (block : A)
(id : Alpha_context.Contract.contract) (offset_commitment : option Int64.t)
(offset_nullifier : option Int64.t) (function_parameter : unit)
: Error_monad.shell_tzresult
(Alpha_context.Sapling.root × Alpha_context.Sapling.diff) :=
let '_ := function_parameter in
S.Sapling.mk_call1 S.Sapling.get_diff ctxt block id
{| Sapling_services.diff_query.offset_commitment := offset_commitment;
Sapling_services.diff_query.offset_nullifier := offset_nullifier; |}.