diff options
34 files changed, 1022 insertions, 323 deletions
@@ -75,13 +75,26 @@ Tactics - Option "Injection On Proofs" was renamed "Keep Proof Equalities". When enabled, injection and inversion do not drop equalities between objects in Prop. Still disabled by default. - +- New tactics "notypeclasses refine" and "simple notypeclasses refine" that + disallow typeclass resolution when typechecking their argument, for use + in typeclass hints. + Hints - Revised the syntax of [Hint Cut] to follow standard notation for regexps. - Hint Mode now accepts "!" which means that the mode matches only if the argument's head is not an evar (it goes under applications, casts, and scrutinees of matches and projections). +- Hints can now take an optional user-given pattern, used only by + [typeclasses eauto] with the [Filtered Unification] option on. + +Typeclasses + +- Many new options and new engine based on the proof monad. The + [typeclasses eauto] tactic is now a multi-goal, multi-success tactic. + See reference manual for more information. It is planned to + replace auto and eauto in the following version. The 8.5 resolution + engine is still available to help solve compatibility issues. Program diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index e8ebb9f99..58ae7191f 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -9,10 +9,6 @@ \aauthor{Matthieu Sozeau} \label{typeclasses} -\begin{flushleft} - \em The status of Type Classes is experimental. -\end{flushleft} - This chapter presents a quick reference of the commands related to type classes. For an actual introduction to type classes, there is a description of the system \cite{sozeau08} and the literature on type @@ -382,6 +378,71 @@ projections as instances. This is almost equivalent to {\tt Hint Resolve Declares variables according to the given binding context, which might use implicit generalization (see \ref{SectionContext}). +\asubsection{\tt typeclasses eauto} +\tacindex{typeclasses eauto} + +The {\tt typeclasses eauto} tactic uses a different resolution engine +than {\tt eauto} and {\tt auto}. The main differences are the following: +\begin{itemize} +\item Contrary to {\tt eauto} and {\tt auto}, the resolution is done + entirely in the new proof engine (as of Coq v8.6), meaning that + backtracking is available among dependent subgoals, and shelving goals + is supported. {\tt typeclasses eauto} is a multi-goal tactic. + It analyses the dependencies between subgoals to avoid + backtracking on subgoals that are entirely independent. +\item When called with no arguments, {\tt typeclasses eauto} uses the + {\tt typeclass\_instances} database by default (instead of {\tt core}) + and will try to solve \emph{only} typeclass goals. If some subgoal of + a hint/instance is non-dependent and not of class type, that hint + application will fail. Dependent subgoals are automatically shelved + and \emph{must be} resolved entirely when the other typeclass subgoals + are resolved or the proof search will fail \emph{globally}, + \emph{without} the possibility to find another complete solution with + no shelved subgoals. + + \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)} + faithfully mimicks what happens during typeclass resolution when it is + called during refinement/type-inference. It might move to {\tt + all:typeclasses eauto} in future versions when the refinement engine + will be able to backtrack. +\item When called with specific databases (e.g. {\tt with}), {\tt + typeclasses eauto} allows shelved goals to remain at any point + during search and treat typeclasses goals like any other. +\item The transparency information of databases is used consistently for + all hints declared in them. It is always used when calling the unifier. + When considering the local hypotheses, we use the transparent + state of the first hint database given. Using an empty database + (created with {\tt Create HintDb} for example) with + unfoldable variables and constants as the first argument of + typeclasses eauto hence makes resolution with the local hypotheses use + full conversion during unification. +\end{itemize} + +\begin{Variants} +\item \label{depth} {\tt typeclasses eauto \zeroone{\num}} + \emph{Warning:} The semantics for the limit {\num} is different than + for {\tt auto}. By default, if no limit is given the search is + unbounded. Contrary to {\tt auto}, introduction steps ({\tt intro}) + are counted, which might result in larger limits being necessary + when searching with {\tt typeclasses eauto} than {\tt auto}. + +\item \label{with} {\tt typeclasses eauto with {\ident}$_1$ \ldots {\ident}$_n$}. + This variant runs resolution with the given hint databases. It treats + typeclass subgoals the same as other subgoals (no shelving of + non-typeclass goals in particular). +\end{Variants} + +\asubsection{\tt autoapply {\term} with {\ident}} +\tacindex{autoapply} + +The tactic {\tt autoapply} applies a term using the transparency +information of the hint database {\ident}, and does \emph{no} typeclass +resolution. This can be used in {\tt Hint Extern}'s for typeclass +instances (in hint db {\tt typeclass\_instances}) to +allow backtracking on the typeclass subgoals created by the lemma +application, rather than doing type class resolution locally at the hint +application time. + \subsection{\tt Typeclasses Transparent, Opaque {\ident$_1$ \ldots \ident$_n$}} \comindex{Typeclasses Transparent} \comindex{Typeclasses Opaque} @@ -400,20 +461,123 @@ abbreviate a type, like {\tt relation A := A -> A -> Prop}. This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}. +\subsection{\tt Set Typeclasses Dependency Order} +\optindex{Typeclasses Dependency Order} + +This option (on by default since 8.6) respects the dependency order between +subgoals, meaning that subgoals which are depended on by other subgoals +come first, while the non-dependent subgoals were put before the +dependent ones previously (Coq v8.5 and below). This can result in quite +different performance behaviors of proof search. + +\subsection{\tt Set Typeclasses Filtered Unification} +\optindex{Typeclasses Filtered Unification} + +This option, available since Coq 8.6 and off by default, switches the +hint application procedure to a filter-then-unify strategy. To apply a +hint, we first check that the goal \emph{matches} syntactically the +inferred or specified pattern of the hint, and only then try to +\emph{unify} the goal with the conclusion of the hint. This can +drastically improve performance by calling unification less often, +matching syntactic patterns being very quick. This also provides more +control on the triggering of instances. For example, forcing a constant +to explicitely appear in the pattern will make it never apply on a goal +where there is a hole in that place. + +\subsection{\tt Set Typeclasses Legacy Resolution} +\optindex{Typeclasses Legacy Resolution} + +This option (off by default) uses the 8.5 implementation of resolution. +Use for compatibility purposes only (porting and debugging). + +\subsection{\tt Set Typeclasses Module Eta} +\optindex{Typeclasses Modulo Eta} + +This option allows eta-conversion for functions and records during +unification of type-classes. This option is now unsupported in 8.6 with +{\tt Typeclasses Filtered Unification} set, but still affects the +default unification strategy, and the one used in {\tt Legacy + Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses + Filtered Unification} is set, this has no effect and unification will +find solutions up-to eta conversion. Note however that syntactic +pattern-matching is not up-to eta. + +\subsection{\tt Set Typeclasses Limit Intros} +\optindex{Typeclasses Limit Intros} + +This option (on by default in Coq 8.6 and below) controls the ability to +apply hints while avoiding (functional) eta-expansions in the generated +proof term. It does so by allowing hints that conclude in a product to +apply to a goal with a matching product directly, avoiding an +introduction. \emph{Warning:} this can be expensive as it requires +rebuilding hint clauses dynamically, and does not benefit from the +invertibility status of the product introduction rule, resulting in +potentially more expensive proof-search (i.e. more useless +backtracking). + +\subsection{\tt Set Typeclass Resolution After Apply} +\optindex{Typeclasses Resolution After Apply} +\emph{Deprecated since 8.6} + +This option (off by default in Coq 8.6 and 8.5) controls the resolution +of typeclass subgoals generated by the {\tt apply} tactic. + +\subsection{\tt Set Typeclass Resolution For Conversion} +\optindex{Typeclasses Resolution For Conversion} + +This option (on by default) controls the use of typeclass resolution +when a unification problem cannot be solved during +elaboration/type-inference. With this option on, when a unification +fails, typeclass resolution is tried before launching unification once again. + +\subsection{\tt Set Typeclasses Strict Resolution} +\optindex{Typeclasses Strict Resolution} + +Typeclass declarations introduced when this option is set have a +stricter resolution behavior (the option is off by default). When +looking for unifications of a goal with an instance of this class, we +``freeze'' all the existentials appearing in the goals, meaning that +they are considered rigid during unification and cannot be instantiated. + +\subsection{\tt Set Typeclasses Unique Solutions} +\optindex{Typeclasses Unique Solutions} + +When a typeclass resolution is launched we ensure that it has a single +solution or fail. This ensures that the resolution is canonical, but can +make proof search much more expensive. + +\subsection{\tt Set Typeclasses Unique Instances} +\optindex{Typeclasses Unique Instances} + +Typeclass declarations introduced when this option is set have a +more efficient resolution behavior (the option is off by default). When +a solution to the typeclass goal of this class is found, we never +backtrack on it, assuming that it is canonical. + \subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]} \comindex{Typeclasses eauto} \label{TypeclassesEauto} -This command allows customization of the type class resolution tactic, -based on a variant of eauto. The flags semantics are: +This command allows more global customization of the type class +resolution tactic. +The semantics of the options are: \begin{itemize} \item {\tt debug} In debug mode, the trace of successfully applied tactics is printed. \item {\tt dfs, bfs} This sets the search strategy to depth-first search (the default) or breadth-first search. -\item {\emph{depth}} This sets the depth of the search (the default is 100). +\item {\emph{depth}} This sets the depth limit of the search. \end{itemize} +\subsection{\tt Set Typeclasses Debug [Verbosity {\num}]} +\optindex{Typeclasses Debug} +\optindex{Typeclasses Debug Verbosity} + +These options allow to see the resolution steps of typeclasses that are +performed during search. The {\tt Debug} option is synonymous to +{\tt Debug Verbosity 1}, and {\tt Debug Verbosity 2} provides more +information (tried tactics, shelving of goals, etc\ldots). + \subsection{\tt Set Refine Instance Mode} \optindex{Refine Instance Mode} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 656ae57b9..d71454a3c 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -263,6 +263,16 @@ Defined. This tactic behaves like {\tt refine}, but it does not shelve any subgoal. It does not perform any beta-reduction either. +\item {\tt notypeclasses refine \term}\tacindex{notypeclasses refine} + + This tactic behaves like {\tt refine} except it performs typechecking + without resolution of typeclasses. + +\item {\tt simple notypeclasses refine \term}\tacindex{simple + notypeclasses refine} + + This tactic behaves like {\tt simple refine} except it performs typechecking + without resolution of typeclasses. \end{Variants} \subsection{\tt apply \term} @@ -3717,12 +3727,14 @@ command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is The {\hintdef} is one of the following expressions: \begin{itemize} -\item {\tt Resolve \term} +\item {\tt Resolve \term {\zeroone{{\tt |} \zeroone{\num} \zeroone{\pattern}}}} \comindex{Hint Resolve} This command adds {\tt simple apply {\term}} to the hint list with the head symbol of the type of \term. The cost of that hint is - the number of subgoals generated by {\tt simple apply {\term}}. + the number of subgoals generated by {\tt simple apply {\term}} or \num + if specified. The associated pattern is inferred from the conclusion + of the type of \term or the given \pattern if specified. %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false In case the inferred type of \term\ does not start with a product @@ -3906,7 +3918,7 @@ Abort. \comindex{Hint Cut} \textit{Warning:} these hints currently only apply to typeclass proof search and - the \texttt{typeclasses eauto} tactic. + the \texttt{typeclasses eauto} tactic (\ref{typeclasseseauto}). This command can be used to cut the proof-search tree according to a regular expression matching paths to be cut. The grammar for regular diff --git a/engine/termops.ml b/engine/termops.ml index 35cacc65b..697b9a5f1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -980,7 +980,7 @@ let smash_rel_context sign = let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let mem_named_context_val id ctxt = - try Environ.lookup_named_val id ctxt; true with Not_found -> false + try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false let compact_named_context_reverse sign = let compact l decl = diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 1336c92b6..92e4dd618 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -123,8 +123,14 @@ type hint_mode = | ModeNoHeadEvar (* No evar at the head *) | ModeOutput (* Anything *) +type 'a hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } + +type hint_info_expr = constr_pattern_expr hint_info_gen + type hints_expr = - | HintsResolve of (int option * bool * reference_or_constr) list + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list | HintsImmediate of reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool @@ -368,12 +374,12 @@ type vernac_expr = local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) (bool * constr_expr) option * (* props *) - int option (* Priority *) + hint_info_expr | VernacContext of local_binder list | VernacDeclareInstances of - reference list * int option (* instance names, priority *) + (reference * hint_info_expr) list (* instances names, priorities and patterns *) | VernacDeclareClass of reference (* inductive or definition name *) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 2cca760c3..d88bcd7eb 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -316,7 +316,8 @@ let project_hint pri l2r r = in let ctx = Evd.universe_context_set sigma in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in - (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) + let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in + (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) let add_hints_iff l2r lc n bl = Hints.add_hints true bl @@ -347,11 +348,12 @@ let constr_flags = { Pretyping.fail_evar = false; Pretyping.expand_evars = true } -let refine_tac ist simple c = +let refine_tac ist simple with_classes c = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - let flags = constr_flags in + let flags = + { constr_flags with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in @@ -363,11 +365,23 @@ let refine_tac ist simple c = end } TACTIC EXTEND refine -| [ "refine" uconstr(c) ] -> [ refine_tac ist false c ] +| [ "refine" uconstr(c) ] -> + [ refine_tac ist false true c ] END TACTIC EXTEND simple_refine -| [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ] +| [ "simple" "refine" uconstr(c) ] -> + [ refine_tac ist true true c ] +END + +TACTIC EXTEND notcs_refine +| [ "notypeclasses" "refine" uconstr(c) ] -> + [ refine_tac ist false false c ] +END + +TACTIC EXTEND notcs_simple_refine +| [ "simple" "notypeclasses" "refine" uconstr(c) ] -> + [ refine_tac ist true false c ] END (* Solve unification constraints using heuristics or fail if any remain *) diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index 18df596eb..7e26b5d18 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -44,19 +44,33 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug | [ ] -> [ false ] END +let pr_search_strategy _prc _prlc _prt = function + | Some Dfs -> Pp.str "dfs" + | Some Bfs -> Pp.str "bfs" + | None -> Pp.mt () + +ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy +| [ "(bfs)" ] -> [ Some Bfs ] +| [ "(dfs)" ] -> [ Some Dfs ] +| [ ] -> [ None ] +END + (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [ + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [ set_typeclasses_debug d; + Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth ] END (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) TACTIC EXTEND typeclasses_eauto + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> + [ typeclasses_eauto ~strategy:Bfs ~depth:d l ] | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - [ typeclasses_eauto d l ] + [ typeclasses_eauto ~depth:d l ] | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [ typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ] END diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 4d7c5d0e4..44efdd383 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1788,7 +1788,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance (Flags.is_universe_polymorphism ()) binders instance (Some (true, CRecord (Loc.ghost,fields))) - ~global ~generalize:false ~refine:false None + ~global ~generalize:false ~refine:false Hints.empty_hint_info let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" @@ -1969,7 +1969,7 @@ let add_morphism_infer glob m n = Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) None glob + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob poly (ConstRef cst)); declare_projection n instance_id (ConstRef cst) else @@ -1980,7 +1980,7 @@ let add_morphism_infer glob m n = let hook _ = function | Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) None + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob poly (ConstRef cst)); declare_projection n instance_id (ConstRef cst) | _ -> assert false @@ -2004,7 +2004,7 @@ let add_morphism glob binders m s n = let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~global:glob poly binders instance (Some (true, CRecord (Loc.ghost,[]))) - ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1e3c4b880..70c5d5d88 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -103,10 +103,9 @@ GEXTEND Gram (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; - pri = OPT [ "|"; i = natural -> i ]; - dbnames = opt_hintbases -> + info = hint_info; dbnames = opt_hintbases -> VernacHints (false,dbnames, - HintsResolve (List.map (fun x -> (pri, true, x)) lc)) + HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] @@ -116,9 +115,8 @@ GEXTEND Gram | c = constr -> HintsConstr c ] ] ; hint: - [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; - pri = OPT [ "|"; i = natural -> i ] -> - HintsResolve (List.map (fun x -> (pri, true, x)) lc) + [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> + HintsResolve (List.map (fun x -> (info, true, x)) lc) | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8f86abcf3..9b52d1bf3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -588,7 +588,7 @@ let warn_deprecated_arguments_syntax = (* Extensions: implicits, coercions, etc. *) GEXTEND Gram - GLOBAL: gallina_ext instance_name; + GLOBAL: gallina_ext instance_name hint_info; gallina_ext: [ [ (* Transparent and Opaque *) @@ -641,17 +641,20 @@ GEXTEND Gram | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] ; + info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | ":="; c = lconstr -> Some (false,c) | -> None ] -> - VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri) + VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) | IDENT "Existing"; IDENT "Instance"; id = global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances ([id], pri) + info = hint_info -> + VernacDeclareInstances [id, info] + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances (ids, pri) + pri = OPT [ "|"; i = natural -> i ] -> + let info = { hint_priority = pri; hint_pattern = None } in + let insts = List.map (fun i -> (i, info)) ids in + VernacDeclareInstances insts | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is @@ -796,6 +799,11 @@ GEXTEND Gram (Option.default [] sup) | -> ((!@loc, Anonymous), None), [] ] ] ; + hint_info: + [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> + { hint_priority = i; hint_pattern = pat } + | -> { hint_priority = None; hint_pattern = None } ] ] + ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] ; @@ -817,8 +825,8 @@ GEXTEND Gram (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] -> - VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri) + info = hint_info -> + VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) (* System directory *) | IDENT "Pwd" -> VernacChdir None diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9e9a7e723..7dc02190e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -379,6 +379,7 @@ module Vernac_ = let vernac = gec_vernac "Vernac.vernac" let vernac_eoi = eoi_entry vernac let rec_definition = gec_vernac "Vernac.rec_definition" + let hint_info = gec_vernac "hint_info" (* Main vernac entry *) let main_entry = Gram.entry_create "vernac" let noedit_mode = gec_vernac "noedit_command" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7f6caf63f..ec8dac821 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -213,6 +213,7 @@ module Vernac_ : val vernac_eoi : vernac_expr Gram.entry val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry + val hint_info : Vernacexpr.hint_info_expr Gram.entry end (** The main entry: reads an optional vernac command *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 31ef3dfdd..b8da6b685 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -65,7 +65,8 @@ type typeclass = { cl_props : Context.Rel.t; (* The method implementaions as projections. *) - cl_projs : (Name.t * (direction * int option) option * constant option) list; + cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option + * constant option) list; cl_strict : bool; @@ -76,10 +77,9 @@ type typeclasses = typeclass Refmap.t type instance = { is_class: global_reference; - is_pri: int option; + is_info: Vernacexpr.hint_info_expr; (* Sections where the instance should be redeclared, - -1 for discard, 0 for none, mutable to avoid redeclarations - when multiple rebuild_object happen. *) + -1 for discard, 0 for none. *) is_global: int; is_poly: bool; is_impl: global_reference; @@ -89,15 +89,15 @@ type instances = (instance Refmap.t) Refmap.t let instance_impl is = is.is_impl -let instance_priority is = is.is_pri +let hint_priority is = is.is_info.Vernacexpr.hint_priority -let new_instance cl pri glob poly impl = +let new_instance cl info glob poly impl = let global = if glob then Lib.sections_depth () else -1 in { is_class = cl.cl_impl; - is_pri = pri ; + is_info = info ; is_global = global ; is_poly = poly; is_impl = impl } @@ -274,7 +274,9 @@ let check_instance env sigma c = not (Evd.has_undefined evd) with e when CErrors.noncritical e -> false -let build_subclasses ~check env sigma glob pri = +open Vernacexpr + +let build_subclasses ~check env sigma glob { hint_priority = pri } = let _id = Nametab.basename_of_global glob in let _next_id = let i = ref (-1) in @@ -297,24 +299,24 @@ let build_subclasses ~check env sigma glob pri = match b with | None -> None | Some (Backward, _) -> None - | Some (Forward, pri') -> + | Some (Forward, info) -> let proj = Option.get proj in let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in if check && check_instance env sigma body then None else - let pri = - match pri, pri' with + let newpri = + match pri, info.hint_priority with | Some p, Some p' -> Some (p + p') | Some p, None -> Some (p + 1) | _, _ -> None in - Some (ConstRef proj, pri, body)) tc.cl_projs + Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs in - let declare_proj hints (cref, pri, body) = + let declare_proj hints (cref, info, body) = let path' = cref :: path in let ty = Retyping.get_type_of env sigma body in let rest = aux pri body ty path' in - hints @ (path', pri, body) :: rest + hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in @@ -368,11 +370,11 @@ let is_local i = Int.equal i.is_global (-1) let add_instance check inst = let poly = Global.is_polymorphic inst.is_impl in add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) - inst.is_pri poly; + inst.is_info poly; List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path (is_local inst) pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) - (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri) + (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) let rebuild_instance (action, inst) = let () = match action with @@ -404,26 +406,22 @@ let remove_instance i = Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); remove_instance_hint i.is_impl -let declare_instance pri local glob = +let declare_instance info local glob = let ty = Global.type_of_global_unsafe glob in + let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr ty with | Some (rels, ((tc,_), args) as _cl) -> - add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob) -(* let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *) -(* let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *) -(* Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *) -(* Auto.add_hints local [typeclasses_db] *) -(* (Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *) + add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob) | None -> () let add_class cl = add_class cl; List.iter (fun (n, inst, body) -> match inst with - | Some (Backward, pri) -> + | Some (Backward, info) -> (match body with | None -> CErrors.error "Non-definable projection can not be declared as a subinstance" - | Some b -> declare_instance pri false (ConstRef b)) + | Some b -> declare_instance (Some info) false (ConstRef b)) | _ -> ()) cl.cl_projs diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 2530f5dfa..620bc367b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -32,7 +32,7 @@ type typeclass = { Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (Name.t * (direction * int option) option * constant option) list; + cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list; (** Whether we use matching or full unification during resolution *) cl_strict : bool; @@ -50,7 +50,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic -> +val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic -> global_reference -> instance val add_instance : instance -> unit val remove_instance : instance -> unit @@ -71,7 +71,7 @@ val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr val instance_impl : instance -> global_reference -val instance_priority : instance -> int option +val hint_priority : instance -> int option val is_class : global_reference -> bool val is_instance : global_reference -> bool @@ -113,21 +113,22 @@ val classes_transparent_state : unit -> transparent_state val add_instance_hint_hook : (global_reference_or_constr -> global_reference list -> - bool (* local? *) -> int option -> Decl_kinds.polymorphic -> unit) Hook.t + bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t val remove_instance_hint_hook : (global_reference -> unit) Hook.t val add_instance_hint : global_reference_or_constr -> global_reference list -> - bool -> int option -> Decl_kinds.polymorphic -> unit + bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit val remove_instance_hint : global_reference -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t -val declare_instance : int option -> bool -> global_reference -> unit +val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit (** Build the subinstances hints for a given typeclass object. check tells if we should check for existence of the subinstances and add only the missing ones. *) -val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) -> - (global_reference list * int option * constr) list +val build_subclasses : check:bool -> env -> evar_map -> global_reference -> + Vernacexpr.hint_info_expr -> + (global_reference list * Vernacexpr.hint_info_expr * constr) list diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5455ab891..3494ad006 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -166,14 +166,17 @@ module Make | ModeNoHeadEvar -> str"!" | ModeOutput -> str"-" + let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } = + pr_opt (fun x -> str"|" ++ int x) pri ++ + pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat + let pr_hints db h pr_c pr_pat = let opth = pr_opt_hintbases db in let pph = match h with | HintsResolve l -> keyword "Resolve " ++ prlist_with_sep sep - (fun (pri, _, c) -> pr_reference_or_constr pr_c c ++ - match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ()) + (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info) l | HintsImmediate l -> keyword "Immediate" ++ spc() ++ @@ -888,7 +891,7 @@ module Make spc() ++ pr_class_rawexpr c2) ) - | VernacInstance (abst, sup, (instid, bk, cl), props, pri) -> + | VernacInstance (abst, sup, (instid, bk, cl), props, info) -> return ( hov 1 ( (if abst then keyword "Declare" ++ spc () else mt ()) ++ @@ -899,7 +902,7 @@ module Make pr_and_type_binders_arg sup ++ str":" ++ spc () ++ (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ - pr_constr cl ++ pr_priority pri ++ + pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with | Some (true,CRecord (_,l)) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" | Some (true,_) -> assert false @@ -913,11 +916,14 @@ module Make keyword "Context" ++ spc () ++ pr_and_type_binders_arg l) ) - | VernacDeclareInstances (ids, pri) -> - return ( + | VernacDeclareInstances insts -> + let pr_inst (id, info) = + pr_reference id ++ pr_hint_info pr_constr_pattern_expr info + in + return ( hov 1 (keyword "Existing" ++ spc () ++ - keyword(String.plural (List.length ids) "Instance") ++ - spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri) + keyword(String.plural (List.length insts) "Instance") ++ + spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts) ) | VernacDeclareClass id -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b590a8c93..e117f1dcb 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -872,7 +872,7 @@ let pr_instance env i = (* gallina_print_constant_with_infos i.is_impl *) (* lighter *) print_ref false (instance_impl i) ++ - begin match instance_priority i with + begin match hint_priority i with | None -> mt () | Some i -> spc () ++ str "|" ++ spc () ++ int i end diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index af1ab4197..262b30893 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -9,7 +9,6 @@ (* TODO: - Find an interface allowing eauto to backtrack when shelved goals remain, e.g. to force instantiations. - - unique solutions *) open Pp @@ -93,7 +92,7 @@ open Goptions let _ = declare_bool_option { optsync = true; - optdepr = false; + optdepr = true; optname = "do typeclass search modulo eta conversion"; optkey = ["Typeclasses";"Modulo";"Eta"]; optread = get_typeclasses_modulo_eta; @@ -181,6 +180,12 @@ let set_typeclasses_depth = optread = get_typeclasses_depth; optwrite = set_typeclasses_depth; } +type search_strategy = Dfs | Bfs + +let set_typeclasses_strategy = function + | Dfs -> set_typeclasses_iterative_deepening false + | Bfs -> set_typeclasses_iterative_deepening true + let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) @@ -240,12 +245,11 @@ let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> end } (** Application of a lemma using [refine] instead of the old [w_unify] *) -let unify_resolve_refine poly flags = +let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = let open Clenv in - { enter = begin fun gls ((c, t, ctx),n,clenv) -> - let env = Proofview.Goal.env gls in - let concl = Proofview.Goal.concl gls in - Refine.refine ~unsafe:true { Sigma.run = fun sigma -> + let env = Proofview.Goal.env gls in + let concl = Proofview.Goal.concl gls in + Refine.refine ~unsafe:true { Sigma.run = fun sigma -> let sigma = Sigma.to_evar_map sigma in let sigma, term, ty = if poly then @@ -260,15 +264,20 @@ let unify_resolve_refine poly flags = let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in let term = applistc term (List.map (fun x -> x.hole_evar) cl.cl_holes) in let sigma' = - let evdref = ref sigma' in - if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta - evdref cl.cl_concl concl) then - Type_errors.error_actual_type env - {Environ.uj_val = term; Environ.uj_type = cl.cl_concl} - concl; - !evdref + Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta + cl.cl_concl concl sigma' in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') } - end } + +let unify_resolve_refine poly flags gl clenv = + Proofview.tclORELSE + (unify_resolve_refine poly flags gl clenv) + (fun ie -> + match fst ie with + | Evarconv.UnableToUnify _ -> + Tacticals.New.tclZEROMSG (str "Unable to unify") + | e when CErrors.noncritical e -> + Tacticals.New.tclZEROMSG (str "Unexpected error") + | _ -> iraise ie) (** Dealing with goals of the form A -> B and hints of the form C -> A -> B. @@ -289,9 +298,11 @@ let clenv_of_prods poly nprods (c, clenv) gl = let with_prods nprods poly (c, clenv) f = if get_typeclasses_limit_intros () then Proofview.Goal.nf_enter { enter = begin fun gl -> - match clenv_of_prods poly nprods (c, clenv) gl with - | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses") - | Some (diff, clenv') -> f.enter gl (c, diff, clenv') end } + try match clenv_of_prods poly nprods (c, clenv) gl with + | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses") + | Some (diff, clenv') -> f.enter gl (c, diff, clenv') + with e when CErrors.noncritical e -> + Tacticals.New.tclZEROMSG (CErrors.print e) end } else Proofview.Goal.nf_enter { enter = begin fun gl -> if Int.equal nprods 0 then f.enter gl (c, None, clenv) @@ -306,7 +317,7 @@ let matches_pattern concl pat = if Constr_matching.is_matching env sigma pat concl then Proofview.tclUNIT () else - Tacticals.New.tclZEROMSG (str "conclPattern") + Tacticals.New.tclZEROMSG (str "pattern does not match") in Proofview.Goal.enter { enter = fun gl -> let env = Proofview.Goal.env gl in @@ -334,10 +345,19 @@ let pr_gls sigma gls = let shelve_dependencies gls = let open Proofview in tclEVARMAP >>= fun sigma -> - (if !typeclasses_debug > 1 then - Feedback.msg_debug (str" shelving goals: " ++ pr_gls sigma gls); + (if !typeclasses_debug > 1 && List.length gls > 0 then + Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls); shelve_goals gls) +let hintmap_of hdc secvars concl = + match hdc with + | None -> fun db -> Hint_db.map_none secvars db + | Some hdc -> + fun db -> + if Hint_db.use_dn db then (* Using dnet *) + Hint_db.map_eauto secvars hdc concl db + else Hint_db.map_existential secvars hdc concl db + (** Hack to properly solve dependent evars that are typeclasses *) let rec e_trivial_fail_db only_classes db_list local_db secvars = let open Tacticals.New in @@ -373,20 +393,20 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co let nprods = List.length prods in let freeze = try - let cl = Typeclasses.class_info (fst hdc) in - if cl.cl_strict then - Evd.evars_of_term concl - else Evar.Set.empty + match hdc with + | Some (hd,_) when only_classes -> + let cl = Typeclasses.class_info hd in + if cl.cl_strict then + Evd.evars_of_term concl + else Evar.Set.empty + | _ -> Evar.Set.empty with e when CErrors.noncritical e -> Evar.Set.empty in + let hint_of_db = hintmap_of hdc secvars concl in let hintl = List.map_append (fun db -> - let tacs = - if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto secvars hdc concl db - else Hint_db.map_existential secvars hdc concl db - in + let tacs = hint_of_db db in let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in List.map (fun x -> (flags, x)) tacs) (local_db::db_list) @@ -399,8 +419,8 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co let tac = with_prods nprods poly (term,cl) ({ enter = fun gl clenv -> - (matches_pattern concl p) <*> - ((unify_resolve_refine poly flags).enter gl clenv)}) + matches_pattern concl p <*> + unify_resolve_refine poly flags gl clenv}) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = @@ -414,8 +434,8 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co if get_typeclasses_filtered_unification () then let tac = (with_prods nprods poly (term,cl) ({ enter = fun gl clenv -> - (matches_pattern concl p) <*> - ((unify_resolve_refine poly flags).enter gl clenv)})) in + matches_pattern concl p <*> + unify_resolve_refine poly flags gl clenv})) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = @@ -425,7 +445,15 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co else Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) - | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c) + | Give_exact (c,clenv) -> + if get_typeclasses_filtered_unification () then + let tac = + matches_pattern concl p <*> + Proofview.Goal.nf_enter + { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in + Tacticals.New.tclTHEN tac Proofview.shelve_unifiable + else + Proofview.V82.tactic (e_give_exact flags poly (c,clenv)) | Res_pf_THEN_trivial_fail (term,cl) -> let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in let snd = if complete then Tacticals.New.tclIDTAC @@ -450,16 +478,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db secvars only_classes sigma concl = + let hd = try Some (decompose_app_bound concl) with Bound -> None in try - e_my_find_search db_list local_db secvars - (decompose_app_bound concl) true only_classes sigma concl - with Bound | Not_found -> [] + e_my_find_search db_list local_db secvars hd true only_classes sigma concl + with Not_found -> [] let e_possible_resolve db_list local_db secvars only_classes sigma concl = + let hd = try Some (decompose_app_bound concl) with Bound -> None in try - e_my_find_search db_list local_db secvars - (decompose_app_bound concl) false only_classes sigma concl - with Bound | Not_found -> [] + e_my_find_search db_list local_db secvars hd false only_classes sigma concl + with Not_found -> [] let cut_of_hints h = List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h @@ -539,10 +567,16 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let name = PathHints [VarRef id] in let hints = if is_class then - let hints = build_subclasses ~check:false env sigma (VarRef id) None in + let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in (List.map_append - (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path) - (true,false,Flags.is_verbose()) pri false + (fun (path,info,c) -> + let info = + { info with Vernacexpr.hint_pattern = + Option.map (Constrintern.intern_constr_pattern env) + info.Vernacexpr.hint_pattern } + in + make_resolves env sigma ~name:(PathHints path) + (true,false,Flags.is_verbose()) info false (IsConstr (c,Univ.ContextSet.empty))) hints) else [] @@ -567,7 +601,7 @@ let make_hints g st only_classes sign = in if consider then let hint = - pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp + pf_apply make_resolve_hyp g st (true,false,false) only_classes empty_hint_info hyp in hint @ hints else hints) ([]) sign @@ -636,7 +670,7 @@ module V85 = struct let env = Goal.V82.env s g' in let context = Environ.named_context_of_val (Goal.V82.hyps s g') in let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) - (true,false,false) info.only_classes None (List.hd context) in + (true,false,false) info.only_classes empty_hint_info (List.hd context) in let ldb = Hint_db.add_list env s hint info.hints in (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls @@ -880,19 +914,20 @@ module V85 = struct let eauto_tac hints = then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) - let eauto_tac depth hints = - if get_typeclasses_iterative_deepening () then - match depth with - | None -> fix_iterative (eauto_tac hints) - | Some depth -> fix_iterative_limit depth (eauto_tac hints) - else - match depth with - | None -> fix (eauto_tac hints) - | Some depth -> fix_limit depth (eauto_tac hints) - - let real_eauto ?depth unique st hints p evd = + let eauto_tac strategy depth hints = + match strategy with + | Bfs -> + begin match depth with + | None -> fix_iterative (eauto_tac hints) + | Some depth -> fix_iterative_limit depth (eauto_tac hints) end + | Dfs -> + match depth with + | None -> fix (eauto_tac hints) + | Some depth -> fix_limit depth (eauto_tac hints) + + let real_eauto ?depth strategy unique st hints p evd = let res = - run_on_evars ~st ~unique p evd hints (eauto_tac depth hints) + run_on_evars ~st ~unique p evd hints (eauto_tac strategy depth hints) in match res with | None -> evd @@ -905,12 +940,18 @@ module V85 = struct let resolve_all_evars_once debug depth unique p evd = let db = searchtable_map typeclasses_db in - real_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd - - let eauto85 ?(only_classes=true) ?st depth hints g = + let strategy = if get_typeclasses_iterative_deepening () then Bfs else Dfs in + real_eauto ?depth strategy unique (Hint_db.transparent_state db) [db] p evd + + let eauto85 ?(only_classes=true) ?st ?strategy depth hints g = + let strategy = + match strategy with + | None -> if get_typeclasses_iterative_deepening () then Bfs else Dfs + | Some s -> s + in let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; } in - match run_tac (eauto_tac depth hints) gl with + match run_tac (eauto_tac strategy depth hints) gl with | None -> raise Not_found | Some {it = goals; sigma = s; } -> {it = List.map fst goals; sigma = s;} @@ -986,6 +1027,18 @@ module Search = struct Evd.add sigma gl evi') sigma goals + let fail_if_nonclass info = + Proofview.Goal.enter { enter = fun gl -> + let gl = Proofview.Goal.assume gl in + let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + if is_class_type sigma (Proofview.Goal.concl gl) then + Proofview.tclUNIT () + else (if !typeclasses_debug > 1 then + Feedback.msg_debug (pr_depth info.search_depth ++ + str": failure due to non-class subgoal " ++ + pr_ev sigma (Proofview.Goal.goal gl)); + Proofview.tclZERO NotApplicableEx) } + (** The general hint application tactic. tac1 + tac2 .... The choice of OR or ORELSE is determined depending on the dependencies of the goal and the unique/Prop @@ -1018,13 +1071,18 @@ module Search = struct let foundone = ref false in let rec onetac e (tac, pat, b, name, pp) tl = let derivs = path_derivate info.search_cut name in - (if !typeclasses_debug > 1 then - Feedback.msg_debug - (pr_depth (!idx :: info.search_depth) ++ str": trying " ++ + let pr_error ie = + if !typeclasses_debug > 1 then + let msg = + pr_depth (!idx :: info.search_depth) ++ str": " ++ Lazy.force pp ++ (if !foundone != true then str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl) - else mt ()))); + else mt ()) + in + Feedback.msg_debug (msg ++ str " failed with " ++ CErrors.iprint ie) + else () + in let tac_of gls i j = Goal.nf_enter { enter = fun gl' -> let sigma' = Goal.sigma gl' in let s' = Sigma.to_evar_map sigma' in @@ -1091,7 +1149,7 @@ module Search = struct in the subgoals, turn them into subgoals now. *) let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in let shelved = List.map fst shelved and goals = List.map fst goals in - if !typeclasses_debug > 1 then + if !typeclasses_debug > 1 && not (List.is_empty goals) then Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++ prlist_with_sep spc (pr_ev sigma) goals ++ @@ -1107,10 +1165,18 @@ module Search = struct in res <*> tclEVARMAP >>= finish in if path_matches derivs [] then aux e tl - else ortac - (with_shelf tac >>= fun s -> + else + let filter = + if info.search_only_classes then fail_if_nonclass info + else Proofview.tclUNIT () + in + ortac + (with_shelf (tac <*> filter) >>= fun s -> let i = !idx in incr idx; result s i None) - (fun e' -> aux (merge_exceptions e e') tl) + (fun e' -> + if CErrors.noncritical (fst e') then + (pr_error e'; aux (merge_exceptions e e') tl) + else (Printf.printf "raising again\n%!"; iraise e')) and aux e = function | x :: xs -> onetac e x xs | [] -> @@ -1140,7 +1206,7 @@ module Search = struct let decl = Tacmach.New.pf_last_hyp gl in let hint = make_resolve_hyp env s (Hint_db.transparent_state info.search_hints) - (true,false,false) info.search_only_classes None decl in + (true,false,false) info.search_only_classes empty_hint_info decl in let ldb = Hint_db.add_list env s hint info.search_hints in let info' = { info with search_hints = ldb; last_tac = lazy (str"intro"); @@ -1172,9 +1238,12 @@ module Search = struct unit Proofview.tactic = let open Proofview in let open Proofview.Notations in - let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in - let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in - search_tac hints depth 1 info + if only_classes && not (is_class_type sigma (Goal.concl gl)) then + Proofview.shelve + else + let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in + let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in + search_tac hints depth 1 info let search_tac ?(st=full_transparent_state) only_classes dep hints depth = let open Proofview in @@ -1205,16 +1274,45 @@ module Search = struct | (e,ie) -> Proofview.tclZERO ~info:ie e) in aux 1 - let eauto_tac ?(st=full_transparent_state) ~only_classes ~depth ~dep hints = + let disallow_shelved initshelf tac = + let open Proofview in + let casefn = function + | Fail (e,info) -> tclZERO ~info e + | Next ((shelved, result), k) -> + if not (List.is_empty shelved) then + begin + Proofview.tclEVARMAP >>= fun sigma -> + let gls = prlist_with_sep spc (pr_ev sigma) shelved in + (if !typeclasses_debug > 0 then + let initgls = prlist_with_sep spc (pr_ev sigma) initshelf in + Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls + ++ str" initially: " ++ initgls ++ str".")); + Tacticals.New.tclZEROMSG (str"Proof search failed: " ++ + str"shelved goals remain: " ++ gls) + end + else + tclOR (tclUNIT result) (fun e -> k e >>= fun (gls, result) -> tclUNIT result) + in + tclCASE (with_shelf tac) >>= casefn + + let eauto_tac ?(st=full_transparent_state) ?(unique=false) + ~only_classes ?strategy ~depth ~dep hints = + let open Proofview in let tac = let search = search_tac ~st only_classes dep hints in - if get_typeclasses_iterative_deepening () then + let dfs = + match strategy with + | None -> not (get_typeclasses_iterative_deepening ()) + | Some Dfs -> true + | Some Bfs -> false + in + if dfs then + let depth = match depth with None -> -1 | Some d -> d in + search depth + else match depth with | None -> fix_iterative search | Some l -> fix_iterative_limit l search - else - let depth = match depth with None -> -1 | Some d -> d in - search depth in let error (e, ie) = match e with @@ -1224,10 +1322,30 @@ module Search = struct Tacticals.New.tclFAIL 0 (str"Proof search failed" ++ (if Option.is_empty depth then mt() else str" without reaching its limit")) + | Proofview.MoreThanOneSuccess -> + Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++ + str"more than one success found") | e -> Proofview.tclZERO ~info:ie e - in Proofview.tclOR tac error - - let run_on_evars ?(unique=false) p evm tac = + in + let tac = Proofview.tclOR tac error in + let tac = + if unique then + Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac + else tac + in + with_shelf numgoals >>= fun (initshelf, i) -> + (if !typeclasses_debug > 1 then + Feedback.msg_debug (str"Starting resolution with " ++ int i ++ + str" goal(s) under focus and " ++ + int (List.length initshelf) ++ str " shelved goal(s)" ++ + if only_classes then str " in only_classes mode" else + str " in regular mode" ++ + match depth with None -> str ", unbounded" + | Some i -> str ", with depth limit " ++ int i)); + let tac = if only_classes then disallow_shelved initshelf tac else tac in + tac + + let run_on_evars p evm tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) | Some (goals, evm') -> @@ -1259,16 +1377,15 @@ module Search = struct else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found - let eauto depth only_classes unique dep st hints p evd = - let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep hints in - let res = run_on_evars ~unique p evd eauto_tac in + let evars_eauto depth only_classes unique dep st hints p evd = + let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in + let res = run_on_evars p evd eauto_tac in match res with | None -> evd | Some evd' -> evd' - (* TODO treat unique solutions *) let typeclasses_eauto ?depth unique st hints p evd = - eauto depth true unique false st hints p evd + evars_eauto depth true unique false st hints p evd (** Typeclasses eauto is an eauto which tries to resolve only goals of typeclass type, and assumes that the initially selected evars in evd are independent of the rest of the evars *) @@ -1279,11 +1396,9 @@ module Search = struct end (** Binding to either V85 or Search implementations. *) -let eauto depth ~only_classes ~st ~dep dbs = - Search.eauto_tac ~st ~only_classes ~depth ~dep dbs let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) - ~depth dbs = + ?strategy ~depth dbs = let dbs = List.map_filter (fun db -> try Some (searchtable_map db) with e when CErrors.noncritical e -> None) @@ -1294,10 +1409,10 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) if get_typeclasses_legacy_resolution () then Proofview.V82.tactic (fun gl -> - try V85.eauto85 depth ~only_classes ~st dbs gl + try V85.eauto85 depth ~only_classes ~st ?strategy dbs gl with Not_found -> Refiner.tclFAIL 0 (str"Proof search failed") gl) - else eauto depth ~only_classes ~st ~dep:true dbs + else Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs (** We compute dependencies via a union-find algorithm. Beware of the imperative effects on the partition structure, diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 8db264ad9..76760db02 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -20,7 +20,11 @@ val get_typeclasses_debug : unit -> bool val set_typeclasses_depth : int option -> unit val get_typeclasses_depth : unit -> int option -val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> +type search_strategy = Dfs | Bfs + +val set_typeclasses_strategy : search_strategy -> unit + +val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy -> depth:(Int.t option) -> Hints.hint_db_name list -> unit Proofview.tactic @@ -36,8 +40,12 @@ module Search : sig val eauto_tac : ?st:Names.transparent_state -> (** The transparent_state used when working with local hypotheses *) + ?unique:bool -> + (** Should we force a unique solution *) only_classes:bool -> (** Should non-class goals be shelved and resolved at the end *) + ?strategy:search_strategy -> + (** Is a traversing-strategy specified? *) depth:Int.t option -> (** Bounded or unbounded search *) dep:bool -> diff --git a/tactics/hints.ml b/tactics/hints.ml index ba92b74df..d91ea8079 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -84,6 +84,10 @@ let secvars_of_hyps hyps = if all then Id.Pred.full (* If the whole section context is available *) else pred +let empty_hint_info = + let open Vernacexpr in + { hint_priority = None; hint_pattern = None } + (************************************************************************) (* The Type of Constructions Autotactic Hints *) (************************************************************************) @@ -735,7 +739,7 @@ let secvars_of_constr env c = let secvars_of_global env gr = secvars_of_idset (vars_of_global_reference env gr) -let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = +let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = let secvars = secvars_of_constr env c in let cty = strip_outer_cast cty in match kind_of_term cty with @@ -746,16 +750,17 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" in - (Some hd, - { pri = (match pri with None -> 0 | Some p -> p); - poly = poly; - pat = Some pat; - name = name; - db = None; - secvars; - code = with_uid (Give_exact (c, cty, ctx)); }) + let pri = match info.hint_priority with None -> 0 | Some p -> p in + let pat = match info.hint_pattern with + | Some pat -> snd pat + | None -> pat + in + (Some hd, + { pri; poly; pat = Some pat; name; + db = None; secvars; + code = with_uid (Give_exact (c, cty, ctx)); }) -let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) = +let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in match kind_of_term cty with | Prod _ -> @@ -768,12 +773,13 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, with BoundPattern -> failwith "make_apply_entry" in let nmiss = List.length (clenv_missing ce) in let secvars = secvars_of_constr env c in + let pri = match info.hint_priority with None -> nb_hyp cty + nmiss | Some p -> p in + let pat = match info.hint_pattern with + | Some p -> snd p | None -> pat + in if Int.equal nmiss 0 then (Some hd, - { pri = (match pri with None -> nb_hyp cty | Some p -> p); - poly = poly; - pat = Some pat; - name = name; + { pri; poly; pat = Some pat; name; db = None; secvars; code = with_uid (Res_pf(c,cty,ctx)); }) @@ -783,12 +789,8 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); (Some hd, - { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); - poly = poly; - pat = Some pat; - name = name; - db = None; - secvars; + { pri; poly; pat = Some pat; name; + db = None; secvars; code = with_uid (ERes_pf(c,cty,ctx)); }) end | _ -> failwith "make_apply_entry" @@ -839,14 +841,14 @@ let fresh_global_or_constr env sigma poly cr = (c, Univ.ContextSet.empty) end -let make_resolves env sigma flags pri poly ?name cr = +let make_resolves env sigma flags info poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in let cty = Retyping.get_type_of env sigma c in let try_apply f = try Some (f (c, cty, ctx)) with Failure _ -> None in let ents = List.map_filter try_apply - [make_exact_entry env sigma pri poly ?name; - make_apply_entry env sigma flags pri poly ?name] + [make_exact_entry env sigma info poly ?name; + make_apply_entry env sigma flags info poly ?name] in if List.is_empty ents then errorlabstrm "Hint" @@ -860,7 +862,7 @@ let make_resolve_hyp env sigma decl = let hname = get_id decl in let c = mkVar hname in try - [make_apply_entry env sigma (true, true, false) None false + [make_apply_entry env sigma (true, true, false) empty_hint_info false ~name:(PathHints [VarRef hname]) (c, get_type decl, Univ.ContextSet.empty)] with @@ -1144,16 +1146,17 @@ let add_transparency l b local dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_extern pri pat tacast local dbname = - let pat = match pat with +let add_extern info tacast local dbname = + let pat = match info.hint_pattern with | None -> None | Some (_, pat) -> Some pat in - let hint = make_hint ~local dbname (AddHints [make_extern pri pat tacast]) in + let hint = make_hint ~local dbname + (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in Lib.add_anonymous_leaf (inAutoHint hint) -let add_externs pri pat tacast local dbnames = - List.iter (add_extern pri pat tacast local) dbnames +let add_externs info tacast local dbnames = + List.iter (add_extern info tacast local) dbnames let add_trivials env sigma l local dbnames = List.iter @@ -1167,15 +1170,16 @@ let (forward_intern_tac, extern_intern_tac) = Hook.make () type hnf = bool +type hint_info = (patvar list * constr_pattern) hint_info_gen + type hints_entry = - | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list + | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsModeEntry of global_reference * hint_mode list - | HintsExternEntry of - int * (patvar list * constr_pattern) option * glob_tactic_expr + | HintsExternEntry of hint_info * glob_tactic_expr let default_prepare_hint_ident = Id.of_string "H" @@ -1239,11 +1243,12 @@ let interp_hints poly = (PathHints [gr], poly, IsGlobRef gr) | HintsConstr c -> (PathAny, poly, f poly c) in - let fres (pri, b, r) = + let fp = Constrintern.intern_constr_pattern (Global.env()) in + let fres (info, b, r) = let path, poly, gr = fi r in - (pri, poly, b, path, gr) + let info = { info with hint_pattern = Option.map fp info.hint_pattern } in + (info, poly, b, path, gr) in - let fp = Constrintern.intern_constr_pattern (Global.env()) in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) @@ -1259,14 +1264,14 @@ let interp_hints poly = List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in - None, mib.Declarations.mind_polymorphic, true, + empty_hint_info, mib.Declarations.mind_polymorphic, true, PathHints [gr], IsGlobRef gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> let pat = Option.map fp patcom in let l = match pat with None -> [] | Some (l, _) -> l in let tacexp = Hook.get forward_intern_tac l tacexp in - HintsExternEntry (pri, pat, tacexp) + HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) let add_hints local dbnames0 h = if String.List.mem "nocore" dbnames0 then @@ -1282,8 +1287,8 @@ let add_hints local dbnames0 h = | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames | HintsTransparencyEntry (lhints, b) -> add_transparency lhints b local dbnames - | HintsExternEntry (pri, pat, tacexp) -> - add_externs pri pat tacexp local dbnames + | HintsExternEntry (info, tacexp) -> + add_externs info tacexp local dbnames let expand_constructor_hints env sigma lems = List.map_append (fun (evd,lem) -> @@ -1307,7 +1312,7 @@ let add_hint_lemmas env sigma eapply lems hint_db = let lems = expand_constructor_hints env sigma lems in let hintlist' = List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) None poly lem) lems in + make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in Hint_db.add_list env sigma hintlist' hint_db let make_local_hint_db env sigma ts eapply lems = @@ -1361,7 +1366,9 @@ let pr_hint h = match h.obj with (str "(*external*) " ++ Pptactic.pr_glb_generic env tac) let pr_id_hint (id, v) = - (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) + let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in + (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat + ++ str", id " ++ int id ++ str ")" ++ spc ()) let pr_hint_list hintlist = (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ()) diff --git a/tactics/hints.mli b/tactics/hints.mli index 8145ae193..42a2896ed 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -27,6 +27,8 @@ val decompose_app_bound : constr -> global_reference * constr array val secvars_of_hyps : Context.Named.t -> Id.Pred.t +val empty_hint_info : 'a hint_info_gen + (** Pre-created hint databases *) type 'a hint_ast = @@ -129,20 +131,21 @@ type hint_db = Hint_db.t type hnf = bool +type hint_info = (patvar list * constr_pattern) hint_info_gen + type hint_term = | IsGlobRef of global_reference | IsConstr of constr * Univ.universe_context_set type hints_entry = - | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * - hint_term) list + | HintsResolveEntry of + (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsModeEntry of global_reference * hint_mode list - | HintsExternEntry of - int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr + | HintsExternEntry of hint_info * Tacexpr.glob_tactic_expr val searchtable_map : hint_db_name -> hint_db @@ -169,23 +172,34 @@ val prepare_hint : bool (* Check no remaining evars *) -> (bool * bool) (* polymorphic or monomorphic, local or global *) -> env -> evar_map -> open_constr -> hint_term -(** [make_exact_entry pri (c, ctyp, ctx, secvars)]. +(** [make_exact_entry info (c, ctyp, ctx)]. [c] is the term given as an exact proof to solve the goal; [ctyp] is the type of [c]. - [ctx] is its (refreshable) universe context. *) -val make_exact_entry : env -> evar_map -> int option -> polymorphic -> ?name:hints_path_atom -> + [ctx] is its (refreshable) universe context. + In info: + [hint_priority] is the hint's desired priority, it is 0 if unspecified + [hint_pattern] is the hint's desired pattern, it is inferred if not specified +*) + +val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom -> (constr * types * Univ.universe_context_set) -> hint_entry -(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty,ctx,secvars)]. +(** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))]. [eapply] is true if this hint will be used only with EApply; [hnf] should be true if we should expand the head of cty before searching for products; [c] is the term given as an exact proof to solve the goal; [cty] is the type of [c]. - [ctx] is its (refreshable) universe context. *) + [ctx] is its (refreshable) universe context. + In info: + [hint_priority] is the hint's desired priority, it is computed as the number of products in [cty] + if unspecified + [hint_pattern] is the hint's desired pattern, it is inferred from the conclusion of [cty] + if not specified +*) val make_apply_entry : - env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom -> + env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom -> (constr * types * Univ.universe_context_set) -> hint_entry (** A constr which is Hint'ed will be: @@ -196,7 +210,7 @@ val make_apply_entry : has missing arguments. *) val make_resolves : - env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom -> + env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom -> hint_term -> hint_entry list (** [make_resolve_hyp hname htyp]. diff --git a/tactics/tactics.ml b/tactics/tactics.ml index db19d54bd..9d64e7c59 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -83,7 +83,7 @@ let _ = let apply_solve_class_goals = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optsync = true; Goptions.optdepr = true; Goptions.optname = "Perform typeclass resolution on apply-generated subgoals."; Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"]; diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index fcdfa0057..ff515038e 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -1,4 +1,3 @@ -Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *) Require Coq.Setoids.Setoid. Import Coq.Setoids.Setoid. @@ -35,7 +34,7 @@ Local Existing Instance ILFun_Ops. Local Existing Instance ILFun_ILogic. Definition catOP (P Q: OPred) : OPred := admit. Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m. -admit. +apply admit. Defined. Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit. Class IsPointed (T : Type) := point : T. @@ -69,8 +68,26 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) pose P; refine (P _ _) end; unfold Basics.flip. - 2: solve [ apply reflexivity ]. - Undo. - 2: reflexivity. (* Toplevel input, characters 18-29: -Error: -Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file + Focus 2. + Set Typeclasses Debug. + Set Typeclasses Legacy Resolution. + apply reflexivity. + (* Debug: 1.1: apply @IsPointed_catOP on +(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0)) +Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0)) +Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x)) +Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails) +Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities +Debug: Backtracking after apply @Equivalence_Reflexive +Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails) +Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails) +Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) +*) + Undo. Unset Typeclasses Legacy Resolution. + Test Typeclasses Unique Solutions. + Test Typeclasses Unique Instances. + Show Existentials. + Set Typeclasses Debug Verbosity 2. + Set Printing All. + Fail apply reflexivity. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 8dadc2419..efa432526 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -34,8 +34,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -47,8 +46,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. @@ -111,8 +109,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -124,8 +121,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v new file mode 100644 index 000000000..83d4ed69d --- /dev/null +++ b/test-suite/bugs/closed/4095.v @@ -0,0 +1,87 @@ +(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines, then from 92 lines to 79 lines *) +(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *) +Require Import TestSuite.admit. +Require Import Coq.Setoids.Setoid. +Generalizable All Variables. +Axiom admit : forall {T}, T. +Class Equiv (A : Type) := equiv : relation A. +Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv. +Class ILogicOps Frm := { lentails: relation Frm; + ltrue: Frm; + land: Frm -> Frm -> Frm; + lor: Frm -> Frm -> Frm }. +Infix "|--" := lentails (at level 79, no associativity). +Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. +Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. +Infix "-|-" := lequiv (at level 85, no associativity). +Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. +Section ILogic_Fun. + Context (T: Type) `{TType: type T}. + Context `{IL: ILogic Frm}. + Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit. + Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit. +End ILogic_Fun. +Implicit Arguments ILFunFrm [[ILOps] [e]]. +Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; + ltrue := True; + land P Q := P /\ Q; + lor P Q := P \/ Q |}. +Axiom Action : Set. +Definition Actions := list Action. +Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }. +Definition OPred := ILFunFrm Actions Prop. +Local Existing Instance ILFun_Ops. +Local Existing Instance ILFun_ILogic. +Definition catOP (P Q: OPred) : OPred := admit. +Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m. +admit. +Defined. +Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit. +Class IsPointed (T : Type) := point : T. +Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)). +Record PointedOPred := mkPointedOPred { + OPred_pred :> OPred; + OPred_inhabited: IsPointed_OPred OPred_pred + }. +Existing Instance OPred_inhabited. +Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred + := {| OPred_pred := O ; OPred_inhabited := _ |}. +Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit. +Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) + (tr : T -> T) (O2 : PointedOPred) (x : T) + (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0), + exists e1 e2, + catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2. + intros; do 2 esplit. + rewrite <- catOPA. + lazymatch goal with + | |- ?R (?f ?a ?b) (?f ?a' ?b') => + let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred) + (@Morphisms.respectful OPred (OPred -> OPred) + (@lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop)) + (@lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==> + @lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP + catOP_entails_m_Proper a a' H b b' H') in + pose P; + refine (P _ _) + end. + Undo. + lazymatch goal with + | |- ?R (?f ?a ?b) (?f ?a' ?b') => + let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in + set(p:=P) + end. (* Toplevel input, characters 15-182: +Error: Cannot infer an instance of type +"PointedOPred" for the variable p in environment: +T : Type +O0 : T -> OPred +O1 : T -> PointedOPred +tr : T -> T +O2 : PointedOPred +x0 : T +H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v index e884355fd..1e47f2957 100644 --- a/test-suite/bugs/closed/4863.v +++ b/test-suite/bugs/closed/4863.v @@ -3,14 +3,14 @@ Require Import Classes.DecidableClass. Inductive Foo : Set := | foo1 | foo2. -Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P. +Lemma Decidable_sumbool : forall P, {P}+{~P} -> Decidable P. Proof. intros P H. refine (Build_Decidable _ (if H then true else false) _). intuition congruence. Qed. -Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances. +Hint Extern 100 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; decide equality))) : typeclass_instances. Goal forall (a b : Foo), {a=b}+{a<>b}. intros. @@ -21,7 +21,8 @@ Check ltac:(abstract (exact I)) : True. Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). intros. -split. typeclasses eauto. typeclasses eauto. Qed. +split. typeclasses eauto. +typeclasses eauto. Qed. Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). intros. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 89b8bd7ac..1abe14774 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -1,4 +1,12 @@ (* Checks syntax of Hints commands *) +(* Old-style syntax *) +Hint Resolve eq_refl eq_sym. +Hint Resolve eq_refl eq_sym: foo. +Hint Immediate eq_refl eq_sym. +Hint Immediate eq_refl eq_sym: foo. +Hint Unfold fst eq_sym. +Hint Unfold fst eq_sym: foo. + (* Checks that qualified names are accepted *) (* New-style syntax *) @@ -8,13 +16,76 @@ Hint Unfold eq_sym: core. Hint Constructors eq: foo bar. Hint Extern 3 (_ = _) => apply eq_refl: foo bar. -(* Old-style syntax *) -Hint Resolve eq_refl eq_sym. -Hint Resolve eq_refl eq_sym: foo. -Hint Immediate eq_refl eq_sym. -Hint Immediate eq_refl eq_sym: foo. -Hint Unfold fst eq_sym. -Hint Unfold fst eq_sym: foo. +(* Extended new syntax with patterns *) +Hint Resolve eq_refl | 4 (_ = _) : baz. +Hint Resolve eq_sym eq_trans : baz. +Hint Extern 3 (_ = _) => apply eq_sym : baz. + +Parameter pred : nat -> Prop. +Parameter pred0 : pred 0. +Parameter f : nat -> nat. +Parameter predf : forall n, pred n -> pred (f n). + +(* No conversion on let-bound variables and constants in pred (the default) *) +Hint Resolve pred0 | 1 (pred _) : pred. +Hint Resolve predf | 0 : pred. + +(* Allow full conversion on let-bound variables and constants *) +Create HintDb predconv discriminated. +Hint Resolve pred0 | 1 (pred _) : predconv. +Hint Resolve predf | 0 : predconv. + +Goal exists n, pred n. + eexists. + Fail Timeout 1 typeclasses eauto with pred. + Set Typeclasses Filtered Unification. + Set Typeclasses Debug Verbosity 2. + (* predf is not tried as it doesn't match the goal *) + typeclasses eauto with pred. +Qed. + +Parameter predconv : forall n, pred n -> pred (0 + S n). + +(* The inferred pattern contains 0 + ?n, syntactic match will fail to see convertible + terms *) +Hint Resolve pred0 : pred2. +Hint Resolve predconv : pred2. + +(** In this database we allow predconv to apply to pred (S _) goals, more generally + than the inferred pattern (pred (0 + S _)). *) +Create HintDb pred2conv discriminated. +Hint Resolve pred0 : pred2conv. +Hint Resolve predconv | 1 (pred (S _)) : pred2conv. + +Goal pred 3. + Fail typeclasses eauto with pred2. + typeclasses eauto with pred2conv. +Abort. + +Set Typeclasses Filtered Unification. +Set Typeclasses Debug Verbosity 2. +Hint Resolve predconv | 1 (pred _) : pred. +Hint Resolve predconv | 1 (pred (S _)) : predconv. +Test Typeclasses Limit Intros. +Goal pred 3. + (* predf is not tried as it doesn't match the goal *) + (* predconv is tried but fails as the transparent state doesn't allow + unfolding + *) + Fail typeclasses eauto with pred. + (* Here predconv succeeds as it matches (pred (S _)) and then + full unification is allowed *) + typeclasses eauto with predconv. +Qed. + +(** The other way around: goal contains redexes instead of instances *) +Goal exists n, pred (0 + n). + eexists. + (* predf is applied indefinitely *) + Fail Timeout 1 typeclasses eauto with pred. + (* pred0 (pred _) matches the goal *) + typeclasses eauto with predconv. +Qed. + (* Checks that local names are accepted *) Section A. @@ -105,4 +176,4 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) Timeout 1 Fail apply _. (* 0.06s *) Abort. -End HintCut.
\ No newline at end of file +End HintCut. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 3eaa04144..6885717ec 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -1,3 +1,45 @@ +Module onlyclasses. + + Variable Foo : Type. + Variable foo : Foo. + Hint Extern 0 Foo => exact foo : typeclass_instances. + Goal Foo * Foo. + split. shelve. + Set Typeclasses Debug. + Fail typeclasses eauto. + typeclasses eauto with typeclass_instances. + Unshelve. typeclasses eauto with typeclass_instances. + Qed. +End onlyclasses. + +Module shelve_non_class_subgoals. + Variable Foo : Type. + Variable foo : Foo. + Hint Extern 0 Foo => exact foo : typeclass_instances. + Class Bar := {}. + Instance bar1 (f:Foo) : Bar. + + Typeclasses eauto := debug. + Set Typeclasses Debug Verbosity 2. + Goal Bar. + (* Solution has shelved subgoals (of non typeclass type) *) + Fail typeclasses eauto. + Abort. +End shelve_non_class_subgoals. + +Module Leivantex2PR339. + (** Was a bug preventing to find hints associated with no pattern *) + Class Bar := {}. + Instance bar1 (t:Type) : Bar. + Hint Extern 0 => exact True : typeclass_instances. + Typeclasses eauto := debug. + Goal Bar. + Fail typeclasses eauto. + Set Typeclasses Debug Verbosity 2. + typeclasses eauto with typeclass_instances. + Qed. +End Leivantex2PR339. + Module bt. Require Import Equivalence. @@ -104,6 +146,40 @@ Section sec. Check U (fun x => e x) _. End sec. +Module UniqueSolutions. + Set Typeclasses Unique Solutions. + Class Eq (A : Type) : Set. + Instance eqa : Eq nat := {}. + Instance eqb : Eq nat := {}. + + Goal Eq nat. + try apply _. + Fail exactly_once typeclasses eauto. + Abort. +End UniqueSolutions. + + +Module UniqueInstances. + (** Optimize proof search on this class by never backtracking on (closed) goals + for it. *) + Set Typeclasses Unique Instances. + Class Eq (A : Type) : Set. + Instance eqa : Eq nat := _. constructor. Qed. + Instance eqb : Eq nat := {}. + Class Foo (A : Type) (e : Eq A) : Set. + Instance fooa : Foo _ eqa := {}. + + Tactic Notation "refineu" open_constr(c) := unshelve refine c. + + Set Typeclasses Debug. + Goal { e : Eq nat & Foo nat e }. + unshelve refineu (existT _ _ _). + all:simpl. + (** Does not backtrack on the (wrong) solution eqb *) + Fail all:typeclasses eauto. + Abort. +End UniqueInstances. + Module IterativeDeepening. Class A. diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index bb1cf0654..3178c6fc1 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -1,3 +1,4 @@ +Require Import Program.Tactics. Module Backtracking. Class A := { foo : nat }. @@ -8,7 +9,6 @@ Module Backtracking. Qed. Arguments foo A : clear implicits. - Example find42 : exists n, n = 42. Proof. eexists. @@ -20,9 +20,13 @@ Module Backtracking. Fail reflexivity. Undo 2. (* Without multiple successes it fails *) - Fail all:((once typeclasses eauto) + apply eq_refl). + Set Typeclasses Debug Verbosity 2. + Fail all:((once (typeclasses eauto with typeclass_instances)) + + apply eq_refl). (* Does backtrack if other goals fail *) - all:((typeclasses eauto) + reflexivity). + all:[> typeclasses eauto + reflexivity .. ]. + Undo 1. + all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *) Show Proof. Qed. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 4db547f4e..160f2d9de 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -5,7 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import List. Class A (A : Type). Instance an: A nat. @@ -31,6 +30,8 @@ Defined. Hint Extern 0 (_ /\ _) => constructor : typeclass_instances. +Existing Class and. + Goal exists (T : Type) (t : T), A T /\ B T t. Proof. eexists. eexists. typeclasses eauto. @@ -46,7 +47,7 @@ Class C {T} `(a : A T) (t : T). Require Import Classes.Init. Hint Extern 0 { x : ?A & _ } => unshelve class_apply @existT : typeclass_instances. - +Existing Class sigT. Set Typeclasses Debug. Instance can: C an 0. (* Backtrack on instance implementation *) @@ -63,41 +64,6 @@ Proof. Defined. -Parameter in_list : list (nat * nat) -> nat -> Prop. -Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop := - ~ in_list l n. - -(* Hints Unfold not_in_list. *) - -Axiom - lem1 : - forall (l1 l2 : list (nat * nat)) (n : nat), - not_in_list (l1 ++ l2) n -> not_in_list l1 n. - -Axiom - lem2 : - forall (l1 l2 : list (nat * nat)) (n : nat), - not_in_list (l1 ++ l2) n -> not_in_list l2 n. - -Axiom - lem3 : - forall (l : list (nat * nat)) (n p q : nat), - not_in_list ((p, q) :: l) n -> not_in_list l n. - -Axiom - lem4 : - forall (l1 l2 : list (nat * nat)) (n : nat), - not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n. - -Hint Resolve lem1 lem2 lem3 lem4: essai. - -Goal -forall (l : list (nat * nat)) (n p q : nat), -not_in_list ((p, q) :: l) n -> not_in_list l n. - intros. - eauto with essai. -Qed. - (* Example from Nicolas Magaud on coq-club - Jul 2000 *) Definition Nat : Set := nat. @@ -126,6 +92,9 @@ Qed. Full backtracking on dependent subgoals. *) Require Import Coq.Classes.Init. + +Module NTabareau. + Set Typeclasses Dependency Order. Unset Typeclasses Iterative Deepening. Notation "x .1" := (projT1 x) (at level 3). @@ -149,7 +118,8 @@ Hint Extern 5 (Bar ?D.1) => Hint Extern 5 (Qux ?D.1) => destruct D; simpl : typeclass_instances. -Hint Extern 1 myType => unshelve refine (fooTobar _ _).1 : typeclass_instances. +Hint Extern 1 myType => + unshelve refine (fooTobar _ _).1 : typeclass_instances. Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances. @@ -158,8 +128,94 @@ Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instance Unset Typeclasses Debug. Definition trivial a (H : Foo a) : {b : myType & Qux b}. Proof. - Time typeclasses eauto 10. + Time typeclasses eauto 10 with typeclass_instances. Undo. Set Typeclasses Iterative Deepening. - Time typeclasses eauto. + Time typeclasses eauto with typeclass_instances. Defined. +End NTabareau. + +Module NTabareauClasses. + +Set Typeclasses Dependency Order. +Unset Typeclasses Iterative Deepening. +Notation "x .1" := (projT1 x) (at level 3). +Notation "x .2" := (projT2 x) (at level 3). + +Parameter myType: Type. +Existing Class myType. + +Class Foo (a:myType) := {}. + +Class Bar (a:myType) := {}. + +Class Qux (a:myType) := {}. + +Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}. + +Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}. + +Hint Extern 5 (Bar ?D.1) => + destruct D; simpl : typeclass_instances. + +Hint Extern 5 (Qux ?D.1) => + destruct D; simpl : typeclass_instances. + +Hint Extern 1 myType => + unshelve notypeclasses refine (fooTobar _ _).1 : typeclass_instances. + +Hint Extern 1 myType => + unshelve notypeclasses refine (barToqux _ _).1 : typeclass_instances. + +Hint Extern 0 { x : _ & _ } => + unshelve notypeclasses refine (existT _ _ _) : typeclass_instances. + +Unset Typeclasses Debug. + +Definition trivial a (H : Foo a) : {b : myType & Qux b}. +Proof. + Time typeclasses eauto 10 with typeclass_instances. + Undo. Set Typeclasses Iterative Deepening. + (* Much faster in iteratove deepening mode *) + Time typeclasses eauto with typeclass_instances. +Defined. + +End NTabareauClasses. + + +Require Import List. + +Parameter in_list : list (nat * nat) -> nat -> Prop. +Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop := + ~ in_list l n. + +(* Hints Unfold not_in_list. *) + +Axiom + lem1 : + forall (l1 l2 : list (nat * nat)) (n : nat), + not_in_list (l1 ++ l2) n -> not_in_list l1 n. + +Axiom + lem2 : + forall (l1 l2 : list (nat * nat)) (n : nat), + not_in_list (l1 ++ l2) n -> not_in_list l2 n. + +Axiom + lem3 : + forall (l : list (nat * nat)) (n p q : nat), + not_in_list ((p, q) :: l) n -> not_in_list l n. + +Axiom + lem4 : + forall (l1 l2 : list (nat * nat)) (n : nat), + not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n. + +Hint Resolve lem1 lem2 lem3 lem4: essai. + +Goal +forall (l : list (nat * nat)) (n p q : nat), +not_in_list ((p, q) :: l) n -> not_in_list l n. + intros. + eauto with essai. +Qed. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index d6a6162f9..1528cbb2f 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -46,25 +46,34 @@ let set_typeclass_transparency c local b = let _ = Hook.set Typeclasses.add_instance_hint_hook - (fun inst path local pri poly -> + (fun inst path local info poly -> let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty) | IsGlobal gr -> Hints.IsGlobRef gr in - Flags.silently (fun () -> + let info = + let open Vernacexpr in + { info with hint_pattern = + Option.map + (Constrintern.intern_constr_pattern (Global.env())) + info.hint_pattern } in + Flags.silently (fun () -> Hints.add_hints local [typeclasses_db] (Hints.HintsResolveEntry - [pri, poly, false, Hints.PathHints path, inst'])) ()); + [info, poly, false, Hints.PathHints path, inst'])) ()); Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; Hook.set Typeclasses.classes_transparent_state_hook (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)) - + +open Vernacexpr + (** TODO: add subinstances *) -let existing_instance glob g pri = +let existing_instance glob g info = let c = global g in + let info = Option.default Hints.empty_hint_info info in let instance = Global.type_of_global_unsafe c in let _, r = decompose_prod_assum instance in match class_of_constr r with - | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob + | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob (*FIXME*) (Flags.use_polymorphic_flag ()) c) | None -> user_err_loc (loc_of_reference g, "declare_instance", Pp.str "Constant does not build instances of a declared type class.") @@ -98,12 +107,12 @@ let id_of_class cl = open Pp -let instance_hook k pri global imps ?hook cst = +let instance_hook k info global imps ?hook cst = Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; - Typeclasses.declare_instance pri (not global) cst; + Typeclasses.declare_instance (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype = +let declare_instance_constant k info global imps ?hook id pl poly evm term termtype = let kind = IsDefinition Instance in let evm = let levels = Univ.LSet.union (Universes.universes_of_constr termtype) @@ -118,7 +127,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty let kn = Declare.declare_constant id cdecl in Declare.definition_message id; Universes.register_universe_binders (ConstRef kn) pl; - instance_hook k pri global imps ?hook (ConstRef kn); + instance_hook k info global imps ?hook (ConstRef kn); id let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props @@ -130,7 +139,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let evars = ref (Evd.from_ctx uctx) in let tclass, ids = match bk with - | Implicit -> + | Decl_kinds.Implicit -> Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false (fun avoid (clname, _) -> match clname with @@ -299,7 +308,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let hook vis gr _ = let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; - Typeclasses.declare_instance pri (not global) (ConstRef cst) + Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) in let obls, constr, typ = match term with @@ -378,7 +387,7 @@ let context poly l = let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr t with | Some (rels, ((tc,_), args) as _cl) -> - add_instance (Typeclasses.new_instance tc None false (*FIXME*) + add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*) poly (ConstRef cst)); status (* declare_subclasses (ConstRef cst) cl *) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 7beb873e6..d2cb788ea 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -20,12 +20,12 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a (** Instance declaration *) -val existing_instance : bool -> reference -> int option -> unit -(** globality, reference, priority *) +val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit +(** globality, reference, optional priority and pattern information *) val declare_instance_constant : typeclass -> - int option -> (** priority *) + Vernacexpr.hint_info_expr -> (** priority *) bool -> (** globality *) Impargs.manual_explicitation list -> (** implicits *) ?hook:(Globnames.global_reference -> unit) -> @@ -48,7 +48,7 @@ val new_instance : ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(Globnames.global_reference -> unit) -> - int option -> + Vernacexpr.hint_info_expr -> Id.t (** Setting opacity *) diff --git a/toplevel/record.ml b/toplevel/record.ml index ba9e7ee22..ef09f6fa5 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -561,8 +561,9 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in let gr = match kind with - | Class def -> - let gr = declare_class finite def poly ctx (loc,idstruc) idbuild + | Class def -> + let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in + let gr = declare_class finite def poly ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> diff --git a/toplevel/record.mli b/toplevel/record.mli index b09425563..c50e57786 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -38,7 +38,8 @@ val declare_structure : inductive val definition_structure : - inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list * + inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * + plident with_coercion * local_binder list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 68485231b..230e62607 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -841,9 +841,9 @@ let vernac_instance abst locality poly sup inst props pri = let vernac_context poly l = if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom -let vernac_declare_instances locality ids pri = +let vernac_declare_instances locality insts = let glob = not (make_section_locality locality) in - List.iter (fun id -> Classes.existing_instance glob id pri) ids + List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts let vernac_declare_class id = Record.declare_existing_class (Nametab.global id) @@ -1996,10 +1996,10 @@ let interp ?proof ~loc locality poly c = vernac_identity_coercion locality poly local id s t (* Type classes *) - | VernacInstance (abst, sup, inst, props, pri) -> - vernac_instance abst locality poly sup inst props pri + | VernacInstance (abst, sup, inst, props, info) -> + vernac_instance abst locality poly sup inst props info | VernacContext sup -> vernac_context poly sup - | VernacDeclareInstances (ids, pri) -> vernac_declare_instances locality ids pri + | VernacDeclareInstances insts -> vernac_declare_instances locality insts | VernacDeclareClass id -> vernac_declare_class id (* Solving *) |