| 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 *) |