40 (* solve_direct command *) |
40 (* solve_direct command *) |
41 |
41 |
42 fun do_solve_direct mode state = |
42 fun do_solve_direct mode state = |
43 let |
43 let |
44 val ctxt = Proof.context_of state; |
44 val ctxt = Proof.context_of state; |
45 val find_ctxt = if mode = Auto_Try then Context_Position.set_visible false ctxt else ctxt; |
45 val find_ctxt = |
|
46 if mode = Auto_Try then Context_Position.set_visible false ctxt else ctxt; |
46 |
47 |
47 val crits = [(true, Find_Theorems.Solves)]; |
48 fun find goal = |
48 fun find g = |
49 #2 (Find_Theorems.find_theorems find_ctxt (SOME goal) |
49 snd (Find_Theorems.find_theorems find_ctxt (SOME g) |
50 (SOME (Config.get find_ctxt max_solutions)) false [(true, Find_Theorems.Solves)]); |
50 (SOME (Config.get find_ctxt max_solutions)) false crits); |
|
51 |
51 |
52 fun prt_result (goal, results) = |
52 fun prt_result (goal, results) = |
53 let |
53 let |
54 val msg = |
54 val msg = |
55 (if mode = Auto_Try then "Auto " else "") ^ solve_directN ^ ": " ^ |
55 (if mode = Auto_Try then "Auto " else "") ^ solve_directN ^ ": " ^ |
63 end; |
63 end; |
64 |
64 |
65 fun seek_against_goal () = |
65 fun seek_against_goal () = |
66 (case try Proof.simple_goal state of |
66 (case try Proof.simple_goal state of |
67 NONE => NONE |
67 NONE => NONE |
68 | SOME {goal = st, ...} => |
68 | SOME {goal, ...} => |
69 let |
69 let |
70 val subgoals = Drule.strip_imp_prems (Thm.cprop_of st); |
70 val subgoals = Drule.strip_imp_prems (Thm.cprop_of goal); |
71 val rs = |
71 val rs = |
72 if length subgoals = 1 |
72 if length subgoals = 1 |
73 then [(NONE, find st)] |
73 then [(NONE, find goal)] |
74 else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; |
74 else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; |
75 val results = filter_out (null o snd) rs; |
75 val results = filter_out (null o #2) rs; |
76 in if null results then NONE else SOME results end); |
76 in if null results then NONE else SOME results end); |
77 fun message results = separate (Pretty.brk 0) (map prt_result results); |
77 fun message results = separate (Pretty.brk 0) (map prt_result results); |
78 in |
78 in |
79 (case try seek_against_goal () of |
79 (case try seek_against_goal () of |
80 SOME (SOME results) => |
80 SOME (SOME results) => |
81 (someN, |
81 (someN, |
82 let |
82 let |
83 val msg = Pretty.string_of (Pretty.chunks (message results)) |
83 val msg = Pretty.string_of (Pretty.chunks (message results)) |
84 in |
84 in |
85 if Config.get ctxt strict_warnings |
85 if Config.get ctxt strict_warnings then (warning msg; []) |
86 then (warning msg; []) |
86 else if mode = Auto_Try then [msg] |
87 else if mode = Auto_Try |
87 else (writeln msg; []) |
88 then [msg] |
|
89 else (writeln msg; []) |
|
90 end) |
88 end) |
91 | SOME NONE => |
89 | SOME NONE => |
92 (if mode = Normal then writeln "No proof found" |
90 (if mode = Normal then writeln "No proof found" else (); |
93 else (); |
|
94 (noneN, [])) |
91 (noneN, [])) |
95 | NONE => |
92 | NONE => |
96 (if mode = Normal then writeln "An error occurred" |
93 (if mode = Normal then writeln "An error occurred" else (); |
97 else (); |
|
98 (unknownN, []))) |
94 (unknownN, []))) |
99 end |
95 end |
100 |> `(fn (outcome_code, _) => outcome_code = someN); |
96 |> `(fn (outcome_code, _) => outcome_code = someN); |
101 |
97 |
102 val solve_direct = do_solve_direct Normal |
98 val solve_direct = do_solve_direct Normal |