Commit 7249b10c authored by MARCHE Claude's avatar MARCHE Claude

doc, API tutorial: ensure consistency with real code using automatic extraction

parent fa011cd3
......@@ -1822,13 +1822,24 @@ doc/bnf$(EXE): doc/bnf.mll
$(OCAMLLEX) $<
$(OCAMLC) -o $@ doc/bnf.ml
doc/logic_%.ml: examples/use_api/logic.ml doc/extract_ocaml_code
doc/extract_ocaml_code examples/use_api/logic.ml $* doc
OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \
buildtask printtask buildtask2
OCAMLCODE = $(addprefix doc/logic_, $(addsuffix .ml, $(OCAMLCODE_LOGIC)))
doc/extract_ocaml_code: doc/extract_ocaml_code.ml
$(OCAMLC) str.cma -o $@ $<
DOC = api glossary ide intro exec macros manpages install \
manual starting syntax syntaxref technical version whyml \
itp pvs coq coq_tactic isabelle
DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib share/provers-detection-data.conf
doc/manual.pdf: $(BNFTEX) $(OCAMLCODE) $(DOCTEX) doc/manual.bib share/provers-detection-data.conf
cd doc; $(RUBBER) --warn all --pdf manual.tex
CLEANDIRS += doc
......
......@@ -16,6 +16,7 @@ Section~\ref{sec:installlib}. The OCaml code given below is available in
the source distribution in directory \verb|examples/use_api/| together
with a few other examples.
\lstset{language={[Objective]Caml}}
\section{Building Propositional Formulas}
......@@ -23,15 +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
a piece of OCaml code for building the formula $\mathit{true} \lor
\mathit{false}$.
\begin{ocamlcode}
(* opening the Why3 library *)
open Why3
(* a ground propositional goal: true or false *)
let fmla_true : Term.term = Term.t_true
let fmla_false : Term.term = Term.t_false
let fmla1 : Term.term = Term.t_or fmla_true fmla_false
\end{ocamlcode}
\lstinputlisting{logic_opening.ml}
The library uses the common type \texttt{term} both for terms
(\ie expressions that produce a value of some particular type)
and formulas (\ie boolean-valued expressions).
......@@ -42,17 +35,12 @@ and formulas (\ie boolean-valued expressions).
Such a formula can be printed using the module \texttt{Pretty}
providing pretty-printers.
\begin{ocamlcode}
(* printing it *)
open Format
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1
\end{ocamlcode}
\lstinputlisting{logic_printformula.ml}
Assuming the lines above are written in a file \texttt{f.ml}, it can
be compiled using
\begin{verbatim}
ocamlc str.cma unix.cma nums.cma dynlink.cma \
-I +ocamlgraph -I +why3 graph.cma why.cma f.ml -o f
ocamlfind ocamlc -package why3 f.ml -o f
\end{verbatim}
Running the generated executable \texttt{f} results in the following output.
\begin{verbatim}
......@@ -62,23 +50,12 @@ formula 1 is: true \/ false
Let us now build a formula with propositional variables: $A \land B
\rightarrow A$. Propositional variables must be declared first before
using them in formulas. This is done as follows.
\begin{ocamlcode}
let prop_var_A : Term.lsymbol =
Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol =
Term.create_psymbol (Ident.id_fresh "B") []
\end{ocamlcode}
\lstinputlisting{logic_declarepropvars.ml}
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
by the general function for applying a predicate symbol to a list of terms.
Here we just need the empty list of arguments.
\begin{ocamlcode}
let atom_A : Term.term = Term.ps_app prop_var_A []
let atom_B : Term.term = Term.ps_app prop_var_B []
let fmla2 : Term.term =
Term.t_implies (Term.t_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
\end{ocamlcode}
\lstinputlisting{logic_declarepropatoms.ml}
As expected, the output is as follows.
\begin{verbatim}
......@@ -97,13 +74,7 @@ tasks from our formulas. Task can be build incrementally from an empty
task by adding declaration to it, using the functions
\texttt{add\_*\_decl} of module \texttt{Task}. For the formula $\mathit{true} \lor
\mathit{false}$ above, this is done as follows.
\begin{ocamlcode}
let task1 : Task.task = None (* empty task *)
let goal_id1 : Decl.prsymbol =
Decl.create_prsymbol (Ident.id_fresh "goal1")
let task1 : Task.task =
Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
\end{ocamlcode}
\lstinputlisting{logic_buildtask.ml}
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
propositions in a theory or a task. Notice again that the concrete
......@@ -115,23 +86,12 @@ Notice that lemmas are not allowed in tasks
and can only be used in theories.
Once a task is built, it can be printed.
\begin{ocamlcode}
(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
\end{ocamlcode}
\lstinputlisting{logic_printtask.ml}
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)
propositional symbols in the task.
\begin{ocamlcode}
(* task for formula 2 *)
let task2 = None
let task2 = Task.add_param_decl task2 prop_var_A
let task2 = Task.add_param_decl task2 prop_var_B
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
let () = printf "@[task 2 is:@\n%a@]@." Pretty.print_task task2
\end{ocamlcode}
\lstinputlisting{logic_buildtask2.ml}
Execution of our OCaml program now outputs:
\begin{verbatim}
......
(*
Simple utility to extract a portion of a file
extract_ocaml_code <path/file.ext> <id> <dir>
extracts the part of path/file.ext between lines containing anchors BEGIN{id} and END{id}
and puts the result in the file dir/file_id.ext
*)
open Format
let filename,section,output_dir =
if Array.length Sys.argv = 4 then
Sys.argv.(1), Sys.argv.(2), Sys.argv.(3)
else
begin
eprintf "Usage: %s <path/file.ext> <id> <dir>@\n\
Extract the part of path/file.ext between lines containing anchors BEGIN{id} and END{id}@\n\
and puts the result in the file dir/file_id.ext@."
Sys.argv.(0);
exit 2
end
let ch_in =
try
open_in filename
with
exn ->
eprintf "Cannot open %s for reading: %s@." filename (Printexc.to_string exn);
exit 1
let basename = Filename.basename filename
let ext = Filename.extension basename
let basename = Filename.remove_extension basename
let begin_re = Str.regexp_string ("BEGIN{" ^ section ^ "}")
let search_begin () =
try
while true do
let l = input_line ch_in in
try
let _ = Str.search_forward begin_re l 0 in raise Exit
with Not_found -> ()
done
with
End_of_file ->
eprintf "Error: opening anchor BEGIN{%s} not found in file %s@." section filename;
close_in ch_in;
exit 1
| Exit -> ()
let end_re = Str.regexp_string ("END{" ^ section ^ "}")
let file_out = Filename.concat output_dir (basename ^ "_" ^ section ^ ext)
let ch_out =
try
open_out file_out
with
exn ->
eprintf "Cannot open %s for writing: %s@." file_out (Printexc.to_string exn);
close_in ch_in;
exit 1
let search_end () =
try
while true do
let l = input_line ch_in in
try
let _ = Str.search_forward end_re l 0 in raise Exit
with Not_found ->
output_string ch_out l;
output_char ch_out '\n'
done
with
End_of_file ->
eprintf "Error: ending anchor END{%s} not found in file %s@." section filename;
close_in ch_in;
close_out ch_out;
exit 1
| Exit ->
close_in ch_in;
close_out ch_out
let () =
search_begin (); search_end ()
......@@ -14,8 +14,11 @@
This file builds some goals using the API and calls
the alt-ergo prover to check them
Note: the comments of the form BEGIN{id} and END{id} are there for automatic extraction
of the chapter "The Why3 API" of the manual
******************)
(* BEGIN{opening} *)
(* opening the Why3 library *)
open Why3
......@@ -23,38 +26,52 @@ open Why3
let fmla_true : Term.term = Term.t_true
let fmla_false : Term.term = Term.t_false
let fmla1 : Term.term = Term.t_or fmla_true fmla_false
(* END{opening} *)
(* BEGIN{printformula} *)
(* printing it *)
open Format
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1
(* END{printformula} *)
(* a propositional goal: A and B implies A *)
let prop_var_A : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "B") []
(* BEGIN{declarepropvars} *)
let prop_var_A : Term.lsymbol =
Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol =
Term.create_psymbol (Ident.id_fresh "B") []
(* END{declarepropvars} *)
(* BEGIN{declarepropatoms} *)
let atom_A : Term.term = Term.ps_app prop_var_A []
let atom_B : Term.term = Term.ps_app prop_var_B []
let fmla2 : Term.term = Term.t_implies (Term.t_and atom_A atom_B) atom_A
let fmla2 : Term.term =
Term.t_implies (Term.t_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
(* END{declarepropatoms} *)
(* BEGIN{buildtask} *)
(* building the task for formula 1 alone *)
let task1 : Task.task = None (* empty task *)
let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1")
let task1 : Task.task = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
(* END{buildtask} *)
(* BEGIN{printtask} *)
(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
(* END{printtask} *)
(* BEGIN{buildtask2} *)
(* task for formula 2 *)
let task2 = None
let task2 = Task.add_param_decl task2 prop_var_A
let task2 = Task.add_param_decl task2 prop_var_B
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2
(* END{buildtask2} *)
......
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