139 |
139 |
140 fun invoke_solve_direct thy t = |
140 fun invoke_solve_direct thy t = |
141 let |
141 let |
142 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) |
142 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) |
143 in |
143 in |
144 case Solve_Direct.solve_direct false state of |
144 case Solve_Direct.solve_direct state of |
145 (true, _) => (Solved, []) |
145 (true, _) => (Solved, []) |
146 | (false, _) => (Unsolved, []) |
146 | (false, _) => (Unsolved, []) |
147 end |
147 end |
148 |
148 |
149 val solve_direct_mtd = ("solve_direct", invoke_solve_direct) |
149 val solve_direct_mtd = ("solve_direct", invoke_solve_direct) |
150 |
150 |
151 (** try **) |
151 (** try **) |
152 |
152 |
153 fun invoke_try thy t = |
153 fun invoke_try_methods thy t = |
154 let |
154 let |
155 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) |
155 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) |
156 in |
156 in |
157 case Try.invoke_try (SOME (seconds 5.0)) ([], [], [], []) state of |
157 case Try_Methods.try_methods (SOME (seconds 5.0)) ([], [], [], []) state of |
158 true => (Solved, []) |
158 true => (Solved, []) |
159 | false => (Unsolved, []) |
159 | false => (Unsolved, []) |
160 end |
160 end |
161 |
161 |
162 val try_mtd = ("try", invoke_try) |
162 val try_methods_mtd = ("try_methods", invoke_try_methods) |
163 |
163 |
164 (** sledgehammer **) |
164 (** sledgehammer **) |
165 (* |
165 (* |
166 fun invoke_sledgehammer thy t = |
166 fun invoke_sledgehammer thy t = |
167 if can (Goal.prove_global thy (Term.add_free_names t []) [] t) |
167 if can (Goal.prove_global thy (Term.add_free_names t []) [] t) |
197 fun invoke_nitpick thy t = |
197 fun invoke_nitpick thy t = |
198 let |
198 let |
199 val ctxt = Proof_Context.init_global thy |
199 val ctxt = Proof_Context.init_global thy |
200 val state = Proof.init ctxt |
200 val state = Proof.init ctxt |
201 val (res, _) = Nitpick.pick_nits_in_term state |
201 val (res, _) = Nitpick.pick_nits_in_term state |
202 (Nitpick_Isar.default_params thy []) false 1 1 1 [] [] t |
202 (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] t |
203 val _ = Output.urgent_message ("Nitpick: " ^ res) |
203 val _ = Output.urgent_message ("Nitpick: " ^ res) |
204 in |
204 in |
205 (rpair []) (case res of |
205 (rpair []) (case res of |
206 "genuine" => GenuineCex |
206 "genuine" => GenuineCex |
207 | "likely_genuine" => GenuineCex |
207 | "likely_genuine" => GenuineCex |