hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
authorwenzelm
Sat Jul 13 00:50:49 2013 +0200 (2013-07-13)
changeset 52641c56b6fa636e8
parent 52640 38679321b251
child 52642 84eb792224a8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
src/HOL/HOL.thy
src/HOL/Metis.thy
src/HOL/Nitpick.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/proof.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/src/HOL/HOL.thy	Sat Jul 13 00:24:05 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Jul 13 00:50:49 2013 +0200
     1.3 @@ -37,8 +37,6 @@
     1.4  
     1.5  setup {*
     1.6    Intuitionistic.method_setup @{binding iprover}
     1.7 -  #> Quickcheck.setup
     1.8 -  #> Solve_Direct.setup
     1.9    #> Subtyping.setup
    1.10    #> Case_Product.setup
    1.11  *}
     2.1 --- a/src/HOL/Metis.thy	Sat Jul 13 00:24:05 2013 +0200
     2.2 +++ b/src/HOL/Metis.thy	Sat Jul 13 00:50:49 2013 +0200
     2.3 @@ -56,6 +56,5 @@
     2.4  subsection {* Try0 *}
     2.5  
     2.6  ML_file "Tools/try0.ML"
     2.7 -setup {* Try0.setup *}
     2.8  
     2.9  end
     3.1 --- a/src/HOL/Nitpick.thy	Sat Jul 13 00:24:05 2013 +0200
     3.2 +++ b/src/HOL/Nitpick.thy	Sat Jul 13 00:50:49 2013 +0200
     3.3 @@ -214,7 +214,6 @@
     3.4  ML_file "Tools/Nitpick/nitpick_tests.ML"
     3.5  
     3.6  setup {*
     3.7 -  Nitpick_Isar.setup #>
     3.8    Nitpick_HOL.register_ersatz_global
     3.9      [(@{const_name card}, @{const_name card'}),
    3.10       (@{const_name setsum}, @{const_name setsum'}),
     4.1 --- a/src/HOL/Sledgehammer.thy	Sat Jul 13 00:24:05 2013 +0200
     4.2 +++ b/src/HOL/Sledgehammer.thy	Sat Jul 13 00:50:49 2013 +0200
     4.3 @@ -11,7 +11,6 @@
     4.4  keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
     4.5  begin
     4.6  
     4.7 -
     4.8  ML_file "Tools/Sledgehammer/async_manager.ML"
     4.9  ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
    4.10  ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
    4.11 @@ -31,6 +30,4 @@
    4.12  ML_file "Tools/Sledgehammer/sledgehammer_run.ML"
    4.13  ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
    4.14  
    4.15 -setup {* Sledgehammer_Isar.setup *}
    4.16 -
    4.17  end
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Jul 13 00:24:05 2013 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Jul 13 00:50:49 2013 +0200
     5.3 @@ -13,7 +13,6 @@
     5.4    val nitpickN : string
     5.5    val nitpick_paramsN : string
     5.6    val default_params : theory -> (string * string) list -> params
     5.7 -  val setup : theory -> theory
     5.8  end;
     5.9  
    5.10  structure Nitpick_Isar : NITPICK_ISAR =
    5.11 @@ -399,6 +398,6 @@
    5.12  
    5.13  fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
    5.14  
    5.15 -val setup = Try.register_tool (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
    5.16 +val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
    5.17  
    5.18  end;
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 13 00:24:05 2013 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 13 00:50:49 2013 +0200
     6.3 @@ -11,7 +11,6 @@
     6.4    val provers : string Unsynchronized.ref
     6.5    val timeout : int Unsynchronized.ref
     6.6    val default_params : Proof.context -> (string * string) list -> params
     6.7 -  val setup : theory -> theory
     6.8  end;
     6.9  
    6.10  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    6.11 @@ -486,6 +485,6 @@
    6.12                       (minimize_command [] i) state
    6.13    end
    6.14  
    6.15 -val setup = Try.register_tool (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
    6.16 +val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
    6.17  
    6.18  end;
     7.1 --- a/src/HOL/Tools/try0.ML	Sat Jul 13 00:24:05 2013 +0200
     7.2 +++ b/src/HOL/Tools/try0.ML	Sat Jul 13 00:50:49 2013 +0200
     7.3 @@ -11,7 +11,6 @@
     7.4    val try0 :
     7.5      Time.time option -> string list * string list * string list * string list
     7.6      -> Proof.state -> bool
     7.7 -  val setup : theory -> theory
     7.8  end;
     7.9  
    7.10  structure Try0 : TRY0 =
    7.11 @@ -193,6 +192,6 @@
    7.12  fun try_try0 auto =
    7.13    do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
    7.14  
    7.15 -val setup = Try.register_tool (try0N, (30, @{option auto_try0}, try_try0))
    7.16 +val _ = Try.tool_setup (try0N, (30, @{option auto_try0}, try_try0))
    7.17  
    7.18  end;
     8.1 --- a/src/Pure/Isar/proof.ML	Sat Jul 13 00:24:05 2013 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Sat Jul 13 00:50:49 2013 +0200
     8.3 @@ -32,6 +32,7 @@
     8.4    val assert_no_chain: state -> state
     8.5    val enter_forward: state -> state
     8.6    val goal_message: (unit -> Pretty.T) -> state -> state
     8.7 +  val pretty_goal_messages: state -> Pretty.T list
     8.8    val pretty_state: int -> state -> Pretty.T list
     8.9    val refine: Method.text -> state -> state Seq.seq
    8.10    val refine_end: Method.text -> state -> state Seq.seq
    8.11 @@ -336,6 +337,11 @@
    8.12  
    8.13  (** pretty_state **)
    8.14  
    8.15 +fun pretty_goal_messages state =
    8.16 +  (case try find_goal state of
    8.17 +    SOME (_, (_, {messages, ...})) => map (fn msg => msg ()) (rev messages)
    8.18 +  | NONE => []);
    8.19 +
    8.20  fun pretty_facts _ _ NONE = []
    8.21    | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""];
    8.22  
     9.1 --- a/src/Tools/quickcheck.ML	Sat Jul 13 00:24:05 2013 +0200
     9.2 +++ b/src/Tools/quickcheck.ML	Sat Jul 13 00:50:49 2013 +0200
     9.3 @@ -10,7 +10,6 @@
     9.4    val genuineN: string
     9.5    val noneN: string
     9.6    val unknownN: string
     9.7 -  val setup: theory -> theory
     9.8    (*configuration*)
     9.9    val batch_tester : string Config.T
    9.10    val size : int Config.T
    9.11 @@ -564,7 +563,7 @@
    9.12    end
    9.13    |> `(fn (outcome_code, _) => outcome_code = genuineN);
    9.14  
    9.15 -val setup = Try.register_tool (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
    9.16 +val _ = Try.tool_setup (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
    9.17  
    9.18  end;
    9.19  
    10.1 --- a/src/Tools/solve_direct.ML	Sat Jul 13 00:24:05 2013 +0200
    10.2 +++ b/src/Tools/solve_direct.ML	Sat Jul 13 00:50:49 2013 +0200
    10.3 @@ -16,7 +16,6 @@
    10.4    val unknownN: string
    10.5    val max_solutions: int Unsynchronized.ref
    10.6    val solve_direct: Proof.state -> bool * (string * Proof.state)
    10.7 -  val setup: theory -> theory
    10.8  end;
    10.9  
   10.10  structure Solve_Direct: SOLVE_DIRECT =
   10.11 @@ -115,6 +114,6 @@
   10.12  
   10.13  fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
   10.14  
   10.15 -val setup = Try.register_tool (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
   10.16 +val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
   10.17  
   10.18  end;
    11.1 --- a/src/Tools/try.ML	Sat Jul 13 00:24:05 2013 +0200
    11.2 +++ b/src/Tools/try.ML	Sat Jul 13 00:50:49 2013 +0200
    11.3 @@ -13,9 +13,9 @@
    11.4  
    11.5    val serial_commas : string -> string list -> string list
    11.6    val subgoal_count : Proof.state -> int
    11.7 -  val register_tool : tool -> theory -> theory
    11.8    val get_tools : theory -> tool list
    11.9    val try_tools : Proof.state -> (string * string) option
   11.10 +  val tool_setup : tool -> unit
   11.11  end;
   11.12  
   11.13  structure Try : TRY =
   11.14 @@ -65,6 +65,7 @@
   11.15  
   11.16  val register_tool = Data.map o Ord_List.insert tool_ord
   11.17  
   11.18 +
   11.19  (* try command *)
   11.20  
   11.21  fun try_tools state =
   11.22 @@ -89,7 +90,7 @@
   11.23      (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
   11.24  
   11.25  
   11.26 -(* automatic try *)
   11.27 +(* automatic try (TTY) *)
   11.28  
   11.29  fun auto_try state =
   11.30    get_tools (Proof.theory_of state)
   11.31 @@ -111,4 +112,35 @@
   11.32        state
   11.33    end))
   11.34  
   11.35 +
   11.36 +(* asynchronous print function (PIDE) *)
   11.37 +
   11.38 +fun print_function ((name, (weight, auto, tool)): tool) =
   11.39 +  Command.print_function {name = name, pri = ~ weight, persistent = true}
   11.40 +    (fn {command_name} =>
   11.41 +      if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
   11.42 +        SOME (fn _ => fn st =>
   11.43 +          let
   11.44 +            val auto_time_limit = Options.default_real @{option auto_time_limit}
   11.45 +          in
   11.46 +            if auto_time_limit > 0.0 then
   11.47 +              (case try Toplevel.proof_of st of
   11.48 +                SOME state =>
   11.49 +                  (case
   11.50 +                    (try o TimeLimit.timeLimit (seconds auto_time_limit))
   11.51 +                      (fn () => tool true state) () of
   11.52 +                    SOME (true, (_, state')) =>
   11.53 +                      Pretty.writeln (Pretty.chunks (Proof.pretty_goal_messages state'))
   11.54 +                  | _ => ())
   11.55 +              | NONE => ())
   11.56 +            else ()
   11.57 +          end)
   11.58 +      else NONE);
   11.59 +
   11.60 +
   11.61 +(* hybrid tool setup *)
   11.62 +
   11.63 +fun tool_setup tool =
   11.64 +  (Context.>> (Context.map_theory (register_tool tool)); print_function tool);
   11.65 +
   11.66  end;