From e807f3407fb19f481dac332e7650eddfa9b5fd5d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 14 Oct 2016 16:53:19 +0200 Subject: Documenting changes in typeclasses --- doc/refman/Classes.tex | 144 ++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 137 insertions(+), 7 deletions(-) (limited to 'doc/refman/Classes.tex') diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index e8ebb9f995..e90621f046 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,55 @@ 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{typeclasseseauto} + +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. 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. Other subgoals are + automatically shelved and \emph{must be} resolved entirely when the + other typeclass subgoals are resolved. +\item The transparency information of databases is used consistently. + 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 does + not treat typeclass subgoals differently than others. +\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 typeclasse +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,18 +445,103 @@ 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 Module Eta} +\optindex{Typeclasses Modulo Eta} + +This allows eta-conversion during unification of type-classes. + +\subsection{\tt Set Typeclasses Dependency Order} +\optindex{Typeclasses Dependency Order} + +This option (now on by default) 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 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 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 eta-expansions in the proof term +generated. It does so by allowing hints that conclude in an product to +apply to a goal with a matching product directly, avoiding an +introduction. \emph{Warning:} 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 more expensive +proof-search (i.e. more useless backtracking). + +\subsection{\tt Set Typeclasses Filtered Unification} +\optindex{Typeclasses Filtered Unification} + +This option, available since Coq 8.6, switches the hint application +procedure to a filter-then-unify strategy. To apply a hint, we first +check that it \emph{matches} syntactically the inferred 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 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 Refine Instance Mode} -- cgit v1.2.3 From 6ec511721efc9235f6c2fa922a21dcb9b041bbfd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 3 Nov 2016 15:51:39 +0100 Subject: Document options of typeclasses (eauto) With update after J. Gross comments --- doc/refman/Classes.tex | 85 +++++++++++++++++++++++++++++++------------------- 1 file changed, 53 insertions(+), 32 deletions(-) (limited to 'doc/refman/Classes.tex') diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index e90621f046..144fc22b96 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -387,14 +387,16 @@ than {\tt eauto} and {\tt auto}. The main differences are the following: \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. It analyses the dependencies between subgoals to avoid + 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. Other subgoals are automatically shelved and \emph{must be} resolved entirely when the - other typeclass subgoals are resolved. -\item The transparency information of databases is used consistently. + other typeclass subgoals are resolved or the proof search will fail. +\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 @@ -412,8 +414,9 @@ than {\tt eauto} and {\tt auto}. The main differences are the following: 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 does - not treat typeclass subgoals differently than others. + 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}} @@ -421,7 +424,7 @@ than {\tt eauto} and {\tt auto}. The main differences are the following: 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 typeclasse +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 @@ -445,50 +448,59 @@ 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 Module Eta} -\optindex{Typeclasses Modulo Eta} - -This allows eta-conversion during unification of type-classes. - \subsection{\tt Set Typeclasses Dependency Order} \optindex{Typeclasses Dependency Order} -This option (now on by default) respects the dependency order between +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 eta-expansions in the proof term -generated. It does so by allowing hints that conclude in an product to +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:} 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 more expensive -proof-search (i.e. more useless backtracking). - -\subsection{\tt Set Typeclasses Filtered Unification} -\optindex{Typeclasses Filtered Unification} - -This option, available since Coq 8.6, switches the hint application -procedure to a filter-then-unify strategy. To apply a hint, we first -check that it \emph{matches} syntactically the inferred 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. +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} @@ -544,6 +556,15 @@ The semantics of the options are: \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} -- cgit v1.2.3 From d6fe6773c959493ed97108e1032b1bd8c1e78081 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 24 Oct 2016 18:18:33 +0200 Subject: Lets Hints/Instances take an optional pattern In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well. --- doc/refman/Classes.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/refman/Classes.tex') diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 144fc22b96..254fca28f7 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -379,7 +379,7 @@ Declares variables according to the given binding context, which might use implicit generalization (see \ref{SectionContext}). \asubsection{\tt typeclasses eauto} -\tacindex{typeclasseseauto} +\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: -- cgit v1.2.3 From 98305374e2fdec4b64d7d086ddca0c4e812b178e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 29 Oct 2016 11:51:38 +0200 Subject: typeclasses eauto Implem/doc of shelving strategy Now [typeclasses eauto] mimicks what happens during resolution faithfully, and the shelving behavior/requirements for a successful proof-search are documented. --- doc/refman/Classes.tex | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'doc/refman/Classes.tex') diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 254fca28f7..d6a553e1a8 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -394,7 +394,18 @@ than {\tt eauto} and {\tt auto}. The main differences are the following: {\tt typeclass\_instances} database by default (instead of {\tt core}) and will try to solve \emph{only} typeclass goals. Other subgoals are automatically shelved and \emph{must be} resolved entirely when the - other typeclass subgoals are resolved or the proof search will fail. + 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 -- cgit v1.2.3 From f6916774eea2ecc1262377cb14c2d494a0486358 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 29 Oct 2016 19:07:21 +0200 Subject: Do not shelve non-class subgoals but fail, it should be the instance writer's responsibility to not generated non-dependent non-class subgoals (otherwise we loose compatibility as shown in e.g. MathClasses, which goes into loops because of unexpectedly unconstrained goals). Reflect it in the doc. --- doc/refman/Classes.tex | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'doc/refman/Classes.tex') diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index d6a553e1a8..58ae7191f8 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -392,11 +392,13 @@ than {\tt eauto} and {\tt auto}. The main differences are the following: 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. Other 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. + 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 -- cgit v1.2.3 From 4b8f19c58a2b6cc841db2c011d23aa8106211fd6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 15 Nov 2016 13:53:57 +0100 Subject: Revert part of a477dc, disallow_shelved In only_classes mode we do not try to implement a stricter semantics for shelved goals in 8.6. Leaving this for 8.7. Update the documentation as well. Remove a spurious printf call as well. Fix test-suite now that shelved goals are allowed --- doc/refman/Classes.tex | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'doc/refman/Classes.tex') diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 58ae7191f8..7c4bd4d201 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -392,13 +392,12 @@ than {\tt eauto} and {\tt auto}. The main differences are the following: 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. + and will try to solve \emph{only} typeclass goals, shelving the other + goals. If some subgoal of a hint/instance is non-dependent and not of + class type, the hint application will fail when faced with that + subgoal. Dependent subgoals are automatically shelved, and shelved + goals can remain after resolution ends (following the behavior of + \Coq{} 8.5). \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)} faithfully mimicks what happens during typeclass resolution when it is -- cgit v1.2.3 From 09fd1e8b5e810bae0e50ecd4901cd7c8f1464f4a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 16 Nov 2016 10:45:25 +0100 Subject: Revert more of a477dc for good measure We stop failing automatically on non-declared-class nested or toplevel subgoals as in 8.5, instead of the previous a477dc behavior of shelving those goals and failing if shelved goals remained at the end of resolution. It means typeclass resolution during refinement is closer to all:typeclasses eauto. Hints in typeclass_instances for non-declared classes can be used during resolution of _nested_ subgoals when it is fired from type-inference, toplevel goals considered in this case are still only classes (as in 8.5 and before). The code that triggers the restriction to only declared class subgoals is commented. Revert changes to test-suite, adding test for #5203, #5198 is fixed too. Add corresponding tests in the test-suite (that will break if we, e.g. disallow non-class subgoals) and update the refman accordingly. --- doc/refman/Classes.tex | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'doc/refman/Classes.tex') diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 7c4bd4d201..bd8ee450ef 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -391,19 +391,19 @@ than {\tt eauto} and {\tt auto}. The main differences are the following: 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, shelving the other - goals. If some subgoal of a hint/instance is non-dependent and not of - class type, the hint application will fail when faced with that - subgoal. Dependent subgoals are automatically shelved, and shelved + {\tt typeclass\_instances} database by default (instead of {\tt + core}). + Dependent subgoals are automatically shelved, and shelved goals can remain after resolution ends (following the behavior of \Coq{} 8.5). \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. + called during refinement/type-inference, except that \emph{only} + declared class subgoals are considered at the start of resolution + during type inference, while ``all'' can select non-class subgoals as + well. 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. -- cgit v1.2.3