Skip to main content

✒️ Contract_delegate_storage.v

Translated OCaml

See proofs, Gitlab , 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
  | Nonereturn? 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).