From ca29570a25be8f9b8757399f5f0b72b4a9bd5e43 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 31 Mar 2003 21:18:27 +0000 Subject: Ajout d'un message à FailTac; localisation des appels à des tactiques définies MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3824 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/newtauto.ml4 | 47 ++++++++++++++++++++++++++--------------------- 1 file changed, 26 insertions(+), 21 deletions(-) (limited to 'tactics/newtauto.ml4') 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 -- cgit v1.2.3