src/HOL/Tools/res_atp.ML
changeset 17234 12a9393c5d77
parent 17231 f42bc4f7afdf
child 17235 8e55ad29b690
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Sep 02 17:23:59 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 02 17:55:24 2005 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  signature RES_ATP =
     1.5  sig
     1.6    val axiom_file : Path.T
     1.7 -  val hyps_file : Path.T
     1.8 -  val prob_file : Path.T;
     1.9  (*val atp_ax_tac : thm list -> int -> Tactical.tactic*)
    1.10  (*val atp_tac : int -> Tactical.tactic*)
    1.11    val full_spass: bool ref
    1.12 @@ -53,16 +51,10 @@
    1.13            REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.14       end);
    1.15  
    1.16 -(* temporarily use these files, which will be loaded by Vampire *)
    1.17 -val file_id_num = ref 0;
    1.18 -fun new_prob_file () = "prob" ^ string_of_int (inc file_id_num);
    1.19 -
    1.20  val axiom_file = File.tmp_path (Path.basic "axioms");
    1.21  val clasimp_file = File.tmp_path (Path.basic "clasimp");
    1.22  val hyps_file = File.tmp_path (Path.basic "hyps");
    1.23  val prob_file = File.tmp_path (Path.basic "prob");
    1.24 -val dummy_tac = all_tac;
    1.25 -val _ =debug  (File.platform_path prob_file);
    1.26  
    1.27  
    1.28  (**** for Isabelle/ML interface  ****)
    1.29 @@ -149,11 +141,11 @@
    1.30          val _ = debug ("about to write out dfg prob file " ^ probfile)
    1.31         	(*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
    1.32          val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)   
    1.33 -        val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
    1.34 +        val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
    1.35                          axclauses [] [] [] tfrees   
    1.36  	val out = TextIO.openOut(probfile)
    1.37      in
    1.38 -	(ResLib.writeln_strs out [filestr]; TextIO.closeOut out; debug probfile )
    1.39 +	(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
    1.40  (* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
    1.41      end;
    1.42  
    1.43 @@ -210,12 +202,12 @@
    1.44    in
    1.45      Watcher.callResProvers(childout,atp_list);
    1.46      debug "Sent commands to watcher!";
    1.47 -    dummy_tac
    1.48 +    all_tac
    1.49    end
    1.50  
    1.51  (**********************************************************)
    1.52  (* write out the current subgoal as a tptp file, probN,   *)
    1.53 -(* then call dummy_tac - should be call_res_tac           *)
    1.54 +(* then call all_tac - should be call_res_tac           *)
    1.55  (**********************************************************)
    1.56  
    1.57  
    1.58 @@ -223,7 +215,7 @@
    1.59      if n=0 then 
    1.60         (call_resolve_tac  (rev sko_thms)
    1.61          sign  sg_terms (childin, childout, pid) (List.length sg_terms);
    1.62 -        dummy_tac thm)
    1.63 +        all_tac thm)
    1.64       else
    1.65  	
    1.66       ( SELECT_GOAL
    1.67 @@ -234,7 +226,7 @@
    1.68               else tptp_inputs_tfrees (make_clauses negs) n tfrees;
    1.69               get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
    1.70                            thm  (n -1) (negs::sko_thms) axclauses; 
    1.71 -             dummy_tac))]) n thm )
    1.72 +             all_tac))]) n thm )
    1.73  
    1.74  
    1.75