⛽ 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
| None ⇒ None
| Some x_value ⇒ f_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_value ⇒ f_value y_value gas
| Pervasives.Error err ⇒ of_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
| None ⇒ None
| Some gas ⇒ Some ((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.
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
| None ⇒ None
| Some x_value ⇒ f_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_value ⇒ f_value y_value gas
| Pervasives.Error err ⇒ of_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
| None ⇒ None
| Some gas ⇒ Some ((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.