Skip to main content

🍃 Error_monad.v

Environment

Gitlab

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

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 tracePervasives.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 xf x
    | NoneNone
    end.

  Definition op_andstar {a b : Set}
    (x : option a) (y : option b) : option (a × b) :=
    match x, y with
    | Some x, Some ySome (x, y)
    | _, _None
    end.

  Definition op_letplus {a b : Set} (x : option a) (f : a b) :
    option b :=
    match x with
    | Some xSome (f x)
    | NoneNone
    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 yreturn? (x, y)
    | Pervasives.Error err_x, Pervasives.Ok _Pervasives.Error [err_x]
    | Pervasives.Ok _, Pervasives.Error err_yPervasives.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 xPervasives.Ok x
    | Pervasives.Error errPervasives.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 xf x
    | NoneNone
    end.

  Definition op_andstar {a b : Set}
    (x : option a) (y : option b) : option (a × b) :=
    match x, y with
    | Some x, Some ySome (x, y)
    | _, _None
    end.

  Definition op_letplus {a b : Set} (x : option a) (f : a b) : option b :=
    match x with
    | Some xSome (f x)
    | NoneNone
    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.