Defining a few base tacticals.

3 files changed, 93 insertions, 1 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 7539e1b697..08f61f2c6c 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -574,6 +574,27 @@ let prm_with_holes : ml_tactic = function
   Tacticals.New.tclWITHHOLES false (interp_app f [ans]) sigma
 | _ -> assert false
 
+let prm_progress : ml_tactic = function
+| [f] -> Proofview.tclPROGRESS (thaw f)
+| _ -> assert false
+
+let prm_abstract : ml_tactic = function
+| [id; f] ->
+  let id = Value.to_option Value.to_ident id in
+  Tactics.tclABSTRACT id (Proofview.tclIGNORE (thaw f)) >>= fun () ->
+  return v_unit
+| _ -> assert false
+
+let prm_time : ml_tactic = function
+| [s; f] ->
+  let s = Value.to_option Value.to_string s in
+  Proofview.tclTIME s (thaw f)
+| _ -> assert false
+
+let prm_check_interrupt : ml_tactic = function
+| [_] -> Proofview.tclCHECKINTERRUPT >>= fun () -> return v_unit
+| _ -> assert false
+
 (** Registering *)
 
 let () = Tac2env.define_primitive (pname "print") prm_print
@@ -632,6 +653,10 @@ let () = Tac2env.define_primitive (pname "hyp") prm_hyp
 let () = Tac2env.define_primitive (pname "hyps") prm_hyps
 let () = Tac2env.define_primitive (pname "refine") prm_refine
 let () = Tac2env.define_primitive (pname "with_holes") prm_with_holes
+let () = Tac2env.define_primitive (pname "progress") prm_progress
+let () = Tac2env.define_primitive (pname "abstract") prm_abstract
+let () = Tac2env.define_primitive (pname "time") prm_time
+let () = Tac2env.define_primitive (pname "check_interrupt") prm_check_interrupt
 
 (** ML types *)
 
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 :=