diff options
Diffstat (limited to 'tactics')
40 files changed, 373 insertions, 108 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 272cb1edaa..7aa5114a4f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/auto.mli b/tactics/auto.mli index a6fb82bab2..b9cd4932ca 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 2d4f202769..ed612c0fc9 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index f765318d04..306ff1868a 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index b4a235ba8c..b101b3a9f5 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 27f624f716..a48c866daf 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2faf1e0ecb..3fc2fc31b3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -92,7 +92,7 @@ open Goptions let _ = declare_bool_option - { optdepr = true; + { optdepr = true; (* remove in 8.8 *) optname = "do typeclass search modulo eta conversion"; optkey = ["Typeclasses";"Modulo";"Eta"]; optread = get_typeclasses_modulo_eta; @@ -125,7 +125,7 @@ let _ = let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "compat"; optkey = ["Typeclasses";"Legacy";"Resolution"]; optread = get_typeclasses_legacy_resolution; @@ -494,16 +494,15 @@ let catchable = function | Refiner.FailError _ -> true | e -> Logic.catchable_exception e -(* alternate separators in debug search path output *) -let debug_seps = [| "." ; "-" |] -let next_sep seps = - let num_seps = Array.length seps in - let sep_index = ref 0 in - fun () -> - let sep = seps.(!sep_index) in - sep_index := (!sep_index + 1) mod num_seps; - str sep -let pr_depth l = prlist_with_sep (next_sep debug_seps) int (List.rev l) +let pr_depth l = + let rec fmt elts = + match elts with + | [] -> [] + | [n] -> [string_of_int n] + | n1::n2::rest -> + (string_of_int n1 ^ "." ^ string_of_int n2) :: fmt rest + in + prlist_with_sep (fun () -> str "-") str (fmt (List.rev l)) let is_Prop env sigma concl = let ty = Retyping.get_type_of env sigma concl in @@ -527,10 +526,10 @@ let top_sort evm undefs = let tosee = ref undefs in let rec visit ev evi = let evs = Evarutil.undefined_evars_of_evar_info evm evi in + tosee := Evar.Map.remove ev !tosee; Evar.Set.iter (fun ev -> if Evar.Map.mem ev !tosee then visit ev (Evar.Map.find ev !tosee)) evs; - tosee := Evar.Map.remove ev !tosee; l' := ev :: !l'; in while not (Evar.Map.is_empty !tosee) do @@ -649,8 +648,9 @@ module V85 = struct Goal.V82.hyps gls.Evd.sigma (sig_it gls) let make_autogoal_hints = - let cache = ref (true, Environ.empty_named_context_val, - Hint_db.empty full_transparent_state true) + let cache = Summary.ref ~name:"make_autogoal_hints_cache" + (true, Environ.empty_named_context_val, + Hint_db.empty full_transparent_state true) in fun only_classes ?(st=full_transparent_state) g -> let sign = pf_filtered_hyps g in @@ -979,8 +979,9 @@ module Search = struct search_hints : hint_db; } (** Local hints *) - let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty, - Hint_db.empty full_transparent_state true) + let autogoal_cache = Summary.ref ~name:"autogoal_cache" + (DirPath.empty, true, Context.Named.empty, + Hint_db.empty full_transparent_state true) let make_autogoal_hints only_classes ?(st=full_transparent_state) g = let open Proofview in @@ -1142,7 +1143,7 @@ module Search = struct let res = if j = 0 then tclUNIT () else tclDISPATCH - (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j)))) + (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j')))) in let finish nestedshelf sigma = let filter ev = @@ -1423,18 +1424,20 @@ let deps_of_constraints cstrs evm p = Intpart.union_set (Evar.Set.union evx evy) p) cstrs -let evar_dependencies evm p = +let evar_dependencies pred evm p = Evd.fold_undefined (fun ev evi _ -> - let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi) - in Intpart.union_set evars p) + if Typeclasses.is_resolvable evi && pred evm ev evi then + let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi) + in Intpart.union_set evars p + else ()) evm () (** [split_evars] returns groups of undefined evars according to dependencies *) -let split_evars evm = +let split_evars pred evm = let p = Intpart.create () in - evar_dependencies evm p; + evar_dependencies pred evm p; deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p; Intpart.partition p @@ -1519,7 +1522,7 @@ exception Unresolved (** If [do_split] is [true], we try to separate the problem in several components and then solve them separately *) let resolve_all_evars debug depth unique env p oevd do_split fail = - let split = if do_split then split_evars oevd else [Evar.Set.empty] in + let split = if do_split then split_evars p oevd else [Evar.Set.empty] in let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true in let rec docomp evd = function diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index c5731e3779..d8a1d2ab85 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 83c2be4106..5e2006ccc8 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 2cf5a68298..59f8a328ea 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/dnet.ml b/tactics/dnet.ml index c501e30628..73afc2eac2 100644 --- a/tactics/dnet.ml +++ b/tactics/dnet.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/dnet.mli b/tactics/dnet.mli index 565a916f8e..92c84fc9ad 100644 --- a/tactics/dnet.mli +++ b/tactics/dnet.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index bae3344612..64d4d3135e 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eauto.mli b/tactics/eauto.mli index c952f4e721..8f847737fe 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/elim.ml b/tactics/elim.ml index 13d64b8e3f..b5668dfff0 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/elim.mli b/tactics/elim.mli index fb7cc7b838..0930f9a92a 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 466b1350d9..2d2a0c1b2a 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -46,26 +46,15 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = let sigma, nf = Evarutil.nf_evars_and_universes sigma in (nf c', Evd.evar_universe_context sigma), eff else - let mib,mip = Inductive.lookup_mind_specif env ind in - let ctx = Declareops.inductive_context mib in - let u = Univ.UContext.instance ctx in - let ctxset = Univ.ContextSet.of_context ctx in - let ectx = Evd.evar_universe_context_of ctxset in - let sigma = Evd.merge_universe_context sigma ectx in - let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in + let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, c = build_induction_scheme env sigma pind dep sort in (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants let build_induction_scheme_in_type dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in - let ctx = - let mib,mip = Inductive.lookup_mind_specif env ind in - Declareops.inductive_context mib - in - let u = Univ.UContext.instance ctx in - let ctxset = Univ.ContextSet.of_context ctx in - let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in - let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in + let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma let rect_scheme_kind_from_type = @@ -80,30 +69,30 @@ let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) -let ind_scheme_kind_from_type = - declare_individual_scheme_object "_ind_nodep" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp) - -let ind_scheme_kind_from_prop = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" - (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp) - -let ind_dep_scheme_kind_from_type = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp) +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) -let rec_scheme_kind_from_type = - declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) - let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) +let ind_scheme_kind_from_type = + declare_individual_scheme_object "_ind_nodep" + (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp) + +let ind_dep_scheme_kind_from_type = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" + (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp) + +let ind_scheme_kind_from_prop = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" + (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp) + (* Case analysis *) let build_case_analysis_scheme_in_type dep sort ind = diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index 77f927f2df..e3fe7ddae9 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,6 +10,14 @@ open Ind_tables (** Induction/recursion schemes *) +val optimize_non_type_induction_scheme : + 'a Ind_tables.scheme_kind -> + Indrec.dep_flag -> + Term.sorts_family -> + 'b -> + Names.inductive -> + (Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants + val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val rec_scheme_kind_from_prop : individual scheme_kind diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 10bc6e3e24..d4cad3fa89 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eqdecide.mli b/tactics/eqdecide.mli index dca1780b76..2d22710b2c 100644 --- a/tactics/eqdecide.mli +++ b/tactics/eqdecide.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index efcefcf16a..ce57682c66 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index aa8a6d4bd9..4acfa7a281 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 6e56dc48e5..66345ce43c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/equality.mli b/tactics/equality.mli index 27be5affb1..421f7c7f5d 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 681db5d08e..a572508d47 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -937,7 +937,7 @@ let make_extern pri pat tacast = let make_mode ref m = let open Term in - let ty = Global.type_of_global_unsafe ref in + let ty, _ = Global.type_of_global_in_context (Global.env ()) ref in let ctx, t = decompose_prod ty in let n = List.length ctx in let m' = Array.of_list m in @@ -1306,7 +1306,8 @@ let interp_hints poly = List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in - empty_hint_info, mib.Declarations.mind_polymorphic, true, + empty_hint_info, + (Declareops.inductive_is_polymorphic mib), true, PathHints [gr], IsGlobRef gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> diff --git a/tactics/hints.mli b/tactics/hints.mli index 3a0339ff57..6325a44706 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 4db744224a..4101004d48 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index a1d986544a..59406e1584 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml new file mode 100644 index 0000000000..0407c1e36a --- /dev/null +++ b/tactics/ind_tables.ml @@ -0,0 +1,203 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* File created by Vincent Siles, Oct 2007, extended into a generic + support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *) + +(* This file provides support for registering inductive scheme builders, + declaring schemes and generating schemes on demand *) + +open Names +open Mod_subst +open Libobject +open Nameops +open Declarations +open Term +open CErrors +open Util +open Declare +open Entries +open Decl_kinds +open Pp + +(**********************************************************************) +(* Registering schemes in the environment *) + +type mutual_scheme_object_function = + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants +type individual_scheme_object_function = + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants + +type 'a scheme_kind = string + +let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" + +let pr_scheme_kind = Pp.str + +let cache_one_scheme kind (ind,const) = + let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in + scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map + +let cache_scheme (_,(kind,l)) = + Array.iter (cache_one_scheme kind) l + +let subst_one_scheme subst (ind,const) = + (* Remark: const is a def: the result of substitution is a constant *) + (subst_ind subst ind,subst_constant subst const) + +let subst_scheme (subst,(kind,l)) = + (kind,Array.map (subst_one_scheme subst) l) + +let discharge_scheme (_,(kind,l)) = + Some (kind,Array.map (fun (ind,const) -> + (Lib.discharge_inductive ind,Lib.discharge_con const)) l) + +let inScheme : string * (inductive * constant) array -> obj = + declare_object {(default_object "SCHEME") with + cache_function = cache_scheme; + load_function = (fun _ -> cache_scheme); + subst_function = subst_scheme; + classify_function = (fun obj -> Substitute obj); + discharge_function = discharge_scheme} + +(**********************************************************************) +(* The table of scheme building functions *) + +type individual +type mutual + +type scheme_object_function = + | MutualSchemeFunction of mutual_scheme_object_function + | IndividualSchemeFunction of individual_scheme_object_function + +let scheme_object_table = + (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) + +let declare_scheme_object s aux f = + let () = + if not (Id.is_valid ("ind" ^ s)) then + user_err Pp.(str ("Illegal induction scheme suffix: " ^ s)) + in + let key = if String.is_empty aux then s else aux in + try + let _ = Hashtbl.find scheme_object_table key in +(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*) + user_err ~hdr:"IndTables.declare_scheme_object" + (str "Scheme object " ++ str key ++ str " already declared.") + with Not_found -> + Hashtbl.add scheme_object_table key (s,f); + key + +let declare_mutual_scheme_object s ?(aux="") f = + declare_scheme_object s aux (MutualSchemeFunction f) + +let declare_individual_scheme_object s ?(aux="") f = + declare_scheme_object s aux (IndividualSchemeFunction f) + +(**********************************************************************) +(* Defining/retrieving schemes *) + +let declare_scheme kind indcl = + Lib.add_anonymous_leaf (inScheme (kind,indcl)) + +let () = Declare.set_declare_scheme declare_scheme + +let is_visible_name id = + try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true + with Not_found -> false + +let compute_name internal id = + match internal with + | UserAutomaticRequest | UserIndividualRequest -> id + | InternalTacticRequest -> + Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name + +let define internal id c p univs = + let fd = declare_constant ~internal in + let id = compute_name internal id in + let ctx = Evd.normalize_evar_universe_context univs in + let c = Vars.subst_univs_fn_constr + (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in + let entry = { + const_entry_body = + Future.from_val ((c,Univ.ContextSet.empty), + Safe_typing.empty_private_constants); + const_entry_secctx = None; + const_entry_type = None; + const_entry_polymorphic = p; + const_entry_universes = Evd.evar_context_universe_context ctx; + const_entry_opaque = false; + const_entry_inline_code = false; + const_entry_feedback = None; + } in + let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let () = match internal with + | InternalTacticRequest -> () + | _-> definition_message id + in + kn + +let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = + let (c, ctx), eff = f mode ind in + let mib = Global.lookup_mind mind in + let id = match idopt with + | Some id -> id + | None -> add_suffix mib.mind_packets.(i).mind_typename suff in + let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in + declare_scheme kind [|ind,const|]; + const, Safe_typing.add_private + (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff + +let define_individual_scheme kind mode names (mind,i as ind) = + match Hashtbl.find scheme_object_table kind with + | _,MutualSchemeFunction f -> assert false + | s,IndividualSchemeFunction f -> + define_individual_scheme_base kind s f mode names ind + +let define_mutual_scheme_base kind suff f mode names mind = + let (cl, ctx), eff = f mode mind in + let mib = Global.lookup_mind mind in + let ids = Array.init (Array.length mib.mind_packets) (fun i -> + try Int.List.assoc i names + with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in + let consts = Array.map2 (fun id cl -> + define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in + let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in + declare_scheme kind schemes; + consts, + Safe_typing.add_private + (Safe_typing.private_con_of_scheme + ~kind (Global.safe_env()) (Array.to_list schemes)) + eff + +let define_mutual_scheme kind mode names mind = + match Hashtbl.find scheme_object_table kind with + | _,IndividualSchemeFunction _ -> assert false + | s,MutualSchemeFunction f -> + define_mutual_scheme_base kind s f mode names mind + +let find_scheme_on_env_too kind ind = + let s = String.Map.find kind (Indmap.find ind !scheme_map) in + s, Safe_typing.add_private + (Safe_typing.private_con_of_scheme + ~kind (Global.safe_env()) [ind, s]) + Safe_typing.empty_private_constants + +let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = + try find_scheme_on_env_too kind ind + with Not_found -> + match Hashtbl.find scheme_object_table kind with + | s,IndividualSchemeFunction f -> + define_individual_scheme_base kind s f mode None ind + | s,MutualSchemeFunction f -> + let ca, eff = define_mutual_scheme_base kind s f mode [] mind in + ca.(i), eff + +let check_scheme kind ind = + try let _ = find_scheme_on_env_too kind ind in true + with Not_found -> false diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli new file mode 100644 index 0000000000..005555caa0 --- /dev/null +++ b/tactics/ind_tables.mli @@ -0,0 +1,51 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Term +open Names +open Declare + +(** This module provides support for registering inductive scheme builders, + declaring schemes and generating schemes on demand *) + +(** A scheme is either a "mutual scheme_kind" or an "individual scheme_kind" *) + +type mutual +type individual +type 'a scheme_kind + +type mutual_scheme_object_function = + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants +type individual_scheme_object_function = + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants + +(** Main functions to register a scheme builder *) + +val declare_mutual_scheme_object : string -> ?aux:string -> + mutual_scheme_object_function -> mutual scheme_kind + +val declare_individual_scheme_object : string -> ?aux:string -> + individual_scheme_object_function -> + individual scheme_kind + +(** Force generation of a (mutually) scheme with possibly user-level names *) + +val define_individual_scheme : individual scheme_kind -> + internal_flag (** internal *) -> + Id.t option -> inductive -> constant * Safe_typing.private_constants + +val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> + (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants + +(** Main function to retrieve a scheme in the cache or to generate it *) +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants + +val check_scheme : 'a scheme_kind -> inductive -> bool + + +val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds diff --git a/tactics/inv.ml b/tactics/inv.ml index 2bc9d9f788..9495ca9c55 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/inv.mli b/tactics/inv.mli index 5835e763dd..828cf7a044 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 87d815fc81..aeb80ae57c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/leminv.mli b/tactics/leminv.mli index a343fc81a7..41b0e09b42 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 4101dc23e4..bce0dda10c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 9603212de6..4ad9c6541d 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 689cc48aa2..8a95ad177d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -80,15 +80,15 @@ let _ = optread = (fun () -> !Flags.tactic_context_compat) ; optwrite = (fun b -> Flags.tactic_context_compat := b) } -let apply_solve_class_goals = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = true; - Goptions.optname = - "Perform typeclass resolution on apply-generated subgoals."; - Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"]; - Goptions.optread = (fun () -> !apply_solve_class_goals); - Goptions.optwrite = (fun a -> apply_solve_class_goals:=a); -} +let apply_solve_class_goals = ref false + +let _ = + declare_bool_option + { optdepr = true; (* remove in 8.8 *) + optname = "Perform typeclass resolution on apply-generated subgoals."; + optkey = ["Typeclass";"Resolution";"After";"Apply"]; + optread = (fun () -> !apply_solve_class_goals); + optwrite = (fun a -> apply_solve_class_goals := a); } let clear_hyp_by_default = ref false @@ -124,7 +124,7 @@ let shrink_abstract = ref true let _ = declare_bool_option - { optdepr = true; + { optdepr = true; (* remove in 8.8 *) optname = "shrinking of abstracted proofs"; optkey = ["Shrink"; "Abstract"]; optread = (fun () -> !shrink_abstract) ; @@ -143,7 +143,7 @@ let use_bracketing_last_or_and_intro_pattern () = let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) + { optdepr = false; optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); @@ -5003,9 +5003,19 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in let cst = Impargs.with_implicit_protection cst () in - (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) - let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in - let lem = EConstr.of_constr lem in + let lem = + if const.Entries.const_entry_polymorphic then + let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in + (** Hack: the kernel may generate definitions whose universe variables are + not the same as requested in the entry because of constraints delayed + in the body, even in polymorphic mode. We mimick what it does for now + in hope it is fixed at some point. *) + let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in + let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in + let u = Univ.UContext.instance uctx in + mkConstU (cst, EInstance.make u) + else mkConst cst + in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in let eff = private_con_of_con (Global.safe_env ()) cst in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 2e17b8dd5c..bca0c4c50d 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 726fd23b64..e90e1959ed 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index fcc03befeb..16122fa5e0 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |