Tentative to add constr-using primitive tactics without grammar rules.

We eta-expand primitive Ltac functions, and instead of feeding TacExtend
directly with its arguments, we use the environment to retrieve them.

Some tactics from the AST were also moved away and made using this
mechanism.

4 files changed, 61 insertions, 38 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 0170b68014..2434d3f453 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -8,6 +8,11 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Util
+open Names
+open Tacexpr
+open Tacinterp
+
 DECLARE PLUGIN "coretactics"
 
 TACTIC EXTEND reflexivity
@@ -17,3 +22,59 @@ END
 TACTIC EXTEND assumption
   [ "assumption" ] -> [ Tactics.assumption ]
 END
+
+let make_vars len =
+  List.init len (fun i -> Id.of_string (Printf.sprintf "_%i" i))
+
+let dummy_id = Id.of_string "_"
+
+(** Add a tactic that only uses constrs arguments. Such tactics actually do
+    not need to define grammar rules, because tactic arguments are already
+    parsed as constrs. So we add them manually. *)
+(** TODO: do this automagically in TACTIC EXTEND and use it in this file *)
+let add_constr_tactic name len tac =
+  let vars = make_vars len in
+  (** We pass the arguments through the environment rather than through the
+      tactic, to overcome the way tactics arguments are interpreted. *)
+  let tac _ ist = Proofview.Goal.raw_enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let map id =
+      let c = Id.Map.find id ist.lfun in
+      try Taccoerce.coerce_to_closed_constr env c
+      with Taccoerce.CannotCoerceTo ty ->
+        error_ltac_variable Loc.ghost dummy_id (Some env) c ty
+    in
+    let args = List.map map vars in
+    tac args ist
+  end in
+  let () = Tacenv.register_ml_tactic name tac in
+  let ref = Libnames.Ident (Loc.ghost, Id.of_string name) in
+  let args = List.map (fun id -> Some id) vars in
+  let body = TacExtend (Loc.ghost, name, []) in
+  let body = TacFun (args, TacAtom (Loc.ghost, body)) in
+  let obj () = Tacenv.register_ltac false false [ref, false, body] in
+  Mltop.declare_cache_obj obj "coretactics"
+
+let () =
+  let tac args _ = match args with [c] _ -> Tactics.cut c | _ -> assert false in
+  add_constr_tactic "cut" 1 tac
+
+let () =
+  let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.exact_no_check c) | _ -> assert false in
+  add_constr_tactic "exact_no_check" 1 tac
+
+let () =
+  let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.vm_cast_no_check c) | _ -> assert false in
+  add_constr_tactic "vm_cast_no_check" 1 tac
+
+let () =
+  let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.case_type c) | _ -> assert false in
+  add_constr_tactic "casetype" 1 tac
+
+let () =
+  let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.elim_type c) | _ -> assert false in
+  add_constr_tactic "elimtype" 1 tac
+
+let () =
+  let tac args _ = match args with [c] -> Tactics.cut_and_apply c | _ -> assert false in
+  add_constr_tactic "lapply" 1 tac
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index ea3e346853..22ea274cb7 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -456,17 +456,13 @@ let rec intern_atomic lf ist x =
       TacIntroMove (Option.map (intern_ident lf ist) ido,
                     intern_move_location ist hto)
   | TacExact c -> TacExact (intern_constr ist c)
-  | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
-  | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
   | TacApply (a,ev,cb,inhyp) ->
       TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb,
                 Option.map (intern_in_hyp_as ist lf) inhyp)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,intern_constr_with_bindings ist cb,
                Option.map (intern_constr_with_bindings ist) cbo)
-  | TacElimType c -> TacElimType (intern_type ist c)
   | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
-  | TacCaseType c -> TacCaseType (intern_type ist c)
   | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
