Skip to main content

🚗 Migration_repr.v

Translated OCaml

See proofs, Gitlab , 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.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.

Module origination_result.
  Record record : Set := Build {
    balance_updates : Receipt_repr.balance_updates;
    originated_contracts : list Contract_repr.t;
    storage_size : Z.t;
    paid_storage_size_diff : Z.t;
  }.
  Definition with_balance_updates balance_updates (r : record) :=
    Build balance_updates r.(originated_contracts) r.(storage_size)
      r.(paid_storage_size_diff).
  Definition with_originated_contracts originated_contracts (r : record) :=
    Build r.(balance_updates) originated_contracts r.(storage_size)
      r.(paid_storage_size_diff).
  Definition with_storage_size storage_size (r : record) :=
    Build r.(balance_updates) r.(originated_contracts) storage_size
      r.(paid_storage_size_diff).
  Definition with_paid_storage_size_diff (r : record) :=
    Build r.(balance_updates) r.(originated_contracts) r.(storage_size)
      paid_storage_size_diff.
End origination_result.
Definition origination_result := origination_result.record.

Definition origination_result_list_encoding
  : Data_encoding.encoding (list origination_result) :=
  (let arg := Data_encoding.def "operation.alpha.origination_result" in
  fun (eta : Data_encoding.encoding (list origination_result)) ⇒
    arg None None eta)
    (Data_encoding.list_value None
      (Data_encoding.conv
        (fun (function_parameter : origination_result) ⇒
          let '{|
            origination_result.balance_updates := balance_updates;
              origination_result.originated_contracts := originated_contracts;
              origination_result.storage_size := storage_size;
              origination_result.paid_storage_size_diff :=
                paid_storage_size_diff
              |} := function_parameter in
          (balance_updates, originated_contracts, storage_size,
            paid_storage_size_diff))
        (fun (function_parameter :
          Receipt_repr.balance_updates × list Contract_repr.t × Z.t × Z.t) ⇒
          let
            '(balance_updates, originated_contracts, storage_size,
              paid_storage_size_diff) := function_parameter in
          {| origination_result.balance_updates := balance_updates;
            origination_result.originated_contracts := originated_contracts;
            origination_result.storage_size := storage_size;
            origination_result.paid_storage_size_diff := paid_storage_size_diff;
            |}) None
        (Data_encoding.obj4
          (Data_encoding.dft None None "balance_updates"
            Receipt_repr.balance_updates_encoding nil)
          (Data_encoding.dft None None "originated_contracts"
            (Data_encoding.list_value None Contract_repr.encoding) nil)
          (Data_encoding.dft None None "storage_size" Data_encoding.z_value
            Z.zero)
          (Data_encoding.dft None None "paid_storage_size_diff"
            Data_encoding.z_value Z.zero)))).