1 (* ID: $Id$ |
1 (* ID: $Id$ |
2 Author: Claire Quigley |
2 Author: Claire Quigley |
3 Copyright 2004 University of Cambridge |
3 Copyright 2004 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 (* Get claset rules *) |
6 signature RES_CLASIMP = |
|
7 sig |
|
8 val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int |
|
9 end; |
|
10 |
|
11 structure ResClasimp : RES_CLASIMP = |
|
12 struct |
7 |
13 |
8 fun has_name th = not((Thm.name_of_thm th)= "") |
14 fun has_name th = not((Thm.name_of_thm th)= "") |
9 |
15 |
10 fun has_name_pair (a,b) = not_equal a ""; |
16 fun has_name_pair (a,b) = not_equal a ""; |
11 fun good_pair c (a,b) = not_equal b c; |
|
12 |
|
13 |
|
14 |
|
15 val num_of_clauses = ref 0; |
|
16 val clause_arr = Array.array(3500, ("empty", 0)); |
|
17 |
|
18 |
|
19 (* |
|
20 val foo_arr = Array.array(20, ("a",0)); |
|
21 |
|
22 fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)]; |
|
23 |
|
24 |
|
25 |
|
26 |
|
27 fun setupFork () = let |
|
28 (** pipes for communication between parent and watcher **) |
|
29 val p1 = Posix.IO.pipe () |
|
30 val p2 = Posix.IO.pipe () |
|
31 fun closep () = ( |
|
32 Posix.IO.close (#outfd p1); |
|
33 Posix.IO.close (#infd p1); |
|
34 Posix.IO.close (#outfd p2); |
|
35 Posix.IO.close (#infd p2) |
|
36 ) |
|
37 (***********************************************************) |
|
38 (****** fork a watcher process and get it set up and going *) |
|
39 (***********************************************************) |
|
40 fun startFork () = |
|
41 (case Posix.Process.fork() (***************************************) |
|
42 of SOME pid => pid (* parent - i.e. main Isabelle process *) |
|
43 (***************************************) |
|
44 |
|
45 (*************************) |
|
46 | NONE => let (* child - i.e. watcher *) |
|
47 val oldchildin = #infd p1 (*************************) |
|
48 val fromParent = Posix.FileSys.wordToFD 0w0 |
|
49 val oldchildout = #outfd p2 |
|
50 val toParent = Posix.FileSys.wordToFD 0w1 |
|
51 val fromParentIOD = Posix.FileSys.fdToIOD fromParent |
|
52 val fromParentStr = openInFD ("_exec_in_parent", fromParent) |
|
53 val toParentStr = openOutFD ("_exec_out_parent", toParent) |
|
54 val fooax = fst(Array.sub(foo_arr, 3)) |
|
55 val outfile = TextIO.openOut("/homes/clq20/Jia_Code/fork"); |
|
56 val _ = TextIO.output (outfile, ("fooax 3 is: "^fooax)) |
|
57 val _ = TextIO.closeOut outfile |
|
58 in |
|
59 (***************************) |
|
60 (*** Sort out pipes ********) |
|
61 (***************************) |
|
62 |
|
63 Posix.IO.close (#outfd p1); |
|
64 Posix.IO.close (#infd p2); |
|
65 Posix.IO.dup2{old = oldchildin, new = fromParent}; |
|
66 Posix.IO.close oldchildin; |
|
67 Posix.IO.dup2{old = oldchildout, new = toParent}; |
|
68 Posix.IO.close oldchildout; |
|
69 |
|
70 (***************************) |
|
71 (* start the watcher loop *) |
|
72 (***************************) |
|
73 |
|
74 (****************************************************************************) |
|
75 (* fake return value - actually want the watcher to loop until killed *) |
|
76 (****************************************************************************) |
|
77 Posix.Process.wordToPid 0w0 |
|
78 |
|
79 end) |
|
80 val start = startFork() |
|
81 in |
|
82 |
|
83 |
|
84 (*******************************) |
|
85 (* close the child-side fds *) |
|
86 (*******************************) |
|
87 Posix.IO.close (#outfd p2); |
|
88 Posix.IO.close (#infd p1); |
|
89 (* set the fds close on exec *) |
|
90 Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
91 Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
92 |
|
93 (*******************************) |
|
94 (* return value *) |
|
95 (*******************************) |
|
96 () |
|
97 end; |
|
98 |
|
99 |
|
100 |
|
101 *) |
|
102 |
|
103 |
|
104 |
|
105 |
|
106 fun multi x 0 xlist = xlist |
|
107 |multi x n xlist = multi x (n -1 ) (x::xlist); |
|
108 |
|
109 |
|
110 fun clause_numbering (name:string, cls) = let val num_of_cls = length cls |
|
111 val numbers = 0 upto (num_of_cls -1) |
|
112 val multi_name = multi name num_of_cls [] |
|
113 in |
|
114 ListPair.zip (multi_name,numbers) |
|
115 end; |
|
116 |
17 |
117 fun stick [] = [] |
18 fun stick [] = [] |
118 | stick (x::xs) = x@(stick xs ) |
19 | stick (x::xs) = x@(stick xs ) |
119 |
20 |
|
21 (* changed, now it also finds out the name of the theorem. *) |
|
22 (* convert a theorem into CNF and then into Clause.clause format. *) |
|
23 fun clausify_axiom_pairs thm = |
|
24 let val isa_clauses = ResAxioms.cnf_axiom thm (*"isa_clauses" are already "standard"ed. *) |
|
25 val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses |
|
26 val thm_name = Thm.name_of_thm thm |
|
27 val clauses_n = length isa_clauses |
|
28 fun make_axiom_clauses _ [] []= [] |
|
29 | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss' |
|
30 in |
|
31 make_axiom_clauses 0 isa_clauses' isa_clauses |
|
32 end; |
120 |
33 |
121 |
34 |
122 fun fill_cls_array array n [] = () |
35 fun clausify_rules_pairs [] err_list = ([],err_list) |
123 | fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x) |
36 | clausify_rules_pairs (thm::thms) err_list = |
124 in |
37 let val (ts,es) = clausify_rules_pairs thms err_list |
125 fill_cls_array array (n+1) (xs) |
38 in |
126 end; |
39 ((clausify_axiom_pairs thm)::ts,es) handle _ => (ts,(thm::es)) |
|
40 end; |
|
41 |
|
42 fun write_out_clasimp filename = let |
|
43 val claset_rules = ResAxioms.claset_rules_of_thy (the_context()); |
|
44 val named_claset = List.filter has_name claset_rules; |
|
45 val claset_cls_thms = #1( clausify_rules_pairs named_claset []); |
|
46 |
|
47 val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context()); |
|
48 val named_simpset = map #2(List.filter has_name_pair simpset_rules); |
|
49 val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []); |
|
50 |
|
51 val cls_thms = (claset_cls_thms@simpset_cls_thms); |
|
52 val cls_thms_list = stick cls_thms; |
|
53 |
|
54 (*********************************************************) |
|
55 (* create array and put clausename, number pairs into it *) |
|
56 (*********************************************************) |
|
57 val num_of_clauses = 0; |
|
58 val clause_arr = Array.fromList cls_thms_list; |
|
59 |
|
60 val num_of_clauses= (List.length cls_thms_list); |
|
61 |
|
62 (*************************************************) |
|
63 (* Write out clauses as tptp strings to filename *) |
|
64 (*************************************************) |
|
65 val clauses = map #1(cls_thms_list); |
|
66 val cls_tptp_strs = map ResClause.tptp_clause clauses; |
|
67 (* list of lists of tptp string clauses *) |
|
68 val stick_clasrls = stick cls_tptp_strs; |
|
69 val out = TextIO.openOut filename; |
|
70 val _= ResLib.writeln_strs out stick_clasrls; |
|
71 val _= TextIO.flushOut out; |
|
72 val _= TextIO.closeOut out |
|
73 in |
|
74 (clause_arr, num_of_clauses) |
|
75 end; |
127 |
76 |
128 |
77 |
129 |
78 end; |
130 val nc = ref (Symtab.empty : (thm list) Symtab.table) |
|
131 |
|
132 |
|
133 |
|
134 fun memo_add_clauses (name:string, cls)= |
|
135 nc := Symtab.update((name , cls), !nc); |
|
136 |
|
137 |
|
138 |
|
139 fun memo_find_clause name = case Symtab.lookup (!nc,name) of |
|
140 NONE => [] |
|
141 |SOME cls => cls ; |
|
142 |
|
143 |
|
144 fun get_simp_metas [] = [[]] |
|
145 | get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x |
|
146 in |
|
147 metas::(get_simp_metas xs) |
|
148 end |
|
149 handle THM _ => get_simp_metas xs |
|
150 |
|
151 |
|
152 (* re-jig all these later as smaller functions for each bit *) |
|
153 val num_of_clauses = ref 0; |
|
154 val clause_arr = Array.array(3500, ("empty", 0)); |
|
155 |
|
156 |
|
157 fun write_out_clasimp filename (clause_arr:(string * int) Array.array) = let |
|
158 val _= warning "in writeoutclasimp" |
|
159 (****************************************) |
|
160 (* add claset rules to array and write out as strings *) |
|
161 (****************************************) |
|
162 val clausifiable_rules = ResAxioms.claset_rules_of_thy (the_context()) |
|
163 val name_fol_cs = List.filter has_name clausifiable_rules; |
|
164 (* length name_fol_cs is 93 *) |
|
165 val good_names = map Thm.name_of_thm name_fol_cs; |
|
166 |
|
167 (*******************************************) |
|
168 (* get (name, thm) pairs for claset rules *) |
|
169 (*******************************************) |
|
170 |
|
171 val names_rules = ListPair.zip (good_names,name_fol_cs); |
|
172 |
|
173 val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[]) |
|
174 |
|
175 val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls; |
|
176 |
|
177 (* list of lists of tptp string clauses *) |
|
178 val stick_clasrls = map stick claset_tptp_strs; |
|
179 (* stick stick_clasrls length is 172*) |
|
180 |
|
181 val name_stick = ListPair.zip (good_names,stick_clasrls); |
|
182 |
|
183 val cl_name_nums =map clause_numbering name_stick; |
|
184 |
|
185 val cl_long_name_nums = stick cl_name_nums; |
|
186 (*******************************************) |
|
187 (* create array and put clausename, number pairs into it *) |
|
188 (*******************************************) |
|
189 |
|
190 val _ = fill_cls_array clause_arr 1 cl_long_name_nums; |
|
191 val _= num_of_clauses := (List.length cl_long_name_nums); |
|
192 |
|
193 (*************************************) |
|
194 (* write claset out as tptp file *) |
|
195 (*************************************) |
|
196 |
|
197 val claset_all_strs = stick stick_clasrls; |
|
198 val out = TextIO.openOut filename; |
|
199 val _= ResLib.writeln_strs out claset_all_strs; |
|
200 val _= TextIO.flushOut out; |
|
201 val _= TextIO.output (out,("\n \n")); |
|
202 val _= TextIO.flushOut out; |
|
203 (*val _= TextIO.closeOut out;*) |
|
204 |
|
205 (*********************) |
|
206 (* Get simpset rules *) |
|
207 (*********************) |
|
208 |
|
209 val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context()); |
|
210 |
|
211 val named_simps = List.filter has_name_pair simpset_name_rules; |
|
212 |
|
213 val simp_names = map #1 named_simps; |
|
214 val simp_rules = map #2 named_simps; |
|
215 |
|
216 (* 1137 clausif simps *) |
|
217 |
|
218 (* need to get names of claset_cluases so we can make sure we've*) |
|
219 (* got the same ones (ie. the named ones ) as the claset rules *) |
|
220 (* length 1374*) |
|
221 val new_simps = #1(ResAxioms.clausify_rules simp_rules []); |
|
222 val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps; |
|
223 |
|
224 val stick_strs = map stick simpset_tptp_strs; |
|
225 val name_stick = ListPair.zip (simp_names,stick_strs); |
|
226 |
|
227 val name_nums =map clause_numbering name_stick; |
|
228 (* length 2409*) |
|
229 val long_name_nums = stick name_nums; |
|
230 |
|
231 |
|
232 val _ =fill_cls_array clause_arr (!num_of_clauses + 1) long_name_nums; |
|
233 val _ =num_of_clauses := (!num_of_clauses) + (List.length long_name_nums); |
|
234 |
|
235 |
|
236 |
|
237 val tptplist = (stick stick_strs) |
|
238 |
|
239 in |
|
240 ResLib.writeln_strs out tptplist; |
|
241 TextIO.flushOut out; |
|
242 TextIO.closeOut out; |
|
243 clause_arr |
|
244 end; |
|
245 |
|
246 (* |
|
247 |
|
248 Array.sub(clause_arr, 2310); |
|
249 *) |
|