misc cleanup of auto_solve and quickcheck:
authorwenzelm
Sat Apr 25 21:28:04 2009 +0200 (2009-04-25)
changeset 30980fe0855471964
parent 30979 10eb446df3c7
child 30981 6b9b93816b30
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;
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/Pure/IsaMakefile
src/Pure/ProofGeneral/ROOT.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/Tools/auto_solve.ML
src/Tools/auto_solve.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/HOL.thy	Sat Apr 25 20:31:27 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Apr 25 21:28:04 2009 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  imports Pure "~~/src/Tools/Code_Generator"
     1.5  uses
     1.6    ("Tools/hologic.ML")
     1.7 +  "~~/src/Tools/auto_solve.ML"
     1.8    "~~/src/Tools/IsaPlanner/zipper.ML"
     1.9    "~~/src/Tools/IsaPlanner/isand.ML"
    1.10    "~~/src/Tools/IsaPlanner/rw_tools.ML"
    1.11 @@ -1921,7 +1922,7 @@
    1.12  quickcheck_params [size = 5, iterations = 50]
    1.13  
    1.14  
    1.15 -subsection {* Nitpick hooks *}
    1.16 +subsection {* Nitpick setup *}
    1.17  
    1.18  text {* This will be relocated once Nitpick is moved to HOL. *}
    1.19  
    1.20 @@ -1947,10 +1948,14 @@
    1.21    val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
    1.22  )
    1.23  *}
    1.24 -setup {* Nitpick_Const_Def_Thms.setup
    1.25 -         #> Nitpick_Const_Simp_Thms.setup
    1.26 -         #> Nitpick_Const_Psimp_Thms.setup
    1.27 -         #> Nitpick_Ind_Intro_Thms.setup *}
    1.28 +
    1.29 +setup {*
    1.30 +  Nitpick_Const_Def_Thms.setup
    1.31 +  #> Nitpick_Const_Simp_Thms.setup
    1.32 +  #> Nitpick_Const_Psimp_Thms.setup
    1.33 +  #> Nitpick_Ind_Intro_Thms.setup
    1.34 +*}
    1.35 +
    1.36  
    1.37  subsection {* Legacy tactics and ML bindings *}
    1.38  
     2.1 --- a/src/HOL/IsaMakefile	Sat Apr 25 20:31:27 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Sat Apr 25 21:28:04 2009 +0200
     2.3 @@ -89,6 +89,7 @@
     2.4    $(SRC)/Tools/IsaPlanner/rw_tools.ML \
     2.5    $(SRC)/Tools/IsaPlanner/zipper.ML \
     2.6    $(SRC)/Tools/atomize_elim.ML \
     2.7 +  $(SRC)/Tools/auto_solve.ML \
     2.8    $(SRC)/Tools/code/code_haskell.ML \
     2.9    $(SRC)/Tools/code/code_ml.ML \
    2.10    $(SRC)/Tools/code/code_name.ML \
     3.1 --- a/src/Pure/IsaMakefile	Sat Apr 25 20:31:27 2009 +0200
     3.2 +++ b/src/Pure/IsaMakefile	Sat Apr 25 21:28:04 2009 +0200
     3.3 @@ -40,9 +40,8 @@
     3.4  
     3.5  Pure: $(OUT)/Pure
     3.6  
     3.7 -$(OUT)/Pure: $(BOOTSTRAP_FILES) \
     3.8 -  Concurrent/ROOT.ML Concurrent/future.ML	\
     3.9 -  Concurrent/mailbox.ML Concurrent/par_list.ML				\
    3.10 +$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/ROOT.ML			\
    3.11 +  Concurrent/future.ML Concurrent/mailbox.ML Concurrent/par_list.ML	\
    3.12    Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
    3.13    Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML	\
    3.14    General/alist.ML General/antiquote.ML General/balanced_tree.ML	\
    3.15 @@ -87,7 +86,7 @@
    3.16    Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML		\
    3.17    Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML	\
    3.18    Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML			\
    3.19 -  Tools/auto_solve.ML Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML	\
    3.20 +  Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML	\
    3.21    Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
    3.22    conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
    3.23    defs.ML display.ML drule.ML envir.ML facts.ML goal.ML			\
     4.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Sat Apr 25 20:31:27 2009 +0200
     4.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Sat Apr 25 21:28:04 2009 +0200
     4.3 @@ -14,11 +14,7 @@
     4.4  
     4.5  use "pgip_isabelle.ML";
     4.6  
     4.7 -(use
     4.8 -  |> setmp Proofterm.proofs 1
     4.9 -  |> setmp quick_and_dirty true
    4.10 -  |> setmp Quickcheck.auto true
    4.11 -  |> setmp auto_solve true) "preferences.ML";
    4.12 +use "preferences.ML";
    4.13  
    4.14  use "pgip_parser.ML";
    4.15  
     5.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 20:31:27 2009 +0200
     5.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 21:28:04 2009 +0200
     5.3 @@ -6,6 +6,10 @@
     5.4  
     5.5  signature PREFERENCES =
     5.6  sig
     5.7 +  val category_display: string
     5.8 +  val category_advanced_display: string
     5.9 +  val category_tracing: string
    5.10 +  val category_proof: string
    5.11    type preference =
    5.12     {name: string,
    5.13      descr: string,
    5.14 @@ -29,6 +33,14 @@
    5.15  structure Preferences: PREFERENCES =
    5.16  struct
    5.17  
    5.18 +(* categories *)
    5.19 +
    5.20 +val category_display = "Display";
    5.21 +val category_advanced_display = "Advanced Display";
    5.22 +val category_tracing = "Tracing";
    5.23 +val category_proof = "Proof"
    5.24 +
    5.25 +
    5.26  (* preferences and preference tables *)
    5.27  
    5.28  type preference =
    5.29 @@ -66,11 +78,11 @@
    5.30  
    5.31  (* preferences of Pure *)
    5.32  
    5.33 -val proof_pref =
    5.34 +val proof_pref = setmp Proofterm.proofs 1 (fn () =>
    5.35    let
    5.36      fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
    5.37      fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
    5.38 -  in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end;
    5.39 +  in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
    5.40  
    5.41  val thm_depsN = "thm_deps";
    5.42  val thm_deps_pref =
    5.43 @@ -145,24 +157,13 @@
    5.44    bool_pref Toplevel.debug
    5.45      "debugging"
    5.46      "Whether to enable debugging.",
    5.47 -  bool_pref Quickcheck.auto
    5.48 -    "auto-quickcheck"
    5.49 -    "Whether to enable quickcheck automatically.",
    5.50 -  nat_pref Quickcheck.auto_time_limit
    5.51 -    "auto-quickcheck-time-limit"
    5.52 -    "Time limit for automatic quickcheck (in milliseconds).",
    5.53 -  bool_pref AutoSolve.auto
    5.54 -    "auto-solve"
    5.55 -    "Try to solve newly declared lemmas with existing theorems.",
    5.56 -  nat_pref AutoSolve.auto_time_limit
    5.57 -    "auto-solve-time-limit"
    5.58 -    "Time limit for seeking automatic solutions (in milliseconds).",
    5.59    thm_deps_pref];
    5.60  
    5.61  val proof_preferences =
    5.62 - [bool_pref quick_and_dirty
    5.63 -    "quick-and-dirty"
    5.64 -    "Take a few short cuts",
    5.65 + [setmp quick_and_dirty true (fn () =>
    5.66 +    bool_pref quick_and_dirty
    5.67 +      "quick-and-dirty"
    5.68 +      "Take a few short cuts") (),
    5.69    bool_pref Toplevel.skip_proofs
    5.70      "skip-proofs"
    5.71      "Skip over proofs (interactive-only)",
    5.72 @@ -175,10 +176,10 @@
    5.73      "Check proofs in parallel"];
    5.74  
    5.75  val pure_preferences =
    5.76 - [("Display", display_preferences),
    5.77 -  ("Advanced Display", advanced_display_preferences),
    5.78 -  ("Tracing", tracing_preferences),
    5.79 -  ("Proof", proof_preferences)];
    5.80 + [(category_display, display_preferences),
    5.81 +  (category_advanced_display, advanced_display_preferences),
    5.82 +  (category_tracing, tracing_preferences),
    5.83 +  (category_proof, proof_preferences)];
    5.84  
    5.85  
    5.86  (* table of categories and preferences; names must be unique *)
     6.1 --- a/src/Pure/Tools/auto_solve.ML	Sat Apr 25 20:31:27 2009 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,87 +0,0 @@
     6.4 -(*  Title:      Tools/auto_solve.ML
     6.5 -    Author:     Timothy Bourke and Gerwin Klein, NICTA
     6.6 -
     6.7 -Check whether a newly stated theorem can be solved directly by an
     6.8 -existing theorem.  Duplicate lemmas can be detected in this way.
     6.9 -
    6.10 -The implementation is based in part on Berghofer and Haftmann's
    6.11 -quickcheck.ML.  It relies critically on the FindTheorems solves
    6.12 -feature.
    6.13 -*)
    6.14 -
    6.15 -signature AUTO_SOLVE =
    6.16 -sig
    6.17 -  val auto : bool ref
    6.18 -  val auto_time_limit : int ref
    6.19 -  val limit : int ref
    6.20 -
    6.21 -  val seek_solution : bool -> Proof.state -> Proof.state
    6.22 -end;
    6.23 -
    6.24 -structure AutoSolve : AUTO_SOLVE =
    6.25 -struct
    6.26 -
    6.27 -val auto = ref false;
    6.28 -val auto_time_limit = ref 2500;
    6.29 -val limit = ref 5;
    6.30 -
    6.31 -fun seek_solution int state =
    6.32 -  let
    6.33 -    val ctxt = Proof.context_of state;
    6.34 -
    6.35 -    val crits = [(true, FindTheorems.Solves)];
    6.36 -    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
    6.37 -
    6.38 -    fun prt_result (goal, results) =
    6.39 -      let
    6.40 -        val msg =
    6.41 -          (case goal of
    6.42 -            NONE => "The current goal"
    6.43 -          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
    6.44 -      in
    6.45 -        Pretty.big_list
    6.46 -          (msg ^ " could be solved directly with:")
    6.47 -          (map (FindTheorems.pretty_thm ctxt) results)
    6.48 -      end;
    6.49 -
    6.50 -    fun seek_against_goal () =
    6.51 -      (case try Proof.get_goal state of
    6.52 -        NONE => NONE
    6.53 -      | SOME (_, (_, goal)) =>
    6.54 -          let
    6.55 -            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
    6.56 -            val rs =
    6.57 -              if length subgoals = 1
    6.58 -              then [(NONE, find goal)]
    6.59 -              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
    6.60 -            val results = filter_out (null o snd) rs;
    6.61 -          in if null results then NONE else SOME results end);
    6.62 -
    6.63 -    fun go () =
    6.64 -      let
    6.65 -        val res =
    6.66 -          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
    6.67 -            (try seek_against_goal) ();
    6.68 -      in
    6.69 -        (case res of
    6.70 -          SOME (SOME results) =>
    6.71 -            state |> Proof.goal_message
    6.72 -              (fn () => Pretty.chunks
    6.73 -                [Pretty.str "",
    6.74 -                  Pretty.markup Markup.hilite
    6.75 -                    (separate (Pretty.brk 0) (map prt_result results))])
    6.76 -        | _ => state)
    6.77 -      end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
    6.78 -  in
    6.79 -    if int andalso ! auto andalso not (! Toplevel.quiet)
    6.80 -    then go ()
    6.81 -    else state
    6.82 -  end;
    6.83 -
    6.84 -end;
    6.85 -
    6.86 -val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
    6.87 -
    6.88 -val auto_solve = AutoSolve.auto;
    6.89 -val auto_solve_time_limit = AutoSolve.auto_time_limit;
    6.90 -
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/auto_solve.ML	Sat Apr 25 21:28:04 2009 +0200
     7.3 @@ -0,0 +1,101 @@
     7.4 +(*  Title:      Tools/auto_solve.ML
     7.5 +    Author:     Timothy Bourke and Gerwin Klein, NICTA
     7.6 +
     7.7 +Check whether a newly stated theorem can be solved directly by an
     7.8 +existing theorem.  Duplicate lemmas can be detected in this way.
     7.9 +
    7.10 +The implementation is based in part on Berghofer and Haftmann's
    7.11 +quickcheck.ML.  It relies critically on the FindTheorems solves
    7.12 +feature.
    7.13 +*)
    7.14 +
    7.15 +signature AUTO_SOLVE =
    7.16 +sig
    7.17 +  val auto : bool ref
    7.18 +  val auto_time_limit : int ref
    7.19 +  val limit : int ref
    7.20 +end;
    7.21 +
    7.22 +structure AutoSolve : AUTO_SOLVE =
    7.23 +struct
    7.24 +
    7.25 +(* preferences *)
    7.26 +
    7.27 +val auto = ref false;
    7.28 +val auto_time_limit = ref 2500;
    7.29 +val limit = ref 5;
    7.30 +
    7.31 +val _ =
    7.32 +  ProofGeneralPgip.add_preference Preferences.category_tracing
    7.33 +  (setmp auto true (fn () =>
    7.34 +    Preferences.bool_pref auto
    7.35 +      "auto-solve"
    7.36 +      "Try to solve newly declared lemmas with existing theorems.") ());
    7.37 +
    7.38 +val _ =
    7.39 +  ProofGeneralPgip.add_preference Preferences.category_tracing
    7.40 +    (Preferences.nat_pref auto_time_limit
    7.41 +      "auto-solve-time-limit"
    7.42 +      "Time limit for seeking automatic solutions (in milliseconds).");
    7.43 +
    7.44 +
    7.45 +(* hook *)
    7.46 +
    7.47 +val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
    7.48 +  let
    7.49 +    val ctxt = Proof.context_of state;
    7.50 +
    7.51 +    val crits = [(true, FindTheorems.Solves)];
    7.52 +    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
    7.53 +
    7.54 +    fun prt_result (goal, results) =
    7.55 +      let
    7.56 +        val msg =
    7.57 +          (case goal of
    7.58 +            NONE => "The current goal"
    7.59 +          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
    7.60 +      in
    7.61 +        Pretty.big_list
    7.62 +          (msg ^ " could be solved directly with:")
    7.63 +          (map (FindTheorems.pretty_thm ctxt) results)
    7.64 +      end;
    7.65 +
    7.66 +    fun seek_against_goal () =
    7.67 +      (case try Proof.get_goal state of
    7.68 +        NONE => NONE
    7.69 +      | SOME (_, (_, goal)) =>
    7.70 +          let
    7.71 +            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
    7.72 +            val rs =
    7.73 +              if length subgoals = 1
    7.74 +              then [(NONE, find goal)]
    7.75 +              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
    7.76 +            val results = filter_out (null o snd) rs;
    7.77 +          in if null results then NONE else SOME results end);
    7.78 +
    7.79 +    fun go () =
    7.80 +      let
    7.81 +        val res =
    7.82 +          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
    7.83 +            (try seek_against_goal) ();
    7.84 +      in
    7.85 +        (case res of
    7.86 +          SOME (SOME results) =>
    7.87 +            state |> Proof.goal_message
    7.88 +              (fn () => Pretty.chunks
    7.89 +                [Pretty.str "",
    7.90 +                  Pretty.markup Markup.hilite
    7.91 +                    (separate (Pretty.brk 0) (map prt_result results))])
    7.92 +        | _ => state)
    7.93 +      end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
    7.94 +  in
    7.95 +    if int andalso ! auto andalso not (! Toplevel.quiet)
    7.96 +    then go ()
    7.97 +    else state
    7.98 +  end));
    7.99 +
   7.100 +end;
   7.101 +
   7.102 +val auto_solve = AutoSolve.auto;
   7.103 +val auto_solve_time_limit = AutoSolve.auto_time_limit;
   7.104 +
     8.1 --- a/src/Tools/quickcheck.ML	Sat Apr 25 20:31:27 2009 +0200
     8.2 +++ b/src/Tools/quickcheck.ML	Sat Apr 25 21:28:04 2009 +0200
     8.3 @@ -6,16 +6,34 @@
     8.4  
     8.5  signature QUICKCHECK =
     8.6  sig
     8.7 -  val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option;
     8.8 -  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
     8.9    val auto: bool ref
    8.10    val auto_time_limit: int ref
    8.11 +  val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
    8.12 +    (string * term) list option
    8.13 +  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
    8.14  end;
    8.15  
    8.16  structure Quickcheck : QUICKCHECK =
    8.17  struct
    8.18  
    8.19 -open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
    8.20 +(* preferences *)
    8.21 +
    8.22 +val auto = ref false;
    8.23 +val auto_time_limit = ref 2500;
    8.24 +
    8.25 +val _ =
    8.26 +  ProofGeneralPgip.add_preference Preferences.category_tracing
    8.27 +  (setmp auto true (fn () =>
    8.28 +    Preferences.bool_pref auto
    8.29 +      "auto-quickcheck"
    8.30 +      "Whether to enable quickcheck automatically.") ());
    8.31 +
    8.32 +val _ =
    8.33 +  ProofGeneralPgip.add_preference Preferences.category_tracing
    8.34 +    (Preferences.nat_pref auto_time_limit
    8.35 +      "auto-quickcheck-time-limit"
    8.36 +      "Time limit for automatic quickcheck (in milliseconds).");
    8.37 +
    8.38  
    8.39  (* quickcheck configuration -- default parameters, test generators *)
    8.40  
    8.41 @@ -140,7 +158,7 @@
    8.42  
    8.43  (* automatic testing *)
    8.44  
    8.45 -fun test_goal_auto int state =
    8.46 +val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
    8.47    let
    8.48      val ctxt = Proof.context_of state;
    8.49      val assms = map term_of (Assumption.all_assms_of ctxt);
    8.50 @@ -161,12 +179,10 @@
    8.51      if int andalso !auto andalso not (!Toplevel.quiet)
    8.52      then test ()
    8.53      else state
    8.54 -  end;
    8.55 -
    8.56 -val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);
    8.57 +  end));
    8.58  
    8.59  
    8.60 -(* Isar interfaces *)
    8.61 +(* Isar commands *)
    8.62  
    8.63  fun read_nat s = case (Library.read_int o Symbol.explode) s
    8.64   of (k, []) => if k >= 0 then k