src/HOL/Tools/ATP/res_clasimpset.ML
changeset 17234 12a9393c5d77
parent 17150 ce2a1aeb42aa
child 17261 193b84a70ca4
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Sep 02 17:23:59 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Sep 02 17:55:24 2005 +0200
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  structure ReduceAxiomsN =
     1.6  (* Author: Jia Meng, Cambridge University Computer Laboratory
     1.7 -   Remove irrelevant axioms used for a proof of a goal, with with iteration control*)
     1.8 +   Remove irrelevant axioms used for a proof of a goal, with with iteration control
     1.9 +   
    1.10 +   Initial version. Needs elaboration. *)
    1.11  
    1.12  struct
    1.13  
    1.14 @@ -143,31 +145,6 @@
    1.15  (* outputs a list of (thm,clause) pairs *)
    1.16  
    1.17  
    1.18 -(* for tracing: encloses each string element in brackets. *)
    1.19 -fun concat_with_stop [] = ""
    1.20 -  | concat_with_stop [x] =  x
    1.21 -  | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs;
    1.22 -
    1.23 -fun remove_symb str = 
    1.24 -    if String.isPrefix  "List.op @." str
    1.25 -    then  ((String.substring(str,0,5)) ^ (String.extract (str, 10, NONE)))
    1.26 -    else str;
    1.27 -
    1.28 -(*FIXME: this logic (especially concat_with_stop) needs to be replaced by code
    1.29 -to invert the function ascii_of.*)
    1.30 -fun remove_spaces str = 
    1.31 -    let val strlist = String.tokens Char.isSpace str
    1.32 -	val spaceless = concat strlist
    1.33 -	val strlist' = String.tokens Char.isPunct spaceless
    1.34 -    in
    1.35 -	concat_with_stop strlist'
    1.36 -    end
    1.37 -
    1.38 -fun remove_symb_pair (str, thm) = (remove_symb str, thm);
    1.39 -
    1.40 -fun remove_spaces_pair (str, thm) = (remove_spaces str, thm);
    1.41 -
    1.42 -
    1.43  (*Insert th into the result provided the name is not "".*)
    1.44  fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths;
    1.45  
    1.46 @@ -187,16 +164,10 @@
    1.47  fun clause_numbering ((clause, theorem), cls) = 
    1.48      let val num_of_cls = length cls
    1.49  	val numbers = 0 upto (num_of_cls -1)
    1.50 -	val multi_name = multi (clause, theorem)  num_of_cls []
    1.51      in 
    1.52 -	(multi_name)
    1.53 +	multi (clause, theorem)  num_of_cls []
    1.54      end;
    1.55 -
    1.56 -
    1.57 -fun concat_with sep []  = ""
    1.58 -  | concat_with sep [x] = "(" ^ x ^ ")"
    1.59 -  | concat_with sep (x::xs) = "(" ^ x ^ ")" ^  sep ^ (concat_with sep xs);
    1.60 -
    1.61 +    
    1.62  
    1.63  (*Write out the claset and simpset rules of the supplied theory.
    1.64    FIXME: argument "goal" is a hack to allow relevance filtering.
    1.65 @@ -211,17 +182,12 @@
    1.66  	val simpset_rules =
    1.67  	      ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.68                  (ResAxioms.simpset_rules_of_thy thy);
    1.69 -	val named_simpset = 
    1.70 -	      map remove_spaces_pair (map put_name_pair simpset_rules)
    1.71 -        val justnames = map #1 named_simpset
    1.72 -        val namestring = concat_with "\n" justnames
    1.73 -        val _ = File.append (File.tmp_path (Path.basic "clasimp_names"))
    1.74 -			  (namestring)
    1.75 +	val named_simpset = map put_name_pair simpset_rules
    1.76  	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    1.77  
    1.78 -	val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) else claset_cls_thms;
    1.79 +	val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) 
    1.80 +	               else claset_cls_thms;
    1.81  	val cls_thms_list = List.concat cls_thms;
    1.82 -        (* length 1429 *)
    1.83  	(*************************************************)
    1.84  	(* Write out clauses as tptp strings to filename *)
    1.85  	(*************************************************)
    1.86 @@ -239,10 +205,8 @@
    1.87  
    1.88  	(* list of lists of tptp string clauses *)
    1.89  	val stick_clasrls =   List.concat cls_tptp_strs;
    1.90 -        (* length 1581*)
    1.91  	val out = TextIO.openOut filename;
    1.92  	val _=   ResLib.writeln_strs out stick_clasrls;
    1.93 -	val _= TextIO.flushOut out;
    1.94  	val _= TextIO.closeOut out
    1.95    in
    1.96  	(clause_arr, num_of_clauses, clauses)