benchmark/tests/logic.sml

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