realizations.tex 3.68 KB
 Guillaume Melquiond committed Mar 23, 2012 1 2 3 4 5 6 7 8 9 10 \chapter{Theory realizations} \label{chap:realizations} \section{Generating a realization} Generating the skeleton for a theory is done by passing to \why the \verb+--realize+ option, a driver suitable for realizations, the names of the theories to realize, and the target directory. \begin{verbatim}  MARCHE Claude committed Apr 06, 2012 11 why3 --realize -D path/to/drivers/coq-realize.drv  Guillaume Melquiond committed Mar 23, 2012 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93  -T env_path.theory_name -o path/to/target/dir/ \end{verbatim} The name of the generated file is inferred from the theory name. If the target directory already contains a file with the same name, \why extracts all the parts that it assumes to be user-made and prints them in the generated file. \section{Using realizations inside proofs} If a theory has been realized, a \why printer for an interactive prover will no longer output assumptions from the theory but instead simply put a directive to load the realization. In order to indicate to the printer that a given theory is realized, one has to add a meta declaration to the corresponding theory section. \begin{verbatim} theory env_path.theory_name meta "realized" "env_path.theory_name", "optional_naming" end \end{verbatim} The first parameter is the theory name for \why, while the second parameter, if not empty, provides a name to be used inside generated scripts to point to the realization, in case the default name is not suitable for the interactive prover. \section{Coq scripts} This section describes the content of the Coq files generated by \why for both proof obligations and theory realizations. When reading a Coq script, \why is guided by the presence of empty lines to split the script, so the user should refrain from removing empty lines around generated parts or adding empty lines inside them. \begin{enumerate} \item The header of the file contains all the library inclusions required by the driver file. Any user-made changes to this part will be lost when the file is regenerated by \why. This part ends at the first empty line. \item Abstract logic symbols are assumed with the vernacular directive \verb+Paramater+. Axioms are assumed with the \verb+Axiom+ directive. When regenerating a script, \why assumes that all such symbols have been generated by a previous run. As a consequence, the user should not introduce new symbols with these two directives, as they would be lost. \item Definitions of functions and inductive types in theories are printed in a block that starts with \verb+(* Why3 assumption *)+. This comment should not be removed; otherwise \why will assume that the definition is user-made. \item Finally, proof obligations and symbols to be realized are introduced by \verb+(* Why3 goal *)+. The user is supposed to fill the script after the statement. \why assumes that the user-made part extends up to \verb+Qed+, \verb+Admitted+, \verb+Save+, or \verb+Defined+, whichever comes first. In the case of definitions, the original statement can be replaced by a \verb+Notation+ directive, in order to ease the usage of already defined symbols. \end{enumerate} Currently, the parser for Coq scripts is rather naive and does not know much about comments. For instance, \why can easily be confused by some terminating directive like \verb+Qed+ that would be present in a comment. \section{Shipping libraries of realizations} While modifying an existing driver file might be sufficient for local use, it does not scale well when the realizations are to be shipped to other users. Instead, an additional configuration file should be created. \begin{verbatim} [main] loadpath="path/to/theories" [prover coq] option="-R path/to/vo/files Logical_directory" driver="path/to/extra_coq.drv" \end{verbatim} This file can be passed to \why thanks to the \verb+--extra-config+ option.