1(*  Title:      Tools/try.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3
4Manager for tools that should be tried on conjectures.
5*)
6
7signature TRY =
8sig
9  type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
10
11  val tryN: string
12
13  val serial_commas: string -> string list -> string list
14  val subgoal_count: Proof.state -> int
15  val get_tools: theory -> tool list
16  val try_tools: Proof.state -> (string * string) option
17  val tool_setup: tool -> unit
18end;
19
20structure Try : TRY =
21struct
22
23type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list)));
24
25val tryN = "try";
26
27
28(* helpers *)
29
30fun serial_commas _ [] = ["??"]
31  | serial_commas _ [s] = [s]
32  | serial_commas conj [s1, s2] = [s1, conj, s2]
33  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
34  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss;
35
36val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal;
37
38
39(* configuration *)
40
41fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
42  prod_ord int_ord string_ord ((weight1, name1), (weight2, name2));
43
44structure Data = Theory_Data
45(
46  type T = tool list;
47  val empty = [];
48  val extend = I;
49  fun merge data : T = Ord_List.merge tool_ord data;
50);
51
52val get_tools = Data.get;
53
54val register_tool = Data.map o Ord_List.insert tool_ord;
55
56
57(* try command *)
58
59fun try_tools state =
60  if subgoal_count state = 0 then
61    (writeln "No subgoal!"; NONE)
62  else
63    get_tools (Proof.theory_of state)
64    |> tap (fn tools =>
65               "Trying " ^ space_implode " "
66                    (serial_commas "and" (map (quote o fst) tools)) ^ "..."
67               |> writeln)
68    |> Par_List.get_some
69           (fn (name, (_, _, tool)) =>
70               case try (tool false) state of
71                 SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
72               | _ => NONE)
73    |> tap (fn NONE => writeln "Tried in vain" | _ => ());
74
75val _ =
76  Outer_Syntax.command \<^command_keyword>\<open>try\<close>
77    "try a combination of automatic proving and disproving tools"
78    (Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of)));
79
80
81(* automatic try (TTY) *)
82
83fun auto_try state =
84  get_tools (Proof.theory_of state)
85  |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
86  |> Par_List.get_some (fn tool =>
87    (case try (tool true) state of
88      SOME (true, (_, outcome)) => SOME outcome
89    | _ => NONE))
90  |> the_default [];
91
92
93(* asynchronous print function (PIDE) *)
94
95fun print_function ((name, (weight, auto, tool)): tool) =
96  Command.print_function ("auto_" ^ name)
97    (fn {keywords, command_name, ...} =>
98      if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then
99        SOME
100         {delay = SOME (seconds (Options.default_real \<^system_option>\<open>auto_time_start\<close>)),
101          pri = ~ weight,
102          persistent = true,
103          strict = true,
104          print_fn = fn _ => fn st =>
105            let
106              val state = Toplevel.proof_of st
107                |> Proof.map_context (Context_Position.set_visible false)
108              val auto_time_limit = Options.default_real \<^system_option>\<open>auto_time_limit\<close>
109            in
110              if auto_time_limit > 0.0 then
111                (case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of
112                  (true, (_, outcome)) => List.app Output.information outcome
113                | _ => ())
114              else ()
115            end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()}
116      else NONE);
117
118
119(* hybrid tool setup *)
120
121fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool);
122
123end;
124