Skip to main content

⛽ Gas_monad.v

Translated OCaml

See proofs, See simulations, 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.Local_gas_counter.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.

Definition t (a trace : Set) : Set :=
  Local_gas_counter.local_gas_counter
  option (Pervasives.result a trace × Local_gas_counter.local_gas_counter).

Definition gas_monad (a trace : Set) : Set := t a trace.

Definition of_result {A B : Set} (x_value : A) (gas : B) : option (A × B) :=
  Some (x_value, gas).

Definition _return {A B C : Set} (x_value : A)
  : B option (Pervasives.result A C × B) := of_result (return? x_value).

Definition return_unit {A B : Set}
  : A option (Pervasives.result unit B × A) := _return tt.

Definition op_gtgtquestionquestion {A B : Set}
  (m_value : option A) (f_value : A option B) : option B :=
  match m_value with
  | NoneNone
  | Some x_valuef_value x_value
  end.

Definition bind {A B C D E : Set}
  (m_value : A option (Pervasives.result B C × D))
  (f_value : B D option (Pervasives.result E C × D)) (gas : A)
  : option (Pervasives.result E C × D) :=
  op_gtgtquestionquestion (m_value gas)
    (fun (function_parameter : Pervasives.result B C × D) ⇒
      let '(res, gas) := function_parameter in
      match res with
      | Pervasives.Ok y_valuef_value y_value gas
      | Pervasives.Error errof_result (Pervasives.Error err) gas
      end).

Definition map {A B C D E : Set}
  (f_value : A B) (m_value : C option (Pervasives.result A D × E))
  (gas : C) : option (Pervasives.result B D × E) :=
  op_gtgtquestionquestion (m_value gas)
    (fun (function_parameter : Pervasives.result A D × E) ⇒
      let '(x_value, gas) := function_parameter in
      of_result (Error_monad.op_gtpipequestion x_value f_value) gas).

Definition bind_result {A B C D : Set}
  (m_value : Pervasives.result A B)
  (f_value : A C option (Pervasives.result D B × C))
  : C option (Pervasives.result D B × C) := bind (of_result m_value) f_value.

Definition bind_recover {A B C D : Set}
  (m_value : A option (B × C)) (f_value : B C option D) (gas : A)
  : option D :=
  op_gtgtquestionquestion (m_value gas)
    (fun (function_parameter : B × C) ⇒
      let '(x_value, gas) := function_parameter in
      f_value x_value gas).

Definition consume_gas {A : Set}
  (cost : Alpha_context.Gas.cost) (gas : Local_gas_counter.local_gas_counter)
  : option (Pervasives.result unit A × Local_gas_counter.local_gas_counter) :=
  match Local_gas_counter.consume_opt gas cost with
  | NoneNone
  | Some gasSome ((return? tt), gas)
  end.

Definition run {A : Set}
  (ctxt : Alpha_context.context)
  (m_value :
    Local_gas_counter.local_gas_counter
    option (A × Local_gas_counter.local_gas_counter))
  : M? (A × Alpha_context.context) :=
  match Alpha_context.Gas.level ctxt with
  | Alpha_context.Gas.Unaccounted
    match
      m_value (Local_gas_counter.Local_gas_counter Saturation_repr.saturated)
      with
    | Some (res, _new_gas_counter)return? (res, ctxt)
    | None
      Error_monad.error_value
        (Build_extensible "Operation_quota_exceeded" unit tt)
    end
  | Alpha_context.Gas.Limited {| Alpha_context.Gas.t.Limited.remaining := _ |}
    ⇒
    let '(gas_counter, outdated_ctxt) :=
      Local_gas_counter.local_gas_counter_and_outdated_context ctxt in
    match m_value gas_counter with
    | Some (res, new_gas_counter)
      let ctxt := Local_gas_counter.update_context new_gas_counter outdated_ctxt
        in
      return? (res, ctxt)
    | None
      Error_monad.error_value
        (Build_extensible "Operation_quota_exceeded" unit tt)
    end
  end.

Definition record_trace_eval {error_context a error_trace : Set}
  (error_details : Script_tc_errors.error_details error_context)
  (f_value : error_context Error_monad._error) (m_value : t a error_trace)
  : t a error_trace :=
  match (error_details, m_value) with
  | (Script_tc_errors.Fast, _)cast (t a error_trace) m_value
  | (Script_tc_errors.Informative err_ctxt, m_value)
    let '[m_value, err_ctxt] :=
      cast [t a (Error_monad.trace Error_monad._error) ** error_context]
        [m_value, err_ctxt] in
    cast (t a error_trace)
    (fun (gas : Local_gas_counter.local_gas_counter) ⇒
      op_gtgtquestionquestion (m_value gas)
        (fun (function_parameter : M? a × Local_gas_counter.local_gas_counter)
          ⇒
          let '(x_value, gas) := function_parameter in
          of_result
            (Error_monad.record_trace_eval
              (fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                f_value err_ctxt) x_value) gas))
  end.

Definition fail {A B C : Set} (e_value : A)
  : B option (Pervasives.result C A × B) :=
  of_result (Pervasives.Error e_value).

Module Syntax.
  Definition _return {A B C : Set}
    : A B option (Pervasives.result A C × B) := _return.

  Definition return_unit {A B : Set}
    : A option (Pervasives.result unit B × A) := return_unit.

  Definition return_none {A B C : Set}
    : A option (Pervasives.result (option B) C × A) := _return None.

  Definition return_some {A B C : Set} (x_value : A)
    : B option (Pervasives.result (option A) C × B) :=
    _return (Some x_value).

  Definition return_nil {A B C : Set}
    : A option (Pervasives.result (list B) C × A) := _return nil.

  Definition return_true {A B : Set}
    : A option (Pervasives.result bool B × A) := _return true.

  Definition return_false {A B : Set}
    : A option (Pervasives.result bool B × A) := _return false.

  Definition fail {A B C : Set}
    : A B option (Pervasives.result C A × B) := fail.

  Definition op_letstar {A B C D E : Set}
    : (A option (Pervasives.result B C × D))
    (B D option (Pervasives.result E C × D)) A
    option (Pervasives.result E C × D) := bind.

  Definition op_letplus {A B C D E : Set}
    (m_value : A option (Pervasives.result B C × D)) (f_value : B E)
    : A option (Pervasives.result E C × D) := map f_value m_value.

  Definition op_letstarquestion {A B C D : Set}
    : Pervasives.result A B (A C option (Pervasives.result D B × C))
    C option (Pervasives.result D B × C) := bind_result.
End Syntax.