🍃 Option.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Format.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.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.
Definition value_e {a trace : Set} (x : option a) (e : trace) :
Pervasives.result a trace :=
match x with
| None ⇒ Pervasives.Error e
| Some v ⇒ Pervasives.Ok v
end.
Definition value_fe {a trace : Set} (x : option a) (f : unit → trace) :
Pervasives.result a trace :=
match x with
| None ⇒ Pervasives.Error (f tt)
| Some v ⇒ Pervasives.Ok v
end.
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.
Definition map_e {a b trace : Set}
(f : a → Pervasives.result b trace) (x : option a) :
Pervasives.result (option b) trace :=
match x with
| None ⇒ Pervasives.Ok None
| Some v ⇒
match f v with
| Pervasives.Error t ⇒ Pervasives.Error t
| Pervasives.Ok v' ⇒ Pervasives.Ok (Some v')
end
end.
Definition map_es {a b trace : Set}
(f : a → Pervasives.result b trace) (x : option a) :
Pervasives.result (option b) trace :=
match x with
| None ⇒ Pervasives.Ok None
| Some v ⇒
match f v with
| Pervasives.Error t ⇒ Pervasives.Error t
| Pervasives.Ok v' ⇒ Pervasives.Ok (Some v')
end
end.
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.
Definition iter_s {a : Set} (f : a → unit) (x : option a) : unit :=
tt.
Definition iter_e {a trace : Set}
(f : a → Pervasives.result unit trace) (x : option a) :
Pervasives.result unit trace :=
match x with
| None ⇒ Pervasives.Ok tt
| Some v ⇒ f v
end.
Definition iter_es {a trace : Set}
(f : a → Pervasives.result unit trace) (x : option a) :
Pervasives.result unit trace :=
match x with
| None ⇒ Pervasives.Ok tt
| Some v ⇒ f v
end.
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 TezosOfOCaml.Environment.Structs.V0.Format.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.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.
Definition value_e {a trace : Set} (x : option a) (e : trace) :
Pervasives.result a trace :=
match x with
| None ⇒ Pervasives.Error e
| Some v ⇒ Pervasives.Ok v
end.
Definition value_fe {a trace : Set} (x : option a) (f : unit → trace) :
Pervasives.result a trace :=
match x with
| None ⇒ Pervasives.Error (f tt)
| Some v ⇒ Pervasives.Ok v
end.
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.
Definition map_e {a b trace : Set}
(f : a → Pervasives.result b trace) (x : option a) :
Pervasives.result (option b) trace :=
match x with
| None ⇒ Pervasives.Ok None
| Some v ⇒
match f v with
| Pervasives.Error t ⇒ Pervasives.Error t
| Pervasives.Ok v' ⇒ Pervasives.Ok (Some v')
end
end.
Definition map_es {a b trace : Set}
(f : a → Pervasives.result b trace) (x : option a) :
Pervasives.result (option b) trace :=
match x with
| None ⇒ Pervasives.Ok None
| Some v ⇒
match f v with
| Pervasives.Error t ⇒ Pervasives.Error t
| Pervasives.Ok v' ⇒ Pervasives.Ok (Some v')
end
end.
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.
Definition iter_s {a : Set} (f : a → unit) (x : option a) : unit :=
tt.
Definition iter_e {a trace : Set}
(f : a → Pervasives.result unit trace) (x : option a) :
Pervasives.result unit trace :=
match x with
| None ⇒ Pervasives.Ok tt
| Some v ⇒ f v
end.
Definition iter_es {a trace : Set}
(f : a → Pervasives.result unit trace) (x : option a) :
Pervasives.result unit trace :=
match x with
| None ⇒ Pervasives.Ok tt
| Some v ⇒ f v
end.
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.
Parameter catch : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → option a.
Definition catch_s : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → option a :=
@catch.
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.
option (extensible_type → bool) → (unit → a) → option a.
Definition catch_s : ∀ {a : Set},
option (extensible_type → bool) → (unit → a) → option a :=
@catch.
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.