Removed backtracking and default variants of various functions and added option combinators

3 files changed, 43 insertions, 49 deletions

diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 5c51c798c1..7c735f3b10 100755
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -63,6 +63,9 @@ Ltac2 Type exn ::= [ Not_focussed ].
 Ltac2 Type exn ::= [ Not_found ].
 (** Used when something is missing. *)
 
+Ltac2 Type exn ::= [ No_value ].
+(** Used for empty lists, None options and the like. *)
+
 Ltac2 Type exn ::= [ Match_failure ].
 (** Used to signal a pattern didn't match a term. *)
 
diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v
index 3783618cb1..89e14445ef 100644
--- a/user-contrib/Ltac2/List.v
+++ b/user-contrib/Ltac2/List.v
@@ -74,21 +74,9 @@ Ltac2 hd_opt (ls : 'a list) :=
   | x :: xs => Some x
   end.
 
-Ltac2 hd_default (default : 'a) (ls : 'a list) :=
-  match hd_opt ls with
-  | Some v => v
-  | None => default
-  end.
-
-Ltac2 hd_throw (ls : 'a list) :=
-  match ls with
-  | [] => Control.throw_invalid_argument "List.hd"
-  | x :: xs => x
-  end.
-
 Ltac2 hd (ls : 'a list) :=
   match ls with
-  | [] => Control.backtrack_tactic_failure "List.hd"
+  | [] => Control.throw_invalid_argument "List.hd"
   | x :: xs => x
   end.
 
@@ -108,21 +96,9 @@ Ltac2 rec last_opt (ls : 'a list) :=
        end
   end.
 
-Ltac2 last_default (default : 'a) (ls : 'a list) :=
-  match last_opt ls with
-  | None => default
-  | Some v => v
-  end.
-
-Ltac2 last_throw (ls : 'a list) :=
-  match last_opt ls with
-  | None => Control.throw_invalid_argument "List.last"
-  | Some v => v
-  end.
-
 Ltac2 last (ls : 'a list) :=
   match last_opt ls with
-  | None => Control.backtrack_tactic_failure "List.last"
+  | None => Control.throw_invalid_argument "List.last"
   | Some v => v
   end.
 
@@ -150,12 +126,6 @@ Ltac2 nth_opt (ls : 'a list) (n : int) :=
   Control.assert_valid_argument "List.nth" (Int.ge n 0);
   nth_opt_aux ls n.
 
-Ltac2 nth_default (default : 'a) (ls : 'a list) (n : int) :=
-  match nth_opt ls n with
-  | Some v => v
-  | None => default
-  end.
-
 Ltac2 nth (ls : 'a list) (n : int) :=
   match nth_opt ls n with
   | Some v => v
@@ -381,16 +351,10 @@ Ltac2 rec find_opt f xs :=
                end
   end.
 
-Ltac2 find_throw f xs :=
-  match find_opt f xs with
-  | Some v => v
-  | None => Control.throw Not_found
-  end.
-
 Ltac2 find f xs :=
   match find_opt f xs with
   | Some v => v
-  | None => Control.zero Not_found
+  | None => Control.throw Not_found
   end.
 
 Ltac2 rec find_rev_opt f xs :=
@@ -405,16 +369,10 @@ Ltac2 rec find_rev_opt f xs :=
                end
   end.
 
-Ltac2 find_rev_throw f xs :=
-  match find_rev_opt f xs with
-  | Some v => v
-  | None => Control.throw Not_found
-  end.
-
 Ltac2 find_rev f xs :=
   match find_rev_opt f xs with
   | Some v => v
-  | None => Control.zero Not_found
+  | None => Control.throw Not_found
   end.
 
 Ltac2 mem (eq : 'a -> 'a -> bool) (a : 'a) (ls : 'a list) :=
diff --git a/user-contrib/Ltac2/Option.v b/user-contrib/Ltac2/Option.v
index af0b7c28ca..584d84ddb5 100644
--- a/user-contrib/Ltac2/Option.v
+++ b/user-contrib/Ltac2/Option.v
@@ -8,14 +8,47 @@
 (*         *     (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 map (f : 'a -> 'b) (x : 'a option) :=
-  match x with
-  | Some x => Some (f x)
+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