dead code removal
authorpaulson
Fri Jul 22 17:43:49 2005 +0200 (2005-07-22)
changeset 1690674eddde1de2f
parent 16905 fa26952fa7b6
child 16907 2187e3f94761
dead code removal
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jul 22 17:43:03 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jul 22 17:43:49 2005 +0200
     1.3 @@ -110,8 +110,6 @@
     1.4    val relevant : int ref
     1.5    val write_out_clasimp : string -> theory -> term -> 
     1.6                               (ResClause.clause * thm) Array.array * int
     1.7 -  val write_out_clasimp_small :
     1.8 -     string -> theory -> (ResClause.clause * thm) Array.array * int
     1.9    end;
    1.10  
    1.11  structure ResClasimp : RES_CLASIMP =
    1.12 @@ -179,7 +177,8 @@
    1.13      end;
    1.14  
    1.15  (*Write out the claset and simpset rules of the supplied theory.
    1.16 -  FIXME: argument "goal" is a hack to allow relevance filtering.*)
    1.17 +  FIXME: argument "goal" is a hack to allow relevance filtering.
    1.18 +  To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    1.19  fun write_out_clasimp filename thy goal = 
    1.20      let val claset_rules = 
    1.21                ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.22 @@ -223,53 +222,6 @@
    1.23  	(clause_arr, num_of_clauses)
    1.24    end;
    1.25  
    1.26 -
    1.27 -
    1.28 -
    1.29 -
    1.30 -(*Write out the claset and simpset rules of the supplied theory. Only include the first 50 rules*)
    1.31 -fun write_out_clasimp_small filename thy = 
    1.32 -    let val claset_rules = ResAxioms.claset_rules_of_thy thy;
    1.33 -	val named_claset = List.filter has_name_pair claset_rules;
    1.34 -	val claset_names = map remove_spaces_pair (named_claset)
    1.35 -	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
    1.36 -
    1.37 -	val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
    1.38 -	val named_simpset = 
    1.39 -	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
    1.40 -	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    1.41 -
    1.42 -	val cls_thms = (claset_cls_thms@simpset_cls_thms);
    1.43 -	val cls_thms_list = List.concat cls_thms;
    1.44 -        (* length 1429 *)
    1.45 -	(*************************************************)
    1.46 -	(* Write out clauses as tptp strings to filename *)
    1.47 -	(*************************************************)
    1.48 -	val clauses = map #1(cls_thms_list);
    1.49 -	val cls_tptp_strs = map ResClause.tptp_clause clauses;
    1.50 -        val alllist = pairup cls_thms_list cls_tptp_strs
    1.51 -        val whole_list = List.concat (map clause_numbering alllist);
    1.52 -        val mini_list = List.take ( whole_list,50)
    1.53 -        (*********************************************************)
    1.54 -	(* create array and put clausename, number pairs into it *)
    1.55 -	(*********************************************************)
    1.56 -	val num_of_clauses =  0;
    1.57 -	val clause_arr = Array.fromList mini_list;
    1.58 -	val num_of_clauses = List.length mini_list;
    1.59 -
    1.60 -	(* list of lists of tptp string clauses *)
    1.61 -	val stick_clasrls =   List.concat cls_tptp_strs;
    1.62 -        (* length 1581*)
    1.63 -	val out = TextIO.openOut filename;
    1.64 -	val _=   ResLib.writeln_strs out (List.take (stick_clasrls,50));
    1.65 -	val _= TextIO.flushOut out;
    1.66 -	val _= TextIO.closeOut out
    1.67 -  in
    1.68 -	(clause_arr, num_of_clauses)
    1.69 -  end;
    1.70 -
    1.71 -
    1.72 -
    1.73  end;
    1.74  
    1.75