Ajout d'un message à FailTac; localisation des appels à des tactiques définies

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

3 files changed, 70 insertions, 45 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index fb6485481..9eb192f4d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -850,7 +850,8 @@ let compileAutoArg contac = function
 		 then 
 		   tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac] 
                  else 
-		   tclFAIL 0) ctx) g)
+		   tclFAIL 0 ((string_of_id id)^"is not a conjunction"))
+	     ctx) g)
   | UsingTDB ->  
       (tclTHEN  
          (Tacticals.tryAllClauses 
diff --git a/tactics/newtauto.ml4 b/tactics/newtauto.ml4
index 04ecc36fa..11958a0ea 100644
--- a/tactics/newtauto.ml4
+++ b/tactics/newtauto.ml4
@@ -31,11 +31,12 @@ let myprint env rc t=
 	let ppstr=Printer.prterm_env env2 t in
 	Pp.msgnl ppstr
 
-let tacinj tac=valueIn (VTactic (tac))
+let tacinj tac=valueIn (VTactic (dummy_loc,tac))
 
 let tclATMOSTn n tac1 gl=
   let result=tac1 gl in
-    if List.length (fst result).it <= n then result else (tclFAIL 0 gl)
+    if List.length (fst result).it <= n then result
+    else (tclFAIL 0 "Not enough subgoals" gl)
 
 let tclTRY_REV_HYPS (tac : constr->tactic) gl = 
   tclTRY_sign tac (List.rev (Tacmach.pf_hyps gl)) gl
@@ -81,9 +82,9 @@ let rule_named_llarrow id gl=
     (try let nam=destVar id in
     let body=Tacmach.pf_get_hyp_typ gl nam in
     let (_,cc,c)=destProd body in
-    if dependent (mkRel 1) c then tclFAIL 0 else
+    if dependent (mkRel 1) c then tclFAIL 0 "" else
     let (_,ta,b)=destProd cc in
-    if dependent (mkRel 1) b then tclFAIL 0 else 
+    if dependent (mkRel 1) b then tclFAIL 0 "" else 
     let tb=pop b and tc=pop c in
     let d=mkLambda (Anonymous,tb,
     mkApp (id,[|mkLambda (Anonymous,(lift 1 ta),(mkRel 2))|])) in
@@ -92,7 +93,7 @@ let rule_named_llarrow id gl=
 	[tclTHEN intro (clear [nam]);
 	 tclTHENS (cut cc) 
 	   [exact_check id; tclTHENLIST [generalize [d];intro;clear [nam]]]]
-   with Invalid_argument _ -> tclFAIL 0) gl
+   with Invalid_argument _ -> tclFAIL 0 "") gl
 
 let rule_llarrow tac=
   tclTRY_REV_HYPS 
@@ -102,16 +103,18 @@ let rule_llarrow tac=
 let rule_rind tac gl=
   (let (hdapp,args)=decompose_app gl.it.Evd.evar_concl in
      try let ind=destInd hdapp in
-       if isrec ind then tclFAIL 0 else
+       if isrec ind then tclFAIL 0 "Found a recursive inductive type" else
 	 any_constructor (Some tac)
-     with Invalid_argument _ -> tclFAIL 0) gl 
+     with Invalid_argument _ -> tclFAIL 0 "") gl 
   
 let rule_rind_rev (* b *) gl=  
   (let (hdapp,args)=decompose_app gl.it.Evd.evar_concl in
      try let ind=destInd hdapp in
-       if (isrec ind)(* || (not b && (nhyps ind).(0)>1) *)then tclFAIL 0 else
+       if (isrec ind)(* || (not b && (nhyps ind).(0)>1) *) then
+	 tclFAIL 0 "Found a recursive inductive type"
+       else
 	 simplest_split
-     with Invalid_argument _ -> tclFAIL 0) gl 
+     with Invalid_argument _ -> tclFAIL 0 "") gl 
   (* this rule increases the number of goals 
 if the unique constructor has several hyps.
 i.e if (nhyps ind).(0)>1 *)
