34 (Conjunction.dest_conjunction t |
34 (Conjunction.dest_conjunction t |
35 |> (fn (t1, t2) => conj_to_list (t1::t2::ts))) |
35 |> (fn (t1, t2) => conj_to_list (t1::t2::ts))) |
36 handle TERM _ => t::conj_to_list ts; |
36 handle TERM _ => t::conj_to_list ts; |
37 |
37 |
38 val crits = [(true, FindTheorems.Solves)]; |
38 val crits = [(true, FindTheorems.Solves)]; |
39 fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (!limit)) false crits)); |
39 fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (! limit)) false crits)); |
40 fun find_cterm g = (SOME g, snd (FindTheorems.find_theorems ctxt |
40 fun find_cterm g = |
41 (SOME (Goal.init g)) (SOME (!limit)) false crits)); |
41 (SOME g, snd (FindTheorems.find_theorems ctxt |
|
42 (SOME (Goal.init g)) (SOME (! limit)) false crits)); |
42 |
43 |
43 fun prt_result (goal, results) = |
44 fun prt_result (goal, results) = |
44 let |
45 let |
45 val msg = case goal of |
46 val msg = |
46 NONE => "The current goal" |
47 (case goal of |
47 | SOME g => Syntax.string_of_term ctxt (term_of g); |
48 NONE => "The current goal" |
|
49 | SOME g => Syntax.string_of_term ctxt (Thm.term_of g)); |
48 in |
50 in |
49 Pretty.big_list (msg ^ " could be solved directly with:") |
51 Pretty.big_list |
50 (map (FindTheorems.pretty_thm ctxt) results) |
52 (msg ^ " could be solved directly with:") |
|
53 (map (FindTheorems.pretty_thm ctxt) results) |
51 end; |
54 end; |
52 |
55 |
53 fun seek_against_goal () = |
56 fun seek_against_goal () = |
54 let |
57 let |
55 val goal = try Proof.get_goal state |
58 val goal = try Proof.get_goal state |
56 |> Option.map (#2 o #2); |
59 |> Option.map (#2 o #2); |
57 |
60 |
58 val goals = goal |
61 val goals = goal |
59 |> Option.map (fn g => cprem_of g 1) |
62 |> Option.map (fn g => cprem_of g 1) |
60 |> the_list |
63 |> the_list |
61 |> conj_to_list; |
64 |> conj_to_list; |
62 |
65 |
63 val rs = if length goals = 1 |
66 val rs = |
64 then [find goal] |
67 if length goals = 1 |
65 else map find_cterm goals; |
68 then [find goal] |
66 val frs = filter_out (null o snd) rs; |
69 else map find_cterm goals; |
|
70 val results = filter_out (null o snd) rs; |
67 |
71 |
68 in if null frs then NONE else SOME frs end; |
72 in if null results then NONE else SOME results end; |
69 |
73 |
70 fun go () = |
74 fun go () = |
71 let |
75 let |
72 val res = TimeLimit.timeLimit |
76 val res = |
73 (Time.fromMilliseconds (! auto_time_limit)) |
77 TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit)) |
74 (try seek_against_goal) (); |
78 (try seek_against_goal) (); |
75 in |
79 in |
76 case Option.join res of |
80 (case res of |
77 NONE => state |
81 SOME (SOME results) => |
78 | SOME results => (Proof.goal_message |
82 state |> Proof.goal_message |
79 (fn () => Pretty.chunks [Pretty.str "", |
83 (fn () => Pretty.chunks |
80 Pretty.markup Markup.hilite |
84 [Pretty.str "", |
81 (Library.separate (Pretty.brk 0) |
85 Pretty.markup Markup.hilite |
82 (map prt_result results))]) |
86 (separate (Pretty.brk 0) (map prt_result results))]) |
83 state) |
87 | NONE => state) |
84 end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); |
88 end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); |
85 in |
89 in |
86 if int andalso ! auto andalso not (! Toplevel.quiet) |
90 if int andalso ! auto andalso not (! Toplevel.quiet) |
87 then go () |
91 then go () |
88 else state |
92 else state |