diff options
91 files changed, 445 insertions, 2862 deletions
diff --git a/.travis.yml b/.travis.yml index b9ea455da..6c926aacb 100644 --- a/.travis.yml +++ b/.travis.yml @@ -147,7 +147,8 @@ matrix: - brew update --debug --verbose - brew install opam gnu-time - - os: osx + - if: NOT type IS pull_request + os: osx osx_image: xcode8.3 env: - TEST_TARGET="" diff --git a/API/API.mli b/API/API.mli index 654d93485..3ed326ff0 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2751,15 +2751,15 @@ sig the whole identifier except for the {i subscript}. E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) - val next_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t - val next_ident_away_in_goal : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val default_dependent_ident : Names.Id.t - val next_global_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val rename_bound_vars_as_displayed : - Evd.evar_map -> Names.Id.t list -> Names.Name.t list -> EConstr.types -> EConstr.types + Evd.evar_map -> Names.Id.Set.t -> Names.Name.t list -> EConstr.types -> EConstr.types end module Termops : @@ -3670,7 +3670,7 @@ sig type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located type opacity_flag = - | Opaque of lident list option + | Opaque | Transparent type locality_flag = bool type inductive_kind = @@ -4011,7 +4011,7 @@ sig | Later : [ `thunk ] delay val print_universes : bool ref val print_evar_arguments : bool ref - val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g + val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit end @@ -4628,6 +4628,7 @@ sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.Id.t list + val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Names.Id.Set.t val pf_concl : 'a Proofview.Goal.t -> EConstr.types val pf_get_new_id : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types @@ -5140,7 +5141,7 @@ sig val convert_concl : ?check:bool -> EConstr.types -> Constr.cast_kind -> unit tactic val intro_using : Names.Id.t -> unit tactic val intro : unit tactic - val fresh_id_in_env : Names.Id.t list -> Names.Id.t -> Environ.env -> Names.Id.t + val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t val is_quantified_hypothesis : Names.Id.t -> 'a Goal.t -> bool val tclABSTRACT : ?opaque:bool -> Names.Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val intro_patterns : bool -> Tactypes.intro_patterns -> unit Proofview.tactic @@ -5240,7 +5241,7 @@ sig val eapply_with_bindings : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic val assert_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic -> unit Proofview.tactic - val intro_avoiding : Names.Id.t list -> unit Proofview.tactic + val intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic val pattern_option : (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic val compute_elim_sig : Evd.evar_map -> ?elimc:EConstr.constr Misctypes.with_bindings -> EConstr.types -> elim_scheme diff --git a/COMPATIBILITY b/COMPATIBILITY index 78dfabaa3..b5fed7f01 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -5,6 +5,10 @@ Potential sources of incompatibilities between Coq V8.6 and V8.7 error rather than a warning when the superfluous name is already in use. The easy fix is to remove the superfluous name. +- Proofs ending in "Qed exporting ident, .., ident" are not supported + anymore. Constants generated during `abstract` are kept private to the + local environment. + Potential sources of incompatibilities between Coq V8.5 and V8.6 ---------------------------------------------------------------- diff --git a/Makefile.doc b/Makefile.doc index 0c3b70149..faa9c879c 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -61,7 +61,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ - RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \ + RefMan-uti.tex RefMan-ide.tex RefMan-modr.tex \ AsyncProofs.tex RefMan-ssr.tex) \ $(REFMANCOQTEXFILES) \ diff --git a/dev/Coq_Bugzilla_autolink.user.js b/dev/Coq_Bugzilla_autolink.user.js new file mode 100644 index 000000000..371c5adc0 --- /dev/null +++ b/dev/Coq_Bugzilla_autolink.user.js @@ -0,0 +1,34 @@ +// ==UserScript== +// @name Coq Bugzilla autolink +// @namespace SkySkimmer +// @include https://github.com/coq/coq/* +// @description Makes BZ#XXXX into links to bugzilla for GitHub +// @version 1 +// @grant none +// ==/UserScript== + +var regex = /BZ#(\d+)/g; +var substr = '<a href="https://coq.inria.fr/bugs/show_bug.cgi?id=$1">$&</a>'; + +function doNode(node) +{ + node.innerHTML = node.innerHTML.replace(regex,substr); +} + +var comments = document.getElementsByClassName("comment-body"); + +for(var i=0; i<comments.length; i++) +{ + var pars = comments[i].getElementsByTagName("p"); + for(var j=0; j<pars.length; j++) + { + doNode(pars[j]); + } +} + +// usually 1 or 0 titles... +var titles = document.getElementsByClassName("js-issue-title"); +for(var i=0; i<titles.length; i++) +{ + doNode(titles[i]); +} diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index f3e4cec0b..f12cbe0a7 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -910,6 +910,10 @@ function make_camlp5 { log2 make install # For some reason gramlib.a is not copied, but it is required by Coq cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/" + # For some reason META is not copied, but it is required by coq_makefile + log2 make -C etc META + mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/" + cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/" log2 make clean build_post fi diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index ca6a5643c..e2fbf1f6d 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -23,13 +23,19 @@ if %USEOPAM% == false ( call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^ -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ - -setup %CYGROOT%\%SETUP% - copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis - 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* + -setup %CYGROOT%\%SETUP% || GOTO ErrorExit + copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit + 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit ) if %USEOPAM% == true ( %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^ -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time - %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh + %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit ) + +GOTO :EOF + +:ErrorExit + ECHO ERROR MakeCoq_MinGW.bat failed + EXIT /b 1 diff --git a/doc/refman/RefMan-add.tex b/doc/refman/RefMan-add.tex deleted file mode 100644 index 2094c9d2d..000000000 --- a/doc/refman/RefMan-add.tex +++ /dev/null @@ -1,58 +0,0 @@ -\chapter[List of additional documentation]{List of additional documentation\label{Addoc}} - -\section[Tutorials]{Tutorials\label{Tutorial}} -A companion volume to this reference manual, the \Coq\ Tutorial, is -aimed at gently introducing new users to developing proofs in \Coq\ -without assuming prior knowledge of type theory. In a second step, the -user can read also the tutorial on recursive types (document {\tt -RecTutorial.ps}). - -\section[The \Coq\ standard library]{The \Coq\ standard library\label{Addoc-library}} -A brief description of the \Coq\ standard library is given in the additional -document {\tt Library.dvi}. - -\section[Installation and un-installation procedures]{Installation and un-installation procedures\label{Addoc-install}} -A \verb!INSTALL! file in the distribution explains how to install -\Coq. - -\section[{\tt Extraction} of programs]{{\tt Extraction} of programs\label{Addoc-extract}} -{\tt Extraction} is a package offering some special facilities to -extract ML program files. It is described in the separate document -{\tt Extraction.dvi} -\index{Extraction of programs} - -\section[{\tt Program}]{A tool for {\tt Program}-ing\label{Addoc-program}} -{\tt Program} is a package offering some special facilities to -extract ML program files. It is described in the separate document -{\tt Program.dvi} -\index{Program-ing} - -\section[Proof printing in {\tt Natural} language]{Proof printing in {\tt Natural} language\label{Addoc-natural}} -{\tt Natural} is a tool to print proofs in natural language. -It is described in the separate document {\tt Natural.dvi}. -\index{Natural@{\tt Print Natural}} -\index{Printing in natural language} - -\section[The {\tt Omega} decision tactic]{The {\tt Omega} decision tactic\label{Addoc-omega}} -{\bf Omega} is a tactic to automatically solve arithmetical goals in -Presburger arithmetic (i.e. arithmetic without multiplication). -It is described in the separate document {\tt Omega.dvi}. -\index{Omega@{\tt Omega}} - -\section[Simplification on rings]{Simplification on rings\label{Addoc-polynom}} -A documentation of the package {\tt polynom} (simplification on rings) -can be found in the document {\tt Polynom.dvi} -\index{Polynom@{\tt Polynom}} -\index{Simplification on rings} - -%\section[Anomalies]{Anomalies\label{Addoc-anomalies}} -%The separate document {\tt Anomalies.*} gives a list of known -%anomalies and bugs of the system. Before communicating us an -%anomalous behavior, please check first whether it has been already -%reported in this document. - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex deleted file mode 100644 index dac3c60bd..000000000 --- a/doc/refman/RefMan-coi.tex +++ /dev/null @@ -1,405 +0,0 @@ -%\documentstyle[11pt,../tools/coq-tex/coq]{article} -%\input{title} - -%\include{macros} -%\begin{document} - -%\coverpage{Co-inductive types in Coq}{Eduardo Gim\'enez} -\chapter[Co-inductive types in Coq]{Co-inductive types in Coq\label{Co-inductives}} - -%\begin{abstract} -{\it Co-inductive} types are types whose elements may not be well-founded. -A formal study of the Calculus of Constructions extended by -co-inductive types has been presented -in \cite{Gim94}. It is based on the notion of -{\it guarded definitions} introduced by Th. Coquand -in \cite{Coquand93}. The implementation is by E. Gim\'enez. -%\end{abstract} - -\section{A short introduction to co-inductive types} - -We assume that the reader is rather familiar with inductive types. -These types are characterized by their {\it constructors}, which can be -regarded as the basic methods from which the elements -of the type can be built up. It is implicit in the definition -of an inductive type that -its elements are the result of a {\it finite} number of -applications of its constructors. Co-inductive types arise from -relaxing this implicit condition and admitting that an element of -the type can also be introduced by a non-ending (but effective) process -of construction defined in terms of the basic methods which characterize the -type. So we could think in the wider notion of types defined by -constructors (let us call them {\it recursive types}) and classify -them into inductive and co-inductive ones, depending on whether or not -we consider non-ending methods as admissible for constructing elements -of the type. Note that in both cases we obtain a ``closed type'', all whose -elements are pre-determined in advance (by the constructors). When we -know that $a$ is an element of a recursive type (no matter if it is -inductive or co-inductive) what we know is that it is the result of applying -one of the basic forms of construction allowed for the type. -So the more primitive way of eliminating an element of a recursive type is -by case analysis, i.e. by considering through which constructor it could have -been introduced. In the case of inductive sets, the additional knowledge that -constructors can be applied only a finite number of times provide -us with a more powerful way of eliminating their elements, say, -the principle of -induction. This principle is obviously not valid for co-inductive types, -since it is just the expression of this extra knowledge attached to inductive -types. - - -An example of a co-inductive type is the type of infinite sequences formed with -elements of type $A$, or streams for shorter. In Coq, -it can be introduced using the \verb!CoInductive! command~: -\begin{coq_example} -CoInductive Stream (A:Set) : Set := - cons : A -> Stream A -> Stream A. -\end{coq_example} - -The syntax of this command is the same as the -command \verb!Inductive! (cf. section -\ref{gal_Inductive_Definitions}). -Definition of mutually co-inductive types are possible. - -As was already said, there are not principles of -induction for co-inductive sets, the only way of eliminating these -elements is by case analysis. -In the example of streams, this elimination principle can be -used for instance to define the well known -destructors on streams $\hd : (\Str\;A)\rightarrow A$ -and $\tl: (\Str\;A)\rightarrow (\Str\;A)$ : -\begin{coq_example} -Section Destructors. -Variable A : Set. -Definition hd (x:Stream A) := match x with - | cons a s => a - end. -Definition tl (x:Stream A) := match x with - | cons a s => s - end. -\end{coq_example} -\begin{coq_example*} -End Destructors. -\end{coq_example*} - -\subsection{Non-ending methods of construction} - -At this point the reader should have realized that we have left unexplained -what is a ``non-ending but effective process of -construction'' of a stream. In the widest sense, a -method is a non-ending process of construction if we can eliminate the -stream that it introduces, in other words, if we can reduce -any case analysis on it. In this sense, the following ways of -introducing a stream are not acceptable. -\begin{center} -$\zeros = (\cons\;\nat\;\nO\;(\tl\;\zeros))\;\;:\;\;(\Str\;\nat)$\\[12pt] -$\filter\;(\cons\;A\;a\;s) = \si\;\;(P\;a)\;\;\alors\;\;(\cons\;A\;a\;(\filter\;s))\;\;\sinon\;\;(\filter\;s) )\;\;:\;\;(\Str\;A)$ -\end{center} -\noindent The former it is not valid since the stream can not be eliminated -to obtain its tail. In the latter, a stream is naively defined as -the result of erasing from another (arbitrary) stream -all the elements which does not verify a certain property $P$. This -does not always makes sense, for example it does not when all the elements -of the stream verify $P$, in which case we can not eliminate it to -obtain its head\footnote{Note that there is no notion of ``the empty -stream'', a stream is always infinite and build by a \texttt{cons}.}. -On the contrary, the following definitions are acceptable methods for -constructing a stream~: -\begin{center} -$\zeros = (\cons\;\nat\;\nO\;\zeros)\;\;:\;\;(\Str\;\nat)\;\;\;(*)$\\[12pt] -$(\from\;n) = (\cons\;\nat\;n\;(\from\;(\nS\;n)))\;:\;(\Str\;\nat)$\\[12pt] -$\alter = (\cons\;\bool\;\true\;(\cons\;\bool\;\false\;\alter))\;:\;(\Str\;\bool)$. -\end{center} -\noindent The first one introduces a stream containing all the natural numbers -greater than a given one, and the second the stream which infinitely -alternates the booleans true and false. - -In general it is not evident to realise when a definition can -be accepted or not. However, there is a class of definitions that -can be easily recognised as being valid : those -where (1) all the recursive calls of the method are done -after having explicitly mentioned which is (at least) the first constructor -to start building the element, and (2) no other -functions apart from constructors are applied to recursive calls. -This class of definitions is usually -referred as {\it guarded-by-constructors} -definitions \cite{Coquand93,Gim94}. -The methods $\from$ -and $\alter$ are examples of definitions which are guarded by constructors. -The definition of function $\filter$ is not, because there is no -constructor to guard -the recursive call in the {\it else} branch. Neither is the one of -$\zeros$, since there is function applied to the recursive call -which is not a constructor. However, there is a difference between -the definition of $\zeros$ and $\filter$. The former may be seen as a -wrong way of characterising an object which makes sense, and it can -be reformulated in an admissible way using the equation (*). On the contrary, -the definition of -$\filter$ can not be patched, since is the idea itself -of traversing an infinite -construction searching for an element whose existence is not ensured -which does not make sense. - - - -Guarded definitions are exactly the kind of non-ending process of -construction which are allowed in Coq. The way of introducing -a guarded definition in Coq is using the special command -{\tt CoFixpoint}. This command verifies that the definition introduces an -element of a co-inductive type, and checks if it is guarded by constructors. -If we try to -introduce the definitions above, $\from$ and $\alter$ will be accepted, -while $\zeros$ and $\filter$ will be rejected giving some explanation -about why. -\begin{coq_example} -CoFixpoint zeros : Stream nat := cons nat 0%N (tl nat zeros). -CoFixpoint zeros : Stream nat := cons nat 0%N zeros. -CoFixpoint from (n:nat) : Stream nat := cons nat n (from (S n)). -\end{coq_example} - -As in the \verb!Fixpoint! command (see Section~\ref{Fixpoint}), it is possible -to introduce a block of mutually dependent methods. The general syntax -for this case is : - -{\tt CoFixpoint {\ident$_1$} :{\term$_1$} := {\term$_1'$}\\ - with\\ - \mbox{}\hspace{0.1cm} $\ldots$ \\ - with {\ident$_m$} : {\term$_m$} := {\term$_m'$}} - - -\subsection{Non-ending methods and reduction} - -The elimination of a stream introduced by a \verb!CoFixpoint! definition -is done lazily, i.e. its definition can be expanded only when it occurs -at the head of an application which is the argument of a case expression. -Isolately it is considered as a canonical expression which -is completely evaluated. We can test this using the command \verb!compute! -to calculate the normal forms of some terms~: -\begin{coq_example} -Eval compute in (from 0). -Eval compute in (hd nat (from 0)). -Eval compute in (tl nat (from 0)). -\end{coq_example} -\noindent Thus, the equality -$(\from\;n)\equiv(\cons\;\nat\;n\;(\from \; (\S\;n)))$ -does not hold as definitional one. Nevertheless, it can be proved -as a propositional equality, in the sense of Leibniz's equality. -The version {\it à la Leibniz} of the equality above follows from -a general lemma stating that eliminating and then re-introducing a stream -yields the same stream. -\begin{coq_example} -Lemma unfold_Stream : - forall x:Stream nat, x = match x with - | cons a s => cons nat a s - end. -\end{coq_example} - -\noindent The proof is immediate from the analysis of -the possible cases for $x$, which transforms -the equality in a trivial one. - -\begin{coq_example} -olddestruct x. -trivial. -\end{coq_example} -\begin{coq_eval} -Qed. -\end{coq_eval} -The application of this lemma to $(\from\;n)$ puts this -constant at the head of an application which is an argument -of a case analysis, forcing its expansion. -We can test the type of this application using Coq's command \verb!Check!, -which infers the type of a given term. -\begin{coq_example} -Check (fun n:nat => unfold_Stream (from n)). -\end{coq_example} - \noindent Actually, The elimination of $(\from\;n)$ has actually -no effect, because it is followed by a re-introduction, -so the type of this application is in fact -definitionally equal to the -desired proposition. We can test this computing -the normal form of the application above to see its type. -\begin{coq_example} -Transparent unfold_Stream. -Eval compute in (fun n:nat => unfold_Stream (from n)). -\end{coq_example} - - -\section{Reasoning about infinite objects} - -At a first sight, it might seem that -case analysis does not provide a very powerful way -of reasoning about infinite objects. In fact, what we can prove about -an infinite object using -only case analysis is just what we can prove unfolding its method -of construction a finite number of times, which is not always -enough. Consider for example the following method for appending -two streams~: -\begin{coq_example} -Variable A : Set. -CoFixpoint conc (s1 s2:Stream A) : Stream A := - cons A (hd A s1) (conc (tl A s1) s2). -\end{coq_example} - -Informally speaking, we expect that for all pair of streams $s_1$ and $s_2$, -$(\conc\;s_1\;s_2)$ -defines the ``the same'' stream as $s_1$, -in the sense that if we would be able to unfold the definition -``up to the infinite'', we would obtain definitionally equal normal forms. -However, no finite unfolding of the definitions gives definitionally -equal terms. Their equality can not be proved just using case analysis. - - -The weakness of the elimination principle proposed for infinite objects -contrast with the power provided by the inductive -elimination principles, but it is not actually surprising. It just means -that we can not expect to prove very interesting things about infinite -objects doing finite proofs. To take advantage of infinite objects we -have to consider infinite proofs as well. For example, -if we want to catch up the equality between $(\conc\;s_1\;s_2)$ and -$s_1$ we have to introduce first the type of the infinite proofs -of equality between streams. This is a -co-inductive type, whose elements are build up from a -unique constructor, requiring a proof of the equality of the -heads of the streams, and an (infinite) proof of the equality -of their tails. - -\begin{coq_example} -CoInductive EqSt : Stream A -> Stream A -> Prop := - eqst : - forall s1 s2:Stream A, - hd A s1 = hd A s2 -> EqSt (tl A s1) (tl A s2) -> EqSt s1 s2. -\end{coq_example} -\noindent Now the equality of both streams can be proved introducing -an infinite object of type - -\noindent $(\EqSt\;s_1\;(\conc\;s_1\;s_2))$ by a \verb!CoFixpoint! -definition. -\begin{coq_example} -CoFixpoint eqproof (s1 s2:Stream A) : EqSt s1 (conc s1 s2) := - eqst s1 (conc s1 s2) (eq_refl (hd A (conc s1 s2))) - (eqproof (tl A s1) s2). -\end{coq_example} -\begin{coq_eval} -Reset eqproof. -\end{coq_eval} -\noindent Instead of giving an explicit definition, -we can use the proof editor of Coq to help us in -the construction of the proof. -A tactic \verb!Cofix! allows placing a \verb!CoFixpoint! definition -inside a proof. -This tactic introduces a variable in the context which has -the same type as the current goal, and its application stands -for a recursive call in the construction of the proof. If no name is -specified for this variable, the name of the lemma is chosen by -default. -%\pagebreak - -\begin{coq_example} -Lemma eqproof : forall s1 s2:Stream A, EqSt s1 (conc s1 s2). -cofix. -\end{coq_example} - -\noindent An easy (and wrong!) way of finishing the proof is just to apply the -variable \verb!eqproof!, which has the same type as the goal. - -\begin{coq_example} -intros. -apply eqproof. -\end{coq_example} - -\noindent The ``proof'' constructed in this way -would correspond to the \verb!CoFixpoint! definition -\begin{coq_example*} -CoFixpoint eqproof : forall s1 s2:Stream A, EqSt s1 (conc s1 s2) := - eqproof. -\end{coq_example*} - -\noindent which is obviously non-guarded. This means that -we can use the proof editor to -define a method of construction which does not make sense. However, -the system will never accept to include it as part of the theory, -because the guard condition is always verified before saving the proof. - -\begin{coq_example} -Qed. -\end{coq_example} - -\noindent Thus, the user must be careful in the -construction of infinite proofs -with the tactic \verb!Cofix!. Remark that once it has been used -the application of tactics performing automatic proof search in -the environment (like for example \verb!Auto!) -could introduce unguarded recursive calls in the proof. -The command \verb!Guarded! verifies -that the guarded condition has been not violated -during the construction of the proof. This command can be -applied even if the proof term is not complete. - - - -\begin{coq_example} -Restart. -cofix. -auto. -Guarded. -Undo. -Guarded. -\end{coq_example} - -\noindent To finish with this example, let us restart from the -beginning and show how to construct an admissible proof~: - -\begin{coq_example} -Restart. - cofix. -\end{coq_example} - -%\pagebreak - -\begin{coq_example} -intros. -apply eqst. -trivial. -simpl. -apply eqproof. -Qed. -\end{coq_example} - - -\section{Experiments with co-inductive types} - -Some examples involving co-inductive types are available with -the distributed system, in the theories library and in the contributions -of the Lyon site. Here we present a short description of their contents~: -\begin{itemize} -\item Directory \verb!theories/LISTS! : - \begin{itemize} - \item File \verb!Streams.v! : The type of streams and the -extensional equality between streams. - \end{itemize} - -\item Directory \verb!contrib/Lyon/COINDUCTIVES! : - \begin{itemize} - \item Directory \verb!ARITH! : An arithmetic where $\infty$ -is an explicit constant of the language instead of a metatheoretical notion. - \item Directory \verb!STREAM! : - \begin{itemize} - \item File \verb!Examples! : -Several examples of guarded definitions, as well as -of frequent errors in the introduction of a stream. A different -way of defining the extensional equality of two streams, -and the proofs showing that it is equivalent to the one in \verb!theories!. - \item File \verb!Alter.v! : An example showing how -an infinite proof introduced by a guarded definition can be also described -using an operator of co-recursion \cite{Gimenez95b}. - \end{itemize} -\item Directory \verb!PROCESSES! : A proof of the alternating -bit protocol based on Pra\-sad's Calculus of Broadcasting Systems \cite{Prasad93}, -and the verification of an interpreter for this calculus. -See \cite{Gimenez95b} for a complete description about this development. - \end{itemize} -\end{itemize} - -%\end{document} - diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index c8e2ae2dd..574591185 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1106,19 +1106,14 @@ Fail all:let n:= numgoals in guard n=2. Reset Initial. \end{coq_eval} -\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract}\comindex{Qed exporting} +\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract} \index{Tacticals!abstract@{\tt abstract}}\index{Tacticals!transparent\_abstract@{\tt transparent\_abstract}}} From the outside ``\texttt{abstract \tacexpr}'' is the same as {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the current goal and \textit{n} is chosen so that this is a fresh name. -Such auxiliary lemma is inlined in the final proof term -unless the proof is ended with ``\texttt{Qed exporting}''. In such -case the lemma is preserved. The syntax -``\texttt{Qed exporting }\ident$_1$\texttt{, ..., }\ident$_n$'' -is also supported. In such case the system checks that the names given by the -user actually exist when the proof is ended. +Such an auxiliary lemma is inlined in the final proof term. This tactical is useful with tactics such as \texttt{omega} or \texttt{discriminate} that generate huge proof terms. With that tool diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex deleted file mode 100644 index 7e5bb81a9..000000000 --- a/doc/refman/RefMan-tus.tex +++ /dev/null @@ -1,2001 +0,0 @@ -%\documentclass[11pt]{article} -%\usepackage{fullpage,euler} -%\usepackage[latin1]{inputenc} -%\begin{document} -%\title{Writing ad-hoc Tactics in Coq} -%\author{} -%\date{} -%\maketitle -%\tableofcontents -%\clearpage - -\chapter[Writing ad-hoc Tactics in Coq]{Writing ad-hoc Tactics in Coq\label{WritingTactics}} - -\section{Introduction} - -\Coq\ is an open proof environment, in the sense that the collection of -proof strategies offered by the system can be extended by the user. -This feature has two important advantages. First, the user can develop -his/her own ad-hoc proof procedures, customizing the system for a -particular domain of application. Second, the repetitive and tedious -aspects of the proofs can be abstracted away implementing new tactics -for dealing with them. For example, this may be useful when a theorem -needs several lemmas which are all proven in a similar but not exactly -the same way. Let us illustrate this with an example. - -Consider the problem of deciding the equality of two booleans. The -theorem establishing that this is always possible is state by -the following theorem: - -\begin{coq_example*} -Theorem decideBool : (x,y:bool){x=y}+{~x=y}. -\end{coq_example*} - -The proof proceeds by case analysis on both $x$ and $y$. This yields -four cases to solve. The cases $x=y=\textsl{true}$ and -$x=y=\textsl{false}$ are immediate by the reflexivity of equality. - -The other two cases follow by discrimination. The following script -describes the proof: - -\begin{coq_example*} -Destruct x. - Destruct y. - Left ; Reflexivity. - Right; Discriminate. - Destruct y. - Right; Discriminate. - Left ; Reflexivity. -\end{coq_example*} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Now, consider the theorem stating the same property but for the -following enumerated type: - -\begin{coq_example*} -Inductive Set Color := Blue:Color | White:Color | Red:Color. -Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}. -\end{coq_example*} - -This theorem can be proven in a very similar way, reasoning by case -analysis on $c_1$ and $c_2$. Once more, each of the (now six) cases is -solved either by reflexivity or by discrimination: - -\begin{coq_example*} -Destruct c1. - Destruct c2. - Left ; Reflexivity. - Right ; Discriminate. - Right ; Discriminate. - Destruct c2. - Right ; Discriminate. - Left ; Reflexivity. - Right ; Discriminate. - Destruct c2. - Right ; Discriminate. - Right ; Discriminate. - Left ; Reflexivity. -\end{coq_example*} -\begin{coq_eval} -Abort. -\end{coq_eval} - -If we face the same theorem for an enumerated datatype corresponding -to the days of the week, it would still follow a similar pattern. In -general, the general pattern for proving the property -$(x,y:R)\{x=y\}+\{\neg x =y\}$ for an enumerated type $R$ proceeds as -follow: -\begin{enumerate} -\item Analyze the cases for $x$. -\item For each of the sub-goals generated by the first step, analyze -the cases for $y$. -\item The remaining subgoals follow either by reflexivity or -by discrimination. -\end{enumerate} - -Let us describe how this general proof procedure can be introduced in -\Coq. - -\section{Tactic Macros} - -The simplest way to introduce it is to define it as new a -\textsl{tactic macro}, as follows: - -\begin{coq_example*} -Tactic Definition DecideEq [$a $b] := - [<:tactic:<Destruct $a; - Destruct $b; - (Left;Reflexivity) Orelse (Right;Discriminate)>>]. -\end{coq_example*} - -The general pattern of the proof is abstracted away using the -tacticals ``\texttt{;}'' and \texttt{Orelse}, and introducing two -parameters for the names of the arguments to be analyzed. - -Once defined, this tactic can be called like any other tactic, just -supplying the list of terms corresponding to its real arguments. Let us -revisit the proof of the former theorems using the new tactic -\texttt{DecideEq}: - -\begin{coq_example*} -Theorem decideBool : (x,y:bool){x=y}+{~x=y}. -DecideEq x y. -Defined. -\end{coq_example*} -\begin{coq_example*} -Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}. -DecideEq c1 c2. -Defined. -\end{coq_example*} - -In general, the command \texttt{Tactic Definition} associates a name -to a parameterized tactic expression, built up from the tactics and -tacticals that are already available. The general syntax rule for this -command is the following: - -\begin{tabbing} -\texttt{Tactic Definition} \textit{tactic-name} \= -\texttt{[}\$$id_1\ldots \$id_n$\texttt{]}\\ -\> := \texttt{[<:tactic:<} \textit{tactic-expression} \verb+>>]+ -\end{tabbing} - -This command provides a quick but also very primitive mechanism for -introducing new tactics. It does not support recursive definitions, -and the arguments of a tactic macro are restricted to term -expressions. Moreover, there is no static checking of the definition -other than the syntactical one. Any error in the definition of the -tactic ---for instance, a call to an undefined tactic--- will not be -noticed until the tactic is called. - -%This command provides a very primitive mechanism for introducing new -%tactics. The arguments of a tactic macro are restricted to term -%expressions. Hence, it is not possible to define higher order tactics -%with this command. Also, there is no static checking of the definition -%other than syntactical. If the tactic contain errors in its definition -%--for instance, a call to an undefined tactic-- this will be noticed -%during the tactic call. - -Let us illustrate the weakness of this way of introducing new tactics -trying to extend our proof procedure to work on a larger class of -inductive types. Consider for example the decidability of equality -for pairs of booleans and colors: - -\begin{coq_example*} -Theorem decideBoolXColor : (p1,p2:bool*Color){p1=p2}+{~p1=p2}. -\end{coq_example*} - -The proof still proceeds by a double case analysis, but now the -constructors of the type take two arguments. Therefore, the sub-goals -that can not be solved by discrimination need further considerations -about the equality of such arguments: - -\begin{coq_example} - Destruct p1; - Destruct p2; Try (Right;Discriminate);Intros. -\end{coq_example} - -The half of the disjunction to be chosen depends on whether or not -$b=b_0$ and $c=c_0$. These equalities can be decided automatically -using the previous lemmas about booleans and colors. If both -equalities are satisfied, then it is sufficient to rewrite $b$ into -$b_0$ and $c$ into $c_0$, so that the left half of the goal follows by -reflexivity. Otherwise, the right half follows by first contraposing -the disequality, and then applying the invectiveness of the pairing -constructor. - -As the cases associated to each argument of the pair are very similar, -a tactic macro can be introduced to abstract this part of the proof: - -\begin{coq_example*} -Hints Resolve decideBool decideColor. -Tactic Definition SolveArg [$t1 $t2] := - [<:tactic:< - ElimType {$t1=$t2}+{~$t1=$t2}; - [(Intro equality;Rewrite equality;Clear equality) | - (Intro diseq; Right; Red; Intro absurd; - Apply diseq;Injection absurd;Trivial) | - Auto]>>]. -\end{coq_example*} - -This tactic is applied to each corresponding pair of arguments of the -arguments, until the goal can be solved by reflexivity: - -\begin{coq_example*} -SolveArg b b0; - SolveArg c c0; - Left; Reflexivity. -Defined. -\end{coq_example*} - -Therefore, a more general strategy for deciding the property -$(x,y:R)\{x=y\}+\{\neg x =y\}$ on $R$ can be sketched as follows: -\begin{enumerate} -\item Eliminate $x$ and then $y$. -\item Try discrimination to solve those goals where $x$ and $y$ has -been introduced by different constructors. -\item If $x$ and $y$ have been introduced by the same constructor, -then iterate the tactic \textsl{SolveArg} for each pair of -arguments. -\item Finally, solve the left half of the goal by reflexivity. -\end{enumerate} - -The implementation of this stronger proof strategy needs to perform a -term decomposition, in order to extract the list of arguments of each -constructor. It also requires the introduction of recursively defined -tactics, so that the \textsl{SolveArg} can be iterated on the lists of -arguments. These features are not supported by the \texttt{Tactic -Definition} command. One possibility could be extended this command in -order to introduce recursion, general parameter passing, -pattern-matching, etc, but this would quickly lead us to introduce the -whole \ocaml{} into \Coq\footnote{This is historically true. In fact, -\ocaml{} is a direct descendent of ML, a functional programming language -conceived language for programming the tactics of the theorem prover -LCF.}. Instead of doing this, we prefer to give to the user the -possibility of writing his/her own tactics directly in \ocaml{}, and then -to link them dynamically with \Coq's code. This requires a minimal -knowledge about \Coq's implementation. The next section provides an -overview of \Coq's architecture. - -%It is important to point out that the introduction of a new tactic -%never endangers the correction of the theorems proven in the extended -%system. In order to understand why, let us introduce briefly the system -%architecture. - -\section{An Overview of \Coq's Architecture} - -The implementation of \Coq\ is based on eight \textsl{logical -modules}. By ``module'' we mean here a logical piece of code having a -conceptual unity, that may concern several \ocaml{} files. By the sake of -organization, all the \ocaml{} files concerning a logical module are -grouped altogether into the same sub-directory. The eight modules -are: - -\begin{tabular}{lll} -1. & The logical framework & (directory \texttt{src/generic})\\ -2. & The language of constructions & (directory \texttt{src/constr})\\ -3. & The type-checker & (directory \texttt{src/typing})\\ -4. & The proof engine & (directory \texttt{src/proofs})\\ -5. & The language of basic tactics & (directory \texttt{src/tactics})\\ -6. & The vernacular interpreter & (directory \texttt{src/env})\\ -7. & The parser and the pretty-printer & (directory \texttt{src/parsing})\\ -8. & The standard library & (directory \texttt{src/lib}) -\end{tabular} - -\vspace{1em} - -The following sections briefly present each of the modules above. -This presentation is not intended to be a complete description of \Coq's -implementation, but rather a guideline to be read before taking a look -at the sources. For each of the modules, we also present some of its -most important functions, which are sufficient to implement a large -class of tactics. - - -\subsection[The Logical Framework]{The Logical Framework\label{LogicalFramework}} - -At the very heart of \Coq there is a generic untyped language for -expressing abstractions, applications and global constants. This -language is used as a meta-language for expressing the terms of the -Calculus of Inductive Constructions. General operations on terms like -collecting the free variables of an expression, substituting a term for -a free variable, etc, are expressed in this language. - -The meta-language \texttt{'op term} of terms has seven main -constructors: -\begin{itemize} -\item $(\texttt{VAR}\;id)$, a reference to a global identifier called $id$; -\item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$ - binder up in the term; -\item $\texttt{DLAM}\;(x,t)$, a de Bruijn's binder on the term $t$; -\item $\texttt{DLAMV}\;(x,vt)$, a de Bruijn's binder on all the terms of - the vector $vt$; -\item $(\texttt{DOP0}\;op)$, a unary operator $op$; -\item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary -operator $op$ to the terms $t_1$ and $t_2$; -\item $\texttt{DOPN} (op,vt)$, the application of an n-ary operator $op$ to the -vector of terms $vt$. -\end{itemize} - -In this meta-language, bound variables are represented using the -so-called de Bruijn's indexes. In this representation, an occurrence of -a bound variable is denoted by an integer, meaning the number of -binders that must be traversed to reach its own -binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders -have to be traversed, since indexes are represented by strictly -positive integers.}. On the other hand, constants are referred by its -name, as usual. For example, if $A$ is a variable of the current -section, then the lambda abstraction $[x:A]x$ of the Calculus of -Constructions is represented in the meta-language by the term: - -\begin{displaymath} -(DOP2 (Lambda,(Var\;A),DLAM (x,(Rel\;1))) -\end{displaymath} - -In this term, $Lambda$ is a binary operator. Its first argument -correspond to the type $A$ of the bound variable, while the second is -a body of the abstraction, where $x$ is bound. The name $x$ is just kept -to pretty-print the occurrences of the bound variable. - -%Similarly, the product -%$(A:Prop)A$ of the Calculus of Constructions is represented by the -%term: -%\begin{displaumath} -%DOP2 (Prod, DOP0 (Sort (Prop Null)), DLAM (Name \#A, Rel 1)) -%\end{displaymath} - -The following functions perform some of the most frequent operations -on the terms of the meta-language: -\begin{description} -\fun{val Generic.subst1 : 'op term -> 'op term -> 'op term} - {$(\texttt{subst1}\;t_1\;t_2)$ substitutes $t_1$ for - $\texttt{(Rel}\;1)$ in $t_2$.} -\fun{val Generic.occur\_var : identifier -> 'op term -> bool} - {Returns true when the given identifier appears in the term, - and false otherwise.} -\fun{val Generic.eq\_term : 'op term -> 'op term -> bool} - {Implements $\alpha$-equality for terms.} -\fun{val Generic.dependent : 'op term -> 'op term -> bool} - {Returns true if the first term is a sub-term of the second.} -%\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term} -% { $(\texttt{subst\_var}\;id\;t)$ substitutes the de Bruijn's index -% associated to $id$ to every occurrence of the term -% $(\texttt{VAR}\;id)$ in $t$.} -\end{description} - -\subsubsection{Identifiers, names and sections paths.} - -Three different kinds of names are used in the meta-language. They are -all defined in the \ocaml{} file \texttt{Names}. - -\paragraph{Identifiers.} The simplest kind of names are -\textsl{identifiers}. An identifier is a string possibly indexed by an -integer. They are used to represent names that are not unique, like -for example the name of a variable in the scope of a section. The -following operations can be used for handling identifiers: - -\begin{description} -\fun{val Names.make\_ident : string -> int -> identifier} - {The value $(\texttt{make\_ident}\;x\;i)$ creates the - identifier $x_i$. If $i=-1$, then the identifier has - is created with no index at all.} -\fun{val Names.repr\_ident : identifier -> string * int} - {The inverse operation of \texttt{make\_ident}: - it yields the string and the index of the identifier.} -\fun{val Names.lift\_ident : identifier -> identifier} - {Increases the index of the identifier by one.} -\fun{val Names.next\_ident\_away : \\ -\qquad identifier -> identifier list -> identifier} - {\\ Generates a new identifier with the same root string than the - given one, but with a new index, different from all the indexes of - a given list of identifiers.} -\fun{val Names.id\_of\_string : string -> - identifier} - {Creates an identifier from a string.} -\fun{val Names.string\_of\_id : identifier -> string} - {The inverse operation: transforms an identifier into a string} -\end{description} - -\paragraph{Names.} A \textsl{name} is either an identifier or the -special name \texttt{Anonymous}. Names are used as arguments of -binders, in order to pretty print bound variables. -The following operations can be used for handling names: - -\begin{description} -\fun{val Names.Name: identifier -> Name} - {Constructs a name from an identifier.} -\fun{val Names.Anonymous : Name} - {Constructs a special, anonymous identifier, like the variable abstracted - in the term $[\_:A]0$.} -\fun{val - Names.next\_name\_away\_with\_default : \\ \qquad - string->name->identifier list->identifier} -{\\ If the name is not anonymous, then this function generates a new - identifier different from all the ones in a given list. Otherwise, it - generates an identifier from the given string.} -\end{description} - -\paragraph[Section paths.]{Section paths.\label{SectionPaths}} -A \textsl{section-path} is a global name to refer to an object without -ambiguity. It can be seen as a sort of filename, where open sections -play the role of directories. Each section path is formed by three -components: a \textsl{directory} (the list of open sections); a -\textsl{basename} (the identifier for the object); and a \textsl{kind} -(either CCI for the terms of the Calculus of Constructions, FW for the -the terms of $F_\omega$, or OBJ for other objects). For example, the -name of the following constant: -\begin{verbatim} - Section A. - Section B. - Section C. - Definition zero := O. -\end{verbatim} - -is internally represented by the section path: - -$$\underbrace{\mathtt{\#A\#B\#C}}_{\mbox{dirpath}} -\underbrace{\mathtt{\tt \#zero}}_{\mbox{basename}} -\underbrace{\mathtt{\tt .cci}_{\;}}_{\mbox{kind}}$$ - -When one of the sections is closed, a new constant is created with an -updated section-path,a nd the old one is no longer reachable. In our -example, after closing the section \texttt{C}, the new section-path -for the constant {\tt zero} becomes: -\begin{center} -\texttt{ \#A\#B\#zero.cci} -\end{center} - -The following operations can be used to handle section paths: - -\begin{description} -\fun{val Names.string\_of\_path : section\_path -> string} - {Transforms the section path into a string.} -\fun{val Names.path\_of\_string : string -> section\_path} - {Parses a string an returns the corresponding section path.} -\fun{val Names.basename : section\_path -> identifier} - {Provides the basename of a section path} -\fun{val Names.dirpath : section\_path -> string list} - {Provides the directory of a section path} -\fun{val Names.kind\_of\_path : section\_path -> path\_kind} - {Provides the kind of a section path} -\end{description} - -\subsubsection{Signatures} - -A \textsl{signature} is a mapping associating different informations -to identifiers (for example, its type, its definition, etc). The -following operations could be useful for working with signatures: - -\begin{description} -\fun{val Names.ids\_of\_sign : 'a signature -> identifier list} - {Gets the list of identifiers of the signature.} -\fun{val Names.vals\_of\_sign : 'a signature -> 'a list} - {Gets the list of values associated to the identifiers of the signature.} -\fun{val Names.lookup\_glob1 : \\ \qquad -identifier -> 'a signature -> (identifier * - 'a)} - {\\ Gets the value associated to a given identifier of the signature.} -\end{description} - - -\subsection{The Terms of the Calculus of Constructions} - -The language of the Calculus of Inductive Constructions described in -Chapter \ref{Cic} is implemented on the top of the logical framework, -instantiating the parameter $op$ of the meta-language with a -particular set of operators. In the implementation this language is -called \texttt{constr}, the language of constructions. - -% The only difference -%with respect to the one described in Section \ref{} is that the terms -%of \texttt{constr} may contain \textsl{existential variables}. An -%existential variable is a place holder representing a part of the term -%that is still to be constructed. Such ``open terms'' are necessary -%when building proofs interactively. - -\subsubsection{Building Constructions} - -The user does not need to know the choices made to represent -\texttt{constr} in the meta-language. They are abstracted away by the -following constructor functions: - -\begin{description} -\fun{val Term.mkRel : int -> constr} - {$(\texttt{mkRel}\;n)$ represents de Bruijn's index $n$.} - -\fun{val Term.mkVar : identifier -> constr} - {$(\texttt{mkVar}\;id)$ - represents a global identifier named $id$, like a variable - inside the scope of a section, or a hypothesis in a proof}. - -\fun{val Term.mkExistential : constr} - {\texttt{mkExistential} represents an implicit sub-term, like the question - marks in the term \texttt{(pair ? ? O true)}.} - -%\fun{val Term.mkMeta : int -> constr} -% {$(\texttt{mkMeta}\;n)$ represents an existential variable, whose -% name is the integer $n$.} - -\fun{val Term.mkProp : constr} - {$\texttt{mkProp}$ represents the sort \textsl{Prop}.} - -\fun{val Term.mkSet : constr} - {$\texttt{mkSet}$ represents the sort \textsl{Set}.} - -\fun{val Term.mkType : Impuniv.universe -> constr} - {$(\texttt{mkType}\;u)$ represents the term - $\textsl{Type}(u)$. The universe $u$ is represented as a - section path indexed by an integer. } - -\fun{val Term.mkConst : section\_path -> constr array -> constr} - {$(\texttt{mkConst}\;c\;v)$ represents a constant whose name is - $c$. The body of the constant is stored in a global table, - accessible through the name of the constant. The array of terms - $v$ corresponds to the variables of the environment appearing in - the body of the constant when it was defined. For instance, a - constant defined in the section \textsl{Foo} containing the - variable $A$, and whose body is $[x:Prop\ra Prop](x\;A)$ is - represented inside the scope of the section by - $(\texttt{mkConst}\;\texttt{\#foo\#f.cci}\;[| \texttt{mkVAR}\;A - |])$. Once the section is closed, the constant is represented by - the term $(\texttt{mkConst}\;\#f.cci\;[| |])$, and its body - becomes $[A:Prop][x:Prop\ra Prop](x\;A)$}. - -\fun{val Term.mkMutInd : section\_path -> int -> constr array ->constr} - {$(\texttt{mkMutInd}\;c\;i)$ represents the $ith$ type - (starting from zero) of the block of mutually dependent - (co)inductive types, whose first type is $c$. Similarly to the - case of constants, the array of terms represents the current - environment of the (co)inductive type. The definition of the type - (its arity, its constructors, whether it is inductive or co-inductive, etc.) - is stored in a global hash table, accessible through the name of - the type.} - -\fun{val Term.mkMutConstruct : \\ \qquad section\_path -> int -> int -> constr array - ->constr} {\\ $(\texttt{mkMutConstruct}\;c\;i\;j)$ represents the - $jth$ constructor of the $ith$ type of the block of mutually - dependent (co)inductive types whose first type is $c$. The array - of terms represents the current environment of the (co)inductive - type.} - -\fun{val Term.mkCast : constr -> constr -> constr} - {$(\texttt{mkCast}\;t\;T)$ represents the annotated term $t::T$ in - \Coq's syntax.} - -\fun{val Term.mkProd : name ->constr ->constr -> constr} - {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$. - The free ocurrences of $x$ in $B$ are represented by de Bruijn's - indexes.} - -\fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr} - {$(\texttt{produit}\;x\;A\;B)$ represents the product $(x:A)B$, - but the bound occurrences of $x$ in $B$ are denoted by - the identifier $(\texttt{mkVar}\;x)$. The function automatically - changes each occurrences of this identifier into the corresponding - de Bruijn's index.} - -\fun{val Term.mkArrow : constr -> constr -> constr} - {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.} - -\fun{val Term.mkLambda : name -> constr -> constr -> constr} - {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction - $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by de Bruijn's - indexes.} - -\fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr} - {$(\texttt{lambda}\;x\;A\;b)$ represents the lambda abstraction - $[x:A]b$, but the bound occurrences of $x$ in $B$ are denoted by - the identifier $(\texttt{mkVar}\;x)$. } - -\fun{val Term.mkAppLA : constr array -> constr} - {$(\texttt{mkAppLA}\;t\;[|t_1\ldots t_n|])$ represents the application - $(t\;t_1\;\ldots t_n)$.} - -\fun{val Term.mkMutCaseA : \\ \qquad - case\_info -> constr ->constr - ->constr array -> constr} - {\\ $(\texttt{mkMutCaseA}\;r\;P\;m\;[|f_1\ldots f_n|])$ - represents the term \Case{P}{m}{f_1\ldots f_n}. The first argument - $r$ is either \texttt{None} or $\texttt{Some}\;(c,i)$, where the - pair $(c,i)$ refers to the inductive type that $m$ belongs to.} - -\fun{val Term.mkFix : \\ \qquad -int array->int->constr array->name - list->constr array->constr} - {\\ $(\texttt{mkFix}\;[|k_1\ldots k_n |]\;i\;[|A_1\ldots - A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term - $\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}$} - -\fun{val Term.mkCoFix : \\ \qquad - int -> constr array -> name list -> - constr array -> constr} - {\\ $(\texttt{mkCoFix}\;i\;[|A_1\ldots - A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term - $\CoFix{f_i}{f_1:A_1:=t_1 \ldots f_n:A_n:=t_n}$. There are no - decreasing indexes in this case.} -\end{description} - -\subsubsection{Decomposing Constructions} - -Each of the construction functions above has its corresponding -(partial) destruction function, whose name is obtained changing the -prefix \texttt{mk} by \texttt{dest}. In addition to these functions, a -concrete datatype \texttt{kindOfTerm} can be used to do pattern -matching on terms without dealing with their internal representation -in the meta-language. This concrete datatype is described in the \ocaml{} -file \texttt{term.mli}. The following function transforms a construction -into an element of type \texttt{kindOfTerm}: - -\begin{description} -\fun{val Term.kind\_of\_term : constr -> kindOfTerm} - {Destructs a term of the language \texttt{constr}, -yielding the direct components of the term. Hence, in order to do -pattern matching on an object $c$ of \texttt{constr}, it is sufficient -to do pattern matching on the value $(\texttt{kind\_of\_term}\;c)$.} -\end{description} - -Part of the information associated to the constants is stored in -global tables. The following functions give access to such -information: - -\begin{description} -\fun{val Termenv.constant\_value : constr -> constr} - {If the term denotes a constant, projects the body of a constant} -\fun{Termenv.constant\_type : constr -> constr} - {If the term denotes a constant, projects the type of the constant} -\fun{val mind\_arity : constr -> constr} - {If the term denotes an inductive type, projects its arity (i.e., - the type of the inductive type).} -\fun{val Termenv.mis\_is\_finite : mind\_specif -> bool} - {Determines whether a recursive type is inductive or co-inductive.} -\fun{val Termenv.mind\_nparams : constr -> int} - {If the term denotes an inductive type, projects the number of - its general parameters.} -\fun{val Termenv.mind\_is\_recursive : constr -> bool} - {If the term denotes an inductive type, - determines if the type has at least one recursive constructor. } -\fun{val Termenv.mind\_recargs : constr -> recarg list array array} - {If the term denotes an inductive type, returns an array $v$ such - that the nth element of $v.(i).(j)$ is - \texttt{Mrec} if the $nth$ argument of the $jth$ constructor of - the $ith$ type is recursive, and \texttt{Norec} if it is not.}. -\end{description} - -\subsection[The Type Checker]{The Type Checker\label{TypeChecker}} - -The third logical module is the type checker. It concentrates two main -tasks concerning the language of constructions. - -On one hand, it contains the type inference and type-checking -functions. The type inference function takes a term -$a$ and a signature $\Gamma$, and yields a term $A$ such that -$\Gamma \vdash a:A$. The type-checking function takes two terms $a$ -and $A$ and a signature $\Gamma$, and determines whether or not -$\Gamma \vdash a:A$. - -On the other hand, this module is in charge of the compilation of -\Coq's abstract syntax trees into the language \texttt{constr} of -constructions. This compilation seeks to eliminate all the ambiguities -contained in \Coq's abstract syntax, restoring the information -necessary to type-check it. It concerns at least the following steps: -\begin{enumerate} -\item Compiling the pattern-matching expressions containing -constructor patterns, wild-cards, etc, into terms that only -use the primitive \textsl{Case} described in Chapter \ref{Cic} -\item Restoring type coercions and synthesizing the implicit arguments -(the one denoted by question marks in -{\Coq} syntax: see Section~\ref{Coercions}). -\item Transforming the named bound variables into de Bruijn's indexes. -\item Classifying the global names into the different classes of -constants (defined constants, constructors, inductive types, etc). -\end{enumerate} - -\subsection{The Proof Engine} - -The fourth stage of \Coq's implementation is the \textsl{proof engine}: -the interactive machine for constructing proofs. The aim of the proof -engine is to construct a top-down derivation or \textsl{proof tree}, -by the application of \textsl{tactics}. A proof tree has the following -general structure:\\ - -\begin{displaymath} -\frac{\Gamma \vdash ? = t(?_1,\ldots?_n) : G} - {\hspace{3ex}\frac{\displaystyle \Gamma_1 \vdash ?_1 = t_1(\ldots) : G_1} - {\stackrel{\vdots}{\displaystyle {\Gamma_{i_1} \vdash ?_{i_1} - : G_{i_1}}}}(tac_1) - \;\;\;\;\;\;\;\;\; - \frac{\displaystyle \Gamma_n \vdash ?_n = t_n(\ldots) : G_n} - {\displaystyle \stackrel{\vdots}{\displaystyle {\Gamma_{i_m} \vdash ?_{i_m} : - G_{i_m}}}}(tac_n)} (tac) -\end{displaymath} - - -\noindent Each node of the tree is called a \textsl{goal}. A goal -is a record type containing the following three fields: -\begin{enumerate} -\item the conclusion $G$ to be proven; -\item a typing signature $\Gamma$ for the free variables in $G$; -\item if the goal is an internal node of the proof tree, the -definition $t(?_1,\ldots?_n)$ of an \textsl{existential variable} -(i.e. a possible undefined constant) $?$ of type $G$ in terms of the -existential variables of the children sub-goals. If the node is a -leaf, the existential variable maybe still undefined. -\end{enumerate} - -Once all the existential variables have been defined the derivation is -completed, and a construction can be generated from the proof tree, -replacing each of the existential variables by its definition. This -is exactly what happens when one of the commands -\texttt{Qed} or \texttt{Defined} is invoked -(see Section~\ref{Qed}). The saved theorem becomes a defined constant, -whose body is the proof object generated. - -\paragraph{Important:} Before being added to the -context, the proof object is type-checked, in order to verify that it is -actually an object of the expected type $G$. Hence, the correctness -of the proof actually does not depend on the tactics applied to -generate it or the machinery of the proof engine, but only on the -type-checker. In other words, extending the system with a potentially -bugged new tactic never endangers the consistency of the system. - -\subsubsection[What is a Tactic?]{What is a Tactic?\label{WhatIsATactic}} -%Let us now explain what is a tactic, and how the user can introduce -%new ones. - -From an operational point of view, the current state of the proof -engine is given by the mapping $emap$ from existential variables into -goals, plus a pointer to one of the leaf goals $g$. Such a pointer -indicates where the proof tree will be refined by the application of a -\textsl{tactic}. A tactic is a function from the current state -$(g,emap)$ of the proof engine into a pair $(l,val)$. The first -component of this pair is the list of children sub-goals $g_1,\ldots -g_n$ of $g$ to be yielded by the tactic. The second one is a -\textsl{validation function}. Once the proof trees $\pi_1,\ldots -\pi_n$ for $g_1,\ldots g_n$ have been completed, this validation -function must yield a proof tree $(val\;\pi_1,\ldots \pi_n)$ deriving -$g$. - -Tactics can be classified into \textsl{primitive} ones and -\textsl{defined} ones. Primitive tactics correspond to the five basic -operations of the proof engine: - -\begin{enumerate} -\item Introducing a universally quantified variable into the local -context of the goal. -\item Defining an undefined existential variable -\item Changing the conclusion of the goal for another ---definitionally equal-- term. -\item Changing the type of a variable in the local context for another -definitionally equal term. -\item Erasing a variable from the local context. -\end{enumerate} - -\textsl{Defined} tactics are tactics constructed by combining these -primitive operations. Defined tactics are registered in a hash table, -so that they can be introduced dynamically. In order to define such a -tactic table, it is necessary to fix what a \textsl{possible argument} -of a tactic may be. The type \texttt{tactic\_arg} of the possible -arguments for tactics is a union type including: -\begin{itemize} -\item quoted strings; -\item integers; -\item identifiers; -\item lists of identifiers; -\item plain terms, represented by its abstract syntax tree; -\item well-typed terms, represented by a construction; -\item a substitution for bound variables, like the -substitution in the tactic \\$\texttt{Apply}\;t\;\texttt{with}\;x:=t_1\ldots -x_n:=t_n$, (see Section~\ref{apply}); -\item a reduction expression, denoting the reduction strategy to be -followed. -\end{itemize} -Therefore, for each function $tac:a \rightarrow tactic$ implementing a -defined tactic, an associated dynamic tactic $tacargs\_tac: -\texttt{tactic\_arg}\;list \rightarrow tactic$ calling $tac$ must be -written. The aim of the auxiliary function $tacargs\_tac$ is to inject -the arguments of the tactic $tac$ into the type of possible arguments -for a tactic. - -The following function can be used for registering and calling a -defined tactic: - -\begin{description} -\fun{val Tacmach.add\_tactic : \\ \qquad -string -> (tactic\_arg list ->tactic) -> unit} - {\\ Registers a dynamic tactic with the given string as access index.} -\fun{val Tacinterp.vernac\_tactic : string*tactic\_arg list -> tactic} - {Interprets a defined tactic given by its entry in the - tactics table with a particular list of possible arguments.} -\fun{val Tacinterp.vernac\_interp : CoqAst.t -> tactic} - {Interprets a tactic expression formed combining \Coq's tactics and - tacticals, and described by its abstract syntax tree.} -\end{description} - -When programming a new tactic that calls an already defined tactic -$tac$, we have the choice between using the \ocaml{} function -implementing $tac$, or calling the tactic interpreter with the name -and arguments for interpreting $tac$. In the first case, a tactic call -will left the trace of the whole implementation of $tac$ in the proof -tree. In the second, the implementation of $tac$ will be hidden, and -only an invocation of $tac$ will be recalled (cf. the example of -Section \ref{ACompleteExample}. The following combinators can be used -to hide the implementation of a tactic: - -\begin{verbatim} -type 'a hiding_combinator = string -> ('a -> tactic) -> ('a -> tactic) -val Tacmach.hide_atomic_tactic : string -> tactic -> tactic -val Tacmach.hide_constr_tactic : constr hiding_combinator -val Tacmach.hide_constrl_tactic : (constr list) hiding_combinator -val Tacmach.hide_numarg_tactic : int hiding_combinator -val Tacmach.hide_ident_tactic : identifier hiding_combinator -val Tacmach.hide_identl_tactic : identifier hiding_combinator -val Tacmach.hide_string_tactic : string hiding_combinator -val Tacmach.hide_bindl_tactic : substitution hiding_combinator -val Tacmach.hide_cbindl_tactic : - (constr * substitution) hiding_combinator -\end{verbatim} - -These functions first register the tactic by a side effect, and then -yield a function calling the interpreter with the registered name and -the right injection into the type of possible arguments. - -\subsection{Tactics and Tacticals Provided by \Coq} - -The fifth logical module is the library of tacticals and basic tactics -provided by \Coq. This library is distributed into the directories -\texttt{tactics} and \texttt{src/tactics}. The former contains those -basic tactics that make use of the types contained in the basic state -of \Coq. For example, inversion or rewriting tactics are in the -directory \texttt{tactics}, since they make use of the propositional -equality type. Those tactics which are independent from the context ---like for example \texttt{Cut}, \texttt{Intros}, etc-- are defined in -the directory \texttt{src/tactics}. This latter directory also -contains some useful tools for programming new tactics, referred in -Section \ref{SomeUsefulToolsforWrittingTactics}. - -In practice, it is very unusual that the list of sub-goals and the -validation function of the tactic must be explicitly constructed by -the user. In most of the cases, the implementation of a new tactic -consists in supplying the appropriate arguments to the basic tactics -and tacticals. - -\subsubsection{Basic Tactics} - -The file \texttt{Tactics} contain the implementation of the basic -tactics provided by \Coq. The following tactics are some of the most -used ones: - -\begin{verbatim} -val Tactics.intro : tactic -val Tactics.assumption : tactic -val Tactics.clear : identifier list -> tactic -val Tactics.apply : constr -> constr substitution -> tactic -val Tactics.one_constructor : int -> constr substitution -> tactic -val Tactics.simplest_elim : constr -> tactic -val Tactics.elimType : constr -> tactic -val Tactics.simplest_case : constr -> tactic -val Tactics.caseType : constr -> tactic -val Tactics.cut : constr -> tactic -val Tactics.reduce : redexpr -> tactic -val Tactics.exact : constr -> tactic -val Auto.auto : int option -> tactic -val Auto.trivial : tactic -\end{verbatim} - -The functions hiding the implementation of these tactics are defined -in the module \texttt{Hiddentac}. Their names are prefixed by ``h\_''. - -\subsubsection[Tacticals]{Tacticals\label{OcamlTacticals}} - -The following tacticals can be used to combine already existing -tactics: - -\begin{description} -\fun{val Tacticals.tclIDTAC : tactic} - {The identity tactic: it leaves the goal as it is.} - -\fun{val Tacticals.tclORELSE : tactic -> tactic -> tactic} - {Tries the first tactic and in case of failure applies the second one.} - -\fun{val Tacticals.tclTHEN : tactic -> tactic -> tactic} - {Applies the first tactic and then the second one to each generated subgoal.} - -\fun{val Tacticals.tclTHENS : tactic -> tactic list -> tactic} - {Applies a tactic, and then applies each tactic of the tactic list to the - corresponding generated subgoal.} - -\fun{val Tacticals.tclTHENL : tactic -> tactic -> tactic} - {Applies the first tactic, and then applies the second one to the last - generated subgoal.} - -\fun{val Tacticals.tclREPEAT : tactic -> tactic} - {If the given tactic succeeds in producing a subgoal, then it - is recursively applied to each generated subgoal, - and so on until it fails. } - -\fun{val Tacticals.tclFIRST : tactic list -> tactic} - {Tries the tactics of the given list one by one, until one of them - succeeds.} - -\fun{val Tacticals.tclTRY : tactic -> tactic} - {Tries the given tactic and in case of failure applies the {\tt - tclIDTAC} tactical to the original goal.} - -\fun{val Tacticals.tclDO : int -> tactic -> tactic} - {Applies the tactic a given number of times.} - -\fun{val Tacticals.tclFAIL : tactic} - {The always failing tactic: it raises a {\tt UserError} exception.} - -\fun{val Tacticals.tclPROGRESS : tactic -> tactic} - {Applies the given tactic to the current goal and fails if the - tactic leaves the goal unchanged} - -\fun{val Tacticals.tclNTH\_HYP : int -> (constr -> tactic) -> tactic} - {Applies a tactic to the nth hypothesis of the local context. - The last hypothesis introduced correspond to the integer 1.} - -\fun{val Tacticals.tclLAST\_HYP : (constr -> tactic) -> tactic} - {Applies a tactic to the last hypothesis introduced.} - -\fun{val Tacticals.tclCOMPLETE : tactic -> tactic} - {Applies a tactic and fails if the tactic did not solve completely the - goal} - -\fun{val Tacticals.tclMAP : ('a -> tactic) -> 'a list -> tactic} - {Applied to the function \texttt{f} and the list \texttt{[x\_1; - ... ; x\_n]}, this tactical applies the tactic - \texttt{tclTHEN (f x1) (tclTHEN (f x2) ... ))))}} - -\fun{val Tacicals.tclIF : (goal sigma -> bool) -> tactic -> tactic -> tactic} - {If the condition holds, apply the first tactic; otherwise, - apply the second one} - -\end{description} - - -\subsection{The Vernacular Interpreter} - -The sixth logical module of the implementation corresponds to the -interpreter of the vernacular phrases of \Coq. These phrases may be -expressions from the \gallina{} language (definitions), general -directives (setting commands) or tactics to be applied by the proof -engine. - -\subsection[The Parser and the Pretty-Printer]{The Parser and the Pretty-Printer\label{PrettyPrinter}} - -The last logical module is the parser and pretty printer of \Coq, -which is the interface between the vernacular interpreter and the -user. They translate the chains of characters entered at the input -into abstract syntax trees, and vice versa. Abstract syntax trees are -represented by labeled n-ary trees, and its type is called -\texttt{CoqAst.t}. For instance, the abstract syntax tree associated -to the term $[x:A]x$ is: - -\begin{displaymath} -\texttt{Node} - ((0,6), "LAMBDA", - [\texttt{Nvar}~((3, 4),"A");~\texttt{Slam}~((0,6),~Some~"x",~\texttt{Nvar}~((5,6),"x"))]) -\end{displaymath} - -The numbers correspond to \textsl{locations}, used to point to some -input line and character positions in the error messages. As it was -already explained in Section \ref{TypeChecker}, this term is then -translated into a construction term in order to be typed. - -The parser of \Coq\ is implemented using \camlpppp. The lexer and the data -used by \camlpppp\ to generate the parser lay in the directory -\texttt{src/parsing}. This directory also contains \Coq's -pretty-printer. The printing rules lay in the directory -\texttt{src/syntax}. The different entries of the grammar are -described in the module \texttt{Pcoq.Entry}. Let us present here two -important functions of this logical module: - -\begin{description} -\fun{val Pcoq.parse\_string : 'a Grammar.Entry.e -> string -> 'a} - {Parses a given string, trying to recognize a phrase - corresponding to some entry in the grammar. If it succeeds, - it yields a value associated to the grammar entry. For example, - applied to the entry \texttt{Pcoq.Command.command}, this function - parses a term of \Coq's language, and yields a value of type - \texttt{CoqAst.t}. When applied to the entry - \texttt{Pcoq.Vernac.vernac}, it parses a vernacular command and - returns the corresponding Ast.} -\fun{val gentermpr : \\ \qquad -path\_kind -> constr assumptions -> constr -> std\_ppcmds} - {\\ Pretty-prints a well-typed term of certain kind (cf. Section - \ref{SectionPaths}) under its context of typing assumption.} -\fun{val gentacpr : CoqAst.t -> std\_ppcmds} - {Pretty-prints a given abstract syntax tree representing a tactic - expression.} -\end{description} - -\subsection{The General Library} - -In addition to the ones laying in the standard library of \ocaml{}, -several useful modules about lists, arrays, sets, mappings, balanced -trees, and other frequently used data structures can be found in the -directory \texttt{lib}. Before writing a new one, check if it is not -already there! - -\subsubsection{The module \texttt{Std}} -This module in the directory \texttt{src/lib/util} is opened by almost -all modules of \Coq{}. Among other things, it contains a definition of -the different kinds of errors used in \Coq{} : - -\begin{description} -\fun{exception UserError of string * std\_ppcmds} - {This is the class of ``users exceptions''. Such errors arise when - the user attempts to do something illegal, for example \texttt{Intro} - when the current goal conclusion is not a product.} - -\fun{val Std.error : string -> 'a} - {For simple error messages} -\fun{val Std.user_err : ?loc:Loc.t -> string -> std\_ppcmds -> 'a} - {See Section~\ref{PrettyPrinter} : this can be used if the user - want to display a term or build a complex error message} - -\fun{exception Anomaly of string * std\_ppcmds} - {This for reporting bugs or things that should not - happen. The tacticals \texttt{tclTRY} and - \texttt{tclTRY} described in Section~\ref{OcamlTacticals} catch the - exceptions of type \texttt{UserError}, but they don't catch the - anomalies. So, in your code, don't raise any anomaly, unless you - know what you are doing. We also recommend to avoid constructs - such as \texttt{try ... with \_ -> ...} : such constructs can trap - an anomaly and make the debugging process harder.} - -\fun{val Std.anomaly : string -> 'a}{} -\fun{val Std.anomalylabstrm : string -> std\_ppcmds -> 'a}{} -\end{description} - -\section{The tactic writer mini-HOWTO} - -\subsection{How to add a vernacular command} - -The command to register a vernacular command can be found -in module \texttt{Vernacinterp}: - -\begin{verbatim} -val vinterp_add : string * (vernac_arg list -> unit -> unit) -> unit;; -\end{verbatim} - -The first argument is the name, the second argument is a function that -parses the arguments and returns a function of type -\texttt{unit}$\rightarrow$\texttt{unit} that do the job. - -In this section we will show how to add a vernacular command -\texttt{CheckCheck} that print a type of a term and the type of its -type. - -File \texttt{dcheck.ml}: - -\begin{verbatim} -open Vernacinterp;; -open Trad;; -let _ = - vinterp_add - ("DblCheck", - function [VARG_COMMAND com] -> - (fun () -> - let evmap = Evd.mt_evd () - and sign = Termenv.initial_sign () in - let {vAL=c;tYP=t;kIND=k} = - fconstruct_with_univ evmap sign com in - Pp.mSGNL [< Printer.prterm c; 'sTR ":"; - Printer.prterm t; 'sTR ":"; - Printer.prterm k >] ) - | _ -> bad_vernac_args "DblCheck") -;; -\end{verbatim} - -Like for a new tactic, a new syntax entry must be created. - -File \texttt{DCheck.v}: - -\begin{verbatim} -Declare ML Module "dcheck.ml". - -Grammar vernac vernac := - dblcheck [ "CheckCheck" comarg($c) ] -> [(DblCheck $c)]. -\end{verbatim} - -We are now able to test our new command: - -\begin{verbatim} -Coq < Require DCheck. -Coq < CheckCheck O. -O:nat:Set -\end{verbatim} - -Most Coq vernacular commands are registered in the module - \verb+src/env/vernacentries.ml+. One can see more examples here. - -\subsection{How to keep a hashtable synchronous with the reset mechanism} - -This is far more tricky. Some vernacular commands modify some -sort of state (for example by adding something in a hashtable). One -wants that \texttt{Reset} has the expected behavior with this -commands. - -\Coq{} provides a general mechanism to do that. \Coq{} environments -contains objects of three kinds: CCI, FW and OBJ. CCI and FW are for -constants of the calculus. OBJ is a dynamically extensible datatype -that contains sections, tactic definitions, hints for auto, and so -on. - -The simplest example of use of such a mechanism is in file -\verb+src/proofs/macros.ml+ (which implements the \texttt{Tactic - Definition} command). Tactic macros are stored in the imperative -hashtable \texttt{mactab}. There are two functions freeze and unfreeze -to make a copy of the table and to restore the state of table from the -copy. Then this table is declared using \texttt{Library.declare\_summary}. - -What does \Coq{} with that ? \Coq{} defines synchronization points. -At each synchronisation point, the declared tables are frozen (that -is, a copy of this tables is stored). - -When \texttt{Reset }$i$ is called, \Coq{} goes back to the first -synchronisation point that is above $i$ and ``replays'' all objects -between that point -and $i$. It will re-declare constants, re-open section, etc. - -So we need to declare a new type of objects, TACTIC-MACRO-DATA. To -``replay'' on object of that type is to add the corresponding tactic -macro to \texttt{mactab} - -So, now, we can say that \texttt{mactab} is synchronous with the Reset -mechanism$^{\mathrm{TM}}$. - -Notice that this works for hash tables but also for a single integer -(the Undo stack size, modified by the \texttt{Set Undo} command, for -example). - -\subsection{The right way to access to Coq constants from your ML code} - -With their long names, Coq constants are stored using: - -\begin{itemize} -\item a section path -\item an identifier -\end{itemize} - -The identifier is exactly the identifier that is used in \Coq{} to -denote the constant; the section path can be known using the -\texttt{Locate} command: - -\begin{coq_example} - Locate S. - Locate nat. - Locate eq. -\end{coq_example} - -Now it is easy to get a constant by its name and section path: - - -\begin{verbatim} -let constant sp id = - Machops.global_reference (Names.gLOB (Termenv.initial_sign ())) - (Names.path_of_string sp) (Names.id_of_string id);; -\end{verbatim} - - -The only issue is that if one cannot put: - - -\begin{verbatim} -let coq_S = constant "#Datatypes#nat.cci" "S";; -\end{verbatim} - - -in his tactic's code. That is because this sentence is evaluated -\emph{before} the module \texttt{Datatypes} is loaded. The solution is -to use the lazy evaluation of \ocaml{}: - - -\begin{verbatim} -let coq_S = lazy (constant "#Datatypes#nat.cci" "S");; - -... (Lazy.force coq_S) ... -\end{verbatim} - - -Be sure to call always Lazy.force behind a closure -- i.e. inside a -function body or behind the \texttt{lazy} keyword. - -One can see examples of that technique in the source code of \Coq{}, -for example -\verb+plugins/omega/coq_omega.ml+. - -\section[Some Useful Tools for Writing Tactics]{Some Useful Tools for Writing Tactics\label{SomeUsefulToolsforWrittingTactics}} -When the implementation of a tactic is not a straightforward -combination of tactics and tacticals, the module \texttt{Tacmach} -provides several useful functions for handling goals, calling the -type-checker, parsing terms, etc. This module is intended to be -the interface of the proof engine for the user. - -\begin{description} -\fun{val Tacmach.pf\_hyps : goal sigma -> constr signature} - {Projects the local typing context $\Gamma$ from a given goal $\Gamma\vdash ?:G$.} -\fun{val pf\_concl : goal sigma -> constr} - {Projects the conclusion $G$ from a given goal $\Gamma\vdash ?:G$.} -\fun{val Tacmach.pf\_nth\_hyp : goal sigma -> int -> identifier * - constr} - {Projects the $ith$ typing constraint $x_i:A_i$ from the local - context of the given goal.} -\fun{val Tacmach.pf\_fexecute : goal sigma -> constr -> judgement} - {Given a goal whose local context is $\Gamma$ and a term $a$, this - function infers a type $A$ and a kind $K$ such that the judgement - $a:A:K$ is valid under $\Gamma$, or raises an exception if there - is no such judgement. A judgement is just a record type containing - the three terms $a$, $A$ and $K$.} -\fun{val Tacmach.pf\_infexecute : \\ - \qquad -goal sigma -> constr -> judgement * information} - {\\ In addition to the typing judgement, this function also extracts - the $F_{\omega}$ program underlying the term.} -\fun{val Tacmach.pf\_type\_of : goal sigma -> constr -> constr} - {Infers a term $A$ such that $\Gamma\vdash a:A$ for a given term - $a$, where $\Gamma$ is the local typing context of the goal.} -\fun{val Tacmach.pf\_check\_type : goal sigma -> constr -> constr -> bool} - {This function yields a type $A$ if the two given terms $a$ and $A$ verify $\Gamma\vdash - a:A$ in the local typing context $\Gamma$ of the goal. Otherwise, - it raises an exception.} -\fun{val Tacmach.pf\_constr\_of\_com : goal sigma -> CoqAst.t -> constr} - {Transforms an abstract syntax tree into a well-typed term of the - language of constructions. Raises an exception if the term cannot - be typed.} -\fun{val Tacmach.pf\_constr\_of\_com\_sort : goal sigma -> CoqAst.t -> constr} - {Transforms an abstract syntax tree representing a type into - a well-typed term of the language of constructions. Raises an - exception if the term cannot be typed.} -\fun{val Tacmach.pf\_parse\_const : goal sigma -> string -> constr} - {Constructs the constant whose name is the given string.} -\fun{val -Tacmach.pf\_reduction\_of\_redexp : \\ - \qquad goal sigma -> red\_expr -> constr -> constr} - {\\ Applies a certain kind of reduction function, specified by an - element of the type red\_expr.} -\fun{val Tacmach.pf\_conv\_x : goal sigma -> constr -> constr -> bool} - {Test whether two given terms are definitionally equal.} -\end{description} - -\subsection[Patterns]{Patterns\label{Patterns}} - -The \ocaml{} file \texttt{Pattern} provides a quick way for describing a -term pattern and performing second-order, binding-preserving, matching -on it. Patterns are described using an extension of \Coq's concrete -syntax, where the second-order meta-variables of the pattern are -denoted by indexed question marks. - -Patterns may depend on constants, and therefore only to make have -sense when certain theories have been loaded. For this reason, they -are stored with a \textsl{module-marker}, telling us which modules -have to be open in order to use the pattern. The following functions -can be used to store and retrieve patterns form the pattern table: - -\begin{description} -\fun{val Pattern.make\_module\_marker : string list -> module\_mark} - {Constructs a module marker from a list of module names.} -\fun{val Pattern.put\_pat : module\_mark -> string -> marked\_term} - {Constructs a pattern from a parseable string containing holes - and a module marker.} -\fun{val Pattern.somatches : constr -> marked\_term-> bool} - {Tests if a term matches a pattern.} -\fun{val dest\_somatch : constr -> marked\_term -> constr list} - {If the term matches the pattern, yields the list of sub-terms - matching the occurrences of the pattern variables (ordered from - left to right). Raises a \texttt{UserError} exception if the term - does not match the pattern.} -\fun{val Pattern.soinstance : marked\_term -> constr list -> constr} - {Substitutes each hole in the pattern - by the corresponding term of the given the list.} -\end{description} - -\paragraph{Warning:} Sometimes, a \Coq\ term may have invisible -sub-terms that the matching functions are nevertheless sensible to. -For example, the \Coq\ term $(?_1,?_2)$ is actually a shorthand for -the expression $(\texttt{pair}\;?\;?\;?_1\;?_2)$. -Hence, matching this term pattern -with the term $(\texttt{true},\texttt{O})$ actually yields the list -$[?;?;\texttt{true};\texttt{O}]$ as result (and \textbf{not} -$[\texttt{true};\texttt{O}]$, as could be expected). - -\subsection{Patterns on Inductive Definitions} - -The module \texttt{Pattern} also includes some functions for testing -if the definition of an inductive type satisfies certain -properties. Such functions may be used to perform pattern matching -independently from the name given to the inductive type and the -universe it inhabits. They yield the value $(\texttt{Some}\;r::l)$ if -the input term reduces into an application of an inductive type $r$ to -a list of terms $l$, and the definition of $r$ satisfies certain -conditions. Otherwise, they yield the value \texttt{None}. - -\begin{description} -\fun{val Pattern.match\_with\_non\_recursive\_type : constr list option} - {Tests if the inductive type $r$ has no recursive constructors} -\fun{val Pattern.match\_with\_disjunction : constr list option} - {Tests if the inductive type $r$ is a non-recursive type - such that all its constructors have a single argument.} -\fun{val Pattern.match\_with\_conjunction : constr list option} - {Tests if the inductive type $r$ is a non-recursive type - with a unique constructor.} -\fun{val Pattern.match\_with\_empty\_type : constr list option} - {Tests if the inductive type $r$ has no constructors at all} -\fun{val Pattern.match\_with\_equation : constr list option} - {Tests if the inductive type $r$ has a single constructor - expressing the property of reflexivity for some type. For - example, the types $a=b$, $A\mbox{==}B$ and $A\mbox{===}B$ satisfy - this predicate.} -\end{description} - -\subsection{Elimination Tacticals} - -It is frequently the case that the subgoals generated by an -elimination can all be solved in a similar way, possibly parametrized -on some information about each case, like for example: -\begin{itemize} -\item the inductive type of the object being eliminated; -\item its arguments (if it is an inductive predicate); -\item the branch number; -\item the predicate to be proven; -\item the number of assumptions to be introduced by the case -\item the signature of the branch, i.e., for each argument of -the branch whether it is recursive or not. -\end{itemize} - -The following tacticals can be useful to deal with such situations. -They - -\begin{description} -\fun{val Elim.simple\_elimination\_then : \\ \qquad -(branch\_args -> tactic) -> constr -> tactic} - {\\ Performs the default elimination on the last argument, and then - tries to solve the generated subgoals using a given parametrized - tactic. The type branch\_args is a record type containing all - information mentioned above.} -\fun{val Elim.simple\_case\_then : \\ \qquad -(branch\_args -> tactic) -> constr -> tactic} - {\\ Similarly, but it performs case analysis instead of induction.} -\end{description} - -\section[A Complete Example]{A Complete Example\label{ACompleteExample}} - -In order to illustrate the implementation of a new tactic, let us come -back to the problem of deciding the equality of two elements of an -inductive type. - -\subsection{Preliminaries} - -Let us call \texttt{newtactic} the directory that will contain the -implementation of the new tactic. In this directory will lay two -files: a file \texttt{eqdecide.ml}, containing the \ocaml{} sources that -implements the tactic, and a \Coq\ file \texttt{Eqdecide.v}, containing -its associated grammar rules and the commands to generate a module -that can be loaded dynamically from \Coq's toplevel. - -To compile our project, we will create a \texttt{Makefile} with the -command \texttt{do\_Makefile} (see Section~\ref{Makefile}) : - -\begin{quotation} - \texttt{do\_Makefile eqdecide.ml EqDecide.v > Makefile}\\ - \texttt{touch .depend}\\ - \texttt{make depend} -\end{quotation} - -We must have kept the sources of \Coq{} somewhere and to set an -environment variable \texttt{COQTOP} that points to that directory. - -\subsection{Implementing the Tactic} - -The file \texttt{eqdecide.ml} contains the implementation of the -tactic in \ocaml{}. Let us recall the main steps of the proof strategy -for deciding the proposition $(x,y:R)\{x=y\}+\{\neg x=y\}$ on the -inductive type $R$: -\begin{enumerate} -\item Eliminate $x$ and then $y$. -\item Try discrimination to solve those goals where $x$ and $y$ has -been introduced by different constructors. -\item If $x$ and $y$ have been introduced by the same constructor, - then analyze one by one the corresponding pairs of arguments. - If they are equal, rewrite one into the other. If they are - not, derive a contradiction from the invectiveness of the - constructor. -\item Once all the arguments have been rewritten, solve the left half -of the goal by reflexivity. -\end{enumerate} - -In the sequel we implement these steps one by one. We start opening -the modules necessary for the implementation of the tactic: - -\begin{verbatim} -open Names -open Term -open Tactics -open Tacticals -open Hiddentac -open Equality -open Auto -open Pattern -open Names -open Termenv -open Std -open Proof_trees -open Tacmach -\end{verbatim} - -The first step of the procedure can be straightforwardly implemented as -follows: - -\begin{verbatim} -let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))));; -\end{verbatim} - -\begin{verbatim} -let mkBranches = - (tclTHEN intro - (tclTHEN (tclLAST_HYP h_simplest_elim) - (tclTHEN clear_last - (tclTHEN intros - (tclTHEN (tclLAST_HYP h_simplest_case) - (tclTHEN clear_last - intros))))));; -\end{verbatim} - -Notice the use of the tactical \texttt{tclLAST\_HYP}, which avoids to -give a (potentially clashing) name to the quantified variables of the -goal when they are introduced. - -The second step of the procedure is implemented by the following -tactic: - -\begin{verbatim} -let solveRightBranch = (tclTHEN simplest_right discrConcl);; -\end{verbatim} - -In order to illustrate how the implementation of a tactic can be -hidden, let us do it with the tactic above: - -\begin{verbatim} -let h_solveRightBranch = - hide_atomic_tactic "solveRightBranch" solveRightBranch -;; -\end{verbatim} - -As it was already mentioned in Section \ref{WhatIsATactic}, the -combinator \texttt{hide\_atomic\_tactic} first registers the tactic -\texttt{solveRightBranch} in the table, and returns a tactic which -calls the interpreter with the used to register it. Hence, when the -tactical \texttt{Info} is used, our tactic will just inform that -\texttt{solveRightBranch} was applied, omitting all the details -corresponding to \texttt{simplest\_right} and \texttt{discrConcl}. - - - -The third step requires some auxiliary functions for constructing the -type $\{c_1=c_2\}+\{\neg c_1=c_2\}$ for a given inductive type $R$ and -two constructions $c_1$ and $c_2$, and for generalizing this type over -$c_1$ and $c_2$: - -\begin{verbatim} -let mmk = make_module_marker ["#Logic.obj";"#Specif.obj"];; -let eqpat = put_pat mmk "eq";; -let sumboolpat = put_pat mmk "sumbool";; -let notpat = put_pat mmk "not";; -let eq = get_pat eqpat;; -let sumbool = get_pat sumboolpat;; -let not = get_pat notpat;; - -let mkDecideEqGoal rectype c1 c2 g = - let equality = mkAppL [eq;rectype;c1;c2] in - let disequality = mkAppL [not;equality] - in mkAppL [sumbool;equality;disequality] -;; -let mkGenDecideEqGoal rectype g = - let hypnames = ids_of_sign (pf_hyps g) in - let xname = next_ident_away (id_of_string "x") hypnames - and yname = next_ident_away (id_of_string "y") hypnames - in (mkNamedProd xname rectype - (mkNamedProd yname rectype - (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g))) -;; -\end{verbatim} - -The tactic will depend on the \Coq modules \texttt{Logic} and -\texttt{Specif}, since we use the constants corresponding to -propositional equality (\texttt{eq}), computational disjunction -(\texttt{sumbool}), and logical negation (\texttt{not}), defined in -that modules. This is specified creating the module maker -\texttt{mmk} (see Section~\ref{Patterns}). - -The third step of the procedure can be divided into three sub-steps. -Assume that both $x$ and $y$ have been introduced by the same -constructor. For each corresponding pair of arguments of that -constructor, we have to consider whether they are equal or not. If -they are equal, the following tactic is applied to rewrite one into -the other: - -\begin{verbatim} -let eqCase tac = - (tclTHEN intro - (tclTHEN (tclLAST_HYP h_rewriteLR) - (tclTHEN clear_last - tac))) -;; -\end{verbatim} - - -If they are not equal, then the goal is contraposed and a -contradiction is reached form the invectiveness of the constructor: - -\begin{verbatim} -let diseqCase = - let diseq = (id_of_string "diseq") in - let absurd = (id_of_string "absurd") - in (tclTHEN (intro_using diseq) - (tclTHEN h_simplest_right - (tclTHEN red_in_concl - (tclTHEN (intro_using absurd) - (tclTHEN (h_simplest_apply (mkVar diseq)) - (tclTHEN (h_injHyp absurd) - trivial )))))) -;; -\end{verbatim} - -In the tactic above we have chosen to name the hypotheses because -they have to be applied later on. This introduces a potential risk -of name clashing if the context already contains other hypotheses -also named ``diseq'' or ``absurd''. - -We are now ready to implement the tactic \textsl{SolveArg}. Given the -two arguments $a_1$ and $a_2$ of the constructor, this tactic cuts the -goal with the proposition $\{a_1=a_2\}+\{\neg a_1=a_2\}$, and then -applies the tactics above to each of the generated cases. If the -disjunction cannot be solved automatically, it remains as a sub-goal -to be proven. - -\begin{verbatim} -let solveArg a1 a2 tac g = - let rectype = pf_type_of g a1 in - let decide = mkDecideEqGoal rectype a1 a2 g - in (tclTHENS (h_elimType decide) - [(eqCase tac);diseqCase;default_auto]) g -;; -\end{verbatim} - -The following tactic implements the third and fourth steps of the -proof procedure: - -\begin{verbatim} -let conclpatt = put_pat mmk "{<?1>?2=?3}+{?4}" -;; -let solveLeftBranch rectype g = - let (_::(lhs::(rhs::_))) = - try (dest_somatch (pf_concl g) conclpatt) - with UserError ("somatch",_)-> error "Unexpected conclusion!" in - let nparams = mind_nparams rectype in - let getargs l = snd (chop_list nparams (snd (decomp_app l))) in - let rargs = getargs rhs - and largs = getargs lhs - in List.fold_right2 - solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g -;; -\end{verbatim} - -Notice the use of a pattern to decompose the goal and obtain the -inductive type and the left and right hand sides of the equality. A -certain number of arguments correspond to the general parameters of -the type, and must be skipped over. Once the corresponding list of -arguments \texttt{rargs} and \texttt{largs} have been obtained, the -tactic \texttt{solveArg} is iterated on them, leaving a disjunction -whose left half can be solved by reflexivity. - -The following tactic joints together the three steps of the -proof procedure: - -\begin{verbatim} -let initialpatt = put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}" -;; -let decideGralEquality g = - let (typ::_) = try (dest_somatch (pf_concl g) initialpatt) - with UserError ("somatch",_) -> - error "The goal does not have the expected form" in - let headtyp = hd_app (pf_compute g typ) in - let rectype = match (kind_of_term headtyp) with - IsMutInd _ -> headtyp - | _ -> error ("This decision procedure only" - " works for inductive objects") - in (tclTHEN mkBranches - (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g -;; -;; -\end{verbatim} - -The tactic above can be specialized in two different ways: either to -decide a particular instance $\{c_1=c_2\}+\{\neg c_1=c_2\}$ of the -universal quantification; or to eliminate this property and obtain two -subgoals containing the hypotheses $c_1=c_2$ and $\neg c_1=c_2$ -respectively. - -\begin{verbatim} -let decideGralEquality = - (tclTHEN mkBranches (tclORELSE h_solveRightBranch solveLeftBranch)) -;; -let decideEquality c1 c2 g = - let rectype = pf_type_of g c1 in - let decide = mkGenDecideEqGoal rectype g - in (tclTHENS (cut decide) [default_auto;decideGralEquality]) g -;; -let compare c1 c2 g = - let rectype = pf_type_of g c1 in - let decide = mkDecideEqGoal rectype c1 c2 g - in (tclTHENS (cut decide) - [(tclTHEN intro - (tclTHEN (tclLAST_HYP simplest_case) - clear_last)); - decideEquality c1 c2]) g -;; -\end{verbatim} - -Next, for each of the tactics that will have an entry in the grammar -we construct the associated dynamic one to be registered in the table -of tactics. This function can be used to overload a tactic name with -several similar tactics. For example, the tactic proving the general -decidability property and the one proving a particular instance for -two terms can be grouped together with the following convention: if -the user provides two terms as arguments, then the specialized tactic -is used; if no argument is provided then the general tactic is invoked. - -\begin{verbatim} -let dyn_decideEquality args g = - match args with - [(COMMAND com1);(COMMAND com2)] -> - let c1 = pf_constr_of_com g com1 - and c2 = pf_constr_of_com g com2 - in decideEquality c1 c2 g - | [] -> decideGralEquality g - | _ -> error "Invalid arguments for dynamic tactic" -;; -add_tactic "DecideEquality" dyn_decideEquality -;; - -let dyn_compare args g = - match args with - [(COMMAND com1);(COMMAND com2)] -> - let c1 = pf_constr_of_com g com1 - and c2 = pf_constr_of_com g com2 - in compare c1 c2 g - | _ -> error "Invalid arguments for dynamic tactic" -;; -add_tactic "Compare" tacargs_compare -;; -\end{verbatim} - -This completes the implementation of the tactic. We turn now to the -\Coq file \texttt{Eqdecide.v}. - - -\subsection{The Grammar Rules} - -Associated to the implementation of the tactic there is a \Coq\ file -containing the grammar and pretty-printing rules for the new tactic, -and the commands to generate an object module that can be then loaded -dynamically during a \Coq\ session. In order to generate an ML module, -the \Coq\ file must contain a -\texttt{Declare ML module} command for all the \ocaml{} files concerning -the implementation of the tactic --in our case there is only one file, -the file \texttt{eqdecide.ml}: - -\begin{verbatim} -Declare ML Module "eqdecide". -\end{verbatim} - -The following grammar and pretty-printing rules are -self-explanatory. We refer the reader to the Section \ref{Grammar} for -the details: - -\begin{verbatim} -Grammar tactic simple_tactic := - EqDecideRuleG1 - [ "Decide" "Equality" comarg($com1) comarg($com2)] -> - [(DecideEquality $com1 $com2)] -| EqDecideRuleG2 - [ "Decide" "Equality" ] -> - [(DecideEquality)] -| CompareRule - [ "Compare" comarg($com1) comarg($com2)] -> - [(Compare $com1 $com2)]. - -Syntax tactic level 0: - EqDecideRulePP1 - [(DecideEquality)] -> - ["Decide" "Equality"] -| EqDecideRulePP2 - [(DecideEquality $com1 $com2)] -> - ["Decide" "Equality" $com1 $com2] -| ComparePP - [(Compare $com1 $com2)] -> - ["Compare" $com1 $com2]. -\end{verbatim} - - -\paragraph{Important:} The names used to label the abstract syntax tree -in the grammar rules ---in this case ``DecideEquality'' and -``Compare''--- must be the same as the name used to register the -tactic in the tactics table. This is what makes the links between the -input entered by the user and the tactic executed by the interpreter. - -\subsection{Loading the Tactic} - -Once the module \texttt{EqDecide.v} has been compiled, the tactic can -be dynamically loaded using the \texttt{Require} command. - -\begin{coq_example} -Require EqDecide. -Goal (x,y:nat){x=y}+{~x=y}. -Decide Equality. -\end{coq_example} - -The implementation of the tactic can be accessed through the -tactical \texttt{Info}: -\begin{coq_example} -Undo. -Info Decide Equality. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Remark that the task performed by the tactic \texttt{solveRightBranch} -is not displayed, since we have chosen to hide its implementation. - -\section[Testing and Debugging your Tactic]{Testing and Debugging your Tactic\label{test-and-debug}} - -When your tactic does not behave as expected, it is possible to trace -it dynamically from \Coq. In order to do this, you have first to leave -the toplevel of \Coq, and come back to the \ocaml{} interpreter. This can -be done using the command \texttt{Drop} (see Section~\ref{Drop}). Once -in the \ocaml{} toplevel, load the file \texttt{tactics/include.ml}. -This file installs several pretty printers for proof trees, goals, -terms, abstract syntax trees, names, etc. It also contains the -function \texttt{go:unit -> unit} that enables to go back to \Coq's -toplevel. - -The modules \texttt{Tacmach} and \texttt{Pfedit} contain some basic -functions for extracting information from the state of the proof -engine. Such functions can be used to debug your tactic if -necessary. Let us mention here some of them: - -\begin{description} -\fun{val get\_pftreestate : unit -> pftreestate} - {Projects the current state of the proof engine.} -\fun{val proof\_of\_pftreestate : pftreestate -> proof} - {Projects the current state of the proof tree. A pretty-printer - displays it in a readable form. } -\fun{val top\_goal\_of\_pftreestate : pftreestate -> goal sigma} - {Projects the goal and the existential variables mapping from - the current state of the proof engine.} -\fun{val nth\_goal\_of\_pftreestate : int -> pftreestate -> goal sigma} - {Projects the goal and mapping corresponding to the $nth$ subgoal - that remains to be proven} -\fun{val traverse : int -> pftreestate -> pftreestate} - {Yields the children of the node that the current state of the - proof engine points to.} -\fun{val solve\_nth\_pftreestate : \\ \qquad -int -> tactic -> pftreestate -> pftreestate} - {\\ Provides the new state of the proof engine obtained applying - a given tactic to some unproven sub-goal.} -\end{description} - -Finally, the traditional \ocaml{} debugging tools like the directives -\texttt{trace} and \texttt{untrace} can be used to follow the -execution of your functions. Frequently, a better solution is to use -the \ocaml{} debugger, see Chapter \ref{Utilities}. - -\section[Concrete syntax for ML tactic and vernacular command]{Concrete syntax for ML tactic and vernacular command\label{Notations-for-ML-command}} - -\subsection{The general case} - -The standard way to bind an ML-written tactic or vernacular command to -a concrete {\Coq} syntax is to use the -\verb=TACTIC EXTEND= and \verb=VERNAC COMMAND EXTEND= macros. - -These macros can be used in any {\ocaml} file defining a (new) ML tactic -or vernacular command. They are expanded into pure {\ocaml} code by -the {\camlpppp} preprocessor of {\ocaml}. Concretely, files that use -these macros need to be compiled by giving to {\tt ocamlc} the option - -\verb=-pp "camlp4o -I $(COQTOP)/parsing grammar.cma pa_extend.cmo"= - -\noindent which is the default for every file compiled by means of a Makefile -generated by {\tt coq\_makefile} (see Chapter~\ref{Addoc-coqc}). So, -just do \verb=make= in this latter case. - -The syntax of the macros is given on figure -\ref{EXTEND-syntax}. They can be used at any place of an {\ocaml} -files where an ML sentence (called \verb=str_item= in the {\tt ocamlc} -parser) is expected. For each rule, the left-hand-side describes the -grammar production and the right-hand-side its interpretation which -must be an {\ocaml} expression. Each grammar production starts with -the concrete name of the tactic or command in {\Coq} and is followed -by arguments, possibly separated by terminal symbols or words. -Here is an example: - -\begin{verbatim} -TACTIC EXTEND Replace - [ "replace" constr(c1) "with" constr(c2) ] -> [ replace c1 c2 ] -END -\end{verbatim} - -\newcommand{\grule}{\textrm{\textsl{rule}}} -\newcommand{\stritem}{\textrm{\textsl{ocaml\_str\_item}}} -\newcommand{\camlexpr}{\textrm{\textsl{ocaml\_expr}}} -\newcommand{\arginfo}{\textrm{\textsl{argument\_infos}}} -\newcommand{\lident}{\textrm{\textsl{lower\_ident}}} -\newcommand{\argument}{\textrm{\textsl{argument}}} -\newcommand{\entry}{\textrm{\textsl{entry}}} -\newcommand{\argtype}{\textrm{\textsl{argtype}}} - -\begin{figure} -\begin{tabular}{|lcll|} -\hline -{\stritem} - & ::= & -\multicolumn{2}{l|}{{\tt TACTIC EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\ - & $|$ & \multicolumn{2}{l|}{{\tt VERNAC COMMAND EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\ -&&\multicolumn{2}{l|}{}\\ -{\grule} & ::= & -\multicolumn{2}{l|}{{\tt [} {\str} \sequence{\argument}{} {\tt ] -> [} {\camlexpr} {\tt ]}}\\ -&&\multicolumn{2}{l|}{}\\ -{\argument} & ::= & {\str} &\mbox{(terminal)}\\ - & $|$ & {\entry} {\tt (} {\lident} {\tt )} &\mbox{(non-terminal)}\\ -&&\multicolumn{2}{l|}{}\\ -{\entry} - & ::= & {\tt string} & (a string)\\ - & $|$ & {\tt preident} & (an identifier typed as a {\tt string})\\ - & $|$ & {\tt ident} & (an identifier of type {\tt identifier})\\ - & $|$ & {\tt global} & (a qualified identifier)\\ - & $|$ & {\tt constr} & (a {\Coq} term)\\ - & $|$ & {\tt openconstr} & (a {\Coq} term with holes)\\ - & $|$ & {\tt sort} & (a {\Coq} sort)\\ - & $|$ & {\tt tactic} & (an ${\cal L}_{tac}$ expression)\\ - & $|$ & {\tt constr\_with\_bindings} & (a {\Coq} term with a list of bindings\footnote{as for the tactics {\tt apply} and {\tt elim}})\\ - & $|$ & {\tt int\_or\_var} & (an integer or an identifier denoting an integer)\\ - & $|$ & {\tt quantified\_hypothesis} & (a quantified hypothesis\footnote{as for the tactics {\tt intros until}})\\ - & $|$ & {\tt {\entry}\_opt} & (an optional {\entry} )\\ - & $|$ & {\tt ne\_{\entry}\_list} & (a non empty list of {\entry})\\ - & $|$ & {\tt {\entry}\_list} & (a list of {\entry})\\ - & $|$ & {\tt bool} & (a boolean: no grammar rule, just for typing)\\ - & $|$ & {\lident} & (a user-defined entry)\\ -\hline -\end{tabular} -\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax} -\label{EXTEND-syntax} -\end{figure} - -There is a set of predefined non-terminal entries which are -automatically translated into an {\ocaml} object of a given type. The -type is not the same for tactics and for vernacular commands. It is -given in the following table: - -\begin{small} -\noindent \begin{tabular}{|l|l|l|} -\hline -{\entry} & {\it type for tactics} & {\it type for commands} \\ -{\tt string} & {\tt string} & {\tt string}\\ -{\tt preident} & {\tt string} & {\tt string}\\ -{\tt ident} & {\tt identifier} & {\tt identifier}\\ -{\tt global} & {\tt global\_reference} & {\tt qualid}\\ -{\tt constr} & {\tt constr} & {\tt constr\_expr}\\ -{\tt openconstr} & {\tt open\_constr} & {\tt constr\_expr}\\ -{\tt sort} & {\tt sorts} & {\tt rawsort}\\ -{\tt tactic} & {\tt glob\_tactic\_expr * tactic} & {\tt raw\_tactic\_expr}\\ -{\tt constr\_with\_bindings} & {\tt constr with\_bindings} & {\tt constr\_expr with\_bindings}\\\\ -{\tt int\_or\_var} & {\tt int or\_var} & {\tt int or\_var}\\ -{\tt quantified\_hypothesis} & {\tt quantified\_hypothesis} & {\tt quantified\_hypothesis}\\ -{\tt {\entry}\_opt} & {\it the type of entry} {\tt option} & {\it the type of entry} {\tt option}\\ -{\tt ne\_{\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\ -{\tt {\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\ -{\tt bool} & {\tt bool} & {\tt bool}\\ -{\lident} & {user-provided, cf next section} & {user-provided, cf next section}\\ -\hline -\end{tabular} -\end{small} - -\bigskip - -Notice that {\entry} consists in a single identifier and that the {\tt -\_opt}, {\tt \_list}, ... modifiers are part of the identifier. -Here is now another example of a tactic which takes either a non empty -list of identifiers and executes the {\ocaml} function {\tt subst} or -takes no arguments and executes the{\ocaml} function {\tt subst\_all}. - -\begin{verbatim} -TACTIC EXTEND Subst -| [ "subst" ne_ident_list(l) ] -> [ subst l ] -| [ "subst" ] -> [ subst_all ] -END -\end{verbatim} - -\subsection{Adding grammar entries for tactic or command arguments} - -In case parsing the arguments of the tactic or the vernacular command -involves grammar entries other than the predefined entries listed -above, you have to declare a new entry using the macros -\verb=ARGUMENT EXTEND= or \verb=VERNAC ARGUMENT EXTEND=. The syntax is -given on Figure~\ref{ARGUMENT-EXTEND-syntax}. Notice that arguments -declared by \verb=ARGUMENT EXTEND= can be used for arguments of both -tactics and vernacular commands while arguments declared by -\verb=VERNAC ARGUMENT EXTEND= can only be used by vernacular commands. - -For \verb=VERNAC ARGUMENT EXTEND=, the identifier is the name of the -entry and it must be a valid {\ocaml} identifier (especially it must -be lowercase). The grammar rules works as before except that they do -not have to start by a terminal symbol or word. As an example, here -is how the {\Coq} {\tt Extraction Language {\it language}} parses its -argument: - -\begin{verbatim} -VERNAC ARGUMENT EXTEND language -| [ "Ocaml" ] -> [ Ocaml ] -| [ "Haskell" ] -> [ Haskell ] -| [ "Scheme" ] -> [ Scheme ] -END -\end{verbatim} - -For tactic arguments, and especially for \verb=ARGUMENT EXTEND=, the -procedure is more subtle because tactics are objects of the {\Coq} -environment which can be printed and interpreted. Then the syntax -requires extra information providing a printer and a type telling how -the argument behaves. Here is an example of entry parsing a pair of -optional {\Coq} terms. - -\begin{verbatim} -let pp_minus_div_arg pr_constr pr_tactic (omin,odiv) = - if omin=None && odiv=None then mt() else - spc() ++ str "with" ++ - pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++ - pr_opt (fun c -> str "div := " ++ pr_constr c) odiv - -ARGUMENT EXTEND minus_div_arg - TYPED AS constr_opt * constr_opt - PRINTED BY pp_minus_div_arg -| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ] -| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ] -| [ ] -> [ None, None ] -END -\end{verbatim} - -Notice that the type {\tt constr\_opt * constr\_opt} tells that the -object behaves as a pair of optional {\Coq} terms, i.e. as an object -of {\ocaml} type {\tt constr option * constr option} if in a -\verb=TACTIC EXTEND= macro and of type {\tt constr\_expr option * -constr\_expr option} if in a \verb=VERNAC COMMAND EXTEND= macro. - -As for the printer, it must be a function expecting a printer for -terms, a printer for tactics and returning a printer for the created -argument. Especially, each sub-{\term} and each sub-{\tac} in the -argument must be typed by the corresponding printers. Otherwise, the -{\ocaml} code will not be well-typed. - -\Rem The entry {\tt bool} is bound to no syntax but it can be used to -give the type of an argument as in the following example: - -\begin{verbatim} -let pr_orient _prc _prt = function - | true -> mt () - | false -> str " <-" - -ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient -| [ "->" ] -> [ true ] -| [ "<-" ] -> [ false ] -| [ ] -> [ true ] -END -\end{verbatim} - -\begin{figure} -\begin{tabular}{|lcl|} -\hline -{\stritem} & ::= & - {\tt ARGUMENT EXTEND} {\ident} {\arginfo} {\nelist{\grule}{$|$}} {\tt END}\\ -& $|$ & {\tt VERNAC ARGUMENT EXTEND} {\ident} {\nelist{\grule}{$|$}} {\tt END}\\ -\\ -{\arginfo} & ::= & {\tt TYPED AS} {\argtype} \\ -&& {\tt PRINTED BY} {\lident} \\ -%&& \zeroone{{\tt INTERPRETED BY} {\lident}}\\ -%&& \zeroone{{\tt GLOBALIZED BY} {\lident}}\\ -%&& \zeroone{{\tt SUBSTITUTED BY} {\lident}}\\ -%&& \zeroone{{\tt RAW\_TYPED AS} {\lident} {\tt RAW\_PRINTED BY} {\lident}}\\ -%&& \zeroone{{\tt GLOB\_TYPED AS} {\lident} {\tt GLOB\_PRINTED BY} {\lident}}\\ -\\ -{\argtype} & ::= & {\argtype} {\tt *} {\argtype} \\ -& $|$ & {\entry} \\ -\hline -\end{tabular} -\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax} -\label{ARGUMENT-EXTEND-syntax} -\end{figure} - -%\end{document} diff --git a/engine/namegen.ml b/engine/namegen.ml index a75fe721f..1dd29e6ea 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -239,7 +239,7 @@ let visible_ids sigma (nenv, c) = let next_name_away_in_cases_pattern sigma env_t na avoid = let id = match na with Name id -> id | Anonymous -> default_dependent_ident in let visible = visible_ids sigma env_t in - let bad id = Id.List.mem id avoid || is_constructor id + let bad id = Id.Set.mem id avoid || is_constructor id || Id.Set.mem id visible in next_ident_away_from id bad @@ -253,8 +253,8 @@ let next_name_away_in_cases_pattern sigma env_t na avoid = name is taken by finding a free subscript starting from 0 *) let next_ident_away_in_goal id avoid = - let id = if Id.List.mem id avoid then restart_subscript id else id in - let bad id = Id.List.mem id avoid || (is_global id && not (is_section_variable id)) in + let id = if Id.Set.mem id avoid then restart_subscript id else id in + let bad id = Id.Set.mem id avoid || (is_global id && not (is_section_variable id)) in next_ident_away_from id bad let next_name_away_in_goal na avoid = @@ -271,16 +271,16 @@ let next_name_away_in_goal na avoid = beyond the current subscript *) let next_global_ident_away id avoid = - let id = if Id.List.mem id avoid then restart_subscript id else id in - let bad id = Id.List.mem id avoid || is_global id in + let id = if Id.Set.mem id avoid then restart_subscript id else id in + let bad id = Id.Set.mem id avoid || is_global id in next_ident_away_from id bad (* 4- Looks for next fresh name outside a list; if name already used, looks for same name with lower available subscript *) let next_ident_away id avoid = - if Id.List.mem id avoid then - next_ident_away_from (restart_subscript id) (fun id -> Id.List.mem id avoid) + if Id.Set.mem id avoid then + next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid) else id let next_name_away_with_default default na avoid = @@ -302,7 +302,7 @@ let next_name_away = next_name_away_with_default default_non_dependent_string let make_all_name_different env sigma = (** FIXME: this is inefficient, but only used in printing *) - let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in + let avoid = ref (ids_of_named_context_val (named_context_val env)) in let sign = named_context_val env in let rels = rel_context env in let env0 = reset_with_named_context sign env in @@ -310,7 +310,7 @@ let make_all_name_different env sigma = (fun decl newenv -> let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in - avoid := id::!avoid; + avoid := Id.Set.add id !avoid; push_rel (RelDecl.set_name (Name id) decl) newenv) rels ~init:env0 @@ -321,7 +321,7 @@ let make_all_name_different env sigma = let next_ident_away_for_default_printing sigma env_t id avoid = let visible = visible_ids sigma env_t in - let bad id = Id.List.mem id avoid || Id.Set.mem id visible in + let bad id = Id.Set.mem id avoid || Id.Set.mem id visible in next_ident_away_from id bad let next_name_away_for_default_printing sigma env_t na avoid = @@ -371,7 +371,7 @@ let compute_displayed_name_in sigma flags avoid na c = | _ -> let fresh_id = next_name_for_display sigma flags na avoid in let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in - (idopt, fresh_id::avoid) + (idopt, Id.Set.add fresh_id avoid) let compute_and_force_displayed_name_in sigma flags avoid na c = match na with @@ -379,11 +379,11 @@ let compute_and_force_displayed_name_in sigma flags avoid na c = (Anonymous,avoid) | _ -> let fresh_id = next_name_for_display sigma flags na avoid in - (Name fresh_id, fresh_id::avoid) + (Name fresh_id, Id.Set.add fresh_id avoid) let compute_displayed_let_name_in sigma flags avoid na c = let fresh_id = next_name_for_display sigma flags na avoid in - (Name fresh_id, fresh_id::avoid) + (Name fresh_id, Id.Set.add fresh_id avoid) let rename_bound_vars_as_displayed sigma avoid env c = let rec rename avoid env c = diff --git a/engine/namegen.mli b/engine/namegen.mli index 14846a918..6fde90a39 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -72,23 +72,22 @@ val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t the whole identifier except for the {i subscript}. E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) -val next_ident_away : Id.t -> Id.t list -> Id.t +val next_ident_away : Id.t -> Id.Set.t -> Id.t (** Avoid clashing with a name already used in current module *) -val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t +val next_ident_away_in_goal : Id.t -> Id.Set.t -> Id.t (** Avoid clashing with a name already used in current module but tolerate overwriting section variables, as in goals *) -val next_global_ident_away : Id.t -> Id.t list -> Id.t +val next_global_ident_away : Id.t -> Id.Set.t -> Id.t (** Default is [default_non_dependent_ident] *) -val next_name_away : Name.t -> Id.t list -> Id.t +val next_name_away : Name.t -> Id.Set.t -> Id.t -val next_name_away_with_default : string -> Name.t -> Id.t list -> - Id.t +val next_name_away_with_default : string -> Name.t -> Id.Set.t -> Id.t val next_name_away_with_default_using_types : string -> Name.t -> - Id.t list -> types -> Id.t + Id.Set.t -> types -> Id.t val set_reserved_typed_name : (types -> Name.t) -> unit @@ -103,13 +102,13 @@ type renaming_flags = val make_all_name_different : env -> evar_map -> env val compute_displayed_name_in : - evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val compute_and_force_displayed_name_in : - evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val compute_displayed_let_name_in : - evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val rename_bound_vars_as_displayed : - evar_map -> Id.t list -> Name.t list -> types -> types + evar_map -> Id.Set.t -> Name.t list -> types -> types (**********************************************************************) (* Naming strategy for arguments in Prop when eliminating inductive types *) diff --git a/engine/termops.ml b/engine/termops.ml index e2bdf7238..b7fa2dc4a 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1071,9 +1071,9 @@ let replace_term_gen sigma eq_fun c by_c in_t = let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t let vars_of_env env = - let s = - Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s) - (named_context env) ~init:Id.Set.empty in + let s = Environ.ids_of_named_context_val (Environ.named_context_val env) in + if List.is_empty (Environ.rel_context env) then s + else Context.Rel.fold_outside (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s) (rel_context env) ~init:s diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 9be70e6d3..0dd08293c 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -480,8 +480,11 @@ object(self) | Message(lvl, loc, msg), Some (id,sentence) -> log_pp ?id Pp.(str "Msg " ++ msg); messages#push lvl msg + (* We do nothing here as for BZ#5583 *) + | Message(Error, loc, msg), None -> + log_pp Pp.(str "Error Msg without a sentence" ++ msg) | Message(lvl, loc, msg), None -> - log_pp Pp.(str "Msg " ++ msg); + log_pp Pp.(str "Msg without a sentence " ++ msg); messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n @@ -655,7 +658,7 @@ object(self) with Doc.Empty -> initial_state | Invalid_argument _ -> assert false in loop tip [] in Coq.bind fill_queue process_queue - + method join_document = let next = function | Good _ -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f5eff693f..f1bee65ef 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1087,7 +1087,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* Not "goal_concl_style" means do alpha-conversion avoiding only *) (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) - let avoid = if goal_concl_style then ids_of_context env else [] in + let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in extern false (scopt,[]) vars r @@ -1099,14 +1099,14 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t = extern_constr_gen lax goal_concl_style None env sigma t let extern_type goal_concl_style env sigma t = - let avoid = if goal_concl_style then ids_of_context env else [] in + let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) let extern_closed_glob ?lax goal_concl_style env sigma t = - let avoid = if goal_concl_style then ids_of_context env else [] in + let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t in @@ -1177,15 +1177,15 @@ let rec glob_of_pat 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 env sigma tm,indnames],mat) - | PFix f -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) - | PCoFix c -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) + | PFix f -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) + | PCoFix c -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) | PSort s -> GSort s let extern_constr_pattern env sigma pat = extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) let extern_rel_context where env sigma sign = - let a = detype_rel_context Detyping.Later where [] (names_of_rel_context env,env) sigma sign in + let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in let a = List.map (extended_glob_local_binder_of_decl) a in pi3 (extern_local_binder (None,[]) vars a) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6f7c6c827..1cea307d7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -469,8 +469,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio | _ -> assert false in let env = {env with ids = List.fold_right Id.Set.add il env.ids} in - let ienv = Id.Set.elements env.ids in - let id = Namegen.next_ident_away (Id.of_string "pat") ienv in + let id = Namegen.next_ident_away (Id.of_string "pat") env.ids in let na = (loc, Name id) in let bk = Default Explicit in let _, bl' = intern_assumption intern lvar env [na] bk tyc in @@ -1939,13 +1938,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | _ -> let fresh = Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in - canonize_args t tt (fresh::forbidden_names) + canonize_args t tt (Id.Set.add fresh forbidden_names) ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) end | _ -> assert false in let _,args_rel = List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in - canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in + canonize_args args_rel l forbidden_names_for_gen [] [] in match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal)) | None -> [], None in diff --git a/interp/impargs.ml b/interp/impargs.ml index d8241c044..09a0ba83c 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -255,7 +255,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = in match kind_of_term (whd_all env t) with | Prod (na,a,b) -> - let na',avoid = find_displayed_name_in all [] na ([],b) in + let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in !rigid, Array.to_list v | _ -> true, [] diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 3d48114ec..0967d21f0 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -577,7 +577,7 @@ let rec subst_notation_constr subst bound raw = if r1' == r1 && k' == k then raw else NCast(r1',k') let subst_interpretation subst (metas,pat) = - let bound = List.map fst metas in + let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in (metas,subst_notation_constr subst bound pat) (**********************************************************************) @@ -1143,7 +1143,7 @@ let rec match_ inner u alp metas sigma a1 a2 = to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *) | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner -> let avoid = - free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in + Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in let id' = Namegen.next_ident_away id avoid in let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with diff --git a/interp/reserve.ml b/interp/reserve.ml index a1e5bd0ea..dc0f60dcf 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -110,7 +110,7 @@ let revert_reserved_type t = let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in let t = EConstr.of_constr t in - let t = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in + let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index cfc3343b6..03e8ea43d 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -139,8 +139,7 @@ type search_restriction = type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) - (* list of idents for qed exporting *) -type opacity_flag = Opaque of lident list option | Transparent +type opacity_flag = Opaque | Transparent type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 621a9931d..c3fd8962e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -101,6 +101,8 @@ let fold_rel_context f env ~init = let named_context_of_val c = c.env_named_ctx +let ids_of_named_context_val c = Id.Map.domain c.env_named_map + (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) diff --git a/kernel/environ.mli b/kernel/environ.mli index 377c61de2..2667ad7ca 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -80,6 +80,7 @@ val fold_rel_context : val named_context_of_val : named_context_val -> Context.Named.t val val_of_named_context : Context.Named.t -> named_context_val val empty_named_context_val : named_context_val +val ids_of_named_context_val : named_context_val -> Id.Set.t (** [map_named_val f ctxt] apply [f] to the body and the type of diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 13de731f5..970666638 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -206,7 +206,7 @@ let rec find_project_file ~from ~projfile_name = if Sys.file_exists fname then Some fname else let newdir = Filename.dirname from in - if newdir = "" || newdir = "/" then None + if newdir = from then None else find_project_file ~from:newdir ~projfile_name ;; diff --git a/lib/util.ml b/lib/util.ml index 36282b2da..6de012da0 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -171,3 +171,12 @@ let open_utf8_file_in fname = let s = Bytes.make 3 ' ' in if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; in_chan + +(** A trick which can typically be used to store on the fly the + computation of values in the "when" clause of a "match" then + retrieve the evaluated result in the r.h.s of the clause *) + +let set_temporary_memory () = + let a = ref None in + (fun x -> assert (!a = None); a := Some x; x), + (fun () -> match !a with Some x -> x | None -> assert false) diff --git a/lib/util.mli b/lib/util.mli index d910e7e28..c54f5825c 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -137,3 +137,8 @@ val sym : ('a, 'b) eq -> ('b, 'a) eq val open_utf8_file_in : string -> in_channel (** Open an utf-8 encoded file and skip the byte-order mark if any. *) + +val set_temporary_memory : unit -> ('a -> 'a) * (unit -> 'a) +(** A trick which can typically be used to store on the fly the + computation of values in the "when" clause of a "match" then + retrieve the evaluated result in the r.h.s of the clause *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 870137ca1..d51b8b54e 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -34,6 +34,7 @@ let default_levels = [200,Extend.RightA,false; 100,Extend.RightA,false; 99,Extend.RightA,true; + 90,Extend.RightA,true; 10,Extend.RightA,false; 9,Extend.RightA,false; 8,Extend.RightA,true; @@ -44,6 +45,7 @@ let default_pattern_levels = [200,Extend.RightA,true; 100,Extend.RightA,false; 99,Extend.RightA,true; + 90,Extend.RightA,true; 11,Extend.LeftA,false; 10,Extend.RightA,false; 1,Extend.LeftA,false; diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 4e8b98fcf..844c040fd 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -376,6 +376,7 @@ GEXTEND Gram | "100" RIGHTA [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ] | "99" RIGHTA [ ] + | "90" RIGHTA [ ] | "11" LEFTA [ p = pattern; "as"; id = ident -> CAst.make ~loc:!@loc @@ CPatAlias (p, id) ] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 42b5bfa93..e2c87bbbf 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -45,11 +45,9 @@ GEXTEND Gram | IDENT "Existential"; n = natural; c = constr_body -> VernacSolveExistential (n,c) | IDENT "Admitted" -> VernacEndProof Admitted - | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None)) - | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," -> - VernacEndProof (Proved (Opaque (Some l),None)) + | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None)) | IDENT "Save"; id = identref -> - VernacEndProof (Proved (Opaque None, Some id)) + VernacEndProof (Proved (Opaque, Some id)) | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None)) | IDENT "Defined"; id=identref -> VernacEndProof (Proved (Transparent,Some id)) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4a59b8597..819d236cd 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -131,7 +131,7 @@ let test_plural_form_types loc kwd = function let fresh_var env c = Namegen.next_ident_away (Id.of_string "pat") - (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c)) + (List.fold_left (fun accu id -> Id.Set.add id accu) (Topconstr.free_vars_of_constr_expr c) env) let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index fca7d9851..150319f6b 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -444,7 +444,7 @@ let cc_tactic depth additionnal_terms = let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in let pr_missing (c, missing) = - let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in + let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in let holes = List.init missing (fun _ -> hole) in Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) in diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9772ebd64..9aec190d0 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -405,7 +405,7 @@ let ref_renaming_fun (k,r) = let idg = safe_basename_of_global r in match l with | [""] -> (* this happens only at toplevel of the monolithic case *) - let globs = Id.Set.elements (get_global_ids ()) in + let globs = get_global_ids () in let id = next_ident_away (kindcase_id k idg) globs in Id.to_string id | _ -> modular_rename k idg diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 7644b49ce..a227478d0 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -141,6 +141,7 @@ let make_typvar n vl = if not (String.contains s '\'') && Unicode.is_basic_ascii s then id else id_of_name Anonymous in + let vl = Id.Set.of_list vl in next_ident_away id' vl let rec type_sign_vl env c = diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ca98f07e8..30e3b520f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -750,11 +750,11 @@ let extraction_implicit r l = let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist" -let modfile_ids = ref [] +let modfile_ids = ref Id.Set.empty let modfile_mps = ref MPmap.empty let reset_modfile () = - modfile_ids := Id.Set.elements !blacklist_table; + modfile_ids := !blacklist_table; modfile_mps := MPmap.empty let string_of_modfile mp = @@ -763,7 +763,7 @@ let string_of_modfile mp = let id = Id.of_string (raw_string_of_modfile mp) in let id' = next_ident_away id !modfile_ids in let s' = Id.to_string id' in - modfile_ids := id' :: !modfile_ids; + modfile_ids := Id.Set.add id' !modfile_ids; modfile_mps := MPmap.add mp s' !modfile_mps; s' diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 169073630..c2606dbe8 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -115,8 +115,8 @@ let mk_open_instance env evmap id idc m t = let nid=(fresh_id_in_env avoid var_id env) in let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in let decl = LocalAssum (Name nid, c) in - aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in - let evmap, decls = aux m [] env evmap [] in + aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in + let evmap, decls = aux m Id.Set.empty env evmap [] in (evmap, decls, revt) (* tactics *) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5f6d78359..bd5fb1d92 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -587,7 +587,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclTHENLIST [ (* We first introduce the variables *) - tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps)); + tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))); (* Then the equation itself *) Proofview.V82.of_tactic (intro_using heq_id); onLastHypId (fun heq_id -> tclTHENLIST [ @@ -1614,7 +1614,7 @@ let prove_principle_for_gen let hid = next_ident_away_in_goal (Id.of_string "prov") - hyps + (Id.Set.of_list hyps) in tclTHENLIST [ diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 409bb89ee..018b51517 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -39,7 +39,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | decl :: predicates -> (match Context.Rel.Declaration.get_name decl with | Name x -> - let id = Namegen.next_ident_away x avoid in + let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in Hashtbl.add tbl id x; RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates | Anonymous -> anomaly (Pp.str "Anonymous property binder.")) @@ -285,7 +285,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* let time2 = System.get_time () in *) (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) let new_princ_name = - next_ident_away_in_goal (Id.of_string "___________princ_________") [] + next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty in let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in let hook = Lemmas.mk_hook (hook new_principle_type) in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7087a195e..e8e5bfccc 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -120,13 +120,13 @@ let combine_args arg args = let ids_of_binder = function - | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> [] - | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id] + | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty + | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id let rec change_vars_in_binder mapping = function [] -> [] | (bt,t)::l -> - let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in + let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in (bt,change_vars mapping t):: (if Id.Map.is_empty new_mapping then l @@ -137,27 +137,27 @@ let rec replace_var_by_term_in_binder x_id term = function | [] -> [] | (bt,t)::l -> (bt,replace_var_by_term x_id term t):: - if Id.List.mem x_id (ids_of_binder bt) + if Id.Set.mem x_id (ids_of_binder bt) then l else replace_var_by_term_in_binder x_id term l -let add_bt_names bt = List.append (ids_of_binder bt) +let add_bt_names bt = Id.Set.union (ids_of_binder bt) let apply_args ctxt body args = let need_convert_id avoid id = - List.exists (is_free_in id) args || Id.List.mem id avoid + List.exists (is_free_in id) args || Id.Set.mem id avoid in let need_convert avoid bt = - List.exists (need_convert_id avoid) (ids_of_binder bt) + Id.Set.exists (need_convert_id avoid) (ids_of_binder bt) in - let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = + let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.Set.t) = match na with - | Name id when Id.List.mem id avoid -> + | Name id when Id.Set.mem id avoid -> let new_id = Namegen.next_ident_away id avoid in - Name new_id,Id.Map.add id new_id mapping,new_id::avoid + Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid | _ -> na,mapping,avoid in - let next_bt_away bt (avoid:Id.t list) = + let next_bt_away bt (avoid:Id.Set.t) = match bt with | LetIn na -> let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in @@ -182,15 +182,15 @@ let apply_args ctxt body args = let new_avoid,new_ctxt',new_body,new_id = if need_convert_id avoid id then - let new_avoid = id::avoid in + let new_avoid = Id.Set.add id avoid in let new_id = Namegen.next_ident_away id new_avoid in - let new_avoid' = new_id :: new_avoid in + let new_avoid' = Id.Set.add new_id new_avoid in let mapping = Id.Map.add id new_id Id.Map.empty in let new_ctxt' = change_vars_in_binder mapping ctxt' in let new_body = change_vars mapping body in new_avoid',new_ctxt',new_body,new_id else - id::avoid,ctxt',body,id + Id.Set.add id avoid,ctxt',body,id in let new_body = replace_var_by_term new_id arg new_body in let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in @@ -214,7 +214,7 @@ let apply_args ctxt body args = in (new_bt,t)::new_ctxt',new_body in - do_apply [] ctxt body args + do_apply Id.Set.empty ctxt body args let combine_app f args = @@ -434,7 +434,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr csta.(i))) + (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i))) ) in let patl_as_term = @@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in - let res_raw_type = Detyping.detype Detyping.Now false [] env (Evd.from_env env) rt_typ in + let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in @@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = match n with | Name id when List.exists (is_free_in id) args -> (* need to alpha-convert the name *) - let new_id = Namegen.next_ident_away id avoid in + let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in let new_avoid = id:: avoid in let new_b = replace_var_by_term @@ -773,7 +773,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype Detyping.Now false [] + Detyping.detype Detyping.Now false Id.Set.empty env_with_pat_ids (Evd.from_env env) typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) @@ -819,7 +819,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in let typ_as_constr = EConstr.of_constr typ_as_constr in - let typ = Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_as_constr in + let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in (* removing trivial holes *) let pat_as_term = solve_trivial_holes pat_as_term e in @@ -833,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve then (Prod (Name id), let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_of_id + Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id in raw_typ_of_id )::acc @@ -1001,7 +1001,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let rt_typ = DAst.make @@ GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None), (List.map - (fun p -> Detyping.detype Detyping.Now false [] + (fun p -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr p)) params)@(Array.to_list (Array.make @@ -1028,12 +1028,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match na with | Anonymous -> acc | Name id' -> - (id',Detyping.detype Detyping.Now false [] + (id',Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) arg)::acc else if isVar var_as_constr - then (destVar var_as_constr,Detyping.detype Detyping.Now false [] + then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) arg)::acc diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 02ee56ac5..0666ab4f1 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -198,7 +198,7 @@ let rec alpha_pat excluded pat = | PatVar(Name id) -> if Id.List.mem id excluded then - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) else pat, excluded,Id.Map.empty @@ -206,7 +206,7 @@ let rec alpha_pat excluded pat = let new_na,new_excluded,map = match na with | Name id when Id.List.mem id excluded -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty | _ -> na,excluded,Id.Map.empty in @@ -261,7 +261,7 @@ let rec alpha_rt excluded rt = match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt | GLambda(Anonymous,k,t,b) -> - let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in + let new_id = Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded) in let new_excluded = new_id :: excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in @@ -276,7 +276,7 @@ let rec alpha_rt excluded rt = let new_c = alpha_rt excluded c in GLetIn(Anonymous,new_b,new_t,new_c) | GLambda(Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let t,b = if Id.equal new_id id then t, b @@ -289,7 +289,7 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in GLambda(Name new_id,k,new_t,new_b) | GProd(Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let new_excluded = new_id::excluded in let t,b = if Id.equal new_id id @@ -302,7 +302,7 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in GProd(Name new_id,k,new_t,new_b) | GLetIn(Name id,b,t,c) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let c = if Id.equal new_id id then c else change_vars (Id.Map.add id new_id Id.Map.empty) c @@ -320,7 +320,7 @@ let rec alpha_rt excluded rt = match na with | Anonymous -> (na::nal,excluded,mapping) | Name id -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in if Id.equal new_id id then na::nal,id::excluded,mapping @@ -741,7 +741,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -763,7 +763,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5f4d514f3..1e8854249 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -12,7 +12,7 @@ let mk_equation_id id = Nameops.add_suffix id "_equation" let msgnl m = () -let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid +let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid) let fresh_name avoid s = Name (fresh_id avoid s) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5f8d50da1..299753766 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -131,9 +131,9 @@ let generate_type evd g_to_f f graph i = | Name id -> Some id | Anonymous -> None in - let named_ctxt = List.map_filter filter fun_ctxt in + let named_ctxt = Id.Set.of_list (List.map_filter filter fun_ctxt) in let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in - let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in + let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (Id.Set.add res_id named_ctxt) in (*i we can then type the argument to be applied to the function [f] i*) let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in (*i @@ -189,7 +189,7 @@ let rec generate_fresh_id x avoid i = if i == 0 then [] else - let id = Namegen.next_ident_away_in_goal x avoid in + let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in id::(generate_fresh_id x (id::avoid) (pred i)) @@ -239,7 +239,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes environment and due to the bug #1174, we will need to pose the principle using a name *) - let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in + let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") (Id.Set.of_list ids) in let ids = principle_id :: ids in (* We get the branches of the principle *) let branches = List.rev princ_infos.branches in @@ -396,7 +396,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let params_bindings,avoid = List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -406,7 +406,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 96200a98a..77c26f8ce 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -767,7 +767,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in let substindtyp = EConstr.of_constr substindtyp in - Detyping.detype Detyping.Now false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in + Detyping.detype Detyping.Now false avoid (Global.env()) Evd.empty substindtyp in let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) @@ -851,7 +851,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with | LocalAssum (nme,t) -> let t = EConstr.of_constr t in - let traw = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in + let traw = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in DAst.make @@ GProd (nme,Explicit,traw,t2) | LocalDef _ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d43fd78f3..74c454334 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -115,13 +115,17 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta (* Generic values *) let pf_get_new_ids idl g = let ids = pf_ids_of_hyps g in + let ids = Id.Set.of_list ids in List.fold_right - (fun id acc -> next_global_ident_away id (acc@ids)::acc) + (fun id acc -> next_global_ident_away id (Id.Set.union (Id.Set.of_list acc) ids)::acc) idl [] +let next_ident_away_in_goal ids avoid = + next_ident_away_in_goal ids (Id.Set.of_list avoid) + let compute_renamed_type gls c = - rename_bound_vars_as_displayed (project gls) (*no avoid*) [] (*no rels*) [] + rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) [] (pf_unsafe_type_of gls c) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" @@ -1288,8 +1292,8 @@ let build_new_goal_type () = let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None - | Declarations.Undef _ -> Vernacexpr.Opaque None + | Declarations.OpaqueDef _ -> Vernacexpr.Opaque + | Declarations.Undef _ -> Vernacexpr.Opaque | Declarations.Def _ -> Vernacexpr.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = @@ -1302,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp with e when CErrors.noncritical e -> anomaly (Pp.str "open_new_goal with an unamed theorem.") in - let na = next_global_ident_away name [] in + let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 4cab6ef33..d9150a7bb 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -88,7 +88,7 @@ let let_evar name typ = let id = match name with | Name.Anonymous -> let id = Namegen.id_of_name_using_hdchar env sigma typ name in - Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) + Namegen.next_ident_away_in_goal id (Termops.vars_of_env env) | Name.Name id -> id in let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index b4c6f9c90..a7aebf9e1 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -665,7 +665,7 @@ let hResolve id c occ t = let sigma = Proofview.Goal.sigma gl in let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in - let env_ids = Termops.ids_of_context env in + let env_ids = Termops.vars_of_env env in let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in let rec resolve_hole t_hole = @@ -764,7 +764,7 @@ let case_eq_intros_rewrite x = mkCaseEq x; Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let hyps = Tacmach.New.pf_ids_of_hyps gl in + let hyps = Tacmach.New.pf_ids_set_of_hyps gl in let n' = nb_prod (Tacmach.New.project gl) concl in let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in Tacticals.New.tclTHENLIST [ diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 2ea0f60eb..86c983bdd 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -388,16 +388,7 @@ let vernac_solve n info tcom b = p,status) in if not status then Feedback.feedback Feedback.AddedAxiom -let pr_range_selector (i, j) = - if Int.equal i j then int i - else int i ++ str "-" ++ int j - -let pr_ltac_selector = function -| SelectNth i -> int i ++ str ":" -| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ - str "]" ++ str ":" -| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" -| SelectAll -> str "all" ++ str ":" +let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector | [ toplevel_selector(s) ] -> [ s ] diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index f4e3ba633..d8bd16620 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -477,12 +477,14 @@ type 'a extra_genarg_printer = if Int.equal i j then int i else int i ++ str "-" ++ int j - let pr_goal_selector = function - | SelectNth i -> int i ++ str ":" - | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ - str "]" ++ str ":" - | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" - | SelectAll -> str "all" ++ str ":" +let pr_goal_selector toplevel = function + | SelectNth i -> int i ++ str ":" + | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" + | SelectId id -> str "[" ++ Id.print id ++ str "]:" + | SelectAll -> assert toplevel; str "all:" + +let pr_goal_selector ~toplevel s = + (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s let pr_lazy = function | General -> keyword "multi" @@ -662,14 +664,14 @@ type 'a extra_genarg_printer = let names = List.fold_left (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) + (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln) ln nal) - [] bll in + Id.Set.empty bll in let idarg,bll = set_nth_name names n bll in - let annot = match names with - | [_] -> + let annot = + if Int.equal (Id.Set.cardinal names) 1 then mt () - | _ -> + else spc() ++ str"{" ++ keyword "struct" ++ spc () ++ pr_id idarg ++ str"}" @@ -988,7 +990,7 @@ type 'a extra_genarg_printer = keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> pr_tac (lcomplete,E) t, lcomplete - | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom + | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom | TacAtom (loc,t) -> diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 1f6ebaf44..c79d5b389 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -53,6 +53,8 @@ type pp_tactic = { pptac_prods : grammar_terminals; } +val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t + val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit val pr_with_occurrences : diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3d01cbe8d..fd791a910 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -664,7 +664,7 @@ type rewrite_result = type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *) env : Environ.env ; - unfresh : Id.t list ; (* Unfresh names *) + unfresh : Id.Set.t; (* Unfresh names *) term1 : constr ; ty1 : types ; (* first term and its type (convertible to rew_from) *) cstr : (bool (* prop *) * constr option) ; @@ -1614,7 +1614,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = in try let res = - cl_rewrite_clause_aux ?abs strat env [] sigma ty clause + cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause in let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma res <*> diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 23767c12f..63e891b45 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -110,7 +110,7 @@ val setoid_transitivity : constr option -> unit Proofview.tactic val apply_strategy : strategy -> Environ.env -> - Names.Id.t list -> + Names.Id.Set.t -> constr -> bool * constr -> evars -> rewrite_result diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 8fa95ffb0..18348bc11 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -139,7 +139,7 @@ let name_vfun appl vle = module TacStore = Geninterp.TacStore -let f_avoid_ids : Id.t list TacStore.field = TacStore.field () +let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field () (* ids inherited from the call context (needed to get fresh ids) *) let f_debug : debug_info TacStore.field = TacStore.field () let f_trace : ltac_trace TacStore.field = TacStore.field () @@ -501,29 +501,29 @@ let extract_ltac_constr_values ist env = could barely be defined as a feature... *) (* Extract the identifier list from lfun: join all branches (what to do else?)*) -let rec intropattern_ids (loc,pat) = match pat with - | IntroNaming (IntroIdentifier id) -> [id] +let rec intropattern_ids accu (loc,pat) = match pat with + | IntroNaming (IntroIdentifier id) -> Id.Set.add id accu | IntroAction (IntroOrAndPattern (IntroAndPattern l)) -> - List.flatten (List.map intropattern_ids l) + List.fold_left intropattern_ids accu l | IntroAction (IntroOrAndPattern (IntroOrPattern ll)) -> - List.flatten (List.map intropattern_ids (List.flatten ll)) + List.fold_left intropattern_ids accu (List.flatten ll) | IntroAction (IntroInjection l) -> - List.flatten (List.map intropattern_ids l) - | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat + List.fold_left intropattern_ids accu l + | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids accu pat | IntroNaming (IntroAnonymous | IntroFresh _) | IntroAction (IntroWildcard | IntroRewrite _) - | IntroForthcoming _ -> [] + | IntroForthcoming _ -> accu -let extract_ids ids lfun = +let extract_ids ids lfun accu = let fold id v accu = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu - else accu @ intropattern_ids (Loc.tag ipat) + else intropattern_ids accu (Loc.tag ipat) else accu in - Id.Map.fold fold lfun [] + Id.Map.fold fold lfun accu let default_fresh_id = Id.of_string "H" @@ -534,10 +534,10 @@ let interp_fresh_id ist env sigma l = with Not_found -> id in let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with - | None -> [] + | None -> Id.Set.empty | Some l -> l in - let avoid = (extract_ids ids ist.lfun) @ avoid in + let avoid = extract_ids ids ist.lfun avoid in let id = if List.is_empty l then default_fresh_id else @@ -1303,7 +1303,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v end | ArgArg (loc,r) -> - let ids = extract_ids [] ist.lfun in + let ids = extract_ids [] ist.lfun Id.Set.empty in let loc_info = (Option.default loc loc',LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in push_trace loc_info ist >>= fun trace -> @@ -1956,7 +1956,7 @@ let interp_tac_gen lfun avoid_ids debug t = (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) end -let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t +let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index c1ab2b4c4..d0a0a81d4 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -40,7 +40,7 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } -val f_avoid_ids : Id.t list TacStore.field +val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field val extract_ltac_constr_values : interp_sign -> Environ.env -> @@ -113,7 +113,7 @@ val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic (** Globalization + interpretation *) -val interp_tac_gen : value Id.Map.t -> Id.t list -> +val interp_tac_gen : value Id.Map.t -> Id.Set.t -> debug_info -> raw_tactic_expr -> unit Proofview.tactic val interp : raw_tactic_expr -> unit Proofview.tactic diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a4103634e..fc6781b06 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1986,7 +1986,7 @@ let micromega_gen let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in - let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in + let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; @@ -2101,7 +2101,7 @@ let micromega_genr prover tac = let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in - let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in + let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 99493d698..ae1a563be 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1760,7 +1760,7 @@ let onClearedName id tac = tclTHEN (tclTRY (clear [id])) (Proofview.Goal.nf_enter begin fun gl -> - let id = fresh_id [] id gl in + let id = fresh_id Id.Set.empty id gl in tclTHEN (introduction id) (tac id) end) @@ -1768,8 +1768,8 @@ let onClearedName2 id tac = tclTHEN (tclTRY (clear [id])) (Proofview.Goal.nf_enter begin fun gl -> - let id1 = fresh_id [] (add_suffix id "_left") gl in - let id2 = fresh_id [] (add_suffix id "_right") gl in + let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in + let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] end) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 8b69c3435..95ca6f49a 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -129,7 +129,7 @@ let newssrcongrtac arg ist gl = let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in pf_saturate gl (EConstr.of_constr eq) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) - (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) ty) ist) + (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist) (fun () -> let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 060225dab..1e1a986da 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -342,7 +342,7 @@ let interp_index ist gl idx = | None -> begin match Tacinterp.Value.to_constr v with | Some c -> - let rc = Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) c in + let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc with | _, Constrexpr.Numeral (s,b) -> let n = int_of_string s in if b then n else -n diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7455587c0..08ce72932 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -113,8 +113,8 @@ let rec relocate_index sigma n1 n2 k t = type 'a rhs = { rhs_env : env; - rhs_vars : Id.t list; - avoid_ids : Id.t list; + rhs_vars : Id.Set.t; + avoid_ids : Id.Set.t; it : 'a option} type 'a equation = @@ -553,7 +553,7 @@ let extract_rhs pb = let occur_in_rhs na rhs = match na with | Anonymous -> false - | Name id -> Id.List.mem id rhs.rhs_vars + | Name id -> Id.Set.mem id rhs.rhs_vars let is_dep_patt_in eqn pat = match DAst.get pat with | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs @@ -747,8 +747,8 @@ let get_names env sigma sign eqns = (* Otherwise, we take names from the parameters of the constructor but avoiding conflicts with user ids *) let allvars = - List.fold_left (fun l (_,_,eqn) -> List.union Id.equal l eqn.rhs.avoid_ids) - [] eqns in + List.fold_left (fun l (_,_,eqn) -> Id.Set.union l eqn.rhs.avoid_ids) + Id.Set.empty eqns in let names3,_ = List.fold_left2 (fun (l,avoid) d na -> @@ -757,7 +757,7 @@ let get_names env sigma sign eqns = (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) d na in - (na::l,(Name.get_id na)::avoid)) + (na::l,Id.Set.add (Name.get_id na) avoid)) ([],allvars) (List.rev sign) names2 in names3,aliasname @@ -999,8 +999,8 @@ let add_assert_false_case pb tomatch = in [ { patterns = pats; rhs = { rhs_env = pb.env; - rhs_vars = []; - avoid_ids = []; + rhs_vars = Id.Set.empty; + avoid_ids = Id.Set.empty; it = None }; alias_stack = Anonymous::aliasnames; eqn_loc = None; @@ -1570,10 +1570,12 @@ let matx_of_eqns env eqns = let build_eqn (loc,(ids,lpat,rhs)) = let initial_lpat,initial_rhs = lpat,rhs in let initial_rhs = rhs in + let avoid = ids_of_named_context_val (named_context_val env) in + let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = { rhs_env = env; rhs_vars = free_glob_vars initial_rhs; - avoid_ids = ids@(ids_of_named_context (named_context env)); + avoid_ids = avoid; it = Some initial_rhs } in { patterns = initial_lpat; alias_stack = []; @@ -1751,7 +1753,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = let build_inversion_problem loc env sigma tms t = let make_patvar t (subst,avoid) = let id = next_name_away (named_hd env sigma t Anonymous) avoid in - DAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in + DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in let rec reveal_pattern t (subst,avoid as acc) = match EConstr.kind sigma (whd_all env sigma t) with | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc @@ -1781,7 +1783,7 @@ let build_inversion_problem loc env sigma tms t = let d = LocalAssum (alias_of_pat pat,typ) in let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in - let avoid0 = ids_of_context env in + let avoid0 = vars_of_env env in (* [patl] is a list of patterns revealing the substructure of constructors present in the constraints on the type of the multiple terms t1..tn that are matched in the original problem; @@ -1823,7 +1825,7 @@ let build_inversion_problem loc env sigma tms t = rhs = { rhs_env = pb_env; (* we assume all vars are used; in practice we discard dependent vars so that the field rhs_vars is normally not used *) - rhs_vars = List.map fst subst; + rhs_vars = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty subst; avoid_ids = avoid; it = Some (lift n t) } } in (* [catch_all] is a catch-all default clause of the auxiliary @@ -1841,7 +1843,7 @@ let build_inversion_problem loc env sigma tms t = eqn_loc = None; used = ref false; rhs = { rhs_env = pb_env; - rhs_vars = []; + rhs_vars = Id.Set.empty; avoid_ids = avoid0; it = None } } ] in (* [pb] is the auxiliary pattern-matching serving as skeleton for the @@ -2085,7 +2087,7 @@ let prime avoid name = let make_prime avoid prevname = let previd, id = prime !avoid prevname in - avoid := id :: !avoid; + avoid := Id.Set.add id !avoid; previd, id let eq_id avoid id = @@ -2113,7 +2115,7 @@ let constr_of_pat env evdref arsign pat avoid = Name n -> name, avoid | Anonymous -> let previd, id = prime avoid (Name (Id.of_string "wildcard")) in - Name id, id :: avoid + Name id, Id.Set.add id avoid in ((DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid) @@ -2157,7 +2159,7 @@ let constr_of_pat env evdref arsign pat avoid = pat', sign, app, apptype, realargs, n, avoid | Name id -> let sign = LocalAssum (alias, lift m ty) :: sign in - let avoid = id :: avoid in + let avoid = Id.Set.add id avoid in let sign, i, avoid = try let env = push_rel_context sign env in @@ -2168,7 +2170,7 @@ let constr_of_pat env evdref arsign pat avoid = (lift 1 app) (* aliased term *) in let neq = eq_id avoid id in - LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, neq :: avoid + LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid with Reduction.NotConvertible -> sign, 1, avoid in (* Mark the equality as a hole *) @@ -2182,7 +2184,7 @@ let constr_of_pat env evdref arsign pat avoid = let eq_id avoid id = let hid = Id.of_string ("Heq_" ^ Id.to_string id) in let hid' = next_ident_away hid !avoid in - avoid := hid' :: !avoid; + avoid := Id.Set.add hid' !avoid; hid' let is_topvar sigma t = @@ -2278,7 +2280,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = (fun (idents, newpatterns, pats) pat arsign -> let pat', cpat, idents = constr_of_pat env evdref arsign pat idents in (idents, pat' :: newpatterns, cpat :: pats)) - ([], [], []) eqn.patterns sign + (Id.Set.empty, [], []) eqn.patterns sign in let newpatterns = List.rev newpatterns and opats = List.rev pats in let rhs_rels, pats, signlen = @@ -2379,8 +2381,8 @@ let abstract_tomatch env sigma tomatchs tycon = let name = next_ident_away (Id.of_string "filtered_var") names in (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, - name :: names, tycon) - ([], [], [], tycon) tomatchs + Id.Set.add name names, tycon) + ([], [], Id.Set.empty, tycon) tomatchs in List.rev prev, ctx, tycon let build_dependent_signature env evdref avoid tomatchs arsign = @@ -2502,7 +2504,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *) (* Build the dependent arity signature, the equalities which makes the first part of the predicate and their instantiations. *) - let avoid = [] in + let avoid = Id.Set.empty in build_dependent_signature env evdref avoid tomatchs arsign in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 428f64b99..7bdc604b8 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -49,16 +49,16 @@ val constr_of_pat : Evd.evar_map ref -> rel_context -> Glob_term.cases_pattern -> - Names.Id.t list -> + Names.Id.Set.t -> Glob_term.cases_pattern * (rel_context * constr * (types * constr list) * Glob_term.cases_pattern) * - Names.Id.t list + Names.Id.Set.t type 'a rhs = { rhs_env : env; - rhs_vars : Id.t list; - avoid_ids : Id.t list; + rhs_vars : Id.Set.t; + avoid_ids : Id.Set.t; it : 'a option} type 'a equation = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index fc0a650bc..7cfd2e27d 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -205,7 +205,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> let name' = - Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env)) + Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.vars_of_env env)) in let env' = push_rel (LocalAssum (name', a')) env in let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ca7f633dc..0973d73ee 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -178,7 +178,7 @@ let push_binder na1 na2 t ctx = let id2 = match na2 with | Name id2 -> id2 | Anonymous -> - let avoid = List.map pi2 ctx in + let avoid = Id.Set.of_list (List.map pi2 ctx) in Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in (na1, id2, t) :: ctx diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 5e1430741..f3e8e72bb 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -221,12 +221,12 @@ let lookup_name_as_displayed env sigma t s = | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | Cast (c,_,_) -> lookup avoid n c | _ -> None - in lookup (ids_of_named_context (named_context env)) 1 t + in lookup (Environ.ids_of_named_context_val (Environ.named_context_val env)) 1 t let lookup_index_as_renamed env sigma t n = let rec lookup n d c = match EConstr.kind sigma c with | Prod (name,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal [] name c' with + (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -236,7 +236,7 @@ let lookup_index_as_renamed env sigma t n = else lookup (n-1) (d+1) c') | LetIn (name,_,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal [] name c' with + (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with | (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -464,7 +464,7 @@ and detype_r d flags avoid env sigma t = (* Using a dash to be unparsable *) GEvar (Id.of_string_soft "CONTEXT-HOLE", []) else - GEvar (Id.of_string_soft ("INTERNAL#" ^ string_of_int n), []) + GEvar (Id.of_string_soft ("M" ^ string_of_int n), []) | Var id -> (try let _ = Global.lookup_named id in GRef (VarRef id, None) with Not_found -> GVar id) @@ -578,7 +578,7 @@ and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = Array.fold_left2 (fun (avoid, env, l) na ty -> let id = next_name_away na avoid in - (id::avoid, add_name (Name id) None ty env, id::l)) + (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 @@ -594,7 +594,7 @@ and detype_cofix d flags avoid env sigma n (names,tys,bodies) = Array.fold_left2 (fun (avoid, env, l) na ty -> let id = next_name_away na avoid in - (id::avoid, add_name (Name id) None ty env, id::l)) + (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 @@ -615,14 +615,14 @@ and share_names d flags n l avoid env sigma c t = | _ -> na in let t' = detype d flags avoid env sigma t in let id = next_name_away na avoid in - let avoid = id::avoid and env = add_name (Name id) None t env 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::avoid and env = add_name (Name id) (Some b) t' env 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 -> @@ -631,7 +631,7 @@ and share_names d flags n l avoid env sigma c t = | _, 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::avoid and env = add_name (Name id) None t' env 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 *) @@ -822,7 +822,7 @@ let rec subst_glob_constr subst = DAst.map (function | GRef (ref,u) as raw -> let ref',t = subst_global subst ref in if ref' == ref then raw else - DAst.get (detype Now false [] (Global.env()) Evd.empty (EConstr.of_constr t)) + DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t)) | GSort _ | GVar _ diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 67c852af3..b70bfd83c 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -35,16 +35,16 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr [isgoal] tells if naming must avoid global-level synonyms as intro does [ctx] gives the names of the free variables *) -val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr +val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> constr -> glob_constr -val detype : 'a delay -> ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> 'a glob_constr_g +val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> constr -> 'a glob_constr_g val detype_sort : evar_map -> sorts -> glob_sort -val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> +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 detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr +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 *) val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 7f5a780f9..5f12f360b 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -72,7 +72,7 @@ let define_pure_evar_as_product evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in + let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in let s = destSort evd concl in let evd1,(dom,u1) = @@ -127,7 +127,7 @@ let define_pure_evar_as_lambda env evd evk = | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ | _ -> error_not_product env evd typ in - let avoid = ids_of_named_context (evar_context evi) in + let avoid = Environ.ids_of_named_context_val evi.evar_hyps in let id = next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in let newenv = push_named (LocalAssum (id, dom)) evenv in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ef0fb8ea6..ad1409f5b 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -679,6 +679,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let filter1 = evar_filter evi1 in let src = subterm_source evk1 evi1.evar_source in let ids1 = List.map get_id (named_context_of_val sign1) in + let avoid = Environ.ids_of_named_context_val sign1 in let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in let open Context.Rel.Declaration in let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) = @@ -700,9 +701,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = (push_named_context_val d' sign, Filter.extend 1 filter, (mkRel 1)::(List.map (lift 1) inst_in_env), (mkRel 1)::(List.map (lift 1) inst_in_sign), - push_rel d env,evd,id::avoid)) + push_rel d env,evd,Id.Set.add id avoid)) rel_sign - (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1) + (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid) in let evd,ev2ty_in_sign = let s = Retyping.get_sort_of env evd ty_in_env in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index e1576b971..7804cc679 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -273,17 +273,17 @@ let free_glob_vars = | _ -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vs = vars Id.Set.empty Id.Set.empty rt in - Id.Set.elements vs + vs let glob_visible_short_qualid c = let rec aux acc c = match DAst.get c with | GRef (c,_) -> let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in let dir,id = Libnames.repr_qualid qualid in - if DirPath.is_empty dir then id :: acc else acc + if DirPath.is_empty dir then Id.Set.add id acc else acc | _ -> fold_glob_constr aux acc c - in aux [] c + in aux Id.Set.empty c let warn_variable_collision = let open Pp in diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index bacc8fbe4..49ea9727c 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -43,11 +43,11 @@ val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> 'a glob_constr_g -> bool -val free_glob_vars : 'a glob_constr_g -> Id.t list +val free_glob_vars : 'a glob_constr_g -> Id.Set.t val bound_glob_vars : glob_constr -> Id.Set.t (* Obsolete *) val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option -val glob_visible_short_qualid : 'a glob_constr_g -> Id.t list +val glob_visible_short_qualid : 'a glob_constr_g -> Id.Set.t (* Renaming free variables using a renaming map; fails with [UnsoundRenaming] if applying the renaming would introduce diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f090921e5..d52c3932d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1616,7 +1616,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let id = let t = match ty with Some t -> t | None -> get_type_of env sigma c in let x = id_of_name_using_hdchar (Global.env()) sigma t name in - let ids = ids_of_named_context (named_context env) in + let ids = Environ.ids_of_named_context_val (named_context_val env) in if name == Anonymous then next_ident_away_in_goal x ids else if mem_named_context_val x (named_context_val env) then user_err ~hdr:"Unification.make_abstraction_core" diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f371fb08c..10dd42ea9 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -718,10 +718,7 @@ open Decl_kinds match o with | None -> (match opac with | Transparent -> keyword "Defined" - | Opaque None -> keyword "Qed" - | Opaque (Some l) -> - keyword "Qed" ++ spc() ++ str"export" ++ - prlist_with_sep (fun () -> str", ") pr_lident l) + | Opaque -> keyword "Qed") | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id ) | VernacExactProof c -> diff --git a/printing/printmod.ml b/printing/printmod.ml index 219eafda4..755e905a7 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -64,9 +64,10 @@ let get_new_id locals id = if not (Nametab.exists_module dir) then id else - get_id (id::l) (Namegen.next_ident_away id l) + get_id (Id.Set.add id l) (Namegen.next_ident_away id l) in - get_id (List.map snd locals) id + let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in + get_id avoid id (** Inductive declarations *) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ea60be31f..5ef7fac81 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -557,7 +557,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function let clause = mk_clenv_from_env env sigma n (c,t) in clenv_constrain_dep_args hyps_only largs clause | ExplicitBindings lbind -> - let t = rename_bound_vars_as_displayed sigma [] [] t in + let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in let clause = mk_clenv_from_env env sigma n (c, t) in clenv_match_args lbind clause @@ -605,7 +605,7 @@ let make_evar_clause env sigma ?len t = | Some n -> assert (0 <= n); n in (** FIXME: do the renaming online *) - let t = rename_bound_vars_as_displayed sigma [] [] t in + let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in let rec clrec (sigma, holes) n t = if n = 0 then (sigma, holes, t) else match EConstr.kind sigma t with diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a4d662e0a..a8ec4d8ca 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -64,15 +64,11 @@ let pf_get_hyp_typ gls id = id |> pf_get_hyp gls |> NamedDecl.get_type let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) +let pf_ids_set_of_hyps gls = + Environ.ids_of_named_context_val (Environ.named_context_val (pf_env gls)) let pf_get_new_id id gls = - next_ident_away id (pf_ids_of_hyps gls) - -let pf_get_new_ids ids gls = - let avoid = pf_ids_of_hyps gls in - List.fold_right - (fun id acc -> (next_ident_away id (acc@avoid))::acc) - ids [] + next_ident_away id (pf_ids_set_of_hyps gls) let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) @@ -177,8 +173,14 @@ module New = struct let hyps = Proofview.Goal.hyps gl in ids_of_named_context hyps + let pf_ids_set_of_hyps gl = + (** We only get the identifiers in [hyps] *) + let gl = Proofview.Goal.assume gl in + let env = Proofview.Goal.env gl in + Environ.ids_of_named_context_val (Environ.named_context_val env) + let pf_get_new_id id gl = - let ids = pf_ids_of_hyps gl in + let ids = pf_ids_set_of_hyps gl in next_ident_away id ids let pf_get_hyp id gl = diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 93bf428fd..7e6d83b10 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -48,7 +48,6 @@ val pf_get_hyp : goal sigma -> Id.t -> named_declaration val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t -val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr @@ -120,6 +119,7 @@ module New : sig val pf_get_new_id : identifier -> 'a Proofview.Goal.t -> identifier val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list + val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 31ede2d8b..5d9b595d3 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -237,7 +237,7 @@ module Make(T : Task) = struct type queue = { active : Pool.pool; queue : (T.task * expiration) TQueue.t; - cleaner : Thread.t; + cleaner : Thread.t option; } let create size = @@ -250,7 +250,7 @@ module Make(T : Task) = struct { active = Pool.create queue ~size; queue; - cleaner = Thread.create cleaner queue; + cleaner = if size > 0 then Some (Thread.create cleaner queue) else None; } let destroy { active; queue } = diff --git a/stm/stm.ml b/stm/stm.ml index e0064df9b..7c44fc86f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1385,7 +1385,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) { verbose = false; loc; indentation = 0; strlen = 0; - expr = (VernacEndProof (Proved (Opaque None,None))) }) in + expr = (VernacEndProof (Proved (Opaque,None))) }) in ignore(Future.join checked_proof); end; RespBuiltProof(proof,time) @@ -1525,7 +1525,7 @@ end = struct (* {{{ *) Reach.known_state ~cache:`No start; stm_vernac_interp stop ~proof { verbose = false; loc; indentation = 0; strlen = 0; - expr = (VernacEndProof (Proved (Opaque None,None))) }; + expr = (VernacEndProof (Proved (Opaque,None))) }; `OK proof end with e -> @@ -1976,7 +1976,6 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in let rec is_defined_expr = function - | VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) -> true | VernacTime (_, e) -> is_defined_expr e | VernacRedirect (_, (_, e)) -> is_defined_expr e | VernacTimeout (_, e) -> is_defined_expr e @@ -2001,24 +2000,24 @@ let collect_proof keep cur hd brkind id = | { expr = (VernacRequire _ | VernacImport _) } -> true | ast -> may_pierce_opaque ast in let parent = function Some (p, _) -> p | None -> assert false in - let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in + let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in let rec collect last accn id = let view = VCS.visit id in match view.step with | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x }) - when too_complex_to_delegate x -> `Sync(no_name,None,`Print) + when too_complex_to_delegate x -> `Sync(no_name,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) - | `Alias _ -> `Sync (no_name,None,`Alias) + | `Alias _ -> `Sync (no_name,`Alias) | `Fork((_,_,_,_::_::_), _) -> - `Sync (no_name,proof_using_ast last,`MutualProofs) + `Sync (no_name,`MutualProofs) | `Fork((_,_,Doesn'tGuaranteeOpacity,_), _) -> - `Sync (no_name,proof_using_ast last,`Doesn'tGuaranteeOpacity) + `Sync (no_name,`Doesn'tGuaranteeOpacity) | `Fork((_,hd',GuaranteesOpacity,ids), _) when has_proof_using last -> assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in - `ASync (parent last,proof_using_ast last,accn,name,delegate name) + `ASync (parent last,accn,name,delegate name) | `Fork((_, hd', GuaranteesOpacity, ids), _) when has_proof_no_using last && not (State.is_cached_and_valid (parent last)) && !Flags.compilation_mode = Flags.BuildVio -> @@ -2027,31 +2026,32 @@ let collect_proof keep cur hd brkind id = let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in v.expr <- VernacProof(t, Some hint); - `ASync (parent last,proof_using_ast last,accn,name,delegate name) + `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in - `MaybeASync (parent last, None, accn, name, delegate name)) + `MaybeASync (parent last, accn, name, delegate name)) | `Fork((_, hd', GuaranteesOpacity, ids), _) -> assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in - `MaybeASync (parent last, None, accn, name, delegate name) + `MaybeASync (parent last, accn, name, delegate name) | `Sideff _ -> warn_deprecated_nested_proofs (); - `Sync (no_name,None,`NestedProof) - | _ -> `Sync (no_name,None,`Unknown) in + `Sync (no_name,`NestedProof) + | _ -> `Sync (no_name,`Unknown) in let make_sync why = function - | `Sync(name,pua,_) -> `Sync (name,pua,why) - | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,why) - | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in + | `Sync(name,_) -> `Sync (name,why) + | `MaybeASync(_,_,name,_) -> `Sync (name,why) + | `ASync(_,_,name,_) -> `Sync (name,why) in + let check_policy rc = if async_policy () then rc else make_sync `Policy rc in match cur, (VCS.visit id).step, brkind with | (parent, { expr = VernacExactProof _ }), `Fork _, _ | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ -> - `Sync (no_name,None,`Immediate) + `Sync (no_name,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) | _ -> - if is_defined cur then `Sync (no_name,None,`Transparent) - else if keep == VtDrop then `Sync (no_name,None,`Aborted) + if is_defined cur then `Sync (no_name,`Transparent) + else if keep == VtDrop then `Sync (no_name,`Aborted) else let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc @@ -2223,7 +2223,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (block_start, pua, nodes, name, delegate) -> (fun () -> + | `ASync (block_start, nodes, name, delegate) -> (fun () -> assert(keep == VtKeep || keep == VtKeepAsAxiom); let drop_pt = keep == VtKeepAsAxiom in let block_stop, exn_info, loc = eop, (id, eop), x.loc in @@ -2270,10 +2270,10 @@ let known_state ?(redefine_qed=false) ~cache id = end; Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true - | `Sync (name, _, `Immediate) -> (fun () -> + | `Sync (name, `Immediate) -> (fun () -> reach eop; stm_vernac_interp id x; Proof_global.discard_all () ), `Yes, true - | `Sync (name, pua, reason) -> (fun () -> + | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; reach eop; let wall_clock = Unix.gettimeofday () in @@ -2298,12 +2298,12 @@ let known_state ?(redefine_qed=false) ~cache id = (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); Proof_global.discard_all () ), `Yes, true - | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () -> + | `MaybeASync (start, nodes, name, delegate) -> (fun () -> reach ~cache:`Shallow start; (* no sections *) if CList.is_empty (Environ.named_context (Global.env ())) - then Util.pi1 (aux (`ASync (start, pua, nodes, name, delegate))) () - else Util.pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) () + then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) () + else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) () ), (if redefine_qed then `No else `Yes), true in aux (collect_proof keep (view.next, x) brname brinfo eop) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index e16fcec7c..d912decff 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -73,7 +73,7 @@ let generalize_right mk typ c1 c2 = let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in Refine.refine ~typecheck:false begin fun sigma -> - let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in + let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in (sigma, mkApp (x, [|c2|])) @@ -114,7 +114,7 @@ let idx = Id.of_string "x" let idy = Id.of_string "y" let mkGenDecideEqGoal rectype ops g = - let hypnames = pf_ids_of_hyps g in + let hypnames = pf_ids_set_of_hyps g in let xname = next_ident_away idx hypnames and yname = next_ident_away idy hypnames in (mkNamedProd xname rectype diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index ce57682c6..bfbac7787 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -64,7 +64,7 @@ module RelDecl = Context.Rel.Declaration let hid = Id.of_string "H" let xid = Id.of_string "X" let default_id_of_sort = function InProp | InSet -> hid | InType -> xid -let fresh env id = next_global_ident_away id [] +let fresh env id = next_global_ident_away id Id.Set.empty let with_context_set ctx (b, ctx') = (b, Univ.ContextSet.union ctx ctx') diff --git a/tactics/equality.ml b/tactics/equality.ml index 3ea9538f3..e33dd2e5e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1003,7 +1003,7 @@ let apply_on_clause (f,t) clause = let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> - let e = next_ident_away eq_baseid (ids_of_context env) in + let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in let discriminator = try @@ -1371,7 +1371,7 @@ let simplify_args env sigma t = | _ -> t let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = - let e = next_ident_away eq_baseid (ids_of_context env) in + let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (e,t)) env in let evdref = ref sigma in let filter (cpath, t1', t2') = diff --git a/tactics/inv.ml b/tactics/inv.ml index 9495ca9c5..f391382bf 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -387,7 +387,7 @@ let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.enter begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in let first_eq = ref MoveLast in - let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in + let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with | Some thin -> tclTHENLIST diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 7c488f524..cc9d98f6f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -142,7 +142,7 @@ let rec add_prods_sign env sigma t = let compute_first_inversion_scheme env sigma ind sort dep_option = let indf,realargs = dest_ind_type ind in - let allvars = ids_of_context env in + let allvars = vars_of_env env in let p = next_ident_away (Id.of_string "P") allvars in let pty,goal = if dep_option then @@ -214,7 +214,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in - let avoid = ref [] in + let avoid = ref Id.Set.empty in let { sigma=sigma } = Proof.V82.subgoals pf in let sigma = Evd.nf_constraints sigma in let rec fill_holes c = @@ -222,7 +222,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = | Evar (e,args) -> let h = next_ident_away (Id.of_string "H") !avoid in let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in - avoid := h::!avoid; + avoid := Id.Set.add h !avoid; ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign; applist (mkVar h, inst) | _ -> EConstr.map sigma fill_holes c diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f1dd61358..d6c24e9cc 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -384,7 +384,9 @@ let rename_hyp repl = (**************************************************************) let fresh_id_in_env avoid id env = - next_ident_away_in_goal id (avoid@ids_of_named_context (named_context env)) + let avoid' = ids_of_named_context_val (named_context_val env) in + let avoid = if Id.Set.is_empty avoid then avoid' else Id.Set.union avoid' avoid in + next_ident_away_in_goal id avoid let fresh_id avoid id gl = fresh_id_in_env avoid id (pf_env gl) @@ -412,12 +414,12 @@ let default_id env sigma decl = possibly a move to do after the introduction *) type name_flag = - | NamingAvoid of Id.t list - | NamingBasedOn of Id.t * Id.t list + | NamingAvoid of Id.Set.t + | NamingBasedOn of Id.t * Id.Set.t | NamingMustBe of Id.t Loc.located let naming_of_name = function - | Anonymous -> NamingAvoid [] + | Anonymous -> NamingAvoid Id.Set.empty | Name id -> NamingMustBe (Loc.tag id) let find_name mayrepl decl naming gl = match naming with @@ -429,7 +431,7 @@ let find_name mayrepl decl naming gl = match naming with | NamingBasedOn (id,idl) -> new_fresh_id idl id gl | NamingMustBe (loc,id) -> (* When name is given, we allow to hide a global name *) - let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in + let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in let id' = next_ident_away id ids_of_hyps in if not mayrepl && not (Id.equal id' id) then user_err ?loc (pr_id id ++ str" is already used."); @@ -603,7 +605,7 @@ let fix ido n = match ido with | None -> Proofview.Goal.enter begin fun gl -> let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id [] name gl in + let id = new_fresh_id Id.Set.empty name gl in mutual_fix id n [] 0 end | Some id -> @@ -654,7 +656,7 @@ let cofix ido = match ido with | None -> Proofview.Goal.enter begin fun gl -> let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id [] name gl in + let id = new_fresh_id Id.Set.empty name gl in mutual_cofix id [] 0 end | Some id -> @@ -975,13 +977,13 @@ let unfold_constr = function the type to build hyp names, we maintain an environment to be able to type dependent hyps. *) let find_intro_names ctxt gl = - let _, res = List.fold_right + let _, res, _ = List.fold_right (fun decl acc -> - let env,idl = acc in - let name = fresh_id idl (default_id env gl.sigma decl) gl in + let env,idl,avoid = acc in + let name = fresh_id avoid (default_id env gl.sigma decl) gl in let newenv = push_rel decl env in - (newenv,(name::idl))) - ctxt (pf_env gl , []) in + (newenv, name :: idl, Id.Set.add name avoid)) + ctxt (pf_env gl, [], Id.Set.empty) in List.rev res let build_intro_tac id dest tac = match dest with @@ -1021,18 +1023,18 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) let intro_mustbe_force id = intro_gen (NamingMustBe (Loc.tag id)) MoveLast true false -let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false +let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false -let intro_then = intro_then_gen (NamingAvoid []) MoveLast false false -let intro = intro_gen (NamingAvoid []) MoveLast false false -let introf = intro_gen (NamingAvoid []) MoveLast true false +let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false +let intro = intro_gen (NamingAvoid Id.Set.empty) MoveLast false false +let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false let intro_move_avoid idopt avoid hto = match idopt with | None -> intro_gen (NamingAvoid avoid) hto true false | Some id -> intro_gen (NamingMustBe (Loc.tag id)) hto true false -let intro_move idopt hto = intro_move_avoid idopt [] hto +let intro_move idopt hto = intro_move_avoid idopt Id.Set.empty hto (**** Multiple introduction tactics ****) @@ -1264,7 +1266,7 @@ let cut c = with e when Pretype_errors.precatchable_exception e -> false in if is_sort then - let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in + let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in (** Backward compat: normalize [c]. *) let c = if normalize_cut then local_strong whd_betaiota sigma c else c in Refine.refine ~typecheck:false begin fun h -> @@ -1763,7 +1765,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in let tac = if with_destruct then - descend_in_conjunctions [] + descend_in_conjunctions Id.Set.empty (fun b id -> Tacticals.New.tclTHEN (try_main_apply b (mkVar id)) @@ -1912,7 +1914,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming ]) with e when with_destruct && CErrors.noncritical e -> let (e, info) = CErrors.push e in - (descend_in_conjunctions [targetid] + (descend_in_conjunctions (Id.Set.singleton targetid) (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) end @@ -2392,15 +2394,16 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = let prepare_naming ?loc = function | IntroIdentifier id -> NamingMustBe (Loc.tag ?loc id) - | IntroAnonymous -> NamingAvoid [] - | IntroFresh id -> NamingBasedOn (id,[]) + | IntroAnonymous -> NamingAvoid Id.Set.empty + | IntroFresh id -> NamingBasedOn (id, Id.Set.empty) let rec explicit_intro_names = function | (_, IntroForthcoming _) :: l -> explicit_intro_names l -| (_, IntroNaming (IntroIdentifier id)) :: l -> id :: explicit_intro_names l +| (_, IntroNaming (IntroIdentifier id)) :: l -> Id.Set.add id (explicit_intro_names l) | (_, IntroAction (IntroOrAndPattern l)) :: l' -> let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in - List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll) + let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in + List.fold_left fold Id.Set.empty ll | (_, IntroAction (IntroInjection l)) :: l' -> explicit_intro_names (l@l') | (_, IntroAction (IntroApplyOn (c,pat))) :: l' -> @@ -2408,7 +2411,7 @@ let rec explicit_intro_names = function | (_, (IntroNaming (IntroAnonymous | IntroFresh _) | IntroAction (IntroWildcard | IntroRewrite _))) :: l -> explicit_intro_names l -| [] -> [] +| [] -> Id.Set.empty let rec check_name_unicity env ok seen = function | (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l @@ -2455,8 +2458,8 @@ let make_tmp_naming avoid l = function IntroAnonymous, but at the cost of a "renaming"; Note that in the case of IntroFresh, we should use check_thin_clash_then anyway to prevent the case of an IntroFresh precisely using the wild_id *) - | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l) - | pat -> NamingAvoid(avoid@explicit_intro_names ((Loc.tag @@ IntroAction pat)::l)) + | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l)) + | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((Loc.tag @@ IntroAction pat)::l))) let fit_bound n = function | None -> true @@ -2497,7 +2500,7 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac = if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else match pat with | IntroForthcoming onlydeps -> - intro_forthcoming_then_gen (NamingAvoid (avoid@explicit_intro_names l)) + intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) destopt onlydeps n bound (fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound (n+List.length ids) tac l) @@ -2520,12 +2523,12 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac intro_then_gen (NamingMustBe (loc,id)) destopt true false (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)) | IntroAnonymous -> - intro_then_gen (NamingAvoid (avoid@explicit_intro_names l)) + intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) destopt true false (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l) | IntroFresh id -> (* todo: avoid thinned names to interfere with generation of fresh name *) - intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l)) + intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))) destopt true false (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l) @@ -2559,7 +2562,7 @@ and prepare_intros ?loc with_evars dft destopt = function | IntroAction ipat -> prepare_naming ?loc dft, (let tac thin bound = - intro_patterns_core with_evars true [] [] thin destopt bound 0 + intro_patterns_core with_evars true Id.Set.empty [] thin destopt bound 0 (fun _ l -> clear_wildcards l) in fun id -> intro_pattern_action ?loc with_evars true true ipat [] destopt tac id) @@ -2570,7 +2573,7 @@ let intro_patterns_head_core with_evars b destopt bound pat = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in check_name_unicity env [] [] pat; - intro_patterns_core with_evars b [] [] [] destopt + intro_patterns_core with_evars b Id.Set.empty [] [] destopt bound 0 (fun _ l -> clear_wildcards l) pat end @@ -2682,8 +2685,8 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let (sigma, (newcl, eq_tac)) = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with - | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl - | IntroFresh heq_base -> new_fresh_id [id] heq_base gl + | IntroAnonymous -> new_fresh_id (Id.Set.singleton id) (add_prefix "Heq" id) gl + | IntroFresh heq_base -> new_fresh_id (Id.Set.singleton id) heq_base gl | IntroIdentifier id -> id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in @@ -2735,8 +2738,8 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with - | IntroAnonymous -> fresh_id_in_env [id] (add_prefix "Heq" id) env - | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env + | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env + | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env | IntroIdentifier id -> if List.mem id (ids_of_named_context (named_context env)) then user_err ?loc (pr_id id ++ str" is already used."); @@ -3143,13 +3146,13 @@ let rec consume_pattern avoid na isdep gl = function | (loc,IntroForthcoming true)::names when not isdep -> consume_pattern avoid na isdep gl names | (loc,IntroForthcoming _)::names as fullpat -> - let avoid = avoid@explicit_intro_names names in + let avoid = Id.Set.union avoid (explicit_intro_names names) in ((loc,intropattern_of_name gl avoid na), fullpat) | (loc,IntroNaming IntroAnonymous)::names -> - let avoid = avoid@explicit_intro_names names in + let avoid = Id.Set.union avoid (explicit_intro_names names) in ((loc,intropattern_of_name gl avoid na), names) | (loc,IntroNaming (IntroFresh id'))::names -> - let avoid = avoid@explicit_intro_names names in + let avoid = Id.Set.union avoid (explicit_intro_names names) in ((loc,IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl))), names) | pat::names -> (pat,names) @@ -3207,7 +3210,7 @@ let get_recarg_dest (recargdests,tophyp) = *) let induct_discharge with_evars dests avoid' tac (avoid,ra) names = - let avoid = avoid @ avoid' in + let avoid = Id.Set.union avoid avoid' in let rec peel_tac ra dests names thin = match ra with | (RecArg,_,deprec,recvarname) :: @@ -3303,7 +3306,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = (* Based on the knowledge given by the user, all constraints on the variable are generalizable in the current environment so that it is clearable after destruction *) - atomize_one (i-1) (c::args) (c::args') (id::avoid) + atomize_one (i-1) (c::args) (c::args') (Id.Set.add id avoid) | _ -> let c' = expand_projections env' sigma c in let dependent t = dependent sigma c t in @@ -3328,9 +3331,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) - (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (x::avoid)) + (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (Id.Set.add x avoid)) in - atomize_one (List.length argl) [] [] [] + atomize_one (List.length argl) [] [] Id.Set.empty end (* [cook_sign] builds the lists [beforetoclear] (preceding the @@ -3402,7 +3405,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = (* First phase from L to R: get [toclear], [decldep] and [statuslist] for the hypotheses before (= more ancient than) hyp0 (see above) *) let toclear = ref [] in - let avoid = ref [] in + let avoid = ref Id.Set.empty in let decldeps = ref [] in let ldeps = ref [] in let rstatus = ref [] in @@ -3419,7 +3422,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = is one of indvars too *) toclear := hyp::!toclear; MoveFirst (* fake value *) - end else if Id.List.mem hyp indvars then begin + end else if Id.Set.mem hyp indvars then begin (* The variables in indvars are such that they don't occur any more after generalization, so declare them to clear. *) toclear := hyp::!toclear; @@ -3429,14 +3432,14 @@ let cook_sign hyp0_opt inhyps indvars env sigma = (Option.cata (fun id -> occur_var_in_decl env sigma id decl) false hyp0_opt) in let depother = List.is_empty inhyps && - (List.exists (fun id -> occur_var_in_decl env sigma id decl) indvars || + (Id.Set.exists (fun id -> occur_var_in_decl env sigma id decl) indvars || List.exists (fun decl' -> occur_var_in_decl env sigma (NamedDecl.get_id decl') decl) !decldeps) in if not (List.is_empty inhyps) && Id.List.mem hyp inhyps || dephyp0 || depother then begin decldeps := decl::!decldeps; - avoid := hyp::!avoid; + avoid := Id.Set.add hyp !avoid; maindep := dephyp0 || !maindep; if !before then begin toclear := hyp::!toclear; @@ -3560,15 +3563,15 @@ let make_up_names n ind_opt cname = else add_prefix ind_prefix cname in let hyprecname = make_base n base_ind in let avoid = - if Int.equal n 1 (* Only one recursive argument *) || Int.equal n 0 then [] + if Int.equal n 1 (* Only one recursive argument *) || Int.equal n 0 then Id.Set.empty else (* Forbid to use cname, cname0, hyprecname and hyprecname0 *) (* in order to get names such as f1, f2, ... *) let avoid = - (make_ident (Id.to_string hyprecname) None) :: - (make_ident (Id.to_string hyprecname) (Some 0)) :: [] in + Id.Set.add (make_ident (Id.to_string hyprecname) None) + (Id.Set.singleton (make_ident (Id.to_string hyprecname) (Some 0))) in if not (String.equal (atompart_of_id cname) "H") then - (make_ident base (Some 0)) :: (make_ident base None) :: avoid + Id.Set.add (make_ident base (Some 0)) (Id.Set.add (make_ident base None) avoid) else avoid in Id.of_string base, hyprecname, avoid @@ -3727,10 +3730,10 @@ let abstract_args gl generalize_vars dep id defined f args = let env = Tacmach.New.pf_env gl in let concl = Tacmach.New.pf_concl gl in let dep = dep || local_occur_var !sigma id concl in - let avoid = ref [] in + let avoid = ref Id.Set.empty in let get_id name = let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in - avoid := id :: !avoid; id + avoid := Id.Set.add id !avoid; id in (* Build application generalized w.r.t. the argument plus the necessary eqs. From env |- c : forall G, T and args : G we build @@ -4154,7 +4157,7 @@ let given_elim hyp0 (elimc,lbind as e) gl = Tacmach.New.project gl, (e, elimt), ind_type_guess type scheme_signature = - (Id.t list * (elim_arg_kind * bool * bool * Id.t) list) array + (Id.Set.t * (elim_arg_kind * bool * bool * Id.t) list) array type eliminator_source = | ElimUsing of (eliminator * EConstr.types) * scheme_signature @@ -4345,7 +4348,7 @@ let induction_without_atomization isrec with_evars elim names lid = gt_wf_rec was taken as a functional scheme with no parameters, but by chance, because of the addition of at least hyp0 for cook_sign, it behaved as if there was a real induction arg. *) - if indvars = [] then [List.hd lid_params] else indvars in + if List.is_empty indvars then Id.Set.singleton (List.hd lid_params) else Id.Set.of_list indvars in let induct_tac elim = Tacticals.New.tclTHENLIST [ (* pattern to make the predicate appear. *) reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl; @@ -4541,7 +4544,7 @@ let induction_gen clear_flag isrec with_evars elim let id = (* Type not the right one if partially applied but anyway for internal use*) let x = id_of_name_using_hdchar env evd t Anonymous in - new_fresh_id [] x gl in + new_fresh_id Id.Set.empty x gl in let info_arg = (is_arg_pure_hyp, not enough_applied) in pose_induction_arg_then isrec with_evars info_arg elim id arg t inhyps cls @@ -4580,7 +4583,7 @@ let induction_gen_l isrec with_evars elim names lc = let x = id_of_name_using_hdchar env sigma (type_of c) Anonymous in - let id = new_fresh_id [] x gl in + let id = new_fresh_id Id.Set.empty x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in let _ = newlc:=id::!newlc in Tacticals.New.tclTHEN @@ -5017,7 +5020,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = then (s1,push_named_context_val d s2) else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, empty_named_context_val) in - let id = next_global_ident_away id (pf_ids_of_hyps gl) in + let id = next_global_ident_away id (pf_ids_set_of_hyps gl) in let concl = match goal_type with | None -> Proofview.Goal.concl gl | Some ty -> ty in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index bca0c4c50..e07d514cd 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -49,18 +49,18 @@ val convert_leq : constr -> constr -> unit Proofview.tactic (** {6 Introduction tactics. } *) -val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t -val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t +val fresh_id_in_env : Id.Set.t -> Id.t -> env -> Id.t +val fresh_id : Id.Set.t -> Id.t -> goal sigma -> Id.t val find_intro_names : rel_context -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic val intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic -val intro_move_avoid : Id.t option -> Id.t list -> Id.t move_location -> unit Proofview.tactic +val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic (** [intro_avoiding idl] acts as intro but prevents the new Id.t to belong to [idl] *) -val intro_avoiding : Id.t list -> unit Proofview.tactic +val intro_avoiding : Id.Set.t -> unit Proofview.tactic val intro_replacing : Id.t -> unit Proofview.tactic val intro_using : Id.t -> unit Proofview.tactic diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 803fe8029..c4bd11c57 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -2,6 +2,7 @@ set -e set -o pipefail export PATH=$COQBIN:$PATH +export LC_ALL=C rm -rf theories src Makefile Makefile.conf tmp git clean -dfx || true diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v deleted file mode 100644 index b3e41ab1f..000000000 --- a/test-suite/success/qed_export.v +++ /dev/null @@ -1,18 +0,0 @@ -Lemma a : True. -Proof. -assert True as H. - abstract (trivial) using exported_seff. -exact H. -Fail Qed exporting a_subproof. -Qed exporting exported_seff. -Check ( exported_seff : True ). - -Lemma b : True. -Proof. -assert True as H. - abstract (trivial) using exported_seff2. -exact H. -Qed. - -Fail Check ( exported_seff2 : True ). - diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index de76bf98b..4a9d871fd 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -274,7 +274,7 @@ let generate_conf oc project args = ;; let ensure_root_dir - ({ ml_includes; r_includes; + ({ ml_includes; r_includes; q_includes; v_files; ml_files; mli_files; ml4_files; mllib_files; mlpack_files } as project) = @@ -283,6 +283,7 @@ let ensure_root_dir let not_tops = List.for_all (fun s -> s <> Filename.basename s) in if exists (fun { canonical_path = x } -> x = here) ml_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes + || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes || (not_tops v_files && not_tops mli_files && not_tops ml4_files && not_tops ml_files && not_tops mllib_files && not_tops mlpack_files) diff --git a/tools/coqwc.mll b/tools/coqwc.mll index a0b6bfbbe..6ddeeb9b2 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -94,7 +94,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036" let stars = "(*" '*'* "*)" let dot = '.' (' ' | '\t' | '\n' | '\r' | eof) let proof_start = - "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next" + "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" space+ (['0' - '9'])+ | "Next" space+ "Obligation" let def_start = "Definition" | "Fixpoint" | "Instance" let proof_end = diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 59920742d..503508fc0 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -533,7 +533,7 @@ open Namegen let compute_bl_goal ind lnamesparrec nparrec = let eqI, eff = eqI ind lnamesparrec in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in @@ -578,7 +578,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) in let fresh_id s gl = - let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in + let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in Proofview.Goal.enter begin fun gl -> @@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in let eqI, eff = eqI ind lnamesparrec in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and @@ -722,7 +722,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = ( List.map (fun (_,_,_,slb) -> slb) list_id ) in let fresh_id s gl = - let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in + let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in Proofview.Goal.enter begin fun gl -> @@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec = check_not_is_defined (); let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in @@ -870,7 +870,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ( List.map (fun (_,_,_,slb) -> slb) list_id ) in let fresh_id s gl = - let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in + let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in Proofview.Goal.enter begin fun gl -> diff --git a/vernac/classes.ml b/vernac/classes.ml index c21345a2a..0926c93e5 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -183,7 +183,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) id | Anonymous -> let i = Nameops.add_suffix (id_of_class k) "_instance_0" in - Namegen.next_global_ident_away i (Termops.ids_of_context env) + Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in evars := Evarutil.nf_evar_map !evars; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 4b36c2d07..2c8f6ec9d 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -211,7 +211,8 @@ let compute_proof_name locality = function user_err ?loc (pr_id id ++ str " already exists."); id | None -> - next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()) + let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in + next_global_ident_away default_thm_id avoid let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in @@ -309,12 +310,6 @@ let get_proof proof do_guard hook opacity = in id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook -let check_exist = - List.iter (fun (loc,id) -> - if not (Nametab.exists_cci (Lib.make_path id)) then - user_err ?loc (pr_id id ++ str " does not exist.") - ) - let universe_proof_terminator compute_guard hook = let open Proof_global in make_terminator begin function @@ -322,17 +317,16 @@ let universe_proof_terminator compute_guard hook = admit (id,k,pe) pl (hook (Some ctx)) (); Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> - let is_opaque, export_seff, exports = match opaque with - | Vernacexpr.Transparent -> false, true, [] - | Vernacexpr.Opaque None -> true, false, [] - | Vernacexpr.Opaque (Some l) -> true, true, l in + let is_opaque, export_seff = match opaque with + | Vernacexpr.Transparent -> false, true + | Vernacexpr.Opaque -> true, false + in let proof = get_proof proof compute_guard (hook (Some (fst proof.Proof_global.universes))) is_opaque in begin match idopt with | None -> save_named ~export_seff proof | Some (_,id) -> save_anonymous ~export_seff proof id - end; - check_exist exports + end end let standard_proof_terminator compute_guard hook = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 89b18d254..81218308f 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -846,9 +846,9 @@ let obligation_terminator name num guard hook auto pf = let obl = obls.(num) in let status = match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp () - | (true, _), Vernacexpr.Opaque _ -> err_not_transp () - | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true + | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () + | (true, _), Vernacexpr.Opaque -> err_not_transp () + | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false | (_, status), Vernacexpr.Transparent -> status in diff --git a/vernac/record.ml b/vernac/record.ml index 4fb607dec..18e7796ca 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -457,7 +457,7 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity let impls = implicits_of_context params in List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls in - let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in + let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in let impl, projs = match fields with | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ee84ff101..83296cf58 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -125,8 +125,8 @@ let make_cases_aux glob_ref = | [] -> [] | (n,_)::l -> let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in - Id.to_string n' :: rename (n'::avoid) l in - let al' = rename [] al in + Id.to_string n' :: rename (Id.Set.add n' avoid) l in + let al' = rename Id.Set.empty al in let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) tarr [] @@ -507,7 +507,7 @@ let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) let status = Pfedit.by (Tactics.exact_proof c) in - save_proof (Vernacexpr.(Proved(Opaque None,None))); + save_proof (Vernacexpr.(Proved(Opaque,None))); if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption locality poly (local, kind) l nl = @@ -1230,7 +1230,7 @@ let vernac_reserve bl = let env = Global.env() in let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in - let t = Detyping.detype Detyping.Now false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in + let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) (EConstr.of_constr t) in let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |