✒️ Contract_delegate_storage.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.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Definition find
: Raw_context.t → Contract_repr.t → M? (option Signature.public_key_hash) :=
Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.find).
Definition init_value
(ctxt : Raw_context.t) (contract : Contract_repr.t)
(delegate : Signature.public_key_hash) : M? Raw_context.t :=
let? ctxt :=
Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.init_value)
ctxt contract delegate in
let delegate_contract := Contract_repr.Implicit delegate in
Error_monad.op_gtpipeeq
(Storage.Contract.Delegated.(Storage_sigs.Data_set_storage.add)
(ctxt, delegate_contract) contract) Error_monad.ok.
Definition unlink (ctxt : Raw_context.t) (contract : Contract_repr.t)
: M? Raw_context.t :=
let? function_parameter :=
Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.find) ctxt
contract in
match function_parameter with
| None ⇒ return? ctxt
| Some delegate ⇒
let delegate_contract := Contract_repr.Implicit delegate in
Error_monad.op_gtpipeeq
(Storage.Contract.Delegated.(Storage_sigs.Data_set_storage.remove)
(ctxt, delegate_contract) contract) Error_monad.ok
end.
Definition delete (ctxt : Raw_context.t) (contract : Contract_repr.t)
: M? Raw_context.t :=
let? ctxt := unlink ctxt contract in
Error_monad.op_gtpipeeq
(Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.remove) ctxt
contract) Error_monad.ok.
Definition set
(ctxt : Raw_context.t) (contract : Contract_repr.t)
(delegate : Signature.public_key_hash) : M? Raw_context.t :=
let? ctxt := unlink ctxt contract in
let ctxt :=
Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.add) ctxt
contract delegate in
let delegate_contract := Contract_repr.Implicit delegate in
Error_monad.op_gtpipeeq
(Storage.Contract.Delegated.(Storage_sigs.Data_set_storage.add)
(ctxt, delegate_contract) contract) Error_monad.ok.
Definition delegated_contracts
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (list Contract_repr.t) :=
let contract := Contract_repr.Implicit delegate in
Storage.Contract.Delegated.(Storage_sigs.Data_set_storage.elements)
(ctxt, contract).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Definition find
: Raw_context.t → Contract_repr.t → M? (option Signature.public_key_hash) :=
Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.find).
Definition init_value
(ctxt : Raw_context.t) (contract : Contract_repr.t)
(delegate : Signature.public_key_hash) : M? Raw_context.t :=
let? ctxt :=
Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.init_value)
ctxt contract delegate in
let delegate_contract := Contract_repr.Implicit delegate in
Error_monad.op_gtpipeeq
(Storage.Contract.Delegated.(Storage_sigs.Data_set_storage.add)
(ctxt, delegate_contract) contract) Error_monad.ok.
Definition unlink (ctxt : Raw_context.t) (contract : Contract_repr.t)
: M? Raw_context.t :=
let? function_parameter :=
Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.find) ctxt
contract in
match function_parameter with
| None ⇒ return? ctxt
| Some delegate ⇒
let delegate_contract := Contract_repr.Implicit delegate in
Error_monad.op_gtpipeeq
(Storage.Contract.Delegated.(Storage_sigs.Data_set_storage.remove)
(ctxt, delegate_contract) contract) Error_monad.ok
end.
Definition delete (ctxt : Raw_context.t) (contract : Contract_repr.t)
: M? Raw_context.t :=
let? ctxt := unlink ctxt contract in
Error_monad.op_gtpipeeq
(Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.remove) ctxt
contract) Error_monad.ok.
Definition set
(ctxt : Raw_context.t) (contract : Contract_repr.t)
(delegate : Signature.public_key_hash) : M? Raw_context.t :=
let? ctxt := unlink ctxt contract in
let ctxt :=
Storage.Contract.Delegate.(Storage_sigs.Indexed_data_storage.add) ctxt
contract delegate in
let delegate_contract := Contract_repr.Implicit delegate in
Error_monad.op_gtpipeeq
(Storage.Contract.Delegated.(Storage_sigs.Data_set_storage.add)
(ctxt, delegate_contract) contract) Error_monad.ok.
Definition delegated_contracts
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (list Contract_repr.t) :=
let contract := Contract_repr.Implicit delegate in
Storage.Contract.Delegated.(Storage_sigs.Data_set_storage.elements)
(ctxt, contract).