🎫 Ticket_receipt.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Ticket_token.

Module update.
  Record record : Set := Build {
    account : Alpha_context.Destination.t;
    amount : Z.t;
  }.
  Definition with_account account (r : record) :=
    Build account r.(amount).
  Definition with_amount amount (r : record) :=
    Build r.(account) amount.
End update.
Definition update := update.record.

Module item.
  Record record : Set := Build {
    ticket_token : Ticket_token.unparsed_token;
    updates : list update;
  }.
  Definition with_ticket_token ticket_token (r : record) :=
    Build ticket_token r.(updates).
  Definition with_updates updates (r : record) :=
    Build r.(ticket_token) updates.
End item.
Definition item := item.record.

Definition t : Set := list item.

Definition update_encoding : Data_encoding.encoding update :=
  Data_encoding.conv
    (fun (function_parameter : update) ⇒
      let '{| update.account := account; update.amount := amount |} :=
        function_parameter in
      (account, amount))
    (fun (function_parameter : Alpha_context.Destination.t × Z.t) ⇒
      let '(account, amount) := function_parameter in
      {| update.account := account; update.amount := amount; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "account" Alpha_context.Destination.encoding)
      (Data_encoding.req None None "amount" Data_encoding.z_value)).

Definition item_encoding : Data_encoding.encoding item :=
  Data_encoding.conv
    (fun (function_parameter : item) ⇒
      let '{| item.ticket_token := ticket_token; item.updates := updates |} :=
        function_parameter in
      (ticket_token, updates))
    (fun (function_parameter : Ticket_token.unparsed_token × list update) ⇒
      let '(ticket_token, updates) := function_parameter in
      {| item.ticket_token := ticket_token; item.updates := updates; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "ticket_token"
        Ticket_token.unparsed_token_encoding)
      (Data_encoding.req None None "updates"
        (Data_encoding.list_value None update_encoding))).

Definition encoding : Data_encoding.encoding (list item) :=
  Data_encoding.list_value None item_encoding.