🍃 Error_monad.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Inductive error_category : Set :=
| Outdated : error_category
| Permanent : error_category
| Temporary : error_category
| Branch : error_category.
Definition _error : Set := extensible_type.
Parameter error_encoding : Data_encoding.t _error.
Parameter pp : Format.formatter → _error → unit.
Parameter register_error_kind : ∀ {err : Set},
error_category → string → string → string →
option (Format.formatter → err → unit) → Data_encoding.t err →
(_error → option err) → (err → _error) → unit.
Parameter json_of_error : _error → Data_encoding.json.
Parameter error_of_json : Data_encoding.json → _error.
Module error_info.
Record record : Set := Build {
category : error_category;
id : string;
title : string;
description : string;
schema : Data_encoding.json_schema }.
Definition with_category category (r : record) :=
Build category r.(id) r.(title) r.(description) r.(schema).
Definition with_id id (r : record) :=
Build r.(category) id r.(title) r.(description) r.(schema).
Definition with_title title (r : record) :=
Build r.(category) r.(id) title r.(description) r.(schema).
Definition with_description description (r : record) :=
Build r.(category) r.(id) r.(title) description r.(schema).
Definition with_schema schema (r : record) :=
Build r.(category) r.(id) r.(title) r.(description) schema.
End error_info.
Definition error_info := error_info.record.
Parameter pp_info : Format.formatter → error_info → unit.
Parameter get_registered_errors : unit → list error_info.
Definition trace (err : Set) : Set := list err.
Definition tzresult (a : Set) : Set := Pervasives.result a (trace _error).
Parameter make_trace_encoding : ∀ {_error : Set},
Data_encoding.t _error → Data_encoding.t (trace _error).
Parameter trace_encoding : Data_encoding.t (trace _error).
Parameter pp_trace : Format.formatter → trace _error → unit.
Parameter result_encoding : ∀ {a : Set},
Data_encoding.t a → Data_encoding.t (tzresult a).
Definition ok {a trace : Set} (x : a) : Pervasives.result a trace :=
Pervasives.Ok x.
Definition op_gtgtquestion {a b trace : Set}
(x : Pervasives.result a trace) (f : a → Pervasives.result b trace) :
Pervasives.result b trace :=
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error trace ⇒ Pervasives.Error trace
end.
Definition _return {a trace : Set} (x : a) :
Pervasives.result a trace :=
ok x.
Definition op_gtgteqquestion {a b trace : Set}
(x : Pervasives.result a trace)
(f : a → Pervasives.result b trace) :
Pervasives.result b trace :=
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error trace ⇒ Pervasives.Error trace
end.
Module Notations.
Notation "M? X" := (tzresult X) (at level 20).
Notation "return? X" := (ok X) (at level 20).
Notation "'let?' x ':=' X 'in' Y" :=
(op_gtgtquestion X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'let?' ' x ':=' X 'in' Y" :=
(op_gtgtquestion X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
End Notations.
Import Notations.
Definition return_unit {trace : Set} : Pervasives.result unit trace :=
return? tt.
Definition return_none {a trace : Set} :
Pervasives.result (option a) trace :=
return? None.
Definition return_some {a trace : Set} (x : a) :
Pervasives.result (option a) trace :=
return? (Some x).
Definition return_nil {a trace : Set} :
Pervasives.result (list a) trace :=
return? [].
Definition return_true {trace : Set} :
Pervasives.result bool trace :=
return? true.
Definition return_false {trace : Set} :
Pervasives.result bool trace :=
return? false.
Definition error_value {a err : Set} (e : err) :
Pervasives.result a (trace err) :=
Pervasives.Error [e].
Definition trace_of_error {err : Set} (e : err) : trace err :=
[e].
Definition fail {a err : Set} (e : err) :
Pervasives.result a (trace err) :=
error_value e.
Definition op_gtgteq {a b : Set} (x : a) (f : a → b) : b :=
f x.
Definition op_gtpipeeq {a b : Set} (x : a) (f : a → b) : b :=
f x.
Definition op_gtpipequestion {a b trace : Set}
(x : Pervasives.result a trace) (f : a → b) : Pervasives.result b trace :=
let? x := x in
return? (f x).
Definition op_gtpipeeqquestion {a b trace : Set}
(x : Pervasives.result a trace) (f : a → b) :
Pervasives.result b trace :=
let? x := x in
return? (f x).
Definition op_gtgtquestioneq {a b trace : Set}
(x : Pervasives.result a trace) (f : a → Pervasives.result b trace) :
Pervasives.result b trace :=
let? x := x in
f x.
Definition op_gtpipequestioneq {a b trace : Set}
(x : Pervasives.result a trace) (f : a → b) :
Pervasives.result b trace :=
let? x := x in
let y := f x in
return? y.
Definition record_trace {a err : Set}
(e : err) (x : Pervasives.result a (trace err)) :
Pervasives.result a (trace err) :=
match x with
| Pervasives.Ok _ ⇒ x
| Pervasives.Error trace ⇒ Pervasives.Error (e :: trace)
end.
Definition trace_value {b err : Set}
(e : err) (x : Pervasives.result b (trace err)) :
Pervasives.result b (trace err) := record_trace e x.
Definition record_trace_eval {a err : Set}
(mk_err : unit → err) (x : Pervasives.result a (trace err))
: Pervasives.result a (trace err) :=
match x with
| Pervasives.Ok _ ⇒ x
| Pervasives.Error trace ⇒
let e := mk_err tt in
Pervasives.Error (e :: trace)
end.
Definition trace_eval {b err : Set}
(mk_err : unit → err) (x : Pervasives.result b (trace err))
: Pervasives.result b (trace err) :=
match x with
| Pervasives.Ok _ ⇒ x
| Pervasives.Error trace ⇒
let e := mk_err tt in
Pervasives.Error (e :: trace)
end.
Definition error_unless {err : Set}
(cond : bool) (e : err) : Pervasives.result unit (trace err) :=
if cond then
return? tt
else
error_value e.
Definition error_when {err : Set}
(cond : bool) (e : err) : Pervasives.result unit (trace err) :=
if cond then
error_value e
else
return? tt.
Definition fail_unless {err : Set}
(cond : bool) (e : err) : Pervasives.result unit (trace err) :=
if cond then
return? tt
else
fail e.
Definition fail_when {err : Set}
(cond : bool) (e : err) : Pervasives.result unit (trace err) :=
if cond then
fail e
else
return? tt.
Definition unless {trace : Set}
(cond : bool) (f : unit → Pervasives.result unit trace) :
Pervasives.result unit trace :=
if cond then
return? tt
else
f tt.
Definition when_ {trace : Set}
(cond : bool) (f : unit → Pervasives.result unit trace) :
Pervasives.result unit trace :=
if cond then
f tt
else
return? tt.
Parameter dont_wait : ∀ {trace : Set},
(extensible_type → unit) → (trace → unit) →
(unit → Pervasives.result unit trace) → unit.
Parameter catch : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → tzresult a.
Parameter catch_f : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) →
(extensible_type → _error) → tzresult a.
Parameter catch_s : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → tzresult a.
Parameter join_e : ∀ {err : Set},
list (Pervasives.result unit (trace err)) →
Pervasives.result unit (trace err).
Parameter all_e : ∀ {a err : Set},
list (Pervasives.result a (trace err)) →
Pervasives.result (list a) (trace err).
Parameter both_e : ∀ {a b err : Set},
Pervasives.result a (trace err) → Pervasives.result b (trace err) →
Pervasives.result (a × b) (trace err).
Parameter shell_tztrace : Set.
Definition shell_tzresult (a : Set) : Set :=
Pervasives.result a shell_tztrace.
Module Lwt_syntax.
Parameter _return : ∀ {a : Set}, a → a.
Parameter return_none : ∀ {A : Set}, option A.
Parameter return_nil : ∀ {A : Set}, list A.
Parameter return_true : bool.
Parameter return_false : bool.
Parameter return_some : ∀ {a : Set}, a → option a.
Parameter return_ok : ∀ {B a : Set}, a → Pervasives.result a B.
Parameter return_error : ∀ {B e : Set}, e → Pervasives.result B e.
Parameter return_ok_unit : ∀ {e : Set}, Pervasives.result unit e.
Parameter return_ok_true : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_ok_false : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_ok_none : ∀ {a e : Set},
Pervasives.result (option a) e.
Parameter return_ok_nil : ∀ {a e : Set}, Pervasives.result (list a) e.
Parameter op_letstar : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_andstar : ∀ {a b : Set}, a → b → a × b.
Parameter op_letplus : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_andplus : ∀ {a b : Set}, a → b → a × b.
Parameter join : list unit → unit.
Parameter all : ∀ {a : Set}, list a → list a.
Parameter both : ∀ {a b : Set}, a → b → a × b.
End Lwt_syntax.
Module Option_syntax.
Definition _return {a : Set} (x : a) : option a :=
Some x.
Definition fail {a : Set} : option a :=
None.
Definition return_unit : option unit :=
Some tt.
Definition return_nil {a : Set} : option (list a) :=
Some [].
Definition return_true : option bool :=
Some true.
Definition return_false : option bool :=
Some false.
Definition op_letstar {a b : Set}
(x : option a) (f : a → option b) : option b :=
match x with
| Some x ⇒ f x
| None ⇒ None
end.
Definition op_andstar {a b : Set}
(x : option a) (y : option b) : option (a × b) :=
match x, y with
| Some x, Some y ⇒ Some (x, y)
| _, _ ⇒ None
end.
Definition op_letplus {a b : Set} (x : option a) (f : a → b) :
option b :=
match x with
| Some x ⇒ Some (f x)
| None ⇒ None
end.
Definition op_andplus := @op_andstar.
Arguments op_andplus {_ _}.
Definition both := @op_andstar.
Arguments op_andplus {_ _}.
End Option_syntax.
Module Result_syntax.
Definition _return := @ok.
Arguments _return {_ _}.
Definition return_unit {e : Set} : Pervasives.result unit e :=
return? tt.
Definition return_none {a e : Set} : Pervasives.result (option a) e :=
return? None.
Definition return_some {a e : Set} (x : a) : Pervasives.result (option a) e :=
return? (Some x).
Definition return_nil {a e : Set} : Pervasives.result (list a) e :=
return? [].
Definition return_true {e : Set} : Pervasives.result bool e :=
return? true.
Definition return_false {e : Set} : Pervasives.result bool e :=
return? false.
Definition fail {a e : Set} (err : e) : Pervasives.result a e :=
Pervasives.Error err.
Definition op_letstar := @op_gtgtquestion.
Arguments op_letstar {_ _ _}.
Definition op_letplus {a b e : Set}
(x : Pervasives.result a e) (f : a → b) : Pervasives.result b e :=
let? x := x in
return? (f x).
Parameter join : ∀ {e : Set},
list (Pervasives.result unit e) → Pervasives.result unit (list e).
Parameter all : ∀ {a e : Set},
list (Pervasives.result a e) → Pervasives.result (list a) (list e).
Definition both {a b e : Set}
(x : Pervasives.result a e) (y : Pervasives.result b e) :
Pervasives.result (a × b) (list e) :=
match x, y with
| Pervasives.Ok x, Pervasives.Ok y ⇒ return? (x, y)
| Pervasives.Error err_x, Pervasives.Ok _ ⇒ Pervasives.Error [err_x]
| Pervasives.Ok _, Pervasives.Error err_y ⇒ Pervasives.Error [err_y]
| Pervasives.Error err_x, Pervasives.Error err_y ⇒
Pervasives.Error [err_x; err_y]
end.
End Result_syntax.
Module Lwt_result_syntax.
Definition _return {a e : Set} (arg : a) : Pervasives.result a e :=
ok arg.
Definition return_unit {e : Set} : Pervasives.result unit e :=
return? tt.
Definition return_none {a e : Set} : Pervasives.result (option a) e :=
return? None.
Definition return_some {a e : Set} (x : a) : Pervasives.result (option a) e :=
return? (Some x).
Definition return_nil {a e : Set} : Pervasives.result (list a) e :=
return? [].
Definition return_true {e : Set} : Pervasives.result bool e :=
return? true.
Definition return_false {e : Set} : Pervasives.result bool e :=
return? false.
Definition fail {a e : Set} (err : e) : Pervasives.result a e :=
Pervasives.Error err.
Definition op_letstar {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in f x.
Definition op_letplus {a b e : Set}
(x : Pervasives.result a e) (f : a → b) : Pervasives.result b e :=
let? x := x in return? (f x).
Definition lwt_map_error {a e e' : Set}
(f : e → e') (x : Pervasives.result a e) : Pervasives.result a e' :=
match x with
| Pervasives.Ok x ⇒ Pervasives.Ok x
| Pervasives.Error err ⇒ Pervasives.Error (f err)
end.
Definition op_letstarexclamation {a b : Set} (x : a) (f : a → b) : b :=
f x.
Definition op_letstarquestion {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in f x.
Parameter join : ∀ {e : Set},
list (Pervasives.result unit e) → Pervasives.result unit (list e).
Parameter all : ∀ {a e : Set},
list (Pervasives.result a e) → Pervasives.result (list a) (list e).
Definition both := @Result_syntax.both.
Arguments both {_ _ _}.
End Lwt_result_syntax.
Module Lwt_option_syntax.
Definition _return {a : Set} (x : a) : option a :=
Some x.
Definition return_unit : option unit :=
Some tt.
Definition return_nil {a : Set} : option (list a) :=
Some [].
Definition return_true : option bool :=
Some true.
Definition return_false : option bool :=
Some false.
Definition fail {a : Set} : option a :=
None.
Definition op_letstar {a b : Set}
(x : option a) (f : a → option b) : option b :=
match x with
| Some x ⇒ f x
| None ⇒ None
end.
Definition op_andstar {a b : Set}
(x : option a) (y : option b) : option (a × b) :=
match x, y with
| Some x, Some y ⇒ Some (x, y)
| _, _ ⇒ None
end.
Definition op_letplus {a b : Set} (x : option a) (f : a → b) : option b :=
match x with
| Some x ⇒ Some (f x)
| None ⇒ None
end.
Definition op_andplus := @op_andstar.
Arguments op_andplus {_ _}.
Definition op_letstarexclamation {a b : Set} (x : a) (f : a → b) : b :=
f x.
Definition op_letstarquestion := @op_letstar.
Arguments op_letstarquestion {_ _}.
Definition both := @op_andstar.
Arguments both {_ _}.
End Lwt_option_syntax.
Module Tzresult_syntax.
Definition _return {_error a : Set} (x : a) : Pervasives.result a _error :=
return? x.
Definition return_unit {_error : Set} : Pervasives.result unit _error :=
return? tt.
Definition return_none {_error a : Set} :
Pervasives.result (option a) _error :=
return? None.
Definition return_some {_error a : Set}
(x : a) : Pervasives.result (option a) _error :=
return? (Some x).
Definition return_nil {_error a : Set} : Pervasives.result (list a) _error :=
return? [].
Definition return_true {_error : Set} : Pervasives.result bool _error :=
return? true.
Definition return_false {_error : Set} : Pervasives.result bool _error :=
return? false.
Definition fail {_error a : Set}
(err : _error) : Pervasives.result a (trace _error) :=
Pervasives.Error [err].
Definition op_letstar {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in f x.
Parameter op_andstar : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Definition op_letplus {a b e : Set}
(x : Pervasives.result a e) (f : a → b) : Pervasives.result b e :=
let? x := x in return? f x.
Parameter op_andplus : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter join : ∀ {_error : Set},
list (Pervasives.result unit (trace _error)) →
Pervasives.result unit (trace _error).
Parameter all : ∀ {_error a : Set},
list (Pervasives.result a (trace _error)) →
Pervasives.result (list a) (trace _error).
Parameter both : ∀ {_error a b : Set},
Pervasives.result a (trace _error) →
Pervasives.result b (trace _error) →
Pervasives.result (a × b) (trace _error).
End Tzresult_syntax.
Module Lwt_tzresult_syntax.
Definition _return {_error a : Set} (x : a) : Pervasives.result a _error :=
return? x.
Definition return_unit {_error : Set} : Pervasives.result unit _error :=
return? tt.
Definition return_none {_error a : Set} :
Pervasives.result (option a) _error :=
return? None.
Definition return_some {_error a : Set}
(x : a) : Pervasives.result (option a) _error :=
return? (Some x).
Definition return_nil {_error a : Set} : Pervasives.result (list a) _error :=
return? [].
Definition return_true {_error : Set} : Pervasives.result bool _error :=
return? true.
Definition return_false {_error : Set} : Pervasives.result bool _error :=
return? false.
Definition fail {_error a : Set} (err : _error) :
Pervasives.result a (trace _error) :=
Pervasives.Error [err].
Definition op_letstar {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in f x.
Parameter op_andstar : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Definition op_letplus {a b e : Set}
(x : Pervasives.result a e) (f : a → b) : Pervasives.result b e :=
let? x := x in return? (f x).
Parameter op_andplus : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Definition op_letstarexclamation {a b : Set}
(x : a) (f : a → b) : b :=
f x.
Definition op_letstarquestion {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in
f x.
Parameter join : ∀ {_error : Set},
list (Pervasives.result unit (trace _error)) →
Pervasives.result unit (trace _error).
Parameter all : ∀ {_error a : Set},
list (Pervasives.result a (trace _error)) →
Pervasives.result (list a) (trace _error).
Parameter both : ∀ {_error a b : Set},
Pervasives.result a (trace _error) →
Pervasives.result b (trace _error) →
Pervasives.result (a × b) (trace _error).
End Lwt_tzresult_syntax.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Inductive error_category : Set :=
| Outdated : error_category
| Permanent : error_category
| Temporary : error_category
| Branch : error_category.
Definition _error : Set := extensible_type.
Parameter error_encoding : Data_encoding.t _error.
Parameter pp : Format.formatter → _error → unit.
Parameter register_error_kind : ∀ {err : Set},
error_category → string → string → string →
option (Format.formatter → err → unit) → Data_encoding.t err →
(_error → option err) → (err → _error) → unit.
Parameter json_of_error : _error → Data_encoding.json.
Parameter error_of_json : Data_encoding.json → _error.
Module error_info.
Record record : Set := Build {
category : error_category;
id : string;
title : string;
description : string;
schema : Data_encoding.json_schema }.
Definition with_category category (r : record) :=
Build category r.(id) r.(title) r.(description) r.(schema).
Definition with_id id (r : record) :=
Build r.(category) id r.(title) r.(description) r.(schema).
Definition with_title title (r : record) :=
Build r.(category) r.(id) title r.(description) r.(schema).
Definition with_description description (r : record) :=
Build r.(category) r.(id) r.(title) description r.(schema).
Definition with_schema schema (r : record) :=
Build r.(category) r.(id) r.(title) r.(description) schema.
End error_info.
Definition error_info := error_info.record.
Parameter pp_info : Format.formatter → error_info → unit.
Parameter get_registered_errors : unit → list error_info.
Definition trace (err : Set) : Set := list err.
Definition tzresult (a : Set) : Set := Pervasives.result a (trace _error).
Parameter make_trace_encoding : ∀ {_error : Set},
Data_encoding.t _error → Data_encoding.t (trace _error).
Parameter trace_encoding : Data_encoding.t (trace _error).
Parameter pp_trace : Format.formatter → trace _error → unit.
Parameter result_encoding : ∀ {a : Set},
Data_encoding.t a → Data_encoding.t (tzresult a).
Definition ok {a trace : Set} (x : a) : Pervasives.result a trace :=
Pervasives.Ok x.
Definition op_gtgtquestion {a b trace : Set}
(x : Pervasives.result a trace) (f : a → Pervasives.result b trace) :
Pervasives.result b trace :=
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error trace ⇒ Pervasives.Error trace
end.
Definition _return {a trace : Set} (x : a) :
Pervasives.result a trace :=
ok x.
Definition op_gtgteqquestion {a b trace : Set}
(x : Pervasives.result a trace)
(f : a → Pervasives.result b trace) :
Pervasives.result b trace :=
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error trace ⇒ Pervasives.Error trace
end.
Module Notations.
Notation "M? X" := (tzresult X) (at level 20).
Notation "return? X" := (ok X) (at level 20).
Notation "'let?' x ':=' X 'in' Y" :=
(op_gtgtquestion X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'let?' ' x ':=' X 'in' Y" :=
(op_gtgtquestion X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
End Notations.
Import Notations.
Definition return_unit {trace : Set} : Pervasives.result unit trace :=
return? tt.
Definition return_none {a trace : Set} :
Pervasives.result (option a) trace :=
return? None.
Definition return_some {a trace : Set} (x : a) :
Pervasives.result (option a) trace :=
return? (Some x).
Definition return_nil {a trace : Set} :
Pervasives.result (list a) trace :=
return? [].
Definition return_true {trace : Set} :
Pervasives.result bool trace :=
return? true.
Definition return_false {trace : Set} :
Pervasives.result bool trace :=
return? false.
Definition error_value {a err : Set} (e : err) :
Pervasives.result a (trace err) :=
Pervasives.Error [e].
Definition trace_of_error {err : Set} (e : err) : trace err :=
[e].
Definition fail {a err : Set} (e : err) :
Pervasives.result a (trace err) :=
error_value e.
Definition op_gtgteq {a b : Set} (x : a) (f : a → b) : b :=
f x.
Definition op_gtpipeeq {a b : Set} (x : a) (f : a → b) : b :=
f x.
Definition op_gtpipequestion {a b trace : Set}
(x : Pervasives.result a trace) (f : a → b) : Pervasives.result b trace :=
let? x := x in
return? (f x).
Definition op_gtpipeeqquestion {a b trace : Set}
(x : Pervasives.result a trace) (f : a → b) :
Pervasives.result b trace :=
let? x := x in
return? (f x).
Definition op_gtgtquestioneq {a b trace : Set}
(x : Pervasives.result a trace) (f : a → Pervasives.result b trace) :
Pervasives.result b trace :=
let? x := x in
f x.
Definition op_gtpipequestioneq {a b trace : Set}
(x : Pervasives.result a trace) (f : a → b) :
Pervasives.result b trace :=
let? x := x in
let y := f x in
return? y.
Definition record_trace {a err : Set}
(e : err) (x : Pervasives.result a (trace err)) :
Pervasives.result a (trace err) :=
match x with
| Pervasives.Ok _ ⇒ x
| Pervasives.Error trace ⇒ Pervasives.Error (e :: trace)
end.
Definition trace_value {b err : Set}
(e : err) (x : Pervasives.result b (trace err)) :
Pervasives.result b (trace err) := record_trace e x.
Definition record_trace_eval {a err : Set}
(mk_err : unit → err) (x : Pervasives.result a (trace err))
: Pervasives.result a (trace err) :=
match x with
| Pervasives.Ok _ ⇒ x
| Pervasives.Error trace ⇒
let e := mk_err tt in
Pervasives.Error (e :: trace)
end.
Definition trace_eval {b err : Set}
(mk_err : unit → err) (x : Pervasives.result b (trace err))
: Pervasives.result b (trace err) :=
match x with
| Pervasives.Ok _ ⇒ x
| Pervasives.Error trace ⇒
let e := mk_err tt in
Pervasives.Error (e :: trace)
end.
Definition error_unless {err : Set}
(cond : bool) (e : err) : Pervasives.result unit (trace err) :=
if cond then
return? tt
else
error_value e.
Definition error_when {err : Set}
(cond : bool) (e : err) : Pervasives.result unit (trace err) :=
if cond then
error_value e
else
return? tt.
Definition fail_unless {err : Set}
(cond : bool) (e : err) : Pervasives.result unit (trace err) :=
if cond then
return? tt
else
fail e.
Definition fail_when {err : Set}
(cond : bool) (e : err) : Pervasives.result unit (trace err) :=
if cond then
fail e
else
return? tt.
Definition unless {trace : Set}
(cond : bool) (f : unit → Pervasives.result unit trace) :
Pervasives.result unit trace :=
if cond then
return? tt
else
f tt.
Definition when_ {trace : Set}
(cond : bool) (f : unit → Pervasives.result unit trace) :
Pervasives.result unit trace :=
if cond then
f tt
else
return? tt.
Parameter dont_wait : ∀ {trace : Set},
(extensible_type → unit) → (trace → unit) →
(unit → Pervasives.result unit trace) → unit.
Parameter catch : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → tzresult a.
Parameter catch_f : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) →
(extensible_type → _error) → tzresult a.
Parameter catch_s : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → tzresult a.
Parameter join_e : ∀ {err : Set},
list (Pervasives.result unit (trace err)) →
Pervasives.result unit (trace err).
Parameter all_e : ∀ {a err : Set},
list (Pervasives.result a (trace err)) →
Pervasives.result (list a) (trace err).
Parameter both_e : ∀ {a b err : Set},
Pervasives.result a (trace err) → Pervasives.result b (trace err) →
Pervasives.result (a × b) (trace err).
Parameter shell_tztrace : Set.
Definition shell_tzresult (a : Set) : Set :=
Pervasives.result a shell_tztrace.
Module Lwt_syntax.
Parameter _return : ∀ {a : Set}, a → a.
Parameter return_none : ∀ {A : Set}, option A.
Parameter return_nil : ∀ {A : Set}, list A.
Parameter return_true : bool.
Parameter return_false : bool.
Parameter return_some : ∀ {a : Set}, a → option a.
Parameter return_ok : ∀ {B a : Set}, a → Pervasives.result a B.
Parameter return_error : ∀ {B e : Set}, e → Pervasives.result B e.
Parameter return_ok_unit : ∀ {e : Set}, Pervasives.result unit e.
Parameter return_ok_true : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_ok_false : ∀ {e : Set}, Pervasives.result bool e.
Parameter return_ok_none : ∀ {a e : Set},
Pervasives.result (option a) e.
Parameter return_ok_nil : ∀ {a e : Set}, Pervasives.result (list a) e.
Parameter op_letstar : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_andstar : ∀ {a b : Set}, a → b → a × b.
Parameter op_letplus : ∀ {a b : Set}, a → (a → b) → b.
Parameter op_andplus : ∀ {a b : Set}, a → b → a × b.
Parameter join : list unit → unit.
Parameter all : ∀ {a : Set}, list a → list a.
Parameter both : ∀ {a b : Set}, a → b → a × b.
End Lwt_syntax.
Module Option_syntax.
Definition _return {a : Set} (x : a) : option a :=
Some x.
Definition fail {a : Set} : option a :=
None.
Definition return_unit : option unit :=
Some tt.
Definition return_nil {a : Set} : option (list a) :=
Some [].
Definition return_true : option bool :=
Some true.
Definition return_false : option bool :=
Some false.
Definition op_letstar {a b : Set}
(x : option a) (f : a → option b) : option b :=
match x with
| Some x ⇒ f x
| None ⇒ None
end.
Definition op_andstar {a b : Set}
(x : option a) (y : option b) : option (a × b) :=
match x, y with
| Some x, Some y ⇒ Some (x, y)
| _, _ ⇒ None
end.
Definition op_letplus {a b : Set} (x : option a) (f : a → b) :
option b :=
match x with
| Some x ⇒ Some (f x)
| None ⇒ None
end.
Definition op_andplus := @op_andstar.
Arguments op_andplus {_ _}.
Definition both := @op_andstar.
Arguments op_andplus {_ _}.
End Option_syntax.
Module Result_syntax.
Definition _return := @ok.
Arguments _return {_ _}.
Definition return_unit {e : Set} : Pervasives.result unit e :=
return? tt.
Definition return_none {a e : Set} : Pervasives.result (option a) e :=
return? None.
Definition return_some {a e : Set} (x : a) : Pervasives.result (option a) e :=
return? (Some x).
Definition return_nil {a e : Set} : Pervasives.result (list a) e :=
return? [].
Definition return_true {e : Set} : Pervasives.result bool e :=
return? true.
Definition return_false {e : Set} : Pervasives.result bool e :=
return? false.
Definition fail {a e : Set} (err : e) : Pervasives.result a e :=
Pervasives.Error err.
Definition op_letstar := @op_gtgtquestion.
Arguments op_letstar {_ _ _}.
Definition op_letplus {a b e : Set}
(x : Pervasives.result a e) (f : a → b) : Pervasives.result b e :=
let? x := x in
return? (f x).
Parameter join : ∀ {e : Set},
list (Pervasives.result unit e) → Pervasives.result unit (list e).
Parameter all : ∀ {a e : Set},
list (Pervasives.result a e) → Pervasives.result (list a) (list e).
Definition both {a b e : Set}
(x : Pervasives.result a e) (y : Pervasives.result b e) :
Pervasives.result (a × b) (list e) :=
match x, y with
| Pervasives.Ok x, Pervasives.Ok y ⇒ return? (x, y)
| Pervasives.Error err_x, Pervasives.Ok _ ⇒ Pervasives.Error [err_x]
| Pervasives.Ok _, Pervasives.Error err_y ⇒ Pervasives.Error [err_y]
| Pervasives.Error err_x, Pervasives.Error err_y ⇒
Pervasives.Error [err_x; err_y]
end.
End Result_syntax.
Module Lwt_result_syntax.
Definition _return {a e : Set} (arg : a) : Pervasives.result a e :=
ok arg.
Definition return_unit {e : Set} : Pervasives.result unit e :=
return? tt.
Definition return_none {a e : Set} : Pervasives.result (option a) e :=
return? None.
Definition return_some {a e : Set} (x : a) : Pervasives.result (option a) e :=
return? (Some x).
Definition return_nil {a e : Set} : Pervasives.result (list a) e :=
return? [].
Definition return_true {e : Set} : Pervasives.result bool e :=
return? true.
Definition return_false {e : Set} : Pervasives.result bool e :=
return? false.
Definition fail {a e : Set} (err : e) : Pervasives.result a e :=
Pervasives.Error err.
Definition op_letstar {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in f x.
Definition op_letplus {a b e : Set}
(x : Pervasives.result a e) (f : a → b) : Pervasives.result b e :=
let? x := x in return? (f x).
Definition lwt_map_error {a e e' : Set}
(f : e → e') (x : Pervasives.result a e) : Pervasives.result a e' :=
match x with
| Pervasives.Ok x ⇒ Pervasives.Ok x
| Pervasives.Error err ⇒ Pervasives.Error (f err)
end.
Definition op_letstarexclamation {a b : Set} (x : a) (f : a → b) : b :=
f x.
Definition op_letstarquestion {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in f x.
Parameter join : ∀ {e : Set},
list (Pervasives.result unit e) → Pervasives.result unit (list e).
Parameter all : ∀ {a e : Set},
list (Pervasives.result a e) → Pervasives.result (list a) (list e).
Definition both := @Result_syntax.both.
Arguments both {_ _ _}.
End Lwt_result_syntax.
Module Lwt_option_syntax.
Definition _return {a : Set} (x : a) : option a :=
Some x.
Definition return_unit : option unit :=
Some tt.
Definition return_nil {a : Set} : option (list a) :=
Some [].
Definition return_true : option bool :=
Some true.
Definition return_false : option bool :=
Some false.
Definition fail {a : Set} : option a :=
None.
Definition op_letstar {a b : Set}
(x : option a) (f : a → option b) : option b :=
match x with
| Some x ⇒ f x
| None ⇒ None
end.
Definition op_andstar {a b : Set}
(x : option a) (y : option b) : option (a × b) :=
match x, y with
| Some x, Some y ⇒ Some (x, y)
| _, _ ⇒ None
end.
Definition op_letplus {a b : Set} (x : option a) (f : a → b) : option b :=
match x with
| Some x ⇒ Some (f x)
| None ⇒ None
end.
Definition op_andplus := @op_andstar.
Arguments op_andplus {_ _}.
Definition op_letstarexclamation {a b : Set} (x : a) (f : a → b) : b :=
f x.
Definition op_letstarquestion := @op_letstar.
Arguments op_letstarquestion {_ _}.
Definition both := @op_andstar.
Arguments both {_ _}.
End Lwt_option_syntax.
Module Tzresult_syntax.
Definition _return {_error a : Set} (x : a) : Pervasives.result a _error :=
return? x.
Definition return_unit {_error : Set} : Pervasives.result unit _error :=
return? tt.
Definition return_none {_error a : Set} :
Pervasives.result (option a) _error :=
return? None.
Definition return_some {_error a : Set}
(x : a) : Pervasives.result (option a) _error :=
return? (Some x).
Definition return_nil {_error a : Set} : Pervasives.result (list a) _error :=
return? [].
Definition return_true {_error : Set} : Pervasives.result bool _error :=
return? true.
Definition return_false {_error : Set} : Pervasives.result bool _error :=
return? false.
Definition fail {_error a : Set}
(err : _error) : Pervasives.result a (trace _error) :=
Pervasives.Error [err].
Definition op_letstar {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in f x.
Parameter op_andstar : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Definition op_letplus {a b e : Set}
(x : Pervasives.result a e) (f : a → b) : Pervasives.result b e :=
let? x := x in return? f x.
Parameter op_andplus : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Parameter join : ∀ {_error : Set},
list (Pervasives.result unit (trace _error)) →
Pervasives.result unit (trace _error).
Parameter all : ∀ {_error a : Set},
list (Pervasives.result a (trace _error)) →
Pervasives.result (list a) (trace _error).
Parameter both : ∀ {_error a b : Set},
Pervasives.result a (trace _error) →
Pervasives.result b (trace _error) →
Pervasives.result (a × b) (trace _error).
End Tzresult_syntax.
Module Lwt_tzresult_syntax.
Definition _return {_error a : Set} (x : a) : Pervasives.result a _error :=
return? x.
Definition return_unit {_error : Set} : Pervasives.result unit _error :=
return? tt.
Definition return_none {_error a : Set} :
Pervasives.result (option a) _error :=
return? None.
Definition return_some {_error a : Set}
(x : a) : Pervasives.result (option a) _error :=
return? (Some x).
Definition return_nil {_error a : Set} : Pervasives.result (list a) _error :=
return? [].
Definition return_true {_error : Set} : Pervasives.result bool _error :=
return? true.
Definition return_false {_error : Set} : Pervasives.result bool _error :=
return? false.
Definition fail {_error a : Set} (err : _error) :
Pervasives.result a (trace _error) :=
Pervasives.Error [err].
Definition op_letstar {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in f x.
Parameter op_andstar : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Definition op_letplus {a b e : Set}
(x : Pervasives.result a e) (f : a → b) : Pervasives.result b e :=
let? x := x in return? (f x).
Parameter op_andplus : ∀ {a b e : Set},
Pervasives.result a (trace e) → Pervasives.result b (trace e) →
Pervasives.result (a × b) (trace e).
Definition op_letstarexclamation {a b : Set}
(x : a) (f : a → b) : b :=
f x.
Definition op_letstarquestion {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e) :
Pervasives.result b e :=
let? x := x in
f x.
Parameter join : ∀ {_error : Set},
list (Pervasives.result unit (trace _error)) →
Pervasives.result unit (trace _error).
Parameter all : ∀ {_error a : Set},
list (Pervasives.result a (trace _error)) →
Pervasives.result (list a) (trace _error).
Parameter both : ∀ {_error a b : Set},
Pervasives.result a (trace _error) →
Pervasives.result b (trace _error) →
Pervasives.result (a × b) (trace _error).
End Lwt_tzresult_syntax.