🎫 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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Carbonated_map.
Require TezosOfOCaml.Proto_alpha.Carbonated_map_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_token.

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

Definition Ticket_token_map :=
  Carbonated_map.Make
    (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.ex_token.Ex_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.context → option A → M? (option A × Alpha_context.context))
  (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.context) :=
  let? '(key_hash, ctxt) := key_of_ticket_token ctxt key_value in
  let f_value {B : Set}
    (ctxt : Alpha_context.context) (val_opt : option (B × A))
    : M? (option (Ticket_token.ex_token × A) × Alpha_context.context) :=
    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 {A B C : Set}
  (ctxt : Alpha_context.context)
  (f_value :
    Alpha_context.context → A → B → C → M? (A × Alpha_context.context))
  : A → Ticket_token_map.(Carbonated_map.S.t) (B × C) →
  M? (A × Alpha_context.context) :=
  Ticket_token_map.(Carbonated_map.S.fold) ctxt
    (fun (ctxt : Alpha_context.context) ⇒
      fun (acc_value : A) ⇒
        fun (_key_hash : Alpha_context.Ticket_hash.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.context) :=
  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.context → A → A → M? (A × Alpha_context.context))
  (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.context) ⇒
            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 {A B C : Set}
  (ctxt : Alpha_context.context)
  (f_value : Alpha_context.context → A → B → M? (C × Alpha_context.context))
  : Ticket_token_map.(Carbonated_map.S.t) (A × B) →
  M? (Ticket_token_map.(Carbonated_map.S.t) (A × C) × Alpha_context.context) :=
  Ticket_token_map.(Carbonated_map.S.map) ctxt
    (fun (ctxt : Alpha_context.context) ⇒
      fun (_key : Alpha_context.Ticket_hash.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.context) (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.context)
  (merge_overlap :
    Alpha_context.context → A → A → M? (A × Alpha_context.context))
  : 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.context) :=
  Ticket_token_map.(Carbonated_map.S.merge) ctxt
    (lift_merge_overlap merge_overlap).