@@ -120,8 +123,8 @@ let rule_named_false id gl=
   (try let nam=destVar id in
    let body=Tacmach.pf_get_hyp_typ gl nam in
      if is_empty_type body then (simplest_elim id)
-     else tclFAIL 0
-   with Invalid_argument _ -> tclFAIL 0) gl
+     else tclFAIL 0 "Found an non empty type"
+   with Invalid_argument _ -> tclFAIL 0 "") gl
 
 let rule_false=tclTRY_REV_HYPS rule_named_false
 
@@ -133,11 +136,13 @@ let rule_named_lind (*b*) id gl=
    (*let nconstr=
     if b then 0 else 
       Array.length (snd (Global.lookup_inductive ind)).mind_consnames in *)
-     if (isrec ind) (*|| (nconstr>1)*) then tclFAIL 0 else 
+     if (isrec ind) (*|| (nconstr>1)*) then 
+       tclFAIL 0 "Found a recursive inductive type"
+     else 
        let l=nhyps ind in
        let f n= tclDO n intro in
 	 tclTHENSV (tclTHEN (simplest_elim id) (clear [nam])) (Array.map f l)
-   with Invalid_argument _ -> tclFAIL 0) gl
+   with Invalid_argument _ -> tclFAIL 0 "") gl
   
 let rule_lind (* b *) =
   tclTRY_REV_HYPS (rule_named_lind (* b *))
@@ -147,14 +152,14 @@ let rule_named_llind id gl=
     (try let nam=destVar id in 
     let body=Tacmach.pf_get_hyp_typ gl nam in
     let (_,xind,b) =destProd body in
-    if dependent (mkRel 1) b then tclFAIL 0 else  
+    if dependent (mkRel 1) b then tclFAIL 0 "Found a dependent product" else  
     let (hdapp,args) = decompose_app xind in
     let vargs=Array.of_list args in
     let ind=destInd hdapp in
-    if isrec ind then tclFAIL 0 else
+    if isrec ind then tclFAIL 0 "" else
     let (mib,mip) = Global.lookup_inductive ind in
     let n=mip.mind_nparams in
-    if n<>(List.length args) then tclFAIL 0 else
+    if n<>(List.length args) then tclFAIL 0 "" else
     let p=nhyps ind in
     let types= mip.mind_nf_lc in
     let names= mip.mind_consnames in
@@ -173,7 +178,7 @@ let rule_named_llind id gl=
     let newhyps=List.map myterm (interval 0 ((Array.length p)-1)) in
      tclTHEN (generalize newhyps)
 	(tclTHEN (clear [nam]) (tclDO (Array.length p) intro))
-	with Invalid_argument _ ->tclFAIL 0) gl
+	with Invalid_argument _ ->tclFAIL 0 "") gl
 
 let rule_llind=tclTRY_REV_HYPS rule_named_llind
 
@@ -196,19 +201,19 @@ let rec newtauto b stac gl=
 		rule_llarrow (tclSOLVE [newtauto b stac]);
 		rule_rind (tclSOLVE [newtauto b stac]);
 		rule_rforall (tclSOLVE [newtauto b stac]);
-		if b then tclFAIL 0 else (rule_simp_larrow stac)])
+		if b then tclFAIL 0 "" else (rule_simp_larrow stac)])
 		(tclPROGRESS (newtauto b stac)))
 		stac)) gl
  
 let q_elim tac=
-  let vtac=Tacexpr.TacArg (valueIn (VTactic tac)) in	
+  let vtac=Tacexpr.TacArg (valueIn (VTactic (dummy_loc,tac))) in	
   interp <:tactic<
   Match Context With 
     [x:?1;H:?1->?|-?]->
       Generalize (H x);Clear H;$vtac>>
 
 let rec lfo n=
-  if n=0 then (tclFAIL 0) else
+  if n=0 then (tclFAIL 0 "NewLinearIntuition failed") else
     let p=if n<0 then n else (n-1) in
     let lfo_rec=q_elim (fun gl->lfo p gl) in
       newtauto true lfo_rec
