Commit 368592f2 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Early documentation about realizations.

parent 16f0445d
......@@ -222,6 +222,8 @@ are the following.
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
\chapter{Theory 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.
\why3 --realize -D path/to/drivers/coq-realize.drv
-T env_path.theory_name -o path/to/target/dir/
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.
theory env_path.theory_name
meta "realized" "env_path.theory_name", "optional_naming"
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.
\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.
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
\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.
[prover coq]
option="-R path/to/vo/files Logical_directory"
This file can be passed to \why thanks to the \verb+--extra-config+
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment