Skip to main content

🍃 Result.v

Environment

Gitlab , OCaml

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

Require Proto_alpha.Environment.Pervasives.
Require Proto_alpha.Environment.Seq.

Definition t (a e : Set) : Set := Pervasives.result a e.

Definition ok {a e : Set} (v : a) : Pervasives.result a e :=
  Pervasives.Ok v.

Definition bind {a b e : Set}
  (e1 : Pervasives.result a e) (e2 : a Pervasives.result b e)
  : Pervasives.result b e :=
  match e1 with
  | Pervasives.Ok v1e2 v1
  | Pervasives.Error e1Pervasives.Error e1
  end.

Parameter ok_s : {a e : Set}, a Pervasives.result a e.

Parameter error_value : {a e : Set}, e Pervasives.result a e.

Parameter error_s : {a e : Set}, e Pervasives.result a e.

Definition _return {a e : Set} (v : a) : Pervasives.result a e :=
  Pervasives.Ok v.

Definition return_unit {trace : Set} : Pervasives.result unit trace :=
  ok tt.

Definition return_none {a trace : Set} : Pervasives.result (option a) trace :=
  ok None.

Definition return_some {a trace : Set} (x : a) :
  Pervasives.result (option a) trace :=
  ok (Some x).

Definition return_nil {a trace : Set} : Pervasives.result (list a) trace :=
  ok [].

Definition return_true {trace : Set} : Pervasives.result bool trace :=
  ok true.

Definition return_false {trace : Set} : Pervasives.result bool trace :=
  ok false.

Definition value_value {a e : Set} (r : Pervasives.result a e) (default : a)
  : a :=
  match r with
  | Pervasives.Ok vv
  | Pervasives.Error _default
  end.

Definition value_f {a e : Set} (r : Pervasives.result a e) (default : unit a)
  : a :=
  match r with
  | Pervasives.Ok vv
  | Pervasives.Error _default tt
  end.

Parameter bind_s : {a b e : Set},
  Pervasives.result a e (a Pervasives.result b e)
  Pervasives.result b e.

Parameter bind_error : {a e f : Set},
  Pervasives.result a e (e Pervasives.result a f)
  Pervasives.result a f.

Parameter bind_error_s : {a e f : Set},
  Pervasives.result a e (e Pervasives.result a f)
  Pervasives.result a f.

Parameter join : {a e : Set},
  Pervasives.result (Pervasives.result a e) e Pervasives.result a e.

Definition map {a b e : Set} (f : a b) (x : Pervasives.result a e) :
  Pervasives.result b e :=
  match x with
  | Pervasives.Ok vPervasives.Ok (f v)
  | Pervasives.Error errPervasives.Error err
  end.

Parameter map_e : {a b e : Set},
  (a Pervasives.result b e) Pervasives.result a e
  Pervasives.result b e.

Parameter map_s : {a b e : Set},
  (a b) Pervasives.result a e Pervasives.result b e.

Parameter map_es : {a b e : Set},
  (a Pervasives.result b e) Pervasives.result a e
  Pervasives.result b e.

Definition map_error {a e f : Set} (func : e f) (res : Pervasives.result a e) : Pervasives.result a f :=
  match res with
    Pervasives.Ok aPervasives.Ok a
  | Pervasives.Error ePervasives.Error (func e)
  end.

Parameter map_error_e : {a e f : Set},
  (e Pervasives.result a f) Pervasives.result a e
  Pervasives.result a f.

Parameter map_error_s : {a e f : Set},
  (e f) Pervasives.result a e Pervasives.result a f.

Parameter map_error_es : {a e f : Set},
  (e Pervasives.result a f) Pervasives.result a e
  Pervasives.result a f.

Parameter fold : {a c e : Set},
  (a c) (e c) Pervasives.result a e c.

Parameter iter : {a e : Set},
  (a unit) Pervasives.result a e unit.

Parameter iter_s : {a e : Set},
  (a unit) Pervasives.result a e unit.

Parameter iter_error : {a e : Set},
  (e unit) Pervasives.result a e unit.

Parameter iter_error_s : {a e : Set},
  (e unit) Pervasives.result a e unit.

Parameter is_ok : {a e : Set}, Pervasives.result a e bool.

Parameter is_error : {a e : Set}, Pervasives.result a e bool.

Parameter equal : {a e : Set},
  (a a bool) (e e bool) Pervasives.result a e
  Pervasives.result a e bool.

Parameter compare : {a e : Set},
  (a a int) (e e int) Pervasives.result a e
  Pervasives.result a e int.

Parameter to_option : {a e : Set}, Pervasives.result a e option a.

Parameter of_option : {a e : Set},
  e option a Pervasives.result a e.

Parameter to_list : {a e : Set}, Pervasives.result a e list a.

Parameter to_seq : {a e : Set},
  Pervasives.result a e Seq.t a.

Parameter catch : {a : Set},
  option (extensible_type bool) (unit a)
  Pervasives.result a extensible_type.

Parameter catch_f : {_error a : Set},
  option (extensible_type bool) (unit a)
  (extensible_type _error) Pervasives.result a _error.

Parameter catch_s : {a : Set},
  option (extensible_type bool) (unit a)
  Pervasives.result a extensible_type.