author | quigley |
Mon, 23 May 2005 00:18:51 +0200 | |
changeset 16039 | dfe264950511 |
parent 15956 | 0da64b5a9a00 |
child 16061 | 8a139c1557bf |
permissions | -rw-r--r-- |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
1 |
|
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
2 |
(* ID: $Id$ |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
3 |
|
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
4 |
Author: Claire Quigley |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
5 |
Copyright 2004 University of Cambridge |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
6 |
*) |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
7 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
8 |
signature RES_CLASIMP = |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
9 |
sig |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
10 |
val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
11 |
end; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
12 |
|
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
13 |
structure ResClasimp : RES_CLASIMP = |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
14 |
struct |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
15 |
fun has_name th = not((Thm.name_of_thm th )= "") |
15643 | 16 |
fun has_name_pair (a,b) = not_equal a ""; |
17 |
||
18 |
fun stick [] = [] |
|
19 |
| stick (x::xs) = x@(stick xs ) |
|
20 |
||
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
21 |
fun filterlist p [] = [] |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
22 |
| filterlist p (x::xs) = if p x |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
23 |
then |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
24 |
(x::(filterlist p xs)) |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
25 |
else |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
26 |
filterlist p xs |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
27 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
28 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
29 |
(* changed, now it also finds out the name of the theorem. *) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
30 |
(* convert a theorem into CNF and then into Clause.clause format. *) |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
31 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
32 |
(* outputs a list of (thm,clause) pairs *) |
15643 | 33 |
|
34 |
||
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
35 |
(* for tracing: encloses each string element in brackets. *) |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
36 |
fun concat_with_stop [] = "" |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
37 |
| concat_with_stop [x] = x |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
38 |
| concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs; |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
39 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
40 |
fun remove_symb str = if String.isPrefix "List.op @." str |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
41 |
then |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
42 |
((String.substring(str,0,5))^(String.extract (str, 10, NONE))) |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
43 |
else |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
44 |
str |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
45 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
46 |
fun remove_spaces str = let val strlist = String.tokens Char.isSpace str |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
47 |
val spaceless = concat strlist |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
48 |
val strlist' = String.tokens Char.isPunct spaceless |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
49 |
in |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
50 |
concat_with_stop strlist' |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
51 |
end |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
52 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
53 |
fun remove_symb_pair (str, thm) = let val newstr = remove_symb str |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
54 |
in |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
55 |
(newstr, thm) |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
56 |
end |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
57 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
58 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
59 |
fun remove_spaces_pair (str, thm) = let val newstr = remove_spaces str |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
60 |
in |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
61 |
(newstr, thm) |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
62 |
end |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
63 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
64 |
|
15643 | 65 |
|
15956 | 66 |
|
67 |
(*Insert th into the result provided the name is not "".*) |
|
68 |
fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths; |
|
69 |
||
70 |
||
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
71 |
fun write_out_clasimp filename = let |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
72 |
val claset_rules = ResAxioms.claset_rules_of_thy (the_context()); |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
73 |
val named_claset = filterlist has_name_pair claset_rules; |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
74 |
val claset_names = map remove_spaces_pair (named_claset) |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
75 |
val claset_cls_thms = #1( ResAxioms.clausify_rules_pairs named_claset []); |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
76 |
|
15643 | 77 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
78 |
val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context()); |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
79 |
val named_simpset = map remove_spaces_pair (filterlist has_name_pair simpset_rules); |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
80 |
val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []); |
15643 | 81 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
82 |
val cls_thms = (claset_cls_thms@simpset_cls_thms); |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
83 |
val cls_thms_list = stick cls_thms; |
15643 | 84 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
85 |
(*********************************************************) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
86 |
(* create array and put clausename, number pairs into it *) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
87 |
(*********************************************************) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
88 |
val num_of_clauses = 0; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
89 |
val clause_arr = Array.fromList cls_thms_list; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
90 |
|
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
91 |
val num_of_clauses= (List.length cls_thms_list); |
15782 | 92 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
93 |
(*************************************************) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
94 |
(* Write out clauses as tptp strings to filename *) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
95 |
(*************************************************) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
96 |
val clauses = map #1(cls_thms_list); |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
97 |
val cls_tptp_strs = map ResClause.tptp_clause clauses; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
98 |
(* list of lists of tptp string clauses *) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
99 |
val stick_clasrls = stick cls_tptp_strs; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
100 |
val out = TextIO.openOut filename; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
101 |
val _= ResLib.writeln_strs out stick_clasrls; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
102 |
val _= TextIO.flushOut out; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
103 |
val _= TextIO.closeOut out |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
104 |
in |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
105 |
(clause_arr, num_of_clauses) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
106 |
end; |
15643 | 107 |
|
108 |
||
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
109 |
end; |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
110 |