🚗 Migration_repr.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_hash.
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_hash.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 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) :=
Data_encoding.def "operation.alpha.origination_result" None None
(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_hash.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.originated_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)))).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
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_hash.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 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) :=
Data_encoding.def "operation.alpha.origination_result" None None
(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_hash.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.originated_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)))).