src/HOL/Tools/ATP/res_clasimpset.ML
author quigley
Fri Jun 10 16:15:36 2005 +0200 (2005-06-10)
changeset 16357 f1275d2a1dee
parent 16172 629ba53a072f
child 16741 7a6c17b826c0
permissions -rw-r--r--
All subgoals sent to the watcher at once now.
Rules added to parser for Spass proofs.
If parsing or translation fails on a proof, the Spass proof is printed out in PG.
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@16357
    11
val write_out_clasimp_small :string -> theory -> (ResClause.clause * thm) Array.array * int
quigley@15919
    12
  end;
quigley@15919
    13
quigley@15919
    14
structure ResClasimp : RES_CLASIMP =
quigley@15919
    15
struct
quigley@15643
    16
paulson@16061
    17
fun has_name th = ((Thm.name_of_thm th)  <>  "")
paulson@16061
    18
paulson@16061
    19
fun has_name_pair (a,b) = (a <> "");
quigley@16039
    20
quigley@16039
    21
quigley@15919
    22
(* changed, now it also finds out the name of the theorem. *)
quigley@15919
    23
(* convert a theorem into CNF and then into Clause.clause format. *)
quigley@16039
    24
quigley@16039
    25
(* outputs a list of (thm,clause) pairs *)
quigley@15643
    26
quigley@15643
    27
quigley@16039
    28
(* for tracing: encloses each string element in brackets. *)
quigley@16039
    29
fun concat_with_stop [] = ""
quigley@16039
    30
  | concat_with_stop [x] =  x
quigley@16039
    31
  | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs;
quigley@16039
    32
paulson@16061
    33
fun remove_symb str = 
paulson@16061
    34
    if String.isPrefix  "List.op @." str
paulson@16061
    35
    then  ((String.substring(str,0,5)) ^ (String.extract (str, 10, NONE)))
paulson@16061
    36
    else str;
quigley@16039
    37
paulson@16061
    38
fun remove_spaces str = 
paulson@16061
    39
    let val strlist = String.tokens Char.isSpace str
paulson@16061
    40
	val spaceless = concat strlist
paulson@16061
    41
	val strlist' = String.tokens Char.isPunct spaceless
paulson@16061
    42
    in
paulson@16061
    43
	concat_with_stop strlist'
paulson@16061
    44
    end
quigley@16039
    45
paulson@16061
    46
fun remove_symb_pair (str, thm) = (remove_symb str, thm);
quigley@16039
    47
paulson@16061
    48
fun remove_spaces_pair (str, thm) = (remove_spaces str, thm);
quigley@15643
    49
paulson@15956
    50
paulson@15956
    51
(*Insert th into the result provided the name is not "".*)
paulson@15956
    52
fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths;
paulson@15956
    53
quigley@16156
    54
fun posinlist x [] n = "not in list"
quigley@16156
    55
|   posinlist x (y::ys) n = if (x=y) 
quigley@16156
    56
			    then
quigley@16156
    57
 				string_of_int n
quigley@16156
    58
			    else posinlist x (ys) (n+1)
quigley@16156
    59
quigley@16156
    60
quigley@16156
    61
fun pairup [] [] = []
quigley@16156
    62
|   pairup (x::xs) (y::ys) = (x,y)::(pairup xs ys)
quigley@16156
    63
quigley@16156
    64
fun multi x 0 xlist = xlist
quigley@16156
    65
   |multi x n xlist = multi x (n -1 ) (x::xlist);
quigley@16156
    66
paulson@16172
    67
fun clause_numbering ((clause, theorem), cls) = 
paulson@16172
    68
    let val num_of_cls = length cls
paulson@16172
    69
	val numbers = 0 upto (num_of_cls -1)
paulson@16172
    70
	val multi_name = multi (clause, theorem)  num_of_cls []
paulson@16172
    71
    in 
paulson@16172
    72
	(multi_name)
paulson@16172
    73
    end;
quigley@16156
    74
paulson@16172
    75
(*Write out the claset and simpset rules of the supplied theory.*)
paulson@16172
    76
fun write_out_clasimp filename thy = 
paulson@16172
    77
    let val claset_rules = ResAxioms.claset_rules_of_thy thy;
paulson@16061
    78
	val named_claset = List.filter has_name_pair claset_rules;
paulson@16061
    79
	val claset_names = map remove_spaces_pair (named_claset)
paulson@16061
    80
	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
quigley@15643
    81
paulson@16172
    82
	val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
paulson@16061
    83
	val named_simpset = 
paulson@16061
    84
	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
paulson@16061
    85
	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
quigley@15643
    86
