|
1 (* Title: HOL/Tools/ATP/atp_satallax.ML |
|
2 Author: Mathias Fleury, ENS Rennes |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Satallax proof parser and transformation for Sledgehammer. |
|
6 *) |
|
7 |
|
8 signature ATP_SATALLAX = |
|
9 sig |
|
10 val atp_proof_of_tstplike_proof : string -> string ATP_Proof.atp_problem -> string -> |
|
11 string ATP_Proof.atp_proof |
|
12 end; |
|
13 |
|
14 structure ATP_Satallax : ATP_SATALLAX = |
|
15 struct |
|
16 |
|
17 open ATP_Proof |
|
18 open ATP_Util |
|
19 open ATP_Problem |
|
20 |
|
21 (*Undocumented format: |
|
22 thf (number, plain | Axiom | ..., inference(rule, [status(thm), assumptions ([hypotheses list]), |
|
23 detailed_rule(discharge,used_hypothese_list) *], used_hypotheses_list, premises)) |
|
24 (seen by tab_mat) |
|
25 |
|
26 Also seen -- but we can ignore it: |
|
27 "tab_inh (a) __11." meaning that the type a is inhabited usueful of variable eigen__11, |
|
28 *) |
|
29 fun parse_satallax_tstp_information x = |
|
30 ((Symbol.scan_ascii_id || ($$ "$" |-- Symbol.scan_ascii_id)) |
|
31 -- Scan.option ( $$ "(" |-- Scan.option (Symbol.scan_ascii_id --| $$ ",") |
|
32 -- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id |
|
33 -- Scan.repeat ($$ "," |-- scan_general_id)) >> uncurry cons) --| $$ "]")) |
|
34 || skip_term >> K NONE) >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x |
|
35 |
|
36 fun parse_prem x = |
|
37 ((Symbol.scan_ascii_id || scan_general_id) --| Scan.option ($$ ":" -- skip_term)) x |
|
38 |
|
39 fun parse_prems x = |
|
40 (($$ "[" |-- parse_prem -- Scan.repeat ($$ "," |-- parse_prem) --| $$ "]") |
|
41 >> uncurry cons) x |
|
42 |
|
43 fun parse_tstp_satallax_extra_arguments x = |
|
44 ($$ "," |-- scan_general_id -- (($$ "(" |-- Symbol.scan_ascii_id --| $$ "," ) |
|
45 -- ($$ "[" |-- Scan.option ((parse_satallax_tstp_information |
|
46 -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> uncurry cons) |
|
47 --| $$ "]") -- |
|
48 (Scan.optional ($$ "," |-- parse_prems) [] -- Scan.optional ($$ "," |-- parse_prems) [] |
|
49 >> (fn (x, []) => x | (_, x) => x)) |
|
50 --| $$ ")")) x |
|
51 |
|
52 val dummy_satallax_step = ((("~1", "tab_inh"), AAtom (ATerm(("False", []), []))), NONE) |
|
53 fun parse_tstp_thf0_satallax_line x = |
|
54 (((Scan.this_string tptp_thf |
|
55 -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," |
|
56 -- parse_thf0_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".") |
|
57 || (Scan.this_string "tab_inh" |-- skip_term --| $$ ".") |
|
58 >> K dummy_satallax_step) x |
|
59 |
|
60 |
|
61 datatype satallax_step = Satallax_Step of { |
|
62 id: string, |
|
63 role: string, |
|
64 theorem: (string, string, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, string) |
|
65 ATP_Problem.atp_formula, |
|
66 assumptions: string list, |
|
67 rule: string, |
|
68 used_assumptions: string list, |
|
69 generated_goal_assumptions: (string * string list) list} |
|
70 |
|
71 fun mk_satallax_step id role theorem assumptions rule used_assumptions |
|
72 generated_goal_assumptions = |
|
73 Satallax_Step {id = id, role = role, theorem = theorem, assumptions = assumptions, rule = rule, |
|
74 used_assumptions = used_assumptions, generated_goal_assumptions = generated_goal_assumptions} |
|
75 |
|
76 fun get_assumptions (("assumptions", SOME (_ , assumptions)) :: _) = |
|
77 the_default [] assumptions |
|
78 | get_assumptions (_ :: l) = get_assumptions l |
|
79 | get_assumptions [] = [] |
|
80 |
|
81 fun seperate_dependices dependencies = |
|
82 let |
|
83 fun sep_dep [] used_assumptions new_goals generated_assumptions _ = |
|
84 (used_assumptions, new_goals, generated_assumptions) |
|
85 | sep_dep (x :: l) used_assumptions new_goals generated_assumptions state = |
|
86 if hd (raw_explode x) = "h" orelse Int.fromString x = NONE then |
|
87 if state = 0 then |
|
88 sep_dep l (x :: used_assumptions) new_goals generated_assumptions state |
|
89 else |
|
90 sep_dep l used_assumptions new_goals (x :: generated_assumptions) 3 |
|
91 else |
|
92 if state = 1 orelse state = 0 then |
|
93 sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1 |
|
94 else |
|
95 raise Fail ("incorrect Satallax proof" ^ PolyML.makestring l) |
|
96 in |
|
97 sep_dep dependencies [] [] [] 0 |
|
98 end |
|
99 |
|
100 fun create_grouped_goal_assumption rule new_goals generated_assumptions = |
|
101 if length new_goals = length generated_assumptions then |
|
102 new_goals ~~ (map single generated_assumptions) |
|
103 else if 2 * length new_goals = length generated_assumptions then |
|
104 let |
|
105 fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) = |
|
106 (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions |
|
107 | group_by_pair [] [] = [] |
|
108 in |
|
109 group_by_pair new_goals generated_assumptions |
|
110 end |
|
111 else |
|
112 raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.") |
|
113 |
|
114 fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) = |
|
115 let |
|
116 val (used_assumptions, new_goals, generated_assumptions) = seperate_dependices used_rules |
|
117 in |
|
118 mk_satallax_step id role formula (get_assumptions (the_default [] l)) rule used_assumptions |
|
119 (create_grouped_goal_assumption rule new_goals generated_assumptions) |
|
120 end |
|
121 | to_satallax_step (((id, role), formula), NONE) = |
|
122 mk_satallax_step id role formula [] "assumption" [] [] |
|
123 |
|
124 fun is_assumption (Satallax_Step {role, ...}) = role = "assumption" orelse role = "axiom" orelse |
|
125 role = "negated_conjecture" orelse role = "conjecture" |
|
126 |
|
127 fun seperate_assumptions_and_steps l = |
|
128 let |
|
129 fun seperate_assumption [] l l' = (l, l') |
|
130 | seperate_assumption (step :: steps) l l' = |
|
131 if is_assumption step then |
|
132 seperate_assumption steps (step :: l) l' |
|
133 else |
|
134 seperate_assumption steps l (step :: l') |
|
135 in |
|
136 seperate_assumption l [] [] |
|
137 end |
|
138 |
|
139 datatype satallax_proof_graph = |
|
140 Node_Source of {node: satallax_step, succs: satallax_proof_graph list} | |
|
141 Node_Conclusion of {node: satallax_step, deps: satallax_proof_graph list} |
|
142 |
|
143 fun find_proof_step ((x as Satallax_Step {id, ...}) :: l) h = |
|
144 if h = id then x else find_proof_step l h |
|
145 | find_proof_step [] h = raise Fail ("not_found: " ^ PolyML.makestring h) |
|
146 |
|
147 fun remove_not_not (x as ATerm ((op1, _), [ATerm ((op2, _), [th])])) = |
|
148 if op1 = op2 andalso op1 = tptp_not then th else x |
|
149 | remove_not_not th = th |
|
150 |
|
151 fun tptp_term_equal (ATerm((op1, _), l1), ATerm((op2, _), l2)) = op1 = op2 andalso |
|
152 fold2 (fn t1 => fn t2 => fn c => c andalso t1 = t2) l1 l2 true |
|
153 | tptp_term_equal (_, _) = false |
|
154 |
|
155 fun find_assumptions_to_inline ths (assm :: assms) to_inline no_inline = |
|
156 (case List.find (curry (op =) assm o fst) no_inline of |
|
157 SOME _ => find_assumptions_to_inline ths assms to_inline no_inline |
|
158 | NONE => |
|
159 (case List.find (curry (op =) assm o fst) to_inline of |
|
160 NONE => find_assumptions_to_inline ths assms to_inline no_inline |
|
161 | SOME (_, th) => |
|
162 let |
|
163 val simplified_ths_with_inlined_assumption = |
|
164 (case List.partition (curry tptp_term_equal th o remove_not_not) ths of |
|
165 ([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths |
|
166 | (_, _) => []) |
|
167 in |
|
168 find_assumptions_to_inline simplified_ths_with_inlined_assumption assms to_inline no_inline |
|
169 end)) |
|
170 | find_assumptions_to_inline ths [] _ _ = ths |
|
171 |
|
172 fun inline_if_needed_and_simplify th assms to_inline no_inline = |
|
173 (case find_assumptions_to_inline [] assms to_inline no_inline of |
|
174 [] => ATerm (("$true", [dummy_atype]), []) |
|
175 | l => foldl1 (fn (a, b) => ATerm ((tptp_or, [dummy_atype]), [a, b])) l) |
|
176 |
|
177 |
|
178 fun get_conclusion (Satallax_Step {theorem = AAtom theorem, ...}) = theorem |
|
179 |
|
180 fun add_assumption new_used_assumptions ((Satallax_Step {id, role, theorem, assumptions, |
|
181 rule, generated_goal_assumptions, used_assumptions})) = |
|
182 mk_satallax_step id role theorem assumptions rule (new_used_assumptions @ used_assumptions) |
|
183 generated_goal_assumptions |
|
184 |
|
185 fun set_rule new_rule (Satallax_Step {id, role, theorem, assumptions, |
|
186 generated_goal_assumptions, used_assumptions, ...}) = |
|
187 mk_satallax_step id role theorem assumptions new_rule used_assumptions |
|
188 generated_goal_assumptions |
|
189 |
|
190 fun transform_inline_assumption hypotheses_step proof_sketch = |
|
191 let |
|
192 fun inline_in_step (Node_Source {node as Satallax_Step {generated_goal_assumptions, |
|
193 used_assumptions, rule, ...}, succs}) = |
|
194 if generated_goal_assumptions = [] then |
|
195 Node_Source {node = node, succs = []} |
|
196 else |
|
197 let |
|
198 (*one singel goal is created, two hypothesis can be created, for the "and" rule: |
|
199 (A /\ B) create two hypotheses A, and B.*) |
|
200 fun set_hypotheses_as_goal [hypothesis] succs = |
|
201 Node_Source {node = set_rule rule |
|
202 (add_assumption used_assumptions (find_proof_step hypotheses_step hypothesis)), |
|
203 succs = map inline_in_step succs} |
|
204 | set_hypotheses_as_goal (hypothesis :: new_goal_hypotheses) succs = |
|
205 Node_Source {node = set_rule rule |
|
206 (add_assumption used_assumptions (find_proof_step hypotheses_step hypothesis)), |
|
207 succs = [set_hypotheses_as_goal new_goal_hypotheses succs]} |
|
208 in |
|
209 set_hypotheses_as_goal (snd (hd generated_goal_assumptions)) succs |
|
210 end |
|
211 | inline_in_step (Node_Conclusion {node = node, deps}) = |
|
212 Node_Conclusion {node = node, deps = map inline_in_step deps} |
|
213 |
|
214 fun inline_contradictory_assumptions (Node_Source {node as Satallax_Step{id, theorem, ...}, |
|
215 succs}) (to_inline, no_inline) = |
|
216 let |
|
217 val (succs, inliner) = fold_map inline_contradictory_assumptions |
|
218 succs (to_inline, (id, theorem) :: no_inline) |
|
219 in |
|
220 (Node_Source {node = node, succs = succs}, inliner) |
|
221 end |
|
222 | inline_contradictory_assumptions (Node_Conclusion {node = Satallax_Step {id, role, |
|
223 theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions, |
|
224 used_assumptions}, deps}) (to_inline, no_inline) = |
|
225 let |
|
226 val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions |
|
227 deps (to_inline, no_inline) |
|
228 val to_inline'' = map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s))) |
|
229 (List.filter (fn s => nth_string s 0 = "h") |
|
230 (used_assumptions @ |
|
231 (map snd generated_goal_assumptions |> flat))) |
|
232 @ to_inline' |
|
233 val node' = Satallax_Step {id = id, role = role, theorem = |
|
234 AAtom (inline_if_needed_and_simplify theorem assumptions to_inline'' no_inline'), |
|
235 assumptions = assumptions, rule = rule, |
|
236 generated_goal_assumptions = generated_goal_assumptions, |
|
237 used_assumptions = |
|
238 List.filter (fn s => List.find (curry (op =) s o fst) to_inline = NONE) |
|
239 used_assumptions} |
|
240 in |
|
241 (Node_Conclusion {node = node', deps = dep'}, (to_inline'', no_inline')) |
|
242 end |
|
243 in |
|
244 fst (inline_contradictory_assumptions (inline_in_step proof_sketch) ([], [])) |
|
245 end |
|
246 |
|
247 fun correct_dependencies (Node_Source {node, succs}) = |
|
248 Node_Source {node = node, succs = map correct_dependencies succs} |
|
249 | correct_dependencies (Node_Conclusion {node, deps}) = |
|
250 let |
|
251 val new_used_assumptions = |
|
252 map (fn Node_Source {node = (Satallax_Step{id, ...}), ...} => id |
|
253 | Node_Conclusion {node = (Satallax_Step{id, ...}), ...} => id) deps |
|
254 in |
|
255 Node_Conclusion {node = add_assumption new_used_assumptions node, |
|
256 deps = map correct_dependencies deps} |
|
257 end |
|
258 |
|
259 fun create_satallax_proof_graph (hypotheses_step, proof_sketch) = |
|
260 let |
|
261 fun create_step (step as Satallax_Step {generated_goal_assumptions, ...}) = |
|
262 Node_Source {node = step, |
|
263 succs = map (create_step o (find_proof_step (hypotheses_step @ proof_sketch))) |
|
264 (map fst generated_goal_assumptions)} |
|
265 fun reverted_discharged_steps is_branched (Node_Source {node as |
|
266 Satallax_Step {generated_goal_assumptions, ...}, succs}) = |
|
267 if is_branched orelse length generated_goal_assumptions > 1 then |
|
268 Node_Conclusion {node = node, deps = map (reverted_discharged_steps true) succs} |
|
269 else |
|
270 Node_Source {node = node, succs = map (reverted_discharged_steps is_branched) succs} |
|
271 val proof_with_correct_sense = |
|
272 correct_dependencies (reverted_discharged_steps false |
|
273 (create_step (find_proof_step proof_sketch "0" ))) |
|
274 in |
|
275 transform_inline_assumption hypotheses_step proof_with_correct_sense |
|
276 end |
|
277 |
|
278 val satallax_known_theorems = ["eq_ind", "eq_trans2", "eq_trans3", "eq_neg_neg_id", "eq_true", |
|
279 "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq", |
|
280 "eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4", |
|
281 "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"] |
|
282 val is_special_satallax_rule = member (op =) satallax_known_theorems |
|
283 |
|
284 |
|
285 fun transform_to_standard_atp_step proof = |
|
286 let |
|
287 fun create_fact_step id = |
|
288 ((id, [id]), Axiom, AAtom (ATerm((id, []), [])), "", []) |
|
289 fun transform_one_step (Satallax_Step {id, theorem, used_assumptions, role, rule, ...}) = |
|
290 let |
|
291 val role' = role_of_tptp_string role |
|
292 in |
|
293 map create_fact_step |
|
294 (List.filter (fn s => size s >=4 andalso not (is_special_satallax_rule s)) |
|
295 used_assumptions) |
|
296 @ [((id, []), if role' = Unknown then Plain else role', theorem, rule, |
|
297 map (fn s => (s, [])) used_assumptions)] |
|
298 end |
|
299 |
|
300 fun transform_steps (Node_Source {node, succs}) = |
|
301 transform_one_step node @ (map transform_steps succs |> flat) |
|
302 | transform_steps (Node_Conclusion {node, deps}) = |
|
303 ((map transform_steps deps) |> flat) @ (transform_one_step node) |
|
304 in |
|
305 transform_steps proof |
|
306 end |
|
307 |
|
308 |
|
309 fun parse_proof local_name problem = |
|
310 strip_spaces_except_between_idents |
|
311 #> raw_explode |
|
312 #> |
|
313 (if local_name <> satallaxN then |
|
314 (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
|
315 (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat))) |
|
316 #> fst) |
|
317 else |
|
318 (Scan.error (!! (fn f => raise UNRECOGNIZED_ATP_PROOF ()) |
|
319 (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line)))) |
|
320 #> fst |
|
321 #> rev |
|
322 #> map to_satallax_step |
|
323 #> seperate_assumptions_and_steps |
|
324 #> create_satallax_proof_graph |
|
325 #> transform_to_standard_atp_step)) |
|
326 |
|
327 |
|
328 fun atp_proof_of_tstplike_proof _ _ "" = [] |
|
329 | atp_proof_of_tstplike_proof local_prover problem tstp = |
|
330 (case core_of_agsyhol_proof tstp of |
|
331 SOME facts => facts |> map (core_inference agsyhol_core_rule) |
|
332 | NONE => |
|
333 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
|
334 |> parse_proof local_prover problem |
|
335 |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1))) |
|
336 |> local_prover = zipperpositionN ? rev) |
|
337 |
|
338 |
|
339 end; |