small tweaks; also now write_out_clasimp takes the current theory as argument
authorpaulson
Wed Jun 01 14:50:48 2005 +0200 (2005-06-01)
changeset 16172629ba53a072f
parent 16171 3c939bb52420
child 16173 9e2f6c0a779d
small tweaks; also now write_out_clasimp takes the current theory as argument
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Jun 01 14:16:45 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Jun 01 14:50:48 2005 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature RES_CLASIMP = 
     1.6    sig
     1.7 -     val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int
     1.8 +     val write_out_clasimp :string -> theory -> (ResClause.clause * thm) Array.array * int
     1.9    end;
    1.10  
    1.11  structure ResClasimp : RES_CLASIMP =
    1.12 @@ -63,25 +63,22 @@
    1.13  fun multi x 0 xlist = xlist
    1.14     |multi x n xlist = multi x (n -1 ) (x::xlist);
    1.15  
    1.16 +fun clause_numbering ((clause, theorem), cls) = 
    1.17 +    let val num_of_cls = length cls
    1.18 +	val numbers = 0 upto (num_of_cls -1)
    1.19 +	val multi_name = multi (clause, theorem)  num_of_cls []
    1.20 +    in 
    1.21 +	(multi_name)
    1.22 +    end;
    1.23  
    1.24 -fun clause_numbering ((clause, theorem), cls) = let val num_of_cls = length cls
    1.25 -                                              val numbers = 0 upto (num_of_cls -1)
    1.26 -                                              val multi_name = multi (clause, theorem)  num_of_cls []
    1.27 -                                          in 
    1.28 -                                              (multi_name)
    1.29 -                                          end;
    1.30 -
    1.31 -
    1.32 -
    1.33 - 
    1.34 -
    1.35 -fun write_out_clasimp filename = 
    1.36 -    let val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
    1.37 +(*Write out the claset and simpset rules of the supplied theory.*)
    1.38 +fun write_out_clasimp filename thy = 
    1.39 +    let val claset_rules = ResAxioms.claset_rules_of_thy thy;
    1.40  	val named_claset = List.filter has_name_pair claset_rules;
    1.41  	val claset_names = map remove_spaces_pair (named_claset)
    1.42  	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
    1.43  
    1.44 -	val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
    1.45 +	val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
    1.46  	val named_simpset = 
    1.47  	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
    1.48  	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
     2.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jun 01 14:16:45 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jun 01 14:50:48 2005 +0200
     2.3 @@ -31,11 +31,9 @@
     2.4  val subgoals = [];
     2.5  
     2.6  val traceflag = ref true;
     2.7 -(* used for debug *)
     2.8 +
     2.9  val debug = ref false;
    2.10 -
    2.11  fun debug_tac tac = (warning "testing";tac);
    2.12 -(* default value is false *)
    2.13  
    2.14  val trace_res = ref false;
    2.15  val full_spass = ref false;
    2.16 @@ -71,13 +69,10 @@
    2.17   
    2.18  (**** for Isabelle/ML interface  ****)
    2.19  
    2.20 -fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
    2.21 +fun is_proof_char ch = (ch = " ") orelse
    2.22 +     ((ord"!" <= ord ch) andalso (ord ch <= ord"~") andalso (ch <> "?"))  
    2.23  
    2.24 -fun proofstring x = let val exp = explode x 
    2.25 -                    in
    2.26 -                        List.filter (is_proof_char ) exp
    2.27 -                    end
    2.28 -
    2.29 +fun proofstring x = List.filter (is_proof_char) (explode x);
    2.30  
    2.31  
    2.32  (*
    2.33 @@ -135,11 +130,11 @@
    2.34          val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    2.35  	val out = TextIO.openOut(probfile)
    2.36      in
    2.37 -	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
    2.38 +	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out;
    2.39 +	 if !trace_res then (warning probfile) else ())
    2.40      end;
    2.41  
    2.42  
    2.43 -
    2.44  (*********************************************************************)
    2.45  (* call SPASS with settings and problem file for the current subgoal *)
    2.46  (* should be modified to allow other provers to be called            *)
    2.47 @@ -221,28 +216,27 @@
    2.48  
    2.49  
    2.50  fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
    2.51 -                                         (
    2.52 -                                           warning("in call_atp_tac_tfrees");
    2.53 -                                           
    2.54 -                                           tptp_inputs_tfrees (make_clauses thms) n tfrees;
    2.55 -                                           call_resolve_tac sign thms sg_term (childin, childout, pid) n;
    2.56 -  					   dummy_tac);
    2.57 + (
    2.58 +   warning("in call_atp_tac_tfrees");
    2.59 +   tptp_inputs_tfrees (make_clauses thms) n tfrees;
    2.60 +   call_resolve_tac sign thms sg_term (childin, childout, pid) n;
    2.61 +   dummy_tac);
    2.62  
    2.63  fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n st = 
    2.64 -let val sign = sign_of_thm st
    2.65 -    val _ = warning ("in atp_tac_tfrees ")
    2.66 -    val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
    2.67 -   
    2.68 -   in
    2.69 -
    2.70 -SELECT_GOAL
    2.71 -  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    2.72 -  METAHYPS(fn negs => ( call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st
    2.73 -end;
    2.74 +  let val sign = sign_of_thm st
    2.75 +      val _ = warning ("in atp_tac_tfrees ")
    2.76 +      val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
    2.77 +  in  
    2.78 +    SELECT_GOAL
    2.79 +      (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    2.80 +       METAHYPS(fn negs => (call_atp_tac_tfrees sign negs n tfrees sg_term
    2.81 +                            (childin, childout,pid) ))]) n st
    2.82 +  end;
    2.83  
    2.84  
    2.85  fun isar_atp_g tfrees sg_term (childin, childout, pid) n =       
    2.86 -((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
    2.87 +  ((warning("in isar_atp_g"));
    2.88 +   atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
    2.89  
    2.90  
    2.91  
    2.92 @@ -256,7 +250,7 @@
    2.93        if (k > n) 
    2.94        then () 
    2.95        else 
    2.96 -	  let val  prems = prems_of thm 
    2.97 +	  let val prems = prems_of thm 
    2.98  	      val sg_term = ReconOrderClauses.get_nth n prems
    2.99  	      val thmstring = string_of_thm thm
   2.100  	  in   
   2.101 @@ -282,9 +276,8 @@
   2.102  
   2.103  fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
   2.104      let val tfree_lits = isar_atp_h thms 
   2.105 -    in
   2.106 -	(warning("in isar_atp_aux"));
   2.107 -         isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid)
   2.108 +    in warning("in isar_atp_aux");
   2.109 +       isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid)
   2.110      end;
   2.111  
   2.112  (******************************************************************)
   2.113 @@ -294,9 +287,8 @@
   2.114  (* turns off xsymbol at start of function, restoring it at end    *)
   2.115  (******************************************************************)
   2.116  (*FIX changed to clasimp_file *)
   2.117 -fun isar_atp' (thms, thm) =
   2.118 -    let 
   2.119 -	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   2.120 +fun isar_atp' (ctxt, thms, thm) =
   2.121 +    let val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   2.122          val _= (warning ("in isar_atp'"))
   2.123          val prems  = prems_of thm
   2.124          val sign = sign_of_thm thm
   2.125 @@ -305,8 +297,10 @@
   2.126          val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   2.127          
   2.128  	(* set up variables for writing out the clasimps to a tptp file *)
   2.129 -	val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) 
   2.130 -        val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
   2.131 +	val (clause_arr, num_of_clauses) =
   2.132 +	    ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) 
   2.133 +	                                 (ProofContext.theory_of ctxt)
   2.134 +        val _ = warning ("clasimp_file is " ^ File.sysify_path clasimp_file)
   2.135  
   2.136          (* cq: add write out clasimps to file *)
   2.137  
   2.138 @@ -349,8 +343,6 @@
   2.139  	safeEs @ safeIs @ hazEs @ hazIs
   2.140      end;
   2.141  
   2.142 -
   2.143 -
   2.144  fun append_name name [] _ = []
   2.145    | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
   2.146  
   2.147 @@ -360,7 +352,6 @@
   2.148  	thms'::(append_names names thmss)
   2.149      end;
   2.150  
   2.151 -
   2.152  fun get_thms_ss [] = []
   2.153    | get_thms_ss thms =
   2.154      let val names = map Thm.name_of_thm thms 
   2.155 @@ -370,9 +361,6 @@
   2.156  	ResLib.flat_noDup thms''
   2.157      end;
   2.158  
   2.159 -
   2.160 -
   2.161 -
   2.162  in
   2.163  
   2.164  
   2.165 @@ -395,8 +383,6 @@
   2.166  *)
   2.167  
   2.168  
   2.169 -
   2.170 -
   2.171  (* called in Isar automatically *)
   2.172  
   2.173  fun isar_atp (ctxt,thm) =
   2.174 @@ -413,14 +399,12 @@
   2.175            (warning ("subgoals in isar_atp: "^prems_string));
   2.176      	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   2.177            ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
   2.178 -           isar_atp' (prems, thm))
   2.179 +           isar_atp' (ctxt, prems, thm))
   2.180      end;
   2.181  
   2.182  end
   2.183  
   2.184  
   2.185 -
   2.186 -
   2.187  end;
   2.188  
   2.189  Proof.atp_hook := ResAtp.isar_atp;