# HG changeset patch # User haftmann # Date 1240587917 -7200 # Node ID 304ab57afa6ecacc354937517a5c18abb729a8d0 # Parent 5b65835ccc920a87797c687d2b3f6f21af193ddf observe distinction between Pure/Tools and Tools more closely diff -r 5b65835ccc92 -r 304ab57afa6e src/HOL/IsaMakefile --- 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 \ diff -r 5b65835ccc92 -r 304ab57afa6e src/Pure/IsaMakefile --- 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 \ diff -r 5b65835ccc92 -r 304ab57afa6e src/Pure/ProofGeneral/ROOT.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"; diff -r 5b65835ccc92 -r 304ab57afa6e src/Pure/Tools/ROOT.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; diff -r 5b65835ccc92 -r 304ab57afa6e src/Pure/Tools/auto_solve.ML --- /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; + diff -r 5b65835ccc92 -r 304ab57afa6e src/Tools/Code_Generator.thy --- 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" diff -r 5b65835ccc92 -r 304ab57afa6e src/Tools/auto_solve.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; - diff -r 5b65835ccc92 -r 304ab57afa6e src/Tools/quickcheck.ML --- 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;