--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 05 09:49:03 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 05 14:36:17 2010 +0100
@@ -982,6 +982,20 @@
\item[\isa{expect}] can be used to check if the user's
expectation was met (\isa{no{\isacharunderscore}expectation}, \isa{no{\isacharunderscore}counterexample}, or \isa{counterexample}).
+ \item[timeout] sets the time limit in seconds.
+
+ \item[default\_type] sets the type(s) generally used to instantiate
+ type variables.
+
+ \item[report] if set quickcheck reports how many tests fulfilled
+ the preconditions.
+
+ \item[quiet] if not set quickcheck informs about the current size
+ for assignment values.
+
+ \item[expect] can be used to check if the user's expectation was met
+ (no\_expectation, no\_counterexample, or counterexample)
+
\end{description}
These option can be given within square brackets.
--- a/lib/scripts/feeder Fri Nov 05 09:49:03 2010 +0100
+++ b/lib/scripts/feeder Fri Nov 05 14:36:17 2010 +0100
@@ -16,7 +16,7 @@
echo "Usage: $PRG [OPTIONS]"
echo
echo " Options are:"
- echo " -h TEXT head text"
+ echo " -h TEXT head text (encoded as utf8)"
echo " -p emit my pid"
echo " -q do not pipe stdin"
echo " -t TEXT tail text"
--- a/lib/scripts/feeder.pl Fri Nov 05 09:49:03 2010 +0100
+++ b/lib/scripts/feeder.pl Fri Nov 05 14:36:17 2010 +0100
@@ -24,7 +24,11 @@
$emitpid && (print $$, "\n");
-$head && (print "$head", "\n");
+if ($head) {
+ utf8::encode($head);
+ $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
+ print $head, "\n";
+}
if (!$quit) {
while (<STDIN>) {
--- a/src/HOL/Groups.thy Fri Nov 05 09:49:03 2010 +0100
+++ b/src/HOL/Groups.thy Fri Nov 05 14:36:17 2010 +0100
@@ -284,6 +284,7 @@
finally show ?thesis .
qed
+
lemmas equals_zero_I = minus_unique (* legacy name *)
lemma minus_zero [simp]: "- 0 = 0"
@@ -305,6 +306,20 @@
finally show ?thesis .
qed
+subclass cancel_semigroup_add
+proof
+ fix a b c :: 'a
+ assume "a + b = a + c"
+ then have "- a + a + b = - a + a + c"
+ unfolding add_assoc by simp
+ then show "b = c" by simp
+next
+ fix a b c :: 'a
+ assume "b + a = c + a"
+ then have "b + a + - a = c + a + - a" by simp
+ then show "b = c" unfolding add_assoc by simp
+qed
+
lemma minus_add_cancel: "- a + (a + b) = b"
by (simp add: add_assoc [symmetric])
--- a/src/HOL/Imperative_HOL/Array.thy Fri Nov 05 09:49:03 2010 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy Fri Nov 05 14:36:17 2010 +0100
@@ -134,9 +134,13 @@
by (auto simp add: update_def set_set_swap list_update_swap)
lemma get_alloc:
- "get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'"
+ "get (snd (alloc xs h)) (fst (alloc ys h)) = xs"
by (simp add: Let_def split_def alloc_def)
+lemma length_alloc:
+ "length (snd (alloc (xs :: 'a::heap list) h)) (fst (alloc (ys :: 'a list) h)) = List.length xs"
+ by (simp add: Array.length_def get_alloc)
+
lemma set:
"set (fst (alloc ls h))
new_ls (snd (alloc ls h))
--- a/src/HOL/Imperative_HOL/Overview.thy Fri Nov 05 09:49:03 2010 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy Fri Nov 05 14:36:17 2010 +0100
@@ -31,7 +31,7 @@
realisation has changed since, due to both extensions and
refinements. Therefore this overview wants to present the framework
\qt{as it is} by now. It focusses on the user-view, less on matters
- of constructions. For details study of the theory sources is
+ of construction. For details study of the theory sources is
encouraged.
*}
@@ -41,7 +41,8 @@
text {*
Heaps (@{type heap}) can be populated by values of class @{class
heap}; HOL's default types are already instantiated to class @{class
- heap}.
+ heap}. Class @{class heap} is a subclass of @{class countable}; see
+ theory @{text Countable} for ways to instantiate types as @{class countable}.
The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
following specification:
@@ -100,7 +101,7 @@
provides a simple relational calculus. Primitive rules are @{text
crelI} and @{text crelE}, rules appropriate for reasoning about
- imperative operation are available in the @{text crel_intros} and
+ imperative operations are available in the @{text crel_intros} and
@{text crel_elims} fact collections.
Often non-failure of imperative computations does not depend
--- a/src/HOL/Library/State_Monad.thy Fri Nov 05 09:49:03 2010 +0100
+++ b/src/HOL/Library/State_Monad.thy Fri Nov 05 14:36:17 2010 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Combinator syntax for generic, open state monads (single threaded monads) *}
+header {* Combinator syntax for generic, open state monads (single-threaded monads) *}
theory State_Monad
imports Main Monad_Syntax
@@ -11,19 +11,18 @@
subsection {* Motivation *}
text {*
- The logic HOL has no notion of constructor classes, so
- it is not possible to model monads the Haskell way
- in full genericity in Isabelle/HOL.
+ The logic HOL has no notion of constructor classes, so it is not
+ possible to model monads the Haskell way in full genericity in
+ Isabelle/HOL.
- However, this theory provides substantial support for
- a very common class of monads: \emph{state monads}
- (or \emph{single-threaded monads}, since a state
- is transformed single-threaded).
+ However, this theory provides substantial support for a very common
+ class of monads: \emph{state monads} (or \emph{single-threaded
+ monads}, since a state is transformed single-threadedly).
To enter from the Haskell world,
- \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
- makes a good motivating start. Here we just sketch briefly
- how those monads enter the game of Isabelle/HOL.
+ \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} makes
+ a good motivating start. Here we just sketch briefly how those
+ monads enter the game of Isabelle/HOL.
*}
subsection {* State transformations and combinators *}
@@ -32,64 +31,66 @@
We classify functions operating on states into two categories:
\begin{description}
- \item[transformations]
- with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
+
+ \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
transforming a state.
- \item[``yielding'' transformations]
- with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
- ``yielding'' a side result while transforming a state.
- \item[queries]
- with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},
- computing a result dependent on a state.
+
+ \item[``yielding'' transformations] with type signature @{text "\<sigma>
+ \<Rightarrow> \<alpha> \<times> \<sigma>'"}, ``yielding'' a side result while transforming a
+ state.
+
+ \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a
+ result dependent on a state.
+
\end{description}
- By convention we write @{text "\<sigma>"} for types representing states
- and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"}
- for types representing side results. Type changes due
- to transformations are not excluded in our scenario.
+ By convention we write @{text "\<sigma>"} for types representing states and
+ @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types
+ representing side results. Type changes due to transformations are
+ not excluded in our scenario.
- We aim to assert that values of any state type @{text "\<sigma>"}
- are used in a single-threaded way: after application
- of a transformation on a value of type @{text "\<sigma>"}, the
- former value should not be used again. To achieve this,
- we use a set of monad combinators:
+ We aim to assert that values of any state type @{text "\<sigma>"} are used
+ in a single-threaded way: after application of a transformation on a
+ value of type @{text "\<sigma>"}, the former value should not be used
+ again. To achieve this, we use a set of monad combinators:
*}
notation fcomp (infixl "\<circ>>" 60)
notation scomp (infixl "\<circ>\<rightarrow>" 60)
-abbreviation (input)
- "return \<equiv> Pair"
-
text {*
- Given two transformations @{term f} and @{term g}, they
- may be directly composed using the @{term "op \<circ>>"} combinator,
- forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
+ Given two transformations @{term f} and @{term g}, they may be
+ directly composed using the @{term "op \<circ>>"} combinator, forming a
+ forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
After any yielding transformation, we bind the side result
- immediately using a lambda abstraction. This
- is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
- @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
+ immediately using a lambda abstraction. This is the purpose of the
+ @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')
+ = f s in g s')"}.
For queries, the existing @{term "Let"} is appropriate.
- Naturally, a computation may yield a side result by pairing
- it to the state from the left; we introduce the
- suggestive abbreviation @{term return} for this purpose.
+ Naturally, a computation may yield a side result by pairing it to
+ the state from the left; we introduce the suggestive abbreviation
+ @{term return} for this purpose.
- The most crucial distinction to Haskell is that we do
- not need to introduce distinguished type constructors
- for different kinds of state. This has two consequences:
+ The most crucial distinction to Haskell is that we do not need to
+ introduce distinguished type constructors for different kinds of
+ state. This has two consequences:
+
\begin{itemize}
- \item The monad model does not state anything about
- the kind of state; the model for the state is
- completely orthogonal and may be
- specified completely independently.
- \item There is no distinguished type constructor
- encapsulating away the state transformation, i.e.~transformations
- may be applied directly without using any lifting
- or providing and dropping units (``open monad'').
+
+ \item The monad model does not state anything about the kind of
+ state; the model for the state is completely orthogonal and may
+ be specified completely independently.
+
+ \item There is no distinguished type constructor encapsulating
+ away the state transformation, i.e.~transformations may be
+ applied directly without using any lifting or providing and
+ dropping units (``open monad'').
+
\item The type of states may change due to a transformation.
+
\end{itemize}
*}
@@ -97,8 +98,8 @@
subsection {* Monad laws *}
text {*
- The common monadic laws hold and may also be used
- as normalization rules for monadic expressions:
+ The common monadic laws hold and may also be used as normalization
+ rules for monadic expressions:
*}
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
@@ -145,7 +146,7 @@
"_sdo_block (_sdo_final e)" => "e"
text {*
- For an example, see HOL/Extraction/Higman.thy.
+ For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}.
*}
end
--- a/src/HOL/List.thy Fri Nov 05 09:49:03 2010 +0100
+++ b/src/HOL/List.thy Fri Nov 05 14:36:17 2010 +0100
@@ -1298,6 +1298,15 @@
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
by (induct xs) auto
+lemma concat_eq_concat_iff: "\<forall>(x, y) \<in> set (zip xs ys). length x = length y ==> length xs = length ys ==> (concat xs = concat ys) = (xs = ys)"
+proof (induct xs arbitrary: ys)
+ case (Cons x xs ys)
+ thus ?case by (cases ys) auto
+qed (auto)
+
+lemma concat_injective: "concat xs = concat ys ==> length xs = length ys ==> \<forall>(x, y) \<in> set (zip xs ys). length x = length y ==> xs = ys"
+by (simp add: concat_eq_concat_iff)
+
subsubsection {* @{text nth} *}
--- a/src/HOL/Proofs/Extraction/Higman.thy Fri Nov 05 09:49:03 2010 +0100
+++ b/src/HOL/Proofs/Extraction/Higman.thy Fri Nov 05 14:36:17 2010 +0100
@@ -352,11 +352,11 @@
function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
"mk_word_aux k = exec {
i \<leftarrow> Random.range 10;
- (if i > 7 \<and> k > 2 \<or> k > 1000 then return []
+ (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
else exec {
let l = (if i mod 2 = 0 then A else B);
ls \<leftarrow> mk_word_aux (Suc k);
- return (l # ls)
+ Pair (l # ls)
})}"
by pat_completeness auto
termination by (relation "measure ((op -) 1001)") auto
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Nov 05 09:49:03 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Nov 05 14:36:17 2010 +0100
@@ -437,15 +437,16 @@
|> Config.put oracle false
|> Config.put filter_only true
|> Config.put keep_assms false
+ val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
val cprop =
- Thm.cprem_of goal i
- |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt
+ concl
+ |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt'
|> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
- val irs = map (pair ~1) (Thm.assume cprop :: facts)
+ val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
val rm = SOME run_remote
in
split_list xrules
- ||> distinct (op =) o fst o smt_solver rm ctxt o append irs o map_index I
+ ||> distinct (op =) o fst o smt_solver rm ctxt' o append irs o map_index I
|-> map_filter o try o nth
|> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
end
--- a/src/Pure/Isar/code.ML Fri Nov 05 09:49:03 2010 +0100
+++ b/src/Pure/Isar/code.ML Fri Nov 05 14:36:17 2010 +0100
@@ -124,11 +124,23 @@
of SOME c_ty => c_ty
| NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
-fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
+fun check_unoverload thy (c, ty) =
+ let
+ val c' = AxClass.unoverload_const thy (c, ty);
+ val ty_decl = Sign.the_const_type thy c';
+ in if Sign.typ_equiv thy
+ (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty)) then c'
+ else error ("Type\n" ^ string_of_typ thy ty
+ ^ "\nof constant " ^ quote c
+ ^ "\nis too specific compared to declared type\n"
+ ^ string_of_typ thy ty_decl)
+ end;
+
+fun check_const thy = check_unoverload thy o check_bare_const thy;
fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
-fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
+fun read_const thy = check_unoverload thy o read_bare_const thy;
(** data store **)
@@ -471,7 +483,7 @@
in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then ()
else bad_thm ("Type\n" ^ string_of_typ thy ty
^ "\nof constant " ^ quote c
- ^ "\nis incompatible with declared type\n"
+ ^ "\nis too specific compared to declared type\n"
^ string_of_typ thy ty_decl)
end;
--- a/src/Pure/ML-Systems/timing.ML Fri Nov 05 09:49:03 2010 +0100
+++ b/src/Pure/ML-Systems/timing.ML Fri Nov 05 14:36:17 2010 +0100
@@ -1,10 +1,10 @@
(* Title: Pure/ML-Systems/timing.ML
Author: Makarius
-Basic support for timing.
+Basic support for time measurement.
*)
-fun seconds s = Time.fromNanoseconds (Real.ceil (s * 1E9));
+val seconds = Time.fromReal;
fun start_timing () =
let
--- a/src/Pure/ML/ml_lex.ML Fri Nov 05 09:49:03 2010 +0100
+++ b/src/Pure/ML/ml_lex.ML Fri Nov 05 14:36:17 2010 +0100
@@ -70,17 +70,18 @@
fun content_of (Token (_, (_, x))) = x;
fun token_leq (tok, tok') = content_of tok <= content_of tok';
+fun warn tok =
+ (case tok of
+ Token (_, (Keyword, ":>")) =>
+ warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
+ \prefer non-opaque matching (:) possibly with abstype" ^
+ Position.str_of (pos_of tok))
+ | _ => ());
+
fun check_content_of tok =
(case kind_of tok of
Error msg => error msg
- | _ =>
- (case tok of
- Token (_, (Keyword, ":>")) =>
- warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
- \prefer non-opaque matching (:) possibly with abstype" ^
- Position.str_of (pos_of tok))
- | _ => ();
- content_of tok));
+ | _ => content_of tok);
val flatten = implode o map (Symbol.escape o check_content_of);
@@ -288,7 +289,7 @@
|> Source.exhaust
|> tap (List.app (Antiquote.report report_token))
|> tap Antiquote.check_nesting
- |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
+ |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
handle ERROR msg =>
cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
in input @ termination end;
--- a/src/Tools/jEdit/plugin/Isabelle.props Fri Nov 05 09:49:03 2010 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props Fri Nov 05 14:36:17 2010 +0100
@@ -29,6 +29,8 @@
options.isabelle.relative-font-size=100
options.isabelle.tooltip-font-size.title=Tooltip Font Size
options.isabelle.tooltip-font-size=10
+options.isabelle.tooltip-margin.title=Tooltip Margin
+options.isabelle.tooltip-margin=40
options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
options.isabelle.tooltip-dismiss-delay=8000
options.isabelle.startup-timeout=10000
--- a/src/Tools/jEdit/src/jedit/document_view.scala Fri Nov 05 09:49:03 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Fri Nov 05 14:36:17 2010 +0100
@@ -165,6 +165,8 @@
/* CONTROL-mouse management */
+ private var control: Boolean = false
+
private def exit_control()
{
exit_popup()
@@ -184,7 +186,7 @@
private val mouse_motion_listener = new MouseMotionAdapter {
override def mouseMoved(e: MouseEvent) {
- val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+ control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
val x = e.getX()
val y = e.getY()
@@ -288,10 +290,20 @@
Isabelle.swing_buffer_lock(model.buffer) {
val snapshot = model.snapshot()
val offset = text_area.xyToOffset(x, y)
- snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
- {
- case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
- case _ => null
+ if (control) {
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+ case _ => null
+ }
+ }
+ else {
+ // FIXME snapshot.cumulate
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+ case _ => null
+ }
}
}
}
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Fri Nov 05 09:49:03 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Fri Nov 05 14:36:17 2010 +0100
@@ -84,10 +84,11 @@
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
}
- val popup: Markup_Tree.Select[XML.Tree] =
+ val popup: Markup_Tree.Select[String] =
{
case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
- if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => msg
+ if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
+ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
}
val gutter_message: Markup_Tree.Select[Icon] =
@@ -109,7 +110,8 @@
val tooltip: Markup_Tree.Select[String] =
{
case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
- Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), margin = 40)
+ Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
+ margin = Isabelle.Int_Property("tooltip-margin"))
case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Fri Nov 05 09:49:03 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Fri Nov 05 14:36:17 2010 +0100
@@ -20,6 +20,7 @@
private val auto_start = new CheckBox()
private val relative_font_size = new JSpinner()
private val tooltip_font_size = new JSpinner()
+ private val tooltip_margin = new JSpinner()
private val tooltip_dismiss_delay = new JSpinner()
override def _init()
@@ -35,6 +36,9 @@
tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
+ tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
+ addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
+
tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
}
@@ -51,6 +55,9 @@
Isabelle.Int_Property("tooltip-font-size") =
tooltip_font_size.getValue().asInstanceOf[Int]
+ Isabelle.Int_Property("tooltip-margin") =
+ tooltip_margin.getValue().asInstanceOf[Int]
+
Isabelle.Int_Property("tooltip-dismiss-delay") =
tooltip_dismiss_delay.getValue().asInstanceOf[Int]
}
--- a/src/Tools/nbe.ML Fri Nov 05 09:49:03 2010 +0100
+++ b/src/Tools/nbe.ML Fri Nov 05 14:36:17 2010 +0100
@@ -64,7 +64,7 @@
val lhs_rhs = case try Logic.dest_equals eqn
of SOME lhs_rhs => lhs_rhs
| _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
- val c_c' = case try (pairself (Code.check_const thy)) lhs_rhs
+ val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
of SOME c_c' => c_c'
| _ => error ("Not an equation with two constants: "
^ Syntax.string_of_term_global thy eqn);
--- a/src/Tools/quickcheck.ML Fri Nov 05 09:49:03 2010 +0100
+++ b/src/Tools/quickcheck.ML Fri Nov 05 14:36:17 2010 +0100
@@ -16,12 +16,12 @@
datatype expectation = No_Expectation | No_Counterexample | Counterexample;
datatype test_params = Test_Params of
{ size: int, iterations: int, default_type: typ list, no_assms: bool,
- expect : expectation, report: bool, quiet : bool, timeout : int};
+ expect : expectation, report: bool, quiet : bool, timeout : real};
val test_params_of : Proof.context -> test_params
val report : Proof.context -> bool
val map_test_params :
- ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * int)))
- -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * int))))
+ ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real)))
+ -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real))))
-> Context.generic -> Context.generic
val add_generator:
string * (Proof.context -> term -> int -> term list option * (bool list * bool))
@@ -81,7 +81,7 @@
datatype test_params = Test_Params of
{ size: int, iterations: int, default_type: typ list, no_assms: bool,
- expect : expectation, report: bool, quiet : bool, timeout : int};
+ expect : expectation, report: bool, quiet : bool, timeout : real};
fun dest_test_params
(Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
@@ -105,7 +105,7 @@
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
((merge_expectation (expect1, expect2), report1 orelse report2),
- (quiet1 orelse quiet2, Int.min (timeout1, timeout2)))));
+ (quiet1 orelse quiet2, Real.min (timeout1, timeout2)))));
structure Data = Generic_Data
(
@@ -114,7 +114,7 @@
* test_params;
val empty = ([], Test_Params
{ size = 10, iterations = 100, default_type = [], no_assms = false,
- expect = No_Expectation, report = false, quiet = false, timeout = 30});
+ expect = No_Expectation, report = false, quiet = false, timeout = 30.0});
val extend = I;
fun merge ((generators1, params1), (generators2, params2)) : T =
(AList.merge (op =) (K true) (generators1, generators2),
@@ -200,6 +200,9 @@
fun test_term ctxt generator_name t =
let
val (names, t') = prep_test_term t;
+ val current_size = Unsynchronized.ref 0
+ fun excipit s =
+ "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
val (testers, comp_time) = cpu_time "quickcheck compilation"
(fn () => (case generator_name
of NONE => if quiet ctxt then mk_testers ctxt t' else mk_testers_strict ctxt t'
@@ -225,15 +228,18 @@
else
(if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
let
+ val _ = current_size := k
val (result, new_report) = with_testers k testers
val reports = ((k, new_report) :: reports)
in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
val ((result, reports), exec_time) =
- TimeLimit.timeLimit (Time.fromSeconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution"
+ TimeLimit.timeLimit (seconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution"
(fn () => apfst
(fn result => case result of NONE => NONE
| SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
- handle TimeLimit.TimeOut => error "Reached timeout during Quickcheck"
+ handle TimeLimit.TimeOut =>
+ error (excipit "ran out of time")
+ | Exn.Interrupt => error (excipit "was interrupted")
in
(result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
end;
@@ -367,6 +373,11 @@
| read_bool "true" = true
| read_bool s = error ("Not a Boolean value: " ^ s)
+fun read_real s =
+ case (Real.fromString s) of
+ SOME s => s
+ | NONE => error ("Not a real number: " ^ s)
+
fun read_expectation "no_expectation" = No_Expectation
| read_expectation "no_counterexample" = No_Counterexample
| read_expectation "counterexample" = Counterexample
@@ -387,7 +398,7 @@
| parse_test_param ctxt ("quiet", [arg]) =
(apsnd o apsnd o apsnd o apfst o K) (read_bool arg)
| parse_test_param ctxt ("timeout", [arg]) =
- (apsnd o apsnd o apsnd o apsnd o K) (read_nat arg)
+ (apsnd o apsnd o apsnd o apsnd o K) (read_real arg)
| parse_test_param ctxt (name, _) =
error ("Unknown test parameter: " ^ name);
@@ -431,7 +442,7 @@
|> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state) false;
val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |--
- ((Parse.name >> single) || (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
+ (((Parse.name || Parse.float_number) >> single) || (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
val parse_args = Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]"
|| Scan.succeed [];