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.

8 files changed, 61 insertions, 67 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index abc0d31a93..6a413ca313 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -310,23 +310,15 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >>
   | Tacexpr.TacExact c ->
       <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
-  | Tacexpr.TacExactNoCheck c ->
-      <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
-  | Tacexpr.TacVmCastNoCheck c ->
-      <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
   | Tacexpr.TacApply (b,false,cb,None) ->
       <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >>
   | Tacexpr.TacElim (false,cb,cbo) ->
       let cb = mlexpr_of_constr_with_binding cb in
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
       <:expr< Tacexpr.TacElim False $cb$ $cbo$ >>
-  | Tacexpr.TacElimType c ->
-      <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >>
   | Tacexpr.TacCase (false,cb) ->
       let cb = mlexpr_of_constr_with_binding cb in
       <:expr< Tacexpr.TacCase False $cb$ >>
-  | Tacexpr.TacCaseType c ->
-      <:expr< Tacexpr.TacCaseType $mlexpr_of_constr c$ >>
   | Tacexpr.TacFix (ido,n) ->
       let ido = mlexpr_of_ident_option ido in
       let n = mlexpr_of_int n in
@@ -346,8 +338,6 @@ let rec mlexpr_of_atomic_tactic = function
       let l = mlexpr_of_list f l in
       <:expr< Tacexpr.TacMutualCofix $id$ $l$ >>
 
-  | Tacexpr.TacCut c ->
-      <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
   | Tacexpr.TacAssert (t,ipat,c) ->
       let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in
       <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 532786fd37..5a7a20ef63 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -106,19 +106,14 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacIntrosUntil of quantified_hypothesis
   | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
-  | TacExactNoCheck of 'trm
-  | TacVmCastNoCheck of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings list *
       ('nam * intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings * 'trm with_bindings option
-  | TacElimType of 'trm
   | TacCase of evars_flag * 'trm with_bindings
-  | TacCaseType of 'trm
   | TacFix of Id.t option * int
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacCofix of Id.t option
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
-  | TacCut of 'trm
   | TacAssert of
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
       intro_pattern_expr located option * 'trm
@@ -136,7 +131,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacDecomposeOr of 'trm
   | TacDecompose of 'ind list * 'trm
   | TacSpecialize of int option * 'trm with_bindings
-  | TacLApply of 'trm
 
   (* Automation tactics *)
   | TacTrivial of debug * 'trm list * string list option
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d1620ca8a7..4ac7a5bffe 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -533,8 +533,6 @@ GEXTEND Gram
       | IDENT "intro" -> TacIntroMove (None, MoveLast)
 
       | IDENT "exact"; c = constr -> TacExact c
-      | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
-      | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
 
       | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
           inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp)
@@ -548,10 +546,8 @@ GEXTEND Gram
           TacElim (false,cl,el)
       | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
           TacElim (true,cl,el)
-      | IDENT "elimtype"; c = constr -> TacElimType c
       | IDENT "case"; icl = induction_clause_list -> mkTacCase false icl
       | IDENT "ecase"; icl = induction_clause_list -> mkTacCase true icl
-      | IDENT "casetype"; c = constr -> TacCaseType c
       | "fix"; n = natural -> TacFix (None,n)
       | "fix"; id = ident; n = natural -> TacFix (Some id,n)
       | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
@@ -587,7 +583,6 @@ GEXTEND Gram
       | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
 	  TacAssert (None,ipat,c)
 
-      | IDENT "cut"; c = constr -> TacCut c
       | IDENT "generalize"; c = constr ->
 	  TacGeneralize [((AllOccurrences,c),Names.Anonymous)]
       | IDENT "generalize"; c = constr; l = LIST1 constr ->
@@ -601,7 +596,6 @@ GEXTEND Gram
 
       | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
 	  TacSpecialize (n,lcb)
-      | IDENT "lapply"; c = constr -> TacLApply c
 
       (* Derived basic tactics *)
       | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c7644f8c60..0ea8b4048c 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -650,8 +650,6 @@ and pr_atom1 = function
       hov 1 (str"intro" ++ pr_opt pr_id ido ++
              Miscprint.pr_move_location pr_ident hto)
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
-  | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
-  | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
   | TacApply (a,ev,cb,inhyp) ->
       hov 1 ((if a then mt() else str "simple ") ++
              str (with_evars ev "apply") ++ spc () ++
@@ -660,10 +658,8 @@ and pr_atom1 = function
   | TacElim (ev,cb,cbo) ->
       hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++
         pr_opt pr_eliminator cbo)
-  | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c)
   | TacCase (ev,cb) ->
       hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
-  | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
   | TacMutualFix (id,n,l) ->
       hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
@@ -672,7 +668,6 @@ and pr_atom1 = function
   | TacMutualCofix (id,l) ->
       hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
              str"with " ++ prlist_with_sep spc pr_cofix_tac l)
-  | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c)
   | TacAssert (Some tac,ipat,c) ->
       hov 1 (str "assert" ++
              pr_assumption pr_lconstr pr_constr ipat c ++
@@ -734,8 +729,6 @@ and pr_atom1 = function
   | TacSpecialize (n,c) ->
       hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++
              pr_with_bindings c)
-  | TacLApply c ->
-      hov 1 (str "lapply" ++ pr_constrarg c)
 
   (* Automation tactics *)
   | TacTrivial (_,[],Some []) as x -> pr_atom0 x
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