🎫 Ticket_token_map.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.Carbonated_map.
Require TezosOfOCaml.Proto_alpha.Carbonated_map_costs.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_token_unparser.

A carbonated map where the keys are [Ticket_hash.t] values.

Definition Ticket_token_map :=
  Carbonated_map.Make
    (let context : Set := Alpha_context.context in
    let consume := Alpha_context.Gas.consume in
    {|
      Carbonated_map.GAS.consume := consume
    |})
    (let t : Set := Alpha_context.Ticket_hash.t in
    let compare := Alpha_context.Ticket_hash.compare in
    let compare_cost {A : Set} (function_parameter : A)
      : Alpha_context.Gas.cost :=
      let '_ := function_parameter in
      Ticket_costs.Constants.cost_compare_ticket_hash in
    {|
      Carbonated_map.COMPARABLE.compare := compare;
      Carbonated_map.COMPARABLE.compare_cost := compare_cost
    |}).

Conceptually a map from [Ticket_token.ex_token] to values. Since ticket-tokens are expensive to compare we use [Ticket_hash.t] keys instead, and store the ticket-token along with the value.

Definition t (a : Set) : Set :=
  Ticket_token_map.(Carbonated_map.S.t) (Ticket_token.ex_token × a).

Definition empty {A : Set} : Ticket_token_map.(Carbonated_map.S.t) A :=
  Ticket_token_map.(Carbonated_map.S.empty).

Definition key_of_ticket_token
  (ctxt : Alpha_context.context) (function_parameter : Ticket_token.ex_token)
  : M? (Alpha_context.Ticket_hash.t × Alpha_context.context) :=
  let
    '(Ticket_token.Ex_token {| Ticket_token.parsed_token.ticketer := ticketer |})
      as token := function_parameter in
  Ticket_balance_key.of_ex_token ctxt
    (Alpha_context.Destination.Contract ticketer) token.

Definition update {A : Set}
  (ctxt : Alpha_context.context) (key_value : Ticket_token.ex_token)
  (f_value : Alpha_context.t → option A → M? (option A × Alpha_context.t))
  (m_value : Ticket_token_map.(Carbonated_map.S.t) (Ticket_token.ex_token × A))
  : M?
    (Ticket_token_map.(Carbonated_map.S.t) (Ticket_token.ex_token × A) ×
      Alpha_context.t) :=
  let? '(key_hash, ctxt) := key_of_ticket_token ctxt key_value in
  let f_value {B : Set} (ctxt : Alpha_context.t) (val_opt : option (B × A))
    : M? (option (Ticket_token.ex_token × A) × Alpha_context.t) :=
    let? '(val_opt, ctxt) :=
      match val_opt with
      | Some (_tkn, value_value) ⇒ f_value ctxt (Some value_value)
      | None ⇒ f_value ctxt None
      end in
    return?
      ((Option.map (fun (v_value : A) ⇒ (key_value, v_value)) val_opt), ctxt)
    in
  Ticket_token_map.(Carbonated_map.S.update) ctxt key_hash f_value m_value.

Definition fold_e {A B C : Set}
  (ctxt : Alpha_context.t)
  (f_value : Alpha_context.t → A → B → C → M? (A × Alpha_context.t))
  : A → Ticket_token_map.(Carbonated_map.S.t) (B × C) →
  M? (A × Alpha_context.t) :=
  Ticket_token_map.(Carbonated_map.S.fold_e) ctxt
    (fun (ctxt : Alpha_context.t) ⇒
      fun (acc_value : A) ⇒
        fun (_key_hash : Ticket_hash_repr.t) ⇒
          fun (function_parameter : B × C) ⇒
            let '(tkn, value_value) := function_parameter in
            f_value ctxt acc_value tkn value_value).

Definition fold_es {A B C : Set}
  (ctxt : Alpha_context.t)
  (f_value : Alpha_context.t → A → B → C → M? (A × Alpha_context.t))
  : A → Ticket_token_map.(Carbonated_map.S.t) (B × C) →
  M? (A × Alpha_context.t) :=
  Ticket_token_map.(Carbonated_map.S.fold_es) ctxt
    (fun (ctxt : Alpha_context.t) ⇒
      fun (acc_value : A) ⇒
        fun (_key_hash : Ticket_hash_repr.t) ⇒
          fun (function_parameter : B × C) ⇒
            let '(tkn, value_value) := function_parameter in
            f_value ctxt acc_value tkn value_value).

Definition find {A B : Set}
  (ctxt : Alpha_context.context) (ticket_token : Ticket_token.ex_token)
  (map : Ticket_token_map.(Carbonated_map.S.t) (A × B))
  : M? (option B × Alpha_context.t) :=
  let? '(key_hash, ctxt) := key_of_ticket_token ctxt ticket_token in
  let? '(val_opt, ctxt) :=
    Ticket_token_map.(Carbonated_map.S.find) ctxt key_hash map in
  return? ((Option.map Pervasives.snd val_opt), ctxt).

