L'application de ltac attend une référence; meilleure protection contre

les erreurs


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3141 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 45 insertions, 42 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 859865ee4..a7c37160a 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -207,7 +207,7 @@ GEXTEND Gram
 	  ConstrMayEval (ConstrContext (id,c))
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
-      | qid = lqualid -> qid
+      | qid = lqualid -> Reference qid
       | ta = tactic_arg0 -> ta ] ]
   ;
   tactic_arg1:
@@ -218,13 +218,13 @@ GEXTEND Gram
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
       | qid = lqualid; la = LIST1 tactic_arg0 -> TacCall (loc,qid,la)
-      | qid = lqualid -> qid
+      | qid = lqualid -> Reference qid
       | ta = tactic_arg0 -> ta ] ]
   ;
   tactic_arg0:
     [ [ "("; a = tactic_expr; ")" -> Tacexp a
       | "()" -> TacVoid
-      | qid = lqualid -> qid
+      | qid = lqualid -> Reference qid
       | n = Prim.integer -> Integer n
       | id = METAIDENT -> MetaIdArg (loc,id)
       |	"?" -> ConstrMayEval (ConstrTerm <:ast< (ISEVAR) >>)
@@ -232,11 +232,7 @@ GEXTEND Gram
       |	"'"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ]
   ;
   lqualid:
-    [ [ qid = Prim.reference -> 
-(*  match Nametab.repr_qualid qid with
-  | (dir,id) when dir = Nameops.empty_dirpath -> Identifier id
-  | _ -> Qualid *) Reference qid
-    ] ]
+    [ [ ref = Prim.reference -> ref ] ]
   ;
 
   (* Definitions for tactics *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 28e51dcd1..a448166e1 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -558,25 +558,24 @@ and pr6 = function
 
   | TacArg c -> pr_tacarg c
 
+and pr_reference = function 
+  | RQualid (_,qid) -> pr_qualid qid
+  | RIdent (_,id) -> pr_id id
+
 and pr_tacarg0 = function
   | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
   | MetaNumArg (_,n) -> str ("?" ^ string_of_int n )
   | MetaIdArg (_,s) -> str ("$" ^ s)
   | TacVoid -> str "()"
-  | Reference (RQualid (_,qid)) -> pr_qualid qid
-  | Reference (RIdent (_,id)) -> pr_id id
+  | Reference r -> pr_reference r
   | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c
   | ConstrMayEval c -> pr_may_eval pr_constr c
   | Integer n -> int n
-(*
-  | Tac of
-      'c * (Coqast.t,qualid or_metanum, identifier or_metaid) gen_tactic_expr
-*)
   | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")"
 
 and pr_tacarg1 = function
   | TacCall (_,f,l) ->
-      hov 0 (pr_tacarg0 f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l)
+      hov 0 (pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l)
   | Tacexp t -> !pr_rawtac t
   | t -> pr_tacarg0 t
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 412625071..8729dce06 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -489,7 +489,7 @@ and mlexpr_of_tactic_arg = function
       <:expr< Tacexpr.AstTacArg $mlexpr_of_ast t$ >>
 *)
   | Tacexpr.TacCall (loc,t,tl) ->
-      <:expr< Tacexpr.TacCall loc $mlexpr_of_tactic_arg t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
+      <:expr< Tacexpr.TacCall loc $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
   | Tacexpr.Tacexp t ->
       <:expr< Tacexpr.Tacexp $mlexpr_of_tactic t$ >>
   | Tacexpr.ConstrMayEval c ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index eefee41f5..b63588aaa 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -209,7 +209,8 @@ and ('constr,'cst,'ind,'id) gen_tactic_arg =
   | ConstrMayEval  of 'constr may_eval
   | Reference      of reference_expr
   | Integer        of int
-  | TacCall of loc * ('constr,'cst,'ind,'id) gen_tactic_arg * ('constr,'cst,'ind,'id) gen_tactic_arg list
+  | TacCall        of loc *
+      reference_expr * ('constr,'cst,'ind,'id) gen_tactic_arg list
   | Tacexp of raw_tactic_expr
 
 type raw_atomic_tactic_expr =
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 92db61f07..a00083938 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -149,7 +149,8 @@ type located_destructor_pattern =
 type destructor_data = {
   d_pat : located_destructor_pattern;
   d_pri : int;
-  d_code : raw_tactic_expr } (* should be of phylum tactic *)
+  d_code : identifier option * raw_tactic_expr (* should be of phylum tactic *)
+}
 
 type t = (identifier,destructor_data) Nbtermdn.t
 type frozen_t = (identifier,destructor_data) Nbtermdn.frozen_t
