Skip to main content

🍃 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 xf x
  | Pervasives.Error tracePervasives.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 xf x
  | Pervasives.Error tracePervasives.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 xY))
    (at level 200, x name, X at level 100, Y at level 200).

  Notation "'let?' ' x ':=' X 'in' Y" :=
    (op_gtgtquestion X (fun xY))
    (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 tracePervasives.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 tracePervasives.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.