Integrating the reconstruction files into the building of HOL

--- a/src/HOL/Tools/meson.ML	Thu Apr 07 17:45:51 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Apr 07 18:20:04 2005 +0200
@@ -86,6 +86,13 @@
 	| has _ = false
   in  has  end;
 
+(* for tracing statements *)
+ 
+fun concat_with_and [] str = str
+|   concat_with_and (x::[]) str = str^" ("^x^")"
+|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
+
+
 
 (**** Clause handling ****)
 
@@ -124,7 +131,7 @@
 (*Conjunctive normal form, detecting tautologies early.
   Strips universal quantifiers and breaks up conjunctions. *)
 fun cnf_aux seen (th,ths) =
- let val _= (warning ("in cnf_aux"))
+ let val _= (warning ("in cnf_aux, th : "^(string_of_thm th)))
  in if taut_lits (literals(prop_of th) @ seen)  
   then ths     (*tautology ignored*)
   else if not (has_consts ["All","op &"] (prop_of th))  
@@ -310,8 +317,8 @@
 (*Pull existential quantifiers (Skolemization)*)
 fun skolemize th =
   if not (has_consts ["Ex"] (prop_of th)) then th
-  else skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
-                              disj_exD, disj_exD1, disj_exD2]))
+  else ((warning("in meson.skolemize with th: "^(string_of_thm th)));skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
+                              disj_exD, disj_exD1, disj_exD2])))
     handle THM _ =>
         skolemize (forward_res skolemize
                    (tryres (th, [conj_forward, disj_forward, all_forward])))
@@ -321,7 +328,7 @@
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
 fun make_clauses ths =
-    sort_clauses (map (generalize o nodups) (foldr cnf [] ths));
+   ( (warning("in make_clauses ths are:"^(concat_with_and (map string_of_thm ths) ""))); sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
 
 (*Convert a list of clauses to (contrapositive) Horn clauses*)
 fun make_horns ths =
@@ -448,9 +455,14 @@
   SUBGOAL
     (fn (prop,_) =>
      let val ts = Logic.strip_assums_hyp prop
+         val _ = (warning("in meson.skolemize_tac "))
+         val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "skolem")))
+         val _ = TextIO.output(outfile, "in skolemize_tac ");
+         val _ = TextIO.flushOut outfile;
+         val _ =  TextIO.closeOut outfile
      in EVERY1 
 	 [METAHYPS
-	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
+	    (fn hyps => ((warning("in meson.skolemize_tac hyps are: "^(string_of_thm (hd hyps))));cut_facts_tac (map (skolemize o make_nnf) hyps) 1
                          THEN REPEAT (etac exE 1))),
 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
      end);

--- a/src/HOL/Tools/res_atp.ML	Thu Apr 07 17:45:51 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Apr 07 18:20:04 2005 +0200
@@ -8,6 +8,8 @@
 (*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
 (*Claire: changed: added actual watcher calls *)
 
+val traceflag = ref true;
+
 signature RES_ATP = 
 sig
 val trace_res : bool ref
@@ -175,7 +177,7 @@
                              val thmstr = implode no_returns
                             
                              val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
-                             val outfile = TextIO.openOut("/home/clq20/Jia_Code/hellofile")
+                             val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile")))
                              val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
                              val _ = TextIO.flushOut outfile;
                              val _ =  TextIO.closeOut outfile
@@ -223,25 +225,45 @@
 (**********************************************************)
 (* should call call_res_tac here, not resolve_tac *)
 (* if we take tptpinputs out it gets into call_res_tac then falls over as usual after printing out goalstring. but if we leave it in it falls over here *)
-fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = 
+
+(* dummy tac vs.  Doesn't call resolve_tac *)
 
-                                         ( (warning("in call_atp_tac_tfrees"));
+fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = 
+                                         ( (warning("ths for tptp: "^(concat_with_and (map string_of_thm thms) "")));
+                                           (warning("in call_atp_tac_tfrees"));
+                                           
                                            tptp_inputs_tfrees (make_clauses thms) n tfrees;
-                                          call_resolve_tac thms sg_term (childin, childout, pid) n;
-  					  dummy_tac);
+                                           call_resolve_tac thms sg_term (childin, childout, pid) n;
+  					   dummy_tac);
 
+
+(*
 fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
 let val _ = (warning ("in atp_tac_tfrees "))
    in
-SELECT_GOAL
-  (EVERY1 [rtac ccontr,atomize_tac,(*skolemize_tac, *)
-  METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees"));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
+SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac,(*skolemize_tac,*) METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) "")));(*make_clauses negs;*)dummy_tac)) ])1
 end;
 
 
-fun isar_atp_g tfrees sg_term (childin, childout, pid)  = 
+
+METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) ""))));make_clauses negs;dummy_tac)) 1;
+*)
+
+
+fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
+let val _ = (warning ("in atp_tac_tfrees "))
+    val _ = (warning ("sg_term :"^((Sign.string_of_term Mainsign) sg_term)))
+   
+   in
+SELECT_GOAL
+  (EVERY1 [rtac ccontr,atomize_tac, tracify traceflag skolemize_tac, 
+  METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) "")));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
+end;
+
+
+fun isar_atp_g tfrees sg_term (childin, childout, pid) n = 
                                         
-(	(warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid));
+((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
 
 
 
@@ -257,9 +279,11 @@
 	  		else 
                            (let val  prems = prems_of thm 
                                 val sg_term = get_nth n prems
+                                val thmstring = string_of_thm thm
                             in   
                                  
                 		(warning("in isar_atp_goal'"));
+                                (warning("thmstring in isar_atp_goal: "^thmstring));
  				 isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
                                  isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
                             end);
@@ -270,7 +294,8 @@
 (**************************************************)
 (* convert clauses from "assume" to conjecture.   *)
 (* i.e. apply make_clauses and then get tptp for  *)
-(* any hypotheses in the goal                     *)
+(* any hypotheses in the goal produced by assume  *)
+(* statements;                                    *)
 (* write to file "hyps"                           *)
 (**************************************************)
 
@@ -375,13 +400,15 @@
 
 
 (* called in Isar automatically *)
+
 fun isar_atp (ctxt,thm) =
     let val prems = ProofContext.prems_of ctxt
         val d_cs = Classical.get_delta_claset ctxt 
         val d_ss_thms = Simplifier.get_delta_simpset ctxt
         val thmstring = string_of_thm thm
-        val prem_no = length prems
-        val prems_string = concat_with_and (map string_of_thm prems) ""
+        val sg_prems = prems_of thm
+        val prem_no = length sg_prems
+        val prems_string =  concat_with_and (map (Sign.string_of_term Mainsign) sg_prems) ""
     in
          
           (warning ("initial thm in isar_atp: "^thmstring));