@@ -230,7 +235,7 @@ TACTIC EXTEND Intuition1
 END
 
 TACTIC EXTEND NewTauto
-  [ "NewTauto" ] -> [ newtauto true (tclFAIL 0) ]
+  [ "NewTauto" ] -> [ newtauto true (tclFAIL 0 "NewTauto failed") ]
 END
 
 TACTIC EXTEND NewLinearIntuition
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 87d756e1f..c28e21e79 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -65,7 +65,7 @@ type ltac_type =
 
 (* Values for interpretation *)
 type value =
-  | VTactic of tactic  (* For mixed ML/Ltac tactics (e.g. Tauto) *)
+  | VTactic of loc * tactic  (* For mixed ML/Ltac tactics (e.g. Tauto) *)
   | VRTactic of (goal list sigma * validation) (* For Match results *)
                                                (* Not a true value *)
   | VFun of (identifier * value) list * identifier option list *raw_tactic_expr
@@ -78,6 +78,17 @@ type value =
   | VConstr_context of constr
   | VRec of value ref
 
+let locate_tactic_call loc = function
+  | VTactic (_,t) -> VTactic (loc,t)
+  | v -> v
+
+let catch_error loc tac g =
+  try tac g
+  with e when loc <> dummy_loc ->
+    match e with
+      |	Stdpp.Exc_located (_,e) -> raise (Stdpp.Exc_located (loc,e))
+      |	e -> raise (Stdpp.Exc_located (loc,e))
+
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign =
   { lfun : (identifier * value) list;
@@ -591,7 +602,7 @@ and glob_tactic_seq (lfun,lmeta,sigma,env as ist) = function
   | TacMatch (c,lmr) ->
       lfun, TacMatch (glob_constr_may_eval ist c,glob_match_rule ist lmr)
   | TacId -> lfun, TacId
-  | TacFail n as x -> lfun, x
+  | TacFail _ as x -> lfun, x
   | TacProgress tac -> lfun, TacProgress (glob_tactic ist tac)
   | TacAbstract (tac,s) -> lfun, TacAbstract (glob_tactic ist tac,s)
   | TacThen (t1,t2) ->
@@ -745,11 +756,15 @@ let rec read_match_rule evc env lfun = function
 (* For Match Context and Match *)
 exception No_match
 exception Not_coherent_metas
-exception Eval_fail
+exception Eval_fail of string
+
+let is_failure = function
+  | FailError _ | Stdpp.Exc_located (_,FailError _) -> true
+  | _ -> false
 
 let is_match_catchable = function
-  | No_match | Eval_fail | FailError _ -> true
-  | e -> Logic.catchable_exception e
+  | No_match | Eval_fail _ -> true
+  | e -> is_failure e or Logic.catchable_exception e
 
 (* Verifies if the matched list is coherent with respect to lcm *)
 let rec verify_metas_coherence gl lcm = function
@@ -1112,7 +1127,7 @@ let rec val_interp ist gl tac =
     | TacMatch (c,lmr) -> match_interp ist gl c lmr
     | TacArg a -> tacarg_interp ist gl a
     (* Delayed evaluation *)
-    | t -> VTactic (eval_tactic ist t)
+    | t -> VTactic (dummy_loc,eval_tactic ist t)
   in 
   match ist.debug with
   | DebugOn | Run _ ->
@@ -1121,9 +1136,7 @@ let rec val_interp ist gl tac =
   | _ -> value_interp ist
 
 and eval_tactic ist = function
-  | TacAtom (loc,t) -> fun gl ->
-      (try interp_atomic ist gl t gl
-       with e -> Stdpp.raise_with_loc loc e)
+  | TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl
   | TacFun (it,body) -> assert false
   | TacLetRecIn (lrc,u) -> assert false
   | TacLetIn (l,u) -> assert false
@@ -1131,7 +1144,7 @@ and eval_tactic ist = function
   | TacMatchContext _ -> assert false
   | TacMatch (c,lmr) -> assert false
   | TacId -> tclIDTAC
-  | TacFail n -> tclFAIL n
+  | TacFail (n,s) -> tclFAIL n s
   | TacProgress tac -> tclPROGRESS (tactic_interp ist tac)
   | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (tactic_interp ist tac)
   | TacThen (t1,t2) -> tclTHEN (tactic_interp ist t1) (tactic_interp ist t2)
@@ -1148,8 +1161,11 @@ and eval_tactic ist = function
   | TacArg a -> assert false
 
 and interp_ltac_qualid is_applied ist gl (loc,qid as lqid) =
-  try val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup qid)
-  with Not_found -> interp_pure_qualid is_applied (pf_env gl) lqid
+  try 
+    let v = val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup qid) in
+    if is_applied then v else locate_tactic_call loc v
+  with
+      Not_found -> interp_pure_qualid is_applied (pf_env gl) lqid
 
 and interp_ltac_reference isapplied ist gl = function
   | Ident (loc,id) -> 
