HCoop / hcoop / debian / mlton.git / blame
| 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 *) |