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