src/HOL/Tools/res_atp.ML
author paulson
Tue Jun 21 13:34:24 2005 +0200 (2005-06-21)
changeset 16515 7896ea4f3a87
parent 16478 d0a1f6231e2f
child 16520 7a9cda53bfa2
permissions -rw-r--r--
VAMPIRE_HOME, helper_path and various stylistic tweaks
     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  = 
   157  let
   158    val axfile = (File.platform_path axiom_file)
   159    val hypsfile = (File.platform_path hyps_file)
   160    val clasimpfile = (File.platform_path clasimp_file)
   161      
   162    fun make_atp_list [] sign n = []
   163    |   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
   164      let 
   165 	val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
   166 	val thmproofstr = proofstring ( skothmstr)
   167 	val no_returns =List.filter   not_newline ( thmproofstr)
   168 	val thmstr = implode no_returns
   169 	val _ = warning ("thmstring in make_atp_lists is: "^thmstr)
   170 
   171 	val sgstr = Sign.string_of_term sign sg_term 
   172 	val goalproofstring = proofstring sgstr
   173 	val no_returns =List.filter not_newline ( goalproofstring)
   174 	val goalstring = implode no_returns
   175 	val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
   176 
   177 	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
   178 	val _ = (warning ("prob file in cal_res_tac is: "^probfile))      
   179      in
   180        if !SpassComm.spass 
   181        then 
   182          let val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
   183          in  (*We've checked that SPASS is there for ATP/spassshell to run.*)
   184            if !full_spass 
   185             then (*Allow SPASS to run in Auto mode, using all its inference rules*)
   186    		([("spass", thmstr, goalstring (*,spass_home*), 
   187 	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
   188 	     	"-DocProof%-TimeLimit=60", 
   189 	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
   190   	    else (*Restrict SPASS to a small set of rules that we can parse*)
   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 	 end
   196      else
   197        let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
   198        in  
   199 	   ([("vampire", thmstr, goalstring, vampire, "-t 300%-m 100000", 
   200 	      clasimpfile, axfile, hypsfile, probfile)] @ 
   201 	    (make_atp_list xs sign (n+1)))
   202        end
   203      end
   204 
   205 val thms_goals = ListPair.zip( thms, sg_terms) 
   206 val atp_list = make_atp_list  thms_goals sign 1
   207 in
   208 	Watcher.callResProvers(childout,atp_list);
   209         warning("Sent commands to watcher!");
   210   	dummy_tac
   211  end
   212 (*
   213   val axfile = (File.platform_path axiom_file)
   214     val hypsfile = (File.platform_path hyps_file)
   215      val clasimpfile = (File.platform_path  clasimp_file)
   216     val spass_home = getenv "SPASS_HOME"
   217  val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int 1)
   218     
   219  val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp_small (File.platform_path clasimp_file) ;
   220  val (childin,childout,pid) = Watcher.createWatcher(mp, clause_arr, num_of_clauses);
   221 Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", spass_home,  "-DocProof", clasimpfile, axfile, hypsfile,probfile)]);
   222 
   223 Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", "/homes/clq20/spassshell",  "", clasimpfile, axfile, hypsfile,probfile)]);
   224 
   225 
   226 *)
   227 (**********************************************************)
   228 (* write out the current subgoal as a tptp file, probN,   *)
   229 (* then call dummy_tac - should be call_res_tac           *)
   230 (**********************************************************)
   231 
   232 
   233 fun get_sko_thms tfrees sign sg_terms (childin, childout,pid)  thm n sko_thms  =
   234     if n=0 then 
   235 	     (call_resolve_tac  (rev sko_thms) sign  sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
   236      else
   237 	
   238      ( SELECT_GOAL
   239 	     (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
   240 	      METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
   241 				 get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms);dummy_tac))]) n thm )
   242 
   243 
   244 
   245 (**********************************************)
   246 (* recursively call atp_tac_g on all subgoals *)
   247 (* sg_term is the nth subgoal as a term - used*)
   248 (* in proof reconstruction                    *)
   249 (**********************************************)
   250 
   251 fun isar_atp_goal' thm n tfree_lits  (childin, childout, pid) = 
   252     let val  prems = prems_of thm 
   253       (*val sg_term = get_nth k prems*)
   254 	val sign = sign_of_thm thm
   255 	val thmstring = string_of_thm thm
   256     in   
   257 	warning("in isar_atp_goal'");
   258 	warning("thmstring in isar_atp_goal': "^thmstring);
   259 	(* go and call callResProvers with this subgoal *)
   260 	(* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   261 	(* recursive call to pick up the remaining subgoals *)
   262 	(* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   263 	get_sko_thms tfree_lits sign  prems (childin, childout, pid) thm n []
   264     end ;
   265 
   266 (*fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
   267               (if (!debug) then warning (string_of_thm thm) 
   268                else (isar_atp_goal' thm n_subgoals tfree_lits  (childin, childout, pid) ));*)
   269 
   270 (**************************************************)
   271 (* convert clauses from "assume" to conjecture.   *)
   272 (* i.e. apply make_clauses and then get tptp for  *)
   273 (* any hypotheses in the goal produced by assume  *)
   274 (* statements;                                    *)
   275 (* write to file "hyps"                           *)
   276 (**************************************************)
   277 
   278 
   279 fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
   280     let val tfree_lits = isar_atp_h thms 
   281     in
   282 	(warning("in isar_atp_aux"));
   283          isar_atp_goal' thm n_subgoals tfree_lits   (childin, childout, pid)
   284     end;
   285 
   286 (******************************************************************)
   287 (* called in Isar automatically                                   *)
   288 (* writes out the current clasimpset to a tptp file               *)
   289 (* passes all subgoals on to isar_atp_aux for further processing  *)
   290 (* turns off xsymbol at start of function, restoring it at end    *)
   291 (******************************************************************)
   292 (*FIX changed to clasimp_file *)
   293 fun isar_atp' (ctxt,thms, thm) =
   294     let 
   295 	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   296         val _= (warning ("in isar_atp'"))
   297         val prems  = prems_of thm
   298         val sign = sign_of_thm thm
   299         val thms_string = Meson.concat_with_and (map string_of_thm thms) 
   300         val thmstring = string_of_thm thm
   301         val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   302         
   303 	(* set up variables for writing out the clasimps to a tptp file *)
   304 	val (clause_arr, num_of_clauses) =
   305 	    ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) 
   306 	                                 (ProofContext.theory_of ctxt)
   307         val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) )  
   308 
   309         (* cq: add write out clasimps to file *)
   310         (* cq:create watcher and pass to isar_atp_aux *)
   311         (* tracing *) 
   312         (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   313          val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab)
   314          val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   315          val _ = (warning ("tenth axiom in array is: "^tenth_ax))         
   316          val _ = (warning ("tenth axiom in table is: "^clause_str))         
   317                  
   318          val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) )     
   319          *)             
   320         
   321         val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
   322         val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
   323     in
   324 	case prems of [] => () 
   325 		    | _ => ((warning ("initial thms: "^thms_string)); 
   326                            (warning ("initial thm: "^thmstring));
   327                            (warning ("subgoals: "^prems_string));
   328                            (warning ("pid: "^ pidstring))); 
   329                             isar_atp_aux thms thm (length prems) (childin, childout, pid) ;
   330                            (warning("turning xsymbol back on!"));
   331                            print_mode := (["xsymbols", "symbols"] @ ! print_mode)
   332     end;
   333 
   334 
   335 
   336 
   337 local
   338 
   339 fun get_thms_cs claset =
   340     let val clsset = rep_cs claset
   341 	val safeEs = #safeEs clsset
   342 	val safeIs = #safeIs clsset
   343 	val hazEs = #hazEs clsset
   344 	val hazIs = #hazIs clsset
   345     in
   346 	safeEs @ safeIs @ hazEs @ hazIs
   347     end;
   348 
   349 
   350 
   351 fun append_name name [] _ = []
   352   | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
   353 
   354 fun append_names (name::names) (thms::thmss) =
   355     let val thms' = append_name name thms 0
   356     in
   357 	thms'::(append_names names thmss)
   358     end;
   359 
   360 
   361 fun get_thms_ss [] = []
   362   | get_thms_ss thms =
   363     let val names = map Thm.name_of_thm thms 
   364         val thms' = map (mksimps mksimps_pairs) thms
   365         val thms'' = append_names names thms'
   366     in
   367 	ResLib.flat_noDup thms''
   368     end;
   369 
   370 
   371 
   372 
   373 in
   374 
   375 
   376 (* convert locally declared rules to axiom clauses *)
   377 (* write axiom clauses to ax_file *)
   378 (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
   379 (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
   380 (*claset file and prob file*)
   381 (* FIX*)
   382 (*fun isar_local_thms (delta_cs, delta_ss_thms) =
   383     let val thms_cs = get_thms_cs delta_cs
   384 	val thms_ss = get_thms_ss delta_ss_thms
   385 	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
   386 	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
   387 	val ax_file = File.platform_path axiom_file
   388 	val out = TextIO.openOut ax_file
   389     in
   390 	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
   391     end;
   392 *)
   393 
   394 
   395 
   396 
   397 (* called in Isar automatically *)
   398 
   399 fun isar_atp (ctxt,thm) =
   400     let val prems = ProofContext.prems_of ctxt
   401         val d_cs = Classical.get_delta_claset ctxt 
   402         val d_ss_thms = Simplifier.get_delta_simpset ctxt
   403         val thmstring = string_of_thm thm
   404         val sg_prems = prems_of thm
   405         val sign = sign_of_thm thm
   406         val prem_no = length sg_prems
   407         val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) 
   408     in
   409           (warning ("initial thm in isar_atp: "^thmstring));
   410           (warning ("subgoals in isar_atp: "^prems_string));
   411     	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   412           (*isar_local_thms (d_cs,d_ss_thms);*)
   413            isar_atp' (ctxt,prems, thm)
   414     end;
   415 
   416 end
   417 
   418 
   419 
   420 
   421 end;
   422 
   423 Proof.atp_hook := ResAtp.isar_atp;