aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml39
-rw-r--r--tactics/elimschemes.ml19
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/ind_tables.ml203
-rw-r--r--tactics/ind_tables.mli51
-rw-r--r--tactics/tactics.ml38
6 files changed, 303 insertions, 49 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7a85956538..3fc2fc31b3 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -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
@@ -1144,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 =
@@ -1425,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
@@ -1521,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/elimschemes.ml b/tactics/elimschemes.ml
index 5d9d36958f..2d2a0c1b2a 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -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_polymorphic_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_polymorphic_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 =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c2c80e6305..a572508d47 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -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
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/tactics.ml b/tactics/tactics.ml
index 2e3a4e33b3..8a95ad177d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 13:38:17 +0000