src/HOL/Tools/atp_wrapper.ML
changeset 31750 f28b7365fabf
parent 31411 1d00ab68bc8d
child 31751 fda2cf4fef58
equal deleted inserted replaced
31749:8ee34e3ceb5a 31750:f28b7365fabf
    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)