src/HOL/Tools/res_atp.ML
author paulson
Thu Apr 07 18:44:45 2005 +0200 (2005-04-07)
changeset 15682 09a7b8909c4d
parent 15679 28eb0fe50533
child 15697 681bcb7f0389
permissions -rw-r--r--
removed bad code
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 ATPs with TPTP format input.
     6 *)
     7 
     8 (*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
     9 (*Claire: changed: added actual watcher calls *)
    10 
    11 signature RES_ATP = 
    12 sig
    13 val trace_res : bool ref
    14 val axiom_file : Path.T
    15 val hyps_file : Path.T
    16 val isar_atp : ProofContext.context * Thm.thm -> unit
    17 val prob_file : Path.T;
    18 (*val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic*)
    19 (*val atp_tac : int -> Tactical.tactic*)
    20 val debug: bool ref
    21 
    22 end;
    23 
    24 structure ResAtp : RES_ATP =
    25 
    26 struct
    27 
    28 
    29 
    30 (* used for debug *)
    31 val debug = ref false;
    32 
    33 fun debug_tac tac = (warning "testing";tac);
    34 (* default value is false *)
    35 
    36 val trace_res = ref false;
    37 
    38 val skolem_tac = skolemize_tac;
    39 
    40 val num_of_clauses = ref 0;
    41 val clause_arr = Array.array(3500, ("empty", 0));
    42 
    43 
    44 val atomize_tac =
    45     SUBGOAL
    46      (fn (prop,_) =>
    47 	 let val ts = Logic.strip_assums_hyp prop
    48 	 in EVERY1 
    49 		[METAHYPS
    50 		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
    51 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    52      end);
    53 
    54 (* temporarily use these files, which will be loaded by Vampire *)
    55 val file_id_num =ref 0;
    56 
    57 fun new_prob_file () =  (file_id_num := (!file_id_num) + 1;"prob"^(string_of_int (!file_id_num)));
    58 
    59 
    60 val axiom_file = File.tmp_path (Path.basic "axioms");
    61 val clasimp_file = File.tmp_path (Path.basic "clasimp");
    62 val hyps_file = File.tmp_path (Path.basic "hyps");
    63 val prob_file = File.tmp_path (Path.basic "prob");
    64 val dummy_tac = PRIMITIVE(fn thm => thm );
    65 
    66  
    67 fun concat_with_and [] str = str
    68 |   concat_with_and (x::[]) str = str^" ("^x^")"
    69 |   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
    70 
    71 
    72 
    73 (**** for Isabelle/ML interface  ****)
    74 
    75 fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
    76 
    77 fun proofstring x = let val exp = explode x 
    78                     in
    79                         List.filter (is_proof_char ) exp
    80                     end
    81 
    82 
    83 
    84 (*
    85 fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac);
    86 
    87 *)
    88 
    89 (**** For running in Isar ****)
    90 
    91 (* same function as that in res_axioms.ML *)
    92 fun repeat_RS thm1 thm2 =
    93     let val thm1' =  thm1 RS thm2 handle THM _ => thm1
    94     in
    95 	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
    96     end;
    97 
    98 (* a special version of repeat_RS *)
    99 fun repeat_someI_ex thm = repeat_RS thm someI_ex;
   100 
   101 (*********************************************************************)
   102 (* convert clauses from "assume" to conjecture. write to file "hyps" *)
   103 (* hypotheses of the goal currently being proved                     *)
   104 (*********************************************************************)
   105 
   106 fun isar_atp_h thms =
   107         
   108     let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
   109         val prems' = map repeat_someI_ex prems
   110         val prems'' = make_clauses prems'
   111         val prems''' = ResAxioms.rm_Eps [] prems''
   112         val clss = map ResClause.make_conjecture_clause prems'''
   113 	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss) 
   114 	val tfree_lits = ResLib.flat_noDup tfree_litss
   115 	val tfree_clss = map ResClause.tfree_clause tfree_lits 
   116         val hypsfile = File.sysify_path hyps_file
   117 	val out = TextIO.openOut(hypsfile)
   118     in
   119 	((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) 
   120     end;
   121 
   122 
   123 (*********************************************************************)
   124 (* write out a subgoal as tptp clauses to the file "probN"           *)
   125 (* where N is the number of this subgoal                             *)
   126 (*********************************************************************)
   127 
   128 fun tptp_inputs_tfrees thms n tfrees = 
   129     let val _ = (warning ("in tptp_inputs_tfrees 0"))
   130         val clss = map (ResClause.make_conjecture_clause_thm) thms
   131          val _ = (warning ("in tptp_inputs_tfrees 1"))
   132 	val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
   133         val _ = (warning ("in tptp_inputs_tfrees 2"))
   134 	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
   135          val _ = (warning ("in tptp_inputs_tfrees 3"))
   136         val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
   137 	val out = TextIO.openOut(probfile)
   138     in
   139 	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
   140     end;
   141 
   142 
   143 
   144 (*********************************************************************)
   145 (* call SPASS with settings and problem file for the current subgoal *)
   146 (* should be modified to allow other provers to be called            *)
   147 (*********************************************************************)
   148 
   149 fun call_resolve_tac thms sg_term (childin, childout,pid) n  = let
   150                              val thmstring = concat_with_and (map string_of_thm thms) ""
   151                              val thm_no = length thms
   152                              val _ = warning ("number of thms is : "^(string_of_int thm_no))
   153                              val _ = warning ("thmstring in call_res is: "^thmstring)
   154 
   155                              val goalstr = Sign.string_of_term Mainsign sg_term 
   156                              val goalproofstring = proofstring goalstr
   157                              val no_returns =List.filter not_newline ( goalproofstring)
   158                              val goalstring = implode no_returns
   159                              val _ = warning ("goalstring in call_res is: "^goalstring)
   160         
   161                              (*val prob_file =File.tmp_path (Path.basic newprobfile); *)
   162                              (*val _ =( warning ("calling make_clauses "))
   163                              val clauses = make_clauses thms
   164                              val _ =( warning ("called make_clauses "))*)
   165                              (*val _ = tptp_inputs clauses prob_file*)
   166                              val thmstring = concat_with_and (map string_of_thm thms) ""
   167                            
   168                              val goalstr = Sign.string_of_term Mainsign sg_term 
   169                              val goalproofstring = proofstring goalstr
   170                              val no_returns =List.filter not_newline ( goalproofstring)
   171                              val goalstring = implode no_returns
   172 
   173                              val thmproofstring = proofstring ( thmstring)
   174                              val no_returns =List.filter   not_newline ( thmproofstring)
   175                              val thmstr = implode no_returns
   176                             
   177                              val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
   178                              val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile")))
   179                              val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
   180                              val _ = TextIO.flushOut outfile;
   181                              val _ =  TextIO.closeOut outfile
   182                           in
   183                            (* without paramodulation *)
   184                            (warning ("goalstring in call_res_tac is: "^goalstring));
   185                            (warning ("prob file in cal_res_tac is: "^probfile));
   186                             Watcher.callResProvers(childout,
   187                             [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",  
   188                              "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
   189                              probfile)]);
   190 
   191                            (* with paramodulation *)
   192                            (*Watcher.callResProvers(childout,
   193                                   [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",
   194                                   "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", 
   195                                     prob_path)]); *)
   196                           (* Watcher.callResProvers(childout,
   197                            [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", 
   198                            "-DocProof",  prob_path)]);*)
   199                            dummy_tac
   200                          end
   201 
   202 (************************************************)
   203 (* pass in subgoal as a term and watcher info   *)
   204 (* process subgoal into skolemized, negated form*)
   205 (* then call call_resolve_tac to send to ATP    *)
   206 (************************************************)
   207 (*
   208 fun resolve_tac sg_term  (childin, childout,pid) = 
   209    let val _ = warning ("in resolve_tac ")
   210    in
   211    SELECT_GOAL
   212   (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)*)))])
   213    end;
   214 
   215 *)
   216 
   217 
   218 (* Need to replace call_atp_tac_tfrees with call res_provers as it's the dummy one *)
   219 
   220 (**********************************************************)
   221 (* write out the current subgoal as a tptp file, probN,   *)
   222 (* then call dummy_tac - should be call_res_tac           *)
   223 (**********************************************************)
   224 (* should call call_res_tac here, not resolve_tac *)
   225 (* 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 *)
   226 
   227 (* dummy tac vs.  Doesn't call resolve_tac *)
   228 
   229 fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = 
   230                                          ( (warning("ths for tptp: "^(concat_with_and (map string_of_thm thms) "")));
   231                                            (warning("in call_atp_tac_tfrees"));
   232                                            
   233                                            tptp_inputs_tfrees (make_clauses thms) n tfrees;
   234                                            call_resolve_tac thms sg_term (childin, childout, pid) n;
   235   					   dummy_tac);
   236 
   237 
   238 (*
   239 fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
   240 let val _ = (warning ("in atp_tac_tfrees "))
   241    in
   242 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
   243 end;
   244 
   245 
   246 
   247 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;
   248 *)
   249 
   250 
   251 fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
   252 let val _ = (warning ("in atp_tac_tfrees "))
   253     val _ = (warning ("sg_term :"^((Sign.string_of_term Mainsign) sg_term)))
   254    
   255    in
   256 SELECT_GOAL
   257   (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
   258   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
   259 end;
   260 
   261 
   262 fun isar_atp_g tfrees sg_term (childin, childout, pid) n = 
   263                                         
   264 ((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
   265 
   266 
   267 
   268 (**********************************************)
   269 (* recursively call atp_tac_g on all subgoals *)
   270 (* sg_term is the nth subgoal as a term - used*)
   271 (* in proof reconstruction                    *)
   272 (**********************************************)
   273 
   274 fun isar_atp_goal' thm k n tfree_lits  (childin, childout, pid) = 
   275                   	if (k > n) 
   276                         then () 
   277 	  		else 
   278                            (let val  prems = prems_of thm 
   279                                 val sg_term = get_nth n prems
   280                                 val thmstring = string_of_thm thm
   281                             in   
   282                                  
   283                 		(warning("in isar_atp_goal'"));
   284                                 (warning("thmstring in isar_atp_goal: "^thmstring));
   285  				 isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
   286                                  isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
   287                             end);
   288 
   289 
   290 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) ));
   291 
   292 (**************************************************)
   293 (* convert clauses from "assume" to conjecture.   *)
   294 (* i.e. apply make_clauses and then get tptp for  *)
   295 (* any hypotheses in the goal produced by assume  *)
   296 (* statements;                                    *)
   297 (* write to file "hyps"                           *)
   298 (**************************************************)
   299 
   300 
   301 fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
   302     let val tfree_lits = isar_atp_h thms 
   303     in
   304 	(warning("in isar_atp_aux"));isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid)
   305     end;
   306 
   307 (******************************************************************)
   308 (* called in Isar automatically                                   *)
   309 (* writes out the current clasimpset to a tptp file               *)
   310 (* passes all subgoals on to isar_atp_aux for further processing  *)
   311 (* turns off xsymbol at start of function, restoring it at end    *)
   312 (******************************************************************)
   313 
   314 fun isar_atp' (thms, thm) =
   315     let val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   316         val _= (warning ("in isar_atp'"))
   317         val prems = prems_of thm
   318         val thms_string =concat_with_and (map  string_of_thm thms) ""
   319         val thmstring = string_of_thm thm
   320         val prems_string = concat_with_and (map (Sign.string_of_term Mainsign) prems) ""
   321         (* set up variables for writing out the clasimps to a tptp file *)
   322         (* val _ = write_out_clasimp (File.sysify_path axiom_file)*)
   323         (* cq: add write out clasimps to file *)
   324         (* cq:create watcher and pass to isar_atp_aux *)                    
   325         val (childin,childout,pid) = Watcher.createWatcher()
   326         val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
   327     in
   328 	case prems of [] => () 
   329 		    | _ => ((warning ("initial thms: "^thms_string)); 
   330                            (warning ("initial thm: "^thmstring));
   331                            (warning ("subgoals: "^prems_string));
   332                            (warning ("pid: "^ pidstring))); 
   333                             isar_atp_aux thms thm (length prems) (childin, childout, pid) ;
   334                            
   335                            print_mode := (["xsymbols", "symbols"] @ ! print_mode)
   336     end;
   337 
   338 
   339 
   340 
   341 local
   342 
   343 fun get_thms_cs claset =
   344     let val clsset = rep_cs claset
   345 	val safeEs = #safeEs clsset
   346 	val safeIs = #safeIs clsset
   347 	val hazEs = #hazEs clsset
   348 	val hazIs = #hazIs clsset
   349     in
   350 	safeEs @ safeIs @ hazEs @ hazIs
   351     end;
   352 
   353 
   354 
   355 fun append_name name [] _ = []
   356   | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
   357 
   358 fun append_names (name::names) (thms::thmss) =
   359     let val thms' = append_name name thms 0
   360     in
   361 	thms'::(append_names names thmss)
   362     end;
   363 
   364 
   365 fun get_thms_ss [] = []
   366   | get_thms_ss thms =
   367     let val names = map Thm.name_of_thm thms 
   368         val thms' = map (mksimps mksimps_pairs) thms
   369         val thms'' = append_names names thms'
   370     in
   371 	ResLib.flat_noDup thms''
   372     end;
   373 
   374 
   375 
   376 
   377 in
   378 
   379 
   380 (* convert locally declared rules to axiom clauses *)
   381 (* write axiom clauses to ax_file *)
   382 (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
   383 (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
   384 (*claset file and prob file*)
   385 fun isar_local_thms (delta_cs, delta_ss_thms) =
   386     let val thms_cs = get_thms_cs delta_cs
   387 	val thms_ss = get_thms_ss delta_ss_thms
   388 	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
   389 	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
   390 	val ax_file = File.sysify_path axiom_file
   391 	val out = TextIO.openOut ax_file
   392     in
   393 	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
   394     end;
   395 
   396 
   397 
   398 
   399 
   400 (* called in Isar automatically *)
   401 
   402 fun isar_atp (ctxt,thm) =
   403     let val prems = ProofContext.prems_of ctxt
   404         val d_cs = Classical.get_delta_claset ctxt 
   405         val d_ss_thms = Simplifier.get_delta_simpset ctxt
   406         val thmstring = string_of_thm thm
   407         val sg_prems = prems_of thm
   408         val prem_no = length sg_prems
   409         val prems_string =  concat_with_and (map (Sign.string_of_term Mainsign) sg_prems) ""
   410     in
   411          
   412           (warning ("initial thm in isar_atp: "^thmstring));
   413           (warning ("subgoals in isar_atp: "^prems_string));
   414     	   (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   415           (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'"));
   416            isar_atp' (prems, thm))
   417     end;
   418 
   419 end
   420 
   421 
   422 
   423 
   424 end;
   425 
   426 Proof.atp_hook := ResAtp.isar_atp;