src/HOL/Tools/res_atp.ML
changeset 24546 c90cee3163b7
parent 24425 ca97c6f3d9cd
child 24612 d1b315bdb8d7
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Sep 06 16:54:03 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Sep 06 17:03:32 2007 +0200
     1.3 @@ -834,7 +834,7 @@
     1.4  		  end
     1.5                | Recon.Vampire =>
     1.6  		  let val vampire = helper_path "VAMPIRE_HOME" "vampire"
     1.7 -		      val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
     1.8 +		      val vopts = "--output_syntax tptp%--mode casc%-t " ^ time
     1.9  		  in
    1.10  		      ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
    1.11  		  end
    1.12 @@ -861,7 +861,7 @@
    1.13    and allows the suppression of the suffix "_1" in problem-generation mode.
    1.14    FIXME: does not cope with &&, and it isn't easy because one could have multiple
    1.15    subgoals, each involving &&.*)
    1.16 -fun write_problem_files probfile (ctxt,th)  =
    1.17 +fun write_problem_files probfile (ctxt, chain_ths, th) =
    1.18    let val goals = Thm.prems_of th
    1.19        val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
    1.20        val thy = ProofContext.theory_of ctxt
    1.21 @@ -873,7 +873,7 @@
    1.22                  Auto => problem_logic_goals (map (map prop_of) goal_cls)
    1.23                | Fol => FOL
    1.24                | Hol => HOL
    1.25 -      val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
    1.26 +      val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
    1.27        val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
    1.28                                         |> restrict_to_logic thy logic
    1.29                                         |> remove_unwanted_clauses
    1.30 @@ -926,12 +926,12 @@
    1.31       handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed");
    1.32  
    1.33  (*writes out the current problems and calls ATPs*)
    1.34 -fun isar_atp (ctxt, th) =
    1.35 +fun isar_atp (ctxt, chain_ths, th) =
    1.36    if Thm.no_prems th then ()
    1.37    else
    1.38      let
    1.39        val _ = kill_last_watcher()
    1.40 -      val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th)
    1.41 +      val (files,thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, th)
    1.42        val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list)
    1.43      in
    1.44        last_watcher_pid := SOME (childin, childout, pid, files);
    1.45 @@ -944,31 +944,32 @@
    1.46  fun callatp () =
    1.47    let val th = topthm()
    1.48        val ctxt = ProofContext.init (theory_of_thm th)
    1.49 -  in  isar_atp (ctxt, th)  end;
    1.50 +  in  isar_atp (ctxt, [], th)  end;
    1.51  
    1.52  val isar_atp_writeonly = setmp print_mode []
    1.53 -      (fn (ctxt,th) =>
    1.54 +      (fn (ctxt, chain_ths, th) =>
    1.55         if Thm.no_prems th then ()
    1.56         else
    1.57           let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
    1.58                              else prob_pathname
    1.59 -         in ignore (write_problem_files probfile (ctxt,th)) end);
    1.60 +         in ignore (write_problem_files probfile (ctxt, chain_ths, th)) end);
    1.61  
    1.62  
    1.63  (** the Isar toplevel command **)
    1.64  
    1.65  fun sledgehammer state =
    1.66    let
    1.67 -    val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state);
    1.68 +    val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state);
    1.69      val thy = ProofContext.theory_of ctxt;
    1.70    in
    1.71      Output.debug (fn () => "subgoals in isar_atp:\n" ^
    1.72                    Pretty.string_of (ProofContext.pretty_term ctxt
    1.73                      (Logic.mk_conjunction_list (Thm.prems_of goal))));
    1.74      Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
    1.75 -    if !time_limit > 0 then isar_atp (ctxt, goal)
    1.76 +    app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
    1.77 +    if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
    1.78      else (warning ("Writing problem file only: " ^ !problem_name);
    1.79 -          isar_atp_writeonly (ctxt, goal))
    1.80 +          isar_atp_writeonly (ctxt, chain_ths, goal))
    1.81    end;
    1.82  
    1.83  val _ = OuterSyntax.add_parsers