🐆 Tx_rollup_parameters.v

Translated OCaml

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.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.

Module deposit_parameters.
  Record record : Set := Build {
    ex_ticket : Ticket_scanner.ex_ticket;
    l2_destination : Script_typed_ir.tx_rollup_l2_address;
  }.
  Definition with_ex_ticket ex_ticket (r : record) :=
    Build ex_ticket r.(l2_destination).
  Definition with_l2_destination l2_destination (r : record) :=
    Build r.(ex_ticket) l2_destination.
End deposit_parameters.
Definition deposit_parameters := deposit_parameters.record.

Definition get_deposit_parameters {a : Set}
  (ty : Script_typed_ir.ty) (contents : a) : M? deposit_parameters :=
  match (ty, contents) with
  |
    (Script_typed_ir.Pair_t (Script_typed_ir.Ticket_t ty _)
      Script_typed_ir.Tx_rollup_l2_address_t _ _, contents) ⇒
    let 'existT _ __2 [contents, ty] :=
      cast_exists (Es := Set)
        (fun __2 ⇒
          [Script_typed_ir.ticket __2 × Script_typed_ir.tx_rollup_l2_address **
            Script_typed_ir.comparable_ty]) [contents, ty] in
    let '(ticket, l2_destination) := contents in
    return?
      {| deposit_parameters.ex_ticket := Ticket_scanner.Ex_ticket ty ticket;
        deposit_parameters.l2_destination := l2_destination; |}
  | _ ⇒
    Error_monad.error_value
      (Build_extensible "Wrong_deposit_parameters" unit tt)
  end.