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