Commit ce10e4b3 authored by Stefan Berghofer's avatar Stefan Berghofer

Adapted to Isabelle2015

parent 2a7fc739
......@@ -616,15 +616,15 @@ else
ISABELLEVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEVERSION in
2014*)
2015*)
enable_isabelle_support=yes
AC_MSG_RESULT($ISABELLEVERSION)
;;
*)
AC_MSG_RESULT($ISABELLEVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle2013-2; Isabelle discarded)
reason_isabelle_support=" (need version 2013-2)"
AC_MSG_WARN(You need Isabelle2015; Isabelle discarded)
reason_isabelle_support=" (need version 2015)"
;;
esac
fi
......
......@@ -11,7 +11,7 @@ using ``Edit'' action in \texttt{why3ide}.
\subsection{Installation}
You need version Isabelle2014. Former versions are not supported.
You need version Isabelle2015. Former versions are not supported.
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
......@@ -20,7 +20,7 @@ and installation of \why, you must manually add the path
\end{verbatim}
into either the user file
\begin{verbatim}
.isabelle/Isabelle2014/etc/components
.isabelle/Isabelle2015/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
......
......@@ -147,8 +147,8 @@ theory set.Fset
end
theory number.Parity
syntax predicate even "<app><const name=\"Parity.even_odd_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.even_odd_class.odd\"/>%1</app>"
syntax predicate even "<app><const name=\"Parity.semiring_parity_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.semiring_parity_class.odd\"/>%1</app>"
end
theory number.Divisibility
......
......@@ -14,7 +14,7 @@ function usage()
echo
echo " Options are:"
echo " -b batch mode"
echo " -i NAME interactive mode using interface NAME"
echo " -i interactive mode"
echo
echo "Process files generated by Why3."
exit 1
......@@ -46,7 +46,7 @@ function make_theory()
## process command line
while getopts "bi:" OPT
while getopts "bi" OPT
do
case "$OPT" in
b)
......@@ -54,7 +54,6 @@ do
;;
i)
INTERACTIVE=true
INTERFACE="$OPTARG"
;;
\?)
usage
......@@ -75,23 +74,13 @@ if [ "$BATCH" = true ]; then
"$ISABELLE_PROCESS" -e "use_thy \"$NAME\";" -rq Why3
elif [ "$INTERACTIVE" = true ]; then
make_theory "$NAME"
case "$INTERFACE" in
emacs)
"$ISABELLE_TOOL" emacs -L Why3 "${NAME}.thy"
;;
jedit)
if [ -f "$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER" ]; then
"$ISABELLE_TOOL" java -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
"-settings=$(jvmpath "$JEDIT_SETTINGS")" "-server=$WHY3_JEDIT_SERVER" \
-reuseview -wait "$(jvmpath "${NAME}.thy")"
else
"$ISABELLE_TOOL" jedit -l Why3 "${NAME}.thy"
fi
;;
*)
fail "Unknown Isabelle interface: \"$INTERFACE\""
;;
esac
if [ -f "$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER" ]; then
"$ISABELLE_TOOL" java -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
"-settings=$(jvmpath "$JEDIT_SETTINGS")" "-server=$WHY3_JEDIT_SERVER" \
-reuseview -wait "$(jvmpath "${NAME}.thy")"
else
"$ISABELLE_TOOL" jedit -l Why3 "${NAME}.thy"
fi
else
usage
fi
......@@ -8,9 +8,9 @@ section {* Parity properties *}
why3_open "number/Parity.xml"
why3_vc even_def by (simp add: even_equiv_def)
why3_vc even_def by arith
why3_vc odd_def by (simp add: odd_equiv_def)
why3_vc odd_def by arith
why3_vc even_or_odd by auto
......@@ -98,9 +98,9 @@ why3_vc divides_mod_computer
by (simp add: cmod_def dvd_eq_mod_eq_0 zabs_def
zmod_zminus1_eq_if zmod_zminus2_eq_if)
why3_vc even_divides by (rule even_iff_2_dvd)
why3_vc even_divides ..
why3_vc odd_divides by (simp add: even_iff_2_dvd)
why3_vc odd_divides ..
why3_end
......@@ -277,14 +277,14 @@ proof -
from `prime (nat p)` have "0 \<le> p" by (simp add: prime_def)
from `prime (nat p)` have "2 \<le> nat p" by auto
with `prime (nat p)` `even p` `0 \<le> p` show ?thesis
by (auto simp add: order_le_less prime_odd_nat pos_int_even_equiv_nat_even)
by (auto simp add: order_le_less prime_odd_nat even_nat_iff [symmetric])
qed
why3_vc odd_prime
proof -
from `prime (nat p)` have "2 \<le> nat p" by auto
with `prime (nat p)` `3 \<le> p` show ?thesis
by (auto simp add: order_le_less prime_odd_nat pos_int_even_equiv_nat_even)
by (auto simp add: order_le_less prime_odd_nat even_nat_iff [symmetric])
qed
why3_end
......
......@@ -452,7 +452,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
true)
| SOME thms =>
if length thms = length ts andalso
forall (Pattern.matches thy o apfst prop_of) (thms ~~ ts)
forall (Pattern.matches thy o apfst Thm.prop_of) (thms ~~ ts)
then (thy, false)
else error ("Failed to match axiom " ^ string_of_id id))
| mk_decl realize (Typedecl ((s, id), args, opt_rhs)) thy =
......@@ -490,10 +490,10 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
add_const s,
true)
| SOME [th] =>
let val (s', _) = head_of_eqn' (prop_of th)
let val (s', _) = head_of_eqn' (Thm.prop_of th)
handle TERM _ => error ("Bad equation for " ^ string_of_id id)
in
if Pattern.matches thy (rename_const [(s', s)] (prop_of th), eqn)
if Pattern.matches thy (rename_const [(s', s)] (Thm.prop_of th), eqn)
then (add_const_raw NONE (s, s') thy, false)
else error ("Failed to match definition " ^ string_of_id id)
end
......@@ -502,7 +502,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
| mk_decl _ (Datatype dts) thy =
(case lookup_list (snd o #1) (lookup_type' thy) dts of
NONE =>
(thy |> Datatype.add_datatype Datatype_Aux.default_config
(thy |> BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]
(map (fn ((s, _), args, constrs) =>
((Binding.name s, map (rpair dummyS) args, NoSyn),
map (fn ((s', _), Ts) =>
......@@ -516,7 +516,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
in
(fold (fn (((s, id), args, constrs), s') =>
let
val (args', constrs') = Datatype.the_spec thy s';
val (args', constrs') = BNF_LFP_Compat.the_spec thy s';
fun err () = error ("Failed to match type " ^ string_of_id id);
val _ =
length args = length args' andalso
......@@ -551,16 +551,16 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
true)
| SOME preds' =>
let val cmap = map (fn (((s, id), _, _), th :: _) =>
(th |> concl_of |> HOLogic.dest_Trueprop |> head_of |>
(th |> Thm.concl_of |> HOLogic.dest_Trueprop |> head_of |>
dest_Const |> fst handle TERM _ =>
error ("Bad introduction rule for " ^ string_of_id id),
s)) preds'
in
app (fn (((_, id), _, intrs), intrs') =>
if length intrs = length intrs' andalso
forall2 (fn (_, t) => fn th =>
Pattern.matches thy (rename_const cmap (prop_of th), t))
intrs intrs'
ListPair.all (fn ((_, t), th) =>
Pattern.matches thy (rename_const cmap (Thm.prop_of th), t))
(intrs, intrs')
then ()
else error ("Failed to match predicate " ^ string_of_id id)) preds';
(fold (add_const_raw NONE o swap) cmap thy, false)
......@@ -578,15 +578,15 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
true)
| SOME eqnss'' =>
let val cmap = map2 (fn ((id, _), th :: _) => fn (s, _) =>
(th |> prop_of |> head_of_eqn' |> fst handle TERM _ =>
(th |> Thm.prop_of |> head_of_eqn' |> fst handle TERM _ =>
error ("Bad equation for " ^ string_of_id id),
s)) eqnss'' eqnss'
in
app (fn ((id, eqns), eqns') =>
if length eqns = length eqns' andalso
forall2 (fn t => fn th =>
Pattern.matches thy (rename_const cmap (prop_of th), t))
eqns eqns'
ListPair.all (fn (t, th) =>
Pattern.matches thy (rename_const cmap (Thm.prop_of th), t))
(eqns, eqns')
then ()
else error ("Failed to match function " ^ string_of_id id)) eqnss'';
(fold (add_const_raw NONE o swap) cmap thy, false)
......@@ -809,7 +809,7 @@ fun prove_vc vc_name lthy =
end;
val _ =
Outer_Syntax.command @{command_spec "why3_open"}
Outer_Syntax.command @{command_keyword "why3_open"}
"open a new Why3 environment and load a Why3-generated .xml file"
(Resources.provide_parse_files "why3_open" --
Scan.optional (Parse.reserved "constants" |-- Parse.!!! (Scan.repeat1
......@@ -819,13 +819,13 @@ val _ =
(Toplevel.theory o why3_open));
val _ =
Outer_Syntax.command @{command_spec "why3_vc"}
Outer_Syntax.command @{command_keyword "why3_vc"}
"enter into proof mode for a specific verification condition"
(Parse.name >> (fn name =>
(Toplevel.local_theory_to_proof NONE (prove_vc name))));
(Toplevel.local_theory_to_proof NONE NONE (prove_vc name))));
val _ =
Outer_Syntax.improper_command @{command_spec "why3_status"}
Outer_Syntax.command @{command_keyword "why3_status"}
"show the name and state of all loaded verification conditions"
(Scan.optional
(Args.parens
......@@ -835,34 +835,34 @@ val _ =
Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
val _ =
Outer_Syntax.command @{command_spec "why3_end"}
Outer_Syntax.command @{command_keyword "why3_end"}
"close the current Why3 environment"
(Scan.optional (@{keyword "("} |-- Parse.!!!
(Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
(Toplevel.theory o close));
val _ =
Outer_Syntax.command @{command_spec "why3_consts"}
Outer_Syntax.command @{command_keyword "why3_consts"}
"associate Why3 constants with constants"
(Scan.repeat1 (Parse.xname --| Args.$$$ "=" -- Parse.xname) >>
(Toplevel.theory o fold add_why3_const));
val _ =
Outer_Syntax.command @{command_spec "why3_types"}
Outer_Syntax.command @{command_keyword "why3_types"}
"associate Why3 types with types"
(Scan.repeat1 (Parse.xname --| Args.$$$ "=" -- Parse.xname) >>
(Toplevel.theory o fold add_why3_type));
val _ =
Outer_Syntax.command @{command_spec "why3_thms"}
Outer_Syntax.command @{command_keyword "why3_thms"}
"associate Why3 axioms with theorems"
(Parse.and_list1 (Parse.xname --| Args.$$$ "=" -- Parse_Spec.xthms1) >>
(Parse.and_list1 (Parse.xname --| Args.$$$ "=" -- Parse.xthms1) >>
(Toplevel.theory o fold add_why3_thm));
val _ =
Outer_Syntax.command @{command_spec "why3_defs"}
Outer_Syntax.command @{command_keyword "why3_defs"}
"associate Why3 definitions with definitions"
(Parse.and_list1 (Parse.xname --| Args.$$$ "=" -- Parse_Spec.xthms1) >>
(Parse.and_list1 (Parse.xname --| Args.$$$ "=" -- Parse.xthms1) >>
(Toplevel.theory o fold add_why3_def));
val setup = Theory.at_end (fn thy =>
......
......@@ -501,9 +501,9 @@ editor = "pvs"
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([^:]+\\)"
version_ok = "2014"
version_bad = "2013-2"
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
version_ok = "2015"
version_bad = "2014"
# not why3-cpulimit 0 %m because isabelle needs more memory at start-up
command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
driver = "drivers/isabelle.drv"
......@@ -525,11 +525,7 @@ command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq-tactic\\\" \\\"Why3\
[editor isabelle-jedit]
name = "Isabelle/jEdit"
command = "isabelle why3 -i jedit %f"
[editor proofgeneral-isabelle]
name = "Emacs/ProofGeneral/Isabelle"
command = "isabelle why3 -i emacs %f"
command = "isabelle why3 -i %f"
[editor altgr-ergo]
name = "AltGr-Ergo"
......
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