Defining a few base tacticals.

2 files changed, 68 insertions, 1 deletions

diff --git a/theories/Control.v b/theories/Control.v
index a8b92aced2..071c2ea8ce 100644
--- a/theories/Control.v
+++ b/theories/Control.v
@@ -34,6 +34,8 @@ Ltac2 @ external new_goal : evar -> unit := "ltac2" "new_goal".
     already defined in the current state, don't do anything. Panics if the
     evar is not in the current state. *)
 
+Ltac2 @ external progress : (unit -> 'a) -> 'a := "ltac2" "progress".
+
 (** Goal inspection *)
 
 Ltac2 @ external goal : unit -> constr := "ltac2" "goal".
@@ -61,3 +63,14 @@ Ltac2 @ external with_holes : (unit -> 'a) -> ('a -> 'b) -> 'b := "ltac2" "with_
 (** [with_holes x f] evaluates [x], then apply [f] to the result, and fails if
     all evars generated by the call to [x] have not been solved when [f]
     returns. *)
+
+(** Misc *)
+
+Ltac2 @ external time : string option -> (unit -> 'a) -> 'a := "ltac2" "time".
+(** Displays the time taken by a tactic to evaluate. *)
+
+Ltac2 @ external abstract : ident option -> (unit -> unit) -> unit := "ltac2" "abstract".
+(** Abstract a subgoal. *)
+
+Ltac2 @ external check_interrupt : unit -> unit := "ltac2" "check_interrupt".
+(** For internal use. *)
diff --git a/theories/Notations.v b/theories/Notations.v
index 4bba9a7495..f11cfbde6e 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -7,7 +7,61 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
-Require Ltac2.Control Ltac2.Std.
+Require Ltac2.Control Ltac2.Int Ltac2.Std.
+
+(** Tacticals *)
+
+Ltac2 orelse t f :=
+match Control.case t with
+| Err e => f e
+| Val ans =>
+  let ((x, k)) := ans in
+  Control.plus (fun _ => x) k
+end.
+
+Ltac2 ifcatch t s f :=
+match Control.case t with
+| Err e => f e
+| Val ans =>
+  let ((x, k)) := ans in
+  Control.plus (fun _ => s x) (fun e => s (k e))
+end.
+
+Ltac2 try0 t := Control.enter (fun _ => orelse t (fun _ => ())).
+
+Ltac2 Notation try := try0.
+
+Ltac2 rec repeat0 (t : unit -> unit) :=
+  Control.enter (fun () =>
+    ifcatch (fun _ => Control.progress t)
+      (fun _ => Control.check_interrupt (); repeat0 t) (fun _ => ())).
+
+Ltac2 Notation repeat := repeat0.
+
+Ltac2 do0 n t :=
+  let rec aux n t := match Int.equal n 0 with
+  | true => ()
+  | false => t (); aux (Int.sub n 1) t
+  end in
+  aux (n ()) t.
+
+Ltac2 Notation do := do0.
+
+Ltac2 Notation once := Control.once.
+
+Ltac2 progress0 tac := Control.enter (fun _ => Control.progress tac).
+
+Ltac2 Notation progress := progress0.
+
+Ltac2 time0 tac := Control.time None tac.
+
+Ltac2 Notation time := time0.
+
+Ltac2 abstract0 tac := Control.abstract None tac.
+
+Ltac2 Notation abstract := abstract0.
+
+(** Base tactics *)
 
 (** Enter and check evar resolution *)
 Ltac2 enter_h ev f arg :=