- added OCaml copyright header to List.v (if for no other reason than out of courtesy)

- index errors (negative or out of bounds) generally throw (panic)
- hd, last, find backtrack, because here backtracking can actually be useful
  added a _throw variant to these functions which panics
  This emaphasizes the difference between backtracking and throwing exceptions, which doesn't exist in OCaml.
- simplified the implementation of for_all2 and exist2 (ok, that is a matter of taste ...)
- added assertions which combine a boolean match with a throw.
  This makes the code more readable and makes it easier to have more specific error messages.
- added a lastn function
- gave Out_of_bounds a message argument (there is no good reason why invalid_argument has one and this not)
  All other exceptions without message argument are quite specific to certain functions (like Not_Found)

1 files changed, 26 insertions, 0 deletions

diff --git a/user-contrib/Ltac2/Control.v b/user-contrib/Ltac2/Control.v
index 071c2ea8ce..6068dd20cb 100644
--- a/user-contrib/Ltac2/Control.v
+++ b/user-contrib/Ltac2/Control.v
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
+Require Ltac2.Message.
 
 (** Panic *)
 
@@ -74,3 +75,28 @@ Ltac2 @ external abstract : ident option -> (unit -> unit) -> unit := "ltac2" "a
 
 Ltac2 @ external check_interrupt : unit -> unit := "ltac2" "check_interrupt".
 (** For internal use. *)
+
+(** Assertions throwing exceptions and short form throws *)
+
+Ltac2 throw_invalid_argument (msg : string) :=
+  Control.throw (Invalid_argument (Some (Message.of_string msg))).
+
+Ltac2 throw_out_of_bounds (msg : string) :=
+  Control.throw (Out_of_bounds (Some (Message.of_string msg))).
+
+Ltac2 assert_valid_argument (msg : string) (test : bool) :=
+  match test with
+  | true => ()
+  | false => throw_invalid_argument msg
+  end.
+
+Ltac2 assert_bounds (msg : string) (test : bool) :=
+  match test with
+  | true => ()
+  | false => throw_out_of_bounds msg
+  end.
+
+(** Short form backtracks *)
+
+Ltac2 backtrack_tactic_failure (msg : string) :=
+  Control.zero (Tactic_failure (Some (Message.of_string msg))).