Commit c81517a0 authored by Jean-Christophe's avatar Jean-Christophe

PVS output: a much better use of PVS prelude

side-effect: function syntax in driver now accepts %v0, %v1, etc.
for type variable instantiations (order is given by variable name)
parent 14b28b60
......@@ -976,6 +976,10 @@ PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES))
PVSLIBS_REAL_FILES = Abs FromInt MinMax Real # ExpLog Square RealInfix
PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES))
PVSLIBS_LIST_FILES =
# List Length
PVSLIBS_LIST = $(addprefix lib/pvs/int/, $(PVSLIBS_LIST_FILES))
PVSLIBS_NUMBER_FILES = # Divisibility Gcd Parity Prime
PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES))
......@@ -985,7 +989,8 @@ PVSLIBS_FP_ALL_FILES = GenFloat $(PVSLIBS_FP_FILES)
PVSLIBS_FP = $(addprefix lib/pvs/floating_point/, $(PVSLIBS_FP_ALL_FILES))
endif
PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_NUMBER) $(PVSLIBS_FP)
PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_LIST) \
$(PVSLIBS_NUMBER) $(PVSLIBS_FP)
drivers/pvs-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
......@@ -994,6 +999,8 @@ drivers/pvs-realizations.aux: Makefile
echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done; \
for f in $(PVSLIBS_REAL_FILES); do \
echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done; \
for f in $(PVSLIBS_LIST_FILES); do \
echo 'theory list.'"$$f"' meta "realized" "list.'"$$f"'", "" end'; done; \
for f in $(PVSLIBS_NUMBER_FILES); do \
echo 'theory number.'"$$f"' meta "realized" "number.'"$$f"'", "" end'; done; \
for f in $(PVSLIBS_FP_FILES); do \
......@@ -1005,6 +1012,8 @@ install_no_local::
cp $(PVSLIBS_INT) $(LIBDIR)/why3/pvs/int/
mkdir -p $(LIBDIR)/why3/pvs/real
cp $(PVSLIBS_REAL) $(LIBDIR)/why3/pvs/real/
mkdir -p $(LIBDIR)/why3/pvs/list
cp $(PVSLIBS_LIST) $(LIBDIR)/why3/pvs/list/
mkdir -p $(LIBDIR)/why3/pvs/number
cp $(PVSLIBS_NUMBER) $(LIBDIR)/why3/pvs/number/
ifeq (@enable_pvs_fp_libs@,yes)
......@@ -1018,6 +1027,7 @@ install_local: drivers/pvs-realizations.aux
update-pvs: bin/why3 drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
for f in $(PVSLIBS_LIST_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
for f in $(PVSLIBS_NUMBER_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
for f in $(PVSLIBS_FP_FILES); do bin/why3 --realize -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
......
......@@ -469,14 +469,21 @@ else
PVSVERSION=`$PVS -version | sed -n -e 's|.*Version* *\([[^ ]]*\)$|\1|p' `
case $PVSVERSION in
6.0)
enable_pvs_support=yes
AC_MSG_RESULT($PVSVERSION)
;;
5.0)
enable_pvs_support=yes
AC_MSG_RESULT($PVSVERSION)
enable_pvs_libs=no
AC_MSG_WARN(No PVS realizations)
reason_pvs_libs="(requires version 6.0 or higher)"
;;
*)
enable_pvs_support=no
AC_MSG_WARN(You need PVS 5.0 or later; PVS discarded)
reason_pvs_support=" (need version 5.0 or later)"
AC_MSG_WARN(You need PVS 5.0 or higher; PVS discarded)
reason_pvs_support=" (need version 5.0 or higher)"
;;
esac
fi
......
......@@ -34,18 +34,16 @@ theory map.Map
syntax type map "[%1 -> %2]"
syntax function get "%1(%2)"
syntax function set "(%1 WITH [(%2) |-> %3])"
syntax function ([]) "%1(%2)"
syntax function set "(%1 WITH [(%2) |-> %3])"
syntax function ([<-]) "(%1 WITH [(%2) |-> %3])"
remove prop Select_eq
remove prop Select_neq
(* %t0 is "map a b"
%t1 is the type of const's argument, that is "b"
but we need type "a" instead, i.e. the first type argument
syntax function const "(LAMBDA (x:%t1): %1)"
syntax function const "(LAMBDA (x:%v0): %1)"
remove prop Const
*)
end
theory Bool
......@@ -65,7 +63,6 @@ theory bool.Bool
end
theory int.Int
syntax function zero "0"
......@@ -115,42 +112,6 @@ theory int.MinMax
end
theory int.EuclideanDivision
syntax function div "ndiv(%1, %2)"
syntax function mod "mod(%1, %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Mod_1
remove prop Div_1
end
(***
theory int.ComputerDivision
syntax function div "(ZOdiv %1 %2)"
syntax function mod "(ZOmod %1 %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Div_sign_pos
remove prop Div_sign_neg
remove prop Mod_sign_pos
remove prop Mod_sign_neg
remove prop Rounds_toward_zero
remove prop Div_1
remove prop Mod_1
remove prop Div_inf
remove prop Mod_inf
remove prop Div_mult
remove prop Mod_mult
end
***)
theory real.Real
......@@ -192,6 +153,16 @@ theory real.Real
end
theory real.MinMax
syntax function min "min(%1, %2)"
syntax function max "max(%1, %2)"
remove prop Max_is_ge
remove prop Max_is_some
remove prop Min_is_le
remove prop Min_is_some
end
theory real.RealInfix
syntax function (+.) "(%1 + %2)"
......@@ -263,6 +234,130 @@ theory real.Trigonometry
end
theory option.Option
syntax type option "lift[%1]"
syntax function None "bottom"
syntax function Some "up(%1)"
end
theory list.List
syntax type list "list[%1]"
syntax function Nil "null"
syntax function Cons "cons(%1, %2)"
end
theory list.Length
syntax function length "length(%1)"
remove prop Length_nonnegative
remove prop Length_nil
end
theory list.Mem
syntax predicate mem "member(%1, %2)"
end
theory list.Nth
syntax function nth
"IF 0 <= %1 AND %1 < length(%2) THEN up(nth(%2, %1)) ELSE bottom ENDIF"
end
theory list.Append
syntax function (++) "append(%1, %2)"
remove prop Append_assoc
remove prop Append_l_nil
remove prop Append_length
end
theory list.Reverse
syntax function reverse "reverse(%1)"
end
theory set.Set
syntax type set "set[%1]"
syntax predicate mem "member(%1, %2)"
remove prop extensionality
syntax predicate subset "subset?(%1, %2)"
remove prop subset_trans
syntax function empty "(emptyset :: %t0)"
syntax predicate is_empty "empty?(%1)"
remove prop empty_def1
syntax function add "add(%1, %2)"
remove prop add_def1
syntax function singleton "singleton(%1)"
syntax function remove "remove(%1, %2)"
remove prop remove_def1
remove prop subset_remove
syntax function union "union(%1, %2)"
remove prop union_def1
syntax function inter "intersection(%1, %2)"
remove prop inter_def1
syntax function diff "difference(%1, %2)"
remove prop diff_def1
remove prop subset_diff
(* TODO: choose *)
syntax function all "fullset"
remove prop all_def
end
theory set.Fset
syntax type set "finite_set[%1]"
syntax predicate mem "member(%1, %2)"
remove prop extensionality
syntax predicate subset "subset?(%1, %2)"
remove prop subset_trans
syntax function empty "(emptyset :: %t0)"
syntax predicate is_empty "empty?(%1)"
remove prop empty_def1
syntax function add "add(%1, %2)"
remove prop add_def1
syntax function singleton "singleton(%1)"
syntax function remove "remove(%1, %2)"
remove prop remove_def1
remove prop subset_remove
syntax function union "union(%1, %2)"
remove prop union_def1
syntax function inter "intersection(%1, %2)"
remove prop inter_def1
syntax function diff "difference(%1, %2)"
remove prop diff_def1
remove prop subset_diff
(* TODO: choose *)
syntax function cardinal "Card(%1)"
remove prop cardinal_nonneg
remove prop cardinal_empty
remove prop cardinal_add
remove prop cardinal_remove
remove prop cardinal_subset
remove prop cardinal1
(* TODO: nth *)
end
(* this file has an extension .aux rather than .gen
since it should not be distributed *)
import "pvs-realizations.aux"
Abs: THEORY
BEGIN
IMPORTING Int
% do not edit above this line
% Why3 tuple0
......
......@@ -2,7 +2,6 @@ ComputerDivision: THEORY
BEGIN
IMPORTING Int
IMPORTING Abs
% do not edit above this line
% Why3 tuple0
......
......@@ -2,7 +2,6 @@ EuclideanDivision: THEORY
BEGIN
IMPORTING Int
IMPORTING Abs
% do not edit above this line
% Why3 tuple0
......
Int: THEORY
BEGIN
% do not edit above this line
% Why3 tuple0
......
MinMax: THEORY
BEGIN
IMPORTING Int
% do not edit above this line
% Why3 tuple0
......
Abs: THEORY
BEGIN
IMPORTING Real
% do not edit above this line
% Why3 tuple0
......
......@@ -2,7 +2,6 @@ FromInt: THEORY
BEGIN
IMPORTING int@Int
IMPORTING Real
% do not edit above this line
% Why3 tuple0
......
MinMax: THEORY
BEGIN
IMPORTING Real
% do not edit above this line
% Why3 tuple0
......
Real: THEORY
BEGIN
% do not edit above this line
% Why3 tuple0
......
......@@ -89,7 +89,7 @@ let iter_group expr iter_fun text =
iter 0 false
let regexp_arg_pos = Str.regexp "%\\([0-9]+\\)"
let regexp_arg_pos_typed = Str.regexp "%\\([t]?[0-9]+\\)"
let regexp_arg_pos_typed = Str.regexp "%\\([tv]?[0-9]+\\)"
exception BadSyntaxIndex of int
exception BadSyntaxArity of int * int
......@@ -102,19 +102,26 @@ let check_syntax s len =
in
iter_group regexp_arg_pos arg s
let check_syntax_typed s len ret =
let check_syntax_typed ls s =
let len = List.length ls.ls_args in
let ret = ls.ls_value <> None in
let nfv = Stv.cardinal (ls_ty_freevars ls) in
let arg s =
let grp = (Str.matched_group 1 s) in
if grp.[0] = 't'
then
if grp.[0] = 't' then begin
let grp = String.sub grp 1 (String.length grp - 1) in
let i = int_of_string grp in
if i < 0 || (not ret && i = 0) then raise (BadSyntaxIndex i);
if i > len then raise (BadSyntaxArity (len,i));
else
if i > len then raise (BadSyntaxArity (len,i))
end else if grp.[0] = 'v' then begin
let grp = String.sub grp 1 (String.length grp - 1) in
let i = int_of_string grp in
if i < 0 || i >= nfv then raise (BadSyntaxIndex i)
end else begin
let i = int_of_string grp in
if i <= 0 then raise (BadSyntaxIndex i);
if i > len then raise (BadSyntaxArity (len,i));
end
in
iter_group regexp_arg_pos_typed arg s
......@@ -125,17 +132,33 @@ let syntax_arguments s print fmt l =
print fmt args.(i-1) in
global_substitute_fmt regexp_arg_pos repl_fun s fmt
(* return the type arguments of a symbol application, sorted according
to their (formal) names *)
let get_type_arguments t = match t.t_node with
| Tapp (ls, tl) ->
let m = oty_match Mtv.empty ls.ls_value t.t_ty in
let m = List.fold_left2
(fun m ty t -> oty_match m (Some ty) t.t_ty) m ls.ls_args tl in
let name tv = Util.Mstr.add tv.tv_name.id_string in
let m = Mtv.fold name m Util.Mstr.empty in
Array.of_list (Util.Mstr.values m)
| _ ->
[||]
let syntax_arguments_typed s print_arg print_type t fmt l =
let args = Array.of_list l in
let repl_fun s fmt =
let grp = (Str.matched_group 1 s) in
if grp.[0] = 't'
then
if grp.[0] = 't' then
let grp = String.sub grp 1 (String.length grp - 1) in
let i = int_of_string grp in
if i = 0
then print_type fmt (t_type (Util.of_option t))
then print_type fmt (t_type t)
else print_type fmt (t_type args.(i-1))
else if grp.[0] = 'v' then
let grp = String.sub grp 1 (String.length grp - 1) in
let m = get_type_arguments t in
print_type fmt m.(int_of_string grp)
else
let i = int_of_string grp in
print_arg fmt args.(i-1) in
......@@ -179,7 +202,7 @@ let syntax_type ts s =
create_meta meta_syntax_type [MAts ts; MAstr s]
let syntax_logic ls s =
check_syntax_typed s (List.length ls.ls_args) (ls.ls_value <> None);
check_syntax_typed ls s;
create_meta meta_syntax_logic [MAls ls; MAstr s]
let remove_prop pr =
......
......@@ -70,7 +70,7 @@ val syntax_arguments : string -> 'a pp -> 'a list pp
the list l using the template templ and the printer print_arg *)
val syntax_arguments_typed :
string -> term pp -> ty pp -> term option -> term list pp
string -> term pp -> ty pp -> term -> term list pp
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
......
......@@ -146,7 +146,7 @@ let rec print_term info fmt t = match t.t_node with
| Tvar v -> print_var fmt v
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments_typed s (print_term info)
(print_type info) (Some t) fmt tl
(print_type info) t fmt tl
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] -> fprintf fmt "%a" print_ident ls.ls_name
| _ -> fprintf fmt "@,%a(%a)"
......@@ -171,7 +171,7 @@ and print_fmla info fmt f = match f.t_node with
print_ident fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments_typed s (print_term info)
(print_type info) None fmt tl
(print_type info) f fmt tl
| None -> begin match tl with
| [] -> fprintf fmt "%a" print_ident ls.ls_name
| _ -> fprintf fmt "(%a(%a))"
......
......@@ -82,6 +82,30 @@ let black_list =
"closure"; "exists"; "law"; "subtypes";
"cond"; "exporting"; "lemma"; "subtype"; "of";
(* PVS prelude *)
"boolean"; "bool";
"pred"; "setof"; "exists1";
"list"; "member"; "append"; "reverse";
"domain"; "range"; "graph"; "preserves"; "inverts"; "transpose";
"restrict"; "extend"; "identity"; "eq";
"epsilon";
"set"; "member"; "emptyset"; "nonempty_set"; "fullset";
"union"; "intersection"; "complement"; "difference";
"symmetric_difference"; "every"; "some"; "singleton"; "add"; "remove";
"choose"; "the"; "singleton_elt"; "rest"; "setofsets"; "powerset";
"rinverse"; "rcomplement"; "runion"; "rintersection"; "image";
"preimage"; "postcondition"; "converse";
"number"; "number_field"; "numfield"; "nonzero_number"; "nznum";
"real"; "nonzero_real"; "nzreal";
"nonneg_real"; "nonpos_real"; "posreal"; "negreal"; "nnreal"; "npreal";
"rational"; "rat"; "nonzero_rational"; "nzrat";
"nonneg_rat"; "nonpos_rat"; "posrat"; "negrat"; "nnrat"; "nprat";
"integer"; "int"; "nonzero_integer"; "nzint";
"nonneg_int"; "nonpos_int"; "posint"; "negint"; "nnint"; "npint";
"subrange"; "even_int"; "odd_int";
"naturalnumber"; "nat"; "upto"; "below"; "succ"; "pred";
"min"; "max"; "sgn"; "abs";
"mod"; "divides"; "rem"; "ndiv";
"upfrom"; "above";
"even";
(* introduced by Why3 *)
"tuple0"; ]
......@@ -320,7 +344,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
| Tapp (fs, tl) ->
begin match query_syntax info.info_syn fs.ls_name with
| Some s ->
syntax_arguments s (print_term info) fmt tl
syntax_arguments_typed s (print_term info) (print_ty info) t fmt tl
| _ ->
let no_cast = unambig_fs fs in
begin match tl with
......@@ -663,8 +687,10 @@ let print_param_decl ~prev info fmt ls =
fprintf fmt "@]@\n@\n"
let print_param_decl ~prev info fmt ls =
if not (Mid.mem ls.ls_name info.info_syn) then
(print_param_decl ~prev info fmt ls; forget_tvs ())
if not (Mid.mem ls.ls_name info.info_syn) then begin
print_param_decl ~prev info fmt ls;
forget_tvs ()
end
let print_logic_decl ~prev info fmt (ls,ld) =
ignore prev;
......@@ -678,8 +704,10 @@ let print_logic_decl ~prev info fmt (ls,ld) =
List.iter forget_var vl
let print_logic_decl ~prev info fmt d =
if not (Mid.mem (fst d).ls_name info.info_syn) then
(print_logic_decl ~prev info fmt d; forget_tvs ())
if not (Mid.mem (fst d).ls_name info.info_syn) then begin
print_logic_decl ~prev info fmt d;
forget_tvs ()
end
let print_recursive_decl info fmt (ls,ld) =
let _, _, all_ty_params = ls_ty_vars ls in
......@@ -693,8 +721,16 @@ let print_recursive_decl info fmt (ls,ld) =
(print_expr info) e;
fprintf fmt "MEASURE %a BY <<@\n@]@\n"
print_vs (List.nth vl i);
List.iter forget_var vl;
forget_tvs ()
List.iter forget_var vl
let print_recursive_decl info fmt d =
eprintf "print_recursive_decl: %a@." print_id (fst d).ls_name;
Mid.iter (fun id _ -> eprintf " syn %a@." print_id id) info.info_syn;
if not (Mid.mem (fst d).ls_name info.info_syn) then begin
eprintf "DO IT@.";
print_recursive_decl info fmt d;
forget_tvs ()
end
let print_ind info fmt (pr,f) =
fprintf fmt "@[%% %a:@\n(%a)@]" print_pr pr (print_fmla info) f
......@@ -711,8 +747,10 @@ let print_ind_decl info fmt (ps,al) =
fprintf fmt "@\n"
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 ())
if not (Mid.mem (fst d).ls_name info.info_syn) then begin
print_ind_decl info fmt d;
forget_tvs ()
end
let re_lemma = Str.regexp "\\(\\bLEMMA\\b\\|\\bTHEOREM\\b\\)"
let rec find_lemma = function
......@@ -762,7 +800,7 @@ let print_decl ~old info fmt d =
| Dlogic [d] ->
print_recursive_decl info fmt d
| Dlogic _ ->
assert false (* PVS does not support mutually recursive defns *)
unsupportedDecl d "PVS does not support mutually recursive definitions"
| Dind (Ind, il) ->
print_list nothing (print_ind_decl info) fmt il
| Dind (Coind, _) ->
......@@ -855,7 +893,7 @@ let print_task env pr thpr realize ?old fmt task =
let lib = if path = thpath then "" else String.concat "." path ^ "@" in
fprintf fmt "IMPORTING %s%s@\n" lib th.Theory.th_name.id_string)
realized_theories;
fprintf fmt "@\n%% do not edit above this line@\n@\n";
fprintf fmt "%% do not edit above this line@\n@\n";
fprintf fmt "%% Why3 tuple0@\n";
fprintf fmt "tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0@\n@\n";
print_decls ~old info fmt local_decls;
......
......@@ -149,7 +149,7 @@ let rec print_term info fmt t = match t.t_node with
| Tvar v -> print_var fmt v
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments_typed s (print_term info)
(print_type info) (Some t) fmt tl
(print_type info) t fmt tl
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
| _ -> fprintf fmt "@[(%a@ %a)@]"
......@@ -174,7 +174,7 @@ and print_fmla info fmt f = match f.t_node with
print_ident fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments_typed s (print_term info)
(print_type info) None fmt tl
(print_type info) f fmt tl
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] -> fprintf fmt "%a" print_ident ls.ls_name
| _ -> fprintf fmt "(%a@ %a)"
......
......@@ -150,7 +150,7 @@ let rec print_term info fmt t = match t.t_node with
| Tvar v -> print_var fmt v
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments_typed s (print_term info)
(print_type info) (Some t) fmt tl
(print_type info) t fmt tl
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] -> fprintf fmt "%a" print_ident ls.ls_name
| _ -> fprintf fmt "@,(%a %a)"
......@@ -175,7 +175,7 @@ and print_fmla info fmt f = match f.t_node with
print_ident fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments_typed s (print_term info)
(print_type info) None fmt tl
(print_type info) f fmt tl
| None -> begin match tl with
| [] -> fprintf fmt "%a" print_ident ls.ls_name
| _ -> fprintf fmt "(%a %a)"
......
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