Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit d1bef4be authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge remote-tracking branch 'berghofer/master'

parents 4d5bffd3 a0a26c4c
......@@ -134,6 +134,11 @@ orphaned-proofs.prf
/lib/pvs/*/*.summary
pvsbin/
# Isabelle
/lib/isabelle/*.xml
/lib/isabelle/int/*.xml
/lib/isabelle/real/*.xml
# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
......@@ -166,6 +171,7 @@ pvsbin/
# /drivers
/drivers/coq-realizations.aux
/drivers/pvs-realizations.aux
/drivers/isabelle-realizations.aux
# /tests/
/tests/test-jcf/
......
......@@ -128,7 +128,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
introduction abstraction close_epsilon lift_epsilon \
eval_match instantiate_predicate smoke_detector
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs \
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
simplify gappa cvc3 yices mathematica
LIB_SESSION = xml termcode session session_tools session_scheduler
......@@ -1047,6 +1047,103 @@ opt byte: drivers/pvs-realizations.aux
clean::
rm -f drivers/pvs-realizations.aux
#######################
# Isabelle realizations
#######################
ifeq (@enable_isabelle_libs@,yes)
ISABELLELIBS_INT_FILES = Exponentiation Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES)))
ISABELLELIBS_BOOL_FILES = Bool
ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_BOOL_FILES)))
ISABELLELIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt Real Square RealInfix
ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix lib/isabelle/real/, $(ISABELLELIBS_REAL_FILES)))
ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime
ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_NUMBER_FILES)))
ISABELLELIBS_SET_FILES = Set Fset
ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_SET_FILES)))
ISABELLELIBS_MAP_FILES = Map MapPermut
ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_MAP_FILES)))
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse
ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_LIST_FILES)))
drivers/isabelle-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
for f in $(ISABELLELIBS_INT_FILES); do \
echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_BOOL_FILES); do \
echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_REAL_FILES); do \
echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_NUMBER_FILES); do \
echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_SET_FILES); do \
echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_MAP_FILES); do \
echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_LIST_FILES); do \
echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_OPTION_FILES); do \
echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
) > $@
install_no_local::
cp -r lib/isabelle $(LIBDIR)/why3
cp drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
$(ISABELLELIBS_INT): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
mkdir -p lib/isabelle/int/
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(ISABELLELIBS_BOOL): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T bool.$(notdir $(basename $@)) -o lib/isabelle/
$(ISABELLELIBS_REAL): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
mkdir -p lib/isabelle/real/
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(ISABELLELIBS_NUMBER): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T number.$(notdir $(basename $@)) -o lib/isabelle/
$(ISABELLELIBS_SET): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T set.$(notdir $(basename $@)) -o lib/isabelle/
$(ISABELLELIBS_MAP): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T map.$(notdir $(basename $@)) -o lib/isabelle/
$(ISABELLELIBS_LIST): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T list.$(notdir $(basename $@)) -o lib/isabelle/
$(ISABELLELIBS_OPTION): bin/why3 drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T option.$(notdir $(basename $@)) -o lib/isabelle/
opt byte: update-isabelle
clean::
rm -f drivers/isabelle-realizations.aux
rm -rf lib/isabelle/*.xml lib/isabelle/int lib/isabelle/real
endif
################
# Jessie3 plugin
################
......
......@@ -97,6 +97,12 @@ AC_ARG_ENABLE(pvs-libs,
[ --enable-pvs-libs enable PVS realizations],,
enable_pvs_libs=yes)
# Isabelle libraries
AC_ARG_ENABLE(isabelle-libs,
[ --enable-isabelle-libs enable Isabelle realizations],,
enable_isabelle_libs=yes)
# hypothesis selection
AC_ARG_ENABLE(hypothesis-selection,
......@@ -527,6 +533,41 @@ else
COMPILETIMEPVS="\\\"PVS\\\", \\\"$PVSVERSION\\\"; "
fi
# Isabelle
if test "$enable_isabelle_libs" = no; then
enable_isabelle_support=no
AC_MSG_WARN(Isabelle support disabled)
reason_isabelle_support=" (disabled by user)"
else
AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
if test "$ISABELLE" = no ; then
enable_isabelle_support=no
AC_MSG_WARN(Cannot find isabelle.)
reason_isabelle_support=" (isabelle not found)"
else
AC_MSG_CHECKING(Isabelle version)
ISABELLEVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEVERSION in
2013-1)
enable_isabelle_support=yes
AC_MSG_RESULT($ISABELLEVERSION)
;;
*)
AC_MSG_RESULT($ISABELLEVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle2013-1 or higher; Isabelle discarded)
reason_isabelle_support=" (need version 2013-1 or higher)"
;;
esac
fi
fi
if test "$enable_isabelle_support" = no; then
enable_isabelle_libs=no
fi
if test "$enable_pvs_libs" = yes; then
AC_MSG_CHECKING([for NASA PVS library])
enable_pvs_libs=no
......@@ -654,6 +695,10 @@ AC_SUBST(PVS)
AC_SUBST(PVSVERSION)
AC_SUBST(COMPILETIMEPVS)
AC_SUBST(enable_isabelle_libs)
AC_SUBST(ISABELLE)
AC_SUBST(ISABELLEVERSION)
AC_SUBST(enable_hypothesis_selection)
AC_SUBST(enable_doc)
......@@ -725,6 +770,11 @@ if test "$enable_pvs_support" = yes ; then
echo " Library path : $PVSLIB"
echo " Realization support : $enable_pvs_libs$reason_pvs_libs"
fi
echo "Isabelle support : $enable_isabelle_support$reason_isabelle_support"
if test "$enable_isabelle_support" = yes ; then
echo " Version : $ISABELLEVERSION"
echo " Realization support : $enable_isabelle_libs$reason_isabelle_libs"
fi
echo "Frama-C support : $enable_frama_c$reason_frama_c"
if test "$enable_frama_c" = yes ; then
echo " Version : $FRAMAC_VERSION"
......
valid "Finished Why3 theory"
fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "eliminate_projections"
transformation "simplify_formula"
theory BuiltIn
syntax type int "<type name=\"Int.int\"/>"
syntax type real "<type name=\"Real.real\"/>"
syntax predicate (=) "<app><const name=\"HOL.eq\"/>%1%2</app>"
end
theory Bool
syntax type bool "<type name=\"HOL.bool\"/>"
syntax function True "<const name=\"HOL.True\"/>"
syntax function False "<const name=\"HOL.False\"/>"
end
theory bool.Bool
syntax function andb "<app><const name=\"HOL.conj\"/>%1%2</app>"
syntax function orb "<app><const name=\"HOL.disj\"/>%1%2</app>"
syntax function notb "<app><const name=\"HOL.Not\"/>%1</app>"
syntax function implb "<app><const name=\"HOL.implies\"/>%1%2</app>"
end
theory int.Int
syntax function zero "<number val=\"0\"><type name=\"Int.int\"/></number>"
syntax function one "<number val=\"1\"><type name=\"Int.int\"/></number>"
syntax function (+) "<app><const name=\"Groups.plus_class.plus\"/>%1%2</app>"
syntax function (-) "<app><const name=\"Groups.minus_class.minus\"/>%1%2</app>"
syntax function (*) "<app><const name=\"Groups.times_class.times\"/>%1%2</app>"
syntax function (-_) "<app><const name=\"Groups.uminus_class.uminus\"/>%1</app>"
syntax predicate (<=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
syntax predicate (<) "<app><const name=\"Orderings.ord_class.less\"/>%1%2</app>"
syntax predicate (>=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%2%1</app>"
syntax predicate (>) "<app><const name=\"Orderings.ord_class.less\"/>%2%1</app>"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop ZeroLessOne
end
theory int.Abs
syntax function abs "<app><const name=\"Groups.abs_class.abs\"/>%1</app>"
remove prop Abs_pos
end
theory int.MinMax
syntax function min "<app><const name=\"Orderings.ord_class.min\"/>%1%2</app>"
syntax function max "<app><const name=\"Orderings.ord_class.max\"/>%1%2</app>"
end
theory int.Exponentiation
syntax function power "<app><const name=\"Power.power_class.power\"/>%1<app><const name=\"Int.nat\"/>%2</app></app>"
end
theory list.List
syntax type list "<type name=\"List.list\">%1</type>"
syntax function Nil "<const name=\"List.list.Nil\">%t0</const>"
syntax function Cons "<app><const name=\"List.list.Cons\"/>%1%2</app>"
end
theory list.Length
syntax function length "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"List.length\"/>%1</app></app>"
end
theory list.Append
syntax function (++) "<app><const name=\"List.append\"/>%1%2</app>"
end
theory list.Reverse
syntax function reverse "<app><const name=\"List.rev\"/>%1</app>"
end
theory list.Mem
syntax predicate mem "<app><const name=\"Set.member\"/>%1<app><const name=\"List.set\"/>%2</app></app>"
end
theory list.NthNoOpt
syntax function nth "<app><const name=\"List.nth\"/>%2<app><const name=\"Int.nat\"/>%1</app></app>"
end
theory option.Option
syntax type option "<type name=\"Option.option\">%1</type>"
syntax function None "<const name=\"Option.option.None\">%t0</const>"
syntax function Some "<app><const name=\"Option.option.Some\"/>%1</app>"
end
theory map.Map
syntax type map "<fun>%1%2</fun>"
syntax function get "<app>%1%2</app>"
syntax function ([]) "<app>%1%2</app>"
syntax function set "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
syntax function ([<-]) "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
syntax function const "<app><const name=\"_type_constraint_\"><fun>%t0%t0</fun></const><abs name=\"\"><type name=\"dummy\"/>%1</abs></app>"
end
theory set.SetGen
syntax predicate (==) "<app><const name=\"HOL.eq\"/>%1%2</app>"
syntax predicate subset "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
end
theory set.Fset
syntax function cardinal "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"FSet.fcard\"/>%1</app></app>"
end
(* this file has an extension .aux rather than .gen since it should not be distributed *)
import "isabelle-realizations.aux"
printer "isabelle-realize"
filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
printer "isabelle"
filename "%f_%t_%g.xml"
transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
chapter Why3
session Why3 = HOL +
options [document = false]
theories Why3
#!/usr/bin/env bash
#
# DESCRIPTION: process files generated by Why3
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] WHY3_FILE"
echo
echo " Options are:"
echo " -b batch mode"
echo " -i NAME interactive mode using interface NAME"
echo
echo " Process files generated by Why3"
exit 1
}
## utilities
function make_theory()
{
BNAME=`basename "$1"`
if [ ! -e "$1.thy" ]; then
echo -e "theory $BNAME\nimports Why3\nbegin\n\nwhy3_open \"$BNAME.xml\"\n" > "$1.thy"
sed \
-e 's/<lemma name="\([^"]*\)"[^>]*>/why3_vc \1\n\n/g' \
-e 's/<[^l][^>]*>//g' \
"$1.xml" >> "$1.thy"
echo -e "why3_end\n\nend" >> "$1.thy"
fi
}
## process command line
while getopts "bi:" OPT
do
case "$OPT" in
b)
BATCH=true
;;
i)
INTERACTIVE=true
INTERFACE="$OPTARG"
;;
\?)
usage
;;
esac
done
## main
shift $(($OPTIND - 1))
if [ "$1" = "" ]; then
usage
else
NAME=`dirname "$1"`/`basename "$1" .xml`
fi
if [ "$BATCH" = true ]; then
$ISABELLE_PROCESS -e "use_thy \"$NAME\";" -rq Why3
elif [ "$INTERACTIVE" = true ]; then
if [ "$INTERFACE" = emacs ]; then
LOGIC="-L"
else
LOGIC="-l"
fi
make_theory "$NAME"
$ISABELLE_TOOL $INTERFACE $LOGIC Why3 "$NAME.thy"
else
usage
fi
theory Why3
imports
Why3_Map
Why3_Set
Why3_List
Why3_Int
begin
end
theory Why3_Int
imports Why3_Setup
begin
section {* Integers and the basic operators *}
why3_open "int/Int.xml"
why3_vc Comm by simp
why3_vc Comm1 by simp
why3_vc Assoc by simp
why3_vc Assoc1 by simp
why3_vc Unitary by simp
why3_vc Inv_def_l by simp
why3_vc Inv_def_r by simp
why3_vc Unit_def_l by simp
why3_vc Unit_def_r by simp
why3_vc Mul_distr_l by (simp add: ring_distribs)
why3_vc Mul_distr_r by (simp add: ring_distribs)
why3_vc infix_mn_def by simp
why3_vc NonTrivialRing by simp
why3_vc infix_lseq_def by auto
why3_vc Refl by simp
why3_vc Trans using assms by simp
why3_vc Total by auto
why3_vc Antisymm using assms by simp
why3_vc ZeroLessOne by simp
why3_vc CompatOrderAdd using assms by simp
why3_vc CompatOrderMult using assms by (rule mult_right_mono)
why3_end
section {* Absolute Value *}
why3_open "int/Abs.xml"
why3_vc abs_def by simp
why3_vc Abs_le by auto
why3_vc Abs_pos by simp
why3_end
section {* Minimum and Maximum *}
why3_open "int/MinMax.xml"
why3_vc Max_x using assms by simp
why3_vc Max_y using assms by simp
why3_vc Max_sym by simp
why3_vc Max_is_ge by simp_all
why3_vc Max_is_some by auto
why3_vc Min_x using assms by simp
why3_vc Min_y using assms by simp
why3_vc Min_sym by simp
why3_vc Min_is_le by simp_all
why3_vc Min_is_some by auto
why3_end
section {* Euclidean Division *}
definition ediv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "ediv" 70) where
"a ediv b = sgn b * (a div \<bar>b\<bar>)"
definition emod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "emod" 70) where
"a emod b = a mod \<bar>b\<bar>"
why3_open "int/EuclideanDivision.xml"
constants
div = ediv
mod = emod
why3_vc Div_1 by (simp add: ediv_def)
why3_vc Div_1_left using assms by (simp add: ediv_def div_pos_pos_trivial)
why3_vc Div_inf using assms by (simp add: ediv_def div_pos_pos_trivial)
why3_vc Div_inf_neg
using assms
by (cases "x = y") (simp_all add: ediv_def
zdiv_zminus1_eq_if div_pos_pos_trivial mod_pos_pos_trivial)
why3_vc Div_mod
by (simp add: ediv_def emod_def mult_assoc [symmetric] abs_sgn)
why3_vc Div_mult using assms by (simp add: ediv_def add_commute)
why3_vc Div_bound
proof -
from assms show ?C1
by (simp add: ediv_def pos_imp_zdiv_nonneg_iff)
show ?C2
proof (cases "x = 0")
case False
show ?thesis
proof (cases "y = 1")
case False
with assms `x \<noteq> 0` have "x div y < x"
by (simp add: int_div_less_self)
with assms show ?thesis by (simp add: ediv_def)
qed (simp add: ediv_def)
qed (simp add: ediv_def)
qed
why3_vc Div_minus1_left
using assms
by (simp only: zdiv_zminus1_eq_if ediv_def)
(simp add: div_pos_pos_trivial mod_pos_pos_trivial)
why3_vc Mod_0 by (simp add: emod_def)
why3_vc Mod_1 by (simp add: emod_def)
why3_vc Mod_1_left using assms by (simp add: emod_def mod_pos_pos_trivial)
why3_vc Mod_minus1_left
using assms
by (simp only: emod_def zmod_zminus1_eq_if) (simp add: mod_pos_pos_trivial)
why3_vc Mod_mult using assms by (simp add: emod_def add_commute)
why3_vc Mod_bound using assms by (simp_all add: emod_def)
why3_end
section {* Computer Division *}
definition cdiv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "cdiv" 70) where
"a cdiv b = sgn a * sgn b * (\<bar>a\<bar> div \<bar>b\<bar>)"
definition cmod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "cmod" 70) where
"a cmod b = sgn a * (\<bar>a\<bar> mod \<bar>b\<bar>)"
why3_open "int/ComputerDivision.xml"
constants
div = cdiv
mod = cmod
why3_vc Div_1 by (simp add: cdiv_def mult_sgn_abs)
why3_vc Div_inf using assms by (simp add: cdiv_def div_pos_pos_trivial)
why3_vc Div_sign_neg
using assms
by (cases "x = 0") (simp_all add: cdiv_def
zdiv_zminus1_eq_if div_nonpos_pos_le0 pos_imp_zdiv_neg_iff)