@@ -1194,7 +1210,8 @@ and app_interp ist gl fv largs loc =
       let (newlfun,lvar,lval)=head_with_value (var,largs) in
       if lvar=[] then
 	let v = val_interp { ist with lfun=newlfun@olfun } gl body in
-        if lval=[] then v else app_interp ist gl v lval loc
+        if lval=[] then locate_tactic_call loc v
+	else app_interp ist gl v lval loc
       else
         VFun(newlfun@olfun,lvar,body)
     | _ ->
@@ -1205,7 +1222,7 @@ and app_interp ist gl fv largs loc =
 and tactic_of_value vle g =
   match vle with
   | VRTactic res -> res
-  | VTactic tac -> tac g
+  | VTactic (loc,tac) -> catch_error loc tac g
   | VFun _ -> error "A fully applied tactic is expected"
   | _ -> raise NotTactic
 
@@ -1213,13 +1230,15 @@ and tactic_of_value vle g =
 and eval_with_fail interp tac goal =
   try
     (match interp goal tac with
-    | VTactic tac -> VRTactic (tac goal)
+    | VTactic (loc,tac) -> VRTactic (catch_error loc tac goal)
     | a -> a)
-  with | FailError lvl ->
-    if lvl = 0 then
-      raise Eval_fail
-    else
-      raise (FailError (lvl - 1))
+  with
+    | Stdpp.Exc_located (_,FailError (0,s)) | FailError (0,s) ->
+	raise (Eval_fail s)
+    | Stdpp.Exc_located (s',FailError (lvl,s)) ->
+	raise (Stdpp.Exc_located (s',FailError (lvl - 1, s)))
+    | FailError (lvl,s) ->
+	raise (FailError (lvl - 1, s))
 
 (* Interprets recursive expressions *)
 and letrec_interp ist gl lrc u =
@@ -1301,7 +1320,7 @@ and match_context_interp ist g lr lmr =
       else
         apply_hyps_context ist env goal mt lgoal mhyps hyps
     with
-    | (FailError _) as e -> raise e
+    | e when is_failure e -> raise e
     | NextOccurrence _ -> raise No_match
     | e when is_match_catchable e ->
       apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
@@ -1341,7 +1360,7 @@ and match_context_interp ist g lr lmr =
           begin 
             (match e with
             | No_match -> db_matching_failure ist.debug
-            | Eval_fail -> db_eval_failure ist.debug
+            | Eval_fail s -> db_eval_failure ist.debug s
             | _ -> db_logic_failure ist.debug e);
             apply_match_context ist env goal (nrs+1) (List.tl lex) tl
           end)
@@ -1385,7 +1404,7 @@ and apply_hyps_context ist env goal mt lgmatch mhyps hyps =
             apply_hyps_context_rec ist mt
               (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
            with
-           | (FailError _) as e -> raise e
+           | e when is_failure e -> raise e
 	   | e when is_match_catchable e -> 
              (match noccopt with
              | None ->