From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- tactics/auto.ml | 11 ++++---- tactics/autorewrite.ml | 12 ++++++--- tactics/class_tactics.ml4 | 7 ++++-- tactics/eauto.ml4 | 3 ++- tactics/equality.ml | 5 ++-- tactics/extratactics.ml4 | 2 +- tactics/hipattern.ml4 | 10 ++++++-- tactics/inv.ml | 4 +-- tactics/rewrite.ml4 | 25 ++++++++++-------- tactics/tacinterp.ml | 64 +++++++++++++++++++++++++---------------------- tactics/tactics.ml | 15 +++++++---- 11 files changed, 95 insertions(+), 63 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index f7d63dcd..44fea151 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -829,7 +829,8 @@ let prepare_hint env (sigma,c) = let path_of_constr_expr c = match c with - | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny) + | Topconstr.CRef r -> + (try PathHints [global r] with e when Errors.noncritical e -> PathAny) | _ -> PathAny let interp_hints h = @@ -1170,9 +1171,9 @@ let tclLOG (dbg,depth,trace) pp tac = let out = tac gl in msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); out - with e -> + with reraise -> msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); - raise e + raise reraise end | Info -> (* For "info (trivial/auto)", we store a log trace *) @@ -1181,9 +1182,9 @@ let tclLOG (dbg,depth,trace) pp tac = let out = tac gl in trace := (depth, Some pp) :: !trace; out - with e -> + with reraise -> trace := (depth, None) :: !trace; - raise e + raise reraise end (** For info, from the linear trace information, we reconstitute the part diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 039f022d..8e1d7cbf 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -208,8 +208,14 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl = (* Functions necessary to the library object declaration *) let cache_hintrewrite (_,(rbase,lrl)) = - let base = try find_base rbase with _ -> HintDN.empty in - let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in + let base = + try find_base rbase + with e when Errors.noncritical e -> HintDN.empty + in + let max = + try fst (Util.list_last (HintDN.find_all base)) + with e when Errors.noncritical e -> 0 + in let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab @@ -248,7 +254,7 @@ let evd_convertible env evd x y = try ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true (* try ignore(Evarconv.the_conv_x env x y evd); true *) - with _ -> false + with e when Errors.noncritical e -> false let decompose_applied_relation metas env sigma c ctype left2right = let find_rel ty = diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index cf4a267f..d05ae680 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -685,7 +685,7 @@ let resolve_typeclass_evars debug m env evd filter split fail = let evd = try Evarconv.consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env evd - with _ -> evd + with e when Errors.noncritical e -> evd in resolve_all_evars debug m env (initial_select_evars filter) evd split fail @@ -776,7 +776,10 @@ END let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl = try - let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in + let dbs = list_map_filter + (fun db -> try Some (Auto.searchtable_map db) + with e when Errors.noncritical e -> None) dbs + in let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 68dd5dba..6981a733 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -205,7 +205,8 @@ module SearchProblem = struct (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls,pptac) :: aux tacl - with e -> Refiner.catch_failerror e; aux tacl + with e when Errors.noncritical e -> + Refiner.catch_failerror e; aux tacl in aux l (* Ordering of states is lexicographic on depth (greatest first) then diff --git a/tactics/equality.ml b/tactics/equality.ml index a352355b..1c5e4b2f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -334,7 +334,8 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac try rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl - with e -> (* Try to see if there's an equality hidden *) + with e when Errors.noncritical e -> + (* Try to see if there's an equality hidden *) let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) match match_with_equality_type t' with @@ -1156,7 +1157,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause = ] (* not a dep eq or no decidable type found *) ) else (raise Not_dep_pair) - ) with _ -> + ) with e when Errors.noncritical e -> inject_at_positions env sigma u eq_clause posns (fun _ -> intros_pattern no_move ipats) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f5fcb736..f6ecb47c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -606,7 +606,7 @@ let hResolve_auto id c t gl = hResolve id c n t gl with | UserError _ as e -> raise e - | _ -> resolve_auto (n+1) + | e when Errors.noncritical e -> resolve_auto (n+1) in resolve_auto 1 diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 47e3b7ca..c6f32ce2 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -64,9 +64,12 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) (* Test dependencies *) +(* NB: we consider also the let-in case in the following function, + since they may appear in types of inductive constructors (see #2629) *) + let rec has_nodep_prod_after n c = match kind_of_term c with - | Prod (_,_,b) -> + | Prod (_,_,b) | LetIn (_,_,_,b) -> ( n>0 || not (dependent (mkRel 1) b)) && (has_nodep_prod_after (n-1) b) | _ -> true @@ -355,7 +358,10 @@ let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ] let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ] let match_eq eqn eq_pat = - let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in + let pat = + try Lazy.force eq_pat + with e when Errors.noncritical e -> raise PatternMatchingFailure + in match matches pat eqn with | [(m1,t);(m2,x);(m3,y)] -> assert (m1 = meta1 & m2 = meta2 & m3 = meta3); diff --git a/tactics/inv.ml b/tactics/inv.ml index b7f6addc..e4b3bdb1 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -497,7 +497,7 @@ let wrap_inv_error id = function (* The most general inversion tactic *) let inversion inv_kind status names id gls = try (raw_inversion inv_kind id status names) gls - with e -> wrap_inv_error id e + with e when Errors.noncritical e -> wrap_inv_error id e (* Specializing it... *) @@ -540,7 +540,7 @@ let invIn k names ids id gls = inversion (false,k) NoDep names id; intros_replace_ids]) gls - with e -> wrap_inv_error id e + with e when Errors.noncritical e -> wrap_inv_error id e let invIn_gen k names idl = try_intros_until (invIn k names idl) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index b90a911a..98885af8 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -121,7 +121,7 @@ let is_applied_rewrite_relation env sigma rels t = let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in let _ = Typeclasses.resolve_one_typeclass env' evd inst in Some (it_mkProd_or_LetIn t rels) - with _ -> None) + with e when Errors.noncritical e -> None) | _ -> None let _ = @@ -145,11 +145,14 @@ let build_signature evars env m (cstrs : (types * types option) option list) new_cstr_evar evars env (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t in - let mk_relty evars env ty obj = + let mk_relty evars newenv ty obj = match obj with | None | Some (_, None) -> let relty = mk_relation ty in - new_evar evars env relty + if closed0 ty then + let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in + new_evar evars env' relty + else new_evar evars newenv relty | Some (x, Some rel) -> evars, rel in let rec aux env evars ty l = @@ -227,7 +230,7 @@ let cstrevars evars = snd evars let evd_convertible env evd x y = try ignore(Evarconv.the_conv_x env x y evd); true - with _ -> false + with e when Errors.noncritical e -> false let rec decompose_app_rel env evd t = match kind_of_term t with @@ -493,7 +496,7 @@ let rec apply_pointwise rel = function | [] -> rel let pointwise_or_dep_relation n t car rel = - if noccurn 1 car then + if noccurn 1 car && noccurn 1 rel then mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |]) else mkApp (Lazy.force forall_relation, @@ -1048,7 +1051,8 @@ module Strategies = let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in let unfolded = try Tacred.try_red_product env sigma c - with _ -> error "fold: the term is not unfoldable !" + with e when Errors.noncritical e -> + error "fold: the term is not unfoldable !" in try let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in @@ -1056,7 +1060,7 @@ module Strategies = Some (Some { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = sigma, cstrevars evars }) - with _ -> None + with e when Errors.noncritical e -> None let fold_glob c : strategy = fun env avoid t ty cstr evars -> @@ -1064,7 +1068,8 @@ module Strategies = let sigma, c = Pretyping.Default.understand_tcc (goalevars evars) env c in let unfolded = try Tacred.try_red_product env sigma c - with _ -> error "fold: the term is not unfoldable !" + with e when Errors.noncritical e -> + error "fold: the term is not unfoldable !" in try let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in @@ -1072,7 +1077,7 @@ module Strategies = Some (Some { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = sigma, cstrevars evars }) - with _ -> None + with e when Errors.noncritical e -> None end @@ -1977,7 +1982,7 @@ let setoid_proof gl ty fn fallback = let evm = project gl in let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in fn env evm car rel gl - with e -> + with e when Errors.noncritical e -> try fallback gl with Hipattern.NoEquationFound -> match e with diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3ff0cf93..7479ee9a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -50,7 +50,7 @@ open Compat open Evd let safe_msgnl s = - try msgnl s with e -> + try msgnl s with e when Errors.noncritical e -> msgnl (str "bug in the debugger: " ++ str "an exception is raised while printing debug information") @@ -92,7 +92,7 @@ let catch_error call_trace tac g = if call_trace = [] then tac g else try tac g with | LtacLocated _ as e -> raise e | Loc.Exc_located (_,LtacLocated _) as e -> raise e - | e -> + | e when Errors.noncritical e -> let (nrep,loc',c),tail = list_sep_last call_trace in let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in if tail = [] then @@ -569,13 +569,13 @@ let dump_glob_red_expr = function try Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) - with _ -> ()) occs + with e when Errors.noncritical e -> ()) occs | Cbv grf | Lazy grf -> List.iter (fun r -> try Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) - with _ -> ()) grf.rConst + with e when Errors.noncritical e -> ()) grf.rConst | _ -> () let intern_red_expr ist = function @@ -1412,19 +1412,20 @@ let interp_may_eval f ist gl = function | ConstrTerm c -> try f ist gl c - with e -> - debugging_exception_step ist false e (fun () -> + with reraise -> + debugging_exception_step ist false reraise (fun () -> str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c)); - raise e + raise reraise (* Interprets a constr expression possibly to first evaluate *) let interp_constr_may_eval ist gl c = let (sigma,csr) = try interp_may_eval pf_interp_constr ist gl c - with e -> - debugging_exception_step ist false e (fun () -> str"evaluation of term"); - raise e + with reraise -> + debugging_exception_step ist false reraise (fun () -> + str"evaluation of term"); + raise reraise in begin db_constr ist.debug (pf_env gl) csr; @@ -1762,10 +1763,7 @@ let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) let pack_sigma (sigma,c) = {it=c;sigma=sigma} let extend_gl_hyps { it=gl ; sigma=sigma } sign = - let hyps = Goal.V82.hyps sigma gl in - let new_hyps = List.fold_right Environ.push_named_context_val sign hyps in - (* spiwack: (2010/01/13) if a bug was reintroduced in [change] in is probably here *) - Goal.V82.new_goal_with sigma gl new_hyps + Goal.V82.new_goal_with sigma gl sign (* Interprets an l-tac expression into a value *) let rec val_interp ist gl (tac:glob_tactic_expr) = @@ -1925,9 +1923,11 @@ and interp_app loc ist gl fv largs = try catch_error trace (val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body - with e -> - debugging_exception_step ist false e (fun () -> str "evaluation"); - raise e in + with reraise -> + debugging_exception_step ist false reraise + (fun () -> str "evaluation"); + raise reraise + in let gl = { gl with sigma=sigma } in debugging_step ist (fun () -> @@ -2212,19 +2212,20 @@ and interp_match ist g lz constr lmr = (try let lmatch = try extended_matches c csr - with e -> - debugging_exception_step ist false e (fun () -> + with reraise -> + debugging_exception_step ist false reraise (fun () -> str "matching with pattern" ++ fnl () ++ pr_constr_pattern_env (pf_env g) c); - raise e in + raise reraise + in try let lfun = extend_values_with_bindings lmatch ist.lfun in eval_with_fail { ist with lfun=lfun } lz g mt - with e -> - debugging_exception_step ist false e (fun () -> + with reraise -> + debugging_exception_step ist false reraise (fun () -> str "rule body for pattern" ++ pr_constr_pattern_env (pf_env g) c); - raise e + raise reraise with e when is_match_catchable e -> debugging_step ist (fun () -> str "switching to the next rule"); apply_match ist sigma csr tl) @@ -2236,15 +2237,16 @@ and interp_match ist g lz constr lmr = errorlabstrm "Tacinterp.apply_match" (str "No matching clauses for match.") in let (sigma,csr) = - try interp_ltac_constr ist g constr with e -> - debugging_exception_step ist true e + try interp_ltac_constr ist g constr with reraise -> + debugging_exception_step ist true reraise (fun () -> str "evaluation of the matched expression"); - raise e in + raise reraise in let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in let res = - try apply_match ist sigma csr ilr with e -> - debugging_exception_step ist true e (fun () -> str "match expression"); - raise e in + try apply_match ist sigma csr ilr with reraise -> + debugging_exception_step ist true reraise + (fun () -> str "match expression"); + raise reraise in debugging_step ist (fun () -> str "match expression returns " ++ pr_value (Some (pf_env g)) (snd res)); res @@ -2404,6 +2406,7 @@ and interp_atomic ist gl tac = (h_generalize_dep c_interp) | TacLetTac (na,c,clp,b,eqpat) -> let clp = interp_clause ist gl clp in + let eqpat = Option.map (interp_intro_pattern ist gl) eqpat in if clp = nowhere then (* We try to fully-typecheck the term *) let (sigma,c_interp) = pf_interp_constr ist gl c in @@ -3180,7 +3183,8 @@ let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t)) let tacticIn t = globTacticIn (fun ist -> try glob_tactic (t ist) - with e -> anomalylabstrm "tacticIn" + with e when Errors.noncritical e -> + anomalylabstrm "tacticIn" (str "Incorrect tactic expression. Received exception is:" ++ Errors.print e)) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 12292196..ac00a73d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1018,7 +1018,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl = let thm = nf_betaiota gl.sigma (pf_type_of gl d) in let rec aux clause = try progress_with_clause flags innerclause clause - with err -> + with err when Errors.noncritical err -> try aux (clenv_push_prod clause) with NotExtensibleClause -> raise err in aux (make_clenv_binding gl (d,thm) lbind) @@ -1708,7 +1708,7 @@ let make_pattern_test env sigma0 (sigma,c) = let flags = default_matching_flags sigma0 in let matching_fun t = try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t) - with _ -> raise NotUnifiable in + with e when Errors.noncritical e -> raise NotUnifiable in let merge_fun c1 c2 = match c1, c2 with | Some (_,c1), Some (_,c2) when not (is_fconv Reduction.CONV env sigma0 c1 c2) -> @@ -2554,7 +2554,10 @@ let specialize_eqs id gl = let specialize_eqs id gl = - if try ignore(clear [id] gl); false with _ -> true then + if + (try ignore(clear [id] gl); false + with e when Errors.noncritical e -> true) + then tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl else specialize_eqs id gl @@ -2716,7 +2719,8 @@ let compute_elim_sig ?elimc elimt = | Some ( _,None,ind) -> let indhd,indargs = decompose_app ind in try {!res with indref = Some (global_of_constr indhd) } - with _ -> error "Cannot find the inductive type of the inductive scheme.";; + with e when Errors.noncritical e -> + error "Cannot find the inductive type of the inductive scheme.";; let compute_scheme_signature scheme names_info ind_type_guess = let f,l = decompose_app scheme.concl in @@ -3551,4 +3555,5 @@ let unify ?(state=full_transparent_state) x y gl = in let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y in tclEVARS evd gl - with _ -> tclFAIL 0 (str"Not unifiable") gl + with e when Errors.noncritical e -> + tclFAIL 0 (str"Not unifiable") gl -- cgit v1.2.3