diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-09 14:46:37 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-09 14:46:37 +0200 |
| commit | 429f493997e34bfaac930c68bf6b267a5b9640ee (patch) | |
| tree | 28f15d0aeff2ce899a312f31e10fe2030b2dd813 | |
| parent | aeec29a177e8f1c89996c0449e4cd81ca3ca4377 (diff) | |
| parent | eaa3f9719d6190ba92ce55816f11c70b30434309 (diff) | |
Merge branch 'v8.5' into trunk
82 files changed, 3286 insertions, 923 deletions
@@ -258,9 +258,9 @@ Tactics - Behavior of introduction patterns -> and <- made more uniform (hypothesis is cleared, rewrite in hypotheses and conclusion and erasing the variable when rewriting a variable). -- Tactics from plugins are now active only when the corresponding - module is imported (source of incompatibilities, solvable by adding - an "Import", like e.g. "Import Omega"). +- Tactics from plugins are now active only when the corresponding module + is imported (source of incompatibilities, solvable by adding an "Import"; + in the particular case of Omega, use "Require Import OmegaTactic"). - Semantics of destruct/induction has been made more regular in some edge cases, possibly leading to incompatibilities: - new goals are now opened when the term does not match a subterm of @@ -306,10 +306,9 @@ Notations Tools -- Option -I now only adds directories to the ml path. To add to both - the load path and the ml path, use -I -as. -- Option -Q behaves as -I -as and -R, except that the logical path of - any loaded file has to be fully qualified. +- Option -I now only adds directories to the ml path. +- Option -Q behaves as -R, except that the logical path of any loaded file has + to be fully qualified. - Option -R no longer adds recursively to the ml path; only the root directory is added. (Behavior with respect to the load path is unchanged.) diff --git a/checker/checker.ml b/checker/checker.ml index ffe155319..9a1007acb 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -181,8 +181,7 @@ let print_usage_channel co command = " -I dir -as coqdir map physical dir to logical coqdir\ \n -I dir map directory dir to the empty logical path\ \n -include dir (idem)\ -\n -R dir -as coqdir recursively map physical dir to logical coqdir\ -\n -R dir coqdir (idem)\ +\n -R dir coqdir recursively map physical dir to logical coqdir\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index e802398b5..76bcaaae6 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -5,7 +5,7 @@ We present here the \Program\ tactic commands, used to build certified \Coq\ programs, elaborating them from their algorithmic skeleton and a -rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction +rich specification \cite{Sozeau06}. It can be thought of as a dual of extraction (see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the specification using the whole \Coq{} proof @@ -48,7 +48,7 @@ operation (see Section~\ref{Caseexpr}). | S n => u end. \end{coq_example*} -will be first rewrote to: +will be first rewritten to: \begin{coq_example*} (match x as y return (x = y -> _) with | 0 => fun H : x = 0 -> t @@ -108,7 +108,7 @@ goals to construct the final definitions. \subsection{\tt Program Definition {\ident} := {\term}. \comindex{Program Definition}\label{ProgramDefinition}} -This command types the value {\term} in \Russell\ and generate proof +This command types the value {\term} in \Russell\ and generates proof obligations. Once solved using the commands shown below, it binds the final \Coq\ term to the name {\ident} in the environment. diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 49bcdb1db..6335dfd32 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -29,9 +29,9 @@ for your platform, which is supposed in the following). By default, \verb!coqc! executes the native-code version; this can be overridden using the \verb!-byte! option. -The byte-code toplevel is based on a Caml +The byte-code toplevel is based on an {\ocaml} toplevel (to allow the dynamic link of tactics). You can switch to -the Caml toplevel with the command \verb!Drop.!, and come back to the +the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the \Coq~toplevel with the command \verb!Toplevel.loop();;!. \section{Batch compilation ({\tt coqc})} @@ -69,13 +69,13 @@ option \verb:-q:. Load path can be specified to the \Coq\ system by setting up \verb:$COQPATH: environment variable. It is a list of directories -separated by \verb|:| (\verb|;| on windows). {\Coq} will also honour -\verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see section +separated by \verb|:| (\verb|;| on windows). {\Coq} will also honor +\verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see Section \ref{loadpath}). Some {\Coq} commands call other {\Coq} commands. In this case, they look for the commands in directory specified by \verb:$COQBIN:. If -this variable is not set, they look for the command in the executable +this variable is not set, they look for the commands in the executable path. The \verb:$COQ_COLORS: environment variable can be used to specify the set of @@ -104,16 +104,16 @@ Add physical path {\em directory} to the {\ocaml} loadpath. Add physical path \emph{directory} to the list of directories where {\Coq} looks for a file and bind it to the the logical directory - \emph{dirpath}. The sub-directory structure of \emph{directory} is + \emph{dirpath}. The subdirectory structure of \emph{directory} is recursively available from {\Coq} using absolute names (extending the {\dirpath} prefix) (see Section~\ref{LongNames}). - + \SeeAlso Section~\ref{Libraries}. -\item[{\tt -R} {\em directory} {\dirpath}, {\tt -R} {\em directory} [{\tt -as} {\dirpath}]]\ +\item[{\tt -R} {\em directory} {\dirpath}]\ Do as \texttt{-Q} \emph{directory} {\dirpath} but make the - sub-directory structure of \emph{directory} recursively visible so + subdirectory structure of \emph{directory} recursively visible so that the recursive contents of physical \emph{directory} is available from {\Coq} using short or partially qualified names. @@ -126,9 +126,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath. \item[{\tt -exclude-dir} {\em subdirectory}]\ - This tells to exclude any sub-directory named {\em subdirectory} + This tells to exclude any subdirectory named {\em subdirectory} while processing option {\tt -R}. Without this option only the - conventional version control management sub-directories named {\tt + conventional version control management subdirectories named {\tt CVS} and {\tt \_darcs} are excluded. \item[{\tt -nois}]\ @@ -142,11 +142,11 @@ Add physical path {\em directory} to the {\ocaml} loadpath. \item[{\tt -load-ml-source} {\em file}]\ - Load the Caml source file {\em file}. + Load the {\ocaml} source file {\em file}. \item[{\tt -load-ml-object} {\em file}]\ - Load the Caml object file {\em file}. + Load the {\ocaml} object file {\em file}. \item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\ diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index d1ce3bf41..cc5239a77 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1059,44 +1059,53 @@ names to {\Coq} names is needed. In this translation, names in the file system are called {\em physical} paths while {\Coq} names are contrastingly called {\em logical} names. -A logical name {\tt Lib} can associated to a physical path +A logical prefix {\tt Lib} can be associated to a physical path \textrm{\textsl{path}} using the command line option {\tt -Q} -\textrm{\textsl{path}} {\tt Lib}. This associates a logical name to -all the compiled files in the directory tree rooted at -\textrm{\textsl{path}}. The name associated to the file {\tt - path/fOO/Bar/File.vo} is {\tt Lib.fOO.Bar.File}. Subdirectories +\textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are +recursively associated to the logical path {\tt Lib} extended with the +corresponding suffix coming from the physical path. For instance, the +folder {\tt path/fOO/Bar} maps to {\tt Lib.fOO.Bar}. Subdirectories corresponding to invalid {\Coq} identifiers are skipped, and, by convention, subdirectories named {\tt CVS} or {\tt \_darcs} are skipped too. -{\Coq} commands also associate automatically a logical path to files +Thanks to this mechanism, {\texttt{.vo}} files are made available through the +logical name of the folder they are in, extended with their own basename. For +example, the name associated to the file {\tt path/fOO/Bar/File.vo} is +{\tt Lib.fOO.Bar.File}. The same caveat applies for invalid identifiers. +When compiling a source file, the {\texttt{.vo}} file stores its logical name, +so that an error is issued if it is loaded with the wrong loadpath afterwards. + +Some folders have a special status and are automatically put in the path. +{\Coq} commands associate automatically a logical path to files in the repository trees rooted at the directory from where the command is launched, \textit{coqlib}\texttt{/user-contrib/}, the directories listed in the \verb:$COQPATH:, \verb:${XDG_DATA_HOME}/coq/: and \verb:${XDG_DATA_DIRS}/coq/: environment variables (see \url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}) -with the same $/ \to .$ convention but no prefix. - -The command line option \texttt{-R} is a variant of \texttt{-Q} that -associates to a physical path the same logical path as \texttt{-Q}, as -well as all suffixes of that logical path. The option \texttt{-R} -\textrm{\textsl{path}} \texttt{Lib} associates to -\texttt{path/fOO/Bar/File.vo} the logical names -\texttt{Lib.fOO.Bar.File}, \texttt{fOO.Bar.File}, \texttt{Bar.File} -and \texttt{File}. If several files with identical base name are -present in different subdirectories of a recursive loadpath, which of +with the same physical-to-logical translation and with an empty logical prefix. + +The command line option \texttt{-R} is a variant of \texttt{-Q} which has the +strictly same behavior regarding loadpaths, but which also makes the +corresponding \texttt{.vo} files available through their short names in a +way not unlike the {\tt Import} command (see~{\ref{Import}}). For instance, +\texttt{-R} \textrm{\textsl{path}} \texttt{Lib} associates to the file +\texttt{path/fOO/Bar/File.vo} the logical name \texttt{Lib.fOO.Bar.File}, but +allows this file to be accessed through the short names \texttt{fOO.Bar.File}, +\texttt{Bar.File} and \texttt{File}. If several files with identical base name +are present in different subdirectories of a recursive loadpath, which of these files is found first may be system-dependent and explicit -qualification is recommended. - -There are currently two loadpaths in {\Coq}. There is one loadpath -where seeking {\Coq} files (extensions \texttt{.v} or \texttt{.vo} or -\texttt{.vi}) whose management has been explained just above, and one -where seeking {\ocaml} files. The {\ocaml} loadpath is -managed using the option \texttt{-I path}. As in {\ocaml} world, there -is nether a notion of logical name prefix nor a way to access files in -subdirectories of \texttt{path}. See the command \texttt{Declare ML - Module} in Section~\ref{compiled} to understand the need of the -{\ocaml} loadpath. +qualification is recommended. The {\tt From} argument of the {\tt Require} +command can be used to bypass the implicit shortening by providing an absolute +root to the required file (see~\ref{Require}). + +There also exists another independent loadpath mechanism attached to {\ocaml} +object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files +as described above. The {\ocaml} loadpath is managed using the option +\texttt{-I path} (in the {\ocaml} world, there is neither a notion of logical +name prefix nor a way to access files in subdirectories of \texttt{path}). +See the command \texttt{Declare ML Module} in Section~\ref{compiled} to +understand the need of the {\ocaml} loadpath. See Section~\ref{coqoptions} for a more general view over the {\Coq} command line options. diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 48b9315e3..e56c8fa7f 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -3,7 +3,7 @@ \label{section:Modules}} The module system provides a way of packaging related elements -together, as well as a mean of massive abstraction. +together, as well as a means of massive abstraction. \begin{figure}[t] \begin{centerframe} diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex index 9ab8aded9..2019a529f 100644 --- a/doc/refman/RefMan-modr.tex +++ b/doc/refman/RefMan-modr.tex @@ -2,7 +2,7 @@ The module system extends the Calculus of Inductive Constructions providing a convenient way to structure large developments as well as -a mean of massive abstraction. +a means of massive abstraction. %It is described in details in Judicael's thesis and Jacek's thesis \section{Modules and module types} diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 556a2dab5..4952ed778 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -4,7 +4,7 @@ \section{Displaying} \subsection[\tt Print {\qualid}.]{\tt Print {\qualid}.\comindex{Print}} -This command displays on the screen informations about the declared or +This command displays on the screen information about the declared or defined object referred by {\qualid}. \begin{ErrMsgs} @@ -20,7 +20,7 @@ global constant. \item {\tt About {\qualid}.} \label{About} \comindex{About}\\ -This displays various informations about the object denoted by {\qualid}: +This displays various information about the object denoted by {\qualid}: its kind (module, constant, assumption, inductive, constructor, abbreviation, \ldots), long name, type, implicit arguments and argument scopes. It does not print the body of @@ -34,7 +34,7 @@ definitions or proofs. \end{Variants} \subsection[\tt Print All.]{\tt Print All.\comindex{Print All}} -This command displays informations about the current state of the +This command displays information about the current state of the environment, including sections and modules. \begin{Variants} @@ -183,7 +183,7 @@ displayed as in \Coq\ terms. \begin{Variants} \item \texttt{Recursive Extraction} {\qualid$_1$} \ldots{} {\qualid$_n$}{\tt .}\\ Recursively extracts all the material needed for the extraction of - globals {\qualid$_1$}, \ldots, {\qualid$_n$}. + global {\qualid$_1$}, \ldots, {\qualid$_n$}. \end{Variants} \SeeAlso Chapter~\ref{Extraction}. @@ -294,7 +294,7 @@ Search "+"%Z "*"%Z "distr" -positive -Prop. Search (?x * _ + ?x * _)%Z outside OmegaLemmas. \end{coq_example} -\Warning \comindex{SearchAbout} Up to Coq version 8.4, {\tt Search} +\Warning \comindex{SearchAbout} Up to {\Coq} version 8.4, {\tt Search} had the behavior of current {\tt SearchHead} and the behavior of current {\tt Search} was obtained with command {\tt SearchAbout}. For compatibility, the deprecated name {\tt SearchAbout} can still be used @@ -343,7 +343,7 @@ No module \module{} has been required (see Section~\ref{Require}). \end{Variants} -\Warning Up to Coq version 8.4, {\tt SearchHead} was named {\tt Search}. +\Warning Up to {\Coq} version 8.4, {\tt SearchHead} was named {\tt Search}. \subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}} @@ -458,8 +458,8 @@ The default blacklisted substrings are {\tt \label{Locate}} This command displays the full name of objects whose name is a prefix of the qualified identifier {\qualid}, and consequently the \Coq\ module in which they -are defined. It searches for objects from the different qualified namespaces of -Coq: terms, modules, Ltac, etc. +are defined. It searches for objects from the different qualified name spaces of +{\Coq}: terms, modules, Ltac, etc. \begin{coq_eval} (*************** The last line should produce **************************) @@ -553,10 +553,11 @@ the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt mapped in {\Coq} loadpath to the logical path {\dirpath} (see Section~\ref{loadpath}). The mapping between physical directories and logical names at the time of requiring the file must be consistent -with the mapping used to compile the file. +with the mapping used to compile the file. If several files match, one of them +is picked in an unspecified fashion. \begin{Variants} -\item {\tt Require Import {\qualid}.} \comindex{Require} +\item {\tt Require Import {\qualid}.} \comindex{Require Import} This loads and declares the module {\qualid} and its dependencies then imports the contents of {\qualid} as described in @@ -585,6 +586,15 @@ with the mapping used to compile the file. given, it also imports {\qualid}$_1$, \ldots, {\qualid}$_n$ and all the recursive dependencies that were marked or transitively marked as {\tt Export}. + +\item {\tt From {\dirpath} Require {\qualid}.} + \comindex{From Require} + + This command acts as {\tt Require}, but picks any library whose absolute name + is of the form {\tt{\dirpath}.{\dirpath'}.{\qualid}} for some {\dirpath'}. + This is useful to ensure that the {\qualid} library comes from a given + package by making explicit its absolute root. + \end{Variants} \begin{ErrMsgs} @@ -610,7 +620,7 @@ with the mapping used to compile the file. \index{Bad-magic-number@{\tt Bad Magic Number}} The file {\tt{\ident}.vo} was found but either it is not a \Coq\ compiled module, or it was compiled with an older and incompatible - version of \Coq. + version of {\Coq}. \item \errindex{The file {\ident}.vo contains library {\dirpath} and not library {\dirpath'}} @@ -647,7 +657,7 @@ searched into the current {\ocaml} loadpath (see the command {\tt Add ML Path} in the Section~\ref{loadpath}). Loading of {\ocaml} files is only possible under the bytecode version of {\tt coqtop} (i.e. {\tt coqtop} called with options {\tt -byte}, see chapter -\ref{Addoc-coqc}), or when Coq has been compiled with a version of +\ref{Addoc-coqc}), or when {\Coq} has been compiled with a version of {\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11). \begin{Variants} @@ -658,7 +668,7 @@ files is only possible under the bytecode version of {\tt coqtop} \begin{ErrMsgs} \item \errindex{File not found on loadpath : \str} -\item \errindex{Loading of ML object file forbidden in a native Coq} +\item \errindex{Loading of ML object file forbidden in a native {\Coq}} \end{ErrMsgs} \subsection[\tt Print ML Modules.]{\tt Print ML Modules.\comindex{Print ML Modules}} @@ -669,7 +679,7 @@ should use the command \texttt{Locate File} (see Section~\ref{Locate File}) \section[Loadpath]{Loadpath} Loadpaths are preferably managed using {\Coq} command line options -(see Section~\ref{loadpath}) but there remains vernacular commands to +(see Section~\ref{loadpath}) but there remain vernacular commands to manage them. \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}} @@ -686,7 +696,7 @@ which can be any valid path. \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}} -This command is equivament to the command line option {\tt -Q {\dirpath} +This command is equivalent to the command line option {\tt -Q {\dirpath} {\str}}. It adds the physical directory {\str} to the current {\Coq} loadpath and maps it to the logical directory {\dirpath}. @@ -768,11 +778,11 @@ over the name of a module or of an object inside a module. This commands undoes all the effects of the last vernacular command. Commands read from a vernacular file via a {\tt Load} are -considered as a single command. Proof managment commands +considered as a single command. Proof management commands are also handled by this command (see Chapter~\ref{Proof-handling}). For that, {\tt Back} may have to undo more than one command in order -to reach a state where the proof managment information is available. -For instance, when the last command is a {\tt Qed}, the managment +to reach a state where the proof management information is available. +For instance, when the last command is a {\tt Qed}, the management information about the closed proof has been discarded. In this case, {\tt Back} will then undo all the proof steps up to the statement of this proof. @@ -793,7 +803,7 @@ this proof. \subsection[\tt BackTo $\num$.]{\tt BackTo $\num$.\comindex{BackTo}} \label{sec:statenums} -This command brings back the system to the state labelled $\num$, +This command brings back the system to the state labeled $\num$, forgetting the effect of all commands executed after this state. The state label is an integer which grows after each successful command. It is displayed in the prompt when in \texttt{-emacs} mode. @@ -804,14 +814,14 @@ extra commands and end on a state $\num' \leq \num$ if necessary. \begin{Variants} \item {\tt Backtrack $\num_1$ $\num_2$ $\num_3$}.\comindex{Backtrack}\\ {\tt Backtrack} is a \emph{deprecated} form of {\tt BackTo} which - allows explicitely manipulating the proof environment. The three + allows explicitly manipulating the proof environment. The three numbers $\num_1$, $\num_2$ and $\num_3$ represent the following: \begin{itemize} \item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number of currently opened nested proofs that must be canceled (see Chapter~\ref{Proof-handling}). \item $\num_2$: \emph{Proof state number} to unbury once aborts have - been done. Coq will compute the number of \texttt{Undo} to perform + been done. {\Coq} will compute the number of \texttt{Undo} to perform (see Chapter~\ref{Proof-handling}). \item $\num_1$: State label to reach, as for {\tt BackTo}. \end{itemize} @@ -939,7 +949,7 @@ algorithm that first normalizes the terms before comparing them. The second algorithm is based on a bytecode representation of terms similar to the bytecode representation used in the ZINC virtual machine~\cite{Leroy90}. It is especially useful for intensive -computation of algebraic values, such as numbers, and for reflexion-based +computation of algebraic values, such as numbers, and for reflection-based tactics. The commands to fine-tune the reduction strategies and the lazy conversion algorithm are described first. diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 76e4efd60..94290bc80 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -113,7 +113,7 @@ subdirectory. A specified subdirectory must have an inner \texttt{Makefile}. The phony targets \texttt{all} and \texttt{clean} will recursively call this target in all the subdirectories. -\item \texttt{-R} and \texttt{-I} options are for {\Coq}, \texttt{-I} +\item \texttt{-R} and \texttt{-Q} options are for {\Coq}, \texttt{-I} for {\ocaml}. The same directory may be ``included'' by both. Using \texttt{-R} or \texttt{-Q} gives a correct logical path diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 01ad0f70f..907b30b3e 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -134,24 +134,17 @@ Options A and B of the licence are {\em not} elected.} \bibliography{biblio} \cutname{biblio.html} -\printindex -\cutname{general-index.html} - -\printindex[tactic] -\cutname{tactic-index.html} - -\printindex[command] -\cutname{command-index.html} - -\printindex[option] -\cutname{option-index.html} - -\printindex[error] -\cutname{error-index.html} +\printrefmanindex{default}{Global Index}{general-index.html} +\printrefmanindex{tactic}{Tactics Index}{tactic-index.html} +\printrefmanindex{command}{Vernacular Commands Index}{command-index.html} +\printrefmanindex{option}{Vernacular Options Index}{option-index.html} +\printrefmanindex{error}{Index of Error Messages}{error-index.html} %BEGIN LATEX -\listoffigures +\cleardoublepage +\phantomsection \addcontentsline{toc}{chapter}{\listfigurename} +\listoffigures %END LATEX \end{document} diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index b42480a56..ee2b042f4 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -141,7 +141,7 @@ Example: \end{verbatim} \paragraph{Rules.} -More than 4 leading dashes produce an horizontal rule. +More than 4 leading dashes produce a horizontal rule. \paragraph{Emphasis.} Text can be italicized by placing it in underscores. A non-identifier diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva index df4aec272..9714a29be 100644 --- a/doc/refman/headers.hva +++ b/doc/refman/headers.hva @@ -8,23 +8,19 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%% \usepackage{index} \makeindex -\newindex{tactic}{tacidx}{tacind}{% -\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index} -\newindex{command}{comidx}{comind}{% -\protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}% -Vernacular Commands Index} -\newindex{option}{optidx}{optind}{% -\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}% -Vernacular Options Index} +\newindex{tactic}{tacidx}{tacind}{Tactics Index} +\newindex{command}{comidx}{comind}{Vernacular Commands Index} +\newindex{option}{optidx}{optind}{Vernacular Options Index} +\newindex{error}{erridx}{errind}{Index of Error Messages} +\renewindex{default}{idx}{ind}{Global Index} -\newindex{error}{erridx}{errind}{% -\protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages} - -\renewindex{default}{idx}{ind}{% -\protect\addcontentsline{toc}{chapter}{Global Index}% -Global Index} +\newcommand{\printrefmanindex}[3]{% +\addcontentsline{toc}{chapter}{#2}% +\printindex[#1]% +\cutname{#3}% +} \newcommand{\tacindex}[1]{% \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}} diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty index ef28588e3..fb39f687d 100644 --- a/doc/refman/headers.sty +++ b/doc/refman/headers.sty @@ -30,27 +30,21 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%% \usepackage{index} \makeindex -\newindex{tactic}{tacidx}{tacind}{% -\protect\setheaders{Tactics Index}% -\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index} -\newindex{command}{comidx}{comind}{% -\protect\setheaders{Vernacular Commands Index}% -\protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}% -Vernacular Commands Index} - -\newindex{option}{optidx}{optind}{% -\protect\setheaders{Vernacular Options Index}% -\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}% -Vernacular Options Index} - -\newindex{error}{erridx}{errind}{% -\protect\setheaders{Index of Error Messages}% -\protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages} - -\renewindex{default}{idx}{ind}{% -\protect\addcontentsline{toc}{chapter}{Global Index}% -\protect\setheaders{Global Index}Global Index} +\newindex{tactic}{tacidx}{tacind}{Tactics Index} +\newindex{command}{comidx}{comind}{Vernacular Commands Index} +\newindex{option}{optidx}{optind}{Vernacular Options Index} +\newindex{error}{erridx}{errind}{Index of Error Messages} +\renewindex{default}{idx}{ind}{Global Index} + +\newcommand{\printrefmanindex}[3]{% +\cleardoublepage% +\phantomsection% +\setheaders{#2}% +\addcontentsline{toc}{chapter}{#2}% +\printindex[#1]% +\cutname{#3}% +} \newcommand{\tacindex}[1]{% \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 159f8df7f..024e13413 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -476,6 +476,7 @@ through the <tt>Require Import</tt> command.</p> theories/MSets/MSetPositive.v theories/MSets/MSetToFiniteSet.v (theories/MSets/MSets.v) + theories/MMaps/MMapAVL.v theories/MMaps/MMapFacts.v theories/MMaps/MMapInterface.v theories/MMaps/MMapList.v diff --git a/ide/coq.lang b/ide/coq.lang index 38dabda50..65150d6a9 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -164,7 +164,7 @@ <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword> <keyword>\%{locality}Infix</keyword> <keyword>Declare\%{space}ML\%{space}Module</keyword> - <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme)</keyword> + <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword> </context> <context id="hint-command" style-ref="vernac-keyword"> <prefix>\%{locality}Hint\%{space}</prefix> diff --git a/ide/coqOps.ml b/ide/coqOps.ml index c6073d599..af728471f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -276,21 +276,11 @@ object(self) Doc.focus document ~cond_top:(at start) ~cond_bot:(at stop); self#print_stack; let qed_s = Doc.tip_data document in - buffer#apply_tag Tags.Script.read_only - ~start:((buffer#get_iter_at_mark qed_s.start)#forward_find_char - (fun c -> not(Glib.Unichar.isspace c))) - ~stop:(buffer#get_iter_at_mark qed_s.stop); buffer#move_mark ~where:(buffer#get_iter_at_mark qed_s.stop) (`NAME "stop_of_input") method private exit_focus = Minilib.log "Unfocusing"; - begin try - let { start; stop } = Doc.tip_data document in - buffer#remove_tag Tags.Script.read_only - ~start:(buffer#get_iter_at_mark start) - ~stop:(buffer#get_iter_at_mark stop) - with Doc.Empty -> () end; Doc.unfocus document; self#print_stack; begin try @@ -515,7 +505,7 @@ object(self) | Some (start, stop) -> if until n start stop then begin () - end else if start#has_tag Tags.Script.processed then begin + end else if stop#backward_char#has_tag Tags.Script.processed then begin Queue.push (`Skip (start, stop)) queue; loop n stop end else begin @@ -563,12 +553,15 @@ object(self) script#recenter_insert; match topstack with | [] -> self#show_goals_aux ?move_insert () - | (_,s) :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in + | (_,s)::_ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in let process_queue queue = let rec loop tip topstack = if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with - | `Skip(start,stop), [] -> assert false + | `Skip(start,stop), [] -> + logger Pp.Error "You muse close the proof with Qed or Admitted"; + self#discard_command_queue queue; + conclude [] | `Skip(start,stop), (_,s) :: topstack -> assert(start#equal (buffer#get_iter_at_mark s.start)); assert(stop#equal (buffer#get_iter_at_mark s.stop)); @@ -589,7 +582,7 @@ object(self) Doc.assign_tip_id document id; let topstack, _ = Doc.context document in self#exit_focus; - self#cleanup ~all:true (Doc.cut_at document tip); + self#cleanup (Doc.cut_at document tip); logger Pp.Notice msg; self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] @@ -651,7 +644,7 @@ object(self) Doc.find_id document (fun id { start;stop } -> until (Some id) start stop) with Not_found -> initial_state, Doc.focused document - method private cleanup ~all seg = + method private cleanup seg = if seg <> [] then begin let start = buffer#get_iter_at_mark (CList.last seg).start in let stop = buffer#get_iter_at_mark (CList.hd seg).stop in @@ -662,7 +655,6 @@ object(self) buffer#remove_tag Tags.Script.unjustified ~start ~stop; buffer#remove_tag Tags.Script.tooltip ~start ~stop; buffer#remove_tag Tags.Script.to_process ~start ~stop; - if all then buffer#remove_tag Tags.Script.read_only ~start ~stop; buffer#remove_tag Tags.Script.error ~start ~stop; buffer#remove_tag Tags.Script.error_bg ~start ~stop; buffer#move_mark ~where:start (`NAME "start_of_input") @@ -694,13 +686,13 @@ object(self) Coq.bind (Coq.edit_at to_id) (function | Good (CSig.Inl (* NewTip *) ()) -> if unfocus_needed then self#exit_focus; - self#cleanup ~all:true (Doc.cut_at document to_id); + self#cleanup (Doc.cut_at document to_id); conclusion () | Good (CSig.Inr (* Focus *) (stop_id,(start_id,tip))) -> if unfocus_needed then self#exit_focus; - self#cleanup ~all:true (Doc.cut_at document tip); + self#cleanup (Doc.cut_at document tip); self#enter_focus start_id stop_id; - self#cleanup ~all:false (Doc.cut_at document to_id); + self#cleanup (Doc.cut_at document to_id); conclusion () | Fail (safe_id, loc, msg) -> if loc <> None then messages#push Pp.Error "Fixme LOC"; diff --git a/ide/coqide.ml b/ide/coqide.ml index 87efd17d2..0f4cb7b07 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -253,11 +253,14 @@ let newfile _ = !refresh_editor_hook (); notebook#goto_page index -let load _ = - match select_file_for_open ~title:"Load file" () with +let load sn = + let filename = sn.fileops#filename in + match select_file_for_open ~title:"Load file" ?filename () with | None -> () | Some f -> FileAux.load_file f +let load = cb_on_current_term load + let save _ = on_current_term (FileAux.check_save ~saveas:false) let saveas sn = @@ -1339,11 +1342,6 @@ let build_ui () = (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); Tags.Script.incomplete#set_property (`BACKGROUND_GDK (Tags.get_processed_color ())); - Tags.Script.read_only#set_property - (`BACKGROUND_STIPPLE - (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); - Tags.Script.read_only#set_property - (`BACKGROUND_GDK (Tags.get_processed_color ())); (* Showtime ! *) w#show () diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 973ff0b77..67e4bdb0c 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -144,8 +144,7 @@ let current_dir () = match current.project_path with | None -> "" | Some dir -> dir -let select_file_for_open ~title () = - let file = ref None in +let select_file_for_open ~title ?filename () = let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title () in @@ -154,19 +153,22 @@ let select_file_for_open ~title () = file_chooser#add_filter (filter_coq_files ()); file_chooser#add_filter (filter_all_files ()); file_chooser#set_default_response `OPEN; - ignore (file_chooser#set_current_folder (current_dir ())); - begin match file_chooser#run () with + let dir = match filename with + | None -> current_dir () + | Some f -> Filename.dirname f in + ignore (file_chooser#set_current_folder dir); + let file = + match file_chooser#run () with | `OPEN -> begin - file := file_chooser#filename; - match !file with - | None -> () - | Some s -> current.project_path <- file_chooser#current_folder + match file_chooser#filename with + | None -> None + | Some _ as f -> + current.project_path <- file_chooser#current_folder; f end - | `DELETE_EVENT | `CANCEL -> () - end ; + | `DELETE_EVENT | `CANCEL -> None in file_chooser#destroy (); - !file + file let select_file_for_save ~title ?filename () = let file = ref None in diff --git a/ide/ideutils.mli b/ide/ideutils.mli index c2b51dd39..1fb30e4d7 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -29,7 +29,7 @@ val find_tag_limits : GText.tag -> GText.iter -> GText.iter * GText.iter val find_tag_start : GText.tag -> GText.iter -> GText.iter val find_tag_stop : GText.tag -> GText.iter -> GText.iter -val select_file_for_open : title:string -> unit -> string option +val select_file_for_open : title:string -> ?filename:string -> unit -> string option val select_file_for_save : title:string -> ?filename:string -> unit -> string option val try_convert : string -> string diff --git a/ide/session.ml b/ide/session.ml index e0466b7e3..12b779663 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -156,8 +156,6 @@ let set_buffer_handlers let () = update_prev it in if it#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" - else if it#has_tag Tags.Script.read_only then - cancel_signal "Altering read_only text not allowed" else if it#has_tag Tags.Script.processed then call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) else if it#has_tag Tags.Script.error_bg then begin @@ -175,8 +173,6 @@ let set_buffer_handlers if min_iter#equal max_iter then () else if min_iter#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" - else if min_iter#has_tag Tags.Script.read_only then - cancel_signal "Altering read_only text not allowed" else if min_iter#has_tag Tags.Script.processed then call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) else if min_iter#has_tag Tags.Script.error_bg then diff --git a/ide/tags.ml b/ide/tags.ml index d4460b077..c9b57af4c 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -52,10 +52,6 @@ struct t let all = edit_zone :: all - let read_only = make_tag table ~name:"read_only" [`EDITABLE false; - `BACKGROUND !processing_color; - `BACKGROUND_STIPPLE_SET true ] - end module Proof = struct @@ -96,7 +92,6 @@ let set_processing_color clr = let s = string_of_color clr in processing_color := s; Script.incomplete#set_property (`BACKGROUND s); - Script.read_only#set_property (`BACKGROUND s); Script.to_process#set_property (`BACKGROUND s) let get_error_color () = color_of_string !error_color diff --git a/ide/tags.mli b/ide/tags.mli index e68015c99..14cfd0dbf 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -21,9 +21,6 @@ sig val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) val all : GText.tag list - - (* Not part of the all list. Special tags! *) - val read_only : GText.tag end module Proof : diff --git a/library/libnames.ml b/library/libnames.ml index f2a9d041d..cdaec6a3d 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -32,6 +32,11 @@ let is_dirpath_prefix_of d1 d2 = List.prefix_of Id.equal (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) +let is_dirpath_suffix_of dir1 dir2 = + let dir1 = DirPath.repr dir1 in + let dir2 = DirPath.repr dir2 in + List.prefix_of Id.equal dir1 dir2 + let chop_dirpath n d = let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in DirPath.make (List.rev d1), DirPath.make (List.rev d2) diff --git a/library/libnames.mli b/library/libnames.mli index 3b5feb94e..b95c08871 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -37,6 +37,8 @@ val append_dirpath : DirPath.t -> DirPath.t -> DirPath.t val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool +val is_dirpath_suffix_of : DirPath.t -> DirPath.t -> bool + module Dirset : Set.S with type elt = DirPath.t module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset diff --git a/library/library.ml b/library/library.ml index 2b607e1a3..9d0ccb972 100644 --- a/library/library.ml +++ b/library/library.ml @@ -268,8 +268,9 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = Loadpath.expand_root_path pref in + let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in + let loadpath = List.map fst loadpath in let find ext = try let name = Id.to_string base ^ ext in @@ -286,10 +287,20 @@ let locate_absolute_library dir = | [vo;vi] -> dir, vo | _ -> assert false -let locate_qualified_library warn qid = +let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) let dir, base = repr_qualid qid in - let loadpath = Loadpath.expand_path dir in + let loadpath = match root with + | None -> Loadpath.expand_path dir + | Some root -> + let filter path = + if is_dirpath_prefix_of root path then + let path = drop_dirpath_prefix root path in + is_dirpath_suffix_of dir path + else false + in + Loadpath.filter_path filter + in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let find ext = try @@ -333,14 +344,6 @@ let try_locate_absolute_library dir = | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) -let try_locate_qualified_library (loc,qid) = - try - let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in - dir,f - with - | LibUnmappedDir -> error_unmapped_dir qid - | LibNotFound -> error_lib_not_found qid - (************************************************************************) (** {6 Tables of opaque proof terms} *) @@ -592,10 +595,6 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library qidl export = - let modrefl = List.map try_locate_qualified_library qidl in - require_library_from_dirpath modrefl export - let require_library_from_file idopt file export = let modref,needed = rec_intern_library_from_file idopt file in let needed = List.rev_map snd needed in diff --git a/library/library.mli b/library/library.mli index 75b256258..350670680 100644 --- a/library/library.mli +++ b/library/library.mli @@ -21,7 +21,6 @@ open Libnames (** {6 ... } *) (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) -val require_library : qualid located list -> bool option -> unit val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit val require_library_from_file : Id.t option -> CUnix.physical_path -> bool option -> unit @@ -73,8 +72,14 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - bool -> qualid -> library_location * DirPath.t * CUnix.physical_path -val try_locate_qualified_library : qualid located -> DirPath.t * string + ?root:DirPath.t -> ?warn:bool -> qualid -> + library_location * DirPath.t * CUnix.physical_path +(** Locates a library by implicit name. + + @raise LibUnmappedDir if the library is not in the path + @raise LibNotFound if there is no corresponding file in the path + +*) (** {6 Statistics: display the memory use of a library. } *) val mem : DirPath.t -> Pp.std_ppcmds diff --git a/library/loadpath.ml b/library/loadpath.ml index ab8b0a307..26af809e7 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -17,7 +17,6 @@ open Libnames type t = { path_physical : CUnix.physical_path; path_logical : DirPath.t; - path_root : bool; path_implicit : bool; } @@ -53,33 +52,35 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths -let add_load_path phys_path coq_path ~root ~implicit = +let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in let filter p = String.equal p.path_physical phys_path in let binding = { path_logical = coq_path; path_physical = phys_path; - path_root = root; path_implicit = implicit; } in match List.filter filter !load_paths with | [] -> load_paths := binding :: !load_paths - | [p] -> - let dir = p.path_logical in - if not (DirPath.equal coq_path dir) - (* If this is not the default -I . to coqtop *) - && not - (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) - && DirPath.equal coq_path (Nameops.default_root_prefix)) - then + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DirPath.equal coq_path old_path then + implicit <> old_implicit + else if DirPath.equal coq_path (Nameops.default_root_prefix) + && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then + false (* This is the default "-I ." path, don't override the old path *) + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DirPath.equal old_path Nameops.default_root_prefix) then + msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath old_path ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path) in + true in + if replace then begin - (* Assume the user is concerned by library naming *) - if not (DirPath.equal dir Nameops.default_root_prefix) then - msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath dir ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path); remove_load_path phys_path; load_paths := binding :: !load_paths; end @@ -89,51 +90,25 @@ let extend_path_with_dirpath p dir = List.fold_left Filename.concat p (List.rev_map Id.to_string (DirPath.repr dir)) -let expand_root_path dir = +let filter_path f = let rec aux = function | [] -> [] | p :: l -> - if p.path_root && is_dirpath_prefix_of p.path_logical dir then - let suffix = drop_dirpath_prefix p.path_logical dir in - extend_path_with_dirpath p.path_physical suffix :: aux l + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l else aux l in aux !load_paths -(* Root p is bound to A.B.C.D and we require file C.D.E.F *) -(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *) - -(* Root p is bound to A.B.C.C and we require file C.C.E.F *) -(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *) - -let intersections d1 d2 = - let rec aux d1 = - if DirPath.is_empty d1 then [d2] else - let rest = aux (snd (chop_dirpath 1 d1)) in - if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest - else rest in - aux d1 - -let expand p dir = - let ph = extend_path_with_dirpath p.path_physical dir in - let log = append_dirpath p.path_logical dir in - (ph, log) - let expand_path dir = let rec aux = function | [] -> [] - | p :: l -> - match p.path_implicit, p.path_root with - | true, false -> expand p dir :: aux l - | true, true -> - let inters = intersections p.path_logical dir in - List.map (expand p) inters @ aux l - | false, true -> - if is_dirpath_prefix_of p.path_logical dir then - expand p (drop_dirpath_prefix p.path_logical dir) :: aux l - else aux l - | false, false -> - (* nothing to do, an explicit root path should also match above - if [is_dirpath_prefix_of p.path_logical dir] were true here *) - aux l in + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + match implicit with + | true -> + (** The path is implicit, so that we only want match the logical suffix *) + if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l + | false -> + (** Otherwise we must match exactly *) + if DirPath.equal dir lg then (ph, lg) :: aux l else aux l + in aux !load_paths diff --git a/library/loadpath.mli b/library/loadpath.mli index d4029303d..3251b8c60 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -30,8 +30,8 @@ val get_load_paths : unit -> t list val get_paths : unit -> CUnix.physical_path list (** Same as [get_load_paths] but only get the physical part. *) -val add_load_path : CUnix.physical_path -> DirPath.t -> root:bool -> implicit:bool -> unit -(** [add_load_path phys type log] adds the binding [phys := log] to the current +val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit +(** [add_load_path phys log type] adds the binding [phys := log] to the current loadpaths. *) val remove_load_path : CUnix.physical_path -> unit @@ -47,7 +47,8 @@ val is_in_load_paths : CUnix.physical_path -> bool val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list (** Given a relative logical path, associate the list of absolute physical and - logical paths which are possible expansions of it. *) + logical paths which are possible matches of it. *) -val expand_root_path : DirPath.t -> CUnix.physical_path list -(** As [expand_path] but restricts to root loadpaths. *) +val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list +(** As {!expand_path} but uses a filter function instead, and ignores the + implicit status of loadpaths. *) diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 07df7c7f0..774c20c9a 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -119,3 +119,18 @@ let get_last env = match Environ.named_context env with | (id,_,_)::_ -> id | [] -> error "no previous statement to use" + +let get_end_command pts = + match get_top_stack pts with + | [] -> "\"end proof\"" + | Claim::_ -> "\"end claim\"" + | Focus_claim::_-> "\"end focus\"" + | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _ -> + begin + match et with + Decl_expr.ET_Case_analysis -> + "\"end cases\" or start a new case" + | Decl_expr.ET_Induction -> + "\"end induction\" or start a new case" + end + | _ -> anomaly (Pp.str"lonely suppose") diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index e12c4c923..fd7e15c15 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -72,6 +72,8 @@ val get_last: Environ.env -> Id.t (** [get_last] raises a [UserError] when it cannot find a previous statement in the environment. *) +val get_end_command : Proof.proof -> string + val focus : Proof.proof -> unit val unfocus : unit -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index ab5282e79..9d0b7f346 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1446,6 +1446,7 @@ let rec postprocess pts instr = anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end | Pend (B_elim ET_Case_analysis) -> goto_current_focus () + | Pend B_proof -> Proof_global.set_proof_mode "Classic" | Pend _ -> () let do_instr raw_instr pts = diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 2bd88d5ae..d598e7c3f 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -36,13 +36,20 @@ let pr_goal gs = str "============================" ++ fnl () ++ thesis ++ str " " ++ pc) ++ fnl () -(* arnaud: rebrancher ça ? -let pr_open_subgoals () = - let p = Proof_global.give_me_the_proof () in - let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in - let close_cmd = Decl_mode.get_end_command p in - pr_subgoals close_cmd sigma goals -*) +let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll = + match gll with + | [goal] when pr_first -> + pr_goal { Evd.it = goal ; sigma = sigma } + | _ -> + (* spiwack: it's not very nice to have to call proof global + here, a more robust solution would be to add a hook for + [Printer.pr_open_subgoals] in proof modes, in order to + compute the end command. Yet a more robust solution would be + to have focuses give explanations of their unfocusing + behaviour. *) + let p = Proof_global.give_me_the_proof () in + let close_cmd = Decl_mode.get_end_command p in + str "Subproof completed, now type " ++ str close_cmd ++ str "." let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr @@ -93,14 +100,16 @@ let proof_instr : raw_proof_instr Gram.entry = let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr -let classify_proof_instr _ = VtProofStep false, VtLater +let classify_proof_instr = function + | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow + | _ -> VtProofStep false, VtLater (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. The "-" indicates that the rule does not start with a distinguished string. *) -VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr - [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ] +VERNAC proof_mode EXTEND ProofInstr + [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ] END (* It is useful to use GEXTEND directly to call grammar entries that have been @@ -130,7 +139,8 @@ let _ = (* We substitute the goal printer, by the one we built for the proof mode. *) Printer.set_printer_pr { Printer.default_printer_pr with - Printer.pr_goal = pr_goal } + Printer.pr_goal = pr_goal; + pr_subgoals = pr_subgoals; } end ; (* function [reset] goes back to No Proof Mode from Declarative Proof Mode *) @@ -147,7 +157,7 @@ VERNAC COMMAND EXTEND DeclProof [ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ] END VERNAC COMMAND EXTEND DeclReturn -[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ] +[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ] END let none_is_empty = function diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v new file mode 100644 index 000000000..294d61023 --- /dev/null +++ b/plugins/extraction/ExtrHaskellBasic.v @@ -0,0 +1,15 @@ +(** Extraction to Haskell : use of basic Haskell types *) + +Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive unit => "()" [ "()" ]. +Extract Inductive list => "([])" [ "([])" "(:)" ]. +Extract Inductive prod => "(,)" [ "(,)" ]. + +Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ]. + +Extract Inlined Constant andb => "(Prelude.&&)". +Extract Inlined Constant orb => "(Prelude.||)". +Extract Inlined Constant negb => "Prelude.not". diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 21819aa8f..97f856944 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -600,6 +600,7 @@ let pp_global k r = let rls = List.rev ls in (* for what come next it's easier this way *) match lang () with | Scheme -> unquote s (* no modular Scheme extraction... *) + | JSON -> dottify (List.map unquote rls) | Haskell -> if modular () then pp_haskell_gen k mp rls else s | Ocaml -> pp_ocaml_gen k mp rls (Some l) @@ -628,7 +629,7 @@ let check_extract_ascii () = try let char_type = match lang () with | Ocaml -> "char" - | Haskell -> "Char" + | Haskell -> "Prelude.Char" | _ -> raise Not_found in String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 5ea4fb763..0f846013b 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -410,6 +410,7 @@ let descr () = match lang () with | Ocaml -> Ocaml.ocaml_descr | Haskell -> Haskell.haskell_descr | Scheme -> Scheme.scheme_descr + | JSON -> Json.json_descr (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" Works similarly for the other languages. *) diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib index b7f458611..ad3212434 100644 --- a/plugins/extraction/extraction_plugin.mllib +++ b/plugins/extraction/extraction_plugin.mllib @@ -6,6 +6,7 @@ Common Ocaml Haskell Scheme +Json Extract_env G_extraction Extraction_plugin_mod diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 3caa558f9..3fe5a8c04 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -41,12 +41,14 @@ let pr_language = function | Ocaml -> str "Ocaml" | Haskell -> str "Haskell" | Scheme -> str "Scheme" + | JSON -> str "JSON" VERNAC ARGUMENT EXTEND language PRINTED BY pr_language | [ "Ocaml" ] -> [ Ocaml ] | [ "Haskell" ] -> [ Haskell ] | [ "Scheme" ] -> [ Scheme ] +| [ "JSON" ] -> [ JSON ] END (* Extraction commands *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 52459f78e..37b414207 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -38,7 +38,7 @@ let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}" let preamble mod_name comment used_modules usf = let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n") in - (if not usf.magic then mt () + (if not (usf.magic || usf.tunknown) then mt () else str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++ str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}") @@ -52,22 +52,36 @@ let preamble mod_name comment used_modules usf = str "import qualified Prelude" ++ fnl () ++ prlist pp_import used_modules ++ fnl () ++ (if List.is_empty used_modules then mt () else fnl ()) ++ - (if not usf.magic then mt () + (if not (usf.magic || usf.tunknown) then mt () else str "\ \n#ifdef __GLASGOW_HASKELL__\ \nimport qualified GHC.Base\ \nimport qualified GHC.Prim\ -\ntype Any = GHC.Prim.Any\ +\n#else\ +\n-- HUGS\ +\nimport qualified IOExts\ +\n#endif" ++ fnl2 ()) + ++ + (if not usf.magic then mt () + else str "\ +\n#ifdef __GLASGOW_HASKELL__\ \nunsafeCoerce :: a -> b\ \nunsafeCoerce = GHC.Base.unsafeCoerce#\ \n#else\ \n-- HUGS\ -\nimport qualified IOExts\ -\ntype Any = ()\ \nunsafeCoerce :: a -> b\ \nunsafeCoerce = IOExts.unsafeCoerce\ \n#endif" ++ fnl2 ()) ++ + (if not usf.tunknown then mt () + else str "\ +\n#ifdef __GLASGOW_HASKELL__\ +\ntype Any = GHC.Prim.Any\ +\n#else\ +\n-- HUGS\ +\ntype Any = ()\ +\n#endif" ++ fnl2 ()) + ++ (if not usf.mldummy then mt () else str "__ :: any" ++ fnl () ++ str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) @@ -349,7 +363,7 @@ and pp_module_expr = function | MEfunctor _ -> mt () (* for the moment we simply discard unapplied functors *) | MEident _ | MEapply _ -> assert false - (* should be expansed in extract_env *) + (* should be expanded in extract_env *) let pp_struct = let pp_sel (mp,sel) = diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml new file mode 100644 index 000000000..125dc86b8 --- /dev/null +++ b/plugins/extraction/json.ml @@ -0,0 +1,278 @@ +open Pp +open Errors +open Util +open Names +open Nameops +open Globnames +open Table +open Miniml +open Mlutil +open Common + +let json_str s = + qs s + +let json_int i = + int i + +let json_bool b = + if b then str "true" else str "false" + +let json_null = + str "null" + +let json_global typ ref = + json_str (Common.pp_global typ ref) + +let json_id id = + json_str (Id.to_string id) + +let json_dict_one (k, v) = + json_str k ++ str (": ") ++ v + +let json_dict_open l = + str ("{") ++ fnl () ++ + str (" ") ++ hov 0 (prlist_with_sep pr_comma json_dict_one l) + +let json_dict l = + json_dict_open l ++ fnl () ++ + str ("}") + +let json_list l = + str ("[") ++ fnl () ++ + str (" ") ++ hov 0 (prlist_with_sep pr_comma (fun x -> x) l) ++ fnl () ++ + str ("]") + +let json_listarr a = + str ("[") ++ fnl () ++ + str (" ") ++ hov 0 (prvect_with_sep pr_comma (fun x -> x) a) ++ fnl () ++ + str ("]") + + +let preamble mod_name comment used_modules usf = + (match comment with + | None -> mt () + | Some s -> str "/* " ++ hov 0 s ++ str " */" ++ fnl ()) ++ + json_dict_open [ + ("what", json_str "module"); + ("name", json_id mod_name); + ("need_magic", json_bool (usf.magic)); + ("need_dummy", json_bool (usf.mldummy)); + ("used_modules", json_list + (List.map (fun mf -> json_str (file_of_modfile mf)) used_modules)) + ] + + +(*s Pretty-printing of types. *) + +let rec json_type vl = function + | Tmeta _ | Tvar' _ -> assert false + | Tvar i -> (try + let varid = List.nth vl (pred i) in json_dict [ + ("what", json_str "type:var"); + ("name", json_id varid) + ] + with Failure _ -> json_dict [ + ("what", json_str "type:varidx"); + ("name", json_int i) + ]) + | Tglob (r, l) -> json_dict [ + ("what", json_str "type:glob"); + ("name", json_global Type r); + ("args", json_list (List.map (json_type vl) l)) + ] + | Tarr (t1,t2) -> json_dict [ + ("what", json_str "type:arrow"); + ("left", json_type vl t1); + ("right", json_type vl t2) + ] + | Tdummy _ -> json_dict [("what", json_str "type:dummy")] + | Tunknown -> json_dict [("what", json_str "type:unknown")] + | Taxiom -> json_dict [("what", json_str "type:axiom")] + + +(*s Pretty-printing of expressions. *) + +let rec json_expr env = function + | MLrel n -> json_dict [ + ("what", json_str "expr:rel"); + ("name", json_id (get_db_name n env)) + ] + | MLapp (f, args) -> json_dict [ + ("what", json_str "expr:apply"); + ("func", json_expr env f); + ("args", json_list (List.map (json_expr env) args)) + ] + | MLlam _ as a -> + let fl, a' = collect_lams a in + let fl, env' = push_vars (List.map id_of_mlid fl) env in + json_dict [ + ("what", json_str "expr:lambda"); + ("argnames", json_list (List.map json_id (List.rev fl))); + ("body", json_expr env' a') + ] + | MLletin (id, a1, a2) -> + let i, env' = push_vars [id_of_mlid id] env in + json_dict [ + ("what", json_str "expr:let"); + ("name", json_id (List.hd i)); + ("nameval", json_expr env a1); + ("body", json_expr env' a2) + ] + | MLglob r -> json_dict [ + ("what", json_str "expr:global"); + ("name", json_global Term r) + ] + | MLcons (_, r, a) -> json_dict [ + ("what", json_str "expr:constructor"); + ("name", json_global Cons r); + ("args", json_list (List.map (json_expr env) a)) + ] + | MLtuple l -> json_dict [ + ("what", json_str "expr:tuple"); + ("items", json_list (List.map (json_expr env) l)) + ] + | MLcase (typ, t, pv) -> json_dict [ + ("what", json_str "expr:case"); + ("expr", json_expr env t); + ("cases", json_listarr (Array.map (fun x -> json_one_pat env x) pv)) + ] + | MLfix (i, ids, defs) -> + let ids', env' = push_vars (List.rev (Array.to_list ids)) env in + let ids' = Array.of_list (List.rev ids') in + json_dict [ + ("what", json_str "expr:fix"); + ("funcs", json_listarr (Array.map (fun (fi, ti) -> + json_dict [ + ("what", json_str "fix:item"); + ("name", json_id fi); + ("body", json_function env' ti) + ]) (Array.map2 (fun a b -> a,b) ids' defs))) + ] + | MLexn s -> json_dict [ + ("what", json_str "expr:exception"); + ("msg", json_str s) + ] + | MLdummy -> json_dict [("what", json_str "expr:dummy")] + | MLmagic a -> json_dict [ + ("what", json_str "expr:coerce"); + ("value", json_expr env a) + ] + | MLaxiom -> json_dict [("what", json_str "expr:axiom")] + +and json_one_pat env (ids,p,t) = + let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [ + ("what", json_str "case"); + ("pat", json_gen_pat (List.rev ids') env' p); + ("body", json_expr env' t) + ] + +and json_gen_pat ids env = function + | Pcons (r, l) -> json_cons_pat r (List.map (json_gen_pat ids env) l) + | Pusual r -> json_cons_pat r (List.map json_id ids) + | Ptuple l -> json_dict [ + ("what", json_str "pat:tuple"); + ("items", json_list (List.map (json_gen_pat ids env) l)) + ] + | Pwild -> json_dict [("what", json_str "pat:wild")] + | Prel n -> json_dict [ + ("what", json_str "pat:rel"); + ("name", json_id (get_db_name n env)) + ] + +and json_cons_pat r ppl = json_dict [ + ("what", json_str "pat:constructor"); + ("name", json_global Cons r); + ("argnames", json_list ppl) + ] + +and json_function env t = + let bl, t' = collect_lams t in + let bl, env' = push_vars (List.map id_of_mlid bl) env in + json_dict [ + ("what", json_str "expr:lambda"); + ("argnames", json_list (List.map json_id (List.rev bl))); + ("body", json_expr env' t') + ] + + +(*s Pretty-printing of inductive types declaration. *) + +let json_ind ip pl cv = json_dict [ + ("what", json_str "decl:ind"); + ("name", json_global Type (IndRef ip)); + ("argnames", json_list (List.map json_id pl)); + ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [ + ("name", json_global Cons (ConstructRef (ip, idx+1))); + ("argtypes", json_list (List.map (json_type pl) c)) + ]) cv)) + ] + + +(*s Pretty-printing of a declaration. *) + +let pp_decl = function + | Dind (kn, defs) -> prvecti_with_sep pr_comma + (fun i p -> if p.ip_logical then str "" + else json_ind (kn, i) p.ip_vars p.ip_types) defs.ind_packets + | Dtype (r, l, t) -> json_dict [ + ("what", json_str "decl:type"); + ("name", json_global Type r); + ("argnames", json_list (List.map json_id l)); + ("value", json_type l t) + ] + | Dfix (rv, defs, typs) -> json_dict [ + ("what", json_str "decl:fixgroup"); + ("fixlist", json_listarr (Array.mapi (fun i r -> + json_dict [ + ("what", json_str "fixgroup:item"); + ("name", json_global Term rv.(i)); + ("type", json_type [] typs.(i)); + ("value", json_function (empty_env ()) defs.(i)) + ]) rv)) + ] + | Dterm (r, a, t) -> json_dict [ + ("what", json_str "decl:term"); + ("name", json_global Term r); + ("type", json_type [] t); + ("value", json_function (empty_env ()) a) + ] + +let rec pp_structure_elem = function + | (l,SEdecl d) -> [ pp_decl d ] + | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr + | (l,SEmodtype m) -> [] + (* for the moment we simply discard module type *) + +and pp_module_expr = function + | MEstruct (mp,sel) -> List.concat (List.map pp_structure_elem sel) + | MEfunctor _ -> [] + (* for the moment we simply discard unapplied functors *) + | MEident _ | MEapply _ -> assert false + (* should be expansed in extract_env *) + +let pp_struct mls = + let pp_sel (mp,sel) = + push_visible mp []; + let p = prlist_with_sep pr_comma identity + (List.concat (List.map pp_structure_elem sel)) in + pop_visible (); p + in + str "," ++ fnl () ++ + str " " ++ qs "declarations" ++ str ": [" ++ fnl () ++ + str " " ++ hov 0 (prlist_with_sep pr_comma pp_sel mls) ++ fnl () ++ + str " ]" ++ fnl () ++ + str "}" ++ fnl () + + +let json_descr = { + keywords = Id.Set.empty; + file_suffix = ".json"; + file_naming = file_of_modfile; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} diff --git a/plugins/extraction/json.mli b/plugins/extraction/json.mli new file mode 100644 index 000000000..3ba240a1d --- /dev/null +++ b/plugins/extraction/json.mli @@ -0,0 +1 @@ +val json_descr : Miniml.language_descr diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 99b4fd448..cc8b6d8e7 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -212,7 +212,7 @@ and pp_module_expr = function | MEfunctor _ -> mt () (* for the moment we simply discard unapplied functors *) | MEident _ | MEapply _ -> assert false - (* should be expansed in extract_env *) + (* should be expanded in extract_env *) let pp_struct = let pp_sel (mp,sel) = diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 44d760ccd..a57c39eef 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -554,7 +554,7 @@ let _ = declare_string_option (*s Extraction Lang *) -type lang = Ocaml | Haskell | Scheme +type lang = Ocaml | Haskell | Scheme | JSON let lang_ref = Summary.ref Ocaml ~name:"ExtrLang" diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 1acbe3555..648f23211 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -142,7 +142,7 @@ val file_comment : unit -> string (*s Target language. *) -type lang = Ocaml | Haskell | Scheme +type lang = Ocaml | Haskell | Scheme | JSON val lang : unit -> lang (*s Extraction modes: modular or monolithic, library or minimal ? diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget index 1fe09f6fa..f04890480 100644 --- a/plugins/extraction/vo.itarget +++ b/plugins/extraction/vo.itarget @@ -1,3 +1,4 @@ +ExtrHaskellBasic.vo ExtrOcamlBasic.vo ExtrOcamlIntConv.vo ExtrOcamlBigIntConv.vo diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 22ddd549e..8b959c278 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -34,7 +34,7 @@ Extract Inductive sumor => option [ Some None ]. - rightmost choice (Inright) is (None) *) -(** To preserve its laziness, andb is normally expansed. +(** To preserve its laziness, andb is normally expanded. Let's rather use the ocaml && *) Extract Inlined Constant andb => "(&&)". diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v index 7400d4629..a5f90dd66 100644 --- a/plugins/omega/Omega.v +++ b/plugins/omega/Omega.v @@ -13,10 +13,11 @@ (* *) (**************************************************************************) -(* We do not require [ZArith] anymore, but only what's necessary for Omega *) +(* We import what is necessary for Omega *) Require Export ZArith_base. Require Export OmegaLemmas. Require Export PreOmega. + Declare ML Module "omega_plugin". Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l @@ -25,11 +26,6 @@ Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l Require Export Zhints. -(* -(* The constant minus is required in coq_omega.ml *) -Require Minus. -*) - Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith. Hint Extern 10 (_ <= _) => abstract omega: zarith. Hint Extern 10 (_ < _) => abstract omega: zarith. diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v index 9e5c14841..9f101dbf2 100644 --- a/plugins/omega/OmegaPlugin.v +++ b/plugins/omega/OmegaPlugin.v @@ -6,4 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* To strictly import the omega tactic *) + +Require ZArith_base. +Require OmegaLemmas. +Require PreOmega. + Declare ML Module "omega_plugin". diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v new file mode 100644 index 000000000..9f101dbf2 --- /dev/null +++ b/plugins/omega/OmegaTactic.v @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* To strictly import the omega tactic *) + +Require ZArith_base. +Require OmegaLemmas. +Require PreOmega. + +Declare ML Module "omega_plugin". diff --git a/plugins/omega/vo.itarget b/plugins/omega/vo.itarget index 9d9a77a8c..842210e21 100644 --- a/plugins/omega/vo.itarget +++ b/plugins/omega/vo.itarget @@ -1,4 +1,5 @@ OmegaLemmas.vo OmegaPlugin.vo +OmegaTactic.vo Omega.vo PreOmega.vo diff --git a/printing/printer.ml b/printing/printer.ml index fb98f6073..0d3a1c17e 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -544,26 +544,27 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals else pr_rec 1 (g::l) in + (* Side effect! This has to be made more robust *) + let () = + match close_cmd with + | Some cmd -> msg_info cmd + | None -> () + in match goals with | [] -> begin - match close_cmd with - Some cmd -> - (str "Subproof completed, now type " ++ str cmd ++ - str ".") - | None -> - let exl = Evarutil.non_instantiated sigma in - if Evar.Map.is_empty exl then - (str"No more subgoals." - ++ emacs_print_dependent_evars sigma seeds) - else - let pei = pr_evars_int sigma 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + let exl = Evarutil.non_instantiated sigma in + if Evar.Map.is_empty exl then + (str"No more subgoals." + ++ emacs_print_dependent_evars sigma seeds) + else + let pei = pr_evars_int sigma 1 exl in + (str "No more subgoals but non-instantiated existential " ++ + str "variables:" ++ fnl () ++ (hov 0 pei) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + str "You can use Grab Existential Variables.") end - | [g] when not !Flags.print_emacs -> + | [g] when not !Flags.print_emacs && pr_first -> let pg = default_pr_goal { it = g ; sigma = sigma; } in v 0 ( str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra @@ -572,8 +573,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals ) | g1::rest -> let goals = print_multiple_goals g1 rest in + let ngoals = List.length rest+1 in v 0 ( - int(List.length rest+1) ++ focused_if_needed ++ str"subgoals" ++ + int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ print_extra ++ str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1") ++ pr_goal_tag g1 @@ -587,7 +589,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals type printer_pr = { - pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; } @@ -631,10 +633,14 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> - msg_info (str "This subproof is complete, but there are still unfocused goals." ++ - (match Proof_global.Bullet.suggest p - with None -> str"" | Some s -> fnl () ++ str s)); - fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals + let end_cmd = + strbrk "This subproof is complete, but there are still \ + unfocused goals." ++ + (match Proof_global.Bullet.suggest p + with None -> str"" | Some s -> fnl () ++ str s) ++ + fnl () + in + pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals end | _ -> pr_subgoals None sigma seeds shelf stack goals end diff --git a/printing/printer.mli b/printing/printer.mli index 42ed2b6d9..a469a8dbe 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -128,7 +128,7 @@ val pr_transparent_state : transparent_state -> std_ppcmds (** Proofs *) val pr_goal : goal sigma -> std_ppcmds -val pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds +val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds val pr_concl : int -> evar_map -> goal -> std_ppcmds @@ -168,7 +168,7 @@ val pr_assumptionset : val pr_goal_by_id : string -> std_ppcmds type printer_pr = { - pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; };; diff --git a/stm/stm.ml b/stm/stm.ml index 477ca1f0d..38745e227 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -131,7 +131,7 @@ type cancel_switch = bool ref type branch_type = [ `Master | `Proof of proof_mode * depth - | `Edit of proof_mode * Stateid.t * Stateid.t ] + | `Edit of proof_mode * Stateid.t * Stateid.t * vernac_qed_type ] type cmd_t = { ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *) cast : ast; @@ -449,7 +449,7 @@ end = struct (* {{{ *) if List.mem edit_branch (Vcs_.branches !vcs) then begin checkout edit_branch; match get_branch edit_branch with - | { kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode + | { kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode | _ -> assert false end else let pl = proof_nesting () in @@ -1787,8 +1787,15 @@ let known_state ?(redefine_qed=false) ~cache id = VCS.create_cluster nodes ~qed:id ~start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false - | { VCS.kind = `Edit _ }, Some (ofp, cancel) -> + | { VCS.kind = `Edit (_,_,_, okeep) }, Some (ofp, cancel) -> assert(redefine_qed = true); + if okeep != keep then + msg_error(strbrk("The command closing the proof changed. " + ^"The kernel cannot take this into account and will " + ^(if keep == VtKeep then "not check " else "reject ") + ^"the "^(if keep == VtKeep then "new" else "incomplete") + ^" proof. Reprocess the command declaring " + ^"the proof's statement to avoid that.")); let fp, cancel = Slaves.build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name in @@ -1914,7 +1921,7 @@ let finish ?(print_goals=false) () = VCS.print (); (* Some commands may by side effect change the proof mode *) match VCS.get_branch head with - | { VCS.kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode + | { VCS.kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode | _ -> () @@ -1982,7 +1989,7 @@ let merge_proof_branch ?valid ?id qast keep brname = VCS.delete_branch brname; if keep <> VtDrop then VCS.propagate_sideff None; `Ok - | { VCS.kind = `Edit (mode, qed_id, master_id) } -> + | { VCS.kind = `Edit (mode, qed_id, master_id, _) } -> let ofp = match VCS.visit qed_id with | { step = `Qed ({ fproof }, _) } -> fproof @@ -2136,9 +2143,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | { VCS.root; kind = `Proof(_,d); pos } -> VCS.delete_branch bn; VCS.branch ~root ~pos bn (`Proof(mode,d)) - | { VCS.root; kind = `Edit(_,f,q); pos } -> + | { VCS.root; kind = `Edit(_,f,q,k); pos } -> VCS.delete_branch bn; - VCS.branch ~root ~pos bn (`Edit(mode,f,q))) + VCS.branch ~root ~pos bn (`Edit(mode,f,q,k))) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); Backtrack.record (); @@ -2291,13 +2298,13 @@ let edit_at id = | { step = `Sideff (`Ast(_,id)|`Id id) } -> id | { next } -> master_for_br root next in let reopen_branch start at_id mode qed_id tip = - let master_id, cancel_switch = + let master_id, cancel_switch, keep = (* Hum, this should be the real start_id in the clusted and not next *) match VCS.visit qed_id with - | { step = `Qed ({ fproof = Some (_,cs)},_) } -> start, cs + | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep | _ -> anomaly (str "Cluster not ending with Qed") in VCS.branch ~root:master_id ~pos:id - VCS.edit_branch (`Edit (mode, qed_id, master_id)); + VCS.edit_branch (`Edit (mode, qed_id, master_id, keep)); VCS.delete_cluster_of id; cancel_switch := true; Reach.known_state ~cache:(interactive ()) id; @@ -2324,7 +2331,7 @@ let edit_at id = let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in let branch_info = match snd (VCS.get_info id).vcs_backup with - | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_)) }} -> Some m + | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_,_)) }} -> Some m | _ -> None in match focused, VCS.cluster_of id, branch_info with | _, Some _, None -> assert false diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 083fd54bf..180f20ae8 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -117,8 +117,8 @@ let xmlReference ref = let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml -let xmlAddLoaPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml -let xmlRemoveLoaPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr +let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml +let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml @@ -667,12 +667,11 @@ let rec tmpp v loc = (* Auxiliary file and library management *) | VernacAddLoadPath (recf,name,None) -> - xmlAddLoaPath loc ~attr:["rec",string_of_bool recf;"path",name] [] + xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] [] | VernacAddLoadPath (recf,name,Some dp) -> - xmlAddLoaPath loc ~attr:["rec",string_of_bool recf;"path",name] + xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] [PCData (Names.DirPath.to_string dp)] - - | VernacRemoveLoadPath name -> xmlRemoveLoaPath loc ~attr:["path",name] [] + | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] [] | VernacAddMLPath (recf,name) -> xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] [] | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index ee8e1855d..4eb8a7925 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -211,6 +211,7 @@ let cache_hintrewrite (_,(rbase,lrl)) = let base = try raw_find_base rbase with Not_found -> HintDN.empty in let max = try fst (Util.List.last (HintDN.find_all base)) with Failure _ -> 0 in + let lrl = HintDN.refresh_metas lrl in let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index c0fe514f0..244f9a727 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -350,7 +350,9 @@ let make_autogoal_hints = let sign = pf_filtered_hyps g in let (onlyc, sign', cached_hints) = !cache in if onlyc == only_classes && - (sign == sign' || Environ.eq_named_context_val sign sign') then + (sign == sign' || Environ.eq_named_context_val sign sign') + && Hint_db.transparent_state cached_hints == st + then cached_hints else let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in diff --git a/tactics/dnet.ml b/tactics/dnet.ml index bb71620c0..93334db73 100644 --- a/tactics/dnet.ml +++ b/tactics/dnet.ml @@ -39,6 +39,7 @@ sig val inter : t -> t -> t val union : t -> t -> t val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t + val map_metas : (meta -> meta) -> t -> t end module Make = @@ -288,4 +289,13 @@ struct | Node e -> Node (T.map (map sidset sterm) e) in Nodes (tmap_map sterm snode t, Mmap.map (idset_map sidset) m) + let rec map_metas f (Nodes (t, m)) : t = + let f_node = function + | Terminal (e, is) -> Terminal (T.map (map_metas f) e, is) + | Node e -> Node (T.map (map_metas f) e) + in + let m' = Mmap.fold (fun m s acc -> Mmap.add (f m) s acc) m Mmap.empty in + let t' = Tmap.fold (fun k n acc -> Tmap.add k (f_node n) acc) t Tmap.empty in + Nodes (t', m') + end diff --git a/tactics/dnet.mli b/tactics/dnet.mli index 4bfa7263e..52853d702 100644 --- a/tactics/dnet.mli +++ b/tactics/dnet.mli @@ -113,6 +113,8 @@ sig (** apply a function on each identifier and node of terms in a dnet *) val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t + + val map_metas : (meta -> meta) -> t -> t end module Make : diff --git a/tactics/equality.ml b/tactics/equality.ml index 838f8865d..bcfd6657e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1230,8 +1230,6 @@ let try_delta_expand env sigma t = let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined") let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k) -let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec" - let inject_if_homogenous_dependent_pair ty = Proofview.Goal.nf_enter begin fun gl -> try @@ -1254,7 +1252,7 @@ let inject_if_homogenous_dependent_pair ty = (* knows inductive types *) if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; - Library.require_library [Loc.ghost,eqdep_dec] (Some false); + Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index e637b2e36..e79fc6dc9 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -371,6 +371,17 @@ struct let find_all dn = Idset.elements (TDnet.find_all dn) let map f dn = TDnet.map f (fun x -> x) dn + + let refresh_metas dn = + let new_metas = ref Int.Map.empty in + let refresh_one_meta i = + try Int.Map.find i !new_metas + with Not_found -> + let new_meta = fresh_meta () in + let () = new_metas := Int.Map.add i new_meta !new_metas in + new_meta + in + TDnet.map_metas refresh_one_meta dn end module type S = @@ -385,4 +396,5 @@ sig val search_pattern : t -> constr -> ident list val find_all : t -> ident list val map : (ident -> ident) -> t -> t + val refresh_metas : t -> t end diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index a5c80cc00..58f95ac6c 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -80,6 +80,8 @@ sig val find_all : t -> ident list val map : (ident -> ident) -> t -> t + + val refresh_metas : t -> t end module Make : diff --git a/test-suite/bugs/closed/3815.v b/test-suite/bugs/closed/3815.v new file mode 100644 index 000000000..5fb483984 --- /dev/null +++ b/test-suite/bugs/closed/3815.v @@ -0,0 +1,9 @@ +Require Import Setoid Coq.Program.Basics. +Global Open Scope program_scope. +Axiom foo : forall A (f : A -> A), f ∘ f = f. +Require Import Coq.Program.Combinators. +Hint Rewrite foo. +Theorem t {A B C D} (f : A -> A) (g : B -> C) (h : C -> D) +: f ∘ f = f. +Proof. + rewrite_strat topdown (hints core). diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index 7c3cc6b79..4408ab885 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *) (* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *) diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index 9a1da16bf..7c1ab8dc2 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-nois" "-emacs") -*- *) +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *) (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *) Require Import Coq.Init.Logic. diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 6a4882443..25e464d67 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -1,3 +1,5 @@ +Require Eqdep_dec. + (* Check the behaviour of Injection *) (* Check that Injection tries Intro until *) diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 073cd5e96..048faa916 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -31,7 +31,7 @@ Set Universe Polymorphism. The relation [R] will be instantiated by [respectful] and [A] by an arrow type for usual morphisms. *) Section Proper. - Context {A B : Type}. + Context {A : Type}. Class Proper (R : crelation A) (m : A) := proper_prf : R m m. @@ -71,7 +71,7 @@ Section Proper. (** The non-dependent version is an instance where we forget dependencies. *) - Definition respectful (R : crelation A) (R' : crelation B) : crelation (A -> B) := + Definition respectful {B} (R : crelation A) (R' : crelation B) : crelation (A -> B) := Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). End Proper. @@ -143,7 +143,7 @@ Ltac f_equiv := end. Section Relations. - Context {A B : Type}. + Context {A : Type}. (** [forall_def] reifies the dependent product as a definition. *) @@ -156,10 +156,10 @@ Section Relations. fun f g => forall a, sig a (f a) (g a). (** Non-dependent pointwise lifting *) - Definition pointwise_relation (R : crelation B) : crelation (A -> B) := + Definition pointwise_relation {B} (R : crelation B) : crelation (A -> B) := fun f g => forall a, R (f a) (g a). - Lemma pointwise_pointwise (R : crelation B) : + Lemma pointwise_pointwise {B} (R : crelation B) : relation_equivalence (pointwise_relation R) (@eq A ==> R). Proof. intros. split. simpl_crelation. firstorder. Qed. @@ -252,7 +252,7 @@ Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S) Section GenericInstances. (* Share universes *) - Context {A B C : Type}. + Implicit Types A B C : Type. (** We can build a PER on the Coq function space if we have PERs on the domain and codomain. *) @@ -379,7 +379,7 @@ Section GenericInstances. Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R). Proof. firstorder. Qed. - Global Program Instance compose_proper RA RB RC : + Global Program Instance compose_proper A B C RA RB RC : Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C). Next Obligation. @@ -396,12 +396,12 @@ Section GenericInstances. Proof. simpl_crelation. Qed. (** [respectful] is a morphism for crelation equivalence . *) - Set Printing All. Set Printing Universes. + Global Instance respectful_morphism : Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. - intros R R' HRR' S S' HSS' f g. + intros A B R R' HRR' S S' HSS' f g. unfold respectful , relation_equivalence in *; simpl in *. split ; intros H x y Hxy. apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). @@ -414,9 +414,9 @@ Section GenericInstances. Proper R' (m x). Proof. simpl_crelation. Qed. - Class Params (of : A) (arity : nat). + Class Params {A} (of : A) (arity : nat). - Lemma flip_respectful (R : crelation A) (R' : crelation B) : + Lemma flip_respectful {A B} (R : crelation A) (R' : crelation B) : relation_equivalence (flip (R ==> R')) (flip R ==> flip R'). Proof. intros. @@ -449,7 +449,7 @@ Section GenericInstances. Lemma reflexive_proper `{Reflexive A R} (x : A) : Proper R x. Proof. firstorder. Qed. - Lemma proper_eq (x : A) : Proper (@eq A) x. + Lemma proper_eq {A} (x : A) : Proper (@eq A) x. Proof. intros. apply reflexive_proper. Qed. End GenericInstances. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 424ca0c8c..a7bdba90a 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -59,7 +59,7 @@ Reserved Notation "( x , y , .. , z )" (at level 0). (** Notation "{ x }" is reserved and has a special status as component of other notations such as "{ A } + { B }" and "A + { B }" (which - are at the same level than "x + y"); + are at the same level as "x + y"); "{ x }" is at level 0 to factor with "{ x : A | P }" *) Reserved Notation "{ x }" (at level 0, x at level 99). diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 85e364c01..1783085fc 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1014,11 +1014,17 @@ Proof. rewrite IHl; auto. Qed. +Lemma map_ext_in : + forall (A B : Type)(f g:A->B) l, (forall a, In a l -> f a = g a) -> map f l = map g l. +Proof. + induction l; simpl; auto. + intros; rewrite H by intuition; rewrite IHl; auto. +Qed. + Lemma map_ext : forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l. Proof. - induction l; simpl; auto. - rewrite H; rewrite IHl; auto. + intros; apply map_ext_in; auto. Qed. diff --git a/theories/MMaps/MMapAVL.v b/theories/MMaps/MMapAVL.v new file mode 100644 index 000000000..d840f1f32 --- /dev/null +++ b/theories/MMaps/MMapAVL.v @@ -0,0 +1,2158 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite map library. *) + +(** * MMapAVL *) + +(** This module implements maps using AVL trees. + It follows the implementation from Ocaml's standard library. + + See the comments at the beginning of MSetAVL for more details. +*) + +Require Import Bool PeanoNat BinInt Int MMapInterface MMapList. +Require Import Orders OrdersFacts OrdersLists. + +Set Implicit Arguments. +Unset Strict Implicit. +(* For nicer extraction, we create inductive principles + only when needed *) +Local Unset Elimination Schemes. + +(** Notations and helper lemma about pairs *) + +Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. +Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. + +(** * The Raw functor + + Functor of pure functions + separate proofs of invariant + preservation *) + +Module Raw (Import I:Int)(X: OrderedType). +Local Open Scope pair_scope. +Local Open Scope lazy_bool_scope. +Local Open Scope Int_scope. +Local Notation int := I.t. + +Definition key := X.t. +Hint Transparent key. + +(** * Trees *) + +Section Elt. + +Variable elt : Type. + +(** * Trees + + The fifth field of [Node] is the height of the tree *) + +Inductive tree := + | Leaf : tree + | Node : tree -> key -> elt -> tree -> int -> tree. + +Notation t := tree. + +(** * Basic functions on trees: height and cardinal *) + +Definition height (m : t) : int := + match m with + | Leaf => 0 + | Node _ _ _ _ h => h + end. + +Fixpoint cardinal (m : t) : nat := + match m with + | Leaf => 0%nat + | Node l _ _ r _ => S (cardinal l + cardinal r) + end. + +(** * Empty Map *) + +Definition empty := Leaf. + +(** * Emptyness test *) + +Definition is_empty m := match m with Leaf => true | _ => false end. + +(** * Membership *) + +(** The [mem] function is deciding membership. It exploits the [Bst] property + to achieve logarithmic complexity. *) + +Fixpoint mem x m : bool := + match m with + | Leaf => false + | Node l y _ r _ => + match X.compare x y with + | Eq => true + | Lt => mem x l + | Gt => mem x r + end + end. + +Fixpoint find x m : option elt := + match m with + | Leaf => None + | Node l y d r _ => + match X.compare x y with + | Eq => Some d + | Lt => find x l + | Gt => find x r + end + end. + +(** * Helper functions *) + +(** [create l x r] creates a node, assuming [l] and [r] + to be balanced and [|height l - height r| <= 2]. *) + +Definition create l x e r := + Node l x e r (max (height l) (height r) + 1). + +(** [bal l x e r] acts as [create], but performs one step of + rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *) + +Definition assert_false := create. + +Fixpoint bal l x d r := + let hl := height l in + let hr := height r in + if (hr+2) <? hl then + match l with + | Leaf => assert_false l x d r + | Node ll lx ld lr _ => + if (height lr) <=? (height ll) then + create ll lx ld (create lr x d r) + else + match lr with + | Leaf => assert_false l x d r + | Node lrl lrx lrd lrr _ => + create (create ll lx ld lrl) lrx lrd (create lrr x d r) + end + end + else + if (hl+2) <? hr then + match r with + | Leaf => assert_false l x d r + | Node rl rx rd rr _ => + if (height rl) <=? (height rr) then + create (create l x d rl) rx rd rr + else + match rl with + | Leaf => assert_false l x d r + | Node rll rlx rld rlr _ => + create (create l x d rll) rlx rld (create rlr rx rd rr) + end + end + else + create l x d r. + +(** * Insertion *) + +Fixpoint add x d m := + match m with + | Leaf => Node Leaf x d Leaf 1 + | Node l y d' r h => + match X.compare x y with + | Eq => Node l y d r h + | Lt => bal (add x d l) y d' r + | Gt => bal l y d' (add x d r) + end + end. + +(** * Extraction of minimum binding + + Morally, [remove_min] is to be applied to a non-empty tree + [t = Node l x e r h]. Since we can't deal here with [assert false] + for [t=Leaf], we pre-unpack [t] (and forget about [h]). +*) + +Fixpoint remove_min l x d r : t*(key*elt) := + match l with + | Leaf => (r,(x,d)) + | Node ll lx ld lr lh => + let (l',m) := remove_min ll lx ld lr in + (bal l' x d r, m) + end. + +(** * Merging two trees + + [merge0 t1 t2] builds the union of [t1] and [t2] assuming all elements + of [t1] to be smaller than all elements of [t2], and + [|height t1 - height t2| <= 2]. +*) + +Definition merge0 s1 s2 := + match s1,s2 with + | Leaf, _ => s2 + | _, Leaf => s1 + | _, Node l2 x2 d2 r2 h2 => + let '(s2',(x,d)) := remove_min l2 x2 d2 r2 in + bal s1 x d s2' + end. + +(** * Deletion *) + +Fixpoint remove x m := match m with + | Leaf => Leaf + | Node l y d r h => + match X.compare x y with + | Eq => merge0 l r + | Lt => bal (remove x l) y d r + | Gt => bal l y d (remove x r) + end + end. + +(** * join + + Same as [bal] but does not assume anything regarding heights of [l] + and [r]. +*) + +Fixpoint join l : key -> elt -> t -> t := + match l with + | Leaf => add + | Node ll lx ld lr lh => fun x d => + fix join_aux (r:t) : t := match r with + | Leaf => add x d l + | Node rl rx rd rr rh => + if rh+2 <? lh then bal ll lx ld (join lr x d r) + else if lh+2 <? rh then bal (join_aux rl) rx rd rr + else create l x d r + end + end. + +(** * Splitting + + [split x m] returns a triple [(l, o, r)] where + - [l] is the set of elements of [m] that are [< x] + - [r] is the set of elements of [m] that are [> x] + - [o] is the result of [find x m]. +*) + +Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }. +Notation "〚 l , b , r 〛" := (mktriple l b r) (at level 9). + +Fixpoint split x m : triple := match m with + | Leaf => 〚 Leaf, None, Leaf 〛 + | Node l y d r h => + match X.compare x y with + | Lt => let (ll,o,rl) := split x l in 〚 ll, o, join rl y d r 〛 + | Eq => 〚 l, Some d, r 〛 + | Gt => let (rl,o,rr) := split x r in 〚 join l y d rl, o, rr 〛 + end + end. + +(** * Concatenation + + Same as [merge] but does not assume anything about heights. +*) + +Definition concat m1 m2 := + match m1, m2 with + | Leaf, _ => m2 + | _ , Leaf => m1 + | _, Node l2 x2 d2 r2 _ => + let (m2',xd) := remove_min l2 x2 d2 r2 in + join m1 xd#1 xd#2 m2' + end. + +(** * Bindings *) + +(** [bindings_aux acc t] catenates the bindings of [t] in infix + order to the list [acc] *) + +Fixpoint bindings_aux (acc : list (key*elt)) m : list (key*elt) := + match m with + | Leaf => acc + | Node l x d r _ => bindings_aux ((x,d) :: bindings_aux acc r) l + end. + +(** then [bindings] is an instantiation with an empty [acc] *) + +Definition bindings := bindings_aux nil. + +(** * Fold *) + +Fixpoint fold {A} (f : key -> elt -> A -> A) (m : t) : A -> A := + fun a => match m with + | Leaf => a + | Node l x d r _ => fold f r (f x d (fold f l a)) + end. + +(** * Comparison *) + +Variable cmp : elt->elt->bool. + +(** ** Enumeration of the elements of a tree *) + +Inductive enumeration := + | End : enumeration + | More : key -> elt -> t -> enumeration -> enumeration. + +(** [cons m e] adds the elements of tree [m] on the head of + enumeration [e]. *) + +Fixpoint cons m e : enumeration := + match m with + | Leaf => e + | Node l x d r h => cons l (More x d r e) + end. + +(** One step of comparison of elements *) + +Definition equal_more x1 d1 (cont:enumeration->bool) e2 := + match e2 with + | End => false + | More x2 d2 r2 e2 => + match X.compare x1 x2 with + | Eq => cmp d1 d2 &&& cont (cons r2 e2) + | _ => false + end + end. + +(** Comparison of left tree, middle element, then right tree *) + +Fixpoint equal_cont m1 (cont:enumeration->bool) e2 := + match m1 with + | Leaf => cont e2 + | Node l1 x1 d1 r1 _ => + equal_cont l1 (equal_more x1 d1 (equal_cont r1 cont)) e2 + end. + +(** Initial continuation *) + +Definition equal_end e2 := match e2 with End => true | _ => false end. + +(** The complete comparison *) + +Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End). + +End Elt. +Notation t := tree. +Notation "〚 l , b , r 〛" := (mktriple l b r) (at level 9). +Notation "t #l" := (t_left t) (at level 9, format "t '#l'"). +Notation "t #o" := (t_opt t) (at level 9, format "t '#o'"). +Notation "t #r" := (t_right t) (at level 9, format "t '#r'"). + + +(** * Map *) + +Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' := + match m with + | Leaf _ => Leaf _ + | Node l x d r h => Node (map f l) x (f d) (map f r) h + end. + +(* * Mapi *) + +Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' := + match m with + | Leaf _ => Leaf _ + | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h + end. + +(** * Map with removal *) + +Fixpoint mapo (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt) + : t elt' := + match m with + | Leaf _ => Leaf _ + | Node l x d r h => + match f x d with + | Some d' => join (mapo f l) x d' (mapo f r) + | None => concat (mapo f l) (mapo f r) + end + end. + +(** * Generalized merge + + Suggestion by B. Gregoire: a [merge] function with specialized + arguments that allows bypassing some tree traversal. Instead of one + [f0] of type [key -> option elt -> option elt' -> option elt''], + we ask here for: + - [f] which is a specialisation of [f0] when first option isn't [None] + - [mapl] treats a [tree elt] with [f0] when second option is [None] + - [mapr] treats a [tree elt'] with [f0] when first option is [None] + + The idea is that [mapl] and [mapr] can be instantaneous (e.g. + the identity or some constant function). +*) + +Section GMerge. +Variable elt elt' elt'' : Type. +Variable f : key -> elt -> option elt' -> option elt''. +Variable mapl : t elt -> t elt''. +Variable mapr : t elt' -> t elt''. + +Fixpoint gmerge m1 m2 := + match m1, m2 with + | Leaf _, _ => mapr m2 + | _, Leaf _ => mapl m1 + | Node l1 x1 d1 r1 h1, _ => + let (l2',o2,r2') := split x1 m2 in + match f x1 d1 o2 with + | Some e => join (gmerge l1 l2') x1 e (gmerge r1 r2') + | None => concat (gmerge l1 l2') (gmerge r1 r2') + end + end. + +End GMerge. + +(** * Merge + + The [merge] function of the Map interface can be implemented + via [gmerge] and [mapo]. +*) + +Section Merge. +Variable elt elt' elt'' : Type. +Variable f : key -> option elt -> option elt' -> option elt''. + +Definition merge : t elt -> t elt' -> t elt'' := + gmerge + (fun k d o => f k (Some d) o) + (mapo (fun k d => f k (Some d) None)) + (mapo (fun k d' => f k None (Some d'))). + +End Merge. + + + +(** * Invariants *) + +Section Invariants. +Variable elt : Type. + +(** ** Occurrence in a tree *) + +Inductive MapsTo (x : key)(e : elt) : t elt -> Prop := + | MapsRoot : forall l r h y, + X.eq x y -> MapsTo x e (Node l y e r h) + | MapsLeft : forall l r h y e', + MapsTo x e l -> MapsTo x e (Node l y e' r h) + | MapsRight : forall l r h y e', + MapsTo x e r -> MapsTo x e (Node l y e' r h). + +Inductive In (x : key) : t elt -> Prop := + | InRoot : forall l r h y e, + X.eq x y -> In x (Node l y e r h) + | InLeft : forall l r h y e', + In x l -> In x (Node l y e' r h) + | InRight : forall l r h y e', + In x r -> In x (Node l y e' r h). + +Definition In0 k m := exists e:elt, MapsTo k e m. + +(** ** Binary search trees *) + +(** [Above x m] : [x] is strictly greater than any key in [m]. + [Below x m] : [x] is strictly smaller than any key in [m]. *) + +Inductive Above (x:key) : t elt -> Prop := + | AbLeaf : Above x (Leaf _) + | AbNode l r h y e : Above x l -> X.lt y x -> Above x r -> + Above x (Node l y e r h). + +Inductive Below (x:key) : t elt -> Prop := + | BeLeaf : Below x (Leaf _) + | BeNode l r h y e : Below x l -> X.lt x y -> Below x r -> + Below x (Node l y e r h). + +Definition Apart (m1 m2 : t elt) : Prop := + forall x1 x2, In x1 m1 -> In x2 m2 -> X.lt x1 x2. + +(** Alternative statements, equivalent with [LtTree] and [GtTree] *) + +Definition lt_tree x m := forall y, In y m -> X.lt y x. +Definition gt_tree x m := forall y, In y m -> X.lt x y. + +(** [Bst t] : [t] is a binary search tree *) + +Inductive Bst : t elt -> Prop := + | BSLeaf : Bst (Leaf _) + | BSNode : forall x e l r h, Bst l -> Bst r -> + Above x l -> Below x r -> Bst (Node l x e r h). + +End Invariants. + + +(** * Correctness proofs, isolated in a sub-module *) + +Module Proofs. + Module MX := OrderedTypeFacts X. + Module PX := KeyOrderedType X. + Module L := MMapList.Raw X. + +Local Infix "∈" := In (at level 70). +Local Infix "==" := X.eq (at level 70). +Local Infix "<" := X.lt (at level 70). +Local Infix "<<" := Below (at level 70). +Local Infix ">>" := Above (at level 70). +Local Infix "<<<" := Apart (at level 70). + +Scheme tree_ind := Induction for tree Sort Prop. +Scheme Bst_ind := Induction for Bst Sort Prop. +Scheme MapsTo_ind := Induction for MapsTo Sort Prop. +Scheme In_ind := Induction for In Sort Prop. +Scheme Above_ind := Induction for Above Sort Prop. +Scheme Below_ind := Induction for Below Sort Prop. + +Functional Scheme mem_ind := Induction for mem Sort Prop. +Functional Scheme find_ind := Induction for find Sort Prop. +Functional Scheme bal_ind := Induction for bal Sort Prop. +Functional Scheme add_ind := Induction for add Sort Prop. +Functional Scheme remove_min_ind := Induction for remove_min Sort Prop. +Functional Scheme merge0_ind := Induction for merge0 Sort Prop. +Functional Scheme remove_ind := Induction for remove Sort Prop. +Functional Scheme concat_ind := Induction for concat Sort Prop. +Functional Scheme split_ind := Induction for split Sort Prop. +Functional Scheme mapo_ind := Induction for mapo Sort Prop. +Functional Scheme gmerge_ind := Induction for gmerge Sort Prop. + +(** * Automation and dedicated tactics. *) + +Local Hint Constructors tree MapsTo In Bst Above Below. +Local Hint Unfold lt_tree gt_tree Apart. +Local Hint Immediate MX.eq_sym. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans. + +Tactic Notation "factornode" ident(s) := + try clear s; + match goal with + | |- context [Node ?l ?x ?e ?r ?h] => + set (s:=Node l x e r h) in *; clearbody s; clear l x e r h + | _ : context [Node ?l ?x ?e ?r ?h] |- _ => + set (s:=Node l x e r h) in *; clearbody s; clear l x e r h + end. + +(** A tactic for cleaning hypothesis after use of functional induction. *) + +Ltac cleanf := + match goal with + | H : X.compare _ _ = Eq |- _ => + rewrite ?H; apply MX.compare_eq in H; cleanf + | H : X.compare _ _ = Lt |- _ => + rewrite ?H; apply MX.compare_lt_iff in H; cleanf + | H : X.compare _ _ = Gt |- _ => + rewrite ?H; apply MX.compare_gt_iff in H; cleanf + | _ => idtac + end. + + +(** A tactic to repeat [inversion_clear] on all hyps of the + form [(f (Node ...))] *) + +Ltac inv f := + match goal with + | H:f (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f _ _ _ (Leaf _) |- _ => inversion_clear H; inv f + | H:f (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f + | _ => idtac + end. + +Ltac inv_all f := + match goal with + | H: f _ |- _ => inversion_clear H; inv f + | H: f _ _ |- _ => inversion_clear H; inv f + | H: f _ _ _ |- _ => inversion_clear H; inv f + | H: f _ _ _ _ |- _ => inversion_clear H; inv f + | _ => idtac + end. + +Ltac intuition_in := repeat (intuition; inv In; inv MapsTo). + +(* Function/Functional Scheme can't deal with internal fix. + Let's do its job by hand: *) + +Ltac join_tac l x d r := + revert x d r; + induction l as [| ll _ lx ld lr Hlr lh]; + [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join; + [ | destruct (rh+2 <? lh) eqn:LT; + [ match goal with |- context [ bal ?u ?v ?w ?z ] => + replace (bal u v w z) + with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto] + end + | destruct (lh+2 <? rh) eqn:LT'; + [ match goal with |- context [ bal ?u ?v ?w ?z ] => + replace (bal u v w z) + with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] + end + | ] ] ] ]; intros. + +Ltac cleansplit := + simpl; cleanf; inv Bst; + match goal with + | E:split _ _ = 〚 ?l, ?o, ?r 〛 |- _ => + change l with (〚l,o,r〛#l); rewrite <- ?E; + change o with (〚l,o,r〛#o); rewrite <- ?E; + change r with (〚l,o,r〛#r); rewrite <- ?E + | _ => idtac + end. + +(** * Basic results about [MapsTo], [In], [lt_tree], [gt_tree], [height] *) + +(** Facts about [MapsTo] and [In]. *) + +Lemma MapsTo_In {elt} k (e:elt) m : MapsTo k e m -> k ∈ m. +Proof. + induction 1; auto. +Qed. +Local Hint Resolve MapsTo_In. + +Lemma In_MapsTo {elt} k m : k ∈ m -> exists (e:elt), MapsTo k e m. +Proof. + induction 1; try destruct IHIn as (e,He); exists e; auto. +Qed. + +Lemma In_alt {elt} k (m:t elt) : In0 k m <-> k ∈ m. +Proof. + split. + intros (e,H); eauto. + unfold In0; apply In_MapsTo; auto. +Qed. + +Lemma MapsTo_1 {elt} m x y (e:elt) : + x == y -> MapsTo x e m -> MapsTo y e m. +Proof. + induction m; simpl; intuition_in; eauto. +Qed. +Hint Immediate MapsTo_1. + +Instance MapsTo_compat {elt} : + Proper (X.eq==>Logic.eq==>Logic.eq==>iff) (@MapsTo elt). +Proof. + intros x x' Hx e e' He m m' Hm. subst. + split; now apply MapsTo_1. +Qed. + +Instance In_compat {elt} : + Proper (X.eq==>Logic.eq==>iff) (@In elt). +Proof. + intros x x' H m m' <-. + induction m; simpl; intuition_in; eauto. +Qed. + +Lemma In_node_iff {elt} l x (e:elt) r h y : + y ∈ (Node l x e r h) <-> y ∈ l \/ y == x \/ y ∈ r. +Proof. + intuition_in. +Qed. + +(** Results about [Above] and [Below] *) + +Lemma above {elt} (m:t elt) x : + x >> m <-> forall y, y ∈ m -> y < x. +Proof. + split. + - induction 1; intuition_in; MX.order. + - induction m; constructor; auto. +Qed. + +Lemma below {elt} (m:t elt) x : + x << m <-> forall y, y ∈ m -> x < y. +Proof. + split. + - induction 1; intuition_in; MX.order. + - induction m; constructor; auto. +Qed. + +Lemma AboveLt {elt} (m:t elt) x y : x >> m -> y ∈ m -> y < x. +Proof. + rewrite above; intuition. +Qed. + +Lemma BelowGt {elt} (m:t elt) x y : x << m -> y ∈ m -> x < y. +Proof. + rewrite below; intuition. +Qed. + +Lemma Above_not_In {elt} (m:t elt) x : x >> m -> ~ x ∈ m. +Proof. + induction 1; intuition_in; MX.order. +Qed. + +Lemma Below_not_In {elt} (m:t elt) x : x << m -> ~ x ∈ m. +Proof. + induction 1; intuition_in; MX.order. +Qed. + +Lemma Above_trans {elt} (m:t elt) x y : x < y -> x >> m -> y >> m. +Proof. + induction 2; constructor; trivial; MX.order. +Qed. + +Lemma Below_trans {elt} (m:t elt) x y : y < x -> x << m -> y << m. +Proof. + induction 2; constructor; trivial; MX.order. +Qed. + +Local Hint Resolve + AboveLt Above_not_In Above_trans + BelowGt Below_not_In Below_trans. + +(** Helper tactic concerning order of elements. *) + +Ltac order := match goal with + | U: _ >> ?m, V: _ ∈ ?m |- _ => + generalize (AboveLt U V); clear U; order + | U: _ << ?m, V: _ ∈ ?m |- _ => + generalize (BelowGt U V); clear U; order + | U: _ >> ?m, V: MapsTo _ _ ?m |- _ => + generalize (AboveLt U (MapsTo_In V)); clear U; order + | U: _ << ?m, V: MapsTo _ _ ?m |- _ => + generalize (BelowGt U (MapsTo_In V)); clear U; order + | _ => MX.order +end. + +Lemma between {elt} (m m':t elt) x : + x >> m -> x << m' -> m <<< m'. +Proof. + intros H H' y y' Hy Hy'. order. +Qed. + +Section Elt. +Variable elt:Type. +Implicit Types m r : t elt. + +(** * Membership *) + +Lemma find_1 m x e : Bst m -> MapsTo x e m -> find x m = Some e. +Proof. + functional induction (find x m); cleanf; + intros; inv Bst; intuition_in; order. +Qed. + +Lemma find_2 m x e : find x m = Some e -> MapsTo x e m. +Proof. + functional induction (find x m); cleanf; subst; intros; auto. + - discriminate. + - injection H as ->. auto. +Qed. + +Lemma find_spec m x e : Bst m -> + (find x m = Some e <-> MapsTo x e m). +Proof. + split; auto using find_1, find_2. +Qed. + +Lemma find_in m x : find x m <> None -> x ∈ m. +Proof. + destruct (find x m) eqn:F; intros H. + - apply MapsTo_In with e. now apply find_2. + - now elim H. +Qed. + +Lemma in_find m x : Bst m -> x ∈ m -> find x m <> None. +Proof. + intros H H'. + destruct (In_MapsTo H') as (d,Hd). + now rewrite (find_1 H Hd). +Qed. + +Lemma find_in_iff m x : Bst m -> + (find x m <> None <-> x ∈ m). +Proof. + split; auto using find_in, in_find. +Qed. + +Lemma not_find_iff m x : Bst m -> + (find x m = None <-> ~ x ∈ m). +Proof. + intros H. rewrite <- find_in_iff; trivial. + destruct (find x m); split; try easy. now destruct 1. +Qed. + +Lemma eq_option_alt (o o':option elt) : + o=o' <-> (forall e, o=Some e <-> o'=Some e). +Proof. +split; intros. +- now subst. +- destruct o, o'; rewrite ?H; auto. symmetry; now apply H. +Qed. + +Lemma find_mapsto_equiv : forall m m' x, Bst m -> Bst m' -> + (find x m = find x m' <-> + (forall d, MapsTo x d m <-> MapsTo x d m')). +Proof. + intros m m' x Hm Hm'. rewrite eq_option_alt. + split; intros H d. now rewrite <- 2 find_spec. now rewrite 2 find_spec. +Qed. + +Lemma find_in_equiv : forall m m' x, Bst m -> Bst m' -> + find x m = find x m' -> + (x ∈ m <-> x ∈ m'). +Proof. + split; intros; apply find_in; [ rewrite <- H1 | rewrite H1 ]; + apply in_find; auto. +Qed. + +Lemma find_compat m x x' : Bst m -> X.eq x x' -> find x m = find x' m. +Proof. + intros B E. + destruct (find x' m) eqn:H. + - apply find_1; trivial. rewrite E. now apply find_2. + - rewrite not_find_iff in *; trivial. now rewrite E. +Qed. + +Lemma mem_spec m x : Bst m -> mem x m = true <-> x ∈ m. +Proof. + functional induction (mem x m); auto; intros; cleanf; + inv Bst; intuition_in; try discriminate; order. +Qed. + +(** * Empty map *) + +Lemma empty_bst : Bst (empty elt). +Proof. + constructor. +Qed. + +Lemma empty_spec x : find x (empty elt) = None. +Proof. + reflexivity. +Qed. + +(** * Emptyness test *) + +Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None. +Proof. + destruct m as [|r x e l h]; simpl; split; try easy. + intros H. specialize (H x). now rewrite MX.compare_refl in H. +Qed. + +(** * Helper functions *) + +Lemma create_bst l x e r : + Bst l -> Bst r -> x >> l -> x << r -> Bst (create l x e r). +Proof. + unfold create; auto. +Qed. +Hint Resolve create_bst. + +Lemma create_in l x e r y : + y ∈ (create l x e r) <-> y == x \/ y ∈ l \/ y ∈ r. +Proof. + unfold create; split; [ inversion_clear 1 | ]; intuition. +Qed. + +Lemma bal_bst l x e r : Bst l -> Bst r -> + x >> l -> x << r -> Bst (bal l x e r). +Proof. + functional induction (bal l x e r); intros; cleanf; + inv Bst; inv Above; inv Below; + repeat apply create_bst; auto; unfold create; constructor; eauto. +Qed. +Hint Resolve bal_bst. + +Lemma bal_in l x e r y : + y ∈ (bal l x e r) <-> y == x \/ y ∈ l \/ y ∈ r. +Proof. + functional induction (bal l x e r); intros; cleanf; + rewrite !create_in; intuition_in. +Qed. + +Lemma bal_mapsto l x e r y e' : + MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r). +Proof. + functional induction (bal l x e r); intros; cleanf; + unfold assert_false, create; intuition_in. +Qed. + +Lemma bal_find l x e r y : + Bst l -> Bst r -> x >> l -> x << r -> + find y (bal l x e r) = find y (create l x e r). +Proof. + functional induction (bal l x e r); intros; cleanf; trivial; + inv Bst; inv Above; inv Below; + simpl; repeat case X.compare_spec; intuition; order. +Qed. + +(** * Insertion *) + +Lemma add_in m x y e : + y ∈ (add x e m) <-> y == x \/ y ∈ m. +Proof. + functional induction (add x e m); auto; intros; cleanf; + rewrite ?bal_in; intuition_in. setoid_replace y with x; auto. +Qed. + +Lemma add_lt m x e y : y >> m -> x < y -> y >> add x e m. +Proof. + intros. apply above. intros z. rewrite add_in. destruct 1; order. +Qed. + +Lemma add_gt m x e y : y << m -> y < x -> y << add x e m. +Proof. + intros. apply below. intros z. rewrite add_in. destruct 1; order. +Qed. + +Lemma add_bst m x e : Bst m -> Bst (add x e m). +Proof. + functional induction (add x e m); intros; cleanf; + inv Bst; try apply bal_bst; auto using add_lt, add_gt. +Qed. +Hint Resolve add_lt add_gt add_bst. + +Lemma add_spec1 m x e : Bst m -> find x (add x e m) = Some e. +Proof. + functional induction (add x e m); simpl; intros; cleanf; trivial. + - now rewrite MX.compare_refl. + - inv Bst. rewrite bal_find; auto. + simpl. case X.compare_spec; try order; auto. + - inv Bst. rewrite bal_find; auto. + simpl. case X.compare_spec; try order; auto. +Qed. + +Lemma add_spec2 m x y e : Bst m -> ~ x == y -> + find y (add x e m) = find y m. +Proof. + functional induction (add x e m); simpl; intros; cleanf; trivial. + - case X.compare_spec; trivial; order. + - case X.compare_spec; trivial; order. + - inv Bst. rewrite bal_find by auto. simpl. now rewrite IHt. + - inv Bst. rewrite bal_find by auto. simpl. now rewrite IHt. +Qed. + +Lemma add_find m x y e : Bst m -> + find y (add x e m) = + match X.compare y x with Eq => Some e | _ => find y m end. +Proof. + intros. + case X.compare_spec; intros. + - apply find_spec; auto. rewrite H0. apply find_spec; auto. + now apply add_spec1. + - apply add_spec2; trivial; order. + - apply add_spec2; trivial; order. +Qed. + +(** * Extraction of minimum binding *) + +Definition RemoveMin m res := + match m with + | Leaf _ => False + | Node l x e r h => remove_min l x e r = res + end. + +Lemma RemoveMin_step l x e r h m' p : + RemoveMin (Node l x e r h) (m',p) -> + (l = Leaf _ /\ m' = r /\ p = (x,e) \/ + exists m0, RemoveMin l (m0,p) /\ m' = bal m0 x e r). +Proof. + simpl. destruct l as [|ll lx le lr lh]; simpl. + - intros [= -> ->]. now left. + - destruct (remove_min ll lx le lr) as (l',p'). + intros [= <- <-]. right. now exists l'. +Qed. + +Lemma remove_min_mapsto m m' p : RemoveMin m (m',p) -> + forall y e, + MapsTo y e m <-> (y == p#1 /\ e = p#2) \/ MapsTo y e m'. +Proof. + revert m'. + induction m as [|l IH x d r _ h]; [destruct 1|]. + intros m' R. apply RemoveMin_step in R. + destruct R as [(->,(->,->))|[m0 (R,->)]]; intros y e; simpl. + - intuition_in. subst. now constructor. + - rewrite bal_mapsto. unfold create. specialize (IH _ R y e). + intuition_in. +Qed. + +Lemma remove_min_in m m' p : RemoveMin m (m',p) -> + forall y, y ∈ m <-> y == p#1 \/ y ∈ m'. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R y. apply RemoveMin_step in R. + destruct R as [(->,(->,->))|[m0 (R,->)]]. + + intuition_in. + + rewrite bal_in, In_node_iff, (IH _ R); intuition. +Qed. + +Lemma remove_min_lt m m' p : RemoveMin m (m',p) -> + forall y, y >> m -> y >> m'. +Proof. + intros R y L. apply above. intros z Hz. + apply (AboveLt L). + apply (remove_min_in R). now right. +Qed. + +Lemma remove_min_gt m m' p : RemoveMin m (m',p) -> + Bst m -> p#1 << m'. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R H. inv Bst. apply RemoveMin_step in R. + destruct R as [(_,(->,->))|[m0 (R,->)]]; auto. + assert (p#1 << m0) by now apply IH. + assert (In p#1 l) by (apply (remove_min_in R); now left). + apply below. intros z. rewrite bal_in. + intuition_in; order. +Qed. + +Lemma remove_min_bst m m' p : RemoveMin m (m',p) -> + Bst m -> Bst m'. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R H. inv Bst. apply RemoveMin_step in R. + destruct R as [(_,(->,->))|[m0 (R,->)]]; auto. + apply bal_bst; eauto using remove_min_lt. +Qed. + +Lemma remove_min_find m m' p : RemoveMin m (m',p) -> + Bst m -> + forall y, + find y m = + match X.compare y p#1 with + | Eq => Some p#2 + | Lt => None + | Gt => find y m' + end. +Proof. + revert m'. + induction m as [|l IH x e r _ h]; [destruct 1|]. + intros m' R B y. inv Bst. apply RemoveMin_step in R. + destruct R as [(->,(->,->))|[m0 (R,->)]]; auto. + assert (Bst m0) by now apply (remove_min_bst R). + assert (p#1 << m0) by now apply (remove_min_gt R). + assert (x >> m0) by now apply (remove_min_lt R). + assert (In p#1 l) by (apply (remove_min_in R); now left). + simpl in *. + rewrite (IH _ R), bal_find by trivial. clear IH. simpl. + do 2 case X.compare_spec; trivial; try order. +Qed. + +(** * Merging two trees *) + +Ltac factor_remove_min m R := match goal with + | h:int, H:remove_min ?l ?x ?e ?r = ?p |- _ => + assert (R:RemoveMin (Node l x e r h) p) by exact H; + set (m:=Node l x e r h) in *; clearbody m; clear H l x e r +end. + +Lemma merge0_in m1 m2 y : + y ∈ (merge0 m1 m2) <-> y ∈ m1 \/ y ∈ m2. +Proof. + functional induction (merge0 m1 m2); intros; try factornode m1. + - intuition_in. + - intuition_in. + - factor_remove_min l R. rewrite bal_in, (remove_min_in R). + simpl; intuition. +Qed. + +Lemma merge0_mapsto m1 m2 y e : + MapsTo y e (merge0 m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2. +Proof. + functional induction (merge0 m1 m2); intros; try factornode m1. + - intuition_in. + - intuition_in. + - factor_remove_min l R. rewrite bal_mapsto, (remove_min_mapsto R). + simpl. unfold create; intuition_in. subst. now constructor. +Qed. + +Lemma merge0_bst m1 m2 : Bst m1 -> Bst m2 -> m1 <<< m2 -> + Bst (merge0 m1 m2). +Proof. + functional induction (merge0 m1 m2); intros B1 B2 B12; trivial. + factornode m1. factor_remove_min l R. + apply bal_bst; auto. + - eapply remove_min_bst; eauto. + - apply above. intros z Hz. apply B12; trivial. + rewrite (remove_min_in R). now left. + - now apply (remove_min_gt R). +Qed. +Hint Resolve merge0_bst. + +(** * Deletion *) + +Lemma remove_in m x y : Bst m -> + (y ∈ remove x m <-> ~ y == x /\ y ∈ m). +Proof. + functional induction (remove x m); simpl; intros; cleanf; inv Bst; + rewrite ?merge0_in, ?bal_in, ?IHt; intuition_in; order. +Qed. + +Lemma remove_lt m x y : Bst m -> y >> m -> y >> remove x m. +Proof. + intros. apply above. intro. rewrite remove_in by trivial. + destruct 1; order. +Qed. + +Lemma remove_gt m x y : Bst m -> y << m -> y << remove x m. +Proof. + intros. apply below. intro. rewrite remove_in by trivial. + destruct 1; order. +Qed. + +Lemma remove_bst m x : Bst m -> Bst (remove x m). +Proof. + functional induction (remove x m); simpl; intros; cleanf; inv Bst. + - trivial. + - apply merge0_bst; eauto. + - apply bal_bst; auto using remove_lt. + - apply bal_bst; auto using remove_gt. +Qed. +Hint Resolve remove_bst remove_gt remove_lt. + +Lemma remove_spec1 m x : Bst m -> find x (remove x m) = None. +Proof. + intros. apply not_find_iff; auto. rewrite remove_in; intuition. +Qed. + +Lemma remove_spec2 m x y : Bst m -> ~ x == y -> + find y (remove x m) = find y m. +Proof. + functional induction (remove x m); simpl; intros; cleanf; inv Bst. + - trivial. + - case X.compare_spec; intros; try order; + rewrite find_mapsto_equiv; auto. + + intros. rewrite merge0_mapsto; intuition; order. + + apply merge0_bst; auto. red; intros; transitivity y0; order. + + intros. rewrite merge0_mapsto; intuition; order. + + apply merge0_bst; auto. now apply between with y0. + - rewrite bal_find by auto. simpl. case X.compare_spec; auto. + - rewrite bal_find by auto. simpl. case X.compare_spec; auto. +Qed. + +(** * join *) + +Lemma join_in l x d r y : + y ∈ (join l x d r) <-> y == x \/ y ∈ l \/ y ∈ r. +Proof. + join_tac l x d r. + - simpl join. rewrite add_in. intuition_in. + - rewrite add_in. intuition_in. + - rewrite bal_in, Hlr. clear Hlr Hrl. intuition_in. + - rewrite bal_in, Hrl; clear Hlr Hrl; intuition_in. + - apply create_in. +Qed. + +Lemma join_bst l x d r : + Bst (create l x d r) -> Bst (join l x d r). +Proof. + join_tac l x d r; unfold create in *; + inv Bst; inv Above; inv Below; auto. + - simpl. auto. + - apply bal_bst; auto. + apply below. intro. rewrite join_in. intuition_in; order. + - apply bal_bst; auto. + apply above. intro. rewrite join_in. intuition_in; order. +Qed. +Hint Resolve join_bst. + +Lemma join_find l x d r y : + Bst (create l x d r) -> + find y (join l x d r) = find y (create l x d r). +Proof. + unfold create at 1. + join_tac l x d r; trivial. + - simpl in *. inv Bst. + rewrite add_find; trivial. + case X.compare_spec; intros; trivial. + apply not_find_iff; auto. intro. order. + - clear Hlr. factornode l. simpl. inv Bst. + rewrite add_find by auto. + case X.compare_spec; intros; trivial. + apply not_find_iff; auto. intro. order. + - clear Hrl LT. factornode r. inv Bst; inv Above; inv Below. + rewrite bal_find; auto; simpl. + + rewrite Hlr; auto; simpl. + repeat (case X.compare_spec; trivial; try order). + + apply below. intro. rewrite join_in. intuition_in; order. + - clear Hlr LT LT'. factornode l. inv Bst; inv Above; inv Below. + rewrite bal_find; auto; simpl. + + rewrite Hrl; auto; simpl. + repeat (case X.compare_spec; trivial; try order). + + apply above. intro. rewrite join_in. intuition_in; order. +Qed. + +(** * split *) + +Lemma split_in_l0 m x y : y ∈ (split x m)#l -> y ∈ m. +Proof. + functional induction (split x m); cleansplit; + rewrite ?join_in; intuition. +Qed. + +Lemma split_in_r0 m x y : y ∈ (split x m)#r -> y ∈ m. +Proof. + functional induction (split x m); cleansplit; + rewrite ?join_in; intuition. +Qed. + +Lemma split_in_l m x y : Bst m -> + (y ∈ (split x m)#l <-> y ∈ m /\ y < x). +Proof. + functional induction (split x m); intros; cleansplit; + rewrite ?join_in, ?IHt; intuition_in; order. +Qed. + +Lemma split_in_r m x y : Bst m -> + (y ∈ (split x m)#r <-> y ∈ m /\ x < y). +Proof. + functional induction (split x m); intros; cleansplit; + rewrite ?join_in, ?IHt; intuition_in; order. +Qed. + +Lemma split_in_o m x : (split x m)#o = find x m. +Proof. + functional induction (split x m); intros; cleansplit; auto. +Qed. + +Lemma split_lt_l m x : Bst m -> x >> (split x m)#l. +Proof. + intro. apply above. intro. rewrite split_in_l; intuition; order. +Qed. + +Lemma split_lt_r m x y : y >> m -> y >> (split x m)#r. +Proof. + intro. apply above. intros z Hz. apply split_in_r0 in Hz. order. +Qed. + +Lemma split_gt_r m x : Bst m -> x << (split x m)#r. +Proof. + intro. apply below. intro. rewrite split_in_r; intuition; order. +Qed. + +Lemma split_gt_l m x y : y << m -> y << (split x m)#l. +Proof. + intro. apply below. intros z Hz. apply split_in_l0 in Hz. order. +Qed. +Hint Resolve split_lt_l split_lt_r split_gt_l split_gt_r. + +Lemma split_bst_l m x : Bst m -> Bst (split x m)#l. +Proof. + functional induction (split x m); intros; cleansplit; intuition; + auto using join_bst. +Qed. + +Lemma split_bst_r m x : Bst m -> Bst (split x m)#r. +Proof. + functional induction (split x m); intros; cleansplit; intuition; + auto using join_bst. +Qed. +Hint Resolve split_bst_l split_bst_r. + +Lemma split_find m x y : Bst m -> + find y m = match X.compare y x with + | Eq => (split x m)#o + | Lt => find y (split x m)#l + | Gt => find y (split x m)#r + end. +Proof. + functional induction (split x m); intros; cleansplit. + - now case X.compare. + - repeat case X.compare_spec; trivial; order. + - simpl in *. rewrite join_find, IHt; auto. + simpl. repeat case X.compare_spec; trivial; order. + - rewrite join_find, IHt; auto. + simpl; repeat case X.compare_spec; trivial; order. +Qed. + +(** * Concatenation *) + +Lemma concat_in m1 m2 y : + y ∈ (concat m1 m2) <-> y ∈ m1 \/ y ∈ m2. +Proof. + functional induction (concat m1 m2); intros; try factornode m1. + - intuition_in. + - intuition_in. + - factor_remove_min m2 R. + rewrite join_in, (remove_min_in R); simpl; intuition. +Qed. + +Lemma concat_bst m1 m2 : Bst m1 -> Bst m2 -> m1 <<< m2 -> + Bst (concat m1 m2). +Proof. + functional induction (concat m1 m2); intros B1 B2 LT; auto; + try factornode m1. + factor_remove_min m2 R. + apply join_bst, create_bst; auto. + - now apply (remove_min_bst R). + - apply above. intros y Hy. apply LT; trivial. + rewrite (remove_min_in R); now left. + - now apply (remove_min_gt R). +Qed. +Hint Resolve concat_bst. + +Definition oelse {A} (o1 o2:option A) := + match o1 with + | Some x => Some x + | None => o2 + end. + +Lemma concat_find m1 m2 y : Bst m1 -> Bst m2 -> m1 <<< m2 -> + find y (concat m1 m2) = oelse (find y m2) (find y m1). +Proof. + functional induction (concat m1 m2); intros B1 B2 B; auto; try factornode m1. + - destruct (find y m2); auto. + - factor_remove_min m2 R. + assert (xd#1 >> m1). + { apply above. intros z Hz. apply B; trivial. + rewrite (remove_min_in R). now left. } + rewrite join_find; simpl; auto. + + rewrite (remove_min_find R B2 y). + case X.compare_spec; intros; auto. + destruct (find y m2'); trivial. + simpl. symmetry. apply not_find_iff; eauto. + + apply create_bst; auto. + * now apply (remove_min_bst R). + * now apply (remove_min_gt R). +Qed. + + +(** * Elements *) + +Notation eqk := (PX.eqk (elt:= elt)). +Notation eqke := (PX.eqke (elt:= elt)). +Notation ltk := (PX.ltk (elt:= elt)). + +Lemma bindings_aux_mapsto : forall (s:t elt) acc x e, + InA eqke (x,e) (bindings_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc. +Proof. + induction s as [ | l Hl x e r Hr h ]; simpl; auto. + intuition. + inversion H0. + intros. + rewrite Hl. + destruct (Hr acc x0 e0); clear Hl Hr. + intuition; inversion_clear H3; intuition. + compute in H0. destruct H0; simpl in *; subst; intuition. +Qed. + +Lemma bindings_mapsto : forall (s:t elt) x e, + InA eqke (x,e) (bindings s) <-> MapsTo x e s. +Proof. + intros; generalize (bindings_aux_mapsto s nil x e); intuition. + inversion_clear H0. +Qed. + +Lemma bindings_in : forall (s:t elt) x, L.PX.In x (bindings s) <-> x ∈ s. +Proof. + intros. + unfold L.PX.In. + rewrite <- In_alt; unfold In0. + split; intros (y,H); exists y. + - now rewrite <- bindings_mapsto. + - unfold L.PX.MapsTo; now rewrite bindings_mapsto. +Qed. + +Lemma bindings_aux_sort : forall (s:t elt) acc, + Bst s -> sort ltk acc -> + (forall x e y, InA eqke (x,e) acc -> y ∈ s -> y < x) -> + sort ltk (bindings_aux acc s). +Proof. + induction s as [ | l Hl y e r Hr h]; simpl; intuition. + inv Bst. + apply Hl; auto. + - constructor. + + apply Hr; eauto. + + clear Hl Hr. + apply InA_InfA with (eqA:=eqke); auto with *. + intros (y',e') Hy'. + apply bindings_aux_mapsto in Hy'. compute. intuition; eauto. + - clear Hl Hr. intros x e' y' Hx Hy'. + inversion_clear Hx. + + compute in H. destruct H; simpl in *. order. + + apply bindings_aux_mapsto in H. intuition eauto. +Qed. + +Lemma bindings_sort : forall s : t elt, Bst s -> sort ltk (bindings s). +Proof. + intros; unfold bindings; apply bindings_aux_sort; auto. + intros; inversion H0. +Qed. +Hint Resolve bindings_sort. + +Lemma bindings_nodup : forall s : t elt, Bst s -> NoDupA eqk (bindings s). +Proof. + intros; apply PX.Sort_NoDupA; auto. +Qed. + +Lemma bindings_aux_cardinal m acc : + (length acc + cardinal m)%nat = length (bindings_aux acc m). +Proof. + revert acc. induction m; simpl; intuition. + rewrite <- IHm1; simpl. + rewrite <- IHm2. rewrite Nat.add_succ_r, <- Nat.add_assoc. + f_equal. f_equal. apply Nat.add_comm. +Qed. + +Lemma bindings_cardinal m : cardinal m = length (bindings m). +Proof. + exact (bindings_aux_cardinal m nil). +Qed. + +Lemma bindings_app : + forall (s:t elt) acc, bindings_aux acc s = bindings s ++ acc. +Proof. + induction s; simpl; intros; auto. + rewrite IHs1, IHs2. + unfold bindings; simpl. + rewrite 2 IHs1, IHs2, !app_nil_r, !app_ass; auto. +Qed. + +Lemma bindings_node : + forall (t1 t2:t elt) x e z l, + bindings t1 ++ (x,e) :: bindings t2 ++ l = + bindings (Node t1 x e t2 z) ++ l. +Proof. + unfold bindings; simpl; intros. + rewrite !bindings_app, !app_nil_r, !app_ass; auto. +Qed. + +(** * Fold *) + +Definition fold' {A} (f : key -> elt -> A -> A)(s : t elt) := + L.fold f (bindings s). + +Lemma fold_equiv_aux {A} (s : t elt) (f : key -> elt -> A -> A) (a : A) acc : + L.fold f (bindings_aux acc s) a = L.fold f acc (fold f s a). +Proof. + revert a acc. + induction s; simpl; trivial. + intros. rewrite IHs1. simpl. apply IHs2. +Qed. + +Lemma fold_equiv {A} (s : t elt) (f : key -> elt -> A -> A) (a : A) : + fold f s a = fold' f s a. +Proof. + unfold fold', bindings. now rewrite fold_equiv_aux. +Qed. + +Lemma fold_spec (s:t elt)(Hs:Bst s){A}(i:A)(f : key -> elt -> A -> A) : + fold f s i = fold_left (fun a p => f p#1 p#2 a) (bindings s) i. +Proof. + rewrite fold_equiv. unfold fold'. now rewrite L.fold_spec. +Qed. + +(** * Comparison *) + +(** [flatten_e e] returns the list of bindings of the enumeration [e] + i.e. the list of bindings actually compared *) + +Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with + | End _ => nil + | More x e t r => (x,e) :: bindings t ++ flatten_e r + end. + +Lemma flatten_e_bindings : + forall (l:t elt) r x d z e, + bindings l ++ flatten_e (More x d r e) = + bindings (Node l x d r z) ++ flatten_e e. +Proof. + intros; apply bindings_node. +Qed. + +Lemma cons_1 : forall (s:t elt) e, + flatten_e (cons s e) = bindings s ++ flatten_e e. +Proof. + induction s; auto; intros. + simpl flatten_e; rewrite IHs1; apply flatten_e_bindings; auto. +Qed. + +(** Proof of correction for the comparison *) + +Variable cmp : elt->elt->bool. + +Definition IfEq b l1 l2 := L.equal cmp l1 l2 = b. + +Lemma cons_IfEq : forall b x1 x2 d1 d2 l1 l2, + X.eq x1 x2 -> cmp d1 d2 = true -> + IfEq b l1 l2 -> + IfEq b ((x1,d1)::l1) ((x2,d2)::l2). +Proof. + unfold IfEq; destruct b; simpl; intros; case X.compare_spec; simpl; + try rewrite H0; auto; order. +Qed. + +Lemma equal_end_IfEq : forall e2, + IfEq (equal_end e2) nil (flatten_e e2). +Proof. + destruct e2; red; auto. +Qed. + +Lemma equal_more_IfEq : + forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l, + IfEq (cont (cons r2 e2)) l (bindings r2 ++ flatten_e e2) -> + IfEq (equal_more cmp x1 d1 cont (More x2 d2 r2 e2)) ((x1,d1)::l) + (flatten_e (More x2 d2 r2 e2)). +Proof. + unfold IfEq; simpl; intros; destruct X.compare; simpl; auto. + rewrite <-andb_lazy_alt; f_equal; auto. +Qed. + +Lemma equal_cont_IfEq : forall m1 cont e2 l, + (forall e, IfEq (cont e) l (flatten_e e)) -> + IfEq (equal_cont cmp m1 cont e2) (bindings m1 ++ l) (flatten_e e2). +Proof. + induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto. + rewrite <- bindings_node; simpl. + apply Hl1; auto. + clear e2; intros [|x2 d2 r2 e2]. + simpl; red; auto. + apply equal_more_IfEq. + rewrite <- cons_1; auto. +Qed. + +Lemma equal_IfEq : forall (m1 m2:t elt), + IfEq (equal cmp m1 m2) (bindings m1) (bindings m2). +Proof. + intros; unfold equal. + rewrite <- (app_nil_r (bindings m1)). + replace (bindings m2) with (flatten_e (cons m2 (End _))) + by (rewrite cons_1; simpl; rewrite app_nil_r; auto). + apply equal_cont_IfEq. + intros. + apply equal_end_IfEq; auto. +Qed. + +Definition Equivb m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). + +Lemma Equivb_bindings : forall s s', + Equivb s s' <-> L.Equivb cmp (bindings s) (bindings s'). +Proof. +unfold Equivb, L.Equivb; split; split; intros. +do 2 rewrite bindings_in; firstorder. +destruct H. +apply (H2 k); rewrite <- bindings_mapsto; auto. +do 2 rewrite <- bindings_in; firstorder. +destruct H. +apply (H2 k); unfold L.PX.MapsTo; rewrite bindings_mapsto; auto. +Qed. + +Lemma equal_Equivb : forall (s s': t elt), Bst s -> Bst s' -> + (equal cmp s s' = true <-> Equivb s s'). +Proof. + intros s s' B B'. + rewrite Equivb_bindings, <- equal_IfEq. + split; [apply L.equal_2|apply L.equal_1]; auto. +Qed. + +End Elt. + +Section Map. +Variable elt elt' : Type. +Variable f : elt -> elt'. + +Lemma map_spec m x : + find x (map f m) = option_map f (find x m). +Proof. +induction m; simpl; trivial. case X.compare_spec; auto. +Qed. + +Lemma map_in m x : x ∈ (map f m) <-> x ∈ m. +Proof. +induction m; simpl; intuition_in. +Qed. + +Lemma map_bst m : Bst m -> Bst (map f m). +Proof. +induction m; simpl; auto. intros; inv Bst; constructor; auto. +- apply above. intro. rewrite map_in. intros. order. +- apply below. intro. rewrite map_in. intros. order. +Qed. + +End Map. +Section Mapi. +Variable elt elt' : Type. +Variable f : key -> elt -> elt'. + +Lemma mapi_spec m x : + exists y:key, + X.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). +Proof. + induction m; simpl. + - now exists x. + - case X.compare_spec; simpl; auto. intros. now exists k. +Qed. + +Lemma mapi_in m x : x ∈ (mapi f m) <-> x ∈ m. +Proof. +induction m; simpl; intuition_in. +Qed. + +Lemma mapi_bst m : Bst m -> Bst (mapi f m). +Proof. +induction m; simpl; auto. intros; inv Bst; constructor; auto. +- apply above. intro. rewrite mapi_in. intros. order. +- apply below. intro. rewrite mapi_in. intros. order. +Qed. + +End Mapi. + +Section Mapo. +Variable elt elt' : Type. +Variable f : key -> elt -> option elt'. + +Lemma mapo_in m x : + x ∈ (mapo f m) -> + exists y d, X.eq y x /\ MapsTo x d m /\ f y d <> None. +Proof. +functional induction (mapo f m); simpl; auto; intro H. +- inv In. +- rewrite join_in in H; destruct H as [H|[H|H]]. + + exists x0, d. do 2 (split; auto). congruence. + + destruct (IHt H) as (y & e & ? & ? & ?). exists y, e. auto. + + destruct (IHt0 H) as (y & e & ? & ? & ?). exists y, e. auto. +- rewrite concat_in in H; destruct H as [H|H]. + + destruct (IHt H) as (y & e & ? & ? & ?). exists y, e. auto. + + destruct (IHt0 H) as (y & e & ? & ? & ?). exists y, e. auto. +Qed. + +Lemma mapo_lt m x : x >> m -> x >> mapo f m. +Proof. + intros H. apply above. intros y Hy. + destruct (mapo_in Hy) as (y' & e & ? & ? & ?). order. +Qed. + +Lemma mapo_gt m x : x << m -> x << mapo f m. +Proof. + intros H. apply below. intros y Hy. + destruct (mapo_in Hy) as (y' & e & ? & ? & ?). order. +Qed. +Hint Resolve mapo_lt mapo_gt. + +Lemma mapo_bst m : Bst m -> Bst (mapo f m). +Proof. +functional induction (mapo f m); simpl; auto; intro H; inv Bst. +- apply join_bst, create_bst; auto. +- apply concat_bst; auto. apply between with x; auto. +Qed. +Hint Resolve mapo_bst. + +Ltac nonify e := + replace e with (@None elt) by + (symmetry; rewrite not_find_iff; auto; intro; order). + +Definition obind {A B} (o:option A) (f:A->option B) := + match o with Some a => f a | None => None end. + +Lemma mapo_find m x : + Bst m -> + exists y, X.eq y x /\ + find x (mapo f m) = obind (find x m) (f y). +Proof. +functional induction (mapo f m); simpl; auto; intros B; + inv Bst. +- now exists x. +- rewrite join_find; auto. + + simpl. case X.compare_spec; simpl; intros. + * now exists x0. + * destruct IHt as (y' & ? & ?); auto. + exists y'; split; trivial. + * destruct IHt0 as (y' & ? & ?); auto. + exists y'; split; trivial. + + constructor; auto using mapo_lt, mapo_gt. +- rewrite concat_find; auto. + + destruct IHt0 as (y' & ? & ->); auto. + destruct IHt as (y'' & ? & ->); auto. + case X.compare_spec; simpl; intros. + * nonify (find x r). nonify (find x l). simpl. now exists x0. + * nonify (find x r). now exists y''. + * nonify (find x l). exists y'. split; trivial. + destruct (find x r); simpl; trivial. + now destruct (f y' e). + + apply between with x0; auto. +Qed. + +End Mapo. + +Section Gmerge. +Variable elt elt' elt'' : Type. +Variable f0 : key -> option elt -> option elt' -> option elt''. +Variable f : key -> elt -> option elt' -> option elt''. +Variable mapl : t elt -> t elt''. +Variable mapr : t elt' -> t elt''. +Hypothesis f0_f : forall x d o, f x d o = f0 x (Some d) o. +Hypothesis mapl_bst : forall m, Bst m -> Bst (mapl m). +Hypothesis mapr_bst : forall m', Bst m' -> Bst (mapr m'). +Hypothesis mapl_f0 : forall x m, Bst m -> + exists y, X.eq y x /\ + find x (mapl m) = obind (find x m) (fun d => f0 y (Some d) None). +Hypothesis mapr_f0 : forall x m, Bst m -> + exists y, X.eq y x /\ + find x (mapr m) = obind (find x m) (fun d => f0 y None (Some d)). + +Notation gmerge := (gmerge f mapl mapr). + +Lemma gmerge_in m m' y : Bst m -> Bst m' -> + y ∈ (gmerge m m') -> y ∈ m \/ y ∈ m'. +Proof. + functional induction (gmerge m m'); intros B1 B2 H; + try factornode m2; inv Bst. + - right. apply find_in. + generalize (in_find (mapr_bst B2) H). + destruct (@mapr_f0 y m2) as (y' & ? & ->); trivial. + intros A B. rewrite B in A. now elim A. + - left. apply find_in. + generalize (in_find (mapl_bst B1) H). + destruct (@mapl_f0 y m2) as (y' & ? & ->); trivial. + intros A B. rewrite B in A. now elim A. + - rewrite join_in in *. revert IHt1 IHt0 H. cleansplit. + generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite split_in_r, split_in_l; intuition_in. + - rewrite concat_in in *. revert IHt1 IHt0 H; cleansplit. + generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite split_in_r, split_in_l; intuition_in. +Qed. + +Lemma gmerge_lt m m' x : Bst m -> Bst m' -> + x >> m -> x >> m' -> x >> gmerge m m'. +Proof. + intros. apply above. intros y Hy. + apply gmerge_in in Hy; intuition_in; order. +Qed. + +Lemma gmerge_gt m m' x : Bst m -> Bst m' -> + x << m -> x << m' -> x << gmerge m m'. +Proof. + intros. apply below. intros y Hy. + apply gmerge_in in Hy; intuition_in; order. +Qed. +Hint Resolve gmerge_lt gmerge_gt. +Hint Resolve split_bst_l split_bst_r split_lt_l split_gt_r. + +Lemma gmerge_bst m m' : Bst m -> Bst m' -> Bst (gmerge m m'). +Proof. + functional induction (gmerge m m'); intros B1 B2; auto; + factornode m2; inv Bst; + (apply join_bst, create_bst || apply concat_bst); + revert IHt1 IHt0; cleansplit; intuition. + apply between with x1; auto. +Qed. +Hint Resolve gmerge_bst. + +Lemma oelse_none_r {A} (o:option A) : oelse o None = o. +Proof. now destruct o. Qed. + +Ltac nonify e := + let E := fresh "E" in + assert (E : e = None); + [ rewrite not_find_iff; auto; intro U; + try apply gmerge_in in U; intuition_in; order + | rewrite E; clear E ]. + +Lemma gmerge_find m m' x : Bst m -> Bst m' -> + In x m \/ In x m' -> + exists y, X.eq y x /\ + find x (gmerge m m') = f0 y (find x m) (find x m'). +Proof. + functional induction (gmerge m m'); intros B1 B2 H; + try factornode m2; inv Bst. + - destruct H; [ intuition_in | ]. + destruct (@mapr_f0 x m2) as (y,(Hy,E)); trivial. + exists y; split; trivial. + rewrite E. simpl. apply in_find in H; trivial. + destruct (find x m2); simpl; intuition. + - destruct H; [ | intuition_in ]. + destruct (@mapl_f0 x m2) as (y,(Hy,E)); trivial. + exists y; split; trivial. + rewrite E. simpl. apply in_find in H; trivial. + destruct (find x m2); simpl; intuition. + - generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite (split_find x1 x B2). + rewrite e1 in *; simpl in *. intros. + rewrite join_find by (cleansplit; constructor; auto). + simpl. case X.compare_spec; intros. + + exists x1. split; auto. now rewrite <- e3, f0_f. + + apply IHt1; auto. clear IHt1 IHt0. + cleansplit; rewrite split_in_l; trivial. + intuition_in; order. + + apply IHt0; auto. clear IHt1 IHt0. + cleansplit; rewrite split_in_r; trivial. + intuition_in; order. + - generalize (split_bst_l x1 B2) (split_bst_r x1 B2). + rewrite (split_find x1 x B2). + pose proof (split_lt_l x1 B2). + pose proof (split_gt_r x1 B2). + rewrite e1 in *; simpl in *. intros. + rewrite concat_find by (try apply between with x1; auto). + case X.compare_spec; intros. + + clear IHt0 IHt1. + exists x1. split; auto. rewrite <- f0_f, e2. + nonify (find x (gmerge r1 r2')). + nonify (find x (gmerge l1 l2')). trivial. + + nonify (find x (gmerge r1 r2')). + simpl. apply IHt1; auto. clear IHt1 IHt0. + intuition_in; try order. + right. cleansplit. now apply split_in_l. + + nonify (find x (gmerge l1 l2')). simpl. + rewrite oelse_none_r. + apply IHt0; auto. clear IHt1 IHt0. + intuition_in; try order. + right. cleansplit. now apply split_in_r. +Qed. + +End Gmerge. + +Section Merge. +Variable elt elt' elt'' : Type. +Variable f : key -> option elt -> option elt' -> option elt''. + +Lemma merge_bst m m' : Bst m -> Bst m' -> Bst (merge f m m'). +Proof. +unfold merge; intros. +apply gmerge_bst with f; + auto using mapo_bst, mapo_find. +Qed. + +Lemma merge_spec1 m m' x : Bst m -> Bst m' -> + In x m \/ In x m' -> + exists y, X.eq y x /\ + find x (merge f m m') = f y (find x m) (find x m'). +Proof. + unfold merge; intros. + edestruct (gmerge_find (f0:=f)) as (y,(Hy,E)); + eauto using mapo_bst. + - reflexivity. + - intros. now apply mapo_find. + - intros. now apply mapo_find. +Qed. + +Lemma merge_spec2 m m' x : Bst m -> Bst m' -> + In x (merge f m m') -> In x m \/ In x m'. +Proof. +unfold merge; intros. +eapply gmerge_in with (f0:=f); try eassumption; + auto using mapo_bst, mapo_find. +Qed. + +End Merge. +End Proofs. +End Raw. + +(** * Encapsulation + + Now, in order to really provide a functor implementing [S], we + need to encapsulate everything into a type of balanced binary search trees. *) + +Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. + + Module E := X. + Module Raw := Raw I X. + Import Raw.Proofs. + + Record tree (elt:Type) := + Mk {this :> Raw.tree elt; is_bst : Raw.Bst this}. + + Definition t := tree. + Definition key := E.t. + + Section Elt. + Variable elt elt' elt'': Type. + + Implicit Types m : t elt. + Implicit Types x y : key. + Implicit Types e : elt. + + Definition empty : t elt := Mk (empty_bst elt). + Definition is_empty m : bool := Raw.is_empty m.(this). + Definition add x e m : t elt := Mk (add_bst x e m.(is_bst)). + Definition remove x m : t elt := Mk (remove_bst x m.(is_bst)). + Definition mem x m : bool := Raw.mem x m.(this). + Definition find x m : option elt := Raw.find x m.(this). + Definition map f m : t elt' := Mk (map_bst f m.(is_bst)). + Definition mapi (f:key->elt->elt') m : t elt' := + Mk (mapi_bst f m.(is_bst)). + Definition merge f m (m':t elt') : t elt'' := + Mk (merge_bst f m.(is_bst) m'.(is_bst)). + Definition bindings m : list (key*elt) := Raw.bindings m.(this). + Definition cardinal m := Raw.cardinal m.(this). + Definition fold {A} (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i. + Definition equal cmp m m' : bool := Raw.equal cmp m.(this) m'.(this). + + Definition MapsTo x e m : Prop := Raw.MapsTo x e m.(this). + Definition In x m : Prop := Raw.In0 x m.(this). + + Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt. + Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt. + Definition lt_key : (key*elt) -> (key*elt) -> Prop := @PX.ltk elt. + + Instance MapsTo_compat : + Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + Proof. + intros k k' Hk e e' He m m' Hm. unfold MapsTo; simpl. + now rewrite Hk, He, Hm. + Qed. + + Lemma find_spec m x e : find x m = Some e <-> MapsTo x e m. + Proof. apply find_spec. apply is_bst. Qed. + + Lemma mem_spec m x : mem x m = true <-> In x m. + Proof. + unfold In, mem; rewrite In_alt. apply mem_spec. apply is_bst. + Qed. + + Lemma empty_spec x : find x empty = None. + Proof. apply empty_spec. Qed. + + Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None. + Proof. apply is_empty_spec. Qed. + + Lemma add_spec1 m x e : find x (add x e m) = Some e. + Proof. apply add_spec1. apply is_bst. Qed. + Lemma add_spec2 m x y e : ~ E.eq x y -> find y (add x e m) = find y m. + Proof. apply add_spec2. apply is_bst. Qed. + + Lemma remove_spec1 m x : find x (remove x m) = None. + Proof. apply remove_spec1. apply is_bst. Qed. + Lemma remove_spec2 m x y : ~E.eq x y -> find y (remove x m) = find y m. + Proof. apply remove_spec2. apply is_bst. Qed. + + Lemma bindings_spec1 m x e : + InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. + Proof. apply bindings_mapsto. Qed. + + Lemma bindings_spec2 m : sort lt_key (bindings m). + Proof. apply bindings_sort. apply is_bst. Qed. + + Lemma bindings_spec2w m : NoDupA eq_key (bindings m). + Proof. apply bindings_nodup. apply is_bst. Qed. + + Lemma fold_spec m {A} (i : A) (f : key -> elt -> A -> A) : + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. + Proof. apply fold_spec. apply is_bst. Qed. + + Lemma cardinal_spec m : cardinal m = length (bindings m). + Proof. apply bindings_cardinal. Qed. + + Definition Equal m m' := forall y, find y m = find y m'. + Definition Equiv (eq_elt:elt->elt->Prop) m m' := + (forall k, In k m <-> In k m') /\ + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'). + Definition Equivb cmp := Equiv (Cmp cmp). + + Lemma Equivb_Equivb cmp m m' : + Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'. + Proof. + unfold Equivb, Equiv, Raw.Proofs.Equivb, In. intuition. + generalize (H0 k); do 2 rewrite In_alt; intuition. + generalize (H0 k); do 2 rewrite In_alt; intuition. + generalize (H0 k); do 2 rewrite <- In_alt; intuition. + generalize (H0 k); do 2 rewrite <- In_alt; intuition. + Qed. + + Lemma equal_spec m m' cmp : + equal cmp m m' = true <-> Equivb cmp m m'. + Proof. rewrite Equivb_Equivb. apply equal_Equivb; apply is_bst. Qed. + + End Elt. + + Lemma map_spec {elt elt'} (f:elt->elt') m x : + find x (map f m) = option_map f (find x m). + Proof. apply map_spec. Qed. + + Lemma mapi_spec {elt elt'} (f:key->elt->elt') m x : + exists y:key, E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m). + Proof. apply mapi_spec. Qed. + + Lemma merge_spec1 {elt elt' elt''} + (f:key->option elt->option elt'->option elt'') m m' x : + In x m \/ In x m' -> + exists y:key, E.eq y x /\ + find x (merge f m m') = f y (find x m) (find x m'). + Proof. + unfold In. rewrite !In_alt. apply merge_spec1; apply is_bst. + Qed. + + Lemma merge_spec2 {elt elt' elt''} + (f:key -> option elt->option elt'->option elt'') m m' x : + In x (merge f m m') -> In x m \/ In x m'. + Proof. + unfold In. rewrite !In_alt. apply merge_spec2; apply is_bst. + Qed. + +End IntMake. + + +Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: + Sord with Module Data := D + with Module MapS.E := X. + + Module Data := D. + Module Import MapS := IntMake(I)(X). + Module LO := MMapList.Make_ord(X)(D). + Module R := Raw. + Module P := Raw.Proofs. + + Definition t := MapS.t D.t. + + Definition cmp e e' := + match D.compare e e' with Eq => true | _ => false end. + + (** One step of comparison of bindings *) + + Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 := + match e2 with + | R.End _ => Gt + | R.More x2 d2 r2 e2 => + match X.compare x1 x2 with + | Eq => match D.compare d1 d2 with + | Eq => cont (R.cons r2 e2) + | Lt => Lt + | Gt => Gt + end + | Lt => Lt + | Gt => Gt + end + end. + + (** Comparison of left tree, middle element, then right tree *) + + Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 := + match s1 with + | R.Leaf _ => cont e2 + | R.Node l1 x1 d1 r1 _ => + compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2 + end. + + (** Initial continuation *) + + Definition compare_end (e2:R.enumeration D.t) := + match e2 with R.End _ => Eq | _ => Lt end. + + (** The complete comparison *) + + Definition compare m1 m2 := + compare_cont m1.(this) compare_end (R.cons m2 .(this) (Raw.End _)). + + (** Correctness of this comparison *) + + Definition Cmp c := + match c with + | Eq => LO.eq_list + | Lt => LO.lt_list + | Gt => (fun l1 l2 => LO.lt_list l2 l1) + end. + + Lemma cons_Cmp c x1 x2 d1 d2 l1 l2 : + X.eq x1 x2 -> D.eq d1 d2 -> + Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). + Proof. + destruct c; simpl; intros; case X.compare_spec; auto; try P.MX.order. + intros. right. split; auto. now symmetry. + Qed. + Hint Resolve cons_Cmp. + + Lemma compare_end_Cmp e2 : + Cmp (compare_end e2) nil (P.flatten_e e2). + Proof. + destruct e2; simpl; auto. + Qed. + + Lemma compare_more_Cmp x1 d1 cont x2 d2 r2 e2 l : + Cmp (cont (R.cons r2 e2)) l (R.bindings r2 ++ P.flatten_e e2) -> + Cmp (compare_more x1 d1 cont (R.More x2 d2 r2 e2)) ((x1,d1)::l) + (P.flatten_e (R.More x2 d2 r2 e2)). + Proof. + simpl; case X.compare_spec; simpl; + try case D.compare_spec; simpl; auto; + case X.compare_spec; try P.MX.order; auto. + Qed. + + Lemma compare_cont_Cmp : forall s1 cont e2 l, + (forall e, Cmp (cont e) l (P.flatten_e e)) -> + Cmp (compare_cont s1 cont e2) (R.bindings s1 ++ l) (P.flatten_e e2). + Proof. + induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1] using P.tree_ind; + intros; auto. + rewrite <- P.bindings_node; simpl. + apply Hl1; auto. clear e2. intros [|x2 d2 r2 e2]. + simpl; auto. + apply compare_more_Cmp. + rewrite <- P.cons_1; auto. + Qed. + + Lemma compare_Cmp m1 m2 : + Cmp (compare m1 m2) (bindings m1) (bindings m2). + Proof. + destruct m1 as (s1,H1), m2 as (s2,H2). + unfold compare, bindings; simpl. + rewrite <- (app_nil_r (R.bindings s1)). + replace (R.bindings s2) with (P.flatten_e (R.cons s2 (R.End _))) by + (rewrite P.cons_1; simpl; rewrite app_nil_r; auto). + auto using compare_cont_Cmp, compare_end_Cmp. + Qed. + + Definition eq (m1 m2 : t) := LO.eq_list (bindings m1) (bindings m2). + Definition lt (m1 m2 : t) := LO.lt_list (bindings m1) (bindings m2). + + Lemma compare_spec m1 m2 : CompSpec eq lt m1 m2 (compare m1 m2). + Proof. + assert (H := compare_Cmp m1 m2). + unfold Cmp in H. + destruct (compare m1 m2); auto. + Qed. + + (* Proofs about [eq] and [lt] *) + + Definition sbindings (m1 : t) := + LO.MapS.Mk (P.bindings_sort m1.(is_bst)). + + Definition seq (m1 m2 : t) := LO.eq (sbindings m1) (sbindings m2). + Definition slt (m1 m2 : t) := LO.lt (sbindings m1) (sbindings m2). + + Lemma eq_seq : forall m1 m2, eq m1 m2 <-> seq m1 m2. + Proof. + unfold eq, seq, sbindings, bindings, LO.eq; intuition. + Qed. + + Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2. + Proof. + unfold lt, slt, sbindings, bindings, LO.lt; intuition. + Qed. + + Lemma eq_spec m m' : eq m m' <-> Equivb cmp m m'. + Proof. + rewrite eq_seq; unfold seq. + rewrite Equivb_Equivb. + rewrite P.Equivb_bindings. apply LO.eq_spec. + Qed. + + Instance eq_equiv : Equivalence eq. + Proof. + constructor; red; [intros x|intros x y| intros x y z]; + rewrite !eq_seq; apply LO.eq_equiv. + Qed. + + Instance lt_compat : Proper (eq ==> eq ==> iff) lt. + Proof. + intros m1 m2 H1 m1' m2' H2. rewrite !lt_slt. rewrite eq_seq in *. + now apply LO.lt_compat. + Qed. + + Instance lt_strorder : StrictOrder lt. + Proof. + constructor; red; [intros x; red|intros x y z]; + rewrite !lt_slt; apply LO.lt_strorder. + Qed. + +End IntMake_ord. + +(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *) + +Module Make (X: OrderedType) <: S with Module E := X + :=IntMake(Z_as_Int)(X). + +Module Make_ord (X: OrderedType)(D: OrderedType) + <: Sord with Module Data := D + with Module MapS.E := X + :=IntMake_ord(Z_as_Int)(X)(D). diff --git a/theories/MMaps/MMapPositive.v b/theories/MMaps/MMapPositive.v index 2da1fff1e..d3aab2389 100644 --- a/theories/MMaps/MMapPositive.v +++ b/theories/MMaps/MMapPositive.v @@ -8,7 +8,7 @@ (** * MMapPositive : an implementation of MMapInterface for [positive] keys. *) -Require Import Bool BinPos Orders OrdersEx OrdersLists MMapInterface. +Require Import Bool PeanoNat BinPos Orders OrdersEx OrdersLists MMapInterface. Set Implicit Arguments. Local Open Scope lazy_bool_scope. @@ -23,44 +23,16 @@ Local Unset Elimination Schemes. compression is implemented, and that the current file is simple enough to be self-contained. *) -(** First, some stuff about [positive] *) +(** Reverses the positive [y] and concatenate it with [x] *) -Fixpoint append (i j : positive) : positive := - match i with - | xH => j - | xI ii => xI (append ii j) - | xO ii => xO (append ii j) - end. - -Lemma append_assoc_0 : - forall (i j : positive), append i (xO j) = append (append i (xO xH)) j. -Proof. - induction i; intros; destruct j; simpl; - try rewrite (IHi (xI j)); - try rewrite (IHi (xO j)); - try rewrite <- (IHi xH); - auto. -Qed. - -Lemma append_assoc_1 : - forall (i j : positive), append i (xI j) = append (append i (xI xH)) j. -Proof. - induction i; intros; destruct j; simpl; - try rewrite (IHi (xI j)); - try rewrite (IHi (xO j)); - try rewrite <- (IHi xH); - auto. -Qed. - -Lemma append_neutral_r : forall (i : positive), append i xH = i. -Proof. - induction i; simpl; congruence. -Qed. - -Lemma append_neutral_l : forall (i : positive), append xH i = i. -Proof. - simpl; auto. -Qed. +Fixpoint rev_append (y x : positive) : positive := + match y with + | 1 => x + | y~1 => rev_append y x~1 + | y~0 => rev_append y x~0 + end. +Local Infix "@" := rev_append (at level 60). +Definition rev x := x@1. (** The module of maps over positive keys *) @@ -71,6 +43,17 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Definition key := positive : Type. + Definition eq_key {A} (p p':key*A) := E.eq (fst p) (fst p'). + + Definition eq_key_elt {A} (p p':key*A) := + E.eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Definition lt_key {A} (p p':key*A) := E.lt (fst p) (fst p'). + + Instance eqk_equiv {A} : Equivalence (@eq_key A) := _. + Instance eqke_equiv {A} : Equivalence (@eq_key_elt A) := _. + Instance ltk_strorder {A} : StrictOrder (@lt_key A) := _. + Inductive tree (A : Type) := | Leaf : tree A | Node : tree A -> option A -> tree A -> tree A. @@ -152,20 +135,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. (** [bindings] *) - Fixpoint xbindings (m : t A) (i : key) : list (key * A) := + Fixpoint xbindings (m : t A) (i : positive) (a: list (key*A)) := match m with - | Leaf => nil - | Node l None r => - (xbindings l (append i (xO xH))) ++ (xbindings r (append i (xI xH))) - | Node l (Some x) r => - (xbindings l (append i (xO xH))) - ++ ((i, x) :: xbindings r (append i (xI xH))) + | Leaf => a + | Node l None r => xbindings l i~0 (xbindings r i~1 a) + | Node l (Some e) r => xbindings l i~0 ((rev i,e) :: xbindings r i~1 a) end. - (* Note: function [xbindings] above is inefficient. We should apply - deforestation to it, but that makes the proofs even harder. *) - - Definition bindings (m : t A) := xbindings m xH. + Definition bindings (m : t A) := xbindings m 1 nil. (** [cardinal] *) @@ -178,6 +155,33 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. (** Specification proofs *) + Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v. + Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m. + + Lemma MapsTo_compat : Proper (E.eq==>eq==>eq==>iff) MapsTo. + Proof. + intros k k' Hk e e' He m m' Hm. red in Hk. now subst. + Qed. + + Lemma find_spec m x e : find x m = Some e <-> MapsTo x e m. + Proof. reflexivity. Qed. + + Lemma mem_find : + forall m x, mem x m = match find x m with None => false | _ => true end. + Proof. + induction m; destruct x; simpl; auto. + Qed. + + Lemma mem_spec : forall m x, mem x m = true <-> In x m. + Proof. + unfold In, MapsTo; intros m x; rewrite mem_find. + split. + - destruct (find x m). + exists a; auto. + intros; discriminate. + - destruct 1 as (e0,H0); rewrite H0; auto. + Qed. + Lemma gleaf : forall (i : key), find i Leaf = None. Proof. destruct i; simpl; auto. Qed. @@ -185,6 +189,20 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. forall (i: key), find i empty = None. Proof. exact gleaf. Qed. + Lemma is_empty_spec m : + is_empty m = true <-> forall k, find k m = None. + Proof. + induction m; simpl. + - intuition. apply empty_spec. + - destruct o. split; try discriminate. + intros H. now specialize (H xH). + rewrite <- andb_lazy_alt, andb_true_iff, IHm1, IHm2. + clear IHm1 IHm2. + split. + + intros (H1,H2) k. destruct k; simpl; auto. + + intros H; split; intros k. apply (H (xO k)). apply (H (xI k)). + Qed. + Theorem add_spec1: forall (m: t A) (i: key) (x: A), find i (add i x m) = Some x. Proof. @@ -230,354 +248,114 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. try apply IHm1; try apply IHm2; congruence. Qed. - Lemma xbindings_correct: - forall (m: t A) (i j : key) (v: A), - find i m = Some v -> List.In (append j i, v) (xbindings m j). - Proof. - induction m; intros. - - rewrite (gleaf i) in H; discriminate. - - destruct o, i; simpl in *; apply in_or_app. - + rewrite append_assoc_1. right; now apply in_cons, IHm2. - + rewrite append_assoc_0. left; now apply IHm1. - + rewrite append_neutral_r. injection H as ->. - right; apply in_eq. - + rewrite append_assoc_1. right; now apply IHm2. - + rewrite append_assoc_0. left; now apply IHm1. - + discriminate. - Qed. - - Theorem bindings_correct: - forall (m: t A) (i: key) (v: A), - find i m = Some v -> List.In (i, v) (bindings m). - Proof. - intros m i v H. - exact (xbindings_correct m i xH H). - Qed. - - Fixpoint xfind (i j : key) (m : t A) : option A := - match i, j with - | _, xH => find i m - | xO ii, xO jj => xfind ii jj m - | xI ii, xI jj => xfind ii jj m - | _, _ => None - end. - - Lemma xfind_left : - forall (j i : key) (m1 m2 : t A) (o : option A) (v : A), - xfind i (append j (xO xH)) m1 = Some v -> - xfind i j (Node m1 o m2) = Some v. - Proof. - induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. - destruct i; simpl in *; auto. - Qed. - - Lemma xbindings_ii : - forall (m: t A) (i j : key) (v: A), - List.In (xI i, v) (xbindings m (xI j)) -> - List.In (i, v) (xbindings m j). - Proof. - induction m. - - simpl; auto. - - intros; destruct o; simpl in *; rewrite in_app_iff in *; - destruct H. - + left; now apply IHm1. - + right; destruct (in_inv H). - * injection H0 as -> ->. apply in_eq. - * apply in_cons; now apply IHm2. - + left; now apply IHm1. - + right; now apply IHm2. - Qed. - - Lemma xbindings_io : - forall (m: t A) (i j : key) (v: A), - ~List.In (xI i, v) (xbindings m (xO j)). - Proof. - induction m. - - simpl; auto. - - intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). - + apply (IHm1 _ _ _ H0). - + destruct (in_inv H0). congruence. apply (IHm2 _ _ _ H1). - + apply (IHm1 _ _ _ H0). - + apply (IHm2 _ _ _ H0). - Qed. - - Lemma xbindings_oo : - forall (m: t A) (i j : key) (v: A), - List.In (xO i, v) (xbindings m (xO j)) -> - List.In (i, v) (xbindings m j). - Proof. - induction m. - - simpl; auto. - - intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); - apply in_or_app. - + left; now apply IHm1. - + right; destruct (in_inv H0). - injection H1 as -> ->; apply in_eq. - apply in_cons; now apply IHm2. - + left; now apply IHm1. - + right; now apply IHm2. - Qed. - - Lemma xbindings_oi : - forall (m: t A) (i j : key) (v: A), - ~List.In (xO i, v) (xbindings m (xI j)). - Proof. - induction m. - - simpl; auto. - - intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). - + apply (IHm1 _ _ _ H0). - + destruct (in_inv H0). congruence. apply (IHm2 _ _ _ H1). - + apply (IHm1 _ _ _ H0). - + apply (IHm2 _ _ _ H0). - Qed. - - Lemma xbindings_ih : - forall (m1 m2: t A) (o: option A) (i : key) (v: A), - List.In (xI i, v) (xbindings (Node m1 o m2) xH) -> - List.In (i, v) (xbindings m2 xH). - Proof. - destruct o; simpl; intros; destruct (in_app_or _ _ _ H). - absurd (List.In (xI i, v) (xbindings m1 2)); auto; apply xbindings_io; auto. - destruct (in_inv H0). - congruence. - apply xbindings_ii; auto. - absurd (List.In (xI i, v) (xbindings m1 2)); auto; apply xbindings_io; auto. - apply xbindings_ii; auto. - Qed. - - Lemma xbindings_oh : - forall (m1 m2: t A) (o: option A) (i : key) (v: A), - List.In (xO i, v) (xbindings (Node m1 o m2) xH) -> - List.In (i, v) (xbindings m1 xH). - Proof. - destruct o; simpl; intros; destruct (in_app_or _ _ _ H). - apply xbindings_oo; auto. - destruct (in_inv H0). - congruence. - absurd (List.In (xO i, v) (xbindings m2 3)); auto; apply xbindings_oi; auto. - apply xbindings_oo; auto. - absurd (List.In (xO i, v) (xbindings m2 3)); auto; apply xbindings_oi; auto. - Qed. - - Lemma xbindings_hi : - forall (m: t A) (i : key) (v: A), - ~List.In (xH, v) (xbindings m (xI i)). - Proof. - induction m; intros. - - simpl; auto. - - destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). - + generalize H0; apply IHm1; auto. - + destruct (in_inv H0). congruence. - generalize H1; apply IHm2; auto. - + generalize H0; apply IHm1; auto. - + generalize H0; apply IHm2; auto. - Qed. - - Lemma xbindings_ho : - forall (m: t A) (i : key) (v: A), - ~List.In (xH, v) (xbindings m (xO i)). - Proof. - induction m; intros. - - simpl; auto. - - destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). - + generalize H0; apply IHm1; auto. - + destruct (in_inv H0). congruence. - generalize H1; apply IHm2; auto. - + generalize H0; apply IHm1; auto. - + generalize H0; apply IHm2; auto. - Qed. - - Lemma find_xfind_h : - forall (m: t A) (i: key), find i m = xfind i xH m. - Proof. - destruct i; simpl; auto. - Qed. - - Lemma xbindings_complete: - forall (i j : key) (m: t A) (v: A), - List.In (i, v) (xbindings m j) -> xfind i j m = Some v. - Proof. - induction i; simpl; intros; destruct j; simpl. - apply IHi; apply xbindings_ii; auto. - absurd (List.In (xI i, v) (xbindings m (xO j))); auto; apply xbindings_io. - destruct m. - simpl in H; tauto. - rewrite find_xfind_h. apply IHi. apply (xbindings_ih _ _ _ _ _ H). - absurd (List.In (xO i, v) (xbindings m (xI j))); auto; apply xbindings_oi. - apply IHi; apply xbindings_oo; auto. - destruct m. - simpl in H; tauto. - rewrite find_xfind_h. apply IHi. apply (xbindings_oh _ _ _ _ _ H). - absurd (List.In (xH, v) (xbindings m (xI j))); auto; apply xbindings_hi. - absurd (List.In (xH, v) (xbindings m (xO j))); auto; apply xbindings_ho. - destruct m. - simpl in H; tauto. - destruct o; simpl in H; destruct (in_app_or _ _ _ H). - absurd (List.In (xH, v) (xbindings m1 (xO xH))); auto; apply xbindings_ho. - destruct (in_inv H0). - congruence. - absurd (List.In (xH, v) (xbindings m2 (xI xH))); auto; apply xbindings_hi. - absurd (List.In (xH, v) (xbindings m1 (xO xH))); auto; apply xbindings_ho. - absurd (List.In (xH, v) (xbindings m2 (xI xH))); auto; apply xbindings_hi. - Qed. - - Theorem bindings_complete: - forall (m: t A) (i: key) (v: A), - List.In (i, v) (bindings m) -> find i m = Some v. - Proof. - intros m i v H. - unfold bindings in H. - rewrite find_xfind_h. - exact (xbindings_complete i xH m v H). - Qed. - - Lemma cardinal_spec : - forall (m: t A), cardinal m = length (bindings m). - Proof. - unfold bindings. - intros m; set (p:=1); clearbody p; revert m p. - induction m; simpl; auto; intros. - rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto. - destruct o; rewrite app_length; simpl; auto. - Qed. - - Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v. - - Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m. - - Definition eq_key (p p':key*A) := E.eq (fst p) (fst p'). - - Definition eq_key_elt (p p':key*A) := - E.eq (fst p) (fst p') /\ (snd p) = (snd p'). - - Definition lt_key (p p':key*A) := E.lt (fst p) (fst p'). - - Global Instance eqk_equiv : Equivalence eq_key := _. - Global Instance eqke_equiv : Equivalence eq_key_elt := _. - Global Instance ltk_strorder : StrictOrder lt_key := _. - - Lemma mem_find : - forall m x, mem x m = match find x m with None => false | _ => true end. - Proof. - induction m; destruct x; simpl; auto. - Qed. - - Lemma mem_spec : forall m x, mem x m = true <-> In x m. - Proof. - unfold In, MapsTo; intros m x; rewrite mem_find. - split. - - destruct (find x m). - exists a; auto. - intros; discriminate. - - destruct 1 as (e0,H0); rewrite H0; auto. - Qed. - - Variable m m' m'' : t A. - Variable x y z : key. - Variable e e' : A. - - Lemma MapsTo_compat : Proper (E.eq==>eq==>eq==>iff) MapsTo. - Proof. - intros k1 k2 Hk e1 e2 He m1 m2 Hm. red in Hk. now subst. - Qed. - - Lemma find_spec : find x m = Some e <-> MapsTo x e m. - Proof. reflexivity. Qed. - - Lemma is_empty_spec : is_empty m = true <-> forall k, find k m = None. - Proof. - induction m; simpl. - - intuition. apply empty_spec. - - destruct o. split; try discriminate. - intros H. now specialize (H xH). - rewrite <- andb_lazy_alt, andb_true_iff, IHt0_1, IHt0_2. - clear IHt0_1 IHt0_2. - split. - + intros (H1,H2) k. destruct k; simpl; auto. - + intros H; split; intros k. apply (H (xO k)). apply (H (xI k)). - Qed. - - Lemma bindings_spec1 : - InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m. - Proof. - unfold MapsTo. - rewrite InA_alt. - split. - - intros ((e0,a),(H,H0)). - red in H; simpl in H; unfold E.eq in H; destruct H; subst. - apply bindings_complete; auto. - - intro H. - exists (x,e). - split. - red; simpl; unfold E.eq; auto. - apply bindings_correct; auto. - Qed. - - Lemma xbindings_bits_lt_1 : forall p p0 q m v, - List.In (p0,v) (xbindings m (append p (xO q))) -> E.bits_lt p0 p. + Local Notation InL := (InA eq_key_elt). + + Lemma xbindings_spec: forall m j acc k e, + InL (k,e) (xbindings m j acc) <-> + InL (k,e) acc \/ exists x, k=(j@x) /\ find x m = Some e. + Proof. + induction m as [|l IHl o r IHr]; simpl. + - intros. split; intro H. + + now left. + + destruct H as [H|[x [_ H]]]. assumption. + now rewrite gleaf in H. + - intros j acc k e. case o as [e'|]; + rewrite IHl, ?InA_cons, IHr; clear IHl IHr; split. + + intros [[H|[H|H]]|H]; auto. + * unfold eq_key_elt, E.eq, fst, snd in H. destruct H as (->,<-). + right. now exists 1. + * destruct H as (x,(->,H)). right. now exists x~1. + * destruct H as (x,(->,H)). right. now exists x~0. + + intros [H|H]; auto. + destruct H as (x,(->,H)). + destruct x; simpl in *. + * left. right. right. now exists x. + * right. now exists x. + * left. left. injection H as ->. reflexivity. + + intros [[H|H]|H]; auto. + * destruct H as (x,(->,H)). right. now exists x~1. + * destruct H as (x,(->,H)). right. now exists x~0. + + intros [H|H]; auto. + destruct H as (x,(->,H)). + destruct x; simpl in *. + * left. right. now exists x. + * right. now exists x. + * discriminate. + Qed. + + Lemma lt_rev_append: forall j x y, E.lt x y -> E.lt (j@x) (j@y). + Proof. induction j; intros; simpl; auto. Qed. + + Lemma xbindings_sort m j acc : + sort lt_key acc -> + (forall x p, In x m -> InL p acc -> E.lt (j@x) (fst p)) -> + sort lt_key (xbindings m j acc). + Proof. + revert j acc. + induction m as [|l IHl o r IHr]; simpl; trivial. + intros j acc Hacc Hsacc. destruct o as [e|]. + - apply IHl;[constructor;[apply IHr; [apply Hacc|]|]|]. + + intros. now apply Hsacc. + + case_eq (xbindings r j~1 acc); [constructor|]. + intros (z,e') q H. constructor. + assert (H': InL (z,e') (xbindings r j~1 acc)). + { rewrite H. now constructor. } + clear H q. rewrite xbindings_spec in H'. + destruct H' as [H'|H']. + * apply (Hsacc 1 (z,e')); trivial. now exists e. + * destruct H' as (x,(->,H)). + red. simpl. now apply lt_rev_append. + + intros x (y,e') Hx Hy. inversion_clear Hy. + rewrite H. simpl. now apply lt_rev_append. + rewrite xbindings_spec in H. + destruct H as [H|H]. + * now apply Hsacc. + * destruct H as (z,(->,H)). simpl. + now apply lt_rev_append. + - apply IHl; [apply IHr; [apply Hacc|]|]. + + intros. now apply Hsacc. + + intros x (y,e') Hx H. rewrite xbindings_spec in H. + destruct H as [H|H]. + * now apply Hsacc. + * destruct H as (z,(->,H)). simpl. + now apply lt_rev_append. + Qed. + + Lemma bindings_spec1 m k e : + InA eq_key_elt (k,e) (bindings m) <-> MapsTo k e m. + Proof. + unfold bindings, MapsTo. rewrite xbindings_spec. + split; [ intros [H|(y & H & H')] | intros IN ]. + - inversion H. + - simpl in *. now subst. + - right. now exists k. + Qed. + + Lemma bindings_spec2 m : sort lt_key (bindings m). + Proof. + unfold bindings. + apply xbindings_sort. constructor. inversion 2. + Qed. + + Lemma bindings_spec2w m : NoDupA eq_key (bindings m). Proof. - intros. - generalize (xbindings_complete _ _ _ _ H); clear H; intros. - revert p0 q m v H. - induction p; destruct p0; simpl; intros; eauto; try discriminate. + apply ME.Sort_NoDupA. + apply bindings_spec2. Qed. - Lemma xbindings_bits_lt_2 : forall p p0 q m v, - List.In (p0,v) (xbindings m (append p (xI q))) -> E.bits_lt p p0. + Lemma xbindings_length m j acc : + length (xbindings m j acc) = (cardinal m + length acc)%nat. Proof. - intros. - generalize (xbindings_complete _ _ _ _ H); clear H; intros. - revert p0 q m v H. - induction p; destruct p0; simpl; intros; eauto; try discriminate. + revert j acc. + induction m; simpl; trivial; intros. + destruct o; simpl; rewrite IHm1; simpl; rewrite IHm2; + now rewrite ?Nat.add_succ_r, Nat.add_assoc. Qed. - Lemma xbindings_sort : forall p, sort lt_key (xbindings m p). + Lemma cardinal_spec m : cardinal m = length (bindings m). Proof. - induction m. - simpl; auto. - destruct o; simpl; intros. - (* Some *) - apply (SortA_app (eqA:=eq_key_elt)); auto with *. - constructor; auto. - apply In_InfA; intros. - destruct y0. - red; red; simpl. - eapply xbindings_bits_lt_2; eauto. - intros x0 y0. - do 2 rewrite InA_alt. - intros (y1,(Hy1,H)) (y2,(Hy2,H0)). - destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst. - destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. - red; red; simpl. - destruct H0. - injection H0; clear H0; intros _ H0; subst. - eapply xbindings_bits_lt_1; eauto. - apply E.bits_lt_trans with p. - eapply xbindings_bits_lt_1; eauto. - eapply xbindings_bits_lt_2; eauto. - (* None *) - apply (SortA_app (eqA:=eq_key_elt)); auto with *. - intros x0 y0. - do 2 rewrite InA_alt. - intros (y1,(Hy1,H)) (y2,(Hy2,H0)). - destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst. - destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. - red; red; simpl. - apply E.bits_lt_trans with p. - eapply xbindings_bits_lt_1; eauto. - eapply xbindings_bits_lt_2; eauto. - Qed. - - Lemma bindings_spec2 : sort lt_key (bindings m). - Proof. - unfold bindings. - apply xbindings_sort; auto. - Qed. - - Lemma bindings_spec2w : NoDupA eq_key (bindings m). - Proof. - apply ME.Sort_NoDupA. - apply bindings_spec2. + unfold bindings. rewrite xbindings_length. simpl. + symmetry. apply Nat.add_0_r. Qed. (** [map] and [mapi] *) @@ -591,40 +369,33 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Fixpoint xmapi (m : t A) (i : key) : t B := match m with | Leaf => Leaf - | Node l o r => Node (xmapi l (append i (xO xH))) - (f i o) - (xmapi r (append i (xI xH))) + | Node l o r => Node (xmapi l (i~0)) + (f (rev i) o) + (xmapi r (i~1)) end. End Mapi. Definition mapi (f : key -> A -> B) m := - xmapi (fun k => option_map (f k)) m xH. + xmapi (fun k => option_map (f k)) m 1. Definition map (f : A -> B) m := mapi (fun _ => f) m. End A. Lemma xgmapi: - forall (A B: Type) (f: key -> option A -> option B) (i j : key) (m: t A), - (forall k, f k None = None) -> - find i (xmapi f m j) = f (append j i) (find i m). + forall (A B: Type) (f: key -> option A -> option B) (i j : key) (m: t A), + (forall k, f k None = None) -> + find i (xmapi f m j) = f (j@i) (find i m). Proof. - induction i; intros; destruct m; simpl; auto. - rewrite (append_assoc_1 j i); apply IHi; auto. - rewrite (append_assoc_0 j i); apply IHi; auto. - rewrite append_neutral_r; auto. + induction i; intros; destruct m; simpl; rewrite ?IHi; auto. Qed. Theorem mapi_spec0 : forall (A B: Type) (f: key -> A -> B) (i: key) (m: t A), find i (mapi f m) = option_map (f i) (find i m). Proof. - intros. - unfold mapi. - replace (f i) with (f (append xH i)). - apply xgmapi; auto. - rewrite append_neutral_l; auto. + intros. unfold mapi. rewrite xgmapi; simpl; auto. Qed. Lemma mapi_spec : @@ -654,20 +425,18 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. match m2 with | Leaf => xmapi (fun k o => f k o None) m1 i | Node l2 o2 r2 => - Node (xmerge l1 l2 (append i (xO xH))) - (f i o1 o2) - (xmerge r1 r2 (append i (xI xH))) + Node (xmerge l1 l2 (i~0)) + (f (rev i) o1 o2) + (xmerge r1 r2 (i~1)) end end. Lemma xgmerge: forall (i j: key)(m1:t A)(m2: t B), (forall i, f i None None = None) -> - find i (xmerge m1 m2 j) = f (append j i) (find i m1) (find i m2). + find i (xmerge m1 m2 j) = f (j@i) (find i m1) (find i m2). Proof. induction i; intros; destruct m1; destruct m2; simpl; auto; - rewrite ?xgmapi, ?IHi, - <- ?append_assoc_1, <- ?append_assoc_0, - ?append_neutral_l, ?append_neutral_r; auto. + rewrite ?xgmapi, ?IHi; simpl; auto. Qed. End merge. @@ -688,8 +457,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Proof. intros. exists x. split. reflexivity. unfold merge. - rewrite xgmerge; auto. - rewrite append_neutral_l. + rewrite xgmerge; simpl; auto. rewrite <- 2 mem_spec, 2 mem_find in H. destruct (find x m); simpl; auto. destruct (find x m'); simpl; auto. intuition discriminate. @@ -701,8 +469,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. intros. rewrite <-mem_spec, mem_find in H. unfold merge in H. - rewrite xgmerge in H; auto. - rewrite append_neutral_l in H. + rewrite xgmerge in H; simpl; auto. rewrite <- 2 mem_spec, 2 mem_find. destruct (find x m); simpl in *; auto. destruct (find x m'); simpl in *; auto. @@ -713,42 +480,36 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Variables A B : Type. Variable f : key -> A -> B -> B. - Fixpoint xfoldi (m : t A) (v : B) (i : key) := + (** the additional argument, [i], records the current path, in + reverse order (this should be more efficient: we reverse this argument + only at present nodes only, rather than at each node of the tree). + we also use this convention in all functions below + *) + + Fixpoint xfold (m : t A) (v : B) (i : key) := match m with | Leaf => v | Node l (Some x) r => - xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3) + xfold r (f (rev i) x (xfold l v i~0)) i~1 | Node l None r => - xfoldi r (xfoldi l v (append i 2)) (append i 3) + xfold r (xfold l v i~0) i~1 end. - - Lemma xfoldi_1 : - forall m v i, - xfoldi m v i = fold_left (fun a p => f (fst p) (snd p) a) (xbindings m i) v. - Proof. - set (F := fun a p => f (fst p) (snd p) a). - induction m; intros; simpl; auto. - destruct o. - rewrite fold_left_app; simpl. - rewrite <- IHm1. - rewrite <- IHm2. - unfold F; simpl; reflexivity. - rewrite fold_left_app; simpl. - rewrite <- IHm1. - rewrite <- IHm2. - reflexivity. - Qed. - - Definition fold m i := xfoldi m i 1. + Definition fold m i := xfold m i 1. End Fold. Lemma fold_spec : - forall (A:Type)(m:t A)(B:Type)(i : B) (f : key -> A -> B -> B), + forall {A}(m:t A){B}(i : B) (f : key -> A -> B -> B), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i. Proof. - intros; unfold fold, bindings. - rewrite xfoldi_1; reflexivity. + unfold fold, bindings. intros A m B i f. revert m i. + set (f' := fun a p => f (fst p) (snd p) a). + assert (H: forall m i j acc, + fold_left f' acc (xfold f m i j) = + fold_left f' (xbindings m j acc) i). + { induction m as [|l IHl o r IHr]; intros; trivial. + destruct o; simpl; now rewrite IHr, <- IHl. } + intros. exact (H m i 1 nil). Qed. Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool := @@ -872,11 +633,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. try discriminate. Qed. -Lemma equal_spec : forall (A:Type)(m m':t A)(cmp:A->A->bool), + Lemma equal_spec : forall (A:Type)(m m':t A)(cmp:A->A->bool), equal cmp m m' = true <-> Equivb cmp m m'. -Proof. - split. apply equal_2. apply equal_1. -Qed. + Proof. + split. apply equal_2. apply equal_1. + Qed. End PositiveMap. diff --git a/theories/MMaps/vo.itarget b/theories/MMaps/vo.itarget index d4861cb06..a7bbd266e 100644 --- a/theories/MMaps/vo.itarget +++ b/theories/MMaps/vo.itarget @@ -4,3 +4,4 @@ MMapWeakList.vo MMapList.vo MMapPositive.vo MMaps.vo +MMapAVL.vo
\ No newline at end of file diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index e1fc454ae..cc023cc3f 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -31,7 +31,7 @@ code after extraction. *) -Require Import MSetInterface MSetGenTree ZArith Int. +Require Import MSetInterface MSetGenTree BinInt Int. Set Implicit Arguments. Unset Strict Implicit. @@ -83,11 +83,11 @@ Definition assert_false := create. Definition bal l x r := let hl := height l in let hr := height r in - if gt_le_dec hl (hr+2) then + if (hr+2) <? hl then match l with | Leaf => assert_false l x r | Node _ ll lx lr => - if ge_lt_dec (height ll) (height lr) then + if (height lr) <=? (height ll) then create ll lx (create lr x r) else match lr with @@ -97,11 +97,11 @@ Definition bal l x r := end end else - if gt_le_dec hr (hl+2) then + if (hl+2) <? hr then match r with | Leaf => assert_false l x r | Node _ rl rx rr => - if ge_lt_dec (height rr) (height rl) then + if (height rl) <=? (height rr) then create (create l x rl) rx rr else match rl with @@ -138,8 +138,8 @@ Fixpoint join l : elt -> t -> t := fix join_aux (r:t) : t := match r with | Leaf => add x l | Node rh rl rx rr => - if gt_le_dec lh (rh+2) then bal ll lx (join lr x r) - else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rr + if (rh+2) <? lh then bal ll lx (join lr x r) + else if (lh+2) <? rh then bal (join_aux rl) rx rr else create l x r end end. @@ -419,12 +419,12 @@ Local Open Scope Int_scope. Ltac join_tac := intro l; induction l as [| lh ll _ lx lr Hlr]; [ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join; - [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE]; + [ | destruct ((rh+2) <? lh) eqn:LT; [ match goal with |- context b [ bal ?a ?b ?c] => replace (bal a b c) with (bal ll lx (join lr x (Node rh rl rx rr))); [ | auto] end - | destruct (gt_le_dec rh (lh+2)) as [GT'|LE']; + | destruct ((lh+2) <? rh) eqn:LT'; [ match goal with |- context b [ bal ?a ?b ?c] => replace (bal a b c) with (bal (join (Node lh ll lx lr) x rl) rx rr); [ | auto] diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index cfb30662b..6d30319c9 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo_def. -Require Import Omega. +Require Import OmegaTactic. Local Open Scope R_scope. Definition A1 (x:R) (N:nat) : R := diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 99ecd150b..d210792f9 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(** * An light axiomatization of integers (used in FSetAVL). *) +(** * An light axiomatization of integers (used in MSetAVL). *) (** We define a signature for an integer datatype based on [Z]. The goal is to allow a switch after extraction to ocaml's @@ -14,11 +14,11 @@ (typically : when mesuring the height of an AVL tree). *) -Require Import ZArith. +Require Import BinInt. Delimit Scope Int_scope with I. Local Open Scope Int_scope. -(** * a specification of integers *) +(** * A specification of integers *) Module Type Int. @@ -31,19 +31,19 @@ Module Type Int. Parameter _1 : t. Parameter _2 : t. Parameter _3 : t. - Parameter plus : t -> t -> t. + Parameter add : t -> t -> t. Parameter opp : t -> t. - Parameter minus : t -> t -> t. - Parameter mult : t -> t -> t. + Parameter sub : t -> t -> t. + Parameter mul : t -> t -> t. Parameter max : t -> t -> t. Notation "0" := _0 : Int_scope. Notation "1" := _1 : Int_scope. Notation "2" := _2 : Int_scope. Notation "3" := _3 : Int_scope. - Infix "+" := plus : Int_scope. - Infix "-" := minus : Int_scope. - Infix "*" := mult : Int_scope. + Infix "+" := add : Int_scope. + Infix "-" := sub : Int_scope. + Infix "*" := mul : Int_scope. Notation "- x" := (opp x) : Int_scope. (** For logical relations, we can rely on their counterparts in Z, @@ -61,7 +61,17 @@ Module Type Int. Notation "x < y < z" := (x < y /\ y < z) : Int_scope. Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope. - (** Some decidability fonctions (informative). *) + (** Informative comparisons. *) + + Axiom eqb : t -> t -> bool. + Axiom ltb : t -> t -> bool. + Axiom leb : t -> t -> bool. + + Infix "=?" := eqb. + Infix "<?" := ltb. + Infix "<=?" := leb. + + (** For compatibility, some decidability fonctions (informative). *) Axiom gt_le_dec : forall x y : t, {x > y} + {x <= y}. Axiom ge_lt_dec : forall x y : t, {x >= y} + {x < y}. @@ -83,11 +93,14 @@ Module Type Int. Axiom i2z_1 : i2z _1 = 1%Z. Axiom i2z_2 : i2z _2 = 2%Z. Axiom i2z_3 : i2z _3 = 3%Z. - Axiom i2z_plus : forall n p, i2z (n + p) = (i2z n + i2z p)%Z. + Axiom i2z_add : forall n p, i2z (n + p) = (i2z n + i2z p)%Z. Axiom i2z_opp : forall n, i2z (-n) = (-i2z n)%Z. - Axiom i2z_minus : forall n p, i2z (n - p) = (i2z n - i2z p)%Z. - Axiom i2z_mult : forall n p, i2z (n * p) = (i2z n * i2z p)%Z. + Axiom i2z_sub : forall n p, i2z (n - p) = (i2z n - i2z p)%Z. + Axiom i2z_mul : forall n p, i2z (n * p) = (i2z n * i2z p)%Z. Axiom i2z_max : forall n p, i2z (max n p) = Z.max (i2z n) (i2z p). + Axiom i2z_eqb : forall n p, eqb n p = Z.eqb (i2z n) (i2z p). + Axiom i2z_ltb : forall n p, ltb n p = Z.ltb (i2z n) (i2z p). + Axiom i2z_leb : forall n p, leb n p = Z.leb (i2z n) (i2z p). End Int. @@ -97,11 +110,42 @@ End Int. Module MoreInt (Import I:Int). Local Notation int := I.t. + Lemma eqb_eq n p : (n =? p) = true <-> n == p. + Proof. + now rewrite i2z_eqb, Z.eqb_eq. + Qed. + + Lemma eqb_neq n p : (n =? p) = false <-> ~(n == p). + Proof. + rewrite <- eqb_eq. destruct (n =? p); intuition. + Qed. + + Lemma ltb_lt n p : (n <? p) = true <-> n < p. + Proof. + now rewrite i2z_ltb, Z.ltb_lt. + Qed. + + Lemma ltb_nlt n p : (n <? p) = false <-> ~(n < p). + Proof. + rewrite <- ltb_lt. destruct (n <? p); intuition. + Qed. + + Lemma leb_le n p : (n <=? p) = true <-> n <= p. + Proof. + now rewrite i2z_leb, Z.leb_le. + Qed. + + Lemma leb_nle n p : (n <=? p) = false <-> ~(n <= p). + Proof. + rewrite <- leb_le. destruct (n <=? p); intuition. + Qed. + (** A magic (but costly) tactic that goes from [int] back to the [Z] friendly world ... *) Hint Rewrite -> - i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z. + i2z_0 i2z_1 i2z_2 i2z_3 i2z_add i2z_opp i2z_sub i2z_mul i2z_max + i2z_eqb i2z_ltb i2z_leb : i2z. Ltac i2z := match goal with | H : ?a = ?b |- _ => @@ -149,18 +193,18 @@ Module MoreInt (Import I:Int). | EI1 : ExprI | EI2 : ExprI | EI3 : ExprI - | EIplus : ExprI -> ExprI -> ExprI + | EIadd : ExprI -> ExprI -> ExprI | EIopp : ExprI -> ExprI - | EIminus : ExprI -> ExprI -> ExprI - | EImult : ExprI -> ExprI -> ExprI + | EIsub : ExprI -> ExprI -> ExprI + | EImul : ExprI -> ExprI -> ExprI | EImax : ExprI -> ExprI -> ExprI | EIraw : int -> ExprI. Inductive ExprZ : Set := - | EZplus : ExprZ -> ExprZ -> ExprZ + | EZadd : ExprZ -> ExprZ -> ExprZ | EZopp : ExprZ -> ExprZ - | EZminus : ExprZ -> ExprZ -> ExprZ - | EZmult : ExprZ -> ExprZ -> ExprZ + | EZsub : ExprZ -> ExprZ -> ExprZ + | EZmul : ExprZ -> ExprZ -> ExprZ | EZmax : ExprZ -> ExprZ -> ExprZ | EZofI : ExprI -> ExprZ | EZraw : Z -> ExprZ. @@ -186,9 +230,9 @@ Module MoreInt (Import I:Int). | 1 => constr:EI1 | 2 => constr:EI2 | 3 => constr:EI3 - | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIplus ex ey) - | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIminus ex ey) - | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImult ex ey) + | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey) + | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey) + | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul ex ey) | max ?x ?y => let ex := i2ei x with ey := i2ei y in constr:(EImax ex ey) | - ?x => let ex := i2ei x in constr:(EIopp ex) | ?x => constr:(EIraw x) @@ -198,9 +242,9 @@ Module MoreInt (Import I:Int). with z2ez trm := match constr:trm with - | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey) - | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey) - | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey) + | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey) + | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey) + | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul ex ey) | (Z.max ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey) | (- ?x)%Z => let ex := z2ez x in constr:(EZopp ex) | i2z ?x => let ex := i2ei x in constr:(EZofI ex) @@ -232,9 +276,9 @@ Module MoreInt (Import I:Int). | EI1 => 1 | EI2 => 2 | EI3 => 3 - | EIplus e1 e2 => (ei2i e1)+(ei2i e2) - | EIminus e1 e2 => (ei2i e1)-(ei2i e2) - | EImult e1 e2 => (ei2i e1)*(ei2i e2) + | EIadd e1 e2 => (ei2i e1)+(ei2i e2) + | EIsub e1 e2 => (ei2i e1)-(ei2i e2) + | EImul e1 e2 => (ei2i e1)*(ei2i e2) | EImax e1 e2 => max (ei2i e1) (ei2i e2) | EIopp e => -(ei2i e) | EIraw i => i @@ -244,9 +288,9 @@ Module MoreInt (Import I:Int). Fixpoint ez2z (e:ExprZ) : Z := match e with - | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z - | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z - | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z + | EZadd e1 e2 => ((ez2z e1)+(ez2z e2))%Z + | EZsub e1 e2 => ((ez2z e1)-(ez2z e2))%Z + | EZmul e1 e2 => ((ez2z e1)*(ez2z e2))%Z | EZmax e1 e2 => Z.max (ez2z e1) (ez2z e2) | EZopp e => (-(ez2z e))%Z | EZofI e => i2z (ei2i e) @@ -278,9 +322,9 @@ Module MoreInt (Import I:Int). | EI1 => EZraw (1%Z) | EI2 => EZraw (2%Z) | EI3 => EZraw (3%Z) - | EIplus e1 e2 => EZplus (norm_ei e1) (norm_ei e2) - | EIminus e1 e2 => EZminus (norm_ei e1) (norm_ei e2) - | EImult e1 e2 => EZmult (norm_ei e1) (norm_ei e2) + | EIadd e1 e2 => EZadd (norm_ei e1) (norm_ei e2) + | EIsub e1 e2 => EZsub (norm_ei e1) (norm_ei e2) + | EImul e1 e2 => EZmul (norm_ei e1) (norm_ei e2) | EImax e1 e2 => EZmax (norm_ei e1) (norm_ei e2) | EIopp e => EZopp (norm_ei e) | EIraw i => EZofI (EIraw i) @@ -290,9 +334,9 @@ Module MoreInt (Import I:Int). Fixpoint norm_ez (e:ExprZ) : ExprZ := match e with - | EZplus e1 e2 => EZplus (norm_ez e1) (norm_ez e2) - | EZminus e1 e2 => EZminus (norm_ez e1) (norm_ez e2) - | EZmult e1 e2 => EZmult (norm_ez e1) (norm_ez e2) + | EZadd e1 e2 => EZadd (norm_ez e1) (norm_ez e2) + | EZsub e1 e2 => EZsub (norm_ez e1) (norm_ez e2) + | EZmul e1 e2 => EZmul (norm_ez e1) (norm_ez e2) | EZmax e1 e2 => EZmax (norm_ez e1) (norm_ez e2) | EZopp e => EZopp (norm_ez e) | EZofI e => norm_ei e @@ -316,24 +360,22 @@ Module MoreInt (Import I:Int). | EPraw p => EPraw p end. - Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e). + Lemma norm_ei_correct (e:ExprI) : ez2z (norm_ei e) = i2z (ei2i e). Proof. - induction e; simpl; intros; i2z; auto; try congruence. + induction e; simpl; i2z; auto; try congruence. Qed. - Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e. + Lemma norm_ez_correct (e:ExprZ) : ez2z (norm_ez e) = ez2z e. Proof. - induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct. + induction e; simpl; i2z; auto; try congruence; apply norm_ei_correct. Qed. - Lemma norm_ep_correct : - forall e:ExprP, ep2p (norm_ep e) <-> ep2p e. + Lemma norm_ep_correct (e:ExprP) : ep2p (norm_ep e) <-> ep2p e. Proof. - induction e; simpl; repeat (rewrite norm_ez_correct); intuition. + induction e; simpl; rewrite ?norm_ez_correct; intuition. Qed. - Lemma norm_ep_correct2 : - forall e:ExprP, ep2p (norm_ep e) -> ep2p e. + Lemma norm_ep_correct2 (e:ExprP) : ep2p (norm_ep e) -> ep2p e. Proof. intros; destruct (norm_ep_correct e); auto. Qed. @@ -363,23 +405,50 @@ Module Z_as_Int <: Int. Definition _1 := 1. Definition _2 := 2. Definition _3 := 3. - Definition plus := Z.add. + Definition add := Z.add. Definition opp := Z.opp. - Definition minus := Z.sub. - Definition mult := Z.mul. + Definition sub := Z.sub. + Definition mul := Z.mul. Definition max := Z.max. - Definition gt_le_dec := Z_gt_le_dec. - Definition ge_lt_dec := Z_ge_lt_dec. + Definition eqb := Z.eqb. + Definition ltb := Z.ltb. + Definition leb := Z.leb. + Definition eq_dec := Z.eq_dec. + Definition gt_le_dec i j : {i > j} + { i <= j }. + Proof. + generalize (Z.ltb_spec j i). + destruct (j <? i); [left|right]; inversion H; trivial. + now apply Z.lt_gt. + Defined. + Definition ge_lt_dec i j : {i >= j} + { i < j }. + Proof. + generalize (Z.ltb_spec i j). + destruct (i <? j); [right|left]; inversion H; trivial. + now apply Z.le_ge. + Defined. + Definition i2z : t -> Z := fun n => n. - Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed. - Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed. - Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed. - Lemma i2z_2 : i2z _2 = 2. Proof. auto. Qed. - Lemma i2z_3 : i2z _3 = 3. Proof. auto. Qed. - Lemma i2z_plus n p : i2z (n + p) = i2z n + i2z p. Proof. auto. Qed. - Lemma i2z_opp n : i2z (- n) = - i2z n. Proof. auto. Qed. - Lemma i2z_minus n p : i2z (n - p) = i2z n - i2z p. Proof. auto. Qed. - Lemma i2z_mult n p : i2z (n * p) = i2z n * i2z p. Proof. auto. Qed. - Lemma i2z_max n p : i2z (max n p) = Z.max (i2z n) (i2z p). Proof. auto. Qed. + Lemma i2z_eq n p : i2z n = i2z p -> n = p. Proof. trivial. Qed. + Lemma i2z_0 : i2z _0 = 0. Proof. reflexivity. Qed. + Lemma i2z_1 : i2z _1 = 1. Proof. reflexivity. Qed. + Lemma i2z_2 : i2z _2 = 2. Proof. reflexivity. Qed. + Lemma i2z_3 : i2z _3 = 3. Proof. reflexivity. Qed. + Lemma i2z_add n p : i2z (n + p) = i2z n + i2z p. + Proof. reflexivity. Qed. + Lemma i2z_opp n : i2z (- n) = - i2z n. + Proof. reflexivity. Qed. + Lemma i2z_sub n p : i2z (n - p) = i2z n - i2z p. + Proof. reflexivity. Qed. + Lemma i2z_mul n p : i2z (n * p) = i2z n * i2z p. + Proof. reflexivity. Qed. + Lemma i2z_max n p : i2z (max n p) = Z.max (i2z n) (i2z p). + Proof. reflexivity. Qed. + Lemma i2z_eqb n p : eqb n p = Z.eqb (i2z n) (i2z p). + Proof. reflexivity. Qed. + Lemma i2z_leb n p : leb n p = Z.leb (i2z n) (i2z p). + Proof. reflexivity. Qed. + Lemma i2z_ltb n p : ltb n p = Z.ltb (i2z n) (i2z p). + Proof. reflexivity. Qed. + End Z_as_Int. diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 20dd69f82..cb7041467 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -456,13 +456,7 @@ rule coq_bol = parse { begin_show (); coq_bol lexbuf } | space* end_show { end_show (); coq_bol lexbuf } - | space* ("Local"|"Global") - { - in_proof := None; - let s = lexeme lexbuf in - output_indented_keyword s lexbuf; - coq_bol lexbuf } - | space* gallina_kw_to_hide + | space* (("Local"|"Global") space+)? gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then let eol = skip_to_dot lexbuf in @@ -596,7 +590,7 @@ and coq = parse end } | eof { () } - | gallina_kw_to_hide + | (("Local"|"Global") space+)? gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then begin diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index ae6e6388f..06030c45a 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -595,7 +595,6 @@ module Html = struct | '<' -> Buffer.add_string buff "<" | '>' -> Buffer.add_string buff ">" | '&' -> Buffer.add_string buff "&" - | '\'' -> Buffer.add_string buff "´" | '\"' -> Buffer.add_string buff """ | c -> Buffer.add_char buff c done; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 1ce3fe28d..3385d67e3 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,26 +59,23 @@ let load_rcfile() = (* Puts dir in the path of ML and in the LoadPath *) let coq_add_path unix_path s = - Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true; + Mltop.add_rec_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true; Mltop.add_ml_dir unix_path (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = - if !Flags.load_init then - Mltop.add_rec_path ~unix_path ~coq_root ~implicit:true - else - Mltop.add_path ~unix_path ~coq_root ~implicit:false; + Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init); if with_ml then Mltop.add_rec_ml_dir unix_path let add_userlib_path ~unix_path = - Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; + Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; Mltop.add_rec_ml_dir unix_path (* Options -I, -I-as, and -R of the command line *) let includes = ref [] -let push_include s alias recursive implicit = - includes := (s,alias,recursive,implicit) :: !includes +let push_include s alias implicit = + includes := (s, alias, implicit) :: !includes let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes @@ -109,13 +106,13 @@ let init_load_path () = List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs; (* then directories in COQPATH *) List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath; - (* then current directory *) - Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix ~implicit:false; - (* additional loadpath, given with options -I-as, -Q, and -R *) + (* then current directory (not recursively!) *) + Mltop.add_ml_dir "."; + Loadpath.add_load_path "." Nameops.default_root_prefix ~implicit:false; + (* additional loadpath, given with options -Q and -R *) List.iter - (fun (unix_path, coq_root, reci, implicit) -> - (if reci then Mltop.add_rec_path else Mltop.add_path) - ~unix_path ~coq_root ~implicit) + (fun (unix_path, coq_root, implicit) -> + Mltop.add_rec_path ~unix_path ~coq_root ~implicit) (List.rev !includes); (* additional ml directories, given with option -I *) List.iter Mltop.add_ml_dir (List.rev !ml_includes) diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 5f7133c37..c019cc1ce 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -15,8 +15,8 @@ val set_rcfile : string -> unit val no_load_rc : unit -> unit val load_rcfile : unit -> unit -val push_include : string -> Names.DirPath.t -> bool -> bool -> unit -(** [push_include phys_path log_path recursive implicit] *) +val push_include : string -> Names.DirPath.t -> bool -> unit +(** [push_include phys_path log_path implicit] *) val push_ml_include : string -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 22ab469dc..1544fd869 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -135,9 +135,9 @@ let set_outputstate s = outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate -let set_include d p recursive implicit = +let set_include d p implicit = let p = dirpath_of_string p in - push_include d p recursive implicit + push_include d p implicit let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = @@ -402,21 +402,21 @@ let parse_args arglist = (* Complex options with many args *) |"-I"|"-include" -> begin match rem with - | d :: "-as" :: p :: rem -> set_include d p false true; args := rem - | d :: "-as" :: [] -> error_missing_arg "-as" | d :: rem -> push_ml_include d; args := rem | [] -> error_missing_arg opt end |"-Q" -> begin match rem with - | d :: p :: rem -> set_include d p true false; args := rem + | d :: p :: rem -> set_include d p false; args := rem | _ -> error_missing_arg opt end |"-R" -> begin match rem with - | d :: "-as" :: [] -> error_missing_arg "-as" - | d :: "-as" :: p :: rem - | d :: p :: rem -> set_include d p true true; args := rem + | d :: "-as" :: [] -> error_missing_arg opt + | d :: "-as" :: p :: rem -> + warning "option -R * -as * deprecated, remove the -as"; + set_include d p true; args := rem + | d :: p :: rem -> set_include d p true; args := rem | _ -> error_missing_arg opt end diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index e7500f6ae..2362d250e 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -161,15 +161,6 @@ let add_rec_ml_dir unix_path = (* Adding files to Coq and ML loadpath *) -let add_path ~unix_path:dir ~coq_root:coq_dirpath ~implicit = - if exists_dir dir then - begin - add_ml_dir dir; - Loadpath.add_load_path dir ~root:true ~implicit coq_dirpath - end - else - msg_warning (str ("Cannot open " ^ dir)) - let convert_string d = try Names.Id.of_string d with UserError _ -> @@ -189,9 +180,9 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let dirs = List.map_filter convert_dirs dirs in let () = add_ml_dir unix_path in let add (path, dir) = - Loadpath.add_load_path path ~root:false ~implicit dir in + Loadpath.add_load_path path ~implicit dir in let () = List.iter add dirs in - Loadpath.add_load_path unix_path ~root:true ~implicit coq_root + Loadpath.add_load_path unix_path ~implicit coq_root else msg_warning (str ("Cannot open " ^ unix_path)) diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 2a91afd88..4f3f4ddde 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -47,7 +47,6 @@ val add_ml_dir : string -> unit val add_rec_ml_dir : string -> unit (** Adds a path to the Coq and ML paths *) -val add_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit (** List of modules linked to the toplevel *) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 4ee3bc474..f053839c7 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -23,9 +23,7 @@ let print_usage_channel co command = output_string co " -I dir look for ML files in dir\ \n -include dir (idem)\ -\n -I dir -as coqdir implicitly map physical dir to logical coqdir\ -\n -R dir -as coqdir recursively map physical dir to logical coqdir\ -\n -R dir coqdir (idem)\ +\n -R dir coqdir recursively map physical dir to logical coqdir\ \n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ \n -notop set the toplevel name to be the empty logical path\ diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 62e5f0a32..cfa9bddc6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -387,12 +387,13 @@ let err_unmapped_library loc qid = pr_dirpath dir ++ str".") let err_notfound_library loc qid = - msg_error - (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")) + user_err_loc + (loc,"locate_library", + strbrk "Unable to locate library " ++ pr_qualid qid ++ str".") let print_located_library r = let (loc,qid) = qualid_of_reference r in - try msg_found_library (Library.locate_qualified_library false qid) + try msg_found_library (Library.locate_qualified_library ~warn:false qid) with | Library.LibUnmappedDir -> err_unmapped_library loc qid | Library.LibNotFound -> err_notfound_library loc qid @@ -750,12 +751,24 @@ let vernac_end_segment (_,id as lid) = (* Libraries *) let vernac_require from import qidl = - let qidl = match from with - | None -> qidl - | Some ns -> List.map (Libnames.join_reference ns) qidl - in let qidl = List.map qualid_of_reference qidl in - let modrefl = List.map Library.try_locate_qualified_library qidl in + let root = match from with + | None -> None + | Some from -> + let (_, qid) = Libnames.qualid_of_reference from in + let (hd, tl) = Libnames.repr_qualid qid in + Some (Libnames.add_dirpath_suffix hd tl) + in + let locate (loc, qid) = + try + let warn = Flags.is_verbose () in + let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in + (dir, f) + with + | Library.LibUnmappedDir -> err_unmapped_library loc qid + | Library.LibNotFound -> err_notfound_library loc qid + in + let modrefl = List.map locate qidl in if Dumpglob.dump () then List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl); Library.require_library_from_dirpath modrefl import @@ -879,11 +892,10 @@ let vernac_set_used_variables e = let expand filename = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename -let vernac_add_loadpath isrec pdir ldiropt = +let vernac_add_loadpath implicit pdir ldiropt = let pdir = expand pdir in let alias = Option.default Nameops.default_root_prefix ldiropt in - (if isrec then Mltop.add_rec_path else Mltop.add_path) - ~unix_path:pdir ~coq_root:alias ~implicit:true + Mltop.add_rec_path ~unix_path:pdir ~coq_root:alias ~implicit let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) |