Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Generalizable All Variables.

From Coq Require Import List.
Import ListNotations.
From CoqFFI Require Seq.
From CoqFFI Require Import Int.

Notation Ok := inl.
Notation Err := inr.

Definition ok (a e : Type) : a → a + e :=
  @Ok a e.

Definition error (a : Type) (e : Type) : e → a + e :=
  @Err a e.

Definition value (a : Type) (e : Type) (x : a + e) (default : a) : a :=
  match x with
  | Ok x ⇒ x
  | _ ⇒ default
  end.

Definition bind {a b e} (x : a + e) (f : a → b + e) : b + e :=
  match x with
  | Ok x ⇒ f x
  | Err e ⇒ Err e
  end.

Definition join (a e : Type) (x : (a + e) + e) : a + e :=
  match x with
  | Ok (Ok x) ⇒ Ok x
  | Ok (Err e) | Err e ⇒ Err e
  end.

Definition map (a b e : Type) (f : a → b) (x : a + e) : b + e :=
  match x with
  | Ok x ⇒ Ok (f x)
  | Err e ⇒ Err e
  end.

Definition map_error (a e e' : Type) (f : e → e') (x : a + e) : a + e' :=
  match x with
  | Err err ⇒ Err (f err)
  | Ok x ⇒ Ok x
  end.

Definition fold (a e c : Type) (f : a → c) (g : e → c) (x : a + e) : c :=
  match x with
  | Ok x ⇒ f x
  | Err err ⇒ g err
  end.

Definition is_ok (a e : Type) (x : a + e) : bool :=
  match x with
  | Ok _ ⇒ true
  | _ ⇒ false
  end.

Definition is_error (a e : Type) (x : a + e) : bool :=
  match x with
  | Err _ ⇒ true
  | _ ⇒ false
  end.

Definition equal (a e : Type) (eqa : a → a → bool) (eqe : e → e → bool)
    (x y : a + e)
  : bool :=
  match x, y with
  | Ok x, Ok y ⇒ eqa x y
  | Err err, Err err' ⇒ eqe err err'
  | _, _ ⇒ false
  end.

Definition compare (a e : Type) (ca : a → a → i63) (ce : e → e → i63)
    (x y : a + e)
  : i63 :=
  match x, y with
  | Ok x, Ok y ⇒ ca x y
  | Err err, Err err' ⇒ ce err err'
  | Ok _, Err _ ⇒ -1
  | Err _, _ ⇒ 1
  end.

Definition to_option (a e : Type) (x : a + e) : option a :=
  match x with
  | Ok x ⇒ Some x
  | Err y ⇒ None
  end.

Definition to_list (a e : Type) (x : a + e) : list a :=
  match x with
  | Ok x ⇒ [x]
  | _ ⇒ []
  end.

Definition to_seq (a e : Type) (x : a + e) : Seq.t a :=
  match x with
  | Ok x ⇒ Seq.ret x
  | _ ⇒ Seq.empty
  end.

Module ResultExtraction.
  Extract Constant ok ⇒ "Stdlib.Result.ok".
  Extract Constant error ⇒ "Stdlib.Result.error".
  Extract Constant value ⇒ "(fun x d -> Stdlib.Result.value x ~default:d)".
  Extract Constant bind ⇒ "Stdlib.Result.bind".
  Extract Constant join ⇒ "Stdlib.Result.join".
  Extract Constant map ⇒ "Stdlib.Result.map".
  Extract Constant map_error ⇒ "Stdlib.Result.map_error".
  Extract Constant fold ⇒ "(fun ok error -> Stdlib.Result.fold ~ok ~error)".
  Extract Constant is_ok ⇒ "Stdlib.Result.is_ok".
  Extract Constant is_error ⇒ "Stdlib.Result.is_error".
  Extract Constant equal ⇒ "(fun ok error -> Stdlib.Result.equal ~ok ~error)".
  Extract Constant compare ⇒ "(fun ok error -> Stdlib.Result.compare ~ok ~error)".
  Extract Constant to_option ⇒ "Stdlib.Result.to_option".
  Extract Constant to_list ⇒ "Stdlib.Result.to_list".
  Extract Constant to_seq ⇒ "Stdlib.Result.to_seq".
End ResultExtraction.