Skip to main content

πŸƒΒ Error_monad.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.

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 tzfail {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
    tzfail e.

Definition fail_when {err : Set}
  (cond : bool) (e : err) : Pervasives.result unit (trace err) :=
  if cond then
    tzfail 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).

Definition shell_tztrace : Set := V0.Error_monad.shell_tztrace.

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.

  Definition tzfail {_error a : Set} (x : _error)
    : Pervasives.result a (trace _error) :=
    error_value x.

  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_andplus : βˆ€ {a b e : Set},
    Pervasives.result a (trace e) β†’ Pervasives.result b (trace e) β†’
    Pervasives.result (a Γ— b) (trace e).

  Parameter tzjoin : βˆ€ {_error : Set},
    list (Pervasives.result unit (trace _error)) β†’
    Pervasives.result unit (trace _error).

  Parameter tzall : βˆ€ {_error a : Set},
    list (Pervasives.result a (trace _error)) β†’
    Pervasives.result (list a) (trace _error).

  Parameter tzboth : βˆ€ {_error a b : Set},
    Pervasives.result a (trace _error) β†’
    Pervasives.result b (trace _error) β†’
    Pervasives.result (a Γ— b) (trace _error).
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 {_ _ _}.

  Definition tzfail {_error a : Set} (x : _error)
    : Pervasives.result a (trace _error) :=
    error_value x.

  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_andplus : βˆ€ {a b e : Set},
    Pervasives.result a (trace e) β†’ Pervasives.result b (trace e) β†’
    Pervasives.result (a Γ— b) (trace e).

  Parameter tzjoin : βˆ€ {_error : Set},
    list (Pervasives.result unit (trace _error)) β†’
    Pervasives.result unit (trace _error).

  Parameter tzall : βˆ€ {_error a : Set},
    list (Pervasives.result a (trace _error)) β†’
    Pervasives.result (list a) (trace _error).

  Parameter tzboth : βˆ€ {_error a b : Set},
    Pervasives.result a (trace _error) β†’
    Pervasives.result b (trace _error) β†’
    Pervasives.result (a Γ— b) (trace _error).
End Lwt_result_syntax.

Module Lwt_option_syntax.
  Parameter _return : βˆ€ {a : Set}, a β†’ option a.

  Parameter return_unit : option unit.

  Parameter return_nil : βˆ€ {a : Set}, option (list a).

  Parameter return_true : option bool.

  Parameter return_false : option bool.

  Parameter fail : βˆ€ {a : Set}, option a.

  Parameter op_letstar : βˆ€ {a b : Set},
    option a β†’ (a β†’ option b) β†’ option b.

  Parameter op_andstar : βˆ€ {a b : Set},
    option a β†’ option b β†’ option (a Γ— b).

  Parameter op_letplus : βˆ€ {a b : Set}, option a β†’ (a β†’ b) β†’ option b.

  Parameter op_andplus : βˆ€ {a b : Set},
    option a β†’ option b β†’ option (a Γ— b).

  Parameter op_letstarexclamation : βˆ€ {a b : Set}, a β†’ (a β†’ b) β†’ b.

  Parameter op_letstarquestion : βˆ€ {a b : Set},
    option a β†’ (a β†’ option b) β†’ option b.

  Parameter both : βˆ€ {a b : Set}, option a β†’ option b β†’ option (a Γ— b).
End Lwt_option_syntax.