🐆 Tx_rollup_state_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.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.
Definition init_value (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
: M? Raw_context.t :=
let? '(ctxt, already_exists) :=
Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
ctxt tx_rollup in
let? '_ :=
Error_monad.fail_when already_exists
(Build_extensible "Tx_rollup_already_exists" Tx_rollup_repr.t tx_rollup)
in
let pre_allocated_storage :=
Z.of_int (Constants_storage.tx_rollup_origination_size ctxt) in
Error_monad.op_gtpipeeqquestion
(Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt tx_rollup (Tx_rollup_state_repr.initial_state pre_allocated_storage))
Pervasives.fst.
Definition find
: Raw_context.t → Tx_rollup_repr.t →
M? (Raw_context.t × option Tx_rollup_state_repr.t) :=
Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find).
Definition get (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
: M? (Raw_context.t × Tx_rollup_state_repr.t) :=
let? '(ctxt, state_value) := find ctxt tx_rollup in
match state_value with
| Some state_value ⇒ return? (ctxt, state_value)
| None ⇒
Error_monad.tzfail
(Build_extensible "Tx_rollup_does_not_exist" Tx_rollup_repr.t tx_rollup)
end.
Definition assert_exist (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
: M? Raw_context.t :=
let? '(ctxt, tx_rollup_exists) :=
Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
ctxt tx_rollup in
let? '_ :=
Error_monad.fail_unless tx_rollup_exists
(Build_extensible "Tx_rollup_does_not_exist" Tx_rollup_repr.t tx_rollup)
in
return? ctxt.
Definition update
(ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
(t_value : Tx_rollup_state_repr.t) : M? Raw_context.t :=
let? '(ctxt, _) :=
Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt tx_rollup t_value in
return? ctxt.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.
Definition init_value (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
: M? Raw_context.t :=
let? '(ctxt, already_exists) :=
Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
ctxt tx_rollup in
let? '_ :=
Error_monad.fail_when already_exists
(Build_extensible "Tx_rollup_already_exists" Tx_rollup_repr.t tx_rollup)
in
let pre_allocated_storage :=
Z.of_int (Constants_storage.tx_rollup_origination_size ctxt) in
Error_monad.op_gtpipeeqquestion
(Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
ctxt tx_rollup (Tx_rollup_state_repr.initial_state pre_allocated_storage))
Pervasives.fst.
Definition find
: Raw_context.t → Tx_rollup_repr.t →
M? (Raw_context.t × option Tx_rollup_state_repr.t) :=
Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find).
Definition get (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
: M? (Raw_context.t × Tx_rollup_state_repr.t) :=
let? '(ctxt, state_value) := find ctxt tx_rollup in
match state_value with
| Some state_value ⇒ return? (ctxt, state_value)
| None ⇒
Error_monad.tzfail
(Build_extensible "Tx_rollup_does_not_exist" Tx_rollup_repr.t tx_rollup)
end.
Definition assert_exist (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
: M? Raw_context.t :=
let? '(ctxt, tx_rollup_exists) :=
Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
ctxt tx_rollup in
let? '_ :=
Error_monad.fail_unless tx_rollup_exists
(Build_extensible "Tx_rollup_does_not_exist" Tx_rollup_repr.t tx_rollup)
in
return? ctxt.
Definition update
(ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
(t_value : Tx_rollup_state_repr.t) : M? Raw_context.t :=
let? '(ctxt, _) :=
Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
ctxt tx_rollup t_value in
return? ctxt.