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

PVS realizations

parent baa1eafa
......@@ -127,6 +127,11 @@ why3.conf
/src/coq-tactic/.why3-vo-*
/lib/coq-tactic/why3tac.cma
# PVS
.pvscontext
/lib/pvs/*/*.summary
pvsbin/
# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
......@@ -156,6 +161,7 @@ why3.conf
# /drivers
/drivers/coq-realizations.aux
/drivers/pvs-realizations.aux
# /tests/
/tests/test-jcf/
......
......@@ -964,6 +964,75 @@ opt byte: drivers/coq-realizations.aux
clean::
rm -f drivers/coq-realizations.aux
####################
# PVS realizations
####################
ifeq (@enable_pvs_libs@,yes)
PVSLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES))
PVSLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix
PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES))
PVSLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime
PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES))
ifeq (@enable_pvs_fp_libs@,yes)
PVSLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
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)
drivers/pvs-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
for f in $(PVSLIBS_INT_FILES); do \
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_NUMBER_FILES); do \
echo 'theory number.'"$$f"' meta "realized" "number.'"$$f"'", "" end'; done; \
for f in $(PVSLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
) > $@
install_no_local::
mkdir -p $(LIBDIR)/why3/pvs/int
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/number
cp $(PVSLIBS_NUMBER) $(LIBDIR)/why3/pvs/number/
ifeq (@enable_pvs_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/pvs/floating_point/
cp $(PVSLIBS_FP) $(LIBDIR)/why3/pvs/
endif
cp drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
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_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
else
drivers/pvs-realizations.aux:
echo "(* generated automatically at compilation time *)" > $@
endif
opt byte: drivers/pvs-realizations.aux
clean::
rm -f drivers/pvs-realizations.aux
#######
# tools
#######
......
......@@ -100,6 +100,12 @@ AC_ARG_ENABLE(coq-libs,
[ --enable-coq-libs enable Coq realizations],,
enable_coq_libs=yes)
# PVS libraries
AC_ARG_ENABLE(pvs-libs,
[ --enable-pvs-libs enable PVS realizations],,
enable_pvs_libs=yes)
# hypothesis selection
AC_ARG_ENABLE(hypothesis-selection,
......@@ -445,6 +451,43 @@ if test "$enable_coq_libs" = yes; then
rm -f conftest.v conftest.vo conftest.err
fi
# PVS
enable_pvs_fp_libs=no
if test "$enable_pvs_libs" = no; then
enable_pvs_support=no
AC_MSG_WARN(PVS support disabled)
reason_pvs_support=" (disabled by user)"
else
AC_CHECK_PROG(PVS,pvs,pvs,no)
if test "$PVS" = no ; then
enable_pvs_support=no
AC_MSG_WARN(Cannot find pvs.)
reason_pvs_support=" (pvs not found)"
else
PVSLIB=`$PVS -where`
AC_MSG_CHECKING(PVS version)
PVSVERSION=`$PVS -version | sed -n -e 's|.*Version* *\([[^ ]]*\)$|\1|p' `
case $PVSVERSION in
5.0)
enable_pvs_support=yes
AC_MSG_RESULT($PVSVERSION)
;;
*)
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)"
;;
esac
fi
fi
if test "$enable_pvs_support" = no; then
enable_pvs_libs=no
fi
# hypothesis_selection
if test "$enable_hypothesis_selection" = yes; then
......@@ -529,6 +572,11 @@ AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQVERSION)
AC_SUBST(enable_pvs_libs)
AC_SUBST(enable_pvs_fp_libs)
AC_SUBST(PVS)
AC_SUBST(PVSVERSION)
AC_SUBST(enable_hypothesis_selection)
AC_SUBST(enable_doc)
......@@ -577,6 +625,15 @@ if test "$enable_coq_support" = "yes" ; then
echo " FP arithmetic : $enable_coq_fp_libs $reason_coq_fp_libs"
fi
fi
echo "PVS support : $enable_pvs_support $reason_pvs_support"
if test "$enable_pvs_support" = "yes" ; then
echo " Version : $PVSVERSION"
echo " Lib : $PVSLIB"
echo " Realization support : $enable_pvs_libs $reason_pvs_libs"
if test "$enable_pvs_libs" = "yes" ; then
echo " FP arithmetic : $enable_pvs_fp_libs $reason_pvs_fp_libs"
fi
fi
echo "hypothesis selection : $enable_hypothesis_selection"
echo "debugging symbols : $enable_debug"
echo "profiling : $enable_profiling"
......
......@@ -262,3 +262,7 @@ theory real.Trigonometry
syntax function tan "TAN(%1)"
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
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 abs
abs(x:int): int = IF (x >= 0) THEN x ELSE (-x) ENDIF
% Why3 abs_le
abs_le: AXIOM FORALL (x:int, y:int): (abs(x) <= y) <=> (((-y) <= x) AND
(x <= y))
% Why3 abs_pos
abs_pos: AXIOM FORALL (x:int): (abs(x) >= 0)
END Abs
\ No newline at end of file
ComputerDivision: THEORY
BEGIN
IMPORTING Int
IMPORTING Abs
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 div
div(x:int, x1:int): int
% Why3 mod
mod(x:int, x1:int): int
% Why3 div_mod
div_mod: AXIOM FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,
y)) + mod(x, y)))
% Why3 div_bound
div_bound: AXIOM FORALL (x:int, y:int): ((x >= 0) AND (y > 0)) =>
((0 <= div(x, y)) AND (div(x, y) <= x))
% Why3 mod_bound
mod_bound: AXIOM FORALL (x:int, y:int): (NOT (y = 0)) =>
(((-abs(y)) < mod(x, y)) AND (mod(x, y) < abs(y)))
% Why3 div_sign_pos
div_sign_pos: AXIOM FORALL (x:int, y:int): ((x >= 0) AND (y > 0)) =>
(div(x, y) >= 0)
% Why3 div_sign_neg
div_sign_neg: AXIOM FORALL (x:int, y:int): ((x <= 0) AND (y > 0)) =>
(div(x, y) <= 0)
% Why3 mod_sign_pos
mod_sign_pos: AXIOM FORALL (x:int, y:int): ((x >= 0) AND NOT (y = 0)) =>
(mod(x, y) >= 0)
% Why3 mod_sign_neg
mod_sign_neg: AXIOM FORALL (x:int, y:int): ((x <= 0) AND NOT (y = 0)) =>
(mod(x, y) <= 0)
% Why3 rounds_toward_zero
rounds_toward_zero: AXIOM FORALL (x:int, y:int): (NOT (y = 0)) =>
(abs((div(x, y) * y)) <= abs(x))
% Why3 div_1
div_1: AXIOM FORALL (x:int): (div(x, 1) = x)
% Why3 mod_1
mod_1: AXIOM FORALL (x:int): (mod(x, 1) = 0)
% Why3 div_inf
div_inf: AXIOM FORALL (x:int, y:int): ((0 <= x) AND (x < y)) => (div(x,
y) = 0)
% Why3 mod_inf
mod_inf: AXIOM FORALL (x:int, y:int): ((0 <= x) AND (x < y)) => (mod(x,
y) = x)
% Why3 div_mult
div_mult: AXIOM FORALL (x:int, y:int, z:int): ((x > 0) AND ((y >= 0) AND
(z >= 0))) => (div(((x * y) + z), x) = (y + div(z, x)))
% Why3 mod_mult
mod_mult: AXIOM FORALL (x:int, y:int, z:int): ((x > 0) AND ((y >= 0) AND
(z >= 0))) => (mod(((x * y) + z), x) = mod(z, x))
END ComputerDivision
\ No newline at end of file
(Int
(unit_def 0
(unit_def-1 nil 3551114638 ("" (grind) nil nil)
((zero const-decl "int" Int nil)) shostak))
(assoc 0
(assoc-1 nil 3551114663 ("" (grind) nil nil)
((int_plus_int_is_int application-judgement "int" integers
nil))
shostak))
(inv_def 0
(inv_def-1 nil 3551114670 ("" (grind) nil nil)
((zero const-decl "int" Int nil)
(minus_int_is_int application-judgement "int" integers nil))
shostak))
(comm 0 (comm-1 nil 3551114676 ("" (grind) nil nil) nil shostak))
(assoc1 0
(assoc1-1 nil 3551114692 ("" (grind) nil nil)
((mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
shostak))
(mul_distr 0
(mul_distr-1 nil 3551114708 ("" (grind) nil nil)
((mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
shostak))
(comm1 0 (comm1-1 nil 3551114723 ("" (grind) nil nil) nil shostak))
(unitary 0
(unitary-1 nil 3551114731 ("" (grind) nil nil)
((one const-decl "int" Int nil)) shostak))
(nontrivialring 0
(nontrivialring-1 nil 3551114740 ("" (grind) nil nil)
((zero const-decl "int" Int nil) (one const-decl "int" Int nil))
shostak))
(refl 0
(refl-1 nil 3551114750 ("" (grind) nil nil)
((infix_lseq const-decl "bool" Int nil)) shostak))
(trans 0
(trans-1 nil 3551114763 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(infix_lseq const-decl "bool" Int nil))
shostak))
(antisymm 0
(antisymm-1 nil 3551114771 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(infix_lseq const-decl "bool" Int nil))
shostak))
(total 0
(total-1 nil 3551114779 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(infix_lseq const-decl "bool" Int nil))
shostak))
(zerolessone 0
(zerolessone-1 nil 3551114789 ("" (grind) nil nil)
((zero const-decl "int" Int nil) (one const-decl "int" Int nil)
(infix_lseq const-decl "bool" Int nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(compatorderadd 0
(compatorderadd-1 nil 3551114796 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(infix_lseq const-decl "bool" Int nil))
shostak))
(compatordermult 0
(compatordermult-1 nil 3551114806
("" (grind)
(("" (auto-rewrite-theory "real_props") (("" (assert) nil nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(zero const-decl "int" Int nil)
(infix_lseq const-decl "bool" Int nil))
shostak)))
Int: THEORY
BEGIN
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 zero
zero: int = 0
% Why3 one
one: int = 1
% Why3 infix_ls
infix_ls(x:int, x1:int): MACRO bool = x<x1
% Why3 infix_gt
infix_gt(x:int, y:int): bool = infix_ls(y, x)
% Why3 infix_lseq
infix_lseq(x:int, y:int): bool = infix_ls(x, y) OR (x = y)
% Why3 infix_pl
infix_pl(x:int, x1:int): MACRO int = x+x1
% Why3 prefix_mn
prefix_mn(x:int): MACRO int = -x
% Why3 infix_as
infix_as(x:int, x1:int): MACRO int = x*x1
% Why3 unit_def
unit_def: LEMMA FORALL (x:int): (infix_pl(x, zero) = x)
% Why3 assoc
assoc: LEMMA FORALL (x:int, y:int, z:int): (infix_pl(infix_pl(x, y),
z) = infix_pl(x, infix_pl(y, z)))
% Why3 inv_def
inv_def: LEMMA FORALL (x:int): (infix_pl(x, prefix_mn(x)) = zero)
% Why3 comm
comm: LEMMA FORALL (x:int, y:int): (infix_pl(x, y) = infix_pl(y, x))
% Why3 assoc1
assoc1: LEMMA FORALL (x:int, y:int, z:int): (infix_as(infix_as(x, y),
z) = infix_as(x, infix_as(y, z)))
% Why3 mul_distr
mul_distr: LEMMA FORALL (x:int, y:int, z:int): (infix_as(x, infix_pl(y,
z)) = infix_pl(infix_as(x, y), infix_as(x, z)))
% Why3 infix_mn
infix_mn(x:int, y:int): int = infix_pl(x, prefix_mn(y))
% Why3 comm1
comm1: LEMMA FORALL (x:int, y:int): (infix_as(x, y) = infix_as(y, x))
% Why3 unitary
unitary: LEMMA FORALL (x:int): (infix_as(one, x) = x)
% Why3 nontrivialring
nontrivialring: LEMMA NOT (zero = one)
% Why3 infix_gteq
infix_gteq(x:int, y:int): bool = infix_lseq(y, x)
% Why3 refl
refl: LEMMA FORALL (x:int): infix_lseq(x, x)
% Why3 trans
trans: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
(infix_lseq(y, z) => infix_lseq(x, z))
% Why3 antisymm
antisymm: LEMMA FORALL (x:int, y:int): infix_lseq(x, y) => (infix_lseq(y,
x) => (x = y))
% Why3 total
total: LEMMA FORALL (x:int, y:int): infix_lseq(x, y) OR infix_lseq(y, x)
% Why3 zerolessone
zerolessone: LEMMA infix_lseq(zero, one)
% Why3 compatorderadd
compatorderadd: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
infix_lseq(infix_pl(x, z), infix_pl(y, z))
% Why3 compatordermult
compatordermult: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
(infix_lseq(zero, z) => infix_lseq(infix_as(x, z), infix_as(y, z)))
END Int
\ No newline at end of file
......@@ -334,7 +334,7 @@ editor = "pvs"
[editor pvs]
name = "PVS"
command = "pvs %f"
command = "PVS_LIBRARY_PATH=%l/pvs pvs %f"
[editor coqide]
name = "CoqIDE"
......
......@@ -43,20 +43,15 @@ QUESTIONS FOR THE PVS TEAM
LET x2 = x1`1, x3 = x1`2 IN ...
* pattern-matching
- By mistake, I used _ as a catch-all in a CASES expressions
(as in ML and in Why3) and it made PVS go wild!
* I intend to use the script "proveit" to replay PVS proofs (when they exist).
What is the canonical way to check that all proofs have indeed been
successfully replayed? (exit code, grep on proveit's output, etc.)
better: LET (x2, x3) = x1 IN ...
TODO
----
* driver
- maps: const
* use proveit (same path as PVS) to replay a proof
*)
open Format
......@@ -487,8 +482,8 @@ type chunk =
| Edition of string * contents (* name contents *)
| Other of contents (* contents *)
let re_theory = Str.regexp "[^ :]+: THEORY"
let re_begin = Str.regexp " BEGIN"
let re_ignored =
Str.regexp "\\([^ :]+: THEORY\\)\\|\\([^ :]+: LIBRARY\\)\\|IMPORTING\\| BEGIN"
let re_why3 = Str.regexp "% Why3 \\([^ ]+\\)"
(* Reads an old version of the file, as a list of chunks.
......@@ -501,8 +496,7 @@ let read_old_script ch =
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
if Str.string_match re_ignored s 0 then read_line () else s
in
let rec read ?name () =
let s = read_line () in
......@@ -604,7 +598,7 @@ let print_type_decl ~prev info fmt ts = ignore (prev);
print_name fmt ts.ts_name;
match ts.ts_def with
| None ->
fprintf fmt "@[<hov 2>%a%a: TYPE"
fprintf fmt "@[<hov 2>%a%a: TYPE+"
print_ts ts print_params_list ts.ts_args;
realization fmt info prev;
fprintf fmt "@]@\n@\n"
......@@ -795,54 +789,69 @@ let print_task env pr thpr realize ?old fmt task =
let f,id =
let l = split_string_rev s1 '.' in List.rev (List.tl l),List.hd l in
let th = Env.find_theory env f id in
Mid.add th.Theory.th_name (th, if s2 = "" then s1 else s2) mid
Mid.add th.Theory.th_name (th, (f, if s2 = "" then s1 else s2)) mid
| _ -> assert false
) Mid.empty task in
(* 2 cases: task is clone T with [] or task is a real goal *)
let thname, realized_theories = match task with
(* two cases: task is clone T with [] or task is a real goal *)
let thname, thpath, realized_theories = match task with
| None -> assert false
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
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
let id = th.Theory.th_name in
id.id_string, th.Theory.th_path, Mid.remove id 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
name, [], realized_theories
in
let realized_theories' =
Mid.map (fun (th,s) -> fprintf fmt "IMPORTING %a.%s@\n"
print_path th.Theory.th_path s; th)
realized_theories in
(* make names as stable as possible by first printing all identifiers *)
let realized_theories' = Mid.map fst realized_theories in
let realized_symbols = Task.used_symbols realized_theories' in
let local_decls = Task.local_decls task realized_symbols in
(* associate a special printer to each symbol in a realized theory *)
let symbol_printers =
let printers =
Mid.map (fun th ->
let pr = fresh_printer () in
Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
pr
) realized_theories' in
pr)
realized_theories' in
Mid.map (fun th ->
(snd (Mid.find th.Theory.th_name realized_theories), th,
Mid.find th.Theory.th_name printers)
) realized_symbols in
let _, (_, s) = Mid.find th.Theory.th_name realized_theories in
(s, th, Mid.find th.Theory.th_name printers))
realized_symbols in
let info = {
info_syn = get_syntax_map task;
symbol_printers = symbol_printers;
realization = realize;
}
in
(* (\* build IMPORTING declarations *\) *)
(* let libraries = Hashtbl.create 17 in (\* path -> library name *\) *)
(* let importing = Hashtbl.create 17 in (\* library name -> theory name *\) *)
(* let add _ (th, (path, _)) = *)
(* if not (Hashtbl.mem libraries path) then begin *)
(* let libname = String.concat "_" ("why3" :: path) in *)
(* Hashtbl.add libraries path libname *)
(* end; *)
(* let libname = Hashtbl.find libraries path in *)
(* Hashtbl.add importing libname th.Theory.th_name.id_string *)
(* in *)
(* Mid.iter add realized_theories; *)
(* finally, read the old file, if any, and generate the new one *)
let old = ref (match old with
| None -> []
| Some ch -> read_old_script ch)
in
fprintf fmt "@[<hov 1>%s: THEORY@\n@[<hov 1>BEGIN@\n@\n" thname;
fprintf fmt "%% Why3 tuple0@\n";
fprintf fmt "@[<hov 1>%s: THEORY@\n@[<hov 1>BEGIN@\n" thname;
Mid.iter
(fun _ (th, (path, _)) ->
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%% Why3 tuple0@\n";
fprintf fmt "tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0@\n@\n";
print_decls ~old info fmt local_decls;
output_remaining fmt !old;
......
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