diff options
74 files changed, 1145 insertions, 899 deletions
diff --git a/.gitattributes b/.gitattributes index db179c8d2..e087e1737 100644 --- a/.gitattributes +++ b/.gitattributes @@ -19,6 +19,7 @@ tools/CoqMakefile.in whitespace=trailing-space *.css whitespace=trailing-space,tab-in-indent *.dtd whitespace=trailing-space,tab-in-indent *.el whitespace=trailing-space,tab-in-indent +*.g whitespace=trailing-space,tab-in-indent *.h whitespace=trailing-space,tab-in-indent *.html whitespace=trailing-space,tab-in-indent *.hva whitespace=trailing-space,tab-in-indent @@ -37,9 +38,11 @@ tools/CoqMakefile.in whitespace=trailing-space *.nsh whitespace=trailing-space,tab-in-indent *.nsi whitespace=trailing-space,tab-in-indent *.py whitespace=trailing-space,tab-in-indent +*.rst whitespace=trailing-space,tab-in-indent *.sh whitespace=trailing-space,tab-in-indent *.sty whitespace=trailing-space,tab-in-indent *.tex whitespace=trailing-space,tab-in-indent +*.tokens whitespace=trailing-space,tab-in-indent *.txt whitespace=trailing-space,tab-in-indent *.v whitespace=trailing-space,tab-in-indent *.xml whitespace=trailing-space,tab-in-indent diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index fea50c58c..f344c5cf5 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -37,6 +37,10 @@ /dev/doc/ @Zimmi48 # Secondary maintainer @maximedenes +/dev/doc/changes.md @ghost +# Trick to avoid getting review requests +# each time someone modifies the dev changelog + /doc/ @maximedenes # Secondary maintainer @silene @@ -104,8 +108,8 @@ /plugins/btauto/ @ppedrot # Secondary maintainer @herbelin -# I don't know Pierre Corbineau's GitHub nickname -/plugins/cc/ @herbelin +/plugins/cc/ @PierreCorbineau +# Secondary maintainer @herbelin /plugins/derive/ @aspiwack # Secondary maintainer @ppedrot @@ -113,8 +117,8 @@ /plugins/extraction/ @letouzey # Secondary maintainer @maximedenes -# I don't know Pierre Corbineau's GitHub nickname -/plugins/firstorder/ @herbelin +/plugins/firstorder/ @PierreCorbineau +# Secondary maintainer @herbelin /plugins/fourier/ @herbelin # Secondary maintainer @gares @@ -149,8 +153,8 @@ /plugins/quote/ @herbelin -# Should be Pierre Corbineau too -/plugins/rtauto/ @herbelin +/plugins/rtauto/ @PierreCorbineau +# Secondary maintainer @herbelin ########## Pretyper ########## @@ -294,6 +298,9 @@ /META.coq @ejgallego # Secondary maintainer @letouzey +/dev/build/windows @MSoegtropIMC +# Secondary maintainer @maximedenes + ########## Developer tools ########## diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 03e001f4a..f0d7463fc 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -85,10 +85,6 @@ before_script: - echo 'end:coq.install' - set +e - variables: &build-variables - EXTRA_CONF: "-native-compiler yes -coqide opt" - EXTRA_PACKAGES: "$COQIDE_PACKAGES" - EXTRA_OPAM: "$COQIDE_OPAM" .warnings-template: &warnings-template # keep warnings in test stage so we can test things even when warnings occur @@ -151,9 +147,9 @@ before_script: build: <<: *build-template variables: - EXTRA_CONF: "-with-doc yes" - EXTRA_PACKAGES: "$COQDOC_PACKAGES" - EXTRA_OPAM: "$COQDOC_OPAM" + EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" + EXTRA_PACKAGES: "$COQIDE_PACKAGES $COQDOC_PACKAGES" + EXTRA_OPAM: "$COQIDE_OPAM $COQDOC_OPAM" PIP_PACKAGES: "$SPHINX_PACKAGES" # no coqide for 32bit: libgtk installation problems @@ -167,9 +163,10 @@ build:32bit: build:bleeding-edge: <<: *build-template variables: - <<: *build-variables + EXTRA_CONF: "-native-compiler yes -coqide opt" COMPILER: "$COMPILER_BLEEDING_EDGE" CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" + EXTRA_PACKAGES: "$COQIDE_PACKAGES" EXTRA_OPAM: "$COQIDE_OPAM_BE" warnings: @@ -6,6 +6,15 @@ Tools - Coq_makefile lets one override or extend the following variables from the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS. +Vernacular Commands + +- Removed deprecated commands Arguments Scope and Implicit Arguments + (not the option). Use the Arguments command instead. + +Tactic language + +- Support for fix/cofix added in Ltac "match" and "lazymatch". + Changes from 8.7.2 to 8.8+beta1 =============================== diff --git a/Makefile.doc b/Makefile.doc index 4a247f1d9..2d2b21ad8 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -62,7 +62,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-pro.v.tex \ Coercion.v.tex Extraction.v.tex \ Program.v.tex Polynom.v.tex Nsatz.v.tex \ - Setoid.v.tex Classes.v.tex Universes.v.tex \ + Setoid.v.tex Universes.v.tex \ Misc.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ diff --git a/clib/cArray.ml b/clib/cArray.ml index b6c033f6d..5eb20bc16 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -41,6 +41,8 @@ sig ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a + val fold_left4 : + ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'e array -> 'a val fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a @@ -267,6 +269,16 @@ let fold_left3 f a v1 v2 v3 = invalid_arg "Array.fold_left2"; fold a 0 +let fold_left4 f a v1 v2 v3 v4 = + let lv1 = Array.length v1 in + let rec fold a n = + if n >= lv1 then a + else fold (f a (uget v1 n) (uget v2 n) (uget v3 n) (uget v4 n)) (succ n) + in + if Array.length v2 <> lv1 || Array.length v3 <> lv1 || Array.length v4 <> lv1 then + invalid_arg "Array.fold_left4"; + fold a 0 + let fold_left_from n f a v = let len = Array.length v in let () = if n < 0 then invalid_arg "Array.fold_left_from" in diff --git a/clib/cArray.mli b/clib/cArray.mli index 97038b0ac..f4f60f8aa 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -66,6 +66,8 @@ sig ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a + val fold_left4 : + ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'e array -> 'a val fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 4e8c7e145..4f7e9517f 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -11,25 +11,6 @@ wget -qO- ${sf_vfa_CI_TARURL} | tar xvz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v -# Delete useless calls to try omega; unfold -patch vfa/SearchTree.v <<EOF -*** SearchTree.v.bak 2017-09-06 19:12:59.000000000 +0200 ---- SearchTree.v 2017-11-21 16:34:41.000000000 +0100 -*************** -*** 674,683 **** - forall i j : key, ~ (i > j) -> ~ (i < j) -> i=j. - Proof. - intros. -- try omega. (* Oops! [omega] cannot solve this one. -- The problem is that [i] and [j] have type [key] instead of type [nat]. -- The solution is easy enough: *) -- unfold key in *. - omega. - - (** So, if you get stuck on an [omega] that ought to work, ---- 674,679 ---- -EOF - ( cd lf && make clean && make ) ( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index ee9c8777a..cd09b6d30 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -31,4 +31,6 @@ fi find . "(" -path ./.git -prune ")" -o -type f -print0 | xargs -0 dev/tools/check-eof-newline.sh || CODE=1 +dev/tools/check-overlays.sh || CODE=1 + exit $CODE diff --git a/dev/tools/check-overlays.sh b/dev/tools/check-overlays.sh new file mode 100755 index 000000000..f7e05b51c --- /dev/null +++ b/dev/tools/check-overlays.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +for f in dev/ci/user-overlays/* +do + if ! ([[ $f = dev/ci/user-overlays/README.md ]] || [[ $f == *.sh ]]) + then + >&2 echo "Bad overlay '$f'." + >&2 echo "User overlays need to have extension .sh to be picked up!" + exit 1 + fi +done diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index c9cdee84a..a514b8866 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -5,6 +5,8 @@ set -e +dev/tools/check-overlays.sh + if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh || ! git diff-index --check --cached HEAD >/dev/null 2>&1 ; then diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex deleted file mode 100644 index da798a238..000000000 --- a/doc/refman/Classes.tex +++ /dev/null @@ -1,578 +0,0 @@ -\def\Haskell{\textsc{Haskell}\xspace} -\def\eol{\setlength\parskip{0pt}\par} -\def\indent#1{\noindent\kern#1} -\def\cst#1{\textsf{#1}} - -\newcommand\tele[1]{\overrightarrow{#1}} - -\achapter{\protect{Type Classes}} -%HEVEA\cutname{type-classes.html} -\aauthor{Matthieu Sozeau} -\label{typeclasses} - -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 -classes in \Haskell which also applies. - -\asection{Class and Instance declarations} -\label{ClassesInstances} - -The syntax for class and instance declarations is the same as -record syntax of \Coq: -\def\kw{\texttt} -\def\classid{\texttt} - -\begin{center} -\[\begin{array}{l} -\kw{Class}~\classid{Id}~(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n) -[: \sort] := \{\\ -\begin{array}{p{0em}lcl} - & \cst{f}_1 & : & \type_1 ; \\ - & \vdots & & \\ - & \cst{f}_m & : & \type_m \}. -\end{array}\end{array}\] -\end{center} -\begin{center} -\[\begin{array}{l} -\kw{Instance}~\ident~:~\classid{Id}~\term_1 \cdots \term_n := \{\\ -\begin{array}{p{0em}lcl} - & \cst{f}_1 & := & \term_{f_1} ; \\ - & \vdots & & \\ - & \cst{f}_m & := & \term_{f_m} \}. -\end{array}\end{array}\] -\end{center} -\begin{coq_eval} - Reset Initial. - Generalizable All Variables. -\end{coq_eval} - -The $\tele{\alpha_i : \tau_i}$ variables are called the \emph{parameters} -of the class and the $\tele{f_k : \type_k}$ are called the -\emph{methods}. Each class definition gives rise to a corresponding -record declaration and each instance is a regular definition whose name -is given by $\ident$ and type is an instantiation of the record type. - -We'll use the following example class in the rest of the chapter: - -\begin{coq_example*} -Class EqDec (A : Type) := { - eqb : A -> A -> bool ; - eqb_leibniz : forall x y, eqb x y = true -> x = y }. -\end{coq_example*} - -This class implements a boolean equality test which is compatible with -Leibniz equality on some type. An example implementation is: - -\begin{coq_example*} -Instance unit_EqDec : EqDec unit := -{ eqb x y := true ; - eqb_leibniz x y H := - match x, y return x = y with tt, tt => eq_refl tt end }. -\end{coq_example*} - -If one does not give all the members in the \texttt{Instance} -declaration, Coq enters the proof-mode and the user is asked to build -inhabitants of the remaining fields, e.g.: - -\begin{coq_example*} -Instance eq_bool : EqDec bool := -{ eqb x y := if x then y else negb y }. -\end{coq_example*} -\begin{coq_example} -Proof. intros x y H. - destruct x ; destruct y ; (discriminate || reflexivity). -Defined. -\end{coq_example} - -One has to take care that the transparency of every field is determined -by the transparency of the \texttt{Instance} proof. One can use -alternatively the \texttt{Program} \texttt{Instance} \comindex{Program Instance} variant which has -richer facilities for dealing with obligations. - -\asection{Binding classes} - -Once a type class is declared, one can use it in class binders: -\begin{coq_example} -Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y). -\end{coq_example} - -When one calls a class method, a constraint is generated that is -satisfied only in contexts where the appropriate instances can be -found. In the example above, a constraint \texttt{EqDec A} is generated and -satisfied by \texttt{{eqa : EqDec A}}. In case no satisfying constraint can be -found, an error is raised: - -\begin{coq_example} -Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y). -\end{coq_example} - -The algorithm used to solve constraints is a variant of the eauto tactic -that does proof search with a set of lemmas (the instances). It will use -local hypotheses as well as declared lemmas in the -\texttt{typeclass\_instances} database. Hence the example can also be -written: - -\begin{coq_example} -Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y). -\end{coq_example} - -However, the generalizing binders should be used instead as they have -particular support for type classes: -\begin{itemize} -\item They automatically set the maximally implicit status for type - class arguments, making derived functions as easy to use as class - methods. In the example above, \texttt{A} and \texttt{eqa} should be - set maximally implicit. -\item They support implicit quantification on partially applied type - classes (\S \ref{implicit-generalization}). - Any argument not given as part of a type class binder will be - automatically generalized. -\item They also support implicit quantification on superclasses - (\S \ref{classes:superclasses}) -\end{itemize} - -Following the previous example, one can write: -\begin{coq_example} -Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y). -\end{coq_example} - -Here \texttt{A} is implicitly generalized, and the resulting function -is equivalent to the one above. - -\asection{Parameterized Instances} - -One can declare parameterized instances as in \Haskell simply by giving -the constraints as a binding context before the instance, e.g.: - -\begin{coq_example} -Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := -{ eqb x y := match x, y with - | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) - end }. -\end{coq_example} -\begin{coq_eval} -Admitted. -\end{coq_eval} - -These instances are used just as well as lemmas in the instance hint database. - -\asection{Sections and contexts} -\label{SectionContext} -To ease the parametrization of developments by type classes, we provide -a new way to introduce variables into section contexts, compatible with -the implicit argument mechanism. -The new command works similarly to the \texttt{Variables} vernacular -(see \ref{Variable}), except it accepts any binding context as argument. -For example: - -\begin{coq_example} -Section EqDec_defs. - Context `{EA : EqDec A}. -\end{coq_example} - -\begin{coq_example*} - Global Instance option_eqb : EqDec (option A) := - { eqb x y := match x, y with - | Some x, Some y => eqb x y - | None, None => true - | _, _ => false - end }. -\end{coq_example*} -\begin{coq_eval} -Proof. -intros x y ; destruct x ; destruct y ; intros H ; -try discriminate ; try apply eqb_leibniz in H ; -subst ; auto. -Defined. -\end{coq_eval} - -\begin{coq_example} -End EqDec_defs. -About option_eqb. -\end{coq_example} - -Here the \texttt{Global} modifier redeclares the instance at the end of -the section, once it has been generalized by the context variables it uses. - -\asection{Building hierarchies} - -\subsection{Superclasses} -\label{classes:superclasses} -One can also parameterize classes by other classes, generating a -hierarchy of classes and superclasses. In the same way, we give the -superclasses as a binding context: - -\begin{coq_example*} -Class Ord `(E : EqDec A) := - { le : A -> A -> bool }. -\end{coq_example*} - -Contrary to \Haskell, we have no special syntax for superclasses, but -this declaration is morally equivalent to: -\begin{verbatim} -Class `(E : EqDec A) => Ord A := - { le : A -> A -> bool }. -\end{verbatim} - -This declaration means that any instance of the \texttt{Ord} class must -have an instance of \texttt{EqDec}. The parameters of the subclass contain -at least all the parameters of its superclasses in their order of -appearance (here \texttt{A} is the only one). -As we have seen, \texttt{Ord} is encoded as a record type with two parameters: -a type \texttt{A} and an \texttt{E} of type \texttt{EqDec A}. However, one can -still use it as if it had a single parameter inside generalizing binders: the -generalization of superclasses will be done automatically. -\begin{coq_example*} -Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x). -\end{coq_example*} - -In some cases, to be able to specify sharing of structures, one may want to give -explicitly the superclasses. It is is possible to do it directly in regular -binders, and using the \texttt{!} modifier in class binders. For -example: -\begin{coq_example*} -Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := - andb (le x y) (neqb x y). -\end{coq_example*} - -The \texttt{!} modifier switches the way a binder is parsed back to the -regular interpretation of Coq. In particular, it uses the implicit -arguments mechanism if available, as shown in the example. - -\subsection{Substructures} - -Substructures are components of a class which are instances of a class -themselves. They often arise when using classes for logical properties, -e.g.: - -\begin{coq_eval} -Require Import Relations. -\end{coq_eval} -\begin{coq_example*} -Class Reflexive (A : Type) (R : relation A) := - reflexivity : forall x, R x x. -Class Transitive (A : Type) (R : relation A) := - transitivity : forall x y z, R x y -> R y z -> R x z. -\end{coq_example*} - -This declares singleton classes for reflexive and transitive relations, -(see \ref{SingletonClass} for an explanation). -These may be used as part of other classes: - -\begin{coq_example*} -Class PreOrder (A : Type) (R : relation A) := -{ PreOrder_Reflexive :> Reflexive A R ; - PreOrder_Transitive :> Transitive A R }. -\end{coq_example*} - -The syntax \texttt{:>} indicates that each \texttt{PreOrder} can be seen -as a \texttt{Reflexive} relation. So each time a reflexive relation is -needed, a preorder can be used instead. This is very similar to the -coercion mechanism of \texttt{Structure} declarations. -The implementation simply declares each projection as an instance. - -One can also declare existing objects or structure -projections using the \texttt{Existing Instance} command to achieve the -same effect. - -\section{Summary of the commands -\label{TypeClassCommands}} - -\subsection{\tt Class {\ident} {\binder$_1$ \ldots~\binder$_n$} - : \sort := \{ field$_1$ ; \ldots ; field$_k$ \}.} -\comindex{Class} -\label{Class} - -The \texttt{Class} command is used to declare a type class with -parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to -{\tt field$_k$}. - -\begin{Variants} -\item \label{SingletonClass} {\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$} - : \sort := \ident$_1$ : \type$_1$.} - This variant declares a \emph{singleton} class whose only method is - {\tt \ident$_1$}. This singleton class is a so-called definitional - class, represented simply as a definition - {\tt {\ident} \binder$_1$ \ldots \binder$_n$ := \type$_1$} and whose - instances are themselves objects of this type. Definitional classes - are not wrapped inside records, and the trivial projection of an - instance of such a class is convertible to the instance itself. This can - be useful to make instances of existing objects easily and to reduce - proof size by not inserting useless projections. The class - constant itself is declared rigid during resolution so that the class - abstraction is maintained. - -\item \label{ExistingClass} {\tt Existing Class {\ident}.\comindex{Existing Class}} - This variant declares a class a posteriori from a constant or - inductive definition. No methods or instances are defined. -\end{Variants} - -\subsection{\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} : - {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}] - := \{ field$_1$ := b$_1$ ; \ldots ; field$_i$ := b$_i$ \}} -\comindex{Instance} -\label{Instance} - -The \texttt{Instance} command is used to declare a type class instance -named {\ident} of the class \emph{Class} with parameters {t$_1$} to {t$_n$} and -fields {\tt b$_1$} to {\tt b$_i$}, where each field must be a declared -field of the class. Missing fields must be filled in interactive proof mode. - -An arbitrary context of the form {\tt \binder$_1$ \ldots \binder$_n$} -can be put after the name of the instance and before the colon to -declare a parameterized instance. -An optional \textit{priority} can be declared, 0 being the highest -priority as for auto hints. If the priority is not specified, it defaults to -$n$, the number of binders of the instance. - -\begin{Variants} -\item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} : - forall {\binder$_{n+1}$ \ldots \binder$_m$}, - {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}] := \term} - This syntax is used for declaration of singleton class instances or - for directly giving an explicit term of type - {\tt forall {\binder$_{n+1}$ \ldots \binder$_m$}, {Class} {t$_1$ \ldots t$_n$}}. - One need not even mention the unique field name for singleton classes. - -\item {\tt Global Instance} One can use the \texttt{Global} modifier on - instances declared in a section so that their generalization is automatically - redeclared after the section is closed. - -\item {\tt Program Instance} \comindex{Program Instance} - Switches the type-checking to \Program~(chapter \ref{Program}) - and uses the obligation mechanism to manage missing fields. - -\item {\tt Declare Instance} \comindex{Declare Instance} - In a {\tt Module Type}, this command states that a corresponding - concrete instance should exist in any implementation of this - {\tt Module Type}. This is similar to the distinction between - {\tt Parameter} vs. {\tt Definition}, or between {\tt Declare Module} - and {\tt Module}. - -\end{Variants} - -Besides the {\tt Class} and {\tt Instance} vernacular commands, there -are a few other commands related to type classes. - -\subsection{\tt Existing Instance {\ident} [| \textit{priority}]} -\comindex{Existing Instance} -\label{ExistingInstance} - -This commands adds an arbitrary constant whose type ends with an applied -type class to the instance database with an optional priority. It can be used -for redeclaring instances at the end of sections, or declaring structure -projections as instances. This is almost equivalent to {\tt Hint Resolve -{\ident} : typeclass\_instances}. - -\begin{Variants} -\item {\tt Existing Instances {\ident}$_1$ \ldots {\ident}$_n$ - [| \textit{priority}]} - \comindex{Existing Instances} - With this command, several existing instances can be declared at once. -\end{Variants} - -\subsection{\tt Context {\binder$_1$ \ldots \binder$_n$}} -\comindex{Context} -\label{Context} - -Declares variables according to the given binding context, which might -use implicit generalization (see \ref{SectionContext}). - -\asubsection{\tt typeclasses eauto} -\tacindex{typeclasses eauto} -\label{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. {\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}). - 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, 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. -\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} -\label{TypeclassesTransparency} - -This commands defines the transparency of {\ident$_1$ \ldots \ident$_n$} -during type class resolution. It is useful when some constants prevent some -unifications and make resolution fail. It is also useful to declare -constants which should never be unfolded during proof-search, like -fixpoints or anything which does not look like an abbreviation. This can -additionally speed up proof search as the typeclass map can be indexed -by such rigid constants (see \ref{HintTransparency}). -By default, all constants and local variables are considered transparent. -One should take care not to make opaque any constant that is used to -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 Axioms Are Instances} -\optindex{Typeclasses Axioms Are Instances} - -This option (off by default since 8.8) automatically declares axioms -whose type is a typeclass at declaration time as instances of that -class. - -\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 Limit Intros} -\optindex{Typeclasses Limit Intros} - -This option (on by default) 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 For Conversion} -\optindex{Typeclass 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 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 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} - -The option {\tt Refine Instance Mode} allows to switch the behavior of instance -declarations made through the {\tt Instance} command. -\begin{itemize} -\item When it is on (the default), instances that have unsolved holes in their -proof-term silently open the proof mode with the remaining obligations to prove. -\item When it is off, they fail with an error instead. -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 86f123322..7ce28ccf8 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -118,7 +118,6 @@ Options A and B of the licence are {\em not} elected.} \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% \include{Coercion.v}% -\include{Classes.v}% \include{Extraction.v}% \include{Program.v}% \include{Polynom.v}% = Ring diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst new file mode 100644 index 000000000..becebb421 --- /dev/null +++ b/doc/sphinx/addendum/type-classes.rst @@ -0,0 +1,587 @@ +.. include:: ../replaces.rst + +.. _typeclasses: + +Type Classes +============ + +:Source: https://coq.inria.fr/distrib/current/refman/type-classes.html +:Author: Matthieu Sozeau + +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 +classes in Haskell which also applies. + + +Class and Instance declarations +------------------------------- + +The syntax for class and instance declarations is the same as the record +syntax of Coq: + +``Class Id (`` |p_1| ``:`` |t_1| ``) ⋯ (`` |p_n| ``:`` |t_n| ``) [: +sort] := {`` |f_1| ``:`` |u_1| ``; ⋮`` |f_m| ``:`` |u_m| ``}.`` + +``Instance ident : Id`` |p_1| ``⋯`` |p_n| ``:= {`` |f_1| ``:=`` |t_1| ``; ⋮`` |f_m| ``:=`` |t_m| ``}.`` + +The |p_i| ``:`` |t_i| variables are called the *parameters* of the class and +the |f_i| ``:`` |t_i| are called the *methods*. Each class definition gives +rise to a corresponding record declaration and each instance is a +regular definition whose name is given by ident and type is an +instantiation of the record type. + +We’ll use the following example class in the rest of the chapter: + +.. coqtop:: in + + Class EqDec (A : Type) := { + eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true -> x = y }. + +This class implements a boolean equality test which is compatible with +Leibniz equality on some type. An example implementation is: + +.. coqtop:: in + + Instance unit_EqDec : EqDec unit := + { eqb x y := true ; + eqb_leibniz x y H := + match x, y return x = y with tt, tt => eq_refl tt end }. + +If one does not give all the members in the Instance declaration, Coq +enters the proof-mode and the user is asked to build inhabitants of +the remaining fields, e.g.: + +.. coqtop:: in + + Instance eq_bool : EqDec bool := + { eqb x y := if x then y else negb y }. + +.. coqtop:: all + + Proof. intros x y H. + +.. coqtop:: all + + destruct x ; destruct y ; (discriminate || reflexivity). + +.. coqtop:: all + + Defined. + +One has to take care that the transparency of every field is +determined by the transparency of the ``Instance`` proof. One can use +alternatively the ``Program Instance`` variant which has richer facilities +for dealing with obligations. + + +Binding classes +--------------- + +Once a type class is declared, one can use it in class binders: + +.. coqtop:: all + + Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y). + +When one calls a class method, a constraint is generated that is +satisfied only in contexts where the appropriate instances can be +found. In the example above, a constraint ``EqDec A`` is generated and +satisfied by ``eqa : EqDec A``. In case no satisfying constraint can be +found, an error is raised: + +.. coqtop:: all + + Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y). + +The algorithm used to solve constraints is a variant of the eauto +tactic that does proof search with a set of lemmas (the instances). It +will use local hypotheses as well as declared lemmas in +the ``typeclass_instances`` database. Hence the example can also be +written: + +.. coqtop:: all + + Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y). + +However, the generalizing binders should be used instead as they have +particular support for type classes: + ++ They automatically set the maximally implicit status for type class + arguments, making derived functions as easy to use as class methods. + In the example above, ``A`` and ``eqa`` should be set maximally implicit. ++ They support implicit quantification on partially applied type + classes (:ref:`implicit-generalization`). Any argument not given as part of a type class + binder will be automatically generalized. ++ They also support implicit quantification on :ref:`superclasses`. + + +Following the previous example, one can write: + +.. coqtop:: all + + Generalizable Variables A B C. + + Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y). + +Here ``A`` is implicitly generalized, and the resulting function is +equivalent to the one above. + +Parameterized Instances +----------------------- + +One can declare parameterized instances as in Haskell simply by giving +the constraints as a binding context before the instance, e.g.: + +.. coqtop:: in + + Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := + { eqb x y := match x, y with + | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) + end }. + +.. coqtop:: none + + Abort. + +These instances are used just as well as lemmas in the instance hint +database. + +Sections and contexts +--------------------- + +To ease the parametrization of developments by type classes, we +provide a new way to introduce variables into section contexts, +compatible with the implicit argument mechanism. The new command works +similarly to the ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it +accepts any binding context as argument. For example: + +.. coqtop:: all + + Section EqDec_defs. + + Context `{EA : EqDec A}. + + Global Instance option_eqb : EqDec (option A) := + { eqb x y := match x, y with + | Some x, Some y => eqb x y + | None, None => true + | _, _ => false + end }. + Admitted. + + End EqDec_defs. + + About option_eqb. + +Here the Global modifier redeclares the instance at the end of the +section, once it has been generalized by the context variables it +uses. + + +Building hierarchies +-------------------- + +.. _superclasses: + +Superclasses +~~~~~~~~~~~~ + +One can also parameterize classes by other classes, generating a +hierarchy of classes and superclasses. In the same way, we give the +superclasses as a binding context: + +.. coqtop:: all + + Class Ord `(E : EqDec A) := { le : A -> A -> bool }. + +Contrary to Haskell, we have no special syntax for superclasses, but +this declaration is morally equivalent to: + +:: + + Class `(E : EqDec A) => Ord A := + { le : A -> A -> bool }. + + +This declaration means that any instance of the ``Ord`` class must have +an instance of ``EqDec``. The parameters of the subclass contain at +least all the parameters of its superclasses in their order of +appearance (here A is the only one). As we have seen, ``Ord`` is encoded +as a record type with two parameters: a type ``A`` and an ``E`` of type +``EqDec A``. However, one can still use it as if it had a single +parameter inside generalizing binders: the generalization of +superclasses will be done automatically. + +.. coqtop:: all + + Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x). + +In some cases, to be able to specify sharing of structures, one may +want to give explicitly the superclasses. It is is possible to do it +directly in regular binders, and using the ``!`` modifier in class +binders. For example: + +.. coqtop:: all + + Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). + +The ``!`` modifier switches the way a binder is parsed back to the regular +interpretation of Coq. In particular, it uses the implicit arguments +mechanism if available, as shown in the example. + +Substructures +~~~~~~~~~~~~~ + +Substructures are components of a class which are instances of a class +themselves. They often arise when using classes for logical +properties, e.g.: + +.. coqtop:: none + + Require Import Relation_Definitions. + +.. coqtop:: in + + Class Reflexive (A : Type) (R : relation A) := + reflexivity : forall x, R x x. + + Class Transitive (A : Type) (R : relation A) := + transitivity : forall x y z, R x y -> R y z -> R x z. + +This declares singleton classes for reflexive and transitive relations, +(see the :ref:`singleton class <singleton-class>` variant for an +explanation). These may be used as part of other classes: + +.. coqtop:: all + + Class PreOrder (A : Type) (R : relation A) := + { PreOrder_Reflexive :> Reflexive A R ; + PreOrder_Transitive :> Transitive A R }. + +The syntax ``:>`` indicates that each ``PreOrder`` can be seen as a +``Reflexive`` relation. So each time a reflexive relation is needed, a +preorder can be used instead. This is very similar to the coercion +mechanism of ``Structure`` declarations. The implementation simply +declares each projection as an instance. + +One can also declare existing objects or structure projections using +the Existing Instance command to achieve the same effect. + + +Summary of the commands +----------------------- + + +.. _Class: + +.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }. + + The ``Class`` command is used to declare a type class with parameters + ``binders`` and fields the declared record fields. + +Variants: + +.. _singleton-class: + +.. cmd:: Class @ident {? @binders} : {? @sort} := @ident : @term + + This variant declares a *singleton* class with a single method. This + singleton class is a so-called definitional class, represented simply + as a definition ``ident binders := term`` and whose instances are + themselves objects of this type. Definitional classes are not wrapped + inside records, and the trivial projection of an instance of such a + class is convertible to the instance itself. This can be useful to + make instances of existing objects easily and to reduce proof size by + not inserting useless projections. The class constant itself is + declared rigid during resolution so that the class abstraction is + maintained. + +.. cmd:: Existing Class @ident + + This variant declares a class a posteriori from a constant or + inductive definition. No methods or instances are defined. + +.. _Instance: + +.. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } + +The ``Instance`` command is used to declare a type class instance named +``ident`` of the class ``Class`` with parameters ``t1`` to ``tn`` and +fields ``b1`` to ``bi``, where each field must be a declared field of +the class. Missing fields must be filled in interactive proof mode. + +An arbitrary context of ``binders`` can be put after the name of the +instance and before the colon to declare a parameterized instance. An +optional priority can be declared, 0 being the highest priority as for +auto hints. If the priority is not specified, it defaults to the number +of non-dependent binders of the instance. + +Variants: + + +.. cmd:: Instance ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term + + This syntax is used for declaration of singleton class instances or + for directly giving an explicit term of type ``forall binders, Class + t1 … tn``. One need not even mention the unique field name for + singleton classes. + +.. cmd:: Global Instance + + One can use the ``Global`` modifier on instances declared in a + section so that their generalization is automatically redeclared + after the section is closed. + +.. cmd:: Program Instance + + Switches the type-checking to Program (chapter :ref:`program`) and + uses the obligation mechanism to manage missing fields. + +.. cmd:: Declare Instance + + In a Module Type, this command states that a corresponding concrete + instance should exist in any implementation of thisModule Type. This + is similar to the distinction betweenParameter vs. Definition, or + between Declare Module and Module. + + +Besides the ``Class`` and ``Instance`` vernacular commands, there are a +few other commands related to type classes. + +.. _ExistingInstance: + +Existing Instance +~~~~~~~~~~~~~~~~~ + +.. cmd:: Existing Instance {+ @ident} [| priority] + +This commands adds an arbitrary list of constants whose type ends with +an applied type class to the instance database with an optional +priority. It can be used for redeclaring instances at the end of +sections, or declaring structure projections as instances. This is +equivalent to ``Hint Resolve ident : typeclass_instances``, except it +registers instances for ``Print Instances``. + +.. _Context: + +Context +~~~~~~~ + +.. cmd:: Context @binders + +Declares variables according to the given binding context, which might +use :ref:`implicit-generalization`. + + +.. _typeclasses-eauto: + +``typeclasses eauto`` +~~~~~~~~~~~~~~~~~~~~~ + +The ``typeclasses eauto`` tactic uses a different resolution engine than +eauto and auto. The main differences are the following: + ++ Contrary to ``eauto`` and ``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. + typeclasses eauto is a multi-goal tactic. It analyses the dependencies + between subgoals to avoid backtracking on subgoals that are entirely + independent. + ++ When called with no arguments, typeclasses eauto uses + thetypeclass_instances database by default (instead of core). + Dependent subgoals are automatically shelved, and shelved goals can + remain after resolution ends (following the behavior ofCoq 8.5). + *Note: * As of Coq 8.6, all:once (typeclasses eauto) faithfully + mimicks what happens during typeclass resolution when it is called + during refinement/type-inference, except that *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 ``all:typeclasses eauto`` in future versions when the + refinement engine will be able to backtrack. + ++ When called with specific databases (e.g. with), typeclasses eauto + allows shelved goals to remain at any point during search and treat + typeclasses goals like any other. + ++ 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 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. + + +Variants: + +#. ``typeclasses eauto [num]`` + + *Warning:* The semantics for the limit num + is different than for auto. By default, if no limit is given the + search is unbounded. Contrary to auto, introduction steps (intro) are + counted, which might result in larger limits being necessary when + searching with typeclasses eauto than auto. + +#. ``typeclasses eauto with {+ @ident}`` + + 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). + +.. _autoapply: + +``autoapply term with ident`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The tactic autoapply applies a term using the transparency information +of the hint database ident, and does *no* typeclass resolution. This can +be used in ``Hint Extern``’s for typeclass instances (in the hint +database ``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. + +.. _TypeclassesTransparent: + +Typeclasses Transparent, Typclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Typeclasses { Transparent | Opaque } {+ @ident} + + This commands defines the transparency of the given identifiers + during type class resolution. It is useful when some constants + prevent some unifications and make resolution fail. It is also useful + to declare constants which should never be unfolded during + proof-search, like fixpoints or anything which does not look like an + abbreviation. This can additionally speed up proof search as the + typeclass map can be indexed by such rigid constants (see + :ref:`thehintsdatabasesforautoandeauto`). By default, all constants + and local variables are considered transparent. One should take care + not to make opaque any constant that is used to abbreviate a type, + like: + +:: + + relation A := A -> A -> Prop. + +This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. + + +Set 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. + + +Set 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 *matches* syntactically the +inferred or specified pattern of the hint, and only then try to +*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. + + +Set Typeclasses Limit Intros +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + +This option (on by default) 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. +*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). + + +Set Typeclass 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. + + +Set 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. + + +Set 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. + + +Set 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. + + +Typeclasses eauto `:=` +~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth + + This command allows more global customization of the type class + resolution tactic. The semantics of the options are: + + + ``debug`` In debug mode, the trace of successfully applied tactics is + printed. + + + ``dfs, bfs`` This sets the search strategy to depth-first search (the + default) or breadth-first search. + + + ``depth`` This sets the depth limit of the search. + + +Set Typeclasses Debug +~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Set Typeclasses Debug {? Verbosity @num} + +These options allow to see the resolution steps of typeclasses that are +performed during search. The ``Debug`` option is synonymous to ``Debug +Verbosity 1``, and ``Debug Verbosity 2`` provides more information +(tried tactics, shelving of goals, etc…). + + +Set Refine Instance Mode +~~~~~~~~~~~~~~~~~~~~~~~~ + +The option Refine Instance Mode allows to switch the behavior of +instance declarations made through the Instance command. + ++ When it is on (the default), instances that have unsolved holes in + their proof-term silently open the proof mode with the remaining + obligations to prove. + ++ When it is off, they fail with an error instead. diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index c5d4936b1..cf64aea03 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -45,6 +45,7 @@ Table of contents addendum/extended-pattern-matching addendum/canonical-structures + addendum/type-classes addendum/omega addendum/micromega diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index d618d90ad..68066faa3 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2109,6 +2109,8 @@ case, this latter type is considered). Adds blocks of implicit types with different specifications. +.. _implicit-generalization: + Implicit generalization ~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst index d4f6835ef..1b2e17221 100644 --- a/doc/sphinx/replaces.rst +++ b/doc/sphinx/replaces.rst @@ -64,6 +64,14 @@ .. |t_i| replace:: `t`\ :math:`_{i}` .. |t_m| replace:: `t`\ :math:`_{m}` .. |t_n| replace:: `t`\ :math:`_{n}` +.. |f_1| replace:: `f`\ :math:`_{1}` +.. |f_i| replace:: `f`\ :math:`_{i}` +.. |f_m| replace:: `f`\ :math:`_{m}` +.. |f_n| replace:: `f`\ :math:`_{n}` +.. |u_1| replace:: `u`\ :math:`_{1}` +.. |u_i| replace:: `u`\ :math:`_{i}` +.. |u_m| replace:: `u`\ :math:`_{m}` +.. |u_n| replace:: `u`\ :math:`_{n}` .. |term_0| replace:: `term`\ :math:`_{0}` .. |term_1| replace:: `term`\ :math:`_{1}` .. |term_2| replace:: `term`\ :math:`_{2}` diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 19444988b..48ddd9496 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -14,7 +14,6 @@ open CErrors open Util open Names open Nameops -open Constr open Termops open Libnames open Globnames @@ -1223,8 +1222,36 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat) - | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) - | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) + | PFix ((ln,i),(lna,tl,bl)) -> + let def_avoid, def_env, lfi = + Array.fold_left + (fun (avoid, env, l) na -> + let id = Namegen.next_name_away na avoid in + (Id.Set.add id avoid, Name id :: env, id::l)) + (avoid, env, []) lna in + let n = Array.length tl in + let v = Array.map3 + (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t)) + bl tl ln in + GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + | PCoFix (ln,(lna,tl,bl)) -> + let def_avoid, def_env, lfi = + Array.fold_left + (fun (avoid, env, l) na -> + let id = Namegen.next_name_away na avoid in + (Id.Set.add id avoid, Name id :: env, id::l)) + (avoid, env, []) lna in + let ntys = Array.length tl in + let v = Array.map2 + (fun c t -> share_pattern_names glob_of_pat 0 [] def_avoid def_env sigma c (Patternops.lift_pattern ntys t)) + bl tl in + GRec(GCoFix ln,Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) | PSort s -> GSort s let extern_constr_pattern env sigma pat = diff --git a/intf/pattern.ml b/intf/pattern.ml index af2347674..76367b612 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -10,7 +10,6 @@ open Names open Globnames -open Constr open Misctypes (** {5 Patterns} *) @@ -37,8 +36,8 @@ type constr_pattern = | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of case_info_pattern * constr_pattern * constr_pattern * (int * bool list * constr_pattern) list (** index of constructor, nb of args *) - | PFix of fixpoint - | PCoFix of cofixpoint + | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) + | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) (** Nota : in a [PCase], the array of branches might be shorter than expected, denoting the use of a final "_ => _" branch *) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index dc1110ad8..96b4a0e26 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -409,8 +409,6 @@ type nonrec vernac_expr = | VernacHints of string list * hints_expr | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag - | VernacDeclareImplicits of reference or_by_notation * - (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * vernac_argument_status list (* Main arguments status list *) * (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * @@ -418,8 +416,6 @@ type nonrec vernac_expr = [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list - | VernacArgumentsScope of reference or_by_notation * - scope_name option list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8543d2b84..7114e6c58 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -601,14 +601,6 @@ GEXTEND Gram ; END -let warn_deprecated_arguments_scope = - CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" - (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") - -let warn_deprecated_implicit_arguments = - CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" - (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") - (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext instance_name hint_info; @@ -691,20 +683,6 @@ GEXTEND Gram let more_implicits = Option.default [] more_implicits in VernacArguments (qid, args, more_implicits, !slash_position, mods) - - (* moved there so that camlp5 factors it with the previous rule *) - | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; - "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - warn_deprecated_arguments_scope ~loc:!@loc (); - VernacArgumentsScope (qid,scl) - - (* Implicit *) - | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; - pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> - List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - warn_deprecated_implicit_arguments ~loc:!@loc (); - VernacDeclareImplicits (qid,pos) - | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl @@ -734,12 +712,6 @@ GEXTEND Gram [`ClearImplicits; `ClearScopes] ] ] ; - implicit_name: - [ [ "!"; id = ident -> (id, false, true) - | id = ident -> (id,false,false) - | "["; "!"; id = ident; "]" -> (id,true,true) - | "["; id = ident; "]" -> (id,true, false) ] ] - ; scope: [ [ "%"; key = IDENT -> key ] ] ; diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 888c76e3d..89d490a41 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -183,9 +183,36 @@ let push_binder na1 na2 t ctx = Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in (na1, id2, t) :: ctx -let to_fix (idx, (nas, cs, ts)) = - let inj = EConstr.of_constr in - (idx, (nas, Array.map inj cs, Array.map inj ts)) +(* This is an optimization of the main pattern-matching which shares + the longest common prefix of the body and type of a fixpoint. The + only practical effect at the time of writing is in binding variable + names: these variable names must be bound only once since the user + view at a fix displays only a (maximal) shared common prefix *) + +let rec match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env' subst t1 t2 b1 b2 = + match t1, EConstr.kind sigma t2, b1, EConstr.kind sigma b2 with + | PProd(na1,c1,t1'), Prod(na2,c2,t2'), PLambda (_,c1',b1'), Lambda (na2',c2',b2') -> + let ctx = push_binder na1 na2 c2 ctx in + let ctx' = push_binder na1 na2' c2' ctx' in + let env = EConstr.push_rel (LocalAssum (na2,c2)) env in + let subst = sorec ctx env subst c1 c2 in + let subst = sorec ctx env subst c1' c2' in + let subst = add_binders na1 na2 binding_vars subst in + match_under_common_fix_binders sorec sigma binding_vars + ctx ctx' env env' subst t1' t2' b1' b2' + | PLetIn(na1,c1,u1,t1), LetIn(na2,c2,u2,t2), PLetIn(_,c1',u1',b1), LetIn(na2',c2',u2',b2) -> + let ctx = push_binder na1 na2 u2 ctx in + let ctx' = push_binder na1 na2' u2' ctx' in + let env = EConstr.push_rel (LocalDef (na2,c2,t2)) env in + let subst = sorec ctx env subst c1 c2 in + let subst = sorec ctx env subst c1' c2' in + let subst = Option.fold_left (fun subst u1 -> sorec ctx env subst u1 u2) subst u1 in + let subst = Option.fold_left (fun subst u1' -> sorec ctx env subst u1' u2') subst u1' in + let subst = add_binders na1 na2 binding_vars subst in + match_under_common_fix_binders sorec sigma binding_vars + ctx ctx' env env' subst t1 t2 b1 b2 + | _ -> + sorec ctx' env' (sorec ctx env subst t1 t2) b1 b2 let merge_binding sigma allow_bound_rels ctx n cT subst = let c = match ctx with @@ -364,8 +391,20 @@ let matches_core env sigma allow_bound_rels let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in List.fold_left chk_branch chk_head br1 - | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst - | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst + | PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2)) + when Array.equal Int.equal ln1 ln2 && i1 = i2 -> + let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in + let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in + let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in + Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2 + + | PCoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(lna2,tl2,bl2)) + when i1 = i2 -> + let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in + let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in + let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in + Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2 + | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> Array.fold_left2 (sorec ctx env) subst args1 args2 | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _ diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 587892141..bb563220b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -501,6 +501,97 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) +let rec share_names detype n l avoid env sigma c t = + match EConstr.kind sigma c, EConstr.kind sigma t with + (* factorize even when not necessary to have better presentation *) + | Lambda (na,t,c), Prod (na',t',c') -> + let na = match (na,na') with + Name _, _ -> na + | _, Name _ -> na' + | _ -> na in + let t' = detype avoid env sigma t in + let id = next_name_away na avoid in + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in + share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + (* May occur for fix built interactively *) + | LetIn (na,b,t',c), _ when n > 0 -> + let t'' = detype avoid env sigma t' in + let b' = detype avoid env sigma b in + let id = next_name_away na avoid in + let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in + share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) + (* Only if built with the f/n notation or w/o let-expansion in types *) + | _, LetIn (_,b,_,t) when n > 0 -> + share_names detype n l avoid env sigma c (subst1 b t) + (* If it is an open proof: we cheat and eta-expand *) + | _, Prod (na',t',c') when n > 0 -> + let t'' = detype avoid env sigma t' in + let id = next_name_away na' avoid in + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in + let appc = mkApp (lift 1 c,[|mkRel 1|]) in + share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' + (* If built with the f/n notation: we renounce to share names *) + | _ -> + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + +let rec share_pattern_names detype n l avoid env sigma c t = + let open Pattern in + if n = 0 then + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + else match c, t with + | PLambda (na,t,c), PProd (na',t',c') -> + let na = match (na,na') with + Name _, _ -> na + | _, Name _ -> na' + | _ -> na in + let t' = detype avoid env sigma t in + let id = next_name_away na avoid in + let avoid = Id.Set.add id avoid in + let env = Name id :: env in + share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + | _ -> + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + +let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) = + let def_avoid, def_env, lfi = + Array.fold_left2 + (fun (avoid, env, l) na ty -> + let id = next_name_away na avoid in + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) + (avoid, env, []) names tys in + let n = Array.length tys in + let v = Array.map3 + (fun c t i -> share_names detype (i+1) [] def_avoid def_env sigma c (lift n t)) + bodies tys vn in + GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + +let detype_cofix detype avoid env sigma n (names,tys,bodies) = + let def_avoid, def_env, lfi = + Array.fold_left2 + (fun (avoid, env, l) na ty -> + let id = next_name_away na avoid in + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) + (avoid, env, []) names tys in + let ntys = Array.length tys in + let v = Array.map2 + (fun c t -> share_names detype 0 [] def_avoid def_env sigma c (lift ntys t)) + bodies tys in + GRec(GCoFix n,Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + let detype_universe sigma u = let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in Univ.Universe.map fn u @@ -655,76 +746,8 @@ and detype_r d flags avoid env sigma t = (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) p c bl - | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef - | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef - -and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = - let def_avoid, def_env, lfi = - Array.fold_left2 - (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in - (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) - (avoid, env, []) names tys in - let n = Array.length tys in - let v = Array.map3 - (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t)) - bodies tys vn in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), - Array.map (fun (bl,_,_) -> bl) v, - Array.map (fun (_,_,ty) -> ty) v, - Array.map (fun (_,bd,_) -> bd) v) - -and detype_cofix d flags avoid env sigma n (names,tys,bodies) = - let def_avoid, def_env, lfi = - Array.fold_left2 - (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in - (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) - (avoid, env, []) names tys in - let ntys = Array.length tys in - let v = Array.map2 - (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t)) - bodies tys in - GRec(GCoFix n,Array.of_list (List.rev lfi), - Array.map (fun (bl,_,_) -> bl) v, - Array.map (fun (_,_,ty) -> ty) v, - Array.map (fun (_,bd,_) -> bd) v) - -and share_names d flags n l avoid env sigma c t = - match EConstr.kind sigma c, EConstr.kind sigma t with - (* factorize even when not necessary to have better presentation *) - | Lambda (na,t,c), Prod (na',t',c') -> - let na = match (na,na') with - Name _, _ -> na - | _, Name _ -> na' - | _ -> na in - let t' = detype d flags avoid env sigma t in - let id = next_name_away na avoid in - let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in - share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' - (* May occur for fix built interactively *) - | LetIn (na,b,t',c), _ when n > 0 -> - let t'' = detype d flags avoid env sigma t' in - let b' = detype d flags avoid env sigma b in - let id = next_name_away na avoid in - let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in - share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) - (* Only if built with the f/n notation or w/o let-expansion in types *) - | _, LetIn (_,b,_,t) when n > 0 -> - share_names d flags n l avoid env sigma c (subst1 b t) - (* If it is an open proof: we cheat and eta-expand *) - | _, Prod (na',t',c') when n > 0 -> - let t'' = detype d flags avoid env sigma t' in - let id = next_name_away na' avoid in - let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in - let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' - (* If built with the f/n notation: we renounce to share names *) - | _ -> - if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); - let c = detype d flags avoid env sigma c in - let t = detype d flags avoid env sigma t in - (List.rev l,c,t) + | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef + | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 32b94e1b0..817b8ba6e 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -56,6 +56,13 @@ val detype_sort : evar_map -> Sorts.t -> glob_sort val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> evar_map -> rel_context -> 'a glob_decl_g list +val share_pattern_names : + (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int -> + (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list -> + Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> + Pattern.constr_pattern -> + (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a + val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr (** look for the index of a named var or a nondep var as it is renamed *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 74f2cefab..e89bbf7c3 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> f m1 m2 && Name.equal pat1 pat2 && Option.equal f p1 p2 && f c1 c2 && f t1 t2 - | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> + | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) -> fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && Array.equal f c1 c2 && Array.equal f t1 t2 diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index dcb93bfb6..e52112fda 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -15,7 +15,6 @@ open Globnames open Nameops open Term open Constr -open Vars open Glob_term open Pp open Mod_subst @@ -57,10 +56,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with constr_pattern_eq p1 p2 && constr_pattern_eq r1 r2 && List.equal pattern_eq l1 l2 -| PFix f1, PFix f2 -> - fixpoint_eq f1 f2 -| PCoFix f1, PCoFix f2 -> - cofixpoint_eq f1 f2 +| PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) -> + Array.equal Int.equal ln1 ln2 && Int.equal i1 i2 && rec_declaration_eq f1 f2 +| PCoFix (i1,f1), PCoFix (i2,f2) -> + Int.equal i1 i2 && rec_declaration_eq f1 f2 | PProj (p1, t1), PProj (p2, t2) -> Projection.equal p1 p2 && constr_pattern_eq t1 t2 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ @@ -71,19 +70,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with and pattern_eq (i1, j1, p1) (i2, j2, p2) = Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2 -and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) = - Int.equal i1 i2 && - Array.equal Int.equal arg1 arg2 && - rec_declaration_eq r1 r2 - -and cofixpoint_eq (i1, r1) (i2, r2) = - Int.equal i1 i2 && - rec_declaration_eq r1 r2 - and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && - Array.equal Constr.equal c1 c2 && - Array.equal Constr.equal r1 r2 + Array.equal constr_pattern_eq c1 c2 && + Array.equal constr_pattern_eq r1 r2 let rec occur_meta_pattern = function | PApp (f,args) -> @@ -123,8 +113,10 @@ let rec occurn_pattern n = function | PMeta _ | PSoApp _ -> true | PEvar (_,args) -> Array.exists (occurn_pattern n) args | PVar _ | PRef _ | PSort _ -> false - | PFix fix -> not (noccurn n (mkFix fix)) - | PCoFix cofix -> not (noccurn n (mkCoFix cofix)) + | PFix (_,(_,tl,bl)) -> + Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl + | PCoFix (_,(_,tl,bl)) -> + Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl let noccurn_pattern n c = not (occurn_pattern n c) @@ -209,8 +201,16 @@ let pattern_of_constr env sigma t = in PCase (cip, pattern_of_constr env p, pattern_of_constr env a, Array.to_list (Array.mapi branch_of_constr br)) - | Fix f -> PFix f - | CoFix f -> PCoFix f in + | Fix (lni,(lna,tl,bl)) -> + let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in + let env' = Array.fold_left2 push env lna tl in + PFix (lni,(lna,Array.map (pattern_of_constr env) tl, + Array.map (pattern_of_constr env') bl)) + | CoFix (ln,(lna,tl,bl)) -> + let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in + let env' = Array.fold_left2 push env lna tl in + PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl, + Array.map (pattern_of_constr env') bl)) in pattern_of_constr env t (* To process patterns, we need a translation without typing at all. *) @@ -225,10 +225,14 @@ let map_pattern_with_binders g f l = function | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl) | PProj (p,pc) -> PProj (p, f l pc) + | PFix (lni,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + PFix (lni,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | PCoFix (ln,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* Non recursive *) - | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ - (* Bound to terms *) - | PFix _ | PCoFix _ as x) -> x + | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x let error_instantiate_pattern id l = let is = match l with @@ -262,15 +266,12 @@ let instantiate_pattern env sigma lvar c = error_instantiate_pattern id (List.subtract Id.equal ctx vars) with Not_found (* Map.find failed *) -> x) - | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.") | c -> map_pattern_with_binders (fun id vars -> id::vars) aux vars c in aux [] c let rec liftn_pattern k n = function | PRel i as x -> if i >= n then PRel (i+k) else x - | PFix x -> PFix (destFix (liftn k n (mkFix x))) - | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x))) | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c let lift_pattern k = liftn_pattern k 1 @@ -337,19 +338,35 @@ let rec subst_pattern subst pat = if cip' == cip && typ' == typ && c' == c && branches' == branches then pat else PCase(cip', typ', c', branches') - | PFix fixpoint -> - let cstr = mkFix fixpoint in - let fixpoint' = destFix (subst_mps subst cstr) in - if fixpoint' == fixpoint then pat else - PFix fixpoint' - | PCoFix cofixpoint -> - let cstr = mkCoFix cofixpoint in - let cofixpoint' = destCoFix (subst_mps subst cstr) in - if cofixpoint' == cofixpoint then pat else - PCoFix cofixpoint' - -let mkPLambda na b = PLambda(na,PMeta None,b) -let rev_it_mkPLambda = List.fold_right mkPLambda + | PFix (lni,(lna,tl,bl)) -> + let tl' = Array.smartmap (subst_pattern subst) tl in + let bl' = Array.smartmap (subst_pattern subst) bl in + if bl' == bl && tl' == tl then pat + else PFix (lni,(lna,tl',bl')) + | PCoFix (ln,(lna,tl,bl)) -> + let tl' = Array.smartmap (subst_pattern subst) tl in + let bl' = Array.smartmap (subst_pattern subst) bl in + if bl' == bl && tl' == tl then pat + else PCoFix (ln,(lna,tl',bl')) + +let mkPLetIn na b t c = PLetIn(na,b,t,c) +let mkPProd na t u = PProd(na,t,u) +let mkPLambda na t b = PLambda(na,t,b) +let mkPLambdaUntyped na b = PLambda(na,PMeta None,b) +let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped + +let mkPProd_or_LetIn (na,_,bo,t) c = + match bo with + | None -> mkPProd na t c + | Some b -> mkPLetIn na b (Some t) c + +let mkPLambda_or_LetIn (na,_,bo,t) c = + match bo with + | None -> mkPLambda na t c + | Some b -> mkPLetIn na b (Some t) c + +let it_mkPProd_or_LetIn = List.fold_left (fun c d -> mkPProd_or_LetIn d c) +let it_mkPLambda_or_LetIn = List.fold_left (fun c d -> mkPLambda_or_LetIn d c) let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp @@ -428,7 +445,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function let pred = match p,indnames with | Some p, Some {CAst.v=(_,nal)} -> let nvars = na :: List.rev nal @ vars in - rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) + rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p)) | None, _ -> PMeta None | Some p, None -> match DAst.get p with @@ -450,9 +467,40 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function | GProj(p,c) -> PProj(p, pat_of_raw metas vars c) - | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> + | GRec (GFix (ln,n), ids, decls, tl, cl) -> + if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then + err ?loc (Pp.str "\"struct\" annotation is expected.") + else + let ln = Array.map (fst %> Option.get) ln in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PFix ((ln,n), (names, tl, cl)) + + | GRec (GCoFix n, ids, decls, tl, cl) -> + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PCoFix (n, (names, tl, cl)) + + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ -> err ?loc (Pp.str "Non supported pattern.")) +and pat_of_glob_in_context metas vars decls c = + let rec aux acc vars = function + | (na,bk,b,t) :: decls -> + let decl = (na,bk,Option.map (pat_of_raw metas vars) b,pat_of_raw metas vars t) in + aux (decl::acc) (na::vars) decls + | [] -> + acc, pat_of_raw metas vars c + in aux [] vars decls + and pats_of_glob_branches loc metas vars ind brs = let get_arg p = match DAst.get p with | PatVar na -> @@ -477,7 +525,7 @@ and pats_of_glob_branches loc metas vars ind brs = (str "No unique branch for " ++ int j ++ str"-th constructor."); let lna = List.map get_arg lv in let vars' = List.rev lna @ vars in - let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in + let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in ext, ((j-1, tags, pat) :: pats) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7df0a0c94..2706893ac 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -155,13 +155,6 @@ open Decl_kinds let pr_locality local = if local then keyword "Local" else keyword "Global" - let pr_explanation (e,b,f) = - let a = match e with - | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.") - | ExplByName id -> pr_id id in - let a = if f then str"!" ++ a else a in - if b then str "[" ++ a ++ str "]" else a - let pr_option_ref_value = function | QualidRefValue id -> pr_reference id | StringRefValue s -> qs s @@ -653,16 +646,6 @@ open Decl_kinds keyword "Bind Scope" ++ spc () ++ str sc ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll ) - | VernacArgumentsScope (q,scl) -> - let pr_opt_scope = function - | None -> str"_" - | Some sc -> str sc - in - return ( - keyword "Arguments Scope" - ++ spc() ++ pr_smart_global q - ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - ) | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " @@ -1016,18 +999,6 @@ open Decl_kinds | Some Flags.Current -> [SetOnlyParsing] | Some v -> [SetCompatVersion v])) ) - | VernacDeclareImplicits (q,[]) -> - return ( - hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q) - ) - | VernacDeclareImplicits (q,impls) -> - return ( - hov 1 (keyword "Implicit Arguments" ++ spc () ++ - spc() ++ pr_smart_global q ++ spc() ++ - prlist_with_sep spc (fun imps -> - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") - impls) - ) | VernacArguments (q, args, more_implicits, nargs, mods) -> return ( hov 2 ( diff --git a/stm/stm.ml b/stm/stm.ml index 4b49d1998..e970a02ee 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2884,18 +2884,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); rc - (* Side effect on all branches *) + (* Side effect in a (still open) proof is replayed on all branches*) | VtSideff l, w -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in - VCS.checkout VCS.Branch.master; - VCS.commit id (mkTransCmd x l in_proof `MainQueue); - (* We can't replay a Definition since universes may be differently - * inferred. This holds in Coq >= 8.5 *) - let action = match Vernacprop.under_control x.expr with - | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv - | _ -> ReplayCommand x in - VCS.propagate_sideff ~action; + begin match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); + | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); + | `Proof _ -> + VCS.checkout VCS.Branch.master; + VCS.commit id (mkTransCmd x l true `MainQueue); + (* We can't replay a Definition since universes may be differently + * inferred. This holds in Coq >= 8.5 *) + let action = match Vernacprop.under_control x.expr with + | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv + | _ -> ReplayCommand x in + VCS.propagate_sideff ~action; + end; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok @@ -2924,9 +2928,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; end else begin - VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - (* We hope it can be replayed, but we can't really know *) - VCS.propagate_sideff ~action:(ReplayCommand x); + begin match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + | `Proof _ -> + VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + (* We hope it can be replayed, but we can't really know *) + VCS.propagate_sideff ~action:(ReplayCommand x); + end; VCS.checkout_shallowest_proof_branch (); end in State.define ~safe_id:head_id ~cache:`Yes step id; diff --git a/stm/stm.mli b/stm/stm.mli index a8eb10fb3..7a720aa72 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -39,14 +39,25 @@ module AsyncOpts : sig end -(** The STM doc type determines some properties such as what - uncompleted proofs are allowed and recording of aux files. *) +(** The STM document type [stm_doc_type] determines some properties + such as what uncompleted proofs are allowed and what gets recorded + to aux files. *) type stm_doc_type = - | VoDoc of string - | VioDoc of string - | Interactive of DirPath.t + | VoDoc of string (* file path *) + | VioDoc of string (* file path *) + | Interactive of DirPath.t (* module path *) -(* Main initalization routine *) +(** Coq initalization options: + + - [doc_type]: Type of document being created. + + - [require_libs]: list of libraries/modules to be pre-loaded at + startup. A tuple [(modname,modfrom,import)] is equivalent to [From + modfrom Require modname]; [import] works similarly to + [Library.require_library_from_dirpath], [Some false] will import + the module, [Some true] will additionally export it. + +*) type stm_init_options = { (* The STM will set some internal flags differently depending on the specified [doc_type]. This distinction should dissappear at some @@ -72,12 +83,14 @@ type stm_init_options = { (** The type of a STM document *) type doc +(** [init_core] performs some low-level initalization; should go away + in future releases. *) val init_core : unit -> unit -(* Starts a new document *) +(** [new_doc opt] Creates a new document with options [opt] *) val new_doc : stm_init_options -> doc * Stateid.t -(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing +(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_control CAst.t @@ -115,14 +128,15 @@ val query : doc:doc -> type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ] -(* Evaluates the tip of the current branch *) +(* [observe doc sid]] Check / execute span [sid] *) +val observe : doc:doc -> Stateid.t -> doc + +(* [finish doc] Fully checks a document up to the "current" tip. *) val finish : doc:doc -> doc (* Internal use (fake_ide) only, do not use *) val wait : doc:doc -> doc -val observe : doc:doc -> Stateid.t -> doc - val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 9a8af3a58..4efe1f7ba 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -145,7 +145,7 @@ let classify_vernac e = | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ | VernacChdir _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ - | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _ + | VernacArguments _ | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 834d73bdd..0d9f3d821 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4987,15 +4987,15 @@ let anon_id = Id.of_string "anonymous" let name_op_to_name name_op object_kind suffix = let open Proof_global in let default_gk = (Global, false, object_kind) in + let name, gk = match Proof_global.V82.get_current_initial_conclusions () with + | (id, (_, gk)) -> Some id, gk + | exception NoCurrentProof -> None, default_gk + in match name_op with - | Some s -> - (try let _, gk, _ = Pfedit.current_proof_statement () in s, gk - with NoCurrentProof -> s, default_gk) - | None -> - let name, gk = - try let name, gk, _ = Pfedit.current_proof_statement () in name, gk - with NoCurrentProof -> anon_id, default_gk in - add_suffix name suffix, gk + | Some s -> s, gk + | None -> + let name = Option.default anon_id name in + add_suffix name suffix, gk let tclABSTRACT ?(opaque=true) name_op tac = let s, gk = if opaque diff --git a/test-suite/bugs/closed/1341.v b/test-suite/bugs/closed/1341.v index 8c5a38859..79a0a14d7 100644 --- a/test-suite/bugs/closed/1341.v +++ b/test-suite/bugs/closed/1341.v @@ -8,7 +8,7 @@ Hypothesis Xst : forall A, Equivalence (Xeq A). Variable map : forall A B, (A -> B) -> X A -> X B. -Implicit Arguments map [A B]. +Arguments map [A B]. Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c). intros A B a b c f Hab Hbc. diff --git a/test-suite/bugs/closed/1844.v b/test-suite/bugs/closed/1844.v index 17eeb3529..c41e45900 100644 --- a/test-suite/bugs/closed/1844.v +++ b/test-suite/bugs/closed/1844.v @@ -5,7 +5,7 @@ Definition zeq := Z.eq_dec. Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A := fun y => if zeq x y then v else s y. -Implicit Arguments update [A]. +Arguments update [A]. Definition ident := Z. Parameter operator: Set. diff --git a/test-suite/bugs/closed/1891.v b/test-suite/bugs/closed/1891.v index 685811176..5024a5bc9 100644 --- a/test-suite/bugs/closed/1891.v +++ b/test-suite/bugs/closed/1891.v @@ -3,7 +3,7 @@ Definition f (A: Set) (l: T A): unit := tt. - Implicit Arguments f [A]. + Arguments f [A]. Lemma L (x: T unit): (unit -> T unit) -> unit. Proof. diff --git a/test-suite/bugs/closed/1951.v b/test-suite/bugs/closed/1951.v index 7558b0b86..e950554c4 100644 --- a/test-suite/bugs/closed/1951.v +++ b/test-suite/bugs/closed/1951.v @@ -42,7 +42,7 @@ match s as a return (S a) with pair (ind2 a0) IHl) l) end. (* some induction principle *) -Implicit Arguments ind [S]. +Arguments ind [S]. Lemma k : a -> Type. (* some ininteresting lemma *) intro;pattern H;apply ind;intros. diff --git a/test-suite/bugs/closed/1981.v b/test-suite/bugs/closed/1981.v index 99952682d..a3d942930 100644 --- a/test-suite/bugs/closed/1981.v +++ b/test-suite/bugs/closed/1981.v @@ -1,4 +1,4 @@ -Implicit Arguments ex_intro [A]. +Arguments ex_intro [A]. Goal exists n : nat, True. eapply ex_intro. exact 0. exact I. diff --git a/test-suite/bugs/closed/2362.v b/test-suite/bugs/closed/2362.v index febb9c7bb..10e86cd12 100644 --- a/test-suite/bugs/closed/2362.v +++ b/test-suite/bugs/closed/2362.v @@ -8,7 +8,7 @@ Class Pointed (M:Type -> Type) := Unset Implicit Arguments. Inductive FPair (A B:Type) (neutral: B) : Type:= fpair : forall (a:A) (b:B), FPair A B neutral. -Implicit Arguments fpair [[A] [B] [neutral]]. +Arguments fpair {A B neutral}. Set Implicit Arguments. diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index 23a58501f..6d73d58d4 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -63,7 +63,7 @@ Fixpoint lpSat st f: Prop := end. End PropLogic. -Implicit Arguments lpSat. +Arguments lpSat : default implicits. Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 := match f with @@ -71,7 +71,7 @@ Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 := | LPAnd _ f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2) | LPNot _ f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1) end. -Implicit Arguments LPTransfo. +Arguments LPTransfo : default implicits. Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f. @@ -139,7 +139,7 @@ Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) := fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)). -Implicit Arguments trProd. +Arguments trProd : default implicits. Require Import Setoid. Theorem satTrProd: diff --git a/test-suite/bugs/closed/2404.v b/test-suite/bugs/closed/2404.v index 8ac696e91..f6ec67601 100644 --- a/test-suite/bugs/closed/2404.v +++ b/test-suite/bugs/closed/2404.v @@ -22,13 +22,13 @@ Section Derived. Definition bexportw := exportw base. Definition bwweak := wweak base. - Implicit Arguments bexportw [a b]. + Arguments bexportw [a b]. Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type := starReflS : forall a, RstarSetProof T a a | starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k. -Implicit Arguments starTransS [I T i j k]. +Arguments starTransS [I T i j k]. Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type := (flip (RstarSetProof (flip rel))). diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v index ef2e4e355..b5a723b47 100644 --- a/test-suite/bugs/closed/2584.v +++ b/test-suite/bugs/closed/2584.v @@ -8,7 +8,7 @@ Inductive res (A: Type) : Type := | OK: A -> res A | Error: err -> res A. -Implicit Arguments Error [A]. +Arguments Error [A]. Set Printing Universes. diff --git a/test-suite/bugs/closed/2667.v b/test-suite/bugs/closed/2667.v index 0631e5358..0e6d0108c 100644 --- a/test-suite/bugs/closed/2667.v +++ b/test-suite/bugs/closed/2667.v @@ -1,11 +1,11 @@ -(* Check that extra arguments to Arguments Scope do not disturb use of *) +(* Check that extra arguments to Arguments do not disturb use of *) (* scopes in constructors *) Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt. Bind Scope Cminor with stmt. (* extra argument is ok because of possible coercion to funclass *) -Arguments Scope Scall [_ Cminor ]. +Arguments Scall _ _%Cminor : extra scopes. (* extra argument is ok because of possible coercion to funclass *) Fixpoint f (c: stmt) : Prop := match c with Scall _ => False | _ => False end. diff --git a/test-suite/bugs/closed/2729.v b/test-suite/bugs/closed/2729.v index 7929b8810..c9d65c12c 100644 --- a/test-suite/bugs/closed/2729.v +++ b/test-suite/bugs/closed/2729.v @@ -82,8 +82,8 @@ Inductive SequenceBase (pu : PatchUniverse) (p : pu_type from mid) (qs : SequenceBase pu mid to), SequenceBase pu from to. -Implicit Arguments Nil [pu cxt]. -Implicit Arguments Cons [pu from mid to]. +Arguments Nil [pu cxt]. +Arguments Cons [pu from mid to]. Program Fixpoint insertBase {pu : PatchUniverse} {from mid to : NameSet} diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v index bb607b785..07a5cf91a 100644 --- a/test-suite/bugs/closed/2830.v +++ b/test-suite/bugs/closed/2830.v @@ -49,9 +49,9 @@ Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A) := ; af_level2 : forall x y, age1 x = Some y -> level x = S (level y) }. -Implicit Arguments af_unage [[A] [level] [age1]]. -Implicit Arguments af_level1 [[A] [level] [age1]]. -Implicit Arguments af_level2 [[A] [level] [age1]]. +Arguments af_unage {A level age1}. +Arguments af_level1 {A level age1}. +Arguments af_level2 {A level age1}. Class ageable (A:Type) := mkAgeable { level : A -> nat @@ -77,7 +77,7 @@ Coercion app_pred : pred >-> Funclass. Global Opaque pred. Definition derives {A} `{ageable A} (P Q:pred A) := forall a:A, P a -> Q a. -Implicit Arguments derives. +Arguments derives : default implicits. Program Definition andp {A} `{ageable A} (P Q:pred A) : pred A := fun a:A => P a /\ Q a. @@ -170,7 +170,7 @@ Class Functor `(C:Category) `(D:Category) (im : C -> D) := { fmap g ∘ fmap f ≈ fmap (g ∘ f) }. Coercion functor_im : Functor >-> Funclass. -Implicit Arguments fmap [Object Hom C Object0 Hom0 D im a b]. +Arguments fmap [Object Hom C Object0 Hom0 D im] _ [a b]. Add Parametric Morphism `(C:Category) `(D:Category) (Im:C->D) (F:Functor C D Im) (a b:C) : (@fmap _ _ C _ _ D Im F a b) diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v index 79671ce93..9811733dc 100644 --- a/test-suite/bugs/closed/3068.v +++ b/test-suite/bugs/closed/3068.v @@ -33,7 +33,7 @@ Section Counted_list. End Counted_list. -Implicit Arguments counted_def_nth [A n]. +Arguments counted_def_nth [A n]. Section Finite_nat_set. diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 1f0f3b0da..a1d0b9107 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -21,7 +21,7 @@ Section ILogic_Fun. 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]]. +Arguments ILFunFrm _ {e} _ {ILOps}. Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; ltrue := True; land P Q := P /\ Q; diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v index f5a22bd50..e91c004c7 100644 --- a/test-suite/bugs/closed/3647.v +++ b/test-suite/bugs/closed/3647.v @@ -26,7 +26,7 @@ Record morphism T T' `{e : type T} `{e' : type T'} := mkMorph { morph :> T -> T'; morph_resp : setoid_resp morph}. -Implicit Arguments mkMorph [T T' e e0 e' e1]. +Arguments mkMorph [T T' e0 e e1 e']. Infix "-s>" := morphism (at level 45, right associativity). Section Morphisms. Context {S T U V} `{eS : type S} `{eT : type T} `{eU : type U} `{eV : type V}. @@ -334,8 +334,8 @@ Section ILogic_Fun. End ILogic_Fun. -Implicit Arguments ILFunFrm [[ILOps] [e]]. -Implicit Arguments mkILFunFrm [T Frm ILOps]. +Arguments ILFunFrm _ {e} _ {ILOps}. +Arguments mkILFunFrm [T] _ [Frm ILOps]. Program Definition ILFun_eq {T R} {ILOps: ILogicOps R} {ILogic: ILogic R} (P : T -> R) : @ILFunFrm T _ R ILOps := diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v index 09f1149c2..13d62b8ff 100644 --- a/test-suite/bugs/closed/3732.v +++ b/test-suite/bugs/closed/3732.v @@ -16,7 +16,7 @@ Section machine. | Inj : forall G, Prop -> propX G | ExistsX : forall G A, propX (A :: G) -> propX G. - Implicit Arguments Inj [G]. + Arguments Inj [G]. Definition PropX := propX nil. Fixpoint last (G : list Type) : Type. diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v index 8d7dfbd49..bc9380f90 100644 --- a/test-suite/bugs/closed/4095.v +++ b/test-suite/bugs/closed/4095.v @@ -23,7 +23,7 @@ Section ILogic_Fun. 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]]. +Arguments ILFunFrm _ {e} _ {ILOps}. Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; ltrue := True; land P Q := P /\ Q; diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v index c5bf3289b..da4e53aab 100644 --- a/test-suite/bugs/closed/4865.v +++ b/test-suite/bugs/closed/4865.v @@ -48,5 +48,5 @@ Fail Check g 0 0 1. (* 2nd 0 in bool *) Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end. Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n end. Notation "0" := true. -Arguments Scope lam [nat_scope nat_scope]. +Arguments lam _%nat_scope _%nat_scope : extra scopes. Check (lam 1 0). diff --git a/test-suite/bugs/closed/6631.v b/test-suite/bugs/closed/6631.v new file mode 100644 index 000000000..100dc13fc --- /dev/null +++ b/test-suite/bugs/closed/6631.v @@ -0,0 +1,7 @@ +Require Import Coq.derive.Derive. + +Derive f SuchThat (f = 1 + 1) As feq. +Proof. + transitivity 2; [refine (eq_refl 2)|]. + transitivity 2. + 2:abstract exact (eq_refl 2). diff --git a/test-suite/bugs/closed/7092.v b/test-suite/bugs/closed/7092.v new file mode 100644 index 000000000..d90de8b93 --- /dev/null +++ b/test-suite/bugs/closed/7092.v @@ -0,0 +1,70 @@ +(* Examples matching fix/cofix in Ltac pattern-matching *) + +Goal True. +lazymatch (eval cbv delta [Nat.add] in Nat.add) with +| (fix F (n : nat) (v : ?A) {struct n} : @?P n v + := match n with + | O => @?O_case v + | S n' => @?S_case n' v F + end) + => + unify A nat; + unify P (fun _ _ : nat => nat); + unify O_case (fun v : nat => v); + unify S_case (fun (p : nat) (m : nat) (add : nat -> nat -> nat) + => S (add p m)) + end. +Abort. + +Fixpoint f l n := match n with 0 => 0 | S n => g n (cons n l) end +with g n l := match n with 0 => 1 | S n => f (cons 0 l) n end. + +Goal True. + +lazymatch (eval cbv delta [f] in f) with +| fix myf (l : ?L) (n : ?N) {struct n} : nat := + match n as _ with + | 0 => ?Z + | S n0 => @?S myf myg n0 l + end + with myg (n' : ?N') (l' : ?L') {struct n'} : nat := + match n' as _ with + | 0 => ?Z' + | S n0' => @?S' myf myg n0' l' + end + for myf => + unify L (list nat); + unify L' (list nat); + unify N nat; + unify N' nat; + unify Z 0; + unify Z' 1; + unify S (fun (f : L -> N -> nat) (g : N -> L -> nat) n l => g n (cons n l)); + unify S' (fun (f : L -> N -> nat) (g : N -> L -> nat) (n:N) l => f (cons 0 l) n) +end. + +Abort. + +CoInductive S1 := C1 : nat -> S2 -> S1 with S2 := C2 : bool -> S1 -> S2. + +CoFixpoint f' n l := C1 n (g' (cons n l) n n) +with g' l n p := C2 true (f' (S n) l). + +Goal True. + +lazymatch (eval cbv delta [f'] in f') with +| cofix myf (n : ?N) (l : ?L) : ?T := @?X n g l + with g (l' : ?L') (n' : ?N') (p' : ?N'') : ?T' := @?X' n' myf l' + for myf => + unify L (list nat); + unify L' (list nat); + unify N nat; + unify N' nat; + unify N'' nat; + unify T S1; + unify T' S2; + unify X (fun n g l => C1 n (g (cons n l) n n)); + unify X' (fun n f (l : list nat) => C2 true (f (S n) l)) +end. + +Abort. diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v index 6cca5c9fb..5294adefd 100644 --- a/test-suite/bugs/opened/2456.v +++ b/test-suite/bugs/opened/2456.v @@ -6,7 +6,7 @@ Parameter Patch : nat -> nat -> Set. Inductive Catch (from to : nat) : Type := MkCatch : forall (p : Patch from to), Catch from to. -Implicit Arguments MkCatch [from to]. +Arguments MkCatch [from to]. Inductive CatchCommute5 : forall {from mid1 mid2 to : nat}, diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v index 2a156e333..c09649de7 100644 --- a/test-suite/bugs/opened/3295.v +++ b/test-suite/bugs/opened/3295.v @@ -5,7 +5,7 @@ Class lops := lmk_ops { weq: relation car }. -Implicit Arguments car []. +Arguments car : clear implicits. Coercion car: lops >-> Sortclass. @@ -23,7 +23,7 @@ Class ops := mk_ops { dot: forall n m p, mor n m -> mor m p -> mor n p }. Coercion mor: ops >-> Funclass. -Implicit Arguments ob []. +Arguments ob : clear implicits. Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p). Proof. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index 08f489d75..a76fa19d3 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -47,7 +47,7 @@ Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), joinmap key j. Parameter ADMIT: forall p: Prop, p. -Implicit Arguments ADMIT [p]. +Arguments ADMIT [p]. Module Share. Parameter jb : joinable bool. diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v index a148ebe8e..0ef4b417a 100644 --- a/test-suite/failure/check.v +++ b/test-suite/failure/check.v @@ -1,3 +1,3 @@ -Implicit Arguments eq [A]. +Arguments eq [A]. Fail Check (bool = true). diff --git a/test-suite/ide/bug7088.fake b/test-suite/ide/bug7088.fake new file mode 100644 index 000000000..e2a2aa52a --- /dev/null +++ b/test-suite/ide/bug7088.fake @@ -0,0 +1,13 @@ +ADD { Arguments id T x : rename. } +ADD { Lemma foo : True. } +ADD here { Proof. } +ADD { exact 3. } +ADD { Qed. } +WAIT +EDIT_AT here +ADD { Arguments id FOO BAR : rename. } +ADD { exact I. } +ADD { Qed. } +ADD { Arguments id T x : assert. } +JOIN + diff --git a/test-suite/ide/load.fake b/test-suite/ide/load.fake new file mode 100644 index 000000000..f6a7ef4dc --- /dev/null +++ b/test-suite/ide/load.fake @@ -0,0 +1,11 @@ +ADD revert { Load "output/load/Load_noproof.v". } +ADD { Load "output/load/Load_proof.v". } +ADD { Fail Load "output/load/Load_openproof.v". } +WAIT +QUERY { Check f. } +QUERY { Check u. } +EDIT_AT revert +QUERY { Check f. } +QUERY { Fail Check u. } +JOIN + diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 8ba8525c6..be3310491 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -1,8 +1,8 @@ Set Implicit Arguments. Unset Strict Implicit. -Implicit Arguments fst. -Implicit Arguments snd. +Arguments fst : default implicits. +Arguments snd : default implicits. Module Type PO. Parameter T : Set. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index 7214287a6..ece1b47b4 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -1,7 +1,7 @@ Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) (th el : T) := if s then th else el. -Implicit Arguments ifte. +Arguments ifte : default implicits. Lemma Reflexivity_provable : forall (A : Set) (a : A) (s : {a = a} + {a <> a}), diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v index 8700a6c4e..6d9117c05 100644 --- a/test-suite/prerequisite/make_local.v +++ b/test-suite/prerequisite/make_local.v @@ -2,8 +2,7 @@ Definition f (A:Type) (a:A) := a. -Local Arguments Scope f [type_scope type_scope]. -Local Implicit Arguments f [A]. +Local Arguments f [A]%type_scope _%type_scope. (* Used in ImportedCoercion.v to test the locality flag *) diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v index b4efa7edc..d0aa5c857 100644 --- a/test-suite/success/AdvancedTypeClasses.v +++ b/test-suite/success/AdvancedTypeClasses.v @@ -28,8 +28,8 @@ Class interp_pair (abs : Type) := { repr : term; link: abs = interp repr }. -Implicit Arguments repr [[interp_pair]]. -Implicit Arguments link [[interp_pair]]. +Arguments repr _ {interp_pair}. +Arguments link _ {interp_pair}. Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)). simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index 921433cad..9a19b595e 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -2,7 +2,7 @@ Inductive vector {A : Type} : nat -> Type := | vnil : vector 0 | vcons : A -> forall {n'}, vector n' -> vector (S n'). -Implicit Arguments vector []. +Arguments vector A : clear implicits. Require Import Coq.Program.Program. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 5b1482fd5..f07c0191f 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -73,7 +73,7 @@ CoInductive LList (A : Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. -Implicit Arguments LNil [A]. +Arguments LNil [A]. Inductive Finite (A : Set) : LList A -> Prop := | Finite_LNil : Finite LNil diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 45c71615f..ca8da3948 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := | in_first : forall e, in_extension r (add_rule r e) | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Implicit Arguments NL [I]. +Arguments NL [I]. Inductive super_extension (I : Set) (e : extension I) : extension I -> Type := diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 841940492..29350d620 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -991,10 +991,10 @@ Proof. Qed. -Implicit Arguments Vector.cons [A n]. -Implicit Arguments Vector.nil [A]. -Implicit Arguments Vector.hd [A n]. -Implicit Arguments Vector.tl [A n]. +Arguments Vector.cons [A] _ [n]. +Arguments Vector.nil [A]. +Arguments Vector.hd [A n]. +Arguments Vector.tl [A n]. Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n. Proof. @@ -1064,7 +1064,7 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v} | S n', Vector.cons _ v' => vector_nth A n' _ v' end. -Implicit Arguments vector_nth [A p]. +Arguments vector_nth [A] _ [p]. Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b, @@ -1159,7 +1159,7 @@ infiniteproof map_iterate'. Qed. -Implicit Arguments LNil [A]. +Arguments LNil [A]. Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A), LNil <> (LCons a l). diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index 6f27c1d36..18ebcd638 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -5,7 +5,7 @@ Require Import Program. Require Import List. Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }. -Implicit Arguments vector []. +Arguments vector : clear implicits. Coercion vec_list : vector >-> list. diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index ca3746716..2da630633 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -11,7 +11,7 @@ Check (A.opp 3). Record B := { f :> Z -> Z }. Variable a:B. -Arguments Scope a [Z_scope]. +Arguments a _%Z_scope : extra scopes. Check a 0. (* Check that casts activate scopes if ever possible *) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index cd6eac35c..400479ae8 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -128,8 +128,8 @@ Record Monad {m : Type -> Type} := { Print Visibility. Print unit. -Implicit Arguments unit [[m] [m0] [α]]. -Implicit Arguments Monad []. +Arguments unit {m m0 α}. +Arguments Monad : clear implicits. Notation "'return' t" := (unit t). (* Test correct handling of existentials and defined fields. *) diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 02e043bc3..b287b5fac 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -39,7 +39,7 @@ Qed. (* Check apply/eapply distinction in presence of open terms *) Parameter h : forall x y z : nat, x = z -> x = y. -Implicit Arguments h [[x] [y]]. +Arguments h {x y}. Goal 1 = 0 -> True. intro H. apply h in H || exact I. diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index f5bb884d2..55ae54ca0 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -42,7 +42,7 @@ Inductive ctx : Type := Bind Scope context_scope with ctx. Delimit Scope context_scope with ctx. -Arguments Scope snoc [context_scope]. +Arguments snoc _%context_scope. Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 627794832..5b13f35d5 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -386,7 +386,7 @@ Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri { tri0 : forall a b c, R a b -> S a c -> T b c }. -Implicit Arguments mkTri [R S T]. +Arguments mkTri [R S T]. Definition tri_iffT : tri iffT iffT iffT := (mkTri (fun X0 X1 X2 E01 E02 => diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index a0981311b..23853890d 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -33,11 +33,11 @@ Definition eq1 := fun (A:Type) (x y:A) => x=y. Definition eq2 := fun (A:Type) (x y:A) => x=y. Definition eq3 := fun (A:Type) (x y:A) => x=y. -Implicit Arguments op' []. -Global Implicit Arguments op'' []. +Arguments op' : clear implicits. +Global Arguments op'' : clear implicits. -Implicit Arguments eq2 []. -Global Implicit Arguments eq3 []. +Arguments eq2 : clear implicits. +Global Arguments eq3 : clear implicits. Check (op 0 0). Check (op' nat 0 0). @@ -89,14 +89,14 @@ Fixpoint plus n m {struct n} := (* Check multiple implicit arguments signatures *) -Implicit Arguments eq_refl [[A] [x]] [[A]]. +Arguments eq_refl {A x}, {A}. Check eq_refl : 0 = 0. (* Check that notations preserve implicit (since 8.3) *) Parameter p : forall A, A -> forall n, n = 0 -> True. -Implicit Arguments p [A n]. +Arguments p [A] _ [n]. Notation Q := (p 0). Check Q eq_refl. diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el index 662762b08..7c59fb6ae 100644 --- a/tools/gallina-syntax.el +++ b/tools/gallina-syntax.el @@ -432,7 +432,6 @@ ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") - ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") ("Cd" nil "Cd #." nil "Cd") diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9ff4e3302..5dcc170b1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2025,7 +2025,6 @@ let interp ?proof ~atts ~st c = | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) - | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc | VernacNotation (c,infpl,sc) -> vernac_notation ~atts c infpl sc @@ -2099,8 +2098,6 @@ let interp ?proof ~atts ~st c = vernac_hints ~atts dbnames hints | VernacSyntacticDefinition (id,c,b) -> vernac_syntactic_definition ~atts id c b - | VernacDeclareImplicits (qid,l) -> - vernac_declare_implicits ~atts qid l | VernacArguments (qid, args, more_implicits, nargs, flags) -> vernac_arguments ~atts qid args more_implicits nargs flags | VernacReserve bl -> vernac_reserve bl @@ -2168,7 +2165,7 @@ let check_vernac_supports_locality c l = | VernacDeclareMLModule _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ | VernacSyntacticDefinition _ - | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ + | VernacArguments _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ | VernacSetOption _ | VernacUnsetOption _ |