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