src/HOL/Tools/ATP/res_clasimpset.ML
changeset 16357 f1275d2a1dee
parent 16172 629ba53a072f
child 16741 7a6c17b826c0
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Jun 09 23:33:28 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jun 10 16:15:36 2005 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  signature RES_CLASIMP = 
     1.5    sig
     1.6       val write_out_clasimp :string -> theory -> (ResClause.clause * thm) Array.array * int
     1.7 +val write_out_clasimp_small :string -> theory -> (ResClause.clause * thm) Array.array * int
     1.8    end;
     1.9  
    1.10  structure ResClasimp : RES_CLASIMP =
    1.11 @@ -112,6 +113,53 @@
    1.12  	(clause_arr, num_of_clauses)
    1.13    end;
    1.14  
    1.15 +
    1.16 +
    1.17 +
    1.18 +
    1.19 +(*Write out the claset and simpset rules of the supplied theory. Only include the first 50 rules*)
    1.20 +fun write_out_clasimp_small filename thy = 
    1.21 +    let val claset_rules = ResAxioms.claset_rules_of_thy thy;
    1.22 +	val named_claset = List.filter has_name_pair claset_rules;
    1.23 +	val claset_names = map remove_spaces_pair (named_claset)
    1.24 +	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
    1.25 +
    1.26 +	val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
    1.27 +	val named_simpset = 
    1.28 +	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
    1.29 +	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    1.30 +
    1.31 +	val cls_thms = (claset_cls_thms@simpset_cls_thms);
    1.32 +	val cls_thms_list = List.concat cls_thms;
    1.33 +        (* length 1429 *)
    1.34 +	(*************************************************)
    1.35 +	(* Write out clauses as tptp strings to filename *)
    1.36 +	(*************************************************)
    1.37 +	val clauses = map #1(cls_thms_list);
    1.38 +	val cls_tptp_strs = map ResClause.tptp_clause clauses;
    1.39 +        val alllist = pairup cls_thms_list cls_tptp_strs
    1.40 +        val whole_list = List.concat (map clause_numbering alllist);
    1.41 +        val mini_list = List.take ( whole_list,50)
    1.42 +        (*********************************************************)
    1.43 +	(* create array and put clausename, number pairs into it *)
    1.44 +	(*********************************************************)
    1.45 +	val num_of_clauses =  0;
    1.46 +	val clause_arr = Array.fromList mini_list;
    1.47 +	val num_of_clauses = List.length mini_list;
    1.48 +
    1.49 +	(* list of lists of tptp string clauses *)
    1.50 +	val stick_clasrls =   List.concat cls_tptp_strs;
    1.51 +        (* length 1581*)
    1.52 +	val out = TextIO.openOut filename;
    1.53 +	val _=   ResLib.writeln_strs out (List.take (stick_clasrls,50));
    1.54 +	val _= TextIO.flushOut out;
    1.55 +	val _= TextIO.closeOut out
    1.56 +  in
    1.57 +	(clause_arr, num_of_clauses)
    1.58 +  end;
    1.59 +
    1.60 +
    1.61 +
    1.62  end;
    1.63  
    1.64