src/HOL/Tools/res_atp.ML
author quigley
Mon May 23 00:18:51 2005 +0200 (2005-05-23)
changeset 16039 dfe264950511
parent 15919 b30a35432f5a
child 16061 8a139c1557bf
permissions -rw-r--r--
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
Changed watcher.ML so that the Unix.execute and Unix.reap functions are used instead of those in modUnix.ML, and
consequently removed modUnix.ML from Reconstruction.thy
     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                              val spass_home = getenv "SPASS_HOME"
   184                           in
   185                            (* without paramodulation *)
   186                            (warning ("goalstring in call_res_tac is: "^goalstring));
   187                            (warning ("prob file in cal_res_tac is: "^probfile));
   188                                                       (* Watcher.callResProvers(childout,
   189                             [("spass",thmstr,goalstring,(*spass_home*),  
   190                              "-DocProof", 
   191                              clasimpfile, axfile, hypsfile, probfile)]);*)
   192 
   193                             Watcher.callResProvers(childout,
   194                             [("spass",thmstr,goalstring(*,spass_home*),"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/spassshell",  
   195                              "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
   196                              clasimpfile, axfile, hypsfile, probfile)]);
   197 
   198                            (* with paramodulation *)
   199                            (*Watcher.callResProvers(childout,
   200                                   [("spass",thmstr,goalstring,spass_home,
   201                                   "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", 
   202                                     prob_path)]); *)
   203                           (* Watcher.callResProvers(childout,
   204                            [("spass",thmstr,goalstring,spass_home, 
   205                            "-DocProof",  prob_path)]);*)
   206                            dummy_tac
   207                          end
   208 
   209 (**********************************************************)
   210 (* write out the current subgoal as a tptp file, probN,   *)
   211 (* then call dummy_tac - should be call_res_tac           *)
   212 (**********************************************************)
   213 
   214 
   215 fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
   216                                          (
   217                                            warning("in call_atp_tac_tfrees");
   218                                            
   219                                            tptp_inputs_tfrees (make_clauses thms) n tfrees;
   220                                            call_resolve_tac sign thms sg_term (childin, childout, pid) n;
   221   					   dummy_tac);
   222 
   223 fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n st = 
   224 let val sign = sign_of_thm st
   225     val _ = warning ("in atp_tac_tfrees ")
   226     val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
   227    
   228    in
   229 
   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 (childin, childout,pid) ))]) n st
   233 end;
   234 
   235 
   236 fun isar_atp_g tfrees sg_term (childin, childout, pid) n =       
   237 ((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
   238 
   239 
   240 
   241 (**********************************************)
   242 (* recursively call atp_tac_g on all subgoals *)
   243 (* sg_term is the nth subgoal as a term - used*)
   244 (* in proof reconstruction                    *)
   245 (**********************************************)
   246 
   247 fun isar_atp_goal' thm k n tfree_lits  (childin, childout, pid) = 
   248                   	if (k > n) 
   249                         then () 
   250 	  		else 
   251                            (let val  prems = prems_of thm 
   252                                 val sg_term = get_nth n prems
   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  				 isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
   259                                  isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
   260                             end);
   261 
   262 
   263 fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
   264               (if (!debug) then warning (string_of_thm thm) 
   265                else (isar_atp_goal' thm 1 n_subgoals tfree_lits  (childin, childout, pid) ));
   266 
   267 (**************************************************)
   268 (* convert clauses from "assume" to conjecture.   *)
   269 (* i.e. apply make_clauses and then get tptp for  *)
   270 (* any hypotheses in the goal produced by assume  *)
   271 (* statements;                                    *)
   272 (* write to file "hyps"                           *)
   273 (**************************************************)
   274 
   275 
   276 fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
   277     let val tfree_lits = isar_atp_h thms 
   278     in
   279 	(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' (thms, thm) =
   291     let 
   292 	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   293         val _= (warning ("in isar_atp'"))
   294         val prems  = prems_of thm
   295         val sign = sign_of_thm thm
   296         val thms_string = Meson.concat_with_and (map string_of_thm thms) 
   297         val thmstring = string_of_thm thm
   298         val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   299         
   300 	(* set up variables for writing out the clasimps to a tptp file *)
   301 	val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) 
   302         val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
   303 
   304         (* cq: add write out clasimps to file *)
   305 
   306         (* cq:create watcher and pass to isar_atp_aux *)
   307         (* tracing *) 
   308         (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   309          val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab)
   310          val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   311          val _ = (warning ("tenth axiom in array is: "^tenth_ax))         
   312          val _ = (warning ("tenth axiom in table is: "^clause_str))         
   313                  
   314          val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) )     
   315          *)             
   316         
   317         val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
   318         val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
   319     in
   320 	case prems of [] => () 
   321 		    | _ => ((warning ("initial thms: "^thms_string)); 
   322                            (warning ("initial thm: "^thmstring));
   323                            (warning ("subgoals: "^prems_string));
   324                            (warning ("pid: "^ pidstring))); 
   325                             isar_atp_aux thms thm (length prems) (childin, childout, pid) ;
   326                            
   327                            print_mode := (["xsymbols", "symbols"] @ ! print_mode)
   328     end;
   329 
   330 
   331 
   332 
   333 local
   334 
   335 fun get_thms_cs claset =
   336     let val clsset = rep_cs claset
   337 	val safeEs = #safeEs clsset
   338 	val safeIs = #safeIs clsset
   339 	val hazEs = #hazEs clsset
   340 	val hazIs = #hazIs clsset
   341     in
   342 	safeEs @ safeIs @ hazEs @ hazIs
   343     end;
   344 
   345 
   346 
   347 fun append_name name [] _ = []
   348   | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
   349 
   350 fun append_names (name::names) (thms::thmss) =
   351     let val thms' = append_name name thms 0
   352     in
   353 	thms'::(append_names names thmss)
   354     end;
   355 
   356 
   357 fun get_thms_ss [] = []
   358   | get_thms_ss thms =
   359     let val names = map Thm.name_of_thm thms 
   360         val thms' = map (mksimps mksimps_pairs) thms
   361         val thms'' = append_names names thms'
   362     in
   363 	ResLib.flat_noDup thms''
   364     end;
   365 
   366 
   367 
   368 
   369 in
   370 
   371 
   372 (* convert locally declared rules to axiom clauses *)
   373 (* write axiom clauses to ax_file *)
   374 (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
   375 (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
   376 (*claset file and prob file*)
   377 (* FIX: update to work with clausify_axiom_pairs now in ResAxioms*)
   378 (*fun isar_local_thms (delta_cs, delta_ss_thms) =
   379     let val thms_cs = get_thms_cs delta_cs
   380 	val thms_ss = get_thms_ss delta_ss_thms
   381 	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
   382 	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
   383 	val ax_file = File.sysify_path axiom_file
   384 	val out = TextIO.openOut ax_file
   385     in
   386 	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
   387     end;
   388 *)
   389 
   390 
   391 
   392 
   393 (* called in Isar automatically *)
   394 
   395 fun isar_atp (ctxt,thm) =
   396     let val prems = ProofContext.prems_of ctxt
   397         val d_cs = Classical.get_delta_claset ctxt 
   398         val d_ss_thms = Simplifier.get_delta_simpset ctxt
   399         val thmstring = string_of_thm thm
   400         val sg_prems = prems_of thm
   401         val sign = sign_of_thm thm
   402         val prem_no = length sg_prems
   403         val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) 
   404     in
   405           (warning ("initial thm in isar_atp: "^thmstring));
   406           (warning ("subgoals in isar_atp: "^prems_string));
   407     	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   408           ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
   409            isar_atp' (prems, thm))
   410     end;
   411 
   412 end
   413 
   414 
   415 
   416 
   417 end;
   418 
   419 Proof.atp_hook := ResAtp.isar_atp;