Commit 04fe976c authored by Jean-Christophe's avatar Jean-Christophe

PVS: realizations in progress

parent fd09599e
......@@ -13,37 +13,35 @@ Currently, realizations are supported for the proof assistants Coq and PVS.
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.
the theories to realize, and a target directory.
\begin{verbatim}
why3 --realize -D path/to/drivers/prover-realize.drv
-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
extracts all the parts that it assumes to be user-edited and merges them in
the generated file.
Note that \why does not track dependencies between realizations and
theories, so a realization will become outdated if a theory is modified.
It is up to the user to handle such dependencies, for instance by adding
a Makefile rule.
theories, so a realization will become outdated if the corresponding
theory is modified.
It is up to the user to handle such dependencies, for instance using a
\texttt{Makefile}.
\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.
If a theory has been realized, the \why printer for the corresponding prover
will no longer output declarations for that theory but instead simply put
a directive to load the realization. In order to tell the printer
that a given theory is realized, one has to add a meta declaration in the
corresponding theory section of the driver.
\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
......@@ -91,7 +89,40 @@ comment.
\subsection{PVS}
TODO
When a PVS file is regenerated, the old version is split into chunks,
according to blank lines. Chunks corresponding to \why declarations
are identified with a comment starting with \verb+% Why3+, \eg
\begin{verbatim}
% Why3 f
f(x: int) : int
\end{verbatim}
Other chunks are considered to be user PVS declarations.
Thus a comment such as \verb+% Why3 f+ must not be removed;
otherwise, there will be two
declarations for \texttt{f} in the next version of the file (one being
regenerated and another one considered to be a user-edited chunk).
The user is allowed to perform the following actions on a PVS
realization:
\begin{itemize}
\item give a definition to an uninterpreted symbol (type, function, or
predicate symbol), by adding an equal sign (\texttt{=}) and a
right-hand side to the definition. When the declaration is
regenerated, the left-hand side is updated and the right-hand side
is reprinted as is. In particular, the names of a function or
predicate arguments should not be modified. In addition, the
\texttt{MACRO} keyword may be inserted and it will be kept in
further generations.
\item turn an axiom into a lemma, that is to replace the PVS keyword
\texttt{AXIOM} with either \texttt{LEMMA} or \texttt{THEOREM}.
\item insert anything between generated declarations, such as a lemma,
an extra definition for the purpose of a proof, etc.
\end{itemize}
\why makes some effort to merge the new declarations with the old ones
and with the user chunks. If it happens that some chunks could not be
merged, they are appended at the end of the file, in comments.
\section{Shipping libraries of realizations}
......
......@@ -57,10 +57,6 @@ TODO
* driver
- maps: const
* MACRO
* AXIOM -> LEMMA
*)
open Format
......@@ -649,14 +645,22 @@ let print_arguments info fmt = function
| [] -> ()
| vl -> fprintf fmt "(%a)" (print_comma_list (print_vsty_nopar info)) vl
let re_macro = Str.regexp "\\bMACRO\\b"
let has_macro s =
try let _ = Str.search_forward re_macro s 0 in true with Not_found -> false
let is_macro info fmt = function
| Some (Edition (_, c)) when info.realization && List.exists has_macro c ->
fprintf fmt "MACRO "
| _ -> ()
let print_param_decl ~prev info fmt ls =
ignore prev;
let _, _, all_ty_params = ls_ty_vars ls in
let vl = List.map create_argument ls.ls_args in
print_name fmt ls.ls_name;
fprintf fmt "@[<hov 2>%a%a%a: %a"
print_ls ls print_params all_ty_params
(print_arguments info) vl (print_ls_type info) ls.ls_value;
fprintf fmt "@[<hov 2>%a%a%a: %a%a"
print_ls ls print_params all_ty_params (print_arguments info) vl
(is_macro info) prev (print_ls_type info) ls.ls_value;
realization fmt info prev;
List.iter forget_var vl;
fprintf fmt "@]@\n@\n"
......@@ -713,30 +717,27 @@ let print_ind_decl info fmt d =
if not (Mid.mem (fst d).ls_name info.info_syn) then
(print_ind_decl info fmt d; forget_tvs ())
let print_pkind info fmt = function
| Paxiom when info.realization -> fprintf fmt "LEMMA"
| Paxiom -> fprintf fmt "AXIOM"
| Plemma -> fprintf fmt "LEMMA"
| Pgoal -> fprintf fmt "THEOREM"
| Pskip -> assert false (* impossible *)
let print_prop_decl info fmt (k,pr,f) =
let re_lemma = Str.regexp "\\(\\bLEMMA\\b\\|\\bTHEOREM\\b\\)"
let rec find_lemma = function
| [] -> "AXIOM"
| s :: sl ->
(try let _ = Str.search_forward re_lemma s 0 in Str.matched_group 1 s
with Not_found -> find_lemma sl)
let axiom_or_lemma = function
| Some (Edition (_, c)) -> find_lemma c
| _ -> "AXIOM"
let print_prop_decl ~prev info fmt (k,pr,f) =
let params = t_ty_freevars Stv.empty f in
let stt = match k with
| Paxiom when info.realization -> "LEMMA"
| Paxiom -> ""
let kind = match k with
| Paxiom when info.realization -> axiom_or_lemma prev
| Paxiom -> "AXIOM"
| Plemma -> "LEMMA"
| Pgoal -> "THEOREM"
| Pskip -> assert false (* impossible *) in
print_name fmt pr.pr_name;
if stt <> "" then
fprintf fmt "@[<hov 2>%a%a: %s %a@]@\n@\n"
print_pr pr print_params params stt
(print_fmla info) f
else
fprintf fmt "@[<hov 2>%a%a: %a %a@]@\n@\n"
print_pr pr print_params params (print_pkind info) k
(print_fmla info) f;
fprintf fmt "@[<hov 2>%a%a: %s %a@]@\n@\n"
print_pr pr print_params params kind (print_fmla info) f;
forget_tvs ()
let print_decl ~old info fmt d =
......@@ -771,7 +772,7 @@ let print_decl ~old info fmt d =
| Dprop (_, pr, _) when Mid.mem pr.pr_name info.info_syn ->
()
| Dprop pr ->
print_prop_decl info fmt pr
print_prop_decl ~prev info fmt pr
let print_decls ~old info fmt dl =
fprintf fmt "@[<hov>%a@]" (print_list nothing (print_decl ~old info)) dl
......@@ -804,8 +805,13 @@ let print_task env pr thpr realize ?old fmt task =
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
id_unique iprinter th.Theory.th_name,
Mid.remove th.Theory.th_name realized_theories
| _ ->
"goal", realized_theories
| Some { Task.task_decl = { Theory.td_node = td } } ->
let name = match td with
| Theory.Decl { Decl.d_node = Dprop (_, pr, _) } ->
pr.pr_name.id_string
| _ -> "goal"
in
name, realized_theories
in
let realized_theories' =
Mid.map (fun (th,s) -> fprintf fmt "IMPORTING %a.%s@\n"
......
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