observe distinction between Pure/Tools and Tools more closely
authorhaftmann
Fri Apr 24 17:45:17 2009 +0200 (2009-04-24)
changeset 30973304ab57afa6e
parent 30972 5b65835ccc92
child 30974 415f2fe37f62
observe distinction between Pure/Tools and Tools more closely
src/HOL/IsaMakefile
src/Pure/IsaMakefile
src/Pure/ProofGeneral/ROOT.ML
src/Pure/Tools/ROOT.ML
src/Pure/Tools/auto_solve.ML
src/Tools/Code_Generator.thy
src/Tools/auto_solve.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 24 17:45:16 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 24 17:45:17 2009 +0200
     1.3 @@ -102,6 +102,7 @@
     1.4    $(SRC)/Tools/intuitionistic.ML \
     1.5    $(SRC)/Tools/induct_tacs.ML \
     1.6    $(SRC)/Tools/nbe.ML \
     1.7 +  $(SRC)/Tools/quickcheck.ML \
     1.8    $(SRC)/Tools/project_rule.ML \
     1.9    $(SRC)/Tools/random_word.ML \
    1.10    $(SRC)/Tools/value.ML \
     2.1 --- a/src/Pure/IsaMakefile	Fri Apr 24 17:45:16 2009 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Fri Apr 24 17:45:17 2009 +0200
     2.3 @@ -40,8 +40,8 @@
     2.4  
     2.5  Pure: $(OUT)/Pure
     2.6  
     2.7 -$(OUT)/Pure: $(BOOTSTRAP_FILES) ../Tools/auto_solve.ML			\
     2.8 -  ../Tools/quickcheck.ML Concurrent/ROOT.ML Concurrent/future.ML	\
     2.9 +$(OUT)/Pure: $(BOOTSTRAP_FILES) \
    2.10 +  Concurrent/ROOT.ML Concurrent/future.ML	\
    2.11    Concurrent/mailbox.ML Concurrent/par_list.ML				\
    2.12    Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
    2.13    Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML	\
    2.14 @@ -87,7 +87,7 @@
    2.15    Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML		\
    2.16    Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML	\
    2.17    Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML			\
    2.18 -  Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML	\
    2.19 +  Tools/auto_solve.ML Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML	\
    2.20    Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
    2.21    conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
    2.22    defs.ML display.ML drule.ML envir.ML facts.ML goal.ML			\
     3.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Fri Apr 24 17:45:16 2009 +0200
     3.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Fri Apr 24 17:45:17 2009 +0200
     3.3 @@ -17,7 +17,7 @@
     3.4  (use
     3.5    |> setmp Proofterm.proofs 1
     3.6    |> setmp quick_and_dirty true
     3.7 -  |> setmp auto_quickcheck true
     3.8 +  |> setmp Quickcheck.auto true
     3.9    |> setmp auto_solve true) "preferences.ML";
    3.10  
    3.11  use "pgip_parser.ML";
     4.1 --- a/src/Pure/Tools/ROOT.ML	Fri Apr 24 17:45:16 2009 +0200
     4.2 +++ b/src/Pure/Tools/ROOT.ML	Fri Apr 24 17:45:17 2009 +0200
     4.3 @@ -11,6 +11,13 @@
     4.4  use "find_theorems.ML";
     4.5  use "find_consts.ML";
     4.6  
     4.7 -(*quickcheck/autosolve needed here because of pg preferences*)
     4.8 -use "../../Tools/quickcheck.ML";
     4.9 -use "../../Tools/auto_solve.ML";
    4.10 +use "auto_solve.ML";
    4.11 +
    4.12 +(*quickcheck stub needed here because of pg preferences*)
    4.13 +structure Quickcheck =
    4.14 +struct
    4.15 +
    4.16 +val auto = ref false;
    4.17 +val auto_time_limit = ref 5000;
    4.18 +
    4.19 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/Tools/auto_solve.ML	Fri Apr 24 17:45:17 2009 +0200
     5.3 @@ -0,0 +1,87 @@
     5.4 +(*  Title:      Tools/auto_solve.ML
     5.5 +    Author:     Timothy Bourke and Gerwin Klein, NICTA
     5.6 +
     5.7 +Check whether a newly stated theorem can be solved directly by an
     5.8 +existing theorem.  Duplicate lemmas can be detected in this way.
     5.9 +
    5.10 +The implementation is based in part on Berghofer and Haftmann's
    5.11 +quickcheck.ML.  It relies critically on the FindTheorems solves
    5.12 +feature.
    5.13 +*)
    5.14 +
    5.15 +signature AUTO_SOLVE =
    5.16 +sig
    5.17 +  val auto : bool ref
    5.18 +  val auto_time_limit : int ref
    5.19 +  val limit : int ref
    5.20 +
    5.21 +  val seek_solution : bool -> Proof.state -> Proof.state
    5.22 +end;
    5.23 +
    5.24 +structure AutoSolve : AUTO_SOLVE =
    5.25 +struct
    5.26 +
    5.27 +val auto = ref false;
    5.28 +val auto_time_limit = ref 2500;
    5.29 +val limit = ref 5;
    5.30 +
    5.31 +fun seek_solution int state =
    5.32 +  let
    5.33 +    val ctxt = Proof.context_of state;
    5.34 +
    5.35 +    val crits = [(true, FindTheorems.Solves)];
    5.36 +    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
    5.37 +
    5.38 +    fun prt_result (goal, results) =
    5.39 +      let
    5.40 +        val msg =
    5.41 +          (case goal of
    5.42 +            NONE => "The current goal"
    5.43 +          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
    5.44 +      in
    5.45 +        Pretty.big_list
    5.46 +          (msg ^ " could be solved directly with:")
    5.47 +          (map (FindTheorems.pretty_thm ctxt) results)
    5.48 +      end;
    5.49 +
    5.50 +    fun seek_against_goal () =
    5.51 +      (case try Proof.get_goal state of
    5.52 +        NONE => NONE
    5.53 +      | SOME (_, (_, goal)) =>
    5.54 +          let
    5.55 +            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
    5.56 +            val rs =
    5.57 +              if length subgoals = 1
    5.58 +              then [(NONE, find goal)]
    5.59 +              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
    5.60 +            val results = filter_out (null o snd) rs;
    5.61 +          in if null results then NONE else SOME results end);
    5.62 +
    5.63 +    fun go () =
    5.64 +      let
    5.65 +        val res =
    5.66 +          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
    5.67 +            (try seek_against_goal) ();
    5.68 +      in
    5.69 +        (case res of
    5.70 +          SOME (SOME results) =>
    5.71 +            state |> Proof.goal_message
    5.72 +              (fn () => Pretty.chunks
    5.73 +                [Pretty.str "",
    5.74 +                  Pretty.markup Markup.hilite
    5.75 +                    (separate (Pretty.brk 0) (map prt_result results))])
    5.76 +        | _ => state)
    5.77 +      end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
    5.78 +  in
    5.79 +    if int andalso ! auto andalso not (! Toplevel.quiet)
    5.80 +    then go ()
    5.81 +    else state
    5.82 +  end;
    5.83 +
    5.84 +end;
    5.85 +
    5.86 +val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
    5.87 +
    5.88 +val auto_solve = AutoSolve.auto;
    5.89 +val auto_solve_time_limit = AutoSolve.auto_time_limit;
    5.90 +
     6.1 --- a/src/Tools/Code_Generator.thy	Fri Apr 24 17:45:16 2009 +0200
     6.2 +++ b/src/Tools/Code_Generator.thy	Fri Apr 24 17:45:17 2009 +0200
     6.3 @@ -8,6 +8,7 @@
     6.4  imports Pure
     6.5  uses
     6.6    "~~/src/Tools/value.ML"
     6.7 +  "~~/src/Tools/quickcheck.ML"
     6.8    "~~/src/Tools/code/code_name.ML"
     6.9    "~~/src/Tools/code/code_wellsorted.ML" 
    6.10    "~~/src/Tools/code/code_thingol.ML"
     7.1 --- a/src/Tools/auto_solve.ML	Fri Apr 24 17:45:16 2009 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,87 +0,0 @@
     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 -
    7.21 -  val seek_solution : bool -> Proof.state -> Proof.state
    7.22 -end;
    7.23 -
    7.24 -structure AutoSolve : AUTO_SOLVE =
    7.25 -struct
    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 -fun seek_solution int state =
    7.32 -  let
    7.33 -    val ctxt = Proof.context_of state;
    7.34 -
    7.35 -    val crits = [(true, FindTheorems.Solves)];
    7.36 -    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
    7.37 -
    7.38 -    fun prt_result (goal, results) =
    7.39 -      let
    7.40 -        val msg =
    7.41 -          (case goal of
    7.42 -            NONE => "The current goal"
    7.43 -          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
    7.44 -      in
    7.45 -        Pretty.big_list
    7.46 -          (msg ^ " could be solved directly with:")
    7.47 -          (map (FindTheorems.pretty_thm ctxt) results)
    7.48 -      end;
    7.49 -
    7.50 -    fun seek_against_goal () =
    7.51 -      (case try Proof.get_goal state of
    7.52 -        NONE => NONE
    7.53 -      | SOME (_, (_, goal)) =>
    7.54 -          let
    7.55 -            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
    7.56 -            val rs =
    7.57 -              if length subgoals = 1
    7.58 -              then [(NONE, find goal)]
    7.59 -              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
    7.60 -            val results = filter_out (null o snd) rs;
    7.61 -          in if null results then NONE else SOME results end);
    7.62 -
    7.63 -    fun go () =
    7.64 -      let
    7.65 -        val res =
    7.66 -          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
    7.67 -            (try seek_against_goal) ();
    7.68 -      in
    7.69 -        (case res of
    7.70 -          SOME (SOME results) =>
    7.71 -            state |> Proof.goal_message
    7.72 -              (fn () => Pretty.chunks
    7.73 -                [Pretty.str "",
    7.74 -                  Pretty.markup Markup.hilite
    7.75 -                    (separate (Pretty.brk 0) (map prt_result results))])
    7.76 -        | _ => state)
    7.77 -      end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
    7.78 -  in
    7.79 -    if int andalso ! auto andalso not (! Toplevel.quiet)
    7.80 -    then go ()
    7.81 -    else state
    7.82 -  end;
    7.83 -
    7.84 -end;
    7.85 -
    7.86 -val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
    7.87 -
    7.88 -val auto_solve = AutoSolve.auto;
    7.89 -val auto_solve_time_limit = AutoSolve.auto_time_limit;
    7.90 -
     8.1 --- a/src/Tools/quickcheck.ML	Fri Apr 24 17:45:16 2009 +0200
     8.2 +++ b/src/Tools/quickcheck.ML	Fri Apr 24 17:45:17 2009 +0200
     8.3 @@ -15,19 +15,21 @@
     8.4  structure Quickcheck : QUICKCHECK =
     8.5  struct
     8.6  
     8.7 +open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
     8.8 +
     8.9  (* quickcheck configuration -- default parameters, test generators *)
    8.10  
    8.11  datatype test_params = Test_Params of
    8.12    { size: int, iterations: int, default_type: typ option };
    8.13  
    8.14 -fun dest_test_params (Test_Params { size, iterations, default_type}) =
    8.15 +fun dest_test_params (Test_Params { size, iterations, default_type }) =
    8.16    ((size, iterations), default_type);
    8.17  fun mk_test_params ((size, iterations), default_type) =
    8.18    Test_Params { size = size, iterations = iterations, default_type = default_type };
    8.19  fun map_test_params f (Test_Params { size, iterations, default_type}) =
    8.20    mk_test_params (f ((size, iterations), default_type));
    8.21 -fun merge_test_params (Test_Params {size = size1, iterations = iterations1, default_type = default_type1},
    8.22 -  Test_Params {size = size2, iterations = iterations2, default_type = default_type2}) =
    8.23 +fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 },
    8.24 +  Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) =
    8.25    mk_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    8.26      case default_type1 of NONE => default_type2 | _ => default_type1);
    8.27  
    8.28 @@ -138,9 +140,6 @@
    8.29  
    8.30  (* automatic testing *)
    8.31  
    8.32 -val auto = ref false;
    8.33 -val auto_time_limit = ref 5000;
    8.34 -
    8.35  fun test_goal_auto int state =
    8.36    let
    8.37      val ctxt = Proof.context_of state;