Skip to main content

🍃 Result.v

Environment

Gitlab

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 v1e2 v1
  | Pervasives.Error e1Pervasives.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 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.

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 vf v
  | Pervasives.Error errPervasives.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 vPervasives.Ok v
  | Pervasives.Error errfunc 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 vPervasives.Ok v
  | Pervasives.Error errfunc err
  end.

Definition join {a e : Set}
  (rr : Pervasives.result (Pervasives.result a e) e)
  : Pervasives.result a e :=
  match rr with
  | Pervasives.Error errPervasives.Error err
  | Pervasives.Ok rr
  end.

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.

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 aPervasives.Ok a
  | Pervasives.Error ePervasives.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 vPervasives.Ok v
  | Pervasives.Error errfunc 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 aPervasives.Ok a
  | Pervasives.Error ePervasives.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 vPervasives.Ok v
  | Pervasives.Error errfunc 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 vf v
  | Pervasives.Error errf' 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 vtrue
  | Pervasives.Error efalse
  end.

Definition is_error {a e : Set} (r : Pervasives.result a e) : bool :=
  match r with
  | Pervasives.Ok vfalse
  | Pervasives.Error etrue
  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 vSome v
  | Pervasives.Error eNone
  end.

Definition of_option {a e : Set} (err : e) (o : option a)
  : Pervasives.result a e :=
  match o with
  | NonePervasives.Error err
  | Some vPervasives.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 vSeq._return v
  | Pervasives.Error errSeq.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 *)