Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* From the SML/NJ benchmark suite. *) |
2 | ||
3 | (* term.sml *) | |
4 | ||
5 | structure Term = | |
6 | struct | |
7 | datatype term | |
8 | = STR of string * term list | |
9 | | INT of int | |
10 | | CON of string | |
11 | | REF of term option ref | |
12 | ||
13 | exception BadArg of string | |
14 | end; | |
15 | ||
16 | (* trail.sml *) | |
17 | ||
18 | structure Trail = | |
19 | struct | |
20 | local | |
21 | open Term | |
22 | val global_trail = ref (nil : term option ref list) | |
23 | val trail_counter = ref 0 | |
24 | in | |
25 | fun unwind_trail (0, tr) = tr | |
26 | | unwind_trail (n, r::tr) = | |
27 | ( r := NONE ; unwind_trail (n-1, tr) ) | |
28 | | unwind_trail (_, nil) = | |
29 | raise BadArg "unwind_trail" | |
30 | ||
31 | fun reset_trail () = ( global_trail := nil ) | |
32 | ||
33 | fun trail func = | |
34 | let | |
35 | val tc0 = !trail_counter | |
36 | in | |
37 | ( func () ; | |
38 | global_trail := | |
39 | unwind_trail (!trail_counter-tc0, !global_trail) ; | |
40 | trail_counter := tc0 ) | |
41 | end | |
42 | ||
43 | fun bind (r, t) = | |
44 | ( r := SOME t ; | |
45 | global_trail := r::(!global_trail) ; | |
46 | trail_counter := !trail_counter+1 ) | |
47 | end (* local *) | |
48 | end; (* Trail *) | |
49 | ||
50 | (* unify.sml *) | |
51 | ||
52 | structure Unify = | |
53 | struct | |
54 | local | |
55 | open Term Trail | |
56 | fun same_ref (r, REF(r')) = (r = r') | |
57 | | same_ref _ = false | |
58 | ||
59 | fun occurs_check r t = | |
60 | let | |
61 | fun oc (STR(_,ts)) = ocs ts | |
62 | | oc (REF(r')) = | |
63 | (case !r' of | |
64 | SOME(s) => oc s | |
65 | | _ => r <> r') | |
66 | | oc (CON _) = true | |
67 | | oc (INT _) = true | |
68 | and ocs nil = true | |
69 | | ocs (t::ts) = oc t andalso ocs ts | |
70 | in | |
71 | oc t | |
72 | end | |
73 | fun deref (t as (REF(x))) = | |
74 | (case !x of | |
75 | SOME(s) => deref s | |
76 | | _ => t) | |
77 | | deref t = t | |
78 | fun unify' (REF(r), t) sc = unify_REF (r,t) sc | |
79 | | unify' (s, REF(r)) sc = unify_REF (r,s) sc | |
80 | | unify' (STR(f,ts), STR(g,ss)) sc = | |
81 | if (f = g) | |
82 | then unifys (ts,ss) sc | |
83 | else () | |
84 | | unify' (CON(f), CON(g)) sc = | |
85 | if (f = g) then | |
86 | sc () | |
87 | else | |
88 | () | |
89 | | unify' (INT(f), INT(g)) sc = | |
90 | if (f = g) then | |
91 | sc () | |
92 | else | |
93 | () | |
94 | | unify' (_, _) sc = () | |
95 | and unifys (nil, nil) sc = sc () | |
96 | | unifys (t::ts, s::ss) sc = | |
97 | unify' (deref(t), deref(s)) | |
98 | (fn () => unifys (ts, ss) sc) | |
99 | | unifys _ sc = () | |
100 | and unify_REF (r, t) sc = | |
101 | if same_ref (r, t) | |
102 | then sc () | |
103 | else if occurs_check r t | |
104 | then ( bind(r, t) ; sc () ) | |
105 | else () | |
106 | in | |
107 | val deref = deref | |
108 | fun unify (s, t) = unify' (deref(s), deref(t)) | |
109 | end (* local *) | |
110 | end; (* Unify *) | |
111 | ||
112 | (* data.sml *) | |
113 | ||
114 | structure Data = | |
115 | struct | |
116 | local | |
117 | open Term Trail Unify | |
118 | val cons_s = "cons" | |
119 | val x_s = "x" | |
120 | val nil_s = "nil" | |
121 | val o_s = "o" | |
122 | val s_s = "s" | |
123 | val CON_o_s = CON(o_s) | |
124 | val CON_nil_s = CON(nil_s) | |
125 | val CON_x_s = CON(x_s) | |
126 | in | |
127 | fun exists sc = sc (REF(ref(NONE))) | |
128 | ||
129 | fun move_horiz (T_1, T_2) sc = | |
130 | ( | |
131 | trail (fn () => | |
132 | ( | |
133 | trail (fn () => | |
134 | ( | |
135 | trail (fn () => | |
136 | ( | |
137 | trail (fn () => | |
138 | ( | |
139 | trail (fn () => | |
140 | ( | |
141 | trail (fn () => | |
142 | ( | |
143 | trail (fn () => | |
144 | ( | |
145 | trail (fn () => | |
146 | ( | |
147 | trail (fn () => | |
148 | ( | |
149 | trail (fn () => | |
150 | ( | |
151 | trail (fn () => | |
152 | exists (fn T => | |
153 | exists (fn TT => | |
154 | unify (T_1, STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, T])])]), TT])) (fn () => | |
155 | unify (T_2, STR(cons_s, [STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, T])])]), TT])) (fn () => | |
156 | sc ()))))) | |
157 | ; | |
158 | exists (fn P1 => | |
159 | exists (fn P5 => | |
160 | exists (fn TT => | |
161 | unify (T_1, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, STR(cons_s, [P5, CON_nil_s])])])])]), TT])) (fn () => | |
162 | unify (T_2, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, STR(cons_s, [P5, CON_nil_s])])])])]), TT])) (fn () => | |
163 | sc ()))))) | |
164 | )) | |
165 | ; | |
166 | exists (fn P1 => | |
167 | exists (fn P2 => | |
168 | exists (fn TT => | |
169 | unify (T_1, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [P2, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, CON_nil_s])])])])]), TT])) (fn () => | |
170 | unify (T_2, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [P2, STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, CON_nil_s])])])])]), TT])) (fn () => | |
171 | sc ()))))) | |
172 | )) | |
173 | ; | |
174 | exists (fn L1 => | |
175 | exists (fn P4 => | |
176 | exists (fn TT => | |
177 | unify (T_1, STR(cons_s, [L1, STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, STR(cons_s, [P4, CON_nil_s])])])]), TT])])) (fn () => | |
178 | unify (T_2, STR(cons_s, [L1, STR(cons_s, [STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, STR(cons_s, [P4, CON_nil_s])])])]), TT])])) (fn () => | |
179 | sc ()))))) | |
180 | )) | |
181 | ; | |
182 | exists (fn L1 => | |
183 | exists (fn P1 => | |
184 | exists (fn TT => | |
185 | unify (T_1, STR(cons_s, [L1, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, CON_nil_s])])])]), TT])])) (fn () => | |
186 | unify (T_2, STR(cons_s, [L1, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, CON_nil_s])])])]), TT])])) (fn () => | |
187 | sc ()))))) | |
188 | )) | |
189 | ; | |
190 | exists (fn L1 => | |
191 | exists (fn L2 => | |
192 | exists (fn TT => | |
193 | unify (T_1, STR(cons_s, [L1, STR(cons_s, [L2, STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, CON_nil_s])])]), TT])])])) (fn () => | |
194 | unify (T_2, STR(cons_s, [L1, STR(cons_s, [L2, STR(cons_s, [STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, CON_nil_s])])]), TT])])])) (fn () => | |
195 | sc ()))))) | |
196 | )) | |
197 | ; | |
198 | exists (fn T => | |
199 | exists (fn TT => | |
200 | unify (T_1, STR(cons_s, [STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, T])])]), TT])) (fn () => | |
201 | unify (T_2, STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, T])])]), TT])) (fn () => | |
202 | sc ())))) | |
203 | )) | |
204 | ; | |
205 | exists (fn P1 => | |
206 | exists (fn P5 => | |
207 | exists (fn TT => | |
208 | unify (T_1, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [P5, CON_nil_s])])])])]), TT])) (fn () => | |
209 | unify (T_2, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, STR(cons_s, [P5, CON_nil_s])])])])]), TT])) (fn () => | |
210 | sc ()))))) | |
211 | )) | |
212 | ; | |
213 | exists (fn P1 => | |
214 | exists (fn P2 => | |
215 | exists (fn TT => | |
216 | unify (T_1, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [P2, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, CON_nil_s])])])])]), TT])) (fn () => | |
217 | unify (T_2, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [P2, STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, CON_nil_s])])])])]), TT])) (fn () => | |
218 | sc ()))))) | |
219 | )) | |
220 | ; | |
221 | exists (fn L1 => | |
222 | exists (fn P4 => | |
223 | exists (fn TT => | |
224 | unify (T_1, STR(cons_s, [L1, STR(cons_s, [STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [P4, CON_nil_s])])])]), TT])])) (fn () => | |
225 | unify (T_2, STR(cons_s, [L1, STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, STR(cons_s, [P4, CON_nil_s])])])]), TT])])) (fn () => | |
226 | sc ()))))) | |
227 | )) | |
228 | ; | |
229 | exists (fn L1 => | |
230 | exists (fn P1 => | |
231 | exists (fn TT => | |
232 | unify (T_1, STR(cons_s, [L1, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, CON_nil_s])])])]), TT])])) (fn () => | |
233 | unify (T_2, STR(cons_s, [L1, STR(cons_s, [STR(cons_s, [P1, STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, CON_nil_s])])])]), TT])])) (fn () => | |
234 | sc ()))))) | |
235 | )) | |
236 | ; | |
237 | exists (fn L1 => | |
238 | exists (fn L2 => | |
239 | exists (fn TT => | |
240 | unify (T_1, STR(cons_s, [L1, STR(cons_s, [L2, STR(cons_s, [STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, CON_nil_s])])]), TT])])])) (fn () => | |
241 | unify (T_2, STR(cons_s, [L1, STR(cons_s, [L2, STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_o_s, CON_nil_s])])]), TT])])])) (fn () => | |
242 | sc ()))))) | |
243 | ) | |
244 | (* | move_horiz _ _ = () *) | |
245 | ||
246 | and rotate (T_1, T_2) sc = | |
247 | exists (fn P11 => | |
248 | exists (fn P12 => | |
249 | exists (fn P13 => | |
250 | exists (fn P14 => | |
251 | exists (fn P15 => | |
252 | exists (fn P21 => | |
253 | exists (fn P22 => | |
254 | exists (fn P23 => | |
255 | exists (fn P24 => | |
256 | exists (fn P31 => | |
257 | exists (fn P32 => | |
258 | exists (fn P33 => | |
259 | exists (fn P41 => | |
260 | exists (fn P42 => | |
261 | exists (fn P51 => | |
262 | unify (T_1, STR(cons_s, [STR(cons_s, [P11, STR(cons_s, [P12, STR(cons_s, [P13, STR(cons_s, [P14, STR(cons_s, [P15, CON_nil_s])])])])]), STR(cons_s, [STR(cons_s, [P21, STR(cons_s, [P22, STR(cons_s, [P23, STR(cons_s, [P24, CON_nil_s])])])]), STR(cons_s, [STR(cons_s, [P31, STR(cons_s, [P32, STR(cons_s, [P33, CON_nil_s])])]), STR(cons_s, [STR(cons_s, [P41, STR(cons_s, [P42, CON_nil_s])]), STR(cons_s, [STR(cons_s, [P51, CON_nil_s]), CON_nil_s])])])])])) (fn () => | |
263 | unify (T_2, STR(cons_s, [STR(cons_s, [P51, STR(cons_s, [P41, STR(cons_s, [P31, STR(cons_s, [P21, STR(cons_s, [P11, CON_nil_s])])])])]), STR(cons_s, [STR(cons_s, [P42, STR(cons_s, [P32, STR(cons_s, [P22, STR(cons_s, [P12, CON_nil_s])])])]), STR(cons_s, [STR(cons_s, [P33, STR(cons_s, [P23, STR(cons_s, [P13, CON_nil_s])])]), STR(cons_s, [STR(cons_s, [P24, STR(cons_s, [P14, CON_nil_s])]), STR(cons_s, [STR(cons_s, [P15, CON_nil_s]), CON_nil_s])])])])])) (fn () => | |
264 | sc ()))))))))))))))))) | |
265 | (* | rotate _ _ = () *) | |
266 | ||
267 | and move (T_1, T_2) sc = | |
268 | ( | |
269 | trail (fn () => | |
270 | ( | |
271 | trail (fn () => | |
272 | exists (fn X => | |
273 | exists (fn Y => | |
274 | unify (T_1, X) (fn () => | |
275 | unify (T_2, Y) (fn () => | |
276 | move_horiz (X, Y) sc))))) | |
277 | ; | |
278 | exists (fn X => | |
279 | exists (fn X1 => | |
280 | exists (fn Y => | |
281 | exists (fn Y1 => | |
282 | unify (T_1, X) (fn () => | |
283 | unify (T_2, Y) (fn () => | |
284 | rotate (X, X1) (fn () => | |
285 | move_horiz (X1, Y1) (fn () => | |
286 | rotate (Y, Y1) sc)))))))) | |
287 | )) | |
288 | ; | |
289 | exists (fn X => | |
290 | exists (fn X1 => | |
291 | exists (fn Y => | |
292 | exists (fn Y1 => | |
293 | unify (T_1, X) (fn () => | |
294 | unify (T_2, Y) (fn () => | |
295 | rotate (X1, X) (fn () => | |
296 | move_horiz (X1, Y1) (fn () => | |
297 | rotate (Y1, Y) sc)))))))) | |
298 | ) | |
299 | (* | move _ _ = () *) | |
300 | ||
301 | and solitaire (T_1, T_2, T_3) sc = | |
302 | ( | |
303 | trail (fn () => | |
304 | exists (fn X => | |
305 | unify (T_1, X) (fn () => | |
306 | unify (T_2, STR(cons_s, [X, CON_nil_s])) (fn () => | |
307 | unify (T_3, INT(0)) (fn () => | |
308 | sc ()))))) | |
309 | ; | |
310 | exists (fn N => | |
311 | exists (fn X => | |
312 | exists (fn Y => | |
313 | exists (fn Z => | |
314 | unify (T_1, X) (fn () => | |
315 | unify (T_2, STR(cons_s, [X, Z])) (fn () => | |
316 | unify (T_3, STR(s_s, [N])) (fn () => | |
317 | move (X, Y) (fn () => | |
318 | solitaire (Y, Z, N) sc)))))))) | |
319 | ) | |
320 | (* | solitaire _ _ = () *) | |
321 | ||
322 | and solution1 (T_1) sc = | |
323 | exists (fn X => | |
324 | unify (T_1, X) (fn () => | |
325 | solitaire (STR(cons_s, [STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, CON_nil_s])])])])]), STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, | |
326 | CON_nil_s])])])]), STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, CON_nil_s])])]), STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, CON_nil_s])]), STR(cons_s, [STR(cons_s, [CON_x_s, CON_nil_s]), CON_nil_s])])])])]) | |
327 | , X, STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [INT(0)])])])])])])])])])])])])])) sc)) | |
328 | (* | solution1 _ _ = () *) | |
329 | ||
330 | and solution2 (T_1) sc = | |
331 | exists (fn X => | |
332 | unify (T_1, X) (fn () => | |
333 | solitaire (STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, CON_nil_s])])])])]), STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, | |
334 | CON_nil_s])])])]), STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_o_s, STR(cons_s, [CON_x_s, CON_nil_s])])]), STR(cons_s, [STR(cons_s, [CON_x_s, STR(cons_s, [CON_x_s, CON_nil_s])]), STR(cons_s, [STR(cons_s, [CON_x_s, CON_nil_s]), CON_nil_s])])])])]) | |
335 | , X, STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [STR(s_s, [INT(0)])])])])])])])])])])])])])) sc)) | |
336 | (* | solution2 _ _ = () *) | |
337 | end (* local *) | |
338 | end; (* Data *) | |
339 | signature BMARK = | |
340 | sig | |
341 | val doit : int -> unit | |
342 | val testit : TextIO.outstream -> unit | |
343 | end; | |
344 | (* main.sml *) | |
345 | ||
346 | structure Main : BMARK = | |
347 | struct | |
348 | val name = "Logic" | |
349 | ||
350 | exception Done | |
351 | ||
352 | fun testit strm = Data.exists(fn Z => Data.solution2 Z (fn () => raise Done)) | |
353 | handle Done => TextIO.output(strm, "yes\n") | |
354 | ||
355 | fun doit () = Data.exists(fn Z => Data.solution2 Z (fn () => raise Done)) | |
356 | handle Done => () | |
357 | ||
358 | val doit = | |
359 | fn size => | |
360 | let | |
361 | fun loop n = | |
362 | if n = 0 | |
363 | then () | |
364 | else (doit(); | |
365 | loop(n-1)) | |
366 | in loop size | |
367 | end | |
368 | ||
369 | end; (* Main *) |