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