@@ -475,7 +471,6 @@ let rec intern_atomic lf ist x =
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
-  | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
       TacAssert (Option.map (intern_pure_tactic ist) otac,
                  Option.map (intern_intro_pattern lf ist) ipat,
@@ -516,7 +511,6 @@ let rec intern_atomic lf ist x =
   | TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in
       TacDecompose (l,intern_constr ist c)
   | TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l)
-  | TacLApply c -> TacLApply (intern_constr ist c)
 
   (* Context management *)
   | TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d72a37d33e..4333c5696d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1455,12 +1455,6 @@ and interp_atomic ist tac =
 	  (Tactics.exact_no_check c_interp)
           gl
       end
-  | TacExactNoCheck c ->
-      (new_interp_constr ist c)
-        (fun c -> Proofview.V82.tactic (Tactics.exact_no_check c))
-  | TacVmCastNoCheck c ->
-      (new_interp_constr ist c)
-        (fun c -> Proofview.V82.tactic (Tactics.vm_cast_no_check c))
   | TacApply (a,ev,cb,cl) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
@@ -1487,14 +1481,6 @@ and interp_atomic ist tac =
         let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
         Tacticals.New.tclWITHHOLES ev (Tactics.elim ev cb) sigma cbo
       end
-  | TacElimType c ->
-      Proofview.V82.tactic begin fun gl -> 
-        let (sigma,c_interp) = pf_interp_type ist gl c in
-        tclTHEN
-	  (tclEVARS sigma)
-	  (Tactics.elim_type c_interp)
-          gl
-      end
   | TacCase (ev,cb) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
@@ -1502,14 +1488,6 @@ and interp_atomic ist tac =
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
         Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev) sigma cb
       end
-  | TacCaseType c ->
-      Proofview.V82.tactic begin fun gl -> 
-        let (sigma,c_interp) = pf_interp_type ist gl c in
-        tclTHEN
-	  (tclEVARS sigma)
-	  (Tactics.case_type c_interp)
-          gl
-      end
   | TacFix (idopt,n) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
@@ -1548,8 +1526,6 @@ and interp_atomic ist tac =
 	  (Tactics.mutual_cofix (interp_fresh_ident ist env id) l_interp 0)
           gl
       end
-  | TacCut c ->
-      new_interp_type ist c Tactics.cut
   | TacAssert (t,ipat,c) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
@@ -1670,8 +1646,6 @@ and interp_atomic ist tac =
           tclWITHHOLES false (Tactics.specialize n) sigma cb gl
         end
       end
-  | TacLApply c ->
-      new_interp_constr ist c Tactics.cut_and_apply
 
   (* Context management *)
   | TacClear (b,l) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 31a1b57bc0..4d0b595690 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -135,23 +135,18 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
   | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
   | TacExact c -> TacExact (subst_glob_constr subst c)
-  | TacExactNoCheck c -> TacExactNoCheck (subst_glob_constr subst c)
-  | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_glob_constr subst c)
   | TacApply (a,ev,cb,cl) ->
       TacApply (a,ev,List.map (subst_glob_with_bindings subst) cb,cl)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,subst_glob_with_bindings subst cb,
                Option.map (subst_glob_with_bindings subst) cbo)
-  | TacElimType c -> TacElimType (subst_glob_constr subst c)
   | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb)
-  | TacCaseType c -> TacCaseType (subst_glob_constr subst c)
   | TacFix (idopt,n) as x -> x
   | TacMutualFix (id,n,l) ->
       TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
   | TacCofix idopt as x -> x
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
-  | TacCut c -> TacCut (subst_glob_constr subst c)
   | TacAssert (b,na,c) ->
       TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c)
   | TacGeneralize cl ->
@@ -177,7 +172,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
       let l = List.map (subst_or_var (subst_ind subst)) l in
       TacDecompose (l,subst_glob_constr subst c)
   | TacSpecialize (n,l) -> TacSpecialize (n,subst_glob_with_bindings subst l)
-  | TacLApply c -> TacLApply (subst_glob_constr subst c)
 
   (* Context management *)
   | TacClear _ as x -> x