@@ -206,12 +207,14 @@ let ((inDD : destructor_data_object->obj),
                     export_function = export_dd }
     
 let add_destructor_hint na loc pat pri code =
-  begin match loc, code with
-    | HypLocation _, TacFun ([id],body) -> ()
-    | ConclLocation _, _ -> ()
-    | _ ->
-	errorlabstrm "add_destructor_hint"
-          (str "The tactic should be a function of the hypothesis name") end;
+  let code =
+    begin match loc, code with
+      | HypLocation _, TacFun ([id],body) -> (id,body)
+      | ConclLocation _, _ -> (None, code)
+      | _ ->
+	  errorlabstrm "add_destructor_hint"
+          (str "The tactic should be a function of the hypothesis name") end
+  in
   let (_,pat) = Astterm.interp_constrpattern Evd.empty (Global.env()) pat in
   let pat = match loc with
     | HypLocation b ->
@@ -246,11 +249,13 @@ let applyDestructor cls discard dd gls =
   let mvb =
     try match_dpat dd.d_pat cls gls
     with PatternMatchingFailure -> error "No match" in
-  let tac = match cls with
-    | Some id -> 
+  let tac = match cls, dd.d_code with
+    | Some id, (Some x, tac) -> 
 	let arg = Reference (RIdent (dummy_loc,id)) in
-	TacCall (dummy_loc, Tacexp dd.d_code, [arg])
-    | None -> Tacexp dd.d_code in
+        TacLetIn ([(dummy_loc, x), None, arg], tac)
+    | None, (None, tac) -> tac
+    | _, (Some _,_) -> error "Destructor expects an hypothesis"
+    | _, (None,_) -> error "Destructor is for conclusion" in
   let discard_0 =
     match (cls,dd.d_pat) with
       | (Some id,HypLocation(discardable,_,_)) ->
@@ -258,7 +263,7 @@ let applyDestructor cls discard dd gls =
       | (None,ConclLocation _) -> tclIDTAC
       | _ -> error "ApplyDestructor" 
   in
