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 --- plugins/funind/functional_principles_proofs.ml | 23 ++++++++++------ plugins/funind/functional_principles_types.ml | 13 ++++----- plugins/funind/g_indfun.ml4 | 4 +-- plugins/funind/glob_term_to_relation.ml | 13 ++++----- plugins/funind/glob_termops.ml | 6 +++-- plugins/funind/indfun.ml | 14 +++++----- plugins/funind/indfun_common.ml | 18 ++++++------- plugins/funind/invfun.ml | 17 +++++++----- plugins/funind/merge.ml | 6 ++--- plugins/funind/recdef.ml | 37 +++++++++++++++++--------- 10 files changed, 86 insertions(+), 65 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 33d77568..48205019 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -33,9 +33,12 @@ let observennl strm = let do_observe_tac s tac g = try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v - with e -> - let e = Cerrors.process_vernac_interp_error e in - let goal = begin try (Printer.pr_goal g) with _ -> assert false end in + with reraise -> + let e = Cerrors.process_vernac_interp_error reraise in + let goal = + try (Printer.pr_goal g) + with e when Errors.noncritical e -> assert false + in msgnl (str "observation "++ s++str " raised exception " ++ Errors.print e ++ str " on goal " ++ goal ); raise e;; @@ -119,7 +122,7 @@ let is_trivial_eq t = eq_constr t1 t2 && eq_constr a1 a2 | _ -> false end - with _ -> false + with e when Errors.noncritical e -> false in (* observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *) res @@ -145,7 +148,7 @@ let is_incompatible_eq t = (eq_constr u1 u2 && incompatible_constructor_terms t1 t2) | _ -> false - with _ -> false + with e when Errors.noncritical e -> false in if res then observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t); res @@ -232,7 +235,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = then (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0)) else nochange "not an equality" - with _ -> nochange "not an equality" + with e when Errors.noncritical e -> nochange "not an equality" in if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs"; let rec compute_substitution sub t1 t2 = @@ -608,7 +611,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = let my_orelse tac1 tac2 g = try tac1 g - with e -> + with e when Errors.noncritical e -> (* observe (str "using snd tac since : " ++ Errors.print e); *) tac2 g @@ -1212,7 +1215,11 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let ctxt,pte_app = (decompose_prod_assum (pf_concl gl)) in let pte,pte_args = (decompose_app pte_app) in try - let pte = try destVar pte with _ -> anomaly "Property is not a variable" in + let pte = + try destVar pte + with e when Errors.noncritical e -> + anomaly "Property is not a variable" + in let fix_info = Idmap.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in tclTHENSEQ diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 00e966fb..04fcc8d4 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -302,11 +302,8 @@ let defined () = "defined" ((try str "On goal : " ++ fnl () ++ pr_open_subgoals () ++ fnl () - with _ -> mt () + with e when Errors.noncritical e -> mt () ) ++msg) - | e -> raise e - - let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) @@ -401,7 +398,7 @@ let generate_functional_principle Don't forget to close the goal if an error is raised !!!! *) save false new_princ_name entry g_kind hook - with e -> + with e when Errors.noncritical e -> begin begin try @@ -413,7 +410,7 @@ let generate_functional_principle then Pfedit.delete_current_proof () else () else () - with _ -> () + with e when Errors.noncritical e -> () end; raise (Defining_principle e) end @@ -554,7 +551,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition 0 (prove_princ_for_struct false 0 (Array.of_list funs)) (fun _ _ _ -> ()) - with e -> + with e when Errors.noncritical e -> begin begin try @@ -566,7 +563,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition then Pfedit.delete_current_proof () else () else () - with _ -> () + with e when Errors.noncritical e -> () end; raise (Defining_principle e) end diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 85d79214..6b6e4838 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -208,14 +208,14 @@ VERNAC COMMAND EXTEND NewFunctionalScheme try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> Util.error ("Cannot generate induction principle(s)") - | e -> + | e when Errors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end | _ -> assert false (* we can only have non empty list *) end - | e -> + | e when Errors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 43b08840..b9e0e62a 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -948,7 +948,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = try observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = - try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue + try Pretyping.Default.understand Evd.empty env t + with e when Errors.noncritical e -> raise Continue in let is_in_b = is_free_in id b in let _keep_eq = @@ -1247,7 +1248,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b l := param::!l ) rels_params.(0) - with _ -> + with e when Errors.noncritical e -> () in List.rev !l @@ -1453,7 +1454,7 @@ let do_build_inductive in observe (msg); raise e - | e -> + | reraise -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = @@ -1464,16 +1465,16 @@ let do_build_inductive str "while trying to define"++ spc () ++ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) ++ fnl () ++ - Errors.print e + Errors.print reraise in observe msg; - raise e + raise reraise let build_inductive funnames funsargs returned_types rtl = try do_build_inductive funnames funsargs returned_types rtl - with e -> raise (Building_graph e) + with e when Errors.noncritical e -> raise (Building_graph e) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index cdd0eaf7..6cc932b1 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -534,7 +534,8 @@ let rec are_unifiable_aux = function else let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "are_unifiable_aux" + with e when Errors.noncritical e -> + anomaly "are_unifiable_aux" in are_unifiable_aux eqs' @@ -556,7 +557,8 @@ let rec eq_cases_pattern_aux = function else let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "eq_cases_pattern_aux" + with e when Errors.noncritical e -> + anomaly "eq_cases_pattern_aux" in eq_cases_pattern_aux eqs' | _ -> raise NotUnifiable diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8caeca57..d2c065a0 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -82,7 +82,7 @@ let functional_induction with_clean c princl pat = List.fold_right (fun a acc -> try Idset.add (destVar a) acc - with _ -> acc + with e when Errors.noncritical e -> acc ) args Idset.empty @@ -166,8 +166,8 @@ let build_newrecursive sigma rec_sign rec_impls def ) lnameargsardef - with e -> - States.unfreeze fs; raise e in + with reraise -> + States.unfreeze fs; raise reraise in States.unfreeze fs; def in recdef,rec_impls @@ -251,12 +251,12 @@ let derive_inversion fix_names = (fun id -> destInd (Constrintern.global_reference (mk_rel_id id))) fix_names ) - with e -> + with e when Errors.noncritical e -> let e' = Cerrors.process_vernac_interp_error e in msg_warning (str "Cannot build inversion information" ++ if do_observe () then (fnl() ++ Errors.print e') else mt ()) - with _ -> () + with e when Errors.noncritical e -> () let warning_error names e = let e = Cerrors.process_vernac_interp_error e in @@ -346,7 +346,7 @@ let generate_principle on_error Array.iter (add_Function is_general) funs_kn; () end - with e -> + with e when Errors.noncritical e -> on_error names e let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = @@ -413,7 +413,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); derive_inversion [fname] - with e -> + with e when Errors.noncritical e -> (* No proof done *) () in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index dd475315..827191b1 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -55,7 +55,6 @@ let locate_with_msg msg f x = f x with | Not_found -> raise (Util.UserError("", msg)) - | e -> raise e let filter_map filter f = @@ -123,7 +122,7 @@ let def_of_const t = (try (match Declarations.body_of_constant (Global.lookup_constant sp) with | Some c -> Declarations.force c | _ -> assert false) - with _ -> assert false) + with e when Errors.noncritical e -> assert false) |_ -> assert false let coq_constant s = @@ -215,13 +214,13 @@ let with_full_print f a = Dumpglob.continue (); res with - | e -> + | reraise -> Impargs.make_implicit_args old_implicit_args; Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Dumpglob.continue (); - raise e + raise reraise @@ -350,7 +349,8 @@ open Term let pr_info f_info = str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ - (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++ + (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) + with e when Errors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++ str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++ str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++ @@ -502,22 +502,22 @@ exception ToShow of exn let init_constant dir s = try Coqlib.gen_constant "Function" dir s - with e -> raise (ToShow e) + with e when Errors.noncritical e -> raise (ToShow e) let jmeq () = try (Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; init_constant ["Logic";"JMeq"] "JMeq") - with e -> raise (ToShow e) + with e when Errors.noncritical e -> raise (ToShow e) let jmeq_rec () = try Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; init_constant ["Logic";"JMeq"] "JMeq_rec" - with e -> raise (ToShow e) + with e when Errors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; init_constant ["Logic";"JMeq"] "JMeq_refl" - with e -> raise (ToShow e) + with e when Errors.noncritical e -> raise (ToShow e) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 55451a9f..7b5dd763 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -59,14 +59,17 @@ let observennl strm = let do_observe_tac s tac g = - let goal = begin try (Printer.pr_goal g) with _ -> assert false end in + let goal = + try Printer.pr_goal g + with e when Errors.noncritical e -> assert false + in try let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v - with e -> - let e' = Cerrors.process_vernac_interp_error e in + with reraise -> + let e' = Cerrors.process_vernac_interp_error reraise in msgnl (str "observation "++ s++str " raised exception " ++ Errors.print e' ++ str " on goal " ++ goal ); - raise e;; + raise reraise;; let observe_tac s tac g = @@ -568,7 +571,7 @@ let rec reflexivity_with_destruct_cases g = observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] | _ -> reflexivity - with _ -> reflexivity + with e when Errors.noncritical e -> reflexivity in let eq_ind = Coqlib.build_coq_eq () in let discr_inject = @@ -862,11 +865,11 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g update_Function {finfo with completeness_lemma = Some lem_cst} ) funs; - with e -> + with reraise -> (* In case of problem, we reset all the lemmas *) Pfedit.delete_all_proofs (); States.unfreeze previous_state; - raise e + raise reraise diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 6ee2f352..bd1a1710 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -70,7 +70,7 @@ let ident_global_exist id = let ans = CRef (Libnames.Ident (dummy_loc,id)) in let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in true - with _ -> false + with e when Errors.noncritical e -> false (** [next_ident_fresh id] returns a fresh identifier (ie not linked in global env) with base [id]. *) @@ -793,10 +793,10 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let params1 = try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) - with _ -> [] in + with e when Errors.noncritical e -> [] in let params2 = try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) - with _ -> [] in + with e when Errors.noncritical e -> [] in let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 892c1a77..9853fd73 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -94,11 +94,11 @@ let do_observe_tac s tac g = let v = tac g in ignore(Stack.pop debug_queue); v - with e -> + with reraise -> if not (Stack.is_empty debug_queue) then - print_debug_queue true e; - raise e + print_debug_queue true reraise; + raise reraise let observe_tac s tac g = if Tacinterp.get_debug () <> Tactic_debug.DebugOff @@ -140,7 +140,7 @@ let def_of_const t = (try (match body_of_constant (Global.lookup_constant sp) with | Some c -> Declarations.force c | _ -> assert false) - with _ -> + with e when Errors.noncritical e -> anomaly ("Cannot find definition of constant "^ (string_of_id (id_of_label (con_label sp)))) ) @@ -380,7 +380,11 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool) (fun g1 -> let ty_teq = pf_type_of g1 (mkVar teq) in let teq_lhs,teq_rhs = - let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in + let _,args = + try destApp ty_teq + with e when Errors.noncritical e -> + Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false + in args.(1),args.(2) in cont_function (mkVar teq::eqs) (Termops.replace_term teq_lhs teq_rhs expr) g1 @@ -701,12 +705,17 @@ let proveterminate nb_arg rec_arg_id is_mes acc_inv (hrec:identifier) (match find_call_occs nb_arg 0 f_constr expr with _,[] -> (try observe_tac "base_leaf" (base_leaf func eqs expr) - with e -> (msgerrnl (str "failure in base case");raise e )) + with reraise -> + (msgerrnl (str "failure in base case");raise reraise )) | _, _::_ -> observe_tac "rec_leaf" (rec_leaf is_mes acc_inv hrec func eqs expr)) in v - with e -> begin msgerrnl(str "failure in proveterminate"); raise e end + with reraise -> + begin + msgerrnl(str "failure in proveterminate"); + raise reraise + end in proveterminate @@ -931,7 +940,7 @@ let is_rec_res id = let id_name = string_of_id id in try String.sub id_name 0 (String.length rec_res_name) = rec_res_name - with _ -> false + with e when Errors.noncritical e -> false let clear_goals = let rec clear_goal t = @@ -969,7 +978,8 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ | Some s -> s | None -> try (add_suffix current_proof_name "_subproof") - with _ -> anomaly "open_new_goal with an unamed theorem" + with e when Errors.noncritical e -> + anomaly "open_new_goal with an unamed theorem" in let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in @@ -1439,7 +1449,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let stop = ref false in begin try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type) - with e -> + with e when Errors.noncritical e -> begin if Tacinterp.get_debug () <> Tactic_debug.DebugOff then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e) @@ -1474,9 +1484,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num using_lemmas (List.length res_vars) hook - with e -> + with reraise -> begin - (try ignore (Backtrack.backto previous_label) with _ -> ()); + (try ignore (Backtrack.backto previous_label) + with e when Errors.noncritical e -> ()); (* anomaly "Cannot create termination Lemma" *) - raise e + raise reraise end -- cgit v1.2.3