src/HOL/Tools/ATP/res_clasimpset.ML
author paulson
Wed Jun 01 14:50:48 2005 +0200 (2005-06-01)
changeset 16172 629ba53a072f
parent 16156 2f6fc19aba1e
child 16357 f1275d2a1dee
permissions -rw-r--r--
small tweaks; also now write_out_clasimp takes the current theory as argument
quigley@16039
     1
paulson@15789
     2
(*  ID:         $Id$
quigley@16039
     3
paulson@15789
     4
    Author:     Claire Quigley
paulson@15789
     5
    Copyright   2004  University of Cambridge
paulson@15789
     6
*)
paulson@15789
     7
quigley@16156
     8
signature RES_CLASIMP = 
quigley@15919
     9
  sig
paulson@16172
    10
     val write_out_clasimp :string -> theory -> (ResClause.clause * thm) Array.array * int
quigley@15919
    11
  end;
quigley@15919
    12
quigley@15919
    13
structure ResClasimp : RES_CLASIMP =
quigley@15919
    14
struct
quigley@15643
    15
paulson@16061
    16
fun has_name th = ((Thm.name_of_thm th)  <>  "")
paulson@16061
    17
paulson@16061
    18
fun has_name_pair (a,b) = (a <> "");
quigley@16039
    19
quigley@16039
    20
quigley@15919
    21
(* changed, now it also finds out the name of the theorem. *)
quigley@15919
    22
(* convert a theorem into CNF and then into Clause.clause format. *)
quigley@16039
    23
quigley@16039
    24
(* outputs a list of (thm,clause) pairs *)
quigley@15643
    25
quigley@15643
    26
quigley@16039
    27
(* for tracing: encloses each string element in brackets. *)
quigley@16039
    28
fun concat_with_stop [] = ""
quigley@16039
    29
  | concat_with_stop [x] =  x
quigley@16039
    30
  | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs;
quigley@16039
    31
paulson@16061
    32
fun remove_symb str = 
paulson@16061
    33
    if String.isPrefix  "List.op @." str
paulson@16061
    34
    then  ((String.substring(str,0,5)) ^ (String.extract (str, 10, NONE)))
paulson@16061
    35
    else str;
quigley@16039
    36
paulson@16061
    37
fun remove_spaces str = 
paulson@16061
    38
    let val strlist = String.tokens Char.isSpace str
paulson@16061
    39
	val spaceless = concat strlist
paulson@16061
    40
	val strlist' = String.tokens Char.isPunct spaceless
paulson@16061
    41
    in
paulson@16061
    42
	concat_with_stop strlist'
paulson@16061
    43
    end
quigley@16039
    44
paulson@16061
    45
fun remove_symb_pair (str, thm) = (remove_symb str, thm);
quigley@16039
    46
paulson@16061
    47
fun remove_spaces_pair (str, thm) = (remove_spaces str, thm);
quigley@15643
    48
paulson@15956
    49
paulson@15956
    50
(*Insert th into the result provided the name is not "".*)
paulson@15956
    51
fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths;
paulson@15956
    52
quigley@16156
    53
fun posinlist x [] n = "not in list"
quigley@16156
    54
|   posinlist x (y::ys) n = if (x=y) 
quigley@16156
    55
			    then
quigley@16156
    56
 				string_of_int n
quigley@16156
    57
			    else posinlist x (ys) (n+1)
quigley@16156
    58
quigley@16156
    59
quigley@16156
    60
fun pairup [] [] = []
quigley@16156
    61
|   pairup (x::xs) (y::ys) = (x,y)::(pairup xs ys)
quigley@16156
    62
quigley@16156
    63
fun multi x 0 xlist = xlist
quigley@16156
    64
   |multi x n xlist = multi x (n -1 ) (x::xlist);
quigley@16156
    65
paulson@16172
    66
fun clause_numbering ((clause, theorem), cls) = 
paulson@16172
    67
    let val num_of_cls = length cls
paulson@16172
    68
	val numbers = 0 upto (num_of_cls -1)
paulson@16172
    69
	val multi_name = multi (clause, theorem)  num_of_cls []
paulson@16172
    70
    in 
paulson@16172
    71
	(multi_name)
paulson@16172
    72
    end;
quigley@16156
    73
paulson@16172
    74
(*Write out the claset and simpset rules of the supplied theory.*)
paulson@16172
    75
fun write_out_clasimp filename thy = 
paulson@16172
    76
    let val claset_rules = ResAxioms.claset_rules_of_thy thy;
paulson@16061
    77
	val named_claset = List.filter has_name_pair claset_rules;
paulson@16061
    78
	val claset_names = map remove_spaces_pair (named_claset)
paulson@16061
    79
	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
quigley@15643
    80
paulson@16172
    81
	val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
paulson@16061
    82
	val named_simpset = 
paulson@16061
    83
	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
paulson@16061
    84
	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
quigley@15643
    85
paulson@16061
    86
	val cls_thms = (claset_cls_thms@simpset_cls_thms);
paulson@16061
    87
	val cls_thms_list = List.concat cls_thms;
quigley@16156
    88
        (* length 1429 *)
paulson@16061
    89
	(*************************************************)
paulson@16061
    90
	(* Write out clauses as tptp strings to filename *)
paulson@16061
    91
	(*************************************************)
paulson@16061
    92
	val clauses = map #1(cls_thms_list);
paulson@16061
    93
	val cls_tptp_strs = map ResClause.tptp_clause clauses;
quigley@16156
    94
        val alllist = pairup cls_thms_list cls_tptp_strs
quigley@16156
    95
        val whole_list = List.concat (map clause_numbering alllist);
quigley@16156
    96
 
quigley@16156
    97
        (*********************************************************)
quigley@16156
    98
	(* create array and put clausename, number pairs into it *)
quigley@16156
    99
	(*********************************************************)
quigley@16156
   100
	val num_of_clauses =  0;
quigley@16156
   101
	val clause_arr = Array.fromList whole_list;
quigley@16156
   102
	val num_of_clauses = List.length whole_list;
quigley@16156
   103
paulson@16061
   104
	(* list of lists of tptp string clauses *)
paulson@16061
   105
	val stick_clasrls =   List.concat cls_tptp_strs;
quigley@16156
   106
        (* length 1581*)
paulson@16061
   107
	val out = TextIO.openOut filename;
paulson@16061
   108
	val _=   ResLib.writeln_strs out stick_clasrls;
paulson@16061
   109
	val _= TextIO.flushOut out;
paulson@16061
   110
	val _= TextIO.closeOut out
paulson@16061
   111
  in
paulson@16061
   112
	(clause_arr, num_of_clauses)
paulson@16061
   113
  end;
quigley@15643
   114
quigley@15919
   115
end;
quigley@16039
   116
quigley@16156
   117
quigley@16156
   118