Skip to main content

🍃 Option.v

Environment

See proofs, Gitlab , OCaml

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
  | Nonev
  | Some vv
  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
  | Nonef tt
  | Some vv
  end.

Definition bind {a b : Set} (x : option a) (f : a option b) : option b :=
  match x with
  | NoneNone
  | Some vf v
  end.

Definition join {a : Set} (x : option (option a)) : option a :=
  match x with
  | None | Some NoneNone
  | 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, NoneNone
  end.

Definition map {a b : Set} (f : a b) (x : option a) : option b :=
  match x with
  | NoneNone
  | Some vSome (f v)
  end.

Definition map_s {a b : Set} (f : a b) (x : option a) : option b :=
  match x with
  | NoneNone
  | Some vSome (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
  | Nonedefault
  | Some vf v
  end.

Definition fold_s {a b : Set} (default : a) (f : b a) (x : option b) : a :=
  match x with
  | Nonedefault
  | Some vf 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 vg 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
  | Nonetrue
  | Some _false
  end.

Definition is_some {a : Set} (x : option a) : bool :=
  match x with
  | Nonefalse
  | Some _true
  end.

Definition equal {a : Set} (f : a a bool) (x1 x2 : option a) : bool :=
  match x1, x2 with
  | None, Nonetrue
  | Some v1, Some v2f v1 v2
  | None, Some _ | Some _, Nonefalse
  end.

Definition compare {a : Set} (f : a a int) (x1 x2 : option a) : int :=
  match x1, x2 with
  | None, None ⇒ 0
  | Some v1, Some v2f 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
  | NonePervasives.Error error
  | Some vPervasives.Ok v
  end.

Definition of_result {a e : Set} (x : Pervasives.result a e) : option a :=
  match x with
  | Pervasives.Error eNone
  | Pervasives.Ok vSome 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
  | NoneSeq.empty
  | Some vSeq._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 xY))
    (at level 200, x name, X at level 100, Y at level 200).

  Notation "'let*' ' x ':=' X 'in' Y" :=
    (bind X (fun xY))
    (at level 200, x pattern, X at level 100, Y at level 200).
End Notations.
Import Notations.