File: Option.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (72 lines) | stat: -rw-r--r-- 1,969 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Some of the below functions are inspired by ocaml-extlib *)

Require Import Ltac2.Init.
Require Import Ltac2.Control.

Ltac2 may (f : 'a -> unit) (ov : 'a option) :=
  match ov with
  | Some v => f v
  | None => ()
  end.

Ltac2 map (f : 'a -> 'b) (ov : 'a option) :=
  match ov with
  | Some v => Some (f v)
  | None => None
  end.

Ltac2 default (def : 'a) (ov : 'a option) :=
  match ov with
  | Some v => v
  | None => def
  end.

Ltac2 map_default (f : 'a -> 'b) (def : 'b) (ov : 'a option) :=
  match ov with
  | Some v => f v
  | None => def
  end.

Ltac2 get (ov : 'a option) :=
  match ov with
  | Some v => v
  | None => Control.throw No_value
  end.

Ltac2 get_bt (ov : 'a option) :=
  match ov with
  | Some v => v
  | None => Control.zero No_value
  end.

Ltac2 bind (x : 'a option) (f : 'a -> 'b option) :=
  match x with
  | Some x => f x
  | None => None
  end.

Ltac2 ret (x : 'a) := Some x.

Ltac2 lift (f : 'a -> 'b) (x : 'a option) := map f x.

Ltac2 equal (eq : 'a -> 'b -> bool) (a : 'a option) (b : 'b option) : bool
  := match a with
     | None => match b with
               | None => true
               | _ => false
               end
     | Some a => match b with
                 | Some b => eq a b
                 | _ => false
                 end
     end.