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 +++++++++++++++++++++++++++++++++++++++++++--- doc/refman/RefMan-tac.tex | 2 +- tactics/tactics.ml | 2 +- 3 files changed, 139 insertions(+), 9 deletions(-) diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index e8ebb9f99..e90621f04 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} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index dd45feebc..c659e19e6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3907,7 +3907,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/tactics/tactics.ml b/tactics/tactics.ml index d2e5d8525..88e84f418 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"]; -- cgit v1.2.3