--- a/src/HOL/IsaMakefile Fri Apr 24 17:45:16 2009 +0200
+++ b/src/HOL/IsaMakefile Fri Apr 24 17:45:17 2009 +0200
@@ -102,6 +102,7 @@
$(SRC)/Tools/intuitionistic.ML \
$(SRC)/Tools/induct_tacs.ML \
$(SRC)/Tools/nbe.ML \
+ $(SRC)/Tools/quickcheck.ML \
$(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/random_word.ML \
$(SRC)/Tools/value.ML \
--- a/src/Pure/IsaMakefile Fri Apr 24 17:45:16 2009 +0200
+++ b/src/Pure/IsaMakefile Fri Apr 24 17:45:17 2009 +0200
@@ -40,8 +40,8 @@
Pure: $(OUT)/Pure
-$(OUT)/Pure: $(BOOTSTRAP_FILES) ../Tools/auto_solve.ML \
- ../Tools/quickcheck.ML Concurrent/ROOT.ML Concurrent/future.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 \
@@ -87,7 +87,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/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \
+ Tools/auto_solve.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 Fri Apr 24 17:45:16 2009 +0200
+++ b/src/Pure/ProofGeneral/ROOT.ML Fri Apr 24 17:45:17 2009 +0200
@@ -17,7 +17,7 @@
(use
|> setmp Proofterm.proofs 1
|> setmp quick_and_dirty true
- |> setmp auto_quickcheck true
+ |> setmp Quickcheck.auto true
|> setmp auto_solve true) "preferences.ML";
use "pgip_parser.ML";
--- a/src/Pure/Tools/ROOT.ML Fri Apr 24 17:45:16 2009 +0200
+++ b/src/Pure/Tools/ROOT.ML Fri Apr 24 17:45:17 2009 +0200
@@ -11,6 +11,13 @@
use "find_theorems.ML";
use "find_consts.ML";
-(*quickcheck/autosolve needed here because of pg preferences*)
-use "../../Tools/quickcheck.ML";
-use "../../Tools/auto_solve.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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/auto_solve.ML Fri Apr 24 17:45:17 2009 +0200
@@ -0,0 +1,87 @@
+(* 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;
+
--- a/src/Tools/Code_Generator.thy Fri Apr 24 17:45:16 2009 +0200
+++ b/src/Tools/Code_Generator.thy Fri Apr 24 17:45:17 2009 +0200
@@ -8,6 +8,7 @@
imports Pure
uses
"~~/src/Tools/value.ML"
+ "~~/src/Tools/quickcheck.ML"
"~~/src/Tools/code/code_name.ML"
"~~/src/Tools/code/code_wellsorted.ML"
"~~/src/Tools/code/code_thingol.ML"
--- a/src/Tools/auto_solve.ML Fri Apr 24 17:45:16 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;
-
--- a/src/Tools/quickcheck.ML Fri Apr 24 17:45:16 2009 +0200
+++ b/src/Tools/quickcheck.ML Fri Apr 24 17:45:17 2009 +0200
@@ -15,19 +15,21 @@
structure Quickcheck : QUICKCHECK =
struct
+open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
+
(* quickcheck configuration -- default parameters, test generators *)
datatype test_params = Test_Params of
{ size: int, iterations: int, default_type: typ option };
-fun dest_test_params (Test_Params { size, iterations, default_type}) =
+fun dest_test_params (Test_Params { size, iterations, default_type }) =
((size, iterations), default_type);
fun mk_test_params ((size, iterations), default_type) =
Test_Params { size = size, iterations = iterations, default_type = default_type };
fun map_test_params f (Test_Params { size, iterations, default_type}) =
mk_test_params (f ((size, iterations), default_type));
-fun merge_test_params (Test_Params {size = size1, iterations = iterations1, default_type = default_type1},
- Test_Params {size = size2, iterations = iterations2, default_type = default_type2}) =
+fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 },
+ Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) =
mk_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
case default_type1 of NONE => default_type2 | _ => default_type1);
@@ -138,9 +140,6 @@
(* automatic testing *)
-val auto = ref false;
-val auto_time_limit = ref 5000;
-
fun test_goal_auto int state =
let
val ctxt = Proof.context_of state;