Current version of res_atp.ML - causes an error when I run it. C.Q.
authorquigley
Tue Apr 05 16:32:47 2005 +0200 (2005-04-05 ago)
changeset 15657bd946fbc7c2b
parent 15656 988f91b9c4ef
child 15658 2edb384bf61f
Current version of res_atp.ML - causes an error when I run it. C.Q.
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Apr 05 13:05:38 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Apr 05 16:32:47 2005 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  val axiom_file : Path.T
     1.5  val hyps_file : Path.T
     1.6  val isar_atp : ProofContext.context * Thm.thm -> unit
     1.7 -(*val prob_file : Path.T*)
     1.8 +val prob_file : Path.T;
     1.9  (*val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic*)
    1.10  (*val atp_tac : int -> Tactical.tactic*)
    1.11  val debug: bool ref
    1.12 @@ -126,9 +126,13 @@
    1.13  (*********************************************************************)
    1.14  
    1.15  fun tptp_inputs_tfrees thms n tfrees = 
    1.16 -    let val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.17 +    let val _ = (warning ("in tptp_inputs_tfrees 0"))
    1.18 +        val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.19 +         val _ = (warning ("in tptp_inputs_tfrees 1"))
    1.20  	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
    1.21 +        val _ = (warning ("in tptp_inputs_tfrees 2"))
    1.22  	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
    1.23 +         val _ = (warning ("in tptp_inputs_tfrees 3"))
    1.24          val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    1.25  	val out = TextIO.openOut(probfile)
    1.26      in
    1.27 @@ -142,55 +146,56 @@
    1.28  (* should be modified to allow other provers to be called            *)
    1.29  (*********************************************************************)
    1.30  
    1.31 -fun call_resolve_tac thms sg_term (childin, childout,pid)  = let
    1.32 -                            val newprobfile = new_prob_file ()
    1.33 +fun call_resolve_tac thms sg_term (childin, childout,pid) n  = let
    1.34                               val thmstring = concat_with_and (map string_of_thm thms) ""
    1.35 -                            val thm_no = length thms
    1.36 -                            val _ = warning ("number of thms is : "^(string_of_int thm_no))
    1.37 -                           val _ = warning ("thmstring in call_res is: "^thmstring)
    1.38 -                            val goalstr = Sign.string_of_term Mainsign sg_term 
    1.39 -                            val goalproofstring = proofstring goalstr
    1.40 -                               val no_returns =List.filter not_newline ( goalproofstring)
    1.41 -                            val goalstring = implode no_returns
    1.42 -                            val _ = warning ("goalstring in call_res is: "^goalstring)
    1.43 +                             val thm_no = length thms
    1.44 +                             val _ = warning ("number of thms is : "^(string_of_int thm_no))
    1.45 +                             val _ = warning ("thmstring in call_res is: "^thmstring)
    1.46 +
    1.47 +                             val goalstr = Sign.string_of_term Mainsign sg_term 
    1.48 +                             val goalproofstring = proofstring goalstr
    1.49 +                             val no_returns =List.filter not_newline ( goalproofstring)
    1.50 +                             val goalstring = implode no_returns
    1.51 +                             val _ = warning ("goalstring in call_res is: "^goalstring)
    1.52          
    1.53 -                            val prob_file =File.tmp_path (Path.basic newprobfile); 
    1.54 +                             (*val prob_file =File.tmp_path (Path.basic newprobfile); *)
    1.55                               (*val _ =( warning ("calling make_clauses "))
    1.56                               val clauses = make_clauses thms
    1.57                               val _ =( warning ("called make_clauses "))*)
    1.58 -                            (*val _ = tptp_inputs clauses prob_file*)
    1.59 -                            val thmstring = concat_with_and (map string_of_thm thms) ""
    1.60 +                             (*val _ = tptp_inputs clauses prob_file*)
    1.61 +                             val thmstring = concat_with_and (map string_of_thm thms) ""
    1.62                             
    1.63 -                            val goalstr = Sign.string_of_term Mainsign sg_term 
    1.64 -                            val goalproofstring = proofstring goalstr
    1.65 +                             val goalstr = Sign.string_of_term Mainsign sg_term 
    1.66 +                             val goalproofstring = proofstring goalstr
    1.67                               val no_returns =List.filter not_newline ( goalproofstring)
    1.68 -                            val goalstring = implode no_returns
    1.69 +                             val goalstring = implode no_returns
    1.70  
    1.71 -                            val thmproofstring = proofstring ( thmstring)
    1.72 -                            val no_returns =List.filter   not_newline ( thmproofstring)
    1.73 -                            val thmstr = implode no_returns
    1.74 +                             val thmproofstring = proofstring ( thmstring)
    1.75 +                             val no_returns =List.filter   not_newline ( thmproofstring)
    1.76 +                             val thmstr = implode no_returns
    1.77                              
    1.78 -                            val prob_path = File.sysify_path prob_file
    1.79 -                            val outfile = TextIO.openOut("/home/clq20/Jia_Code/hellofile")
    1.80 -                            val _ = TextIO.output(outfile, "prob file path is "^prob_path^" thmstring is "^thmstr^" goalstring is "^goalstring);
    1.81 -                            val _ = TextIO.flushOut outfile;
    1.82 -                            val _ =  TextIO.closeOut outfile
    1.83 +                             val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    1.84 +                             val outfile = TextIO.openOut("/home/clq20/Jia_Code/hellofile")
    1.85 +                             val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
    1.86 +                             val _ = TextIO.flushOut outfile;
    1.87 +                             val _ =  TextIO.closeOut outfile
    1.88                            in
    1.89                             (* without paramodulation *)
    1.90 -                           (*(warning ("goalstring in call_res_tac is: "^goalstring));
    1.91 -                           (warning ("prob path in cal_res_tac is: "^prob_path));
    1.92 +                           (warning ("goalstring in call_res_tac is: "^goalstring));
    1.93 +                           (warning ("prob file in cal_res_tac is: "^probfile));
    1.94                              Watcher.callResProvers(childout,
    1.95                              [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",  
    1.96                               "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
    1.97 -                             prob_path)]);*)
    1.98 +                             probfile)]);
    1.99 +
   1.100                             (* with paramodulation *)
   1.101                             (*Watcher.callResProvers(childout,
   1.102                                    [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",
   1.103                                    "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", 
   1.104                                      prob_path)]); *)
   1.105 -                           Watcher.callResProvers(childout,
   1.106 +                          (* Watcher.callResProvers(childout,
   1.107                             [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", 
   1.108 -                           "-DocProof",  prob_path)]);
   1.109 +                           "-DocProof",  prob_path)]);*)
   1.110                             dummy_tac
   1.111                           end
   1.112  
   1.113 @@ -199,7 +204,7 @@
   1.114  (* process subgoal into skolemized, negated form*)
   1.115  (* then call call_resolve_tac to send to ATP    *)
   1.116  (************************************************)
   1.117 -
   1.118 +(*
   1.119  fun resolve_tac sg_term  (childin, childout,pid) = 
   1.120     let val _ = warning ("in resolve_tac ")
   1.121     in
   1.122 @@ -207,7 +212,7 @@
   1.123    (EVERY1 [rtac ccontr,atomize_tac,skolemize_tac,  METAHYPS(fn negs => (warning ("calling call_resolve_tac next ");dummy_tac (*call_resolve_tac negs sg_term (childin, childout,pid)*)))])
   1.124     end;
   1.125  
   1.126 -
   1.127 +*)
   1.128  
   1.129  
   1.130  (* Need to replace call_atp_tac_tfrees with call res_provers as it's the dummy one *)
   1.131 @@ -219,16 +224,18 @@
   1.132  (* should call call_res_tac here, not resolve_tac *)
   1.133  (* 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 *)
   1.134  fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = 
   1.135 -                                         ((*tptp_inputs_tfrees (make_clauses thms) n tfrees;*)
   1.136 -                                          call_resolve_tac thms sg_term (childin, childout, pid);
   1.137 +
   1.138 +                                         ( (warning("in call_atp_tac_tfrees"));
   1.139 +                                           tptp_inputs_tfrees (make_clauses thms) n tfrees;
   1.140 +                                          call_resolve_tac thms sg_term (childin, childout, pid) n;
   1.141    					  dummy_tac);
   1.142  
   1.143  fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
   1.144  let val _ = (warning ("in atp_tac_tfrees "))
   1.145     in
   1.146  SELECT_GOAL
   1.147 -  (EVERY1 [rtac ccontr,atomize_tac, (*skolemize_tac, *)
   1.148 -  METAHYPS(fn negs => (call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
   1.149 +  (EVERY1 [rtac ccontr,atomize_tac,(*skolemize_tac, *)
   1.150 +  METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees"));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
   1.151  end;
   1.152  
   1.153  
   1.154 @@ -292,7 +299,7 @@
   1.155          (* val _ = write_out_clasimp (File.sysify_path axiom_file)*)
   1.156          (* cq: add write out clasimps to file *)
   1.157          (* cq:create watcher and pass to isar_atp_aux *)                    
   1.158 -        val (childin,childout,pid) = Watcher.createWatcher(thm)
   1.159 +        val (childin,childout,pid) = Watcher.createWatcher()
   1.160          val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
   1.161      in
   1.162  	case prems of [] => ()