19 |
21 |
20 |
22 |
21 |
23 |
22 val num_of_clauses = ref 0; |
24 val num_of_clauses = ref 0; |
23 val clause_arr = Array.array(3500, ("empty", 0)); |
25 val clause_arr = Array.array(3500, ("empty", 0)); |
|
26 |
|
27 |
|
28 val foo_arr = Array.array(20, ("a",0)); |
|
29 |
|
30 |
|
31 (* |
|
32 |
|
33 fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)]; |
|
34 |
|
35 |
|
36 |
|
37 |
|
38 fun setupFork () = let |
|
39 (** pipes for communication between parent and watcher **) |
|
40 val p1 = Posix.IO.pipe () |
|
41 val p2 = Posix.IO.pipe () |
|
42 fun closep () = ( |
|
43 Posix.IO.close (#outfd p1); |
|
44 Posix.IO.close (#infd p1); |
|
45 Posix.IO.close (#outfd p2); |
|
46 Posix.IO.close (#infd p2) |
|
47 ) |
|
48 (***********************************************************) |
|
49 (****** fork a watcher process and get it set up and going *) |
|
50 (***********************************************************) |
|
51 fun startFork () = |
|
52 (case Posix.Process.fork() (***************************************) |
|
53 of SOME pid => pid (* parent - i.e. main Isabelle process *) |
|
54 (***************************************) |
|
55 |
|
56 (*************************) |
|
57 | NONE => let (* child - i.e. watcher *) |
|
58 val oldchildin = #infd p1 (*************************) |
|
59 val fromParent = Posix.FileSys.wordToFD 0w0 |
|
60 val oldchildout = #outfd p2 |
|
61 val toParent = Posix.FileSys.wordToFD 0w1 |
|
62 val fromParentIOD = Posix.FileSys.fdToIOD fromParent |
|
63 val fromParentStr = openInFD ("_exec_in_parent", fromParent) |
|
64 val toParentStr = openOutFD ("_exec_out_parent", toParent) |
|
65 val fooax = fst(Array.sub(foo_arr, 3)) |
|
66 val outfile = TextIO.openOut("/homes/clq20/Jia_Code/fork"); |
|
67 val _ = TextIO.output (outfile, ("fooax 3 is: "^fooax)) |
|
68 val _ = TextIO.closeOut outfile |
|
69 in |
|
70 (***************************) |
|
71 (*** Sort out pipes ********) |
|
72 (***************************) |
|
73 |
|
74 Posix.IO.close (#outfd p1); |
|
75 Posix.IO.close (#infd p2); |
|
76 Posix.IO.dup2{old = oldchildin, new = fromParent}; |
|
77 Posix.IO.close oldchildin; |
|
78 Posix.IO.dup2{old = oldchildout, new = toParent}; |
|
79 Posix.IO.close oldchildout; |
|
80 |
|
81 (***************************) |
|
82 (* start the watcher loop *) |
|
83 (***************************) |
|
84 |
|
85 (****************************************************************************) |
|
86 (* fake return value - actually want the watcher to loop until killed *) |
|
87 (****************************************************************************) |
|
88 Posix.Process.wordToPid 0w0 |
|
89 |
|
90 end) |
|
91 val start = startFork() |
|
92 in |
|
93 |
|
94 |
|
95 (*******************************) |
|
96 (* close the child-side fds *) |
|
97 (*******************************) |
|
98 Posix.IO.close (#outfd p2); |
|
99 Posix.IO.close (#infd p1); |
|
100 (* set the fds close on exec *) |
|
101 Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
102 Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
103 |
|
104 (*******************************) |
|
105 (* return value *) |
|
106 (*******************************) |
|
107 () |
|
108 end; |
|
109 |
|
110 |
|
111 |
|
112 *) |
|
113 |
24 |
114 |
25 |
115 |
26 |
116 |
27 fun multi x 0 xlist = xlist |
117 fun multi x 0 xlist = xlist |
28 |multi x n xlist = multi x (n -1 ) (x::xlist); |
118 |multi x n xlist = multi x (n -1 ) (x::xlist); |
89 (* re-jig all these later as smaller functions for each bit *) |
179 (* re-jig all these later as smaller functions for each bit *) |
90 val num_of_clauses = ref 0; |
180 val num_of_clauses = ref 0; |
91 val clause_arr = Array.array(3500, ("empty", 0)); |
181 val clause_arr = Array.array(3500, ("empty", 0)); |
92 |
182 |
93 |
183 |
94 fun write_out_clasimp filename = let |
184 fun write_out_clasimp filename (clause_arr:(string * int) Array.array) = let |
|
185 val outfile = TextIO.openOut("wibble"); val _ = TextIO.output (outfile, ("in write_out_clasimpset")) |
|
186 val _ = TextIO.closeOut outfile |
|
187 val _= (warning ("in writeoutclasimp")) |
95 (****************************************) |
188 (****************************************) |
96 (* add claset rules to array and write out as strings *) |
189 (* add claset rules to array and write out as strings *) |
97 (****************************************) |
190 (****************************************) |
98 val claset_rules = ResAxioms.claset_rules_of_thy (the_context()) |
191 val claset_rules = ResAxioms.claset_rules_of_thy (the_context()) |
99 val claset = ResAxioms.clausify_classical_rules_thy (the_context()) |
192 val claset = ResAxioms.clausify_classical_rules_thy (the_context()) |
125 val cl_long_name_nums = stick cl_name_nums; |
218 val cl_long_name_nums = stick cl_name_nums; |
126 (*******************************************) |
219 (*******************************************) |
127 (* create array and put clausename, number pairs into it *) |
220 (* create array and put clausename, number pairs into it *) |
128 (*******************************************) |
221 (*******************************************) |
129 |
222 |
130 val _ = fill_cls_array clause_arr 1 cl_long_name_nums; |
223 val _ = fill_cls_array clause_arr 1 cl_long_name_nums; |
131 |
|
132 |
|
133 val _= num_of_clauses := (List.length cl_long_name_nums); |
224 val _= num_of_clauses := (List.length cl_long_name_nums); |
134 |
225 |
135 (*************************************) |
226 (*************************************) |
136 (* write claset out as tptp file *) |
227 (* write claset out as tptp file *) |
137 (*************************************) |
228 (*************************************) |
145 (*val _= TextIO.closeOut out;*) |
236 (*val _= TextIO.closeOut out;*) |
146 |
237 |
147 (*********************) |
238 (*********************) |
148 (* Get simpset rules *) |
239 (* Get simpset rules *) |
149 (*********************) |
240 (*********************) |
|
241 |
150 val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context()); |
242 val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context()); |
|
243 |
151 val named_simps = List.filter has_name_pair simpset_name_rules; |
244 val named_simps = List.filter has_name_pair simpset_name_rules; |
152 |
245 |
153 val simp_names = map #1 named_simps; |
246 val simp_names = map #1 named_simps; |
154 val simp_rules = map #2 named_simps; |
247 val simp_rules = map #2 named_simps; |
155 |
248 |