*** empty log message ***
authorquigley
Thu Mar 31 20:12:54 2005 +0200 (2005-03-31 ago)
changeset 15644f2ef8c258fa4
parent 15643 5829f30fc20a
child 15645 5e20c54683d3
*** empty log message ***
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Mar 31 19:47:30 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Mar 31 20:12:54 2005 +0200
     1.3 @@ -6,17 +6,17 @@
     1.4  *)
     1.5  
     1.6  (*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
     1.7 +(*Claire: changed: added actual watcher calls *)
     1.8  
     1.9  signature RES_ATP = 
    1.10  sig
    1.11 -
    1.12  val trace_res : bool ref
    1.13  val axiom_file : Path.T
    1.14  val hyps_file : Path.T
    1.15  val isar_atp : ProofContext.context * Thm.thm -> unit
    1.16 -val prob_file : Path.T
    1.17 -val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
    1.18 -val atp_tac : int -> Tactical.tactic
    1.19 +(*val prob_file : Path.T*)
    1.20 +(*val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic*)
    1.21 +(*val atp_tac : int -> Tactical.tactic*)
    1.22  val debug: bool ref
    1.23  
    1.24  end;
    1.25 @@ -25,6 +25,8 @@
    1.26  
    1.27  struct
    1.28  
    1.29 +
    1.30 +
    1.31  (* used for debug *)
    1.32  val debug = ref false;
    1.33  
    1.34 @@ -35,6 +37,9 @@
    1.35  
    1.36  val skolem_tac = skolemize_tac;
    1.37  
    1.38 +val num_of_clauses = ref 0;
    1.39 +val clause_arr = Array.array(3500, ("empty", 0));
    1.40 +
    1.41  
    1.42  val atomize_tac =
    1.43      SUBGOAL
    1.44 @@ -47,52 +52,39 @@
    1.45       end);
    1.46  
    1.47  (* temporarily use these files, which will be loaded by Vampire *)
    1.48 -val prob_file = File.tmp_path (Path.basic "prob");
    1.49 -val axiom_file = File.tmp_path (Path.basic "axioms");
    1.50 -val hyps_file = File.tmp_path (Path.basic "hyps");
    1.51 -val dummy_tac = PRIMITIVE(fn thm => thm );
    1.52 +val file_id_num =ref 0;
    1.53  
    1.54 +fun new_prob_file () =  (file_id_num := (!file_id_num) + 1;"prob"^(string_of_int (!file_id_num)));
    1.55  
    1.56  
    1.57 -fun tptp_inputs thms n = 
    1.58 -    let val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.59 -	val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss) 
    1.60 -        val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    1.61 -	val out = TextIO.openOut(probfile)
    1.62 -    in
    1.63 -	(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
    1.64 -    end;
    1.65 +val axiom_file = File.tmp_path (Path.basic "axioms");
    1.66 +val clasimp_file = File.tmp_path (Path.basic "clasimp");
    1.67 +val hyps_file = File.tmp_path (Path.basic "hyps");
    1.68 +val prob_file = File.tmp_path (Path.basic "prob");
    1.69 +val dummy_tac = PRIMITIVE(fn thm => thm );
    1.70 +
    1.71 + 
    1.72 +fun concat_with_and [] str = str
    1.73 +|   concat_with_and (x::[]) str = str^" ("^x^")"
    1.74 +|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
    1.75 +
    1.76  
    1.77  
    1.78  (**** for Isabelle/ML interface  ****)
    1.79  
    1.80 -fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);
    1.81 +fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
    1.82  
    1.83 +fun proofstring x = let val exp = explode x 
    1.84 +                    in
    1.85 +                        List.filter (is_proof_char ) exp
    1.86 +                    end
    1.87  
    1.88  
    1.89  
    1.90 -fun atp_tac n = SELECT_GOAL
    1.91 -  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.92 -  METAHYPS(fn negs => (call_atp_tac (make_clauses negs) n))]) n ;
    1.93 -
    1.94 +(*
    1.95 +fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac);
    1.96  
    1.97 -fun atp_ax_tac axioms n = 
    1.98 -    let val axcls = ResLib.flat_noDup(map ResAxioms.clausify_axiom axioms)
    1.99 -	val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup(map ResClause.tptp_clause axcls))
   1.100 -	val axiomfile = File.sysify_path axiom_file
   1.101 -	val out = TextIO.openOut (axiomfile)
   1.102 -    in
   1.103 -	(TextIO.output(out,axcls_str);TextIO.closeOut out; if !trace_res then (warning axiomfile) else (); atp_tac n)
   1.104 -    end;
   1.105 -
   1.106 -
   1.107 -fun atp thm =
   1.108 -    let val prems = prems_of thm
   1.109 -    in
   1.110 -	case prems of [] => () 
   1.111 -		    | _ => (atp_tac 1 thm; ())
   1.112 -    end;
   1.113 -
   1.114 +*)
   1.115  
   1.116  (**** For running in Isar ****)
   1.117  
   1.118 @@ -106,14 +98,18 @@
   1.119  (* a special version of repeat_RS *)
   1.120  fun repeat_someI_ex thm = repeat_RS thm someI_ex;
   1.121  
   1.122 -
   1.123 +(*********************************************************************)
   1.124  (* convert clauses from "assume" to conjecture. write to file "hyps" *)
   1.125 +(* hypotheses of the goal currently being proved                     *)
   1.126 +(*********************************************************************)
   1.127 +
   1.128  fun isar_atp_h thms =
   1.129 +        
   1.130      let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
   1.131 -	val prems' = map repeat_someI_ex prems
   1.132 -	val prems'' = make_clauses prems'
   1.133 -	val prems''' = ResAxioms.rm_Eps [] prems''
   1.134 -	val clss = map ResClause.make_conjecture_clause prems'''
   1.135 +        val prems' = map repeat_someI_ex prems
   1.136 +        val prems'' = make_clauses prems'
   1.137 +        val prems''' = ResAxioms.rm_Eps [] prems''
   1.138 +        val clss = map ResClause.make_conjecture_clause prems'''
   1.139  	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss) 
   1.140  	val tfree_lits = ResLib.flat_noDup tfree_litss
   1.141  	val tfree_clss = map ResClause.tfree_clause tfree_lits 
   1.142 @@ -123,6 +119,12 @@
   1.143  	((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) 
   1.144      end;
   1.145  
   1.146 +
   1.147 +(*********************************************************************)
   1.148 +(* write out a subgoal as tptp clauses to the file "probN"           *)
   1.149 +(* where N is the number of this subgoal                             *)
   1.150 +(*********************************************************************)
   1.151 +
   1.152  fun tptp_inputs_tfrees thms n tfrees = 
   1.153      let val clss = map (ResClause.make_conjecture_clause_thm) thms
   1.154  	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
   1.155 @@ -134,36 +136,168 @@
   1.156      end;
   1.157  
   1.158  
   1.159 -fun call_atp_tac_tfrees thms n tfrees = (tptp_inputs_tfrees thms n tfrees; dummy_tac);
   1.160  
   1.161 +(*********************************************************************)
   1.162 +(* call SPASS with settings and problem file for the current subgoal *)
   1.163 +(* should be modified to allow other provers to be called            *)
   1.164 +(*********************************************************************)
   1.165  
   1.166 -fun atp_tac_tfrees tfrees n  = SELECT_GOAL
   1.167 -  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
   1.168 -  METAHYPS(fn negs => (call_atp_tac_tfrees (make_clauses negs) n tfrees))]) n;
   1.169 -
   1.170 +fun call_resolve_tac thms sg_term (childin, childout,pid)  = let
   1.171 +                            val newprobfile = new_prob_file ()
   1.172 +                             val thmstring = concat_with_and (map string_of_thm thms) ""
   1.173 +                           val _ = warning ("thmstring in call_res is: "^thmstring)
   1.174 +                            val goalstr = Sign.string_of_term Mainsign sg_term 
   1.175 +                            val goalproofstring = proofstring goalstr
   1.176 +                               val no_returns =List.filter not_newline ( goalproofstring)
   1.177 +                            val goalstring = implode no_returns
   1.178 +                            val _ = warning ("goalstring in call_res is: "^goalstring)
   1.179 +        
   1.180 +                            val prob_file =File.tmp_path (Path.basic newprobfile); 
   1.181 +                             val clauses = make_clauses thms
   1.182 +                            (*val _ = tptp_inputs clauses prob_file*)
   1.183 +                            val thmstring = concat_with_and (map string_of_thm thms) ""
   1.184 +                           
   1.185 +                            val goalstr = Sign.string_of_term Mainsign sg_term 
   1.186 +                            val goalproofstring = proofstring goalstr
   1.187 +                             val no_returns =List.filter not_newline ( goalproofstring)
   1.188 +                            val goalstring = implode no_returns
   1.189  
   1.190 -fun isar_atp_g tfrees = atp_tac_tfrees tfrees;
   1.191 +                            val thmproofstring = proofstring ( thmstring)
   1.192 +                            val no_returns =List.filter   not_newline ( thmproofstring)
   1.193 +                            val thmstr = implode no_returns
   1.194 +                            
   1.195 +                            val prob_path = File.sysify_path prob_file
   1.196 +                            val outfile = TextIO.openOut("/home/clq20/Jia_Code/hellofile")
   1.197 +                            val _ = TextIO.output(outfile, "prob file path is "^prob_path^" thmstring is "^thmstr^" goalstring is "^goalstring);
   1.198 +                            val _ = TextIO.flushOut outfile;
   1.199 +                            val _ =  TextIO.closeOut outfile
   1.200 +                          in
   1.201 +                           (* without paramodulation *)
   1.202 +                           (*(warning ("goalstring in call_res_tac is: "^goalstring));
   1.203 +                           (warning ("prob path in cal_res_tac is: "^prob_path));
   1.204 +                            Watcher.callResProvers(childout,
   1.205 +                            [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",  
   1.206 +                             "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
   1.207 +                             prob_path)]);*)
   1.208 +                           (* with paramodulation *)
   1.209 +                           (*Watcher.callResProvers(childout,
   1.210 +                                  [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",
   1.211 +                                  "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", 
   1.212 +                                    prob_path)]); *)
   1.213 +                           Watcher.callResProvers(childout,
   1.214 +                           [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", 
   1.215 +                           "-DocProof",  prob_path)]);
   1.216 +                           dummy_tac
   1.217 +                         end
   1.218  
   1.219 -fun isar_atp_goal' thm k n tfree_lits = 
   1.220 -    if (k > n) then () else (isar_atp_g tfree_lits k thm; isar_atp_goal' thm (k+1) n tfree_lits);
   1.221 +(************************************************)
   1.222 +(* pass in subgoal as a term and watcher info   *)
   1.223 +(* process subgoal into skolemized, negated form*)
   1.224 +(* then call call_resolve_tac to send to ATP    *)
   1.225 +(************************************************)
   1.226  
   1.227 +fun resolve_tac sg_term  (childin, childout,pid) = 
   1.228 +   let val _ = warning ("in resolve_tac ")
   1.229 +   in
   1.230 +   SELECT_GOAL
   1.231 +  (EVERY1 [rtac ccontr,atomize_tac,skolemize_tac,  METAHYPS(fn negs => (warning ("calling call_resolve_tac next ");call_resolve_tac negs sg_term (childin, childout,pid)))])
   1.232 +   end;
   1.233  
   1.234 -fun isar_atp_goal thm n_subgoals tfree_lits = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals tfree_lits));
   1.235  
   1.236  
   1.237  
   1.238 -fun isar_atp_aux thms thm n_subgoals = 
   1.239 +(* Need to replace call_atp_tac_tfrees with call res_provers as it's the dummy one *)
   1.240 +
   1.241 +(**********************************************************)
   1.242 +(* write out the current subgoal as a tptp file, probN,   *)
   1.243 +(* then call dummy_tac - should be call_res_tac           *)
   1.244 +(**********************************************************)
   1.245 +
   1.246 +fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = 
   1.247 +                                         (tptp_inputs_tfrees (make_clauses thms) n tfrees; 
   1.248 +                                          resolve_tac sg_term (childin, childout, pid);
   1.249 +  					  dummy_tac);
   1.250 +
   1.251 +fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
   1.252 +let val _ = (warning ("in atp_tac_tfrees "))
   1.253 +   in
   1.254 +SELECT_GOAL
   1.255 +  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
   1.256 +  METAHYPS(fn negs => (call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid)))]) n
   1.257 +end;
   1.258 +
   1.259 +
   1.260 +fun isar_atp_g tfrees sg_term (childin, childout, pid)  = 
   1.261 +                                        
   1.262 +(	(warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid));
   1.263 +
   1.264 +
   1.265 +
   1.266 +(**********************************************)
   1.267 +(* recursively call atp_tac_g on all subgoals *)
   1.268 +(* sg_term is the nth subgoal as a term - used*)
   1.269 +(* in proof reconstruction                    *)
   1.270 +(**********************************************)
   1.271 +
   1.272 +fun isar_atp_goal' thm k n tfree_lits  (childin, childout, pid) = 
   1.273 +                  	if (k > n) 
   1.274 +                        then () 
   1.275 +	  		else 
   1.276 +                           (let val  prems = prems_of thm 
   1.277 +                                val sg_term = get_nth n prems
   1.278 +                            in   
   1.279 +                                 
   1.280 +                		(warning("in isar_atp_goal'"));
   1.281 + 				 isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
   1.282 +                                 isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
   1.283 +                            end);
   1.284 +
   1.285 +
   1.286 +fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals tfree_lits  (childin, childout, pid) ));
   1.287 +
   1.288 +(**************************************************)
   1.289 +(* convert clauses from "assume" to conjecture.   *)
   1.290 +(* i.e. apply make_clauses and then get tptp for  *)
   1.291 +(* any hypotheses in the goal                     *)
   1.292 +(* write to file "hyps"                           *)
   1.293 +(**************************************************)
   1.294 +
   1.295 +
   1.296 +fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
   1.297      let val tfree_lits = isar_atp_h thms 
   1.298      in
   1.299 -	isar_atp_goal thm n_subgoals tfree_lits
   1.300 +	(warning("in isar_atp_aux"));isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid)
   1.301      end;
   1.302 -   
   1.303 +
   1.304 +(******************************************************************)
   1.305 +(* called in Isar automatically                                   *)
   1.306 +(* writes out the current clasimpset to a tptp file               *)
   1.307 +(* passes all subgoals on to isar_atp_aux for further processing  *)
   1.308 +(* turns off xsymbol at start of function, restoring it at end    *)
   1.309 +(******************************************************************)
   1.310  
   1.311  fun isar_atp' (thms, thm) =
   1.312 -    let val prems = prems_of thm
   1.313 +    let val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   1.314 +        val _= (warning ("in isar_atp'"))
   1.315 +        val prems = prems_of thm
   1.316 +        val thms_string =concat_with_and (map  string_of_thm thms) ""
   1.317 +        val thmstring = string_of_thm thm
   1.318 +        val prems_string = concat_with_and (map (Sign.string_of_term Mainsign) prems) ""
   1.319 +        (* set up variables for writing out the clasimps to a tptp file *)
   1.320 +        (* val _ = write_out_clasimp (File.sysify_path axiom_file)*)
   1.321 +        (* cq: add write out clasimps to file *)
   1.322 +        (* cq:create watcher and pass to isar_atp_aux *)                    
   1.323 +        val (childin,childout,pid) = Watcher.createWatcher(thm)
   1.324 +        val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
   1.325      in
   1.326 -	case prems of [] => (if (!debug) then warning "entering forward, no goal" else ())
   1.327 -		    | _ => (isar_atp_aux thms thm (length prems))
   1.328 +	case prems of [] => () 
   1.329 +		    | _ => ((warning ("initial thms: "^thms_string)); 
   1.330 +                           (warning ("initial thm: "^thmstring));
   1.331 +                           (warning ("subgoals: "^prems_string));
   1.332 +                           (warning ("pid: "^ pidstring))); 
   1.333 +                            isar_atp_aux thms thm (length prems) (childin, childout, pid) ;
   1.334 +                           
   1.335 +                           print_mode := (["xsymbols", "symbols"] @ ! print_mode)
   1.336      end;
   1.337  
   1.338  
   1.339 @@ -210,6 +344,9 @@
   1.340  
   1.341  (* convert locally declared rules to axiom clauses *)
   1.342  (* write axiom clauses to ax_file *)
   1.343 +(* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
   1.344 +(* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
   1.345 +(*claset file and prob file*)
   1.346  fun isar_local_thms (delta_cs, delta_ss_thms) =
   1.347      let val thms_cs = get_thms_cs delta_cs
   1.348  	val thms_ss = get_thms_ss delta_ss_thms
   1.349 @@ -218,7 +355,7 @@
   1.350  	val ax_file = File.sysify_path axiom_file
   1.351  	val out = TextIO.openOut ax_file
   1.352      in
   1.353 -	(ResLib.writeln_strs out clauses_strs; TextIO.closeOut out)
   1.354 +	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
   1.355      end;
   1.356  
   1.357  
   1.358 @@ -228,10 +365,18 @@
   1.359  (* called in Isar automatically *)
   1.360  fun isar_atp (ctxt,thm) =
   1.361      let val prems = ProofContext.prems_of ctxt
   1.362 -      val d_cs = Classical.get_delta_claset ctxt
   1.363 -      val d_ss_thms = Simplifier.get_delta_simpset ctxt
   1.364 +        val d_cs = Classical.get_delta_claset ctxt 
   1.365 +        val d_ss_thms = Simplifier.get_delta_simpset ctxt
   1.366 +        val thmstring = string_of_thm thm
   1.367 +        val prem_no = length prems
   1.368 +        val prems_string = concat_with_and (map string_of_thm prems) ""
   1.369      in
   1.370 -	(isar_local_thms (d_cs,d_ss_thms); isar_atp' (prems, thm))
   1.371 +         
   1.372 +          (warning ("initial thm in isar_atp: "^thmstring));
   1.373 +          (warning ("subgoals in isar_atp: "^prems_string));
   1.374 +    	   (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   1.375 +          (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'"));
   1.376 +           isar_atp' (prems, thm))
   1.377      end;
   1.378  
   1.379  end
   1.380 @@ -242,5 +387,3 @@
   1.381  end;
   1.382  
   1.383  Proof.atp_hook := ResAtp.isar_atp;
   1.384 -
   1.385 -
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Mar 31 19:47:30 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 31 20:12:54 2005 +0200
     2.3 @@ -458,7 +458,27 @@
     2.4  	clausify_simpset_rules thms []
     2.5      end;
     2.6  
     2.7 +(* lcp-modified code *)
     2.8 +(*
     2.9 +fun retr_thms ([]:MetaSimplifier.rrule list) = []
    2.10 +	  | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
    2.11 +
    2.12 +fun snds [] = []
    2.13 +   | snds ((x,y)::l) = y::(snds l);
    2.14 +
    2.15 +fun simpset_rules_of_thy thy =
    2.16 +     let val simpset = simpset_of thy
    2.17 +	val rules = #rules(fst (rep_ss simpset))
    2.18 +	val thms = retr_thms (snds(Net.dest rules))
    2.19 +     in	thms  end;
    2.20 +
    2.21 +print_depth 200;
    2.22 +simpset_rules_of_thy Main.thy;
    2.23  
    2.24  
    2.25  
    2.26 +
    2.27 +
    2.28 +*)
    2.29 +
    2.30  end;