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 ( $$ "(" |
|
32 |-- (Scan.option (Symbol.scan_ascii_id --| $$ ",") |
|
33 -- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id |
|
34 -- Scan.repeat ($$ "," |-- scan_general_id)) >> op ::) --| $$ "]")) |
|
35 || (scan_general_id) >> (fn x => SOME [x])) |
|
36 >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")")) |
|
37 || (skip_term >> K (NONE, NONE)))) x |
|
38 |
|
39 fun parse_prem x = |
|
40 ((Symbol.scan_ascii_id || scan_general_id) --| Scan.option ($$ ":" -- skip_term)) x |
|
41 |
|
42 fun parse_prems x = |
|
43 (($$ "[" |-- parse_prem -- Scan.repeat ($$ "," |-- parse_prem) --| $$ "]") |
|
44 >> op ::) x |
|
45 |
|
46 fun parse_tstp_satallax_extra_arguments x = |
|
47 ($$ "," |-- scan_general_id -- (($$ "(" |-- Symbol.scan_ascii_id --| $$ "," ) |
|
48 -- ($$ "[" |-- Scan.option ((parse_satallax_tstp_information |
|
49 -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> op ::) |
|
50 --| $$ "]") -- |
|
51 (Scan.optional ($$ "," |-- parse_prems) [] -- Scan.optional ($$ "," |-- parse_prems) [] |
|
52 >> (fn (x, []) => x | (_, x) => x)) |
|
53 --| $$ ")")) x |
|
54 |
|
55 val dummy_satallax_step = ((("~1", "tab_inh"), AAtom (ATerm(("False", []), []))), NONE) |
|
56 fun parse_tstp_thf0_satallax_line x = |
|
57 (((Scan.this_string tptp_thf |
|
58 -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," |
|
59 -- parse_hol_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".") |
|
60 || (Scan.this_string "tab_inh" |-- skip_term --| $$ ".") |
|
61 >> K dummy_satallax_step) x |
|
62 |
|
63 datatype satallax_step = Satallax_Step of { |
|
64 id: string, |
|
65 role: string, |
|
66 theorem: (string, string, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, string) |
|
67 ATP_Problem.atp_formula, |
|
68 assumptions: string list, |
|
69 rule: string, |
|
70 used_assumptions: string list, |
|
71 detailed_eigen: string, |
|
72 generated_goal_assumptions: (string * string list) list} |
|
73 |
|
74 fun mk_satallax_step id role theorem assumptions rule used_assumptions |
|
75 generated_goal_assumptions detailed_eigen = |
|
76 Satallax_Step {id = id, role = role, theorem = theorem, assumptions = assumptions, rule = rule, |
|
77 used_assumptions = used_assumptions, generated_goal_assumptions = generated_goal_assumptions, |
|
78 detailed_eigen = detailed_eigen} |
|
79 |
|
80 fun get_assumptions (("assumptions", SOME (_ , assumptions)) :: _) = |
|
81 the_default [] assumptions |
|
82 | get_assumptions (_ :: l) = get_assumptions l |
|
83 | get_assumptions [] = [] |
|
84 |
|
85 fun get_detailled_eigen ((_, SOME (SOME "eigenvar" , var)) :: _) = |
|
86 hd (the_default [""] var) |
|
87 | get_detailled_eigen (_ :: l) = get_detailled_eigen l |
|
88 | get_detailled_eigen [] = "" |
|
89 |
|
90 fun seperate_dependices dependencies = |
|
91 let |
|
92 fun sep_dep [] used_assumptions new_goals generated_assumptions _ = |
|
93 (used_assumptions, new_goals, generated_assumptions) |
|
94 | sep_dep (x :: l) used_assumptions new_goals generated_assumptions state = |
|
95 if hd (raw_explode x) = "h" orelse Int.fromString x = NONE then |
|
96 if state = 0 then |
|
97 sep_dep l (x :: used_assumptions) new_goals generated_assumptions state |
|
98 else |
|
99 sep_dep l used_assumptions new_goals (x :: generated_assumptions) 3 |
|
100 else |
|
101 if state = 1 orelse state = 0 then |
|
102 sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1 |
|
103 else |
|
104 raise Fail ("incorrect Satallax proof: " ^ \<^make_string> l) |
|
105 in |
|
106 sep_dep dependencies [] [] [] 0 |
|
107 end |
|
108 |
|
109 fun create_grouped_goal_assumption rule new_goals generated_assumptions = |
|
110 let |
|
111 val number_of_new_goals = length new_goals |
|
112 val number_of_new_assms = length generated_assumptions |
|
113 in |
|
114 if number_of_new_goals = number_of_new_assms then |
|
115 new_goals ~~ (map single generated_assumptions) |
|
116 else if 2 * number_of_new_goals = number_of_new_assms then |
|
117 let |
|
118 fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) = |
|
119 (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions |
|
120 | group_by_pair [] [] = [] |
|
121 in |
|
122 group_by_pair new_goals generated_assumptions |
|
123 end |
|
124 else |
|
125 raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction") |
|
126 end |
|
127 |
|
128 fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) = |
|
129 let |
|
130 val (used_assumptions, new_goals, generated_assumptions) = seperate_dependices used_rules |
|
131 in |
|
132 mk_satallax_step id role formula (get_assumptions (the_default [] l)) rule used_assumptions |
|
133 (create_grouped_goal_assumption rule new_goals generated_assumptions) |
|
134 (get_detailled_eigen (the_default [] l)) |
|
135 end |
|
136 | to_satallax_step (((id, role), formula), NONE) = |
|
137 mk_satallax_step id role formula [] "assumption" [] [] "" |
|
138 |
|
139 fun is_assumption (Satallax_Step {role, ...}) = role = "assumption" orelse role = "axiom" orelse |
|
140 role = "negated_conjecture" orelse role = "conjecture" |
|
141 |
|
142 fun seperate_assumptions_and_steps l = |
|
143 let |
|
144 fun seperate_assumption [] l l' = (l, l') |
|
145 | seperate_assumption (step :: steps) l l' = |
|
146 if is_assumption step then |
|
147 seperate_assumption steps (step :: l) l' |
|
148 else |
|
149 seperate_assumption steps l (step :: l') |
|
150 in |
|
151 seperate_assumption l [] [] |
|
152 end |
|
153 |
|
154 datatype satallax_proof_graph = |
|
155 Linear_Part of {node: satallax_step, succs: satallax_proof_graph list} | |
|
156 Tree_Part of {node: satallax_step, deps: satallax_proof_graph list} |
|
157 |
|
158 fun find_proof_step ((x as Satallax_Step {id, ...}) :: l) h = |
|
159 if h = id then x else find_proof_step l h |
|
160 | find_proof_step [] h = raise Fail ("not_found: " ^ \<^make_string> h ^ " (probably a parsing \ |
|
161 \error)") |
|
162 |
|
163 fun remove_not_not (x as ATerm ((op1, _), [ATerm ((op2, _), [th])])) = |
|
164 if op1 = op2 andalso op1 = tptp_not then th else x |
|
165 | remove_not_not th = th |
|
166 |
|
167 fun tptp_term_equal (ATerm((op1, _), l1), ATerm((op2, _), l2)) = op1 = op2 andalso |
|
168 fold2 (fn t1 => fn t2 => fn c => c andalso t1 = t2) l1 l2 true |
|
169 | tptp_term_equal (_, _) = false |
|
170 |
|
171 val dummy_true_aterm = ATerm (("$true", [dummy_atype]), []) |
|
172 |
|
173 fun find_assumptions_to_inline ths (assm :: assms) to_inline no_inline = |
|
174 (case List.find (curry (op =) assm o fst) no_inline of |
|
175 SOME _ => find_assumptions_to_inline ths assms to_inline no_inline |
|
176 | NONE => |
|
177 (case List.find (curry (op =) assm o fst) to_inline of |
|
178 NONE => find_assumptions_to_inline ths assms to_inline no_inline |
|
179 | SOME (_, th) => |
|
180 let |
|
181 val simplified_ths_with_inlined_asms = |
|
182 (case List.partition (curry tptp_term_equal th o remove_not_not) ths of |
|
183 ([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths |
|
184 | (_, _) => []) |
|
185 in |
|
186 find_assumptions_to_inline simplified_ths_with_inlined_asms assms to_inline no_inline |
|
187 end)) |
|
188 | find_assumptions_to_inline ths [] _ _ = ths |
|
189 |
|
190 fun inline_if_needed_and_simplify th assms to_inline no_inline = |
|
191 (case find_assumptions_to_inline [th] assms to_inline no_inline of |
|
192 [] => dummy_true_aterm |
|
193 | l => foldl1 (fn (a, b) => |
|
194 (case b of |
|
195 ATerm (("$false", _), _) => a |
|
196 | ATerm (("~", _ ), [ATerm (("$true", _), _)]) => a |
|
197 | _ => ATerm ((tptp_or, [dummy_atype]), [a, b]))) l) |
|
198 |
|
199 fun get_conclusion (Satallax_Step {theorem = AAtom theorem, ...}) = theorem |
|
200 |
|
201 fun add_assumptions new_used_assumptions (Satallax_Step {id, role, theorem, assumptions, |
|
202 rule, generated_goal_assumptions, used_assumptions, detailed_eigen}) = |
|
203 mk_satallax_step id role theorem assumptions rule (new_used_assumptions @ used_assumptions) |
|
204 generated_goal_assumptions detailed_eigen |
|
205 |
|
206 fun set_rule new_rule (Satallax_Step {id, role, theorem, assumptions, |
|
207 generated_goal_assumptions, used_assumptions, detailed_eigen, ...}) = |
|
208 mk_satallax_step id role theorem assumptions new_rule used_assumptions |
|
209 generated_goal_assumptions detailed_eigen |
|
210 |
|
211 fun add_detailled_eigen eigen (Satallax_Step {id, role, theorem, assumptions, |
|
212 rule, generated_goal_assumptions, used_assumptions, detailed_eigen}) = |
|
213 mk_satallax_step id role theorem assumptions rule used_assumptions |
|
214 generated_goal_assumptions (if detailed_eigen <> "" then detailed_eigen else eigen) |
|
215 |
|
216 fun transform_inline_assumption hypotheses_step proof_sketch = |
|
217 let |
|
218 fun inline_in_step (Linear_Part {node as Satallax_Step {generated_goal_assumptions, |
|
219 used_assumptions, rule, detailed_eigen, ...}, succs}) = |
|
220 if generated_goal_assumptions = [] then |
|
221 Linear_Part {node = node, succs = []} |
|
222 else |
|
223 let |
|
224 (*one single goal is created, two hypothesis can be created, for the "and" rule: |
|
225 (A /\ B) create two hypotheses A, and B.*) |
|
226 fun set_hypotheses_as_goal [hypothesis] succs = |
|
227 Linear_Part {node = add_detailled_eigen detailed_eigen |
|
228 (set_rule rule (add_assumptions used_assumptions |
|
229 (find_proof_step hypotheses_step hypothesis))), |
|
230 succs = map inline_in_step succs} |
|
231 | set_hypotheses_as_goal (hypothesis :: new_goal_hypotheses) succs = |
|
232 Linear_Part {node = set_rule rule (add_assumptions used_assumptions |
|
233 (find_proof_step hypotheses_step hypothesis)), |
|
234 succs = [set_hypotheses_as_goal new_goal_hypotheses succs]} |
|
235 in |
|
236 set_hypotheses_as_goal (snd (hd generated_goal_assumptions)) succs |
|
237 end |
|
238 | inline_in_step (Tree_Part {node = node, deps}) = |
|
239 Tree_Part {node = node, deps = map inline_in_step deps} |
|
240 |
|
241 fun inline_contradictory_assumptions (Linear_Part {node as Satallax_Step{id, theorem, ...}, |
|
242 succs}) (to_inline, no_inline) = |
|
243 let |
|
244 val (succs, inliner) = fold_map inline_contradictory_assumptions succs |
|
245 (to_inline, (id, theorem) :: no_inline) |
|
246 in |
|
247 (Linear_Part {node = node, succs = succs}, inliner) |
|
248 end |
|
249 | inline_contradictory_assumptions (Tree_Part {node = Satallax_Step {id, role, |
|
250 theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions, |
|
251 used_assumptions, detailed_eigen}, deps}) (to_inline, no_inline) = |
|
252 let |
|
253 val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions deps |
|
254 (to_inline, no_inline) |
|
255 val to_inline'' = |
|
256 map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s))) |
|
257 (filter (fn s => (nth_string s 0 = "h") andalso List.find (curry (op =) s o fst) |
|
258 no_inline' = NONE) (used_assumptions @ (map snd generated_goal_assumptions |> flat))) |
|
259 @ to_inline' |
|
260 val node' = Satallax_Step {id = id, role = role, theorem = |
|
261 AAtom (inline_if_needed_and_simplify theorem assumptions to_inline'' no_inline'), |
|
262 assumptions = assumptions, rule = rule, |
|
263 generated_goal_assumptions = generated_goal_assumptions, detailed_eigen = detailed_eigen, |
|
264 used_assumptions = |
|
265 filter (fn s => List.find (curry (op =) s o fst) to_inline'' = NONE) |
|
266 used_assumptions} |
|
267 in |
|
268 (Tree_Part {node = node', deps = dep'}, (to_inline'', no_inline')) |
|
269 end |
|
270 in |
|
271 fst (inline_contradictory_assumptions (inline_in_step proof_sketch) ([], [])) |
|
272 end |
|
273 |
|
274 fun correct_dependencies (Linear_Part {node, succs}) = |
|
275 Linear_Part {node = node, succs = map correct_dependencies succs} |
|
276 | correct_dependencies (Tree_Part {node, deps}) = |
|
277 let |
|
278 val new_used_assumptions = |
|
279 map (fn Linear_Part {node = (Satallax_Step{id, ...}), ...} => id |
|
280 | Tree_Part {node = (Satallax_Step{id, ...}), ...} => id) deps |
|
281 in |
|
282 Tree_Part {node = add_assumptions new_used_assumptions node, |
|
283 deps = map correct_dependencies deps} |
|
284 end |
|
285 |
|
286 fun create_satallax_proof_graph (hypotheses_step, proof_sketch) = |
|
287 let |
|
288 fun create_step (step as Satallax_Step {generated_goal_assumptions, ...}) = |
|
289 Linear_Part {node = step, |
|
290 succs = map (create_step o (find_proof_step (hypotheses_step @ proof_sketch))) |
|
291 (map fst generated_goal_assumptions)} |
|
292 fun reverted_discharged_steps is_branched (Linear_Part {node as |
|
293 Satallax_Step {generated_goal_assumptions, ...}, succs}) = |
|
294 if is_branched orelse length generated_goal_assumptions > 1 then |
|
295 Tree_Part {node = node, deps = map (reverted_discharged_steps true) succs} |
|
296 else |
|
297 Linear_Part {node = node, succs = map (reverted_discharged_steps is_branched) succs} |
|
298 val proof_with_correct_sense = |
|
299 correct_dependencies (reverted_discharged_steps false |
|
300 (create_step (find_proof_step proof_sketch "0" ))) |
|
301 in |
|
302 transform_inline_assumption hypotheses_step proof_with_correct_sense |
|
303 end |
|
304 |
|
305 val satallax_known_rules = ["eq_ind", "eq_trans2", "eq_trans3", "eq_neg_neg_id", "eq_true", |
|
306 "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq", |
|
307 "eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4", |
|
308 "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"] |
|
309 val is_special_satallax_rule = member (op =) satallax_known_rules |
|
310 |
|
311 fun terms_to_upper_case var (AAbs (((var', ty), b), ts)) = |
|
312 let |
|
313 val bdy = terms_to_upper_case var b |
|
314 val ts' = map (terms_to_upper_case var) ts |
|
315 in |
|
316 AAbs (((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), ty), |
|
317 bdy), ts') |
|
318 end |
|
319 | terms_to_upper_case var (ATerm ((var', ty), ts)) = |
|
320 ATerm ((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), |
|
321 ty), map (terms_to_upper_case var) ts) |
|
322 |
|
323 fun add_quantifier_in_tree_part var_rule_to_add assumption_to_add |
|
324 (Linear_Part {node as Satallax_Step {detailed_eigen, rule, ...} , succs}) = |
|
325 Linear_Part {node = node, succs = map (add_quantifier_in_tree_part |
|
326 ((detailed_eigen <> "" ? cons (detailed_eigen, rule)) var_rule_to_add) assumption_to_add) |
|
327 succs} |
|
328 | add_quantifier_in_tree_part var_rule_to_add assumption_to_add |
|
329 (Tree_Part {node = Satallax_Step {rule, detailed_eigen, id, role, theorem = AAtom th, |
|
330 assumptions, used_assumptions, generated_goal_assumptions}, deps}) = |
|
331 let |
|
332 val theorem' = fold (fn v => fn body => terms_to_upper_case (fst v) body) var_rule_to_add th |
|
333 fun add_quantified_var (var, rule) = fn body => |
|
334 let |
|
335 val quant = if rule = "tab_ex" then tptp_ho_exists else tptp_ho_forall |
|
336 val upperVar = (String.implode o (map Char.toUpper) o String.explode) var |
|
337 val quant_bdy = if rule = "tab_ex" |
|
338 then ATerm ((quant, []), [AAbs (((upperVar, dummy_atype), body), []) ]) else body |
|
339 in |
|
340 quant_bdy |
|
341 end |
|
342 val theorem'' = fold add_quantified_var var_rule_to_add theorem' |
|
343 val node' = mk_satallax_step id role (AAtom theorem'') assumptions rule |
|
344 (used_assumptions @ (filter (curry (op <=) (the (Int.fromString id)) o size) |
|
345 assumption_to_add)) generated_goal_assumptions detailed_eigen |
|
346 in |
|
347 if detailed_eigen <> "" then |
|
348 Tree_Part {node = node', |
|
349 deps = map (add_quantifier_in_tree_part ((detailed_eigen, rule) :: var_rule_to_add) |
|
350 (used_assumptions @ assumption_to_add)) deps} |
|
351 else |
|
352 Tree_Part {node = node', |
|
353 deps = map (add_quantifier_in_tree_part var_rule_to_add assumption_to_add) deps} |
|
354 end |
|
355 |
|
356 fun transform_to_standard_atp_step already_transformed proof = |
|
357 let |
|
358 fun create_fact_step id = |
|
359 ((id, [id]), Axiom, AAtom (ATerm((id, []), [])), "", []) |
|
360 fun transform_one_step already_transformed (Satallax_Step {id, theorem, used_assumptions, role, |
|
361 rule, ...}) = |
|
362 let |
|
363 val role' = role_of_tptp_string role |
|
364 val new_transformed = filter |
|
365 (fn s => size s >= 4 andalso not (is_special_satallax_rule s) andalso not |
|
366 (member (op =) already_transformed s)) used_assumptions |
|
367 in |
|
368 (map create_fact_step new_transformed |
|
369 @ [((id, []), if role' = Unknown then Plain else role', theorem, rule, |
|
370 map (fn s => (s, [])) (filter_out is_special_satallax_rule used_assumptions))], |
|
371 new_transformed @ already_transformed) |
|
372 end |
|
373 fun transform_steps (Linear_Part {node, succs}) already_transformed = |
|
374 transform_one_step already_transformed node |
|
375 ||> (fold_map transform_steps succs) |
|
376 ||> apfst flat |
|
377 |> (fn (a, (b, transformed)) => (a @ b, transformed)) |
|
378 | transform_steps (Tree_Part {node, deps}) already_transformed = |
|
379 fold_map transform_steps deps already_transformed |
|
380 |>> flat |
|
381 ||> (fn transformed => transform_one_step transformed node) |
|
382 |> (fn (a, (b, transformed)) => (a @ b, transformed)) |
|
383 in |
|
384 fst (transform_steps proof already_transformed) |
|
385 end |
|
386 |
|
387 fun remove_unused_dependency steps = |
|
388 let |
|
389 fun find_all_ids [] = [] |
|
390 | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps |
|
391 fun keep_only_used used_ids steps = |
|
392 let |
|
393 fun remove_unused (((id, ids), role, theorem, rule, deps) :: steps) = |
|
394 (((id, ids), role, theorem, rule, filter (member (op =) used_ids o fst) deps) :: steps) |
|
395 | remove_unused [] = [] |
|
396 in |
|
397 remove_unused steps |
|
398 end |
|
399 in |
|
400 keep_only_used (find_all_ids steps) steps |
|
401 end |
|
402 |
|
403 fun parse_proof local_name problem = |
|
404 strip_spaces_except_between_idents |
|
405 #> raw_explode |
|
406 #> |
|
407 (if local_name <> satallaxN then |
|
408 (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
|
409 (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem)))) |
|
410 #> fst) |
|
411 else |
|
412 (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
|
413 (Scan.finite Symbol.stopper (Scan.repeat1 parse_tstp_thf0_satallax_line))) |
|
414 #> fst |
|
415 #> rev |
|
416 #> map to_satallax_step |
|
417 #> seperate_assumptions_and_steps |
|
418 #> create_satallax_proof_graph |
|
419 #> add_quantifier_in_tree_part [] [] |
|
420 #> transform_to_standard_atp_step [] |
|
421 #> remove_unused_dependency)) |
|
422 |
|
423 fun atp_proof_of_tstplike_proof _ _ "" = [] |
|
424 | atp_proof_of_tstplike_proof local_prover problem tstp = |
|
425 (case core_of_agsyhol_proof tstp of |
|
426 SOME facts => facts |> map (core_inference agsyhol_core_rule) |
|
427 | NONE => |
|
428 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
|
429 |> parse_proof local_prover problem |
|
430 |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1))) |
|
431 |> local_prover = zipperpositionN ? rev) |
|
432 |
|
433 end; |
|