# HG changeset patch # User wenzelm # Date 1240687684 -7200 # Node ID fe0855471964745b3b0ca31031ca7087b18acb6d # Parent 10eb446df3c7384d64317b86a31971d18b53825c misc cleanup of auto_solve and quickcheck: tools are in src/Tools and loaded uniformly in HOL; preferences are configured in their proper place -- despite old misleading comments in the source; use predefined preferences categories; setmp preferences in-place; diff -r 10eb446df3c7 -r fe0855471964 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Apr 25 20:31:27 2009 +0200 +++ b/src/HOL/HOL.thy Sat Apr 25 21:28:04 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 *} diff -r 10eb446df3c7 -r fe0855471964 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Apr 25 20:31:27 2009 +0200 +++ b/src/HOL/IsaMakefile Sat Apr 25 21:28:04 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 \ diff -r 10eb446df3c7 -r fe0855471964 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Apr 25 20:31:27 2009 +0200 +++ b/src/Pure/IsaMakefile Sat Apr 25 21:28:04 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 \ diff -r 10eb446df3c7 -r fe0855471964 src/Pure/ProofGeneral/ROOT.ML --- a/src/Pure/ProofGeneral/ROOT.ML Sat Apr 25 20:31:27 2009 +0200 +++ b/src/Pure/ProofGeneral/ROOT.ML Sat Apr 25 21:28:04 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"; diff -r 10eb446df3c7 -r fe0855471964 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Sat Apr 25 20:31:27 2009 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Sat Apr 25 21:28:04 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 *) diff -r 10eb446df3c7 -r fe0855471964 src/Pure/Tools/auto_solve.ML --- a/src/Pure/Tools/auto_solve.ML Sat Apr 25 20:31:27 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 10eb446df3c7 -r fe0855471964 src/Tools/auto_solve.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/auto_solve.ML Sat Apr 25 21:28:04 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; + diff -r 10eb446df3c7 -r fe0855471964 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Sat Apr 25 20:31:27 2009 +0200 +++ b/src/Tools/quickcheck.ML Sat Apr 25 21:28:04 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