Commit e7fe6ce9 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

PVS output revamped (in preparation of forthcoming PVS realizations)

parent 00f2af66
......@@ -1268,13 +1268,13 @@ clean::
tags:
find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
"--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
"--regex=/and[ \t]+\([^ \t]+\)/\1/" \
"--regex=/type[ \t]+\([^ \t]+\)/\1/" \
"--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
"--regex=/val[ \t]+\([^ \t]+\)/\1/" \
"--regex=/module[ \t]+\([^ \t]+\)/\1/"
etags "--regex-ocaml=/let[ \t]+\([^ \t]+\)/\1/" \
"--regex-ocaml=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
"--regex-ocaml=/and[ \t]+\([^ \t]+\)/\1/" \
"--regex-ocaml=/type[ \t]+\([^ \t]+\)/\1/" \
"--regex-ocaml=/exception[ \t]+\([^ \t]+\)/\1/" \
"--regex-ocaml=/val[ \t]+\([^ \t]+\)/\1/" \
"--regex-ocaml=/module[ \t]+\([^ \t]+\)/\1/"
otags:
find \( -name '*.ml' -or -name '*.mli' \) -print0 | xargs -0 otags
......
\chapter{Theory Realizations}
\label{chap:realizations}
Given a \why theory, one can use a proof assistant to make a
\emph{realization} of this theory, that is to provide definitions for
some of its uninterpreted symbols and proofs for some of its
axioms. This way, one can show the consistency of some axiomatized
theory and/or make a connection to an existing library (of the proof
assistant) to ease some proofs.
Currently, realizations are supported for the proof assistants Coq and PVS.
\section{Generating a realization}
Generating the skeleton for a theory is done by passing to \why the
......@@ -8,7 +16,7 @@ Generating the skeleton for a theory is done by passing to \why the
the theories to realize, and the target directory.
\begin{verbatim}
why3 --realize -D path/to/drivers/coq-realize.drv
why3 --realize -D path/to/drivers/prover-realize.drv
-T env_path.theory_name -o path/to/target/dir/
\end{verbatim}
......@@ -41,7 +49,9 @@ 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}
\section{Generated/edited files}
\subsection{Coq}
This section describes the content of the Coq files generated by \why for
both proof obligations and theory realizations. When reading a Coq
......@@ -79,6 +89,10 @@ much about comments. For instance, \why can easily be confused by
some terminating directive like \verb+Qed+ that would be present in a
comment.
\subsection{PVS}
TODO
\section{Shipping libraries of realizations}
While modifying an existing driver file might be sufficient for local
......
......@@ -4,7 +4,7 @@ unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "inline_trivial"
(*transformation "inline_trivial"*)
transformation "eliminate_builtin"
(* PVS does not support mutual recursion *)
......@@ -71,10 +71,10 @@ theory int.Int
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (-_) "(-%1)"
syntax function ( + ) "(%1 + %2)"
syntax function ( - ) "(%1 - %2)"
syntax function ( * ) "(%1 * %2)"
syntax function (-_) "(-%1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
......@@ -157,12 +157,12 @@ theory real.Real
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (-_) "(-%1)"
syntax function (*) "(%1 * %2)"
syntax function (/) "(%1 / %2)"
syntax function inv "(1 / %1)"
syntax function ( + ) "(%1 + %2)"
syntax function ( - ) "(%1 - %2)"
syntax function (-_) "(-%1)"
syntax function ( * ) "(%1 * %2)"
syntax function ( / ) "(%1 / %2)"
syntax function inv "(1 / %1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
......
(*
prelude "% This file is generated by Why3's PVS driver"
prelude "% Beware! Only edit allowed sections below "
*)
printer "pvs-realize"
filename "%t.pvs"
import "pvs-common.gen"
(*
prelude "% This file is generated by Why3's PVS driver"
prelude "% Beware! Only edit allowed sections below "
*)
printer "pvs"
filename "%f_%t_%g.pvs"
......
......@@ -322,18 +322,19 @@ command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3
driver = "drivers/coq.drv"
editor = "coqide"
# [ITP pvs]
# name = "PVS"
# exec = "pvs"
# version_switch = "-version"
# version_regexp = "PVS Version \\([^ \n]+\\)"
# version_ok = "5.0"
# command = "'@LOCALBIN@why3-cpulimit' 0 %m -s proveit %f"
# driver = "drivers/pvs.drv"
# editor = "pvs"
[ITP pvs]
name = "PVS"
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
version_ok = "5.0"
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s proveit %f"
driver = "drivers/pvs.drv"
editor = "pvs"
# [editor pvs]
# command = "pvs %f"
[editor pvs]
name = "PVS"
command = "pvs %f"
[editor coqide]
name = "CoqIDE"
......
......@@ -199,6 +199,6 @@ let () =
try
main ()
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
eprintf "Error: %a@." Exn_printer.exn_printer e;
exit 1
......@@ -91,6 +91,10 @@ let black_list =
(* introduced by Why3 *)
"tuple0"; ]
let fresh_printer () =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer black_list ~sanitizer:isanitize
let iprinter =
let isanitize = sanitizer char_to_lalpha char_to_lalnumus in
create_ident_printer black_list ~sanitizer:isanitize
......@@ -137,11 +141,14 @@ let print_ls fmt ls =
let print_pr fmt pr =
fprintf fmt "%s" (id_unique iprinter pr.pr_name)
let print_name fmt id =
fprintf fmt "%% Why3 %s@\n" (id_unique iprinter id)
(* info *)
type info = {
info_syn : syntax_map;
symbol_printers : (Theory.theory * ident_printer) Mid.t;
symbol_printers : (string * Theory.theory * ident_printer) Mid.t;
realization : bool;
}
......@@ -150,9 +157,9 @@ let print_path = print_list (constant_string ".") string
let print_id fmt id = string fmt (id_unique iprinter id)
let print_id_real info fmt id =
try let th,ipr = Mid.find id info.symbol_printers in
fprintf fmt "%a.%s.%s"
print_path th.Theory.th_path
try let path,th,ipr = Mid.find id info.symbol_printers in
fprintf fmt "%s.%s.%s"
path
th.Theory.th_name.id_string
(id_unique ipr id)
with Not_found -> print_id fmt id
......@@ -474,6 +481,7 @@ let clean_line s =
let n = String.length s in
if n >= 2 && s.[0] = ' ' && s.[1] = ' ' then String.sub s 2 (n - 2) else s
(***
let copy_user_script begin_string end_string ch fmt =
fprintf fmt "%s@\n" begin_string;
try
......@@ -517,151 +525,132 @@ let lookup_context_or_proof old_state old_channel =
try loop ()
with End_of_file -> ()
let print_empty_context fmt =
fprintf fmt "%s@\n" context_begin;
fprintf fmt "@\n";
fprintf fmt "%s@\n@\n" context_end
let print_empty_proof ?(def=false) fmt =
fprintf fmt "%s@\n" proof_begin;
if not def then fprintf fmt "intuition.@\n";
fprintf fmt "@\n";
fprintf fmt "%s.@\n" (if def then "Defined" else "Qed");
fprintf fmt "%s@\n@\n" proof_end
(*
let print_next_proof ?def ch fmt =
try
while true do
let s = input_line ch in
if s = proof_begin then
begin
fprintf fmt "%s@\n" proof_begin;
while true do
let s = input_line ch in
fprintf fmt "%s@\n" s;
if s = proof_end then raise Exit
done
end
done
with
| End_of_file -> print_empty_proof ?def fmt
| Exit -> fprintf fmt "@\n"
*)
let print_context ~old fmt =
match old with
| None -> print_empty_context fmt
| Some(s,ch) ->
lookup_context_or_proof s ch;
match !s with
| InProof | NoWhere -> print_empty_context fmt
| InContext -> copy_context s ch fmt
let print_proof ~old ?def fmt =
match old with
| None ->
print_empty_proof ?def fmt
| Some(s, ch) ->
lookup_context_or_proof s ch;
match !s with
| InContext | NoWhere -> print_empty_proof ?def fmt
| InProof -> copy_proof s ch fmt
let produce_remaining_contexts_and_proofs ~old fmt =
match old with
| None -> ()
| Some(s,ch) ->
let rec loop () =
lookup_context_or_proof s ch;
match !s with
| NoWhere -> ()
| InContext -> copy_context s ch fmt; loop ()
| InProof -> copy_proof s ch fmt; loop ()
in
loop ()
let read_old_script _ch =
[]
****)
type chunk =
| Edition of string * string (* name and contents *)
| Other of string (* contents *)
let re_theory = Str.regexp "[^ :]+: THEORY"
let re_begin = Str.regexp " BEGIN"
let re_why3 = Str.regexp "% Why3 \\([^ ]+\\)"
let read_old_script ch =
let chunks = ref [] in
let buffer = Buffer.create 1024 in
let rec read_line () =
let s = input_line ch in
let s = clean_line s in
if Str.string_match re_theory s 0 || Str.string_match re_begin s 0
then read_line () else s
in
let rec read ?name () =
let s = read_line () in
if s = "" then begin
new_chunk ?name (); read ()
end else if Str.string_match re_why3 s 0 then begin
new_chunk ?name ();
let name = Str.matched_group 1 s in
read ~name ()
end else begin
if Buffer.length buffer > 0 then Buffer.add_string buffer "\n ";
Buffer.add_string buffer s;
read ?name ()
end
and new_chunk ?name () =
let s = Buffer.contents buffer in
Buffer.clear buffer;
match s, name with
| "", _ | _, Some "tuple0" -> ()
| _, None -> chunks := Other s :: !chunks
| _, Some n -> chunks := Edition (n, s) :: !chunks
in
try read () with End_of_file -> List.rev !chunks
(* note: the very last chunk is purposely ignored, as it is "END th" *)
(* Output all the Other entries of the script that occur before the
location of name. Modify the script by removing the name entry and all
these outputs. Return the user content. *)
let output_till_statement fmt script name =
let print i =
let rec aux acc = function
| h :: l when h == i ->
let l = match l with Other "" :: l -> l | _ -> l in
script := List.rev_append acc l
| Other o :: l -> fprintf fmt "%s@\n@\n" o; aux acc l
| h :: l -> aux (h :: acc) l
| [] -> assert false
in
aux [] !script
in
let rec find = function
| Edition (n,_) as o :: _ when n = name -> print o; Some o
| [] -> None
| _ :: t -> find t
in
find !script
(*
let produce_remaining_proofs ~old fmt =
match old with
| None -> ()
| Some ch ->
try
while true do
let s = input_line ch in
if s = proof_begin then
begin
fprintf fmt "(* OBSOLETE PROOF *)@\n";
try while true do
let s = input_line ch in
if s = proof_end then
begin
fprintf fmt "(* END OF OBSOLETE PROOF *)@\n@\n";
raise Exit
end;
fprintf fmt "%s@\n" s;
done
with Exit -> ()
end
done
with
| End_of_file -> fprintf fmt "@\n"
*)
let comment_out s =
Str.global_replace (Str.regexp "\n") "\n % " s
let realization ~old ?def fmt produce_realization =
if produce_realization then
print_proof ~old ?def fmt
(*
begin match old with
| None -> print_empty_proof ?def fmt
| Some ch -> print_next_proof ?def ch fmt
end
*)
else
fprintf fmt "@\n"
let output_remaining fmt cl =
let print = function
| Edition (n, c) ->
fprintf fmt "%% Obsolete chunk %s@\n%% %s@\n" n (comment_out c)
| Other c ->
fprintf fmt "%% %s@\n" (comment_out c)
in
List.iter print cl
let print_type_decl ~old info fmt ts =
if is_ts_tuple ts then () else
match ts.ts_def with
let print_type_decl ~prev info fmt ts = ignore (prev);
if not (is_ts_tuple ts) then begin
print_name fmt ts.ts_name;
match ts.ts_def with
| None ->
fprintf fmt "@[<hov 2>%a%a: TYPE@]@\n%a"
fprintf fmt "@[<hov 2>%a%a: TYPE@]@\n@\n"
print_ts ts print_params_list ts.ts_args
(realization ~old ~def:true) info.realization
(* (realization ~old ~def:true) info.realization *)
| Some ty ->
fprintf fmt "@[<hov 2>%a%a: TYPE =@ %a@]@\n@\n"
print_ts ts print_params_list ts.ts_args
(print_ty info) ty
end
let print_type_decl ~old info fmt ts =
if not (Mid.mem ts.ts_name info.info_syn) then
(print_type_decl ~old info fmt ts; forget_tvs ())
let print_type_decl ~prev info fmt ts =
if not (Mid.mem ts.ts_name info.info_syn) then begin
print_type_decl ~prev info fmt ts;
forget_tvs ()
end
let print_data_decl info fmt (ts,csl) =
if is_ts_tuple ts then () else
fprintf fmt
"@[<hov 1>%a%a: DATATYPE@\n@[<hov 1>BEGIN@\n%a@]@\nEND %a@]@\n@\n"
print_ts ts print_params_list ts.ts_args
(print_list newline (print_constr info ts)) csl
print_ts ts
if not (is_ts_tuple ts) then begin
print_name fmt ts.ts_name;
fprintf fmt
"@[<hov 1>%a%a: DATATYPE@\n@[<hov 1>BEGIN@\n%a@]@\nEND %a@]@\n@\n"
print_ts ts print_params_list ts.ts_args
(print_list newline (print_constr info ts)) csl print_ts ts
end
let print_data_decl info fmt d =
if not (Mid.mem (fst d).ts_name info.info_syn) then
(print_data_decl info fmt d; forget_tvs ())
let print_ls_type info fmt ls =
begin match ls with
| None -> fprintf fmt "bool"
| Some ty -> print_ty info fmt ty
if not (Mid.mem (fst d).ts_name info.info_syn) then begin
print_data_decl info fmt d;
forget_tvs ()
end
let print_param_decl ~old info fmt ls =
ignore old;
let print_ls_type info fmt = function
| None -> fprintf fmt "bool"
| Some ty -> print_ty info fmt ty
let print_param_decl ~prev info fmt ls =
ignore prev;
let _ty_vars_args, _ty_vars_value, all_ty_params = ls_ty_vars ls in
print_name fmt ls.ls_name;
match ls.ls_args with
| [] ->
fprintf fmt "@[<hov 2>%a%a: %a@]@\n@\n"
print_ls ls
print_params all_ty_params
print_ls ls print_params all_ty_params
(print_ls_type info) ls.ls_value
| _ ->
fprintf fmt "@[<hov 2>%a%a: [%a -> %a]@]@\n@\n"
......@@ -670,14 +659,15 @@ let print_param_decl ~old info fmt ls =
(print_ls_type info) ls.ls_value
(* (realization ~old ~def:true) info.realization *)
let print_param_decl ~old info fmt ls =
let print_param_decl ~prev info fmt ls =
if not (Mid.mem ls.ls_name info.info_syn) then
(print_param_decl ~old info fmt ls; forget_tvs ())
(print_param_decl ~prev info fmt ls; forget_tvs ())
let print_logic_decl ~old info fmt (ls,ld) =
ignore old;
let print_logic_decl ~prev info fmt (ls,ld) =
ignore prev;
let _ty_vars_args, _ty_vars_value, all_ty_params = ls_ty_vars ls in
let vl,e = open_ls_defn ld in
print_name fmt ls.ls_name;
fprintf fmt "@[<hov 2>%a%a(%a): %a =@ %a@]@\n@\n"
print_ls ls print_params all_ty_params
(print_comma_list (print_vsty_nopar info)) vl
......@@ -685,15 +675,16 @@ let print_logic_decl ~old info fmt (ls,ld) =
(print_expr info) e;
List.iter forget_var vl
let print_logic_decl ~old info fmt d =
let print_logic_decl ~prev info fmt d =
if not (Mid.mem (fst d).ls_name info.info_syn) then
(print_logic_decl ~old info fmt d; forget_tvs ())
(print_logic_decl ~prev info fmt d; forget_tvs ())
let print_recursive_decl info fmt (ls,ld) =
let _, _, all_ty_params = ls_ty_vars ls in
let i = match Decl.ls_defn_decrease ld with
| [i] -> i | _ -> assert false in
let vl,e = open_ls_defn ld in
print_name fmt ls.ls_name;
fprintf fmt "@[<hov 2>%a%a(%a): RECURSIVE %a =@ %a@\n"
print_ls ls print_params all_ty_params
(print_comma_list (print_vsty_nopar info)) vl
......@@ -722,6 +713,7 @@ let print_ind_decl info fmt (ps,al) =
let vl = List.map (create_vsymbol (id_fresh "z")) ps.ls_args in
let tl = List.map t_var vl in
let dj = Util.map_join_left (Eliminate_inductive.exi tl) t_or al in
print_name fmt ps.ls_name;
fprintf fmt "@[<hov 2>%a%a(%a): INDUCTIVE bool =@ @[<hov>%a@]@]@\n"
print_ls ps print_params all_ty_params
(print_comma_list (print_vsty_nopar info)) vl
......@@ -739,46 +731,56 @@ let print_pkind info fmt = function
| Pgoal -> fprintf fmt "THEOREM"
| Pskip -> assert false (* impossible *)
let print_proof ~old info fmt = function
| Plemma | Pgoal ->
realization ~old fmt true
| Paxiom ->
realization ~old fmt info.realization
| Pskip -> ()
let print_proof_context ~old info fmt = function
| Plemma | Pgoal ->
print_context ~old fmt
| Paxiom ->
if info.realization then print_context ~old fmt
| Pskip -> ()
let print_decl ~old info fmt d = match d.d_node with
let print_prop_decl 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 -> ""
| 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;
forget_tvs ()
let print_decl ~old info fmt d =
let name = match d.d_node with
| Dtype ts
| Ddata ((ts, _) :: _) -> id_unique iprinter ts.ts_name
| Dparam ls
| Dlogic ((ls, _) :: _)
| Dind (_, (ls,_) :: _) -> id_unique iprinter ls.ls_name
| Dprop (_, pr, _) -> id_unique iprinter pr.pr_name
| Ddata []
| Dlogic []
| Dind (_, []) -> assert false in
let prev = output_till_statement fmt old name in
match d.d_node with
| Dtype ts ->
print_type_decl ~old info fmt ts
print_type_decl ~prev info fmt ts
| Ddata tl ->
print_list nothing (print_data_decl info) fmt tl
| Dparam ls ->
print_param_decl ~old info fmt ls
print_param_decl ~prev info fmt ls
| Dlogic [s, _ as ld] when not (Sid.mem s.ls_name d.d_syms) ->
print_logic_decl ~old info fmt ld
print_logic_decl ~prev info fmt ld
| Dlogic ll ->
print_recursive_decl info fmt ll
| Dind (Ind, il) ->
print_list nothing (print_ind_decl info) fmt il
| Dind (Coind, _) ->
unsupportedDecl d
"PVS: coinductive definitions are not supported"
unsupportedDecl d "PVS: coinductive definitions are not supported"
| Dprop (_, pr, _) when Mid.mem pr.pr_name info.info_syn ->
()
| Dprop (k, pr, f) ->
print_proof_context ~old info fmt k;
let params = t_ty_freevars Stv.empty f in
fprintf fmt "@[<hov 2>%a%a: %a %a@]@\n@\n"
print_pr pr print_params params
(print_pkind info) k
(print_fmla info) f (* (print_proof ~old info) k *);
forget_tvs ()
| Dprop pr ->
print_prop_decl info fmt pr
let print_decls ~old info fmt dl =
fprintf fmt "@[<hov>%a@]" (print_list nothing (print_decl ~old info)) dl
......@@ -789,60 +791,62 @@ let init_printer th =
Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
pr
(* TODO: add a driver meta and make lookup for realized theories a bit
more efficient *)
let realized_theories = []
let print_task _env pr thpr realize ?old fmt task =
let print_task env pr thpr realize ?old fmt task =
forget_all ();
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let symbol_printers,decls =
let used = Task.used_theories task in