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