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