🎫 Ticket_token.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.Script_typed_ir.

Module parsed_token.
  Record record {a : Set} : Set := Build {
    ticketer : Alpha_context.Contract.t;
    contents_type : Script_typed_ir.comparable_ty;
    contents : a;
  }.
  Arguments record : clear implicits.
  Definition with_ticketer {t_a} ticketer (r : record t_a) :=
    Build t_a ticketer r.(contents_type) r.(contents).
  Definition with_contents_type {t_a} contents_type (r : record t_a) :=
    Build t_a r.(ticketer) contents_type r.(contents).
  Definition with_contents {t_a} contents (r : record t_a) :=
    Build t_a r.(ticketer) r.(contents_type) contents.
End parsed_token.
Definition parsed_token := parsed_token.record.

Inductive ex_token : Set :=
| Ex_token : ∀ {a : Set}, parsed_token a → ex_token.

Module unparsed_token.
  Record record : Set := Build {
    ticketer : Alpha_context.Contract.t;
    contents_type : Alpha_context.Script.expr;
    contents : Alpha_context.Script.expr;
  }.
  Definition with_ticketer ticketer (r : record) :=
    Build ticketer r.(contents_type) r.(contents).
  Definition with_contents_type contents_type (r : record) :=
    Build r.(ticketer) contents_type r.(contents).
  Definition with_contents contents (r : record) :=
    Build r.(ticketer) r.(contents_type) contents.
End unparsed_token.
Definition unparsed_token := unparsed_token.record.

Definition unparsed_token_encoding : Data_encoding.encoding unparsed_token :=
  Data_encoding.conv
    (fun (function_parameter : unparsed_token) ⇒
      let '{|
        unparsed_token.ticketer := ticketer;
          unparsed_token.contents_type := contents_type;
          unparsed_token.contents := contents
          |} := function_parameter in
      (ticketer, contents_type, contents))
    (fun (function_parameter :
      Alpha_context.Contract.t × Alpha_context.Script.expr ×
        Alpha_context.Script.expr) ⇒
      let '(ticketer, contents_type, contents) := function_parameter in
      {| unparsed_token.ticketer := ticketer;
        unparsed_token.contents_type := contents_type;
        unparsed_token.contents := contents; |}) None
    (Data_encoding.obj3
      (Data_encoding.req None None "ticketer" Alpha_context.Contract.encoding)
      (Data_encoding.req None None "content_type"
        Alpha_context.Script.expr_encoding)
      (Data_encoding.req None None "content" Alpha_context.Script.expr_encoding)).