⛽ Local_gas_counter.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.

Inductive local_gas_counter : Set :=
| Local_gas_counter : int → local_gas_counter.

Inductive outdated_context : Set :=
| Outdated_context : Alpha_context.context → outdated_context.

Definition outdated_context_value (ctxt : Alpha_context.context)
  : outdated_context := Outdated_context ctxt.

Definition update_context (function_parameter : local_gas_counter)
  : outdated_context → Alpha_context.context :=
  let 'Local_gas_counter gas_counter := function_parameter in
  fun (function_parameter : outdated_context) ⇒
    let 'Outdated_context ctxt := function_parameter in
    Alpha_context.Gas.update_remaining_operation_gas ctxt
      (Alpha_context.Gas.fp_of_milligas_int gas_counter).

Definition local_gas_counter_value (ctxt : Alpha_context.context)
  : local_gas_counter :=
  Local_gas_counter (Alpha_context.Gas.remaining_operation_gas ctxt).

Definition local_gas_counter_and_outdated_context (ctxt : Alpha_context.context)
  : local_gas_counter × outdated_context :=
  ((local_gas_counter_value ctxt), (outdated_context_value ctxt)).

Definition use_gas_counter_in_context {A B : Set}
  (ctxt : outdated_context) (gas_counter : local_gas_counter)
  (f_value :
    Alpha_context.context → Pervasives.result (A × Alpha_context.context) B)
  : Pervasives.result (A × outdated_context × local_gas_counter) B :=
  let ctxt := update_context gas_counter ctxt in
  let? '(y_value, ctxt) := f_value ctxt in
  return?
    (y_value, (outdated_context_value ctxt), (local_gas_counter_value ctxt)).

Definition consume_opt (function_parameter : local_gas_counter)
  : Alpha_context.Gas.cost → option local_gas_counter :=
  let 'Local_gas_counter gas_counter := function_parameter in
  fun (cost : Alpha_context.Gas.cost) ⇒
    let gas_counter := gas_counter -i cost in
    if gas_counter <i 0 then
      None
    else
      Some (Local_gas_counter gas_counter).

Definition consume
  (local_gas_counter_value : local_gas_counter) (cost : Alpha_context.Gas.cost)
  : M? local_gas_counter :=
  match consume_opt local_gas_counter_value cost with
  | None ⇒
    Error_monad.error_value
      (Build_extensible "Operation_quota_exceeded" unit tt)
  | Some local_gas_counter_value ⇒ Pervasives.Ok local_gas_counter_value
  end.