src/HOL/Tools/res_atp.ML
author paulson
Tue May 24 10:23:24 2005 +0200 (2005-05-24)
changeset 16061 8a139c1557bf
parent 16039 dfe264950511
child 16089 9169bdf930f8
permissions -rw-r--r--
A new structure and reduced indentation
     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 = ReconOrderClauses.get_nth n prems
   253 	      val thmstring = string_of_thm thm
   254 	  in   
   255 	      (warning("in isar_atp_goal'"));
   256 	      (warning("thmstring in isar_atp_goal': "^thmstring));
   257 	       isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
   258 	       isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
   259 	  end;
   260 
   261 
   262 fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
   263               (if (!debug) then warning (string_of_thm thm) 
   264                else (isar_atp_goal' thm 1 n_subgoals tfree_lits  (childin, childout, pid) ));
   265 
   266 (**************************************************)
   267 (* convert clauses from "assume" to conjecture.   *)
   268 (* i.e. apply make_clauses and then get tptp for  *)
   269 (* any hypotheses in the goal produced by assume  *)
   270 (* statements;                                    *)
   271 (* write to file "hyps"                           *)
   272 (**************************************************)
   273 
   274 
   275 fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
   276     let val tfree_lits = isar_atp_h thms 
   277     in
   278 	(warning("in isar_atp_aux"));
   279          isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid)
   280     end;
   281 
   282 (******************************************************************)
   283 (* called in Isar automatically                                   *)
   284 (* writes out the current clasimpset to a tptp file               *)
   285 (* passes all subgoals on to isar_atp_aux for further processing  *)
   286 (* turns off xsymbol at start of function, restoring it at end    *)
   287 (******************************************************************)
   288 (*FIX changed to clasimp_file *)
   289 fun isar_atp' (thms, thm) =
   290     let 
   291 	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) = ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) 
   301         val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
   302 
   303         (* cq: add write out clasimps to file *)
   304 
   305         (* cq:create watcher and pass to isar_atp_aux *)
   306         (* tracing *) 
   307         (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   308          val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab)
   309          val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   310          val _ = (warning ("tenth axiom in array is: "^tenth_ax))         
   311          val _ = (warning ("tenth axiom in table is: "^clause_str))         
   312                  
   313          val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) )     
   314          *)             
   315         
   316         val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
   317         val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
   318     in
   319 	case prems of [] => () 
   320 		    | _ => ((warning ("initial thms: "^thms_string)); 
   321                            (warning ("initial thm: "^thmstring));
   322                            (warning ("subgoals: "^prems_string));
   323                            (warning ("pid: "^ pidstring))); 
   324                             isar_atp_aux thms thm (length prems) (childin, childout, pid) ;
   325                            
   326                            print_mode := (["xsymbols", "symbols"] @ ! print_mode)
   327     end;
   328 
   329 
   330 
   331 
   332 local
   333 
   334 fun get_thms_cs claset =
   335     let val clsset = rep_cs claset
   336 	val safeEs = #safeEs clsset
   337 	val safeIs = #safeIs clsset
   338 	val hazEs = #hazEs clsset
   339 	val hazIs = #hazIs clsset
   340     in
   341 	safeEs @ safeIs @ hazEs @ hazIs
   342     end;
   343 
   344 
   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 
   356 fun get_thms_ss [] = []
   357   | get_thms_ss thms =
   358     let val names = map Thm.name_of_thm thms 
   359         val thms' = map (mksimps mksimps_pairs) thms
   360         val thms'' = append_names names thms'
   361     in
   362 	ResLib.flat_noDup thms''
   363     end;
   364 
   365 
   366 
   367 
   368 in
   369 
   370 
   371 (* convert locally declared rules to axiom clauses *)
   372 (* write axiom clauses to ax_file *)
   373 (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
   374 (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
   375 (*claset file and prob file*)
   376 (* FIX: update to work with clausify_axiom_pairs now in ResAxioms*)
   377 (*fun isar_local_thms (delta_cs, delta_ss_thms) =
   378     let val thms_cs = get_thms_cs delta_cs
   379 	val thms_ss = get_thms_ss delta_ss_thms
   380 	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
   381 	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
   382 	val ax_file = File.sysify_path axiom_file
   383 	val out = TextIO.openOut ax_file
   384     in
   385 	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
   386     end;
   387 *)
   388 
   389 
   390 
   391 
   392 (* called in Isar automatically *)
   393 
   394 fun isar_atp (ctxt,thm) =
   395     let val prems = ProofContext.prems_of ctxt
   396         val d_cs = Classical.get_delta_claset ctxt 
   397         val d_ss_thms = Simplifier.get_delta_simpset ctxt
   398         val thmstring = string_of_thm thm
   399         val sg_prems = prems_of thm
   400         val sign = sign_of_thm thm
   401         val prem_no = length sg_prems
   402         val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) 
   403     in
   404           (warning ("initial thm in isar_atp: "^thmstring));
   405           (warning ("subgoals in isar_atp: "^prems_string));
   406     	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   407           ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
   408            isar_atp' (prems, thm))
   409     end;
   410 
   411 end
   412 
   413 
   414 
   415 
   416 end;
   417 
   418 Proof.atp_hook := ResAtp.isar_atp;