Definition lift_merge_overlap {A B C D E F G H : Set}
  (merge_overlap : A → B → C → Pervasives.result (D × E) F) (ctxt : A)
  (function_parameter : G × B) : H × C → Pervasives.result ((G × D) × E) F :=
  let '(tkn1, v1) := function_parameter in
  fun (function_parameter : H × C) ⇒
    let '(_tkn2, v2) := function_parameter in
    let? '(v_value, ctxt) := merge_overlap ctxt v1 v2 in
    return? ((tkn1, v_value), ctxt).

Definition of_list {A : Set}
  (ctxt : Alpha_context.context)
  (merge_overlap : Alpha_context.t → A → A → M? (A × Alpha_context.t))
  (token_values : list (Ticket_token.ex_token × A))
  : M?
    (Ticket_token_map.(Carbonated_map.S.t) (Ticket_token.ex_token × A) ×
      Alpha_context.context) :=
  List.fold_left_es
    (fun (function_parameter :
      Ticket_token_map.(Carbonated_map.S.t) (Ticket_token.ex_token × A) ×
        Alpha_context.context) ⇒
      let '(map, ctxt) := function_parameter in
      fun (function_parameter : Ticket_token.ex_token × A) ⇒
        let '(token, value_value) := function_parameter in
        let? '(key_hash, ctxt) := key_of_ticket_token ctxt token in
        Ticket_token_map.(Carbonated_map.S.update) ctxt key_hash
          (fun (ctxt : Alpha_context.t) ⇒
            fun (old_val : option (Ticket_token.ex_token × A)) ⇒
              match old_val with
              | None ⇒ return? ((Some (token, value_value)), ctxt)
              | Some old ⇒
                let? '(x_value, ctxt) :=
                  lift_merge_overlap merge_overlap ctxt old (token, value_value)
                  in
                return? ((Some x_value), ctxt)
              end) map) (Ticket_token_map.(Carbonated_map.S.empty), ctxt)
    token_values.

Definition map_e {A B C : Set}
  (ctxt : Alpha_context.t)
  (f_value : Alpha_context.t → A → B → M? (C × Alpha_context.t))
  : Ticket_token_map.(Carbonated_map.S.t) (A × B) →
  M? (Ticket_token_map.(Carbonated_map.S.t) (A × C) × Alpha_context.t) :=
  Ticket_token_map.(Carbonated_map.S.map_e) ctxt
    (fun (ctxt : Alpha_context.t) ⇒
      fun (_key : Ticket_hash_repr.t) ⇒
        fun (function_parameter : A × B) ⇒
          let '(tkn, value_value) := function_parameter in
          let? '(new_value, ctxt) := f_value ctxt tkn value_value in
          return? ((tkn, new_value), ctxt)).

Definition to_list {A : Set}
  (ctxt : Alpha_context.t) (map : Ticket_token_map.(Carbonated_map.S.t) A)
  : M? (list A × Alpha_context.context) :=
  let? '(list_value, ctxt) :=
    Ticket_token_map.(Carbonated_map.S.to_list) ctxt map in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Carbonated_map_costs.fold_cost
        (Ticket_token_map.(Carbonated_map.S.size_value) map)) in
  return? ((List.map Pervasives.snd list_value), ctxt).

Definition merge {A B : Set}
  (ctxt : Alpha_context.t)
  (merge_overlap : Alpha_context.t → A → A → M? (A × Alpha_context.t))
  : Ticket_token_map.(Carbonated_map.S.t) (B × A) →
  Ticket_token_map.(Carbonated_map.S.t) (B × A) →
  M? (Ticket_token_map.(Carbonated_map.S.t) (B × A) × Alpha_context.t) :=
  Ticket_token_map.(Carbonated_map.S.merge) ctxt
    (lift_merge_overlap merge_overlap).

Definition to_ticket_receipt
  (ctxt : Alpha_context.t) (owner : Alpha_context.Destination.t)
  (ticket_token_map :
    Ticket_token_map.(Carbonated_map.S.t) (Ticket_token.ex_token × Z.t))
  : M? (list Ticket_receipt.item × Alpha_context.t) :=
  Ticket_token_map.(Carbonated_map.S.fold_es) ctxt
    (fun (ctxt : Alpha_context.t) ⇒
      fun (acc_value : list Ticket_receipt.item) ⇒
        fun (_ticket_hash : Ticket_hash_repr.t) ⇒
          fun (function_parameter : Ticket_token.ex_token × Z.t) ⇒
            let '(ex_ticket, amount) := function_parameter in
            if Z.equal amount Z.zero then
              return? (acc_value, ctxt)
            else
              let? '(ticket_token, ctxt) :=
                Ticket_token_unparser.unparse ctxt ex_ticket in
              let update :=
                {| Ticket_receipt.item.ticket_token := ticket_token;
                  Ticket_receipt.item.updates :=
                    [
                      {| Ticket_receipt.update.account := owner;
                        Ticket_receipt.update.amount :=
                          amount; |}
                    ]; |} in
              return? ((cons update acc_value), ctxt)) nil ticket_token_map.