paulson@16061
    87
	val cls_thms = (claset_cls_thms@simpset_cls_thms);
paulson@16061
    88
	val cls_thms_list = List.concat cls_thms;
quigley@16156
    89
        (* length 1429 *)
paulson@16061
    90
	(*************************************************)
paulson@16061
    91
	(* Write out clauses as tptp strings to filename *)
paulson@16061
    92
	(*************************************************)
paulson@16061
    93
	val clauses = map #1(cls_thms_list);
paulson@16061
    94
	val cls_tptp_strs = map ResClause.tptp_clause clauses;
quigley@16156
    95
        val alllist = pairup cls_thms_list cls_tptp_strs
quigley@16156
    96
        val whole_list = List.concat (map clause_numbering alllist);
quigley@16156
    97
 
quigley@16156
    98
        (*********************************************************)
quigley@16156
    99
	(* create array and put clausename, number pairs into it *)
quigley@16156
   100
	(*********************************************************)
quigley@16156
   101
	val num_of_clauses =  0;
quigley@16156
   102
	val clause_arr = Array.fromList whole_list;
quigley@16156
   103
	val num_of_clauses = List.length whole_list;
quigley@16156
   104
paulson@16061
   105
	(* list of lists of tptp string clauses *)
paulson@16061
   106
	val stick_clasrls =   List.concat cls_tptp_strs;
quigley@16156
   107
        (* length 1581*)
paulson@16061
   108
	val out = TextIO.openOut filename;
paulson@16061
   109
	val _=   ResLib.writeln_strs out stick_clasrls;
paulson@16061
   110
	val _= TextIO.flushOut out;
paulson@16061
   111
	val _= TextIO.closeOut out
paulson@16061
   112
  in
paulson@16061
   113
	(clause_arr, num_of_clauses)
paulson@16061
   114
  end;
quigley@15643
   115
quigley@16357
   116
quigley@16357
   117
quigley@16357
   118
quigley@16357
   119
quigley@16357
   120
(*Write out the claset and simpset rules of the supplied theory. Only include the first 50 rules*)
quigley@16357
   121
fun write_out_clasimp_small filename thy = 
quigley@16357
   122
    let val claset_rules = ResAxioms.claset_rules_of_thy thy;
quigley@16357
   123
	val named_claset = List.filter has_name_pair claset_rules;
quigley@16357
   124
	val claset_names = map remove_spaces_pair (named_claset)
quigley@16357
   125
	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
quigley@16357
   126
quigley@16357
   127
	val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
quigley@16357
   128
	val named_simpset = 
quigley@16357
   129
	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
quigley@16357
   130
	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
quigley@16357
   131
quigley@16357
   132
	val cls_thms = (claset_cls_thms@simpset_cls_thms);
quigley@16357
   133
	val cls_thms_list = List.concat cls_thms;
quigley@16357
   134
        (* length 1429 *)
quigley@16357
   135
	(*************************************************)
quigley@16357
   136
	(* Write out clauses as tptp strings to filename *)
quigley@16357
   137
	(*************************************************)
quigley@16357
   138
	val clauses = map #1(cls_thms_list);
quigley@16357
   139
	val cls_tptp_strs = map ResClause.tptp_clause clauses;
quigley@16357
   140
        val alllist = pairup cls_thms_list cls_tptp_strs
quigley@16357
   141
        val whole_list = List.concat (map clause_numbering alllist);
quigley@16357
   142
        val mini_list = List.take ( whole_list,50)
quigley@16357
   143
        (*********************************************************)
quigley@16357
   144
	(* create array and put clausename, number pairs into it *)
quigley@16357
   145
	(*********************************************************)
quigley@16357
   146
	val num_of_clauses =  0;
quigley@16357
   147
	val clause_arr = Array.fromList mini_list;
quigley@16357
   148
	val num_of_clauses = List.length mini_list;
quigley@16357
   149
quigley@16357
   150
	(* list of lists of tptp string clauses *)
quigley@16357
   151
	val stick_clasrls =   List.concat cls_tptp_strs;
quigley@16357
   152
        (* length 1581*)
quigley@16357
   153
	val out = TextIO.openOut filename;
quigley@16357
   154
	val _=   ResLib.writeln_strs out (List.take (stick_clasrls,50));
quigley@16357
   155
	val _= TextIO.flushOut out;
quigley@16357
   156
	val _= TextIO.closeOut out
quigley@16357
   157
  in
quigley@16357
   158
	(clause_arr, num_of_clauses)
quigley@16357
   159
  end;
quigley@16357
   160
quigley@16357
   161
quigley@16357
   162
quigley@15919
   163
end;
quigley@16039
   164
quigley@16156
   165
quigley@16156
   166