52 else if File.exists (Path.explode (destdir')) |
52 else if File.exists (Path.explode (destdir')) |
53 then Path.append (Path.explode (destdir')) probfile |
53 then Path.append (Path.explode (destdir')) probfile |
54 else error ("No such directory: " ^ destdir') |
54 else error ("No such directory: " ^ destdir') |
55 end |
55 end |
56 |
56 |
57 (* write out problem file and call prover *) |
57 (* get clauses and prepare them for writing *) |
58 val (ctxt, (chain_ths, th)) = goal |
58 val (ctxt, (chain_ths, th)) = goal |
59 val thy = ProofContext.theory_of ctxt |
59 val thy = ProofContext.theory_of ctxt |
60 val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths |
60 val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths |
61 val probfile = prob_pathname subgoalno |
|
62 val fname = File.platform_path probfile |
|
63 val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno) |
61 val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno) |
64 handle THM ("assume: variables", _, _) => |
62 handle THM ("assume: variables", _, _) => |
65 error "Sledgehammer: Goal contains type variables (TVars)" |
63 error "Sledgehammer: Goal contains type variables (TVars)" |
66 val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls |
64 val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls |
67 val the_axiom_clauses = |
65 val the_axiom_clauses = |
75 case axiom_clauses of |
73 case axiom_clauses of |
76 NONE => clauses |
74 NONE => clauses |
77 | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy) |
75 | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy) |
78 ) |
76 ) |
79 | SOME ccs => ccs |
77 | SOME ccs => ccs |
|
78 |
|
79 (* write out problem file and call prover *) |
|
80 val probfile = prob_pathname subgoalno |
|
81 val fname = File.platform_path probfile |
80 val _ = writer fname the_const_counts clauses |
82 val _ = writer fname the_const_counts clauses |
81 val cmdline = |
83 val cmdline = |
82 if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args |
84 if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args |
83 else error ("Bad executable: " ^ Path.implode cmd) |
85 else error ("Bad executable: " ^ Path.implode cmd) |
84 val (proof, rc) = system_out (cmdline ^ " " ^ fname) |
86 val (proof, rc) = system_out (cmdline ^ " " ^ fname) |