Commit 2b61be07 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Move away most of the generated files from doc/ as it is getting crowded.

parent 54d6b937
...@@ -120,21 +120,17 @@ why3.conf ...@@ -120,21 +120,17 @@ why3.conf
/doc/manual.synctex.gz /doc/manual.synctex.gz
/doc/*.haux /doc/*.haux
/doc/*.pdf /doc/*.pdf
/doc/generated/
/doc/html/ /doc/html/
/doc/*.hind /doc/*.hind
/doc/*.htoc /doc/*.htoc
/doc/bnf /doc/bnf
/doc/bnf.ml /doc/bnf.ml
/doc/*_bnf.tex
/doc/apidoc.tex /doc/apidoc.tex
/doc/apidoc/ /doc/apidoc/
/doc/stdlibdoc/ /doc/stdlibdoc/
/doc/texput.log /doc/texput.log
/doc/extract_ocaml_code /doc/extract_ocaml_code
/doc/logic_*.ml
/doc/call_provers_*.ml
/doc/whyconf_*.ml
/doc/*__*.ml
# /lib # /lib
/lib/why3-cpulimit /lib/why3-cpulimit
......
...@@ -1860,9 +1860,9 @@ doc: doc/manual.pdf doc/html/index.html ...@@ -1860,9 +1860,9 @@ doc: doc/manual.pdf doc/html/index.html
BNF = ident qualid attribute constant operator type formula term1 term2 term3 \ BNF = ident qualid attribute constant operator type formula term1 term2 term3 \
theory theory2 \ theory theory2 \
why_file spec expr expr2 module whyml_file term_old_at why_file spec expr expr2 module whyml_file term_old_at
BNFTEX = $(BNF:%=doc/%_bnf.tex) BNFTEX = $(BNF:%=doc/generated/%_bnf.tex)
doc/%_bnf.tex: doc/%.bnf doc/bnf$(EXE) doc/generated/%_bnf.tex: doc/%.bnf doc/bnf$(EXE)
doc/bnf$(EXE) $< > $@ doc/bnf$(EXE) $< > $@
doc/bnf$(EXE): doc/bnf.mll doc/bnf$(EXE): doc/bnf.mll
...@@ -1872,19 +1872,19 @@ doc/bnf$(EXE): doc/bnf.mll ...@@ -1872,19 +1872,19 @@ doc/bnf$(EXE): doc/bnf.mll
doc/extract_ocaml_code: doc/extract_ocaml_code.ml doc/extract_ocaml_code: doc/extract_ocaml_code.ml
$(OCAMLC) str.cma -o $@ $< $(OCAMLC) str.cma -o $@ $<
doc/logic__%.ml: examples/use_api/logic.ml doc/extract_ocaml_code doc/generated/logic__%.ml: examples/use_api/logic.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@ doc/extract_ocaml_code $* < $< > $@
doc/whyconf__%.ml: src/driver/whyconf.ml doc/extract_ocaml_code doc/generated/whyconf__%.ml: src/driver/whyconf.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@ doc/extract_ocaml_code $* < $< > $@
doc/call_provers__%.ml: src/driver/call_provers.ml doc/extract_ocaml_code doc/generated/call_provers__%.ml: src/driver/call_provers.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@ doc/extract_ocaml_code $* < $< > $@
doc/mlw_tree__%.ml: examples/use_api/mlw_tree.ml doc/extract_ocaml_code doc/generated/mlw_tree__%.ml: examples/use_api/mlw_tree.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@ doc/extract_ocaml_code $* < $< > $@
doc/transform__%.ml: examples/use_api/transform.ml doc/extract_ocaml_code doc/generated/transform__%.ml: examples/use_api/transform.ml doc/extract_ocaml_code
doc/extract_ocaml_code $* < $< > $@ doc/extract_ocaml_code $* < $< > $@
OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \ OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \
...@@ -1904,11 +1904,12 @@ OCAMLCODE_MLWTREE = buildenv openmodule useimport \ ...@@ -1904,11 +1904,12 @@ OCAMLCODE_MLWTREE = buildenv openmodule useimport \
source1 code1 helper1 source2 code2 source3 code3 \ source1 code1 helper1 source2 code2 source3 code3 \
closemodule checkingvcs closemodule checkingvcs
OCAMLCODE = $(addprefix doc/logic__, $(addsuffix .ml, $(OCAMLCODE_LOGIC))) \ OCAMLCODE = \
$(addprefix doc/call_provers__, $(addsuffix .ml, $(OCAMLCODE_CALLPROVERS))) \ $(addprefix doc/generated/logic__, $(addsuffix .ml, $(OCAMLCODE_LOGIC))) \
$(addprefix doc/transform__, $(addsuffix .ml, $(OCAMLCODE_TRANSFORM))) \ $(addprefix doc/generated/call_provers__, $(addsuffix .ml, $(OCAMLCODE_CALLPROVERS))) \
$(addprefix doc/mlw_tree__, $(addsuffix .ml, $(OCAMLCODE_MLWTREE))) \ $(addprefix doc/generated/transform__, $(addsuffix .ml, $(OCAMLCODE_TRANSFORM))) \
doc/whyconf__provertype.ml $(addprefix doc/generated/mlw_tree__, $(addsuffix .ml, $(OCAMLCODE_MLWTREE))) \
doc/generated/whyconf__provertype.ml
DOC = api glossary ide intro exec macros manpages install \ DOC = api glossary ide intro exec macros manpages install \
manual starting syntax syntaxref technical version whyml \ manual starting syntax syntaxref technical version whyml \
......
...@@ -24,7 +24,7 @@ The first step is to know how to build propositional formulas. The ...@@ -24,7 +24,7 @@ The first step is to know how to build propositional formulas. The
module \texttt{Term} gives a few functions for building these. Here is module \texttt{Term} gives a few functions for building these. Here is
a piece of OCaml code for building the formula $\mathit{true} \lor a piece of OCaml code for building the formula $\mathit{true} \lor
\mathit{false}$. \mathit{false}$.
\lstinputlisting{logic__opening.ml} \lstinputlisting{generated/logic__opening.ml}
The library uses the common type \texttt{term} both for terms The library uses the common type \texttt{term} both for terms
(\ie expressions that produce a value of some particular type) (\ie expressions that produce a value of some particular type)
and formulas (\ie boolean-valued expressions). and formulas (\ie boolean-valued expressions).
...@@ -35,7 +35,7 @@ and formulas (\ie boolean-valued expressions). ...@@ -35,7 +35,7 @@ and formulas (\ie boolean-valued expressions).
Such a formula can be printed using the module \texttt{Pretty} Such a formula can be printed using the module \texttt{Pretty}
providing pretty-printers. providing pretty-printers.
\lstinputlisting{logic__printformula.ml} \lstinputlisting{generated/logic__printformula.ml}
Assuming the lines above are written in a file \texttt{f.ml}, it can Assuming the lines above are written in a file \texttt{f.ml}, it can
be compiled using be compiled using
...@@ -50,12 +50,12 @@ formula 1 is: true \/ false ...@@ -50,12 +50,12 @@ formula 1 is: true \/ false
Let us now build a formula with propositional variables: $A \land B Let us now build a formula with propositional variables: $A \land B
\rightarrow A$. Propositional variables must be declared first before \rightarrow A$. Propositional variables must be declared first before
using them in formulas. This is done as follows. using them in formulas. This is done as follows.
\lstinputlisting{logic__declarepropvars.ml} \lstinputlisting{generated/logic__declarepropvars.ml}
The type \texttt{lsymbol} is the type of function and predicate symbols (which The type \texttt{lsymbol} is the type of function and predicate symbols (which
we call logic symbols for brevity). Then the atoms $A$ and $B$ must be built we call logic symbols for brevity). Then the atoms $A$ and $B$ must be built
by the general function for applying a predicate symbol to a list of terms. by the general function for applying a predicate symbol to a list of terms.
Here we just need the empty list of arguments. Here we just need the empty list of arguments.
\lstinputlisting{logic__declarepropatoms.ml} \lstinputlisting{generated/logic__declarepropatoms.ml}
As expected, the output is as follows. As expected, the output is as follows.
\begin{verbatim} \begin{verbatim}
...@@ -74,7 +74,7 @@ tasks from our formulas. Task can be build incrementally from an empty ...@@ -74,7 +74,7 @@ tasks from our formulas. Task can be build incrementally from an empty
task by adding declaration to it, using the functions task by adding declaration to it, using the functions
\texttt{add\_*\_decl} of module \texttt{Task}. For the formula $\mathit{true} \lor \texttt{add\_*\_decl} of module \texttt{Task}. For the formula $\mathit{true} \lor
\mathit{false}$ above, this is done as follows. \mathit{false}$ above, this is done as follows.
\lstinputlisting{logic__buildtask.ml} \lstinputlisting{generated/logic__buildtask.ml}
To make the formula a goal, we must give a name to it, here ``goal1''. A To make the formula a goal, we must give a name to it, here ``goal1''. A
goal name has type \texttt{prsymbol}, for identifiers denoting goal name has type \texttt{prsymbol}, for identifiers denoting
propositions in a theory or a task. Notice again that the concrete propositions in a theory or a task. Notice again that the concrete
...@@ -86,12 +86,12 @@ Notice that lemmas are not allowed in tasks ...@@ -86,12 +86,12 @@ Notice that lemmas are not allowed in tasks
and can only be used in theories. and can only be used in theories.
Once a task is built, it can be printed. Once a task is built, it can be printed.
\lstinputlisting{logic__printtask.ml} \lstinputlisting{generated/logic__printtask.ml}
The task for our second formula is a bit more complex to build, because The task for our second formula is a bit more complex to build, because
the variables A and B must be added as abstract (\ie not defined) the variables A and B must be added as abstract (\ie not defined)
propositional symbols in the task. propositional symbols in the task.
\lstinputlisting{logic__buildtask2.ml} \lstinputlisting{generated/logic__buildtask2.ml}
Execution of our OCaml program now outputs: Execution of our OCaml program now outputs:
\begin{verbatim} \begin{verbatim}
...@@ -118,44 +118,44 @@ file \texttt{why3.conf}, as it was built using the \texttt{why3config} ...@@ -118,44 +118,44 @@ file \texttt{why3.conf}, as it was built using the \texttt{why3config}
command line tool or the \textsf{Detect Provers} menu of the graphical command line tool or the \textsf{Detect Provers} menu of the graphical
IDE. The following API calls allow to access the content of this IDE. The following API calls allow to access the content of this
configuration file. configuration file.
\lstinputlisting{logic__getconf.ml} \lstinputlisting{generated/logic__getconf.ml}
The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A
prover is a record with a name, a version, and an alternative description prover is a record with a name, a version, and an alternative description
(to differentiate between various configurations of a given prover). Its (to differentiate between various configurations of a given prover). Its
definition is in the module \texttt{Whyconf}: definition is in the module \texttt{Whyconf}:
\lstinputlisting{whyconf__provertype.ml} \lstinputlisting{generated/whyconf__provertype.ml}
The map \texttt{provers} provides the set of existing provers. The map \texttt{provers} provides the set of existing provers.
In the following, we directly In the following, we directly
attempt to access a prover named ``Alt-Ergo'', any version. attempt to access a prover named ``Alt-Ergo'', any version.
\lstinputlisting{logic__getanyaltergo.ml} \lstinputlisting{generated/logic__getanyaltergo.ml}
We could also get a specific version with : We could also get a specific version with :
\lstinputlisting{logic__getaltergo200.ml} \lstinputlisting{generated/logic__getaltergo200.ml}
The next step is to obtain the driver associated to this prover. A The next step is to obtain the driver associated to this prover. A
driver typically depends on the standard theories so these should be driver typically depends on the standard theories so these should be
loaded first. loaded first.
\lstinputlisting{logic__getdriver.ml} \lstinputlisting{generated/logic__getdriver.ml}
We are now ready to call the prover on the tasks. This is done by a We are now ready to call the prover on the tasks. This is done by a
function call that launches the external executable and waits for its function call that launches the external executable and waits for its
termination. Here is a simple way to proceed: termination. Here is a simple way to proceed:
\lstinputlisting{logic__callprover.ml} \lstinputlisting{generated/logic__callprover.ml}
This way to call a prover is in general too naive, since it may never This way to call a prover is in general too naive, since it may never
return if the prover runs without time limit. The function return if the prover runs without time limit. The function
\texttt{prove\_task} has an optional parameter \texttt{limit}, a record defined \texttt{prove\_task} has an optional parameter \texttt{limit}, a record defined
in module \texttt{Call\_provers}: in module \texttt{Call\_provers}:
\lstinputlisting{call_provers__resourcelimit.ml} \lstinputlisting{generated/call_provers__resourcelimit.ml}
where the field \texttt{limit\_time} is the maximum allowed running time in seconds, where the field \texttt{limit\_time} is the maximum allowed running time in seconds,
and \texttt{limit\_mem} is the maximum allowed memory in megabytes. The type and \texttt{limit\_mem} is the maximum allowed memory in megabytes. The type
\texttt{prover\_result} is a record defined in module \texttt{Call\_provers}: \texttt{prover\_result} is a record defined in module \texttt{Call\_provers}:
\lstinputlisting{call_provers__proverresult.ml} \lstinputlisting{generated/call_provers__proverresult.ml}
with in particular the fields: with in particular the fields:
\begin{itemize} \begin{itemize}
\item \texttt{pr\_answer}: the prover answer, explained below; \item \texttt{pr\_answer}: the prover answer, explained below;
\item \texttt{pr\_time} : the time taken by the prover, in seconds. \item \texttt{pr\_time} : the time taken by the prover, in seconds.
\end{itemize} \end{itemize}
A \texttt{pr\_answer} is the sum type defined in module \texttt{Call\_provers}: A \texttt{pr\_answer} is the sum type defined in module \texttt{Call\_provers}:
\lstinputlisting{call_provers__proveranswer.ml} \lstinputlisting{generated/call_provers__proveranswer.ml}
corresponding to these kinds of answers: corresponding to these kinds of answers:
\begin{itemize} \begin{itemize}
\item \texttt{Valid}: the task is valid according to the prover. \item \texttt{Valid}: the task is valid according to the prover.
...@@ -174,7 +174,7 @@ corresponding to these kinds of answers: ...@@ -174,7 +174,7 @@ corresponding to these kinds of answers:
\end{itemize} \end{itemize}
Here is thus another way of calling the Alt-Ergo prover, on our second Here is thus another way of calling the Alt-Ergo prover, on our second
task. task.
\lstinputlisting{logic__calltimelimit.ml} \lstinputlisting{generated/logic__calltimelimit.ml}
The output of our program is now as follows. The output of our program is now as follows.
\begin{verbatim} \begin{verbatim}
On task 1, alt-ergo answers Valid (0.01s) On task 1, alt-ergo answers Valid (0.01s)
...@@ -191,29 +191,29 @@ Here is the way we build the formula $2+2=4$. The main difficulty is to ...@@ -191,29 +191,29 @@ Here is the way we build the formula $2+2=4$. The main difficulty is to
access the internal identifier for addition: it must be retrieved from access the internal identifier for addition: it must be retrieved from
the standard theory \texttt{Int} of the file \texttt{int.why} (see the standard theory \texttt{Int} of the file \texttt{int.why} (see
Chap~\ref{sec:library}). Chap~\ref{sec:library}).
\lstinputlisting{logic__buildfmla.ml} \lstinputlisting{generated/logic__buildfmla.ml}
An important point to notice as that when building the application of An important point to notice as that when building the application of
$+$ to the arguments, it is checked that the types are correct. Indeed $+$ to the arguments, it is checked that the types are correct. Indeed
the constructor \texttt{t\_app\_infer} infers the type of the resulting the constructor \texttt{t\_app\_infer} infers the type of the resulting
term. One could also provide the expected type as follows. term. One could also provide the expected type as follows.
\lstinputlisting{logic__buildtermalt.ml} \lstinputlisting{generated/logic__buildtermalt.ml}
When building a task with this formula, we need to declare that we use When building a task with this formula, we need to declare that we use
theory \texttt{Int}: theory \texttt{Int}:
\lstinputlisting{logic__buildtaskimport.ml} \lstinputlisting{generated/logic__buildtaskimport.ml}
\section{Building Quantified Formulas} \section{Building Quantified Formulas}
To illustrate how to build quantified formulas, let us consider To illustrate how to build quantified formulas, let us consider
the formula $\forall x:int. x*x \geq 0$. The first step is to the formula $\forall x:int. x*x \geq 0$. The first step is to
obtain the symbols from \texttt{Int}. obtain the symbols from \texttt{Int}.
\lstinputlisting{logic__quantfmla1.ml} \lstinputlisting{generated/logic__quantfmla1.ml}
The next step is to introduce the variable $x$ with the type int. The next step is to introduce the variable $x$ with the type int.
\lstinputlisting{logic__quantfmla2.ml} \lstinputlisting{generated/logic__quantfmla2.ml}
The formula $x*x \geq 0$ is obtained as in the previous example. The formula $x*x \geq 0$ is obtained as in the previous example.
\lstinputlisting{logic__quantfmla3.ml} \lstinputlisting{generated/logic__quantfmla3.ml}
To quantify on $x$, we use the appropriate smart constructor as follows. To quantify on $x$, we use the appropriate smart constructor as follows.
\lstinputlisting{logic__quantfmla4.ml} \lstinputlisting{generated/logic__quantfmla4.ml}
\section{Building Theories} \section{Building Theories}
...@@ -226,33 +226,33 @@ be done by a sequence of calls: ...@@ -226,33 +226,33 @@ be done by a sequence of calls:
\end{itemize} \end{itemize}
Creation of a theory named \verb|My_theory| is done by Creation of a theory named \verb|My_theory| is done by
\lstinputlisting{logic__buildth1.ml} \lstinputlisting{generated/logic__buildth1.ml}
First let us add formula 1 above as a goal: First let us add formula 1 above as a goal:
\lstinputlisting{logic__buildth2.ml} \lstinputlisting{generated/logic__buildth2.ml}
Note that we reused the goal identifier \verb|goal_id1| that we Note that we reused the goal identifier \verb|goal_id1| that we
already defined to create task 1 above. already defined to create task 1 above.
Adding formula 2 needs to add the declarations of predicate variables A Adding formula 2 needs to add the declarations of predicate variables A
and B first: and B first:
\lstinputlisting{logic__buildth3.ml} \lstinputlisting{generated/logic__buildth3.ml}
Adding formula 3 is a bit more complex since it uses integers, thus it Adding formula 3 is a bit more complex since it uses integers, thus it
requires to ``use'' the theory \verb|int.Int|. Using a theory is requires to ``use'' the theory \verb|int.Int|. Using a theory is
indeed not a primitive operation in the API: it must be done by a indeed not a primitive operation in the API: it must be done by a
combination of an ``export'' and the creation of a namespace. We combination of an ``export'' and the creation of a namespace. We
provide a helper function for that: provide a helper function for that:
\lstinputlisting{logic__buildth4.ml} \lstinputlisting{generated/logic__buildth4.ml}
Addition of formula 3 is then Addition of formula 3 is then
\lstinputlisting{logic__buildth5.ml} \lstinputlisting{generated/logic__buildth5.ml}
Addition of goal 4 is nothing more complex: Addition of goal 4 is nothing more complex:
\lstinputlisting{logic__buildth6.ml} \lstinputlisting{generated/logic__buildth6.ml}
Finally, we close our theory under construction as follows. Finally, we close our theory under construction as follows.
\lstinputlisting{logic__buildth7.ml} \lstinputlisting{generated/logic__buildth7.ml}
We can inspect what we did by printing that theory: We can inspect what we did by printing that theory:
\lstinputlisting{logic__printtheory.ml} \lstinputlisting{generated/logic__printtheory.ml}
which outputs which outputs
\begin{verbatim} \begin{verbatim}
my new theory is as follows: my new theory is as follows:
...@@ -278,12 +278,12 @@ end ...@@ -278,12 +278,12 @@ end
From a theory, one can compute at once all the proof tasks it contains From a theory, one can compute at once all the proof tasks it contains
as follows: as follows:
\lstinputlisting{logic__splittheory.ml} \lstinputlisting{generated/logic__splittheory.ml}
Note that the tasks are returned in reverse order, so we reverse the Note that the tasks are returned in reverse order, so we reverse the
list above. list above.
We can check our generated tasks by printing them: We can check our generated tasks by printing them:
\lstinputlisting{logic__printalltasks.ml} \lstinputlisting{generated/logic__printalltasks.ml}
One can run provers on those tasks exactly as we did above. One can run provers on those tasks exactly as we did above.
...@@ -293,12 +293,12 @@ The following code illustrates a simple recursive functions of ...@@ -293,12 +293,12 @@ The following code illustrates a simple recursive functions of
formulas. It explores the formula and when a negation is found, it formulas. It explores the formula and when a negation is found, it
tries to push it down below a conjunction, a disjunction or a tries to push it down below a conjunction, a disjunction or a
quantifier. quantifier.
\lstinputlisting{transform__negate.ml} \lstinputlisting{generated/transform__negate.ml}
The following illustrates how to turn such an OCaml function into a The following illustrates how to turn such an OCaml function into a
transformation in the sens of Why3 API. moreover, it registers that transformation in the sens of Why3 API. moreover, it registers that
transformation to make it available for example in Why3 IDE. transformation to make it available for example in Why3 IDE.
\lstinputlisting{transform__register.ml} \lstinputlisting{generated/transform__register.ml}
The directory \verb|src/transform| contains the code for the many The directory \verb|src/transform| contains the code for the many
transformations that are already available in Why3. transformations that are already available in Why3.
...@@ -322,13 +322,13 @@ The first step is to build an environment as already illustrated in ...@@ -322,13 +322,13 @@ The first step is to build an environment as already illustrated in
Section~\ref{sec:api:callingprovers}, and open the OCaml module Section~\ref{sec:api:callingprovers}, and open the OCaml module
\verb|Ptree| which contains most of the OCaml functions we need in \verb|Ptree| which contains most of the OCaml functions we need in
this section. this section.
\lstinputlisting{mlw_tree__buildenv.ml} \lstinputlisting{generated/mlw_tree__buildenv.ml}
To contain all the example programs we are going to build we need a To contain all the example programs we are going to build we need a
module. We start the creation of that module using the following module. We start the creation of that module using the following
declarations, that first introduces a pseudo ``file'' to hold the declarations, that first introduces a pseudo ``file'' to hold the
module, then the module itself called \verb|Program|. module, then the module itself called \verb|Program|.
\lstinputlisting{mlw_tree__openmodule.ml} \lstinputlisting{generated/mlw_tree__openmodule.ml}
Notice the use of a first Notice the use of a first
simple helper function \verb|mk_ident| to build an identifier without simple helper function \verb|mk_ident| to build an identifier without
any label nor any location. any label nor any location.
...@@ -337,39 +337,39 @@ To write our programs, we need to import some other modules from the ...@@ -337,39 +337,39 @@ To write our programs, we need to import some other modules from the
standard library. The following introduces two helper functions for standard library. The following introduces two helper functions for
building qualified identifiers and importing modules, and finally building qualified identifiers and importing modules, and finally
imports \verb|int.Int|. imports \verb|int.Int|.
\lstinputlisting{mlw_tree__useimport.ml} \lstinputlisting{generated/mlw_tree__useimport.ml}
We want now to build a program equivalent to the following code in concrete Why3 syntax. We want now to build a program equivalent to the following code in concrete Why3 syntax.
\lstinputlisting[language=why3]{mlw_tree__source1.ml} \lstinputlisting[language=why3]{generated/mlw_tree__source1.ml}
The OCaml code that programmatically build this Why3 function is as follows. The OCaml code that programmatically build this Why3 function is as follows.
\lstinputlisting{mlw_tree__code1.ml} \lstinputlisting{generated/mlw_tree__code1.ml}
This code makes uses of helper functions that are given in Figure~\ref{fig:helpers}. This code makes uses of helper functions that are given in Figure~\ref{fig:helpers}.
\begin{figure}[t] \begin{figure}[t]
\lstinputlisting{mlw_tree__helper1.ml} \lstinputlisting{generated/mlw_tree__helper1.ml}
\caption{Helper functions for building WhyML programs} \caption{Helper functions for building WhyML programs}
\label{fig:helpers} \label{fig:helpers}
\end{figure} \end{figure}
We want now to build a program equivalent to the following code in concrete Why3 syntax. We want now to build a program equivalent to the following code in concrete Why3 syntax.
\lstinputlisting[language=why3]{mlw_tree__source2.ml} \lstinputlisting[language=why3]{generated/mlw_tree__source2.ml}
We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows
\lstinputlisting{mlw_tree__code2.ml} \lstinputlisting{generated/mlw_tree__code2.ml}
The next example makes use of arrays. The next example makes use of arrays.
\lstinputlisting[language=why3]{mlw_tree__source3.ml} \lstinputlisting[language=why3]{generated/mlw_tree__source3.ml}
The corresponding OCaml code is as follows The corresponding OCaml code is as follows
\lstinputlisting{mlw_tree__code3.ml} \lstinputlisting{generated/mlw_tree__code3.ml}
Having declared all the programs we wanted to write, we can now close Having declared all the programs we wanted to write, we can now close
the module and the file, and get as a result the set of modules of our the module and the file, and get as a result the set of modules of our
file, under the form of a map of module names to modules. file, under the form of a map of module names to modules.
\lstinputlisting{mlw_tree__closemodule.ml} \lstinputlisting{generated/mlw_tree__closemodule.ml}
We can then construct the proofs tasks for our module, and then try to We can then construct the proofs tasks for our module, and then try to
call the Alt-Ergo prover. The reste of that code is using OCaml call the Alt-Ergo prover. The reste of that code is using OCaml
functions that were already introduced before. functions that were already introduced before.
\lstinputlisting{mlw_tree__checkingvcs.ml} \lstinputlisting{generated/mlw_tree__checkingvcs.ml}
%%% Local Variables: %%% Local Variables:
%%% mode: latex %%% mode: latex
......
...@@ -178,7 +178,7 @@ In the following, strings are referred to with the non-terminal ...@@ -178,7 +178,7 @@ In the following, strings are referred to with the non-terminal
uppercase identifiers and, similarly, lowercase and uppercase uppercase identifiers and, similarly, lowercase and uppercase
qualified identifiers. qualified identifiers.
\begin{center}\framebox{\input{./qualid_bnf.tex}}\end{center} \begin{center}\framebox{\input{./generated/qualid_bnf.tex}}\end{center}
\paragraph{Constants.} \paragraph{Constants.}
The syntax for constants is given in Figure~\ref{fig:bnf:constant}. The syntax for constants is given in Figure~\ref{fig:bnf:constant}.
...@@ -187,7 +187,7 @@ Integer constants may be given in base 16, 10, 8 or 2. ...@@ -187,7 +187,7 @@ Integer constants may be given in base 16, 10, 8 or 2.
Real constants may be given in base 16 or 10. Real constants may be given in base 16 or 10.
\begin{figure} \begin{figure}
\begin{center}\framebox{\input{./constant_bnf.tex}}\end{center} \begin{center}\framebox{\input{./generated/constant_bnf.tex}}\end{center}
\caption{Syntax for constants.} \caption{Syntax for constants.}
\label{fig:bnf:constant} \label{fig:bnf:constant}
\end{figure} \end{figure}
...@@ -195,7 +195,7 @@ Real constants may be given in base 16 or 10. ...@@ -195,7 +195,7 @@ Real constants may be given in base 16 or 10.
\paragraph{Operators.} \paragraph{Operators.}
Prefix and infix operators are built from characters organized in four Prefix and infix operators are built from characters organized in four
categories (\textsl{op-char-1} to \textsl{op-char-4}). categories (\textsl{op-char-1} to \textsl{op-char-4}).
\begin{center}\framebox{\input{./operator_bnf.tex}}\end{center} \begin{center}\framebox{\input{./generated/operator_bnf.tex}}\end{center}
Infix operators are classified into 4 categories, according to the Infix operators are classified into 4 categories, according to the
characters they are built from: characters they are built from:
\begin{itemize} \begin{itemize}
...@@ -211,7 +211,7 @@ characters they are built from: ...@@ -211,7 +211,7 @@ characters they are built from:
\paragraph{Labels.} Identifiers, terms, formulas, program expressions \paragraph{Labels.} Identifiers, terms, formulas, program expressions
can all be labeled, either with a string, or with a location tag. can all be labeled, either with a string, or with a location tag.
\begin{center}\framebox{\input{./label_bnf.tex}}\end{center} \begin{center}\framebox{\input{./generated/label_bnf.tex}}\end{center}
A location tag consists of a file name, a line number, and starting A location tag consists of a file name, a line number, and starting
and ending characters. and ending characters.
......
...@@ -25,7 +25,7 @@ In the following, strings are referred to with the non-terminal ...@@ -25,7 +25,7 @@ In the following, strings are referred to with the non-terminal
%\subsection{Constants} %\subsection{Constants}
The syntax for numerical constants is given by the following rules: The syntax for numerical constants is given by the following rules:
%\begin{figure}[ht] %\begin{figure}[ht]
\begin{center}\input{./constant_bnf.tex}\end{center} \begin{center}\input{./generated/constant_bnf.tex}\end{center}
%\caption{Syntax for numerical constants.} %\caption{Syntax for numerical constants.}
%\label{fig:bnf:constant} %\label{fig:bnf:constant}
%\end{figure} %\end{figure}
...@@ -42,7 +42,7 @@ The syntax distinguishes identifiers that start with a lowercase letter ...@@ -42,7 +42,7 @@ The syntax distinguishes identifiers that start with a lowercase letter
or an underscore (\nonterm{lident}{}\spacefalse) and identifiers that or an underscore (\nonterm{lident}{}\spacefalse) and identifiers that
start with an uppercase letter (\nonterm{uident}{}\spacefalse): start with an uppercase letter (\nonterm{uident}{}\spacefalse):
%\begin{figure}[ht] %\begin{figure}[ht]
\begin{center}\input{./ident_bnf.tex}\end{center} \begin{center}\input{./generated/ident_bnf.tex}\end{center}
%\caption{Syntax for identifiers.} %\caption{Syntax for identifiers.}
%\label{fig:bnf:ident} %\label{fig:bnf:ident}
%\end{figure} %\end{figure}
...@@ -56,7 +56,7 @@ Prefix and infix operators are built from characters organized in four ...@@ -56,7 +56,7 @@ Prefix and infix operators are built from characters organized in four
precedence groups (\textsl{op-char-1} to \textsl{op-char-4}): precedence groups (\textsl{op-char-1} to \textsl{op-char-4}):
%as shown in Figure~\ref{fig:bnf:operator}. %as shown in Figure~\ref{fig:bnf:operator}.
%\begin{figure}[ht] %\begin{figure}[ht]
\begin{center}\input{./operator_bnf.tex}\end{center} \begin{center}\input{./generated/operator_bnf.tex}\end{center}
%\caption{Syntax for operators.} %\caption{Syntax for operators.}
%\label{fig:bnf:operator} %\label{fig:bnf:operator}
%\end{figure} %\end{figure}
...@@ -80,7 +80,7 @@ are always recognized as bang operators. ...@@ -80,7 +80,7 @@ are always recognized as bang operators.
%Qualified identifiers are prefixed with a sequence of uppercase %Qualified identifiers are prefixed with a sequence of uppercase
%identifiers, e.g., \texttt{App.S.get}: %identifiers, e.g., \texttt{App.S.get}:
%\begin{figure}[ht] %\begin{figure}[ht]
%\begin{center}\input{./qualid_bnf.tex}\end{center} %\begin{center}\input{./generated/qualid_bnf.tex}\end{center}
%\caption{Syntax for qualified identifiers.} %\caption{Syntax for qualified identifiers.}
%\label{fig:bnf:qualid}