src/HOL/Tools/ATP/res_clasimpset.ML
author paulson
Tue May 24 10:23:24 2005 +0200 (2005-05-24)
changeset 16061 8a139c1557bf
parent 16039 dfe264950511
child 16156 2f6fc19aba1e
permissions -rw-r--r--
A new structure and reduced indentation
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@15919
     8
signature RES_CLASIMP =
quigley@15919
     9
  sig
quigley@15919
    10
     val write_out_clasimp :string -> (ResClause.clause * Thm.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
paulson@15956
    53
paulson@16061
    54
fun write_out_clasimp filename = 
paulson@16061
    55
    let val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
paulson@16061
    56
	val named_claset = List.filter has_name_pair claset_rules;
paulson@16061
    57
	val claset_names = map remove_spaces_pair (named_claset)
paulson@16061
    58
	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
quigley@15643
    59
paulson@16061
    60
	val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
paulson@16061
    61
	val named_simpset = 
paulson@16061
    62
	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
paulson@16061
    63
	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
quigley@15643
    64
paulson@16061
    65
	val cls_thms = (claset_cls_thms@simpset_cls_thms);
paulson@16061
    66
	val cls_thms_list = List.concat cls_thms;
quigley@15643
    67
paulson@16061
    68
	(*********************************************************)
paulson@16061
    69
	(* create array and put clausename, number pairs into it *)
paulson@16061
    70
	(*********************************************************)
paulson@16061
    71
	val num_of_clauses =  0;
paulson@16061
    72
	val clause_arr = Array.fromList cls_thms_list;
paulson@16061
    73
paulson@16061
    74
	val num_of_clauses = List.length cls_thms_list;
quigley@15782
    75
paulson@16061
    76
	(*************************************************)
paulson@16061
    77
	(* Write out clauses as tptp strings to filename *)
paulson@16061
    78
	(*************************************************)
paulson@16061
    79
	val clauses = map #1(cls_thms_list);
paulson@16061
    80
	val cls_tptp_strs = map ResClause.tptp_clause clauses;
paulson@16061
    81
	(* list of lists of tptp string clauses *)
paulson@16061
    82
	val stick_clasrls =   List.concat cls_tptp_strs;
paulson@16061
    83
	val out = TextIO.openOut filename;
paulson@16061
    84
	val _=   ResLib.writeln_strs out stick_clasrls;
paulson@16061
    85
	val _= TextIO.flushOut out;
paulson@16061
    86
	val _= TextIO.closeOut out
paulson@16061
    87
  in
paulson@16061
    88
	(clause_arr, num_of_clauses)
paulson@16061
    89
  end;
quigley@15643
    90
quigley@15643
    91
quigley@15919
    92
end;
quigley@16039
    93