-  tclTHEN (!forward_tac_interp (TacArg tac)) discard_0 gls
+  tclTHEN (!forward_tac_interp tac) discard_0 gls
 
 
 (* [DHyp id gls]
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3c50c2672..71ec78b4c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -608,7 +608,7 @@ and glob_tacarg ist = function
   | MetaNumArg (loc,n) -> MetaNumArg (loc,glob_metanum ist loc n)
   | MetaIdArg (loc,_) -> error_syntactic_metavariables_not_allowed loc
   | TacCall (loc,f,l) ->
-      TacCall (loc,glob_tacarg ist f,List.map (glob_tacarg ist) l)
+      TacCall (loc,glob_ltac_reference ist f,List.map (glob_tacarg ist) l)
   | Tacexp t -> Tacexp (glob_tactic ist t)
   | TacDynamic(_,t) as x ->
       (match tag t with
@@ -905,22 +905,23 @@ let hyp_or_metanum_interp ist = function
 (* To avoid to move to much simple functions in the big recursive block *)
 let forward_vcontext_interp = ref (fun ist v -> failwith "not implemented")
 
-let interp_pure_qualid ist (loc,qid) =
+let interp_pure_qualid is_applied ist (loc,qid) =
   try VConstr (constr_of_reference (find_reference ist qid))
   with Not_found ->
     let (dir,id) = repr_qualid qid in
-    if dir = empty_dirpath then VIdentifier id
+    if not is_applied & dir = empty_dirpath then VIdentifier id
     else user_err_loc (loc,"interp_pure_qualid",str "Unknown reference")
 
-let interp_ltac_qualid ist (loc,qid as lqid) =
+let interp_ltac_qualid is_applied ist (loc,qid as lqid) =
   try (!forward_vcontext_interp ist (lookup qid))
-  with Not_found -> interp_pure_qualid ist lqid
+  with Not_found -> interp_pure_qualid is_applied ist lqid
 
-let interp_ltac_reference ist = function
+let interp_ltac_reference isapplied ist = function
   | RIdent (loc,id) -> 
       (try unrec (List.assoc id ist.lfun)
-      with | Not_found -> interp_ltac_qualid ist (loc,make_short_qualid id))
-  | RQualid qid -> interp_ltac_qualid ist qid
+      with | Not_found ->
+        interp_ltac_qualid isapplied ist (loc,make_short_qualid id))
+  | RQualid qid -> interp_ltac_qualid isapplied ist qid
 
 (* Interprets a qualified name *)
 let eval_qualid ist (loc,qid as locqid) =
@@ -929,7 +930,7 @@ let eval_qualid ist (loc,qid as locqid) =
     if dir = empty_dirpath then unrec (List.assoc id ist.lfun) 
     else raise Not_found
   with | Not_found ->
-    interp_pure_qualid ist locqid
+    interp_pure_qualid false ist locqid
 
 let qualid_interp ist qid =
   let v = eval_qualid ist qid in
@@ -1149,7 +1150,7 @@ and eval_tactic ist = function
 
 and tacarg_interp ist = function
   | TacVoid -> VVoid
-  | Reference r -> interp_ltac_reference ist r
+  | Reference r -> interp_ltac_reference false ist r
   | Integer n -> VInteger n
   | ConstrMayEval c -> VConstr (constr_interp_may_eval ist c)
   | MetaNumArg (_,n) -> VConstr (List.assoc n ist.lmatch)
@@ -1159,7 +1160,7 @@ and tacarg_interp ist = function
       with
         | Not_found -> error_syntactic_metavariables_not_allowed loc)
   | TacCall (loc,f,l) ->
-      let fv = tacarg_interp ist f
+      let fv = interp_ltac_reference true ist f
       and largs = List.map (tacarg_interp ist) l in
       app_interp ist fv largs loc
   | Tacexp t -> val_interp ist t
@@ -1209,6 +1210,7 @@ and tactic_of_value vle g =
   | VFTactic (largs,f) -> (f largs g) 
   | VRTactic res -> res
   | VTactic tac -> tac g
+  | VFun _ -> error "A fully applied tactic is expected"
   | _ -> raise NotTactic
 
 (* Evaluation with FailError catching *)
@@ -1278,7 +1280,7 @@ and letin_interp ist = function
        with | NotTactic ->
          delete_proof id;
          errorlabstrm "Tacinterp.letin_interp"
-         (str "Term or tactic expected"))
+         (str "Term or fully applied tactic expected in Let"))
 
 (* Interprets the clauses of a LetCut *)
 and letcut_interp ist = function
@@ -1333,7 +1335,7 @@ and letcut_interp ist = function
        with | NotTactic ->
          delete_proof id;
          errorlabstrm "Tacinterp.letcut_interp"
-         (str "Term or tactic expected")))
+         (str "Term or fully applied tactic expected in Let")))
 
 (* Interprets the Match Context expressions *)
 and match_context_interp ist lr lmr g =