🦏 Sc_rollup_outbox_message_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.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
let msg :=
"Failed to encode a rollup management protocol outbox message value" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_outbox_message_repr.error_encoding_outbox_message" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_encode_outbox_message" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_encode_outbox_message" unit tt) in
let msg :=
"Failed to decode a rollup management protocol outbox message value" in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_outbox_message_repr.error_decoding_outbox_message" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_decode_outbox_message" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_decode_outbox_message" unit tt).
Module transaction.
Record record : Set := Build {
unparsed_parameters : Script_repr.expr;
destination : Contract_hash.t;
entrypoint : Entrypoint_repr.t;
}.
Definition with_unparsed_parameters unparsed_parameters (r : record) :=
Build unparsed_parameters r.(destination) r.(entrypoint).
Definition with_destination destination (r : record) :=
Build r.(unparsed_parameters) destination r.(entrypoint).
Definition with_entrypoint entrypoint (r : record) :=
Build r.(unparsed_parameters) r.(destination) entrypoint.
End transaction.
Definition transaction := transaction.record.
let msg :=
"Failed to encode a rollup management protocol outbox message value" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_outbox_message_repr.error_encoding_outbox_message" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_encode_outbox_message" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_encode_outbox_message" unit tt) in
let msg :=
"Failed to decode a rollup management protocol outbox message value" in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_outbox_message_repr.error_decoding_outbox_message" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_decode_outbox_message" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_decode_outbox_message" unit tt).
Module transaction.
Record record : Set := Build {
unparsed_parameters : Script_repr.expr;
destination : Contract_hash.t;
entrypoint : Entrypoint_repr.t;
}.
Definition with_unparsed_parameters unparsed_parameters (r : record) :=
Build unparsed_parameters r.(destination) r.(entrypoint).
Definition with_destination destination (r : record) :=
Build r.(unparsed_parameters) destination r.(entrypoint).
Definition with_entrypoint entrypoint (r : record) :=
Build r.(unparsed_parameters) r.(destination) entrypoint.
End transaction.
Definition transaction := transaction.record.
Records for the constructor parameters
Module ConstructorRecords_t.
Module t.
Module Atomic_transaction_batch.
Record record {transactions : Set} : Set := Build {
transactions : transactions;
}.
Arguments record : clear implicits.
Definition with_transactions {t_transactions} transactions
(r : record t_transactions) :=
Build t_transactions transactions.
End Atomic_transaction_batch.
Definition Atomic_transaction_batch_skeleton :=
Atomic_transaction_batch.record.
End t.
End ConstructorRecords_t.
Import ConstructorRecords_t.
Reserved Notation "'t.Atomic_transaction_batch".
Inductive t : Set :=
| Atomic_transaction_batch : 't.Atomic_transaction_batch → t
where "'t.Atomic_transaction_batch" :=
(t.Atomic_transaction_batch_skeleton (list transaction)).
Module t.
Include ConstructorRecords_t.t.
Definition Atomic_transaction_batch := 't.Atomic_transaction_batch.
End t.
Definition transaction_encoding : Data_encoding.encoding transaction :=
Data_encoding.conv
(fun (function_parameter : transaction) ⇒
let '{|
transaction.unparsed_parameters := unparsed_parameters;
transaction.destination := destination;
transaction.entrypoint := entrypoint
|} := function_parameter in
(unparsed_parameters, destination, entrypoint))
(fun (function_parameter :
Script_repr.expr × Contract_hash.t × Entrypoint_repr.t) ⇒
let '(unparsed_parameters, destination, entrypoint) := function_parameter
in
{| transaction.unparsed_parameters := unparsed_parameters;
transaction.destination := destination;
transaction.entrypoint := entrypoint; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "parameters" Script_repr.expr_encoding)
(Data_encoding.req None None "destination"
Contract_repr.originated_encoding)
(Data_encoding.dft None None "entrypoint" Entrypoint_repr.simple_encoding
Entrypoint_repr.default)).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.check_size Constants_repr.sc_rollup_message_size_limit
(Data_encoding.union None
[
Data_encoding.case_value "Atomic_transaction_batch" None
(Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "transactions"
(Data_encoding.list_value None transaction_encoding)))
(fun (function_parameter : t) ⇒
let
'Atomic_transaction_batch {|
t.Atomic_transaction_batch.transactions := transactions
|} := function_parameter in
Some transactions)
(fun (transactions : list transaction) ⇒
Atomic_transaction_batch
{|
t.Atomic_transaction_batch.transactions :=
transactions; |})
]).
Definition pp_transaction
(fmt : Format.formatter) (function_parameter : transaction) : unit :=
let '{|
transaction.unparsed_parameters := unparsed_parameters;
transaction.destination := destination;
transaction.entrypoint := entrypoint
|} := function_parameter in
let json_value :=
Data_encoding.Json.construct None Script_repr.expr_encoding
unparsed_parameters in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))
"@[%a@;%a@;%a@]") Contract_hash.pp destination Entrypoint_repr.pp
entrypoint Data_encoding.Json.pp json_value.
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let
'Atomic_transaction_batch {|
t.Atomic_transaction_batch.transactions := transactions |} :=
function_parameter in
Format.pp_print_list (Some Format.pp_print_space) pp_transaction fmt
transactions.
Definition serialized : Set := string.
Definition deserialize (data : string) : M? t :=
match Data_encoding.Binary.of_string_opt encoding data with
| Some x_value ⇒ return? x_value
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Error_decode_outbox_message" unit tt)
end.
Definition serialize (outbox_message : t) : M? string :=
match Data_encoding.Binary.to_string_opt None encoding outbox_message with
| Some str ⇒ return? str
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Error_encode_outbox_message" unit tt)
end.
Definition unsafe_of_string {A : Set} (s_value : A) : A := s_value.
Definition unsafe_to_string {A : Set} (s_value : A) : A := s_value.
Module t.
Module Atomic_transaction_batch.
Record record {transactions : Set} : Set := Build {
transactions : transactions;
}.
Arguments record : clear implicits.
Definition with_transactions {t_transactions} transactions
(r : record t_transactions) :=
Build t_transactions transactions.
End Atomic_transaction_batch.
Definition Atomic_transaction_batch_skeleton :=
Atomic_transaction_batch.record.
End t.
End ConstructorRecords_t.
Import ConstructorRecords_t.
Reserved Notation "'t.Atomic_transaction_batch".
Inductive t : Set :=
| Atomic_transaction_batch : 't.Atomic_transaction_batch → t
where "'t.Atomic_transaction_batch" :=
(t.Atomic_transaction_batch_skeleton (list transaction)).
Module t.
Include ConstructorRecords_t.t.
Definition Atomic_transaction_batch := 't.Atomic_transaction_batch.
End t.
Definition transaction_encoding : Data_encoding.encoding transaction :=
Data_encoding.conv
(fun (function_parameter : transaction) ⇒
let '{|
transaction.unparsed_parameters := unparsed_parameters;
transaction.destination := destination;
transaction.entrypoint := entrypoint
|} := function_parameter in
(unparsed_parameters, destination, entrypoint))
(fun (function_parameter :
Script_repr.expr × Contract_hash.t × Entrypoint_repr.t) ⇒
let '(unparsed_parameters, destination, entrypoint) := function_parameter
in
{| transaction.unparsed_parameters := unparsed_parameters;
transaction.destination := destination;
transaction.entrypoint := entrypoint; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "parameters" Script_repr.expr_encoding)
(Data_encoding.req None None "destination"
Contract_repr.originated_encoding)
(Data_encoding.dft None None "entrypoint" Entrypoint_repr.simple_encoding
Entrypoint_repr.default)).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.check_size Constants_repr.sc_rollup_message_size_limit
(Data_encoding.union None
[
Data_encoding.case_value "Atomic_transaction_batch" None
(Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "transactions"
(Data_encoding.list_value None transaction_encoding)))
(fun (function_parameter : t) ⇒
let
'Atomic_transaction_batch {|
t.Atomic_transaction_batch.transactions := transactions
|} := function_parameter in
Some transactions)
(fun (transactions : list transaction) ⇒
Atomic_transaction_batch
{|
t.Atomic_transaction_batch.transactions :=
transactions; |})
]).
Definition pp_transaction
(fmt : Format.formatter) (function_parameter : transaction) : unit :=
let '{|
transaction.unparsed_parameters := unparsed_parameters;
transaction.destination := destination;
transaction.entrypoint := entrypoint
|} := function_parameter in
let json_value :=
Data_encoding.Json.construct None Script_repr.expr_encoding
unparsed_parameters in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
CamlinternalFormatBasics.End_of_format ""))
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@;" 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))
"@[%a@;%a@;%a@]") Contract_hash.pp destination Entrypoint_repr.pp
entrypoint Data_encoding.Json.pp json_value.
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let
'Atomic_transaction_batch {|
t.Atomic_transaction_batch.transactions := transactions |} :=
function_parameter in
Format.pp_print_list (Some Format.pp_print_space) pp_transaction fmt
transactions.
Definition serialized : Set := string.
Definition deserialize (data : string) : M? t :=
match Data_encoding.Binary.of_string_opt encoding data with
| Some x_value ⇒ return? x_value
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Error_decode_outbox_message" unit tt)
end.
Definition serialize (outbox_message : t) : M? string :=
match Data_encoding.Binary.to_string_opt None encoding outbox_message with
| Some str ⇒ return? str
| None ⇒
Error_monad.Result_syntax.tzfail
(Build_extensible "Error_encode_outbox_message" unit tt)
end.
Definition unsafe_of_string {A : Set} (s_value : A) : A := s_value.
Definition unsafe_to_string {A : Set} (s_value : A) : A := s_value.