🍃 Option.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Proto_alpha.Environment.Format.
Require Proto_alpha.Environment.Pervasives.
Require Proto_alpha.Environment.Seq.
Definition t (a : Set) : Set := option a.
Definition none {a : Set} : option a :=
None.
Definition none_e {a trace : Set} : Pervasives.result (option a) trace :=
Pervasives.Ok None.
Definition none_s {a : Set} : option a := None.
Definition none_es {a trace : Set} : Pervasives.result (option a) trace := none_e.
Definition some {a : Set} (x : a) : option a :=
Some x.
Definition some_unit : option unit := Some tt.
Definition some_nil {a : Set} : option (list a) := Some [].
Definition some_e {a trace : Set} (x : a) : Pervasives.result (option a) trace := Pervasives.Ok (Some x).
Definition some_s {a : Set} (x : a) : option a := Some x.
Definition some_es {a trace : Set} (x : a) : Pervasives.result (option a) trace :=
Pervasives.Ok (Some x).
Definition value_value {a : Set} (x : option a) (v : a) : a :=
match x with
| None ⇒ v
| Some v ⇒ v
end.
Parameter value_e : ∀ {a trace : Set},
option a → trace → Pervasives.result a trace.
Parameter value_fe : ∀ {a trace : Set},
option a → (unit → trace) → Pervasives.result a trace.
Definition value_f {a : Set} (x : option a) (f : unit → a) : a :=
match x with
| None ⇒ f tt
| Some v ⇒ v
end.
Definition bind {a b : Set} (x : option a) (f : a → option b) : option b :=
match x with
| None ⇒ None
| Some v ⇒ f v
end.
Definition join {a : Set} (x : option (option a)) : option a :=
match x with
| None | Some None ⇒ None
| Some (Some v) ⇒ Some v
end.
Definition either {a : Set} (x1 x2 : option a) : option a :=
match x1, x2 with
| Some _, _ ⇒ x1
| None, Some _ ⇒ x2
| None, None ⇒ None
end.
Definition map {a b : Set} (f : a → b) (x : option a) : option b :=
match x with
| None ⇒ None
| Some v ⇒ Some (f v)
end.
Definition map_s {a b : Set} (f : a → b) (x : option a) : option b :=
match x with
| None ⇒ None
| Some v ⇒ Some (f v)
end.
Parameter map_e : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → option a →
Pervasives.result (option b) trace.
Parameter map_es : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → option a →
Pervasives.result (option b) trace.
Definition fold {a b : Set} (default : a) (f : b → a) (x : option b) : a :=
match x with
| None ⇒ default
| Some v ⇒ f v
end.
Definition fold_s {a b : Set} (default : a) (f : b → a) (x : option b) : a :=
match x with
| None ⇒ default
| Some v ⇒ f v
end.
Definition fold_f {a b : Set} (f : unit → a) (g : b → a) (x : option b) : a :=
match x with
| None ⇒ (f tt)
| Some v ⇒ g v
end.
Definition iter {a : Set} (f : a → unit) (x : option a) : unit :=
tt.
Parameter iter_s : ∀ {a : Set},
(a → unit) → option a → unit.
Parameter iter_e : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → option a →
Pervasives.result unit trace.
Parameter iter_es : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → option a →
Pervasives.result unit trace.
Definition is_none {a : Set} (x : option a) : bool :=
match x with
| None ⇒ true
| Some _ ⇒ false
end.
Definition is_some {a : Set} (x : option a) : bool :=
match x with
| None ⇒ false
| Some _ ⇒ true
end.
Definition equal {a : Set} (f : a → a → bool) (x1 x2 : option a) : bool :=
match x1, x2 with
| None, None ⇒ true
| Some v1, Some v2 ⇒ f v1 v2
| None, Some _ | Some _, None ⇒ false
end.
Definition compare {a : Set} (f : a → a → int) (x1 x2 : option a) : int :=
match x1, x2 with
| None, None ⇒ 0
| Some v1, Some v2 ⇒ f v1 v2
| None, Some _ ⇒ -1
| Some _, None ⇒ 1
end.
Definition to_result {a trace : Set} (error : trace) (v : option a)
: Pervasives.result a trace :=
match v with
| None ⇒ Pervasives.Error error
| Some v ⇒ Pervasives.Ok v
end.
Definition of_result {a e : Set} (x : Pervasives.result a e) : option a :=
match x with
| Pervasives.Error e ⇒ None
| Pervasives.Ok v ⇒ Some v
end.
Definition to_list {a : Set} (x : option a) : list a :=
match x with
| None ⇒ []
| Some v ⇒ [v]
end.
Definition to_seq {a : Set} (x : option a) : Seq.t a :=
match x with
| None ⇒ Seq.empty
| Some v ⇒ Seq._return v
end.
Require Import CoqOfOCaml.Settings.
Require Proto_alpha.Environment.Format.
Require Proto_alpha.Environment.Pervasives.
Require Proto_alpha.Environment.Seq.
Definition t (a : Set) : Set := option a.
Definition none {a : Set} : option a :=
None.
Definition none_e {a trace : Set} : Pervasives.result (option a) trace :=
Pervasives.Ok None.
Definition none_s {a : Set} : option a := None.
Definition none_es {a trace : Set} : Pervasives.result (option a) trace := none_e.
Definition some {a : Set} (x : a) : option a :=
Some x.
Definition some_unit : option unit := Some tt.
Definition some_nil {a : Set} : option (list a) := Some [].
Definition some_e {a trace : Set} (x : a) : Pervasives.result (option a) trace := Pervasives.Ok (Some x).
Definition some_s {a : Set} (x : a) : option a := Some x.
Definition some_es {a trace : Set} (x : a) : Pervasives.result (option a) trace :=
Pervasives.Ok (Some x).
Definition value_value {a : Set} (x : option a) (v : a) : a :=
match x with
| None ⇒ v
| Some v ⇒ v
end.
Parameter value_e : ∀ {a trace : Set},
option a → trace → Pervasives.result a trace.
Parameter value_fe : ∀ {a trace : Set},
option a → (unit → trace) → Pervasives.result a trace.
Definition value_f {a : Set} (x : option a) (f : unit → a) : a :=
match x with
| None ⇒ f tt
| Some v ⇒ v
end.
Definition bind {a b : Set} (x : option a) (f : a → option b) : option b :=
match x with
| None ⇒ None
| Some v ⇒ f v
end.
Definition join {a : Set} (x : option (option a)) : option a :=
match x with
| None | Some None ⇒ None
| Some (Some v) ⇒ Some v
end.
Definition either {a : Set} (x1 x2 : option a) : option a :=
match x1, x2 with
| Some _, _ ⇒ x1
| None, Some _ ⇒ x2
| None, None ⇒ None
end.
Definition map {a b : Set} (f : a → b) (x : option a) : option b :=
match x with
| None ⇒ None
| Some v ⇒ Some (f v)
end.
Definition map_s {a b : Set} (f : a → b) (x : option a) : option b :=
match x with
| None ⇒ None
| Some v ⇒ Some (f v)
end.
Parameter map_e : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → option a →
Pervasives.result (option b) trace.
Parameter map_es : ∀ {a b trace : Set},
(a → Pervasives.result b trace) → option a →
Pervasives.result (option b) trace.
Definition fold {a b : Set} (default : a) (f : b → a) (x : option b) : a :=
match x with
| None ⇒ default
| Some v ⇒ f v
end.
Definition fold_s {a b : Set} (default : a) (f : b → a) (x : option b) : a :=
match x with
| None ⇒ default
| Some v ⇒ f v
end.
Definition fold_f {a b : Set} (f : unit → a) (g : b → a) (x : option b) : a :=
match x with
| None ⇒ (f tt)
| Some v ⇒ g v
end.
Definition iter {a : Set} (f : a → unit) (x : option a) : unit :=
tt.
Parameter iter_s : ∀ {a : Set},
(a → unit) → option a → unit.
Parameter iter_e : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → option a →
Pervasives.result unit trace.
Parameter iter_es : ∀ {a trace : Set},
(a → Pervasives.result unit trace) → option a →
Pervasives.result unit trace.
Definition is_none {a : Set} (x : option a) : bool :=
match x with
| None ⇒ true
| Some _ ⇒ false
end.
Definition is_some {a : Set} (x : option a) : bool :=
match x with
| None ⇒ false
| Some _ ⇒ true
end.
Definition equal {a : Set} (f : a → a → bool) (x1 x2 : option a) : bool :=
match x1, x2 with
| None, None ⇒ true
| Some v1, Some v2 ⇒ f v1 v2
| None, Some _ | Some _, None ⇒ false
end.
Definition compare {a : Set} (f : a → a → int) (x1 x2 : option a) : int :=
match x1, x2 with
| None, None ⇒ 0
| Some v1, Some v2 ⇒ f v1 v2
| None, Some _ ⇒ -1
| Some _, None ⇒ 1
end.
Definition to_result {a trace : Set} (error : trace) (v : option a)
: Pervasives.result a trace :=
match v with
| None ⇒ Pervasives.Error error
| Some v ⇒ Pervasives.Ok v
end.
Definition of_result {a e : Set} (x : Pervasives.result a e) : option a :=
match x with
| Pervasives.Error e ⇒ None
| Pervasives.Ok v ⇒ Some v
end.
Definition to_list {a : Set} (x : option a) : list a :=
match x with
| None ⇒ []
| Some v ⇒ [v]
end.
Definition to_seq {a : Set} (x : option a) : Seq.t a :=
match x with
| None ⇒ Seq.empty
| Some v ⇒ Seq._return v
end.
With-side effect.
Definition catch {a : Set} (_ : option (extensible_type → bool))
(f : unit → a) : option a :=
Some (f tt).
Parameter catch_s : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → option a.
Module Notations.
Notation "M* X" := (option X) (at level 20).
Notation "return* X" := (some X) (at level 20).
Notation "'let*' x ':=' X 'in' Y" :=
(bind X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'let*' ' x ':=' X 'in' Y" :=
(bind X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
End Notations.
Import Notations.
(f : unit → a) : option a :=
Some (f tt).
Parameter catch_s : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → option a.
Module Notations.
Notation "M* X" := (option X) (at level 20).
Notation "return* X" := (some X) (at level 20).
Notation "'let*' x ':=' X 'in' Y" :=
(bind X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'let*' ' x ':=' X 'in' Y" :=
(bind X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
End Notations.
Import Notations.