--- a/CONTRIBUTORS Sat Apr 25 21:42:05 2009 +0200
+++ b/CONTRIBUTORS Sat Apr 25 22:29:13 2009 +0200
@@ -7,6 +7,10 @@
Contributions to this Isabelle version
--------------------------------------
+
+Contributions to Isabelle2009
+-----------------------------
+
* March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
Cambridge
Elementary topology in Euclidean space.
--- a/contrib/SystemOnTPTP/remote Sat Apr 25 21:42:05 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-#!/usr/bin/env perl
-#
-# Wrapper for custom remote provers on SystemOnTPTP
-# Author: Fabian Immler, TU Muenchen
-#
-
-use warnings;
-use strict;
-use Getopt::Std;
-use HTTP::Request::Common;
-use LWP;
-
-my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
-
-# default parameters
-my %URLParameters = (
- "NoHTML" => 1,
- "QuietFlag" => "-q01",
- "X2TPTP" => "-S",
- "SubmitButton" => "RunSelectedSystems",
- "ProblemSource" => "UPLOAD",
- );
-
-#----Get format and transform options if specified
-my %Options;
-getopts("hws:t:c:",\%Options);
-
-#----Usage
-sub usage() {
- print("Usage: remote [<options>] <File name>\n");
- print(" <options> are ...\n");
- print(" -h - print this help\n");
- print(" -w - list available ATP systems\n");
- print(" -s<system> - specified system to use\n");
- print(" -t<timelimit> - CPU time limit for system\n");
- print(" -c<command> - custom command for system\n");
- print(" <File name> - TPTP problem file\n");
- exit(0);
-}
-if (exists($Options{'h'})) {
- usage();
-}
-#----What systems flag
-if (exists($Options{'w'})) {
- $URLParameters{"SubmitButton"} = "ListSystems";
- delete($URLParameters{"ProblemSource"});
-}
-#----Selected system
-my $System;
-if (exists($Options{'s'})) {
- $System = $Options{'s'};
-} else {
- # use Vampire as default
- $System = "Vampire---9.0";
-}
-$URLParameters{"System___$System"} = $System;
-
-#----Time limit
-if (exists($Options{'t'})) {
- $URLParameters{"TimeLimit___$System"} = $Options{'t'};
-}
-#----Custom command
-if (exists($Options{'c'})) {
- $URLParameters{"Command___$System"} = $Options{'c'};
-}
-
-#----Get single file name
-if (exists($URLParameters{"ProblemSource"})) {
- if (scalar(@ARGV) >= 1) {
- $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
- } else {
- print("Missing problem file\n");
- usage();
- die;
- }
-}
-
-# Query Server
-my $Agent = LWP::UserAgent->new;
-if (exists($Options{'t'})) {
- # give server more time to respond
- $Agent->timeout($Options{'t'} + 10);
-}
-my $Request = POST($SystemOnTPTPFormReplyURL,
- Content_Type => 'form-data',Content => \%URLParameters);
-my $Response = $Agent->request($Request);
-
-#catch errors / failure
-if(! $Response->is_success){
- print "HTTP-Error: " . $Response->message . "\n";
- exit(-1);
-} elsif (exists($Options{'w'})) {
- print $Response->content;
- exit (0);
-} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
- print "Specified System $1 does not exist\n";
- exit(-1);
-} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) {
- my @lines = split( /\n/, $Response->content);
- my $extract = "";
- foreach my $line (@lines){
- #ignore comments
- if ($line !~ /^%/ && !($line eq "")) {
- $extract .= "$line";
- }
- }
- # insert newlines after ').'
- $extract =~ s/\s//g;
- $extract =~ s/\)\.cnf/\)\.\ncnf/g;
-
- # orientation for res_reconstruct.ML
- print "# SZS output start CNFRefutation.\n";
- print "$extract\n";
- print "# SZS output end CNFRefutation.\n";
- exit(0);
-} else {
- print "Remote-script could not extract proof:\n".$Response->content;
- exit(-1);
-}
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/SystemOnTPTP Sat Apr 25 22:29:13 2009 +0200
@@ -0,0 +1,120 @@
+#!/usr/bin/env perl
+#
+# Wrapper for custom remote provers on SystemOnTPTP
+# Author: Fabian Immler, TU Muenchen
+#
+
+use warnings;
+use strict;
+use Getopt::Std;
+use HTTP::Request::Common;
+use LWP;
+
+my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
+
+# default parameters
+my %URLParameters = (
+ "NoHTML" => 1,
+ "QuietFlag" => "-q01",
+ "X2TPTP" => "-S",
+ "SubmitButton" => "RunSelectedSystems",
+ "ProblemSource" => "UPLOAD",
+ );
+
+#----Get format and transform options if specified
+my %Options;
+getopts("hws:t:c:",\%Options);
+
+#----Usage
+sub usage() {
+ print("Usage: remote [<options>] <File name>\n");
+ print(" <options> are ...\n");
+ print(" -h - print this help\n");
+ print(" -w - list available ATP systems\n");
+ print(" -s<system> - specified system to use\n");
+ print(" -t<timelimit> - CPU time limit for system\n");
+ print(" -c<command> - custom command for system\n");
+ print(" <File name> - TPTP problem file\n");
+ exit(0);
+}
+if (exists($Options{'h'})) {
+ usage();
+}
+#----What systems flag
+if (exists($Options{'w'})) {
+ $URLParameters{"SubmitButton"} = "ListSystems";
+ delete($URLParameters{"ProblemSource"});
+}
+#----Selected system
+my $System;
+if (exists($Options{'s'})) {
+ $System = $Options{'s'};
+} else {
+ # use Vampire as default
+ $System = "Vampire---9.0";
+}
+$URLParameters{"System___$System"} = $System;
+
+#----Time limit
+if (exists($Options{'t'})) {
+ $URLParameters{"TimeLimit___$System"} = $Options{'t'};
+}
+#----Custom command
+if (exists($Options{'c'})) {
+ $URLParameters{"Command___$System"} = $Options{'c'};
+}
+
+#----Get single file name
+if (exists($URLParameters{"ProblemSource"})) {
+ if (scalar(@ARGV) >= 1) {
+ $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
+ } else {
+ print("Missing problem file\n");
+ usage();
+ die;
+ }
+}
+
+# Query Server
+my $Agent = LWP::UserAgent->new;
+if (exists($Options{'t'})) {
+ # give server more time to respond
+ $Agent->timeout($Options{'t'} + 10);
+}
+my $Request = POST($SystemOnTPTPFormReplyURL,
+ Content_Type => 'form-data',Content => \%URLParameters);
+my $Response = $Agent->request($Request);
+
+#catch errors / failure
+if(! $Response->is_success){
+ print "HTTP-Error: " . $Response->message . "\n";
+ exit(-1);
+} elsif (exists($Options{'w'})) {
+ print $Response->content;
+ exit (0);
+} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
+ print "Specified System $1 does not exist\n";
+ exit(-1);
+} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) {
+ my @lines = split( /\n/, $Response->content);
+ my $extract = "";
+ foreach my $line (@lines){
+ #ignore comments
+ if ($line !~ /^%/ && !($line eq "")) {
+ $extract .= "$line";
+ }
+ }
+ # insert newlines after ').'
+ $extract =~ s/\s//g;
+ $extract =~ s/\)\.cnf/\)\.\ncnf/g;
+
+ # orientation for res_reconstruct.ML
+ print "# SZS output start CNFRefutation.\n";
+ print "$extract\n";
+ print "# SZS output end CNFRefutation.\n";
+ exit(0);
+} else {
+ print "Remote-script could not extract proof:\n".$Response->content;
+ exit(-1);
+}
+
--- a/src/HOL/HOL.thy Sat Apr 25 21:42:05 2009 +0200
+++ b/src/HOL/HOL.thy Sat Apr 25 22:29:13 2009 +0200
@@ -8,6 +8,7 @@
imports Pure "~~/src/Tools/Code_Generator"
uses
("Tools/hologic.ML")
+ "~~/src/Tools/auto_solve.ML"
"~~/src/Tools/IsaPlanner/zipper.ML"
"~~/src/Tools/IsaPlanner/isand.ML"
"~~/src/Tools/IsaPlanner/rw_tools.ML"
@@ -1921,7 +1922,7 @@
quickcheck_params [size = 5, iterations = 50]
-subsection {* Nitpick hooks *}
+subsection {* Nitpick setup *}
text {* This will be relocated once Nitpick is moved to HOL. *}
@@ -1947,10 +1948,14 @@
val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
)
*}
-setup {* Nitpick_Const_Def_Thms.setup
- #> Nitpick_Const_Simp_Thms.setup
- #> Nitpick_Const_Psimp_Thms.setup
- #> Nitpick_Ind_Intro_Thms.setup *}
+
+setup {*
+ Nitpick_Const_Def_Thms.setup
+ #> Nitpick_Const_Simp_Thms.setup
+ #> Nitpick_Const_Psimp_Thms.setup
+ #> Nitpick_Ind_Intro_Thms.setup
+*}
+
subsection {* Legacy tactics and ML bindings *}
--- a/src/HOL/IsaMakefile Sat Apr 25 21:42:05 2009 +0200
+++ b/src/HOL/IsaMakefile Sat Apr 25 22:29:13 2009 +0200
@@ -89,6 +89,7 @@
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/zipper.ML \
$(SRC)/Tools/atomize_elim.ML \
+ $(SRC)/Tools/auto_solve.ML \
$(SRC)/Tools/code/code_haskell.ML \
$(SRC)/Tools/code/code_ml.ML \
$(SRC)/Tools/code/code_name.ML \
--- a/src/HOL/Tools/atp_manager.ML Sat Apr 25 21:42:05 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML Sat Apr 25 22:29:13 2009 +0200
@@ -51,15 +51,17 @@
fun set_timeout time = CRITICAL (fn () => timeout := time);
val _ =
- ProofGeneralPgip.add_preference "Proof"
+ ProofGeneralPgip.add_preference Preferences.category_proof
(Preferences.string_pref atps
"ATP: provers" "Default automatic provers (separated by whitespace)");
-val _ = ProofGeneralPgip.add_preference "Proof"
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_proof
(Preferences.int_pref max_atps
"ATP: maximum number" "How many provers may run in parallel");
-val _ = ProofGeneralPgip.add_preference "Proof"
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_proof
(Preferences.int_pref timeout
"ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
--- a/src/HOL/Tools/atp_wrapper.ML Sat Apr 25 21:42:05 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Sat Apr 25 22:29:13 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/atp_wrapper.ML
- ID: $Id$
Author: Fabian Immler, TU Muenchen
Wrapper functions for external ATPs.
@@ -179,7 +178,7 @@
fun remote_prover_opts max_new theory_const args timeout =
tptp_prover_opts max_new theory_const
- (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int timeout)
+ (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", args ^ " -t " ^ string_of_int timeout)
timeout;
val remote_prover = remote_prover_opts 60 false;
--- a/src/Pure/IsaMakefile Sat Apr 25 21:42:05 2009 +0200
+++ b/src/Pure/IsaMakefile Sat Apr 25 22:29:13 2009 +0200
@@ -40,9 +40,8 @@
Pure: $(OUT)/Pure
-$(OUT)/Pure: $(BOOTSTRAP_FILES) \
- Concurrent/ROOT.ML Concurrent/future.ML \
- Concurrent/mailbox.ML Concurrent/par_list.ML \
+$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/ROOT.ML \
+ Concurrent/future.ML Concurrent/mailbox.ML Concurrent/par_list.ML \
Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \
Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \
General/alist.ML General/antiquote.ML General/balanced_tree.ML \
@@ -87,7 +86,7 @@
Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \
Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML \
- Tools/auto_solve.ML Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \
+ Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \
Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \
conjunction.ML consts.ML context.ML context_position.ML conv.ML \
defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \
--- a/src/Pure/ProofGeneral/ROOT.ML Sat Apr 25 21:42:05 2009 +0200
+++ b/src/Pure/ProofGeneral/ROOT.ML Sat Apr 25 22:29:13 2009 +0200
@@ -14,11 +14,7 @@
use "pgip_isabelle.ML";
-(use
- |> setmp Proofterm.proofs 1
- |> setmp quick_and_dirty true
- |> setmp Quickcheck.auto true
- |> setmp auto_solve true) "preferences.ML";
+use "preferences.ML";
use "pgip_parser.ML";
--- a/src/Pure/ProofGeneral/preferences.ML Sat Apr 25 21:42:05 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Sat Apr 25 22:29:13 2009 +0200
@@ -6,6 +6,10 @@
signature PREFERENCES =
sig
+ val category_display: string
+ val category_advanced_display: string
+ val category_tracing: string
+ val category_proof: string
type preference =
{name: string,
descr: string,
@@ -29,6 +33,14 @@
structure Preferences: PREFERENCES =
struct
+(* categories *)
+
+val category_display = "Display";
+val category_advanced_display = "Advanced Display";
+val category_tracing = "Tracing";
+val category_proof = "Proof"
+
+
(* preferences and preference tables *)
type preference =
@@ -66,11 +78,11 @@
(* preferences of Pure *)
-val proof_pref =
+val proof_pref = setmp Proofterm.proofs 1 (fn () =>
let
fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
- in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end;
+ in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
val thm_depsN = "thm_deps";
val thm_deps_pref =
@@ -145,24 +157,13 @@
bool_pref Toplevel.debug
"debugging"
"Whether to enable debugging.",
- bool_pref Quickcheck.auto
- "auto-quickcheck"
- "Whether to enable quickcheck automatically.",
- nat_pref Quickcheck.auto_time_limit
- "auto-quickcheck-time-limit"
- "Time limit for automatic quickcheck (in milliseconds).",
- bool_pref AutoSolve.auto
- "auto-solve"
- "Try to solve newly declared lemmas with existing theorems.",
- nat_pref AutoSolve.auto_time_limit
- "auto-solve-time-limit"
- "Time limit for seeking automatic solutions (in milliseconds).",
thm_deps_pref];
val proof_preferences =
- [bool_pref quick_and_dirty
- "quick-and-dirty"
- "Take a few short cuts",
+ [setmp quick_and_dirty true (fn () =>
+ bool_pref quick_and_dirty
+ "quick-and-dirty"
+ "Take a few short cuts") (),
bool_pref Toplevel.skip_proofs
"skip-proofs"
"Skip over proofs (interactive-only)",
@@ -175,10 +176,10 @@
"Check proofs in parallel"];
val pure_preferences =
- [("Display", display_preferences),
- ("Advanced Display", advanced_display_preferences),
- ("Tracing", tracing_preferences),
- ("Proof", proof_preferences)];
+ [(category_display, display_preferences),
+ (category_advanced_display, advanced_display_preferences),
+ (category_tracing, tracing_preferences),
+ (category_proof, proof_preferences)];
(* table of categories and preferences; names must be unique *)
--- a/src/Pure/Tools/ROOT.ML Sat Apr 25 21:42:05 2009 +0200
+++ b/src/Pure/Tools/ROOT.ML Sat Apr 25 22:29:13 2009 +0200
@@ -1,23 +1,9 @@
-(* Title: Pure/Tools/ROOT.ML
-
-Miscellaneous tools and packages for Pure Isabelle.
-*)
+(* Miscellaneous tools and packages for Pure Isabelle *)
use "named_thms.ML";
-(*basic XML support*)
use "xml_syntax.ML";
use "find_theorems.ML";
use "find_consts.ML";
-use "auto_solve.ML";
-
-(*quickcheck stub needed here because of pg preferences*)
-structure Quickcheck =
-struct
-
-val auto = ref false;
-val auto_time_limit = ref 5000;
-
-end;
--- a/src/Pure/Tools/auto_solve.ML Sat Apr 25 21:42:05 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-(* Title: Tools/auto_solve.ML
- Author: Timothy Bourke and Gerwin Klein, NICTA
-
-Check whether a newly stated theorem can be solved directly by an
-existing theorem. Duplicate lemmas can be detected in this way.
-
-The implementation is based in part on Berghofer and Haftmann's
-quickcheck.ML. It relies critically on the FindTheorems solves
-feature.
-*)
-
-signature AUTO_SOLVE =
-sig
- val auto : bool ref
- val auto_time_limit : int ref
- val limit : int ref
-
- val seek_solution : bool -> Proof.state -> Proof.state
-end;
-
-structure AutoSolve : AUTO_SOLVE =
-struct
-
-val auto = ref false;
-val auto_time_limit = ref 2500;
-val limit = ref 5;
-
-fun seek_solution int state =
- let
- val ctxt = Proof.context_of state;
-
- val crits = [(true, FindTheorems.Solves)];
- fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
-
- fun prt_result (goal, results) =
- let
- val msg =
- (case goal of
- NONE => "The current goal"
- | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
- in
- Pretty.big_list
- (msg ^ " could be solved directly with:")
- (map (FindTheorems.pretty_thm ctxt) results)
- end;
-
- fun seek_against_goal () =
- (case try Proof.get_goal state of
- NONE => NONE
- | SOME (_, (_, goal)) =>
- let
- val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
- val rs =
- if length subgoals = 1
- then [(NONE, find goal)]
- else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
- val results = filter_out (null o snd) rs;
- in if null results then NONE else SOME results end);
-
- fun go () =
- let
- val res =
- TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
- (try seek_against_goal) ();
- in
- (case res of
- SOME (SOME results) =>
- state |> Proof.goal_message
- (fn () => Pretty.chunks
- [Pretty.str "",
- Pretty.markup Markup.hilite
- (separate (Pretty.brk 0) (map prt_result results))])
- | _ => state)
- end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
- in
- if int andalso ! auto andalso not (! Toplevel.quiet)
- then go ()
- else state
- end;
-
-end;
-
-val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
-
-val auto_solve = AutoSolve.auto;
-val auto_solve_time_limit = AutoSolve.auto_time_limit;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/auto_solve.ML Sat Apr 25 22:29:13 2009 +0200
@@ -0,0 +1,101 @@
+(* Title: Tools/auto_solve.ML
+ Author: Timothy Bourke and Gerwin Klein, NICTA
+
+Check whether a newly stated theorem can be solved directly by an
+existing theorem. Duplicate lemmas can be detected in this way.
+
+The implementation is based in part on Berghofer and Haftmann's
+quickcheck.ML. It relies critically on the FindTheorems solves
+feature.
+*)
+
+signature AUTO_SOLVE =
+sig
+ val auto : bool ref
+ val auto_time_limit : int ref
+ val limit : int ref
+end;
+
+structure AutoSolve : AUTO_SOLVE =
+struct
+
+(* preferences *)
+
+val auto = ref false;
+val auto_time_limit = ref 2500;
+val limit = ref 5;
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (setmp auto true (fn () =>
+ Preferences.bool_pref auto
+ "auto-solve"
+ "Try to solve newly declared lemmas with existing theorems.") ());
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (Preferences.nat_pref auto_time_limit
+ "auto-solve-time-limit"
+ "Time limit for seeking automatic solutions (in milliseconds).");
+
+
+(* hook *)
+
+val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
+ let
+ val ctxt = Proof.context_of state;
+
+ val crits = [(true, FindTheorems.Solves)];
+ fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
+
+ fun prt_result (goal, results) =
+ let
+ val msg =
+ (case goal of
+ NONE => "The current goal"
+ | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
+ in
+ Pretty.big_list
+ (msg ^ " could be solved directly with:")
+ (map (FindTheorems.pretty_thm ctxt) results)
+ end;
+
+ fun seek_against_goal () =
+ (case try Proof.get_goal state of
+ NONE => NONE
+ | SOME (_, (_, goal)) =>
+ let
+ val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
+ val rs =
+ if length subgoals = 1
+ then [(NONE, find goal)]
+ else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
+ val results = filter_out (null o snd) rs;
+ in if null results then NONE else SOME results end);
+
+ fun go () =
+ let
+ val res =
+ TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
+ (try seek_against_goal) ();
+ in
+ (case res of
+ SOME (SOME results) =>
+ state |> Proof.goal_message
+ (fn () => Pretty.chunks
+ [Pretty.str "",
+ Pretty.markup Markup.hilite
+ (separate (Pretty.brk 0) (map prt_result results))])
+ | _ => state)
+ end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
+ in
+ if int andalso ! auto andalso not (! Toplevel.quiet)
+ then go ()
+ else state
+ end));
+
+end;
+
+val auto_solve = AutoSolve.auto;
+val auto_solve_time_limit = AutoSolve.auto_time_limit;
+
--- a/src/Tools/quickcheck.ML Sat Apr 25 21:42:05 2009 +0200
+++ b/src/Tools/quickcheck.ML Sat Apr 25 22:29:13 2009 +0200
@@ -6,16 +6,34 @@
signature QUICKCHECK =
sig
- val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option;
- val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
val auto: bool ref
val auto_time_limit: int ref
+ val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
+ (string * term) list option
+ val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
end;
structure Quickcheck : QUICKCHECK =
struct
-open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
+(* preferences *)
+
+val auto = ref false;
+val auto_time_limit = ref 2500;
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (setmp auto true (fn () =>
+ Preferences.bool_pref auto
+ "auto-quickcheck"
+ "Whether to enable quickcheck automatically.") ());
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (Preferences.nat_pref auto_time_limit
+ "auto-quickcheck-time-limit"
+ "Time limit for automatic quickcheck (in milliseconds).");
+
(* quickcheck configuration -- default parameters, test generators *)
@@ -140,7 +158,7 @@
(* automatic testing *)
-fun test_goal_auto int state =
+val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
let
val ctxt = Proof.context_of state;
val assms = map term_of (Assumption.all_assms_of ctxt);
@@ -161,12 +179,10 @@
if int andalso !auto andalso not (!Toplevel.quiet)
then test ()
else state
- end;
-
-val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);
+ end));
-(* Isar interfaces *)
+(* Isar commands *)
fun read_nat s = case (Library.read_int o Symbol.explode) s
of (k, []) => if k >= 0 then k