🍃 Result.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.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 v1 ⇒ e2 v1
| Pervasives.Error e1 ⇒ Pervasives.Error e1
end.
Definition ok_s {a e : Set} (v : a) : Pervasives.result a e :=
Pervasives.Ok v.
Definition error_value {a e : Set} (err : e) : Pervasives.result a e :=
Pervasives.Error err.
Definition error_s {a e : Set} (err : e) : Pervasives.result a e :=
Pervasives.Error err.
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 v ⇒ v
| Pervasives.Error _ ⇒ default
end.
Definition value_f {a e : Set} (r : Pervasives.result a e) (default : unit → a)
: a :=
match r with
| Pervasives.Ok v ⇒ v
| Pervasives.Error _ ⇒ default tt
end.
Definition bind_s {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e)
: Pervasives.result b e :=
match x with
| Pervasives.Ok v ⇒ f v
| Pervasives.Error err ⇒ Pervasives.Error err
end.
Definition bind_error {a e f : Set}
(x : Pervasives.result a e) (func : e → Pervasives.result a f)
: Pervasives.result a f :=
match x with
| Pervasives.Ok v ⇒ Pervasives.Ok v
| Pervasives.Error err ⇒ func err
end.
Definition bind_error_s {a e f : Set}
(x : Pervasives.result a e) (func : e → Pervasives.result a f)
: Pervasives.result a f :=
match x with
| Pervasives.Ok v ⇒ Pervasives.Ok v
| Pervasives.Error err ⇒ func err
end.
Definition join {a e : Set}
(rr : Pervasives.result (Pervasives.result a e) e)
: Pervasives.result a e :=
match rr with
| Pervasives.Error err ⇒ Pervasives.Error err
| Pervasives.Ok r ⇒ r
end.
Definition map {a b e : Set} (f : a → b) (x : Pervasives.result a e) :
Pervasives.result b e :=
match x with
| Pervasives.Ok v ⇒ Pervasives.Ok (f v)
| Pervasives.Error err ⇒ Pervasives.Error err
end.
Definition map_e {a b e : Set}
(f : a → Pervasives.result b e) (x : Pervasives.result a e)
: Pervasives.result b e :=
join (map f x).
Definition map_s : ∀ {a b e : Set},
(a → b) → Pervasives.result a e → Pervasives.result b e := @map.
Definition map_es : ∀ {a b e : Set},
(a → Pervasives.result b e) → Pervasives.result a e →
Pervasives.result b e := @map_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 a ⇒ Pervasives.Ok a
| Pervasives.Error e ⇒ Pervasives.Error (func e)
end.
Definition map_error_e {a e f : Set}
(func : e → Pervasives.result a f) (res : Pervasives.result a e)
: Pervasives.result a f :=
match res with
| Pervasives.Ok v ⇒ Pervasives.Ok v
| Pervasives.Error err ⇒ func err
end.
Definition map_error_s {a e f : Set}
(func : e → f) (res : Pervasives.result a e) : Pervasives.result a f :=
match res with
Pervasives.Ok a ⇒ Pervasives.Ok a
| Pervasives.Error e ⇒ Pervasives.Error (func e)
end.
Definition map_error_es {a e f : Set}
(func : e → Pervasives.result a f) (res : Pervasives.result a e)
: Pervasives.result a f :=
match res with
| Pervasives.Ok v ⇒ Pervasives.Ok v
| Pervasives.Error err ⇒ func err
end.
Definition fold {a c e : Set}
(f : a → c) (f' : e → c) (r : Pervasives.result a e) : c :=
match r with
| Pervasives.Ok v ⇒ f v
| Pervasives.Error err ⇒ f' err
end.
Definition iter {a e : Set}
(f : a → unit) (r : Pervasives.result a e) : unit := tt.
Definition iter_s {a e : Set}
(f : a → unit) (r : Pervasives.result a e) : unit := tt.
Definition iter_error {a e : Set}
(f : e → unit) (r : Pervasives.result a e) : unit := tt.
Definition iter_error_s {a e : Set}
(f : e → unit) (r : Pervasives.result a e) : unit := tt.
Definition is_ok {a e : Set} (r : Pervasives.result a e) : bool :=
match r with
| Pervasives.Ok v ⇒ true
| Pervasives.Error e ⇒ false
end.
Definition is_error {a e : Set} (r : Pervasives.result a e) : bool :=
match r with
| Pervasives.Ok v ⇒ false
| Pervasives.Error e ⇒ true
end.
Definition equal {a e : Set} (cmp_val : a → a → bool)
(cmp_err : e → e → bool) (r : Pervasives.result a e)
(r' : Pervasives.result a e) : bool :=
match r, r' with
| Pervasives.Ok v, Pervasives.Ok v' ⇒ cmp_val v v'
| Pervasives.Error e, Pervasives.Error e' ⇒ cmp_err e e'
| _, _ ⇒ false
end.
Definition compare {a e : Set} (cmp_val : a → a → int)
(cmp_err : e → e → int) (r : Pervasives.result a e)
(r' : Pervasives.result a e) : int :=
match r, r' with
| Pervasives.Ok v, Pervasives.Ok v' ⇒ cmp_val v v'
| Pervasives.Error e, Pervasives.Error e' ⇒ cmp_err e e'
| Pervasives.Ok _, Pervasives.Error _ ⇒ -1
| Pervasives.Error _, Pervasives.Ok _ ⇒ 1
end.
Definition to_option {a e : Set} (r : Pervasives.result a e) : option a :=
match r with
| Pervasives.Ok v ⇒ Some v
| Pervasives.Error e ⇒ None
end.
Definition of_option {a e : Set} (err : e) (o : option a)
: Pervasives.result a e :=
match o with
| None ⇒ Pervasives.Error err
| Some v ⇒ Pervasives.Ok v
end.
Definition to_list {a e : Set} (r : Pervasives.result a e) : list a :=
match r with
| Pervasives.Ok v ⇒ [v]
| Pervasives.Error e ⇒ []
end.
Definition to_seq {a e : Set} (r : Pervasives.result a e) : Seq.t a :=
match r with
| Pervasives.Ok v ⇒ Seq._return v
| Pervasives.Error err ⇒ Seq.empty
end.
Definition catch {a : Set} (_ : option (extensible_type → bool))
(f : unit → a) : Pervasives.result a extensible_type :=
Pervasives.Ok (f tt). (* Here f cannot raise an exception *)
Definition catch_f {_error a : Set} (_ : option (extensible_type → bool))
(f : unit → a) (_ : extensible_type → _error)
: Pervasives.result a _error :=
Pervasives.Ok (f tt). (* Here again f cannot raise an exception *)
Definition catch_s {a : Set} (_ : option (extensible_type → bool))
(f : unit → a) : Pervasives.result a extensible_type :=
Pervasives.Ok (f tt). (* Here again f cannot raise an exception *)
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.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 v1 ⇒ e2 v1
| Pervasives.Error e1 ⇒ Pervasives.Error e1
end.
Definition ok_s {a e : Set} (v : a) : Pervasives.result a e :=
Pervasives.Ok v.
Definition error_value {a e : Set} (err : e) : Pervasives.result a e :=
Pervasives.Error err.
Definition error_s {a e : Set} (err : e) : Pervasives.result a e :=
Pervasives.Error err.
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 v ⇒ v
| Pervasives.Error _ ⇒ default
end.
Definition value_f {a e : Set} (r : Pervasives.result a e) (default : unit → a)
: a :=
match r with
| Pervasives.Ok v ⇒ v
| Pervasives.Error _ ⇒ default tt
end.
Definition bind_s {a b e : Set}
(x : Pervasives.result a e) (f : a → Pervasives.result b e)
: Pervasives.result b e :=
match x with
| Pervasives.Ok v ⇒ f v
| Pervasives.Error err ⇒ Pervasives.Error err
end.
Definition bind_error {a e f : Set}
(x : Pervasives.result a e) (func : e → Pervasives.result a f)
: Pervasives.result a f :=
match x with
| Pervasives.Ok v ⇒ Pervasives.Ok v
| Pervasives.Error err ⇒ func err
end.
Definition bind_error_s {a e f : Set}
(x : Pervasives.result a e) (func : e → Pervasives.result a f)
: Pervasives.result a f :=
match x with
| Pervasives.Ok v ⇒ Pervasives.Ok v
| Pervasives.Error err ⇒ func err
end.
Definition join {a e : Set}
(rr : Pervasives.result (Pervasives.result a e) e)
: Pervasives.result a e :=
match rr with
| Pervasives.Error err ⇒ Pervasives.Error err
| Pervasives.Ok r ⇒ r
end.
Definition map {a b e : Set} (f : a → b) (x : Pervasives.result a e) :
Pervasives.result b e :=
match x with
| Pervasives.Ok v ⇒ Pervasives.Ok (f v)
| Pervasives.Error err ⇒ Pervasives.Error err
end.
Definition map_e {a b e : Set}
(f : a → Pervasives.result b e) (x : Pervasives.result a e)
: Pervasives.result b e :=
join (map f x).
Definition map_s : ∀ {a b e : Set},
(a → b) → Pervasives.result a e → Pervasives.result b e := @map.
Definition map_es : ∀ {a b e : Set},
(a → Pervasives.result b e) → Pervasives.result a e →
Pervasives.result b e := @map_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 a ⇒ Pervasives.Ok a
| Pervasives.Error e ⇒ Pervasives.Error (func e)
end.
Definition map_error_e {a e f : Set}
(func : e → Pervasives.result a f) (res : Pervasives.result a e)
: Pervasives.result a f :=
match res with
| Pervasives.Ok v ⇒ Pervasives.Ok v
| Pervasives.Error err ⇒ func err
end.
Definition map_error_s {a e f : Set}
(func : e → f) (res : Pervasives.result a e) : Pervasives.result a f :=
match res with
Pervasives.Ok a ⇒ Pervasives.Ok a
| Pervasives.Error e ⇒ Pervasives.Error (func e)
end.
Definition map_error_es {a e f : Set}
(func : e → Pervasives.result a f) (res : Pervasives.result a e)
: Pervasives.result a f :=
match res with
| Pervasives.Ok v ⇒ Pervasives.Ok v
| Pervasives.Error err ⇒ func err
end.
Definition fold {a c e : Set}
(f : a → c) (f' : e → c) (r : Pervasives.result a e) : c :=
match r with
| Pervasives.Ok v ⇒ f v
| Pervasives.Error err ⇒ f' err
end.
Definition iter {a e : Set}
(f : a → unit) (r : Pervasives.result a e) : unit := tt.
Definition iter_s {a e : Set}
(f : a → unit) (r : Pervasives.result a e) : unit := tt.
Definition iter_error {a e : Set}
(f : e → unit) (r : Pervasives.result a e) : unit := tt.
Definition iter_error_s {a e : Set}
(f : e → unit) (r : Pervasives.result a e) : unit := tt.
Definition is_ok {a e : Set} (r : Pervasives.result a e) : bool :=
match r with
| Pervasives.Ok v ⇒ true
| Pervasives.Error e ⇒ false
end.
Definition is_error {a e : Set} (r : Pervasives.result a e) : bool :=
match r with
| Pervasives.Ok v ⇒ false
| Pervasives.Error e ⇒ true
end.
Definition equal {a e : Set} (cmp_val : a → a → bool)
(cmp_err : e → e → bool) (r : Pervasives.result a e)
(r' : Pervasives.result a e) : bool :=
match r, r' with
| Pervasives.Ok v, Pervasives.Ok v' ⇒ cmp_val v v'
| Pervasives.Error e, Pervasives.Error e' ⇒ cmp_err e e'
| _, _ ⇒ false
end.
Definition compare {a e : Set} (cmp_val : a → a → int)
(cmp_err : e → e → int) (r : Pervasives.result a e)
(r' : Pervasives.result a e) : int :=
match r, r' with
| Pervasives.Ok v, Pervasives.Ok v' ⇒ cmp_val v v'
| Pervasives.Error e, Pervasives.Error e' ⇒ cmp_err e e'
| Pervasives.Ok _, Pervasives.Error _ ⇒ -1
| Pervasives.Error _, Pervasives.Ok _ ⇒ 1
end.
Definition to_option {a e : Set} (r : Pervasives.result a e) : option a :=
match r with
| Pervasives.Ok v ⇒ Some v
| Pervasives.Error e ⇒ None
end.
Definition of_option {a e : Set} (err : e) (o : option a)
: Pervasives.result a e :=
match o with
| None ⇒ Pervasives.Error err
| Some v ⇒ Pervasives.Ok v
end.
Definition to_list {a e : Set} (r : Pervasives.result a e) : list a :=
match r with
| Pervasives.Ok v ⇒ [v]
| Pervasives.Error e ⇒ []
end.
Definition to_seq {a e : Set} (r : Pervasives.result a e) : Seq.t a :=
match r with
| Pervasives.Ok v ⇒ Seq._return v
| Pervasives.Error err ⇒ Seq.empty
end.
Definition catch {a : Set} (_ : option (extensible_type → bool))
(f : unit → a) : Pervasives.result a extensible_type :=
Pervasives.Ok (f tt). (* Here f cannot raise an exception *)
Definition catch_f {_error a : Set} (_ : option (extensible_type → bool))
(f : unit → a) (_ : extensible_type → _error)
: Pervasives.result a _error :=
Pervasives.Ok (f tt). (* Here again f cannot raise an exception *)
Definition catch_s {a : Set} (_ : option (extensible_type → bool))
(f : unit → a) : Pervasives.result a extensible_type :=
Pervasives.Ok (f tt). (* Here again f cannot raise an exception *)