365 |
365 |
366 fun find_formula_in_problem problem phi = |
366 fun find_formula_in_problem problem phi = |
367 problem |> maps snd |> map_filter (matching_formula_line_identifier phi) |
367 problem |> maps snd |> map_filter (matching_formula_line_identifier phi) |
368 |> try hd |
368 |> try hd |
369 |
369 |
370 (* Syntax: (cnf|fof|tff)\(<num>, <formula_role>, <formula> <extra_arguments>\). |
370 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>, |
|
371 <formula> <extra_arguments>\). |
371 The <num> could be an identifier, but we assume integers. *) |
372 The <num> could be an identifier, but we assume integers. *) |
372 fun parse_tstp_line problem = |
373 fun parse_tstp_line problem = |
373 ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff") |
374 ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff" |
374 -- $$ "(") |
375 || Scan.this_string "thf") -- $$ "(") |
375 |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ "," |
376 |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ "," |
376 -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." |
377 -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." |
377 >> (fn (((num, role), phi), deps) => |
378 >> (fn (((num, role), phi), deps) => |
378 let |
379 let |
379 val (name, deps) = |
380 val (name, deps) = |