🍃 Error_monad.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.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].

Parameter trace_of_error : ∀ {err : Set}, err → trace err.

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) :=
  match x with
  | Pervasives.Ok _ ⇒ x
  | Pervasives.Error trace ⇒ Pervasives.Error (e :: trace)
  end.

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 Result_syntax.
  Definition _return := @ok.
  Arguments _return {_ _}.

  Parameter return_unit : ∀ {e : Set}, Pervasives.result unit e.

  Parameter return_none : ∀ {a e : Set}, Pervasives.result (option a) e.

  Parameter return_some : ∀ {a e : Set},
    a → Pervasives.result (option a) e.

  Parameter return_nil : ∀ {a e : Set}, Pervasives.result (list a) e.

  Parameter return_true : ∀ {e : Set}, Pervasives.result bool e.

  Parameter return_false : ∀ {e : Set}, Pervasives.result bool e.

  Parameter fail : ∀ {a e : Set}, e → Pervasives.result a e.

  Definition op_letstar := @op_gtgtquestion.
  Arguments op_letstar {_ _ _}.

  Parameter op_letplus : ∀ {a b e : Set},
    Pervasives.result a e → (a → b) → Pervasives.result b e.

  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).

  Parameter both : ∀ {a b e : Set},
    Pervasives.result a e → Pervasives.result b e →
    Pervasives.result (a × b) (list e).
End Result_syntax.

Module Lwt_result_syntax.
  Parameter _return : ∀ {a e : Set}, a → Pervasives.result a e.

  Parameter return_unit : ∀ {e : Set}, Pervasives.result unit e.

  Parameter return_none : ∀ {a e : Set}, Pervasives.result (option a) e.

  Parameter return_some : ∀ {a e : Set},
    a → Pervasives.result (option a) e.

  Parameter return_nil : ∀ {a e : Set}, Pervasives.result (list a) e.

  Parameter return_true : ∀ {e : Set}, Pervasives.result bool e.

  Parameter return_false : ∀ {e : Set}, Pervasives.result bool e.

  Parameter fail : ∀ {a e : Set}, e → Pervasives.result a e.

  Parameter op_letstar : ∀ {a b e : Set},
    Pervasives.result a e → (a → Pervasives.result b e) →
    Pervasives.result b e.

  Parameter op_letplus : ∀ {a b e : Set},
    Pervasives.result a e → (a → b) → Pervasives.result b e.

  Parameter lwt_map_error : ∀ {a e f : Set},
    (e → f) → Pervasives.result a e → Pervasives.result a f.

  Parameter op_letstarexclamation : ∀ {a b : Set}, a → (a → b) → b.

  Parameter op_letstarquestion : ∀ {a b e : Set},
    Pervasives.result a e → (a → Pervasives.result b e) →
    Pervasives.result b e.

  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).

  Parameter both : ∀ {a b e : Set},
    Pervasives.result a e → Pervasives.result b e →
    Pervasives.result (a × b) (list e).
End Lwt_result_syntax.

Module Tzresult_syntax.
  Parameter _return : ∀ {_error a : Set},
    a → Pervasives.result a _error.

  Parameter return_unit : ∀ {_error : Set},
    Pervasives.result unit _error.

  Parameter return_none : ∀ {_error a : Set},
    Pervasives.result (option a) _error.

  Parameter return_some : ∀ {_error a : Set},
    a → Pervasives.result (option a) _error.

  Parameter return_nil : ∀ {_error a : Set},
    Pervasives.result (list a) _error.

  Parameter return_true : ∀ {_error : Set},
    Pervasives.result bool _error.

  Parameter return_false : ∀ {_error : Set},
    Pervasives.result bool _error.

  Parameter fail : ∀ {_error a : Set},
    _error → Pervasives.result a (trace _error).

  Parameter op_letstar : ∀ {a b e : Set},
    Pervasives.result a e → (a → Pervasives.result b e) →
    Pervasives.result b e.

  Parameter op_andstar : ∀ {a b e : Set},
    Pervasives.result a (trace e) → Pervasives.result b (trace e) →
    Pervasives.result (a × b) (trace e).

  Parameter op_letplus : ∀ {a b e : Set},
    Pervasives.result a e → (a → b) → Pervasives.result b e.

  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.
  Parameter _return : ∀ {_error a : Set},
    a → Pervasives.result a _error.

  Parameter return_unit : ∀ {_error : Set},
    Pervasives.result unit _error.

  Parameter return_none : ∀ {_error a : Set},
    Pervasives.result (option a) _error.

  Parameter return_some : ∀ {_error a : Set},
    a → Pervasives.result (option a) _error.

  Parameter return_nil : ∀ {_error a : Set},
    Pervasives.result (list a) _error.

  Parameter return_true : ∀ {_error : Set},
    Pervasives.result bool _error.

  Parameter return_false : ∀ {_error : Set},
    Pervasives.result bool _error.

  Parameter fail : ∀ {_error a : Set},
    _error → Pervasives.result a (trace _error).

  Parameter op_letstar : ∀ {a b e : Set},
    Pervasives.result a e → (a → Pervasives.result b e) →
    Pervasives.result b e.

  Parameter op_andstar : ∀ {a b e : Set},
    Pervasives.result a (trace e) → Pervasives.result b (trace e) →
    Pervasives.result (a × b) (trace e).

  Parameter op_letplus : ∀ {a b e : Set},
    Pervasives.result a e → (a → b) → Pervasives.result b e.

  Parameter op_andplus : ∀ {a b e : Set},
    Pervasives.result a (trace e) → Pervasives.result b (trace e) →
    Pervasives.result (a × b) (trace e).

  Parameter op_letstarexclamation : ∀ {a b : Set}, a → (a → b) → b.

  Parameter op_letstarquestion : ∀ {a b e : Set},
    Pervasives.result a e → (a → Pervasives.result b e) →
    Pervasives.result b 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 Lwt_tzresult_syntax.