1.1 --- a/src/Tools/Code_Generator.thy	Sat Sep 11 12:31:58 2010 +0200
     1.2 +++ b/src/Tools/Code_Generator.thy	Sat Sep 11 12:32:31 2010 +0200
     1.3 @@ -26,7 +26,8 @@
     1.4  begin
     1.5  
     1.6  setup {*
     1.7 -  Code_Preproc.setup
     1.8 +  Auto_Solve.setup
     1.9 +  #> Code_Preproc.setup
    1.10    #> Code_Simp.setup
    1.11    #> Code_ML.setup
    1.12    #> Code_Haskell.setup

     2.1 --- a/src/Tools/auto_solve.ML	Sat Sep 11 12:31:58 2010 +0200
     2.2 +++ b/src/Tools/auto_solve.ML	Sat Sep 11 12:32:31 2010 +0200
     2.3 @@ -4,16 +4,15 @@
     2.4  Check whether a newly stated theorem can be solved directly by an
     2.5  existing theorem.  Duplicate lemmas can be detected in this way.
     2.6  
     2.7 -The implementation is based in part on Berghofer and Haftmann's
     2.8 -quickcheck.ML.  It relies critically on the Find_Theorems solves
     2.9 +The implementation relies critically on the Find_Theorems solves
    2.10  feature.
    2.11  *)
    2.12  
    2.13  signature AUTO_SOLVE =
    2.14  sig
    2.15    val auto : bool Unsynchronized.ref
    2.16 -  val auto_time_limit : int Unsynchronized.ref
    2.17 -  val limit : int Unsynchronized.ref
    2.18 +  val max_solutions : int Unsynchronized.ref
    2.19 +  val setup : theory -> theory
    2.20  end;
    2.21  
    2.22  structure Auto_Solve : AUTO_SOLVE =
    2.23 @@ -22,31 +21,23 @@
    2.24  (* preferences *)
    2.25  
    2.26  val auto = Unsynchronized.ref false;
    2.27 -val auto_time_limit = Unsynchronized.ref 2500;
    2.28 -val limit = Unsynchronized.ref 5;
    2.29 -
    2.30 -val _ =
    2.31 -  ProofGeneralPgip.add_preference Preferences.category_tracing
    2.32 -    (Preferences.nat_pref auto_time_limit
    2.33 -      "auto-solve-time-limit"
    2.34 -      "Time limit for seeking automatic solutions (in milliseconds).");
    2.35 +val max_solutions = Unsynchronized.ref 5;
    2.36  
    2.37  val _ =
    2.38    ProofGeneralPgip.add_preference Preferences.category_tracing
    2.39    (setmp_noncritical auto true (fn () =>
    2.40      Preferences.bool_pref auto
    2.41 -      "auto-solve"
    2.42 -      "Try to solve newly declared lemmas with existing theorems.") ());
    2.43 +      "auto-solve" "Try to solve conjectures with existing theorems.") ());
    2.44  
    2.45  
    2.46  (* hook *)
    2.47  
    2.48 -val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
    2.49 +fun auto_solve state =
    2.50    let
    2.51      val ctxt = Proof.context_of state;
    2.52  
    2.53      val crits = [(true, Find_Theorems.Solves)];
    2.54 -    fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
    2.55 +    fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
    2.56  
    2.57      fun prt_result (goal, results) =
    2.58        let
    2.59 @@ -74,28 +65,16 @@
    2.60            in if null results then NONE else SOME results end);
    2.61  
    2.62      fun go () =
    2.63 -      let
    2.64 -        val res =
    2.65 -          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
    2.66 -            (try seek_against_goal) ();
    2.67 -      in
    2.68 -        (case res of
    2.69 -          SOME (SOME results) =>
    2.70 -            state |> Proof.goal_message
    2.71 -              (fn () => Pretty.chunks
    2.72 -                [Pretty.str "",
    2.73 -                  Pretty.markup Markup.hilite
    2.74 -                    (separate (Pretty.brk 0) (map prt_result results))])
    2.75 -        | _ => state)
    2.76 -      end handle TimeLimit.TimeOut => (warning "Auto solve: timeout"; state);
    2.77 -  in
    2.78 -    if int andalso ! auto andalso not (! Toplevel.quiet)
    2.79 -    then go ()
    2.80 -    else state
    2.81 -  end));
    2.82 +      (case try seek_against_goal () of
    2.83 +        SOME (SOME results) =>
    2.84 +          (true, state |> Proof.goal_message
    2.85 +                  (fn () => Pretty.chunks
    2.86 +                    [Pretty.str "",
    2.87 +                      Pretty.markup Markup.hilite
    2.88 +                        (separate (Pretty.brk 0) (map prt_result results))]))
    2.89 +      | _ => (false, state));
    2.90 +  in if not (!auto) then (false, state) else go () end;
    2.91 +
    2.92 +val setup = Auto_Tools.register_tool ("solve", auto_solve)
    2.93  
    2.94  end;
    2.95 -
    2.96 -val auto_solve = Auto_Solve.auto;
    2.97 -val auto_solve_time_limit = Auto_Solve.auto_time_limit;
    2.98 -

     3.1 --- a/src/Tools/quickcheck.ML	Sat Sep 11 12:31:58 2010 +0200
     3.2 +++ b/src/Tools/quickcheck.ML	Sat Sep 11 12:32:31 2010 +0200
     3.3 @@ -45,7 +45,7 @@
     3.4    (setmp_noncritical auto true (fn () =>
     3.5      Preferences.bool_pref auto
     3.6        "auto-quickcheck"
     3.7 -      "Whether to run Quickcheck automatically.") ());
     3.8 +      "Run Quickcheck automatically.") ());
     3.9  
    3.10  (* quickcheck report *)
    3.11