benchmark/tests/boyer.sml

   1 (* From the SML/NJ benchmark suite. *)
   2 (* terms.sml:
   3  *
   4  * Manipulations over terms
   5  *)
   6
   7 signature TERMS =
   8   sig
   9     type head;
  10     datatype term =
  11       Var of int
  12     | Prop of head * term list;
  13     datatype binding = Bind of int * term;
  14     val get: string -> head
  15     and headname: head -> string
  16     and add_lemma: term -> unit
  17     and apply_subst: binding list -> term -> term
  18     and rewrite: term -> term
  19   end;
  20
  21 structure Terms:TERMS =
  22   struct
  23
  24     datatype term
  25       = Var of int
  26       | Prop of { name: string, props: (term * term) list ref } * term list
  27
  28     type head = { name: string, props: (term * term) list ref }
  29
  30     val lemmas = ref ([] : head list)
  31
  32 (* replacement for property lists *)
  33
  34     fun headname {name = n, props=p} = n;
  35
  36 fun get name =
  37   let fun get_rec ((hd1 as {name=n,...})::hdl) =
  38       if n = name then hd1 else get_rec hdl
  39         | get_rec [] =
  40       let val entry = {name = name, props = ref []} in
  41         lemmas := entry :: !lemmas;
  42         entry
  43       end
  44   in
  45     get_rec (!lemmas)
  46   end
  47 ;
  48
  49 fun add_lemma (Prop(_, [(left as Prop({props=r,...},_)), right])) =
  50   r := (left, right) :: !r
  51 ;
  52
  53 (* substitutions *)
  54
  55 exception failure of string;
  56
  57 datatype binding = Bind of int * term
  58 ;
  59
  60 fun get_binding v =
  61   let fun get_rec [] = raise (failure "unbound")
  62         | get_rec (Bind(w,t)::rest) =
  63             if v = w then t else get_rec rest
  64   in
  65     get_rec
  66   end
  67 ;
  68
  69 fun apply_subst alist =
  70   let fun as_rec (term as Var v) =
  71             ((get_binding v alist) handle failure _ => term)
  72         | as_rec (Prop (head,argl)) =
  73             Prop (head, map as_rec argl)
  74   in
  75     as_rec
  76   end
  77 ;
  78
  79 exception Unify;
  80
  81 fun unify (term1, term2) = unify1 (term1, term2, [])
  82 and unify1 (term1, term2, unify_subst) =
  83  (case term2 of
  84     Var v =>
  85       ((if get_binding v unify_subst = term1
  86         then unify_subst
  87         else raise Unify)
  88        handle failure _ =>
  89         Bind(v,term1)::unify_subst)
  90   | Prop (head2,argl2) =>
  91       case term1 of
  92          Var _ => raise Unify
  93        | Prop (head1,argl1) =>
  94            if head1=head2 then unify1_lst (argl1, argl2, unify_subst)
  95                           else raise Unify)
  96 and unify1_lst ([], [], unify_subst) = unify_subst
  97   | unify1_lst (h1::r1, h2::r2, unify_subst) =
  98       unify1_lst(r1, r2, unify1(h1, h2, unify_subst))
  99   | unify1_lst _ = raise Unify
 100 ;
 101
 102 fun rewrite (term as Var _) = term
 103   | rewrite (Prop ((head as {props=p,...}), argl)) =
 104       rewrite_with_lemmas (Prop (head, map rewrite argl),  !p)
 105 and rewrite_with_lemmas (term, []) = term
 106   | rewrite_with_lemmas (term, (t1,t2)::rest) =
 107         rewrite (apply_subst (unify (term, t1)) t2)
 108       handle unify =>
 109         rewrite_with_lemmas (term, rest)
 110 ;
 111 end;
 112 (* rules.sml:
 113  *)
 114
 115 structure Rules =
 116   struct
 117
 118     open Terms;
 119
 120     datatype cterm = CVar of int | CProp of string * cterm list;
 121
 122     fun cterm_to_term (CVar v) = Var v
 123       | cterm_to_term (CProp(p, l)) = Prop(get p, map cterm_to_term l)
 124
 125     fun add t = add_lemma (cterm_to_term t)
 126
 127     val _ = (
 128 add (CProp
 129 ("equal",
 130  [CProp ("compile",[CVar 5]),
 131   CProp
 132   ("reverse",
 133    [CProp ("codegen",[CProp ("optimize",[CVar 5]), CProp ("nil",[])])])]));
 134 add (CProp
 135 ("equal",
 136  [CProp ("eqp",[CVar 23, CVar 24]),
 137   CProp ("equal",[CProp ("fix",[CVar 23]), CProp ("fix",[CVar 24])])]));
 138 add (CProp
 139 ("equal",
 140  [CProp ("gt",[CVar 23, CVar 24]), CProp ("lt",[CVar 24, CVar 23])]));
 141 add (CProp
 142 ("equal",
 143  [CProp ("le",[CVar 23, CVar 24]), CProp ("ge",[CVar 24, CVar 23])]));
 144 add (CProp
 145 ("equal",
 146  [CProp ("ge",[CVar 23, CVar 24]), CProp ("le",[CVar 24, CVar 23])]));
 147 add (CProp
 148 ("equal",
 149  [CProp ("boolean",[CVar 23]),
 150   CProp
 151   ("or",
 152    [CProp ("equal",[CVar 23, CProp ("true",[])]),
 153     CProp ("equal",[CVar 23, CProp ("false",[])])])]));
 154 add (CProp
 155 ("equal",
 156  [CProp ("iff",[CVar 23, CVar 24]),
 157   CProp
 158   ("and",
 159    [CProp ("implies",[CVar 23, CVar 24]),
 160     CProp ("implies",[CVar 24, CVar 23])])]));
 161 add (CProp
 162 ("equal",
 163  [CProp ("even1",[CVar 23]),
 164   CProp
 165   ("if",
 166    [CProp ("zerop",[CVar 23]), CProp ("true",[]),
 167     CProp ("odd",[CProp ("sub1",[CVar 23])])])]));
 168 add (CProp
 169 ("equal",
 170  [CProp ("countps_",[CVar 11, CVar 15]),
 171   CProp ("countps_loop",[CVar 11, CVar 15, CProp ("zero",[])])]));
 172 add (CProp
 173 ("equal",
 174  [CProp ("fact_",[CVar 8]),
 175   CProp ("fact_loop",[CVar 8, CProp ("one",[])])]));
 176 add (CProp
 177 ("equal",
 178  [CProp ("reverse_",[CVar 23]),
 179   CProp ("reverse_loop",[CVar 23, CProp ("nil",[])])]));
 180 add (CProp
 181 ("equal",
 182  [CProp ("divides",[CVar 23, CVar 24]),
 183   CProp ("zerop",[CProp ("remainder",[CVar 24, CVar 23])])]));
 184 add (CProp
 185 ("equal",
 186  [CProp ("assume_true",[CVar 21, CVar 0]),
 187   CProp ("cons",[CProp ("cons",[CVar 21, CProp ("true",[])]), CVar 0])]));
 188 add (CProp
 189 ("equal",
 190  [CProp ("assume_false",[CVar 21, CVar 0]),
 191   CProp ("cons",[CProp ("cons",[CVar 21, CProp ("false",[])]), CVar 0])]));
 192 add (CProp
 193 ("equal",
 194  [CProp ("tautology_checker",[CVar 23]),
 195   CProp ("tautologyp",[CProp ("normalize",[CVar 23]), CProp ("nil",[])])]));
 196 add (CProp
 197 ("equal",
 198  [CProp ("falsify",[CVar 23]),
 199   CProp ("falsify1",[CProp ("normalize",[CVar 23]), CProp ("nil",[])])]));
 200 add (CProp
 201 ("equal",
 202  [CProp ("prime",[CVar 23]),
 203   CProp
 204   ("and",
 205    [CProp ("not",[CProp ("zerop",[CVar 23])]),
 206     CProp
 207     ("not",
 208      [CProp ("equal",[CVar 23, CProp ("add1",[CProp ("zero",[])])])]),
 209     CProp ("prime1",[CVar 23, CProp ("sub1",[CVar 23])])])]));
 210 add (CProp
 211 ("equal",
 212  [CProp ("and",[CVar 15, CVar 16]),
 213   CProp
 214   ("if",
 215    [CVar 15,
 216     CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]),
 217     CProp ("false",[])])]));
 218 add (CProp
 219 ("equal",
 220  [CProp ("or",[CVar 15, CVar 16]),
 221   CProp
 222   ("if",
 223    [CVar 15, CProp ("true",[]),
 224     CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]),
 225     CProp ("false",[])])]));
 226 add (CProp
 227 ("equal",
 228  [CProp ("not",[CVar 15]),
 229   CProp ("if",[CVar 15, CProp ("false",[]), CProp ("true",[])])]));
 230 add (CProp
 231 ("equal",
 232  [CProp ("implies",[CVar 15, CVar 16]),
 233   CProp
 234   ("if",
 235    [CVar 15,
 236     CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]),
 237     CProp ("true",[])])]));
 238 add (CProp
 239 ("equal",
 240  [CProp ("fix",[CVar 23]),
 241   CProp ("if",[CProp ("numberp",[CVar 23]), CVar 23, CProp ("zero",[])])]));
 242 add (CProp
 243 ("equal",
 244  [CProp ("if",[CProp ("if",[CVar 0, CVar 1, CVar 2]), CVar 3, CVar 4]),
 245   CProp
 246   ("if",
 247    [CVar 0, CProp ("if",[CVar 1, CVar 3, CVar 4]),
 248     CProp ("if",[CVar 2, CVar 3, CVar 4])])]));
 249 add (CProp
 250 ("equal",
 251  [CProp ("zerop",[CVar 23]),
 252   CProp
 253   ("or",
 254    [CProp ("equal",[CVar 23, CProp ("zero",[])]),
 255     CProp ("not",[CProp ("numberp",[CVar 23])])])]));
 256 add (CProp
 257 ("equal",
 258  [CProp ("plus",[CProp ("plus",[CVar 23, CVar 24]), CVar 25]),
 259   CProp ("plus",[CVar 23, CProp ("plus",[CVar 24, CVar 25])])]));
 260 add (CProp
 261 ("equal",
 262  [CProp ("equal",[CProp ("plus",[CVar 0, CVar 1]), CProp ("zero",[])]),
 263   CProp ("and",[CProp ("zerop",[CVar 0]), CProp ("zerop",[CVar 1])])]));
 264 add (CProp
 265 ("equal",[CProp ("difference",[CVar 23, CVar 23]), CProp ("zero",[])]));
 266 add (CProp
 267 ("equal",
 268  [CProp
 269   ("equal",
 270    [CProp ("plus",[CVar 0, CVar 1]), CProp ("plus",[CVar 0, CVar 2])]),
 271   CProp ("equal",[CProp ("fix",[CVar 1]), CProp ("fix",[CVar 2])])]));
 272 add (CProp
 273 ("equal",
 274  [CProp
 275   ("equal",[CProp ("zero",[]), CProp ("difference",[CVar 23, CVar 24])]),
 276   CProp ("not",[CProp ("gt",[CVar 24, CVar 23])])]));
 277 add (CProp
 278 ("equal",
 279  [CProp ("equal",[CVar 23, CProp ("difference",[CVar 23, CVar 24])]),
 280   CProp
 281   ("and",
 282    [CProp ("numberp",[CVar 23]),
 283     CProp
 284     ("or",
 285      [CProp ("equal",[CVar 23, CProp ("zero",[])]),
 286       CProp ("zerop",[CVar 24])])])]));
 287 add (CProp
 288 ("equal",
 289  [CProp
 290   ("meaning",
 291    [CProp ("plus_tree",[CProp ("append",[CVar 23, CVar 24])]), CVar 0]),
 292   CProp
 293   ("plus",
 294    [CProp ("meaning",[CProp ("plus_tree",[CVar 23]), CVar 0]),
 295     CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0])])]));
 296 add (CProp
 297 ("equal",
 298  [CProp
 299   ("meaning",
 300    [CProp ("plus_tree",[CProp ("plus_fringe",[CVar 23])]), CVar 0]),
 301   CProp ("fix",[CProp ("meaning",[CVar 23, CVar 0])])]));
 302 add (CProp
 303 ("equal",
 304  [CProp ("append",[CProp ("append",[CVar 23, CVar 24]), CVar 25]),
 305   CProp ("append",[CVar 23, CProp ("append",[CVar 24, CVar 25])])]));
 306 add (CProp
 307 ("equal",
 308  [CProp ("reverse",[CProp ("append",[CVar 0, CVar 1])]),
 309   CProp
 310   ("append",[CProp ("reverse",[CVar 1]), CProp ("reverse",[CVar 0])])]));
 311 add (CProp
 312 ("equal",
 313  [CProp ("times",[CVar 23, CProp ("plus",[CVar 24, CVar 25])]),
 314   CProp
 315   ("plus",
 316    [CProp ("times",[CVar 23, CVar 24]),
 317     CProp ("times",[CVar 23, CVar 25])])]));
 318 add (CProp
 319 ("equal",
 320  [CProp ("times",[CProp ("times",[CVar 23, CVar 24]), CVar 25]),
 321   CProp ("times",[CVar 23, CProp ("times",[CVar 24, CVar 25])])]));
 322 add (CProp
 323 ("equal",
 324  [CProp
 325   ("equal",[CProp ("times",[CVar 23, CVar 24]), CProp ("zero",[])]),
 326   CProp ("or",[CProp ("zerop",[CVar 23]), CProp ("zerop",[CVar 24])])]));
 327 add (CProp
 328 ("equal",
 329  [CProp ("exec",[CProp ("append",[CVar 23, CVar 24]), CVar 15, CVar 4]),
 330   CProp
 331   ("exec",[CVar 24, CProp ("exec",[CVar 23, CVar 15, CVar 4]), CVar 4])]));
 332 add (CProp
 333 ("equal",
 334  [CProp ("mc_flatten",[CVar 23, CVar 24]),
 335   CProp ("append",[CProp ("flatten",[CVar 23]), CVar 24])]));
 336 add (CProp
 337 ("equal",
 338  [CProp ("member",[CVar 23, CProp ("append",[CVar 0, CVar 1])]),
 339   CProp
 340   ("or",
 341    [CProp ("member",[CVar 23, CVar 0]),
 342     CProp ("member",[CVar 23, CVar 1])])]));
 343 add (CProp
 344 ("equal",
 345  [CProp ("member",[CVar 23, CProp ("reverse",[CVar 24])]),
 346   CProp ("member",[CVar 23, CVar 24])]));
 347 add (CProp
 348 ("equal",
 349  [CProp ("length",[CProp ("reverse",[CVar 23])]),
 350   CProp ("length",[CVar 23])]));
 351 add (CProp
 352 ("equal",
 353  [CProp ("member",[CVar 0, CProp ("intersect",[CVar 1, CVar 2])]),
 354   CProp
 355   ("and",
 356    [CProp ("member",[CVar 0, CVar 1]), CProp ("member",[CVar 0, CVar 2])])]));
 357 add (CProp
 358 ("equal",[CProp ("nth",[CProp ("zero",[]), CVar 8]), CProp ("zero",[])]));
 359 add (CProp
 360 ("equal",
 361  [CProp ("exp",[CVar 8, CProp ("plus",[CVar 9, CVar 10])]),
 362   CProp
 363   ("times",
 364    [CProp ("exp",[CVar 8, CVar 9]), CProp ("exp",[CVar 8, CVar 10])])]));
 365 add (CProp
 366 ("equal",
 367  [CProp ("exp",[CVar 8, CProp ("times",[CVar 9, CVar 10])]),
 368   CProp ("exp",[CProp ("exp",[CVar 8, CVar 9]), CVar 10])]));
 369 add (CProp
 370 ("equal",
 371  [CProp ("reverse_loop",[CVar 23, CVar 24]),
 372   CProp ("append",[CProp ("reverse",[CVar 23]), CVar 24])]));
 373 add (CProp
 374 ("equal",
 375  [CProp ("reverse_loop",[CVar 23, CProp ("nil",[])]),
 376   CProp ("reverse",[CVar 23])]));
 377 add (CProp
 378 ("equal",
 379  [CProp ("count_list",[CVar 25, CProp ("sort_lp",[CVar 23, CVar 24])]),
 380   CProp
 381   ("plus",
 382    [CProp ("count_list",[CVar 25, CVar 23]),
 383     CProp ("count_list",[CVar 25, CVar 24])])]));
 384 add (CProp
 385 ("equal",
 386  [CProp
 387   ("equal",
 388    [CProp ("append",[CVar 0, CVar 1]), CProp ("append",[CVar 0, CVar 2])]),
 389   CProp ("equal",[CVar 1, CVar 2])]));
 390 add (CProp
 391 ("equal",
 392  [CProp
 393   ("plus",
 394    [CProp ("remainder",[CVar 23, CVar 24]),
 395     CProp ("times",[CVar 24, CProp ("quotient",[CVar 23, CVar 24])])]),
 396   CProp ("fix",[CVar 23])]));
 397 add (CProp
 398 ("equal",
 399  [CProp
 400   ("power_eval",[CProp ("big_plus",[CVar 11, CVar 8, CVar 1]), CVar 1]),
 401   CProp ("plus",[CProp ("power_eval",[CVar 11, CVar 1]), CVar 8])]));
 402 add (CProp
 403 ("equal",
 404  [CProp
 405   ("power_eval",
 406    [CProp ("big_plus",[CVar 23, CVar 24, CVar 8, CVar 1]), CVar 1]),
 407   CProp
 408   ("plus",
 409    [CVar 8,
 410     CProp
 411     ("plus",
 412      [CProp ("power_eval",[CVar 23, CVar 1]),
 413       CProp ("power_eval",[CVar 24, CVar 1])])])]));
 414 add (CProp
 415 ("equal",
 416  [CProp ("remainder",[CVar 24, CProp ("one",[])]), CProp ("zero",[])]));
 417 add (CProp
 418 ("equal",
 419  [CProp ("lt",[CProp ("remainder",[CVar 23, CVar 24]), CVar 24]),
 420   CProp ("not",[CProp ("zerop",[CVar 24])])]));
 421 add (CProp
 422 ("equal",[CProp ("remainder",[CVar 23, CVar 23]), CProp ("zero",[])]));
 423 add (CProp
 424 ("equal",
 425  [CProp ("lt",[CProp ("quotient",[CVar 8, CVar 9]), CVar 8]),
 426   CProp
 427   ("and",
 428    [CProp ("not",[CProp ("zerop",[CVar 8])]),
 429     CProp
 430     ("or",
 431      [CProp ("zerop",[CVar 9]),
 432       CProp ("not",[CProp ("equal",[CVar 9, CProp ("one",[])])])])])]));
 433 add (CProp
 434 ("equal",
 435  [CProp ("lt",[CProp ("remainder",[CVar 23, CVar 24]), CVar 23]),
 436   CProp
 437   ("and",
 438    [CProp ("not",[CProp ("zerop",[CVar 24])]),
 439     CProp ("not",[CProp ("zerop",[CVar 23])]),
 440     CProp ("not",[CProp ("lt",[CVar 23, CVar 24])])])]));
 441 add (CProp
 442 ("equal",
 443  [CProp ("power_eval",[CProp ("power_rep",[CVar 8, CVar 1]), CVar 1]),
 444   CProp ("fix",[CVar 8])]));
 445 add (CProp
 446 ("equal",
 447  [CProp
 448   ("power_eval",
 449    [CProp
 450     ("big_plus",
 451      [CProp ("power_rep",[CVar 8, CVar 1]),
 452       CProp ("power_rep",[CVar 9, CVar 1]), CProp ("zero",[]),
 453       CVar 1]),
 454     CVar 1]),
 455   CProp ("plus",[CVar 8, CVar 9])]));
 456 add (CProp
 457 ("equal",
 458  [CProp ("gcd",[CVar 23, CVar 24]), CProp ("gcd",[CVar 24, CVar 23])]));
 459 add (CProp
 460 ("equal",
 461  [CProp ("nth",[CProp ("append",[CVar 0, CVar 1]), CVar 8]),
 462   CProp
 463   ("append",
 464    [CProp ("nth",[CVar 0, CVar 8]),
 465     CProp
 466     ("nth",
 467      [CVar 1, CProp ("difference",[CVar 8, CProp ("length",[CVar 0])])])])]));
 468 add (CProp
 469 ("equal",
 470  [CProp ("difference",[CProp ("plus",[CVar 23, CVar 24]), CVar 23]),
 471   CProp ("fix",[CVar 24])]));
 472 add (CProp
 473 ("equal",
 474  [CProp ("difference",[CProp ("plus",[CVar 24, CVar 23]), CVar 23]),
 475   CProp ("fix",[CVar 24])]));
 476 add (CProp
 477 ("equal",
 478  [CProp
 479   ("difference",
 480    [CProp ("plus",[CVar 23, CVar 24]), CProp ("plus",[CVar 23, CVar 25])]),
 481   CProp ("difference",[CVar 24, CVar 25])]));
 482 add (CProp
 483 ("equal",
 484  [CProp ("times",[CVar 23, CProp ("difference",[CVar 2, CVar 22])]),
 485   CProp
 486   ("difference",
 487    [CProp ("times",[CVar 2, CVar 23]),
 488     CProp ("times",[CVar 22, CVar 23])])]));
 489 add (CProp
 490 ("equal",
 491  [CProp ("remainder",[CProp ("times",[CVar 23, CVar 25]), CVar 25]),
 492   CProp ("zero",[])]));
 493 add (CProp
 494 ("equal",
 495  [CProp
 496   ("difference",
 497    [CProp ("plus",[CVar 1, CProp ("plus",[CVar 0, CVar 2])]), CVar 0]),
 498   CProp ("plus",[CVar 1, CVar 2])]));
 499 add (CProp
 500 ("equal",
 501  [CProp
 502   ("difference",
 503    [CProp ("add1",[CProp ("plus",[CVar 24, CVar 25])]), CVar 25]),
 504   CProp ("add1",[CVar 24])]));
 505 add (CProp
 506 ("equal",
 507  [CProp
 508   ("lt",
 509    [CProp ("plus",[CVar 23, CVar 24]), CProp ("plus",[CVar 23, CVar 25])]),
 510   CProp ("lt",[CVar 24, CVar 25])]));
 511 add (CProp
 512 ("equal",
 513  [CProp
 514   ("lt",
 515    [CProp ("times",[CVar 23, CVar 25]),
 516     CProp ("times",[CVar 24, CVar 25])]),
 517   CProp
 518   ("and",
 519    [CProp ("not",[CProp ("zerop",[CVar 25])]),
 520     CProp ("lt",[CVar 23, CVar 24])])]));
 521 add (CProp
 522 ("equal",
 523  [CProp ("lt",[CVar 24, CProp ("plus",[CVar 23, CVar 24])]),
 524   CProp ("not",[CProp ("zerop",[CVar 23])])]));
 525 add (CProp
 526 ("equal",
 527  [CProp
 528   ("gcd",
 529    [CProp ("times",[CVar 23, CVar 25]),
 530     CProp ("times",[CVar 24, CVar 25])]),
 531   CProp ("times",[CVar 25, CProp ("gcd",[CVar 23, CVar 24])])]));
 532 add (CProp
 533 ("equal",
 534  [CProp ("value",[CProp ("normalize",[CVar 23]), CVar 0]),
 535   CProp ("value",[CVar 23, CVar 0])]));
 536 add (CProp
 537 ("equal",
 538  [CProp
 539   ("equal",
 540    [CProp ("flatten",[CVar 23]),
 541     CProp ("cons",[CVar 24, CProp ("nil",[])])]),
 542   CProp
 543   ("and",
 544    [CProp ("nlistp",[CVar 23]), CProp ("equal",[CVar 23, CVar 24])])]));
 545 add (CProp
 546 ("equal",
 547  [CProp ("listp",[CProp ("gother",[CVar 23])]),
 548   CProp ("listp",[CVar 23])]));
 549 add (CProp
 550 ("equal",
 551  [CProp ("samefringe",[CVar 23, CVar 24]),
 552   CProp
 553   ("equal",[CProp ("flatten",[CVar 23]), CProp ("flatten",[CVar 24])])]));
 554 add (CProp
 555 ("equal",
 556  [CProp
 557   ("equal",
 558    [CProp ("greatest_factor",[CVar 23, CVar 24]), CProp ("zero",[])]),
 559   CProp
 560   ("and",
 561    [CProp
 562     ("or",
 563      [CProp ("zerop",[CVar 24]),
 564       CProp ("equal",[CVar 24, CProp ("one",[])])]),
 565     CProp ("equal",[CVar 23, CProp ("zero",[])])])]));
 566 add (CProp
 567 ("equal",
 568  [CProp
 569   ("equal",
 570    [CProp ("greatest_factor",[CVar 23, CVar 24]), CProp ("one",[])]),
 571   CProp ("equal",[CVar 23, CProp ("one",[])])]));
 572 add (CProp
 573 ("equal",
 574  [CProp ("numberp",[CProp ("greatest_factor",[CVar 23, CVar 24])]),
 575   CProp
 576   ("not",
 577    [CProp
 578     ("and",
 579      [CProp
 580       ("or",
 581        [CProp ("zerop",[CVar 24]),
 582         CProp ("equal",[CVar 24, CProp ("one",[])])]),
 583       CProp ("not",[CProp ("numberp",[CVar 23])])])])]));
 584 add (CProp
 585 ("equal",
 586  [CProp ("times_list",[CProp ("append",[CVar 23, CVar 24])]),
 587   CProp
 588   ("times",
 589    [CProp ("times_list",[CVar 23]), CProp ("times_list",[CVar 24])])]));
 590 add (CProp
 591 ("equal",
 592  [CProp ("prime_list",[CProp ("append",[CVar 23, CVar 24])]),
 593   CProp
 594   ("and",
 595    [CProp ("prime_list",[CVar 23]), CProp ("prime_list",[CVar 24])])]));
 596 add (CProp
 597 ("equal",
 598  [CProp ("equal",[CVar 25, CProp ("times",[CVar 22, CVar 25])]),
 599   CProp
 600   ("and",
 601    [CProp ("numberp",[CVar 25]),
 602     CProp
 603     ("or",
 604      [CProp ("equal",[CVar 25, CProp ("zero",[])]),
 605       CProp ("equal",[CVar 22, CProp ("one",[])])])])]));
 606 add (CProp
 607 ("equal",
 608  [CProp ("ge",[CVar 23, CVar 24]),
 609   CProp ("not",[CProp ("lt",[CVar 23, CVar 24])])]));
 610 add (CProp
 611 ("equal",
 612  [CProp ("equal",[CVar 23, CProp ("times",[CVar 23, CVar 24])]),
 613   CProp
 614   ("or",
 615    [CProp ("equal",[CVar 23, CProp ("zero",[])]),
 616     CProp
 617     ("and",
 618      [CProp ("numberp",[CVar 23]),
 619       CProp ("equal",[CVar 24, CProp ("one",[])])])])]));
 620 add (CProp
 621 ("equal",
 622  [CProp ("remainder",[CProp ("times",[CVar 24, CVar 23]), CVar 24]),
 623   CProp ("zero",[])]));
 624 add (CProp
 625 ("equal",
 626  [CProp ("equal",[CProp ("times",[CVar 0, CVar 1]), CProp ("one",[])]),
 627   CProp
 628   ("and",
 629    [CProp ("not",[CProp ("equal",[CVar 0, CProp ("zero",[])])]),
 630     CProp ("not",[CProp ("equal",[CVar 1, CProp ("zero",[])])]),
 631     CProp ("numberp",[CVar 0]), CProp ("numberp",[CVar 1]),
 632     CProp ("equal",[CProp ("sub1",[CVar 0]), CProp ("zero",[])]),
 633     CProp ("equal",[CProp ("sub1",[CVar 1]), CProp ("zero",[])])])]));
 634 add (CProp
 635 ("equal",
 636  [CProp
 637   ("lt",
 638    [CProp ("length",[CProp ("delete",[CVar 23, CVar 11])]),
 639     CProp ("length",[CVar 11])]),
 640   CProp ("member",[CVar 23, CVar 11])]));
 641 add (CProp
 642 ("equal",
 643  [CProp ("sort2",[CProp ("delete",[CVar 23, CVar 11])]),
 644   CProp ("delete",[CVar 23, CProp ("sort2",[CVar 11])])]));
 645 add (CProp ("equal",[CProp ("dsort",[CVar 23]), CProp ("sort2",[CVar 23])]));
 646 add (CProp
 647 ("equal",
 648  [CProp
 649   ("length",
 650    [CProp
 651     ("cons",
 652      [CVar 0,
 653       CProp
 654       ("cons",
 655        [CVar 1,
 656         CProp
 657         ("cons",
 658          [CVar 2,
 659           CProp
 660           ("cons",
 661            [CVar 3,
 662             CProp ("cons",[CVar 4, CProp ("cons",[CVar 5, CVar 6])])])])])])])
 663   , CProp ("plus",[CProp ("six",[]), CProp ("length",[CVar 6])])]));
 664 add (CProp
 665 ("equal",
 666  [CProp
 667   ("difference",
 668    [CProp ("add1",[CProp ("add1",[CVar 23])]), CProp ("two",[])]),
 669   CProp ("fix",[CVar 23])]));
 670 add (CProp
 671 ("equal",
 672  [CProp
 673   ("quotient",
 674    [CProp ("plus",[CVar 23, CProp ("plus",[CVar 23, CVar 24])]),
 675     CProp ("two",[])]),
 676   CProp
 677   ("plus",[CVar 23, CProp ("quotient",[CVar 24, CProp ("two",[])])])]));
 678 add (CProp
 679 ("equal",
 680  [CProp ("sigma",[CProp ("zero",[]), CVar 8]),
 681   CProp
 682   ("quotient",
 683    [CProp ("times",[CVar 8, CProp ("add1",[CVar 8])]), CProp ("two",[])])]));
 684 add (CProp
 685 ("equal",
 686  [CProp ("plus",[CVar 23, CProp ("add1",[CVar 24])]),
 687   CProp
 688   ("if",
 689    [CProp ("numberp",[CVar 24]),
 690     CProp ("add1",[CProp ("plus",[CVar 23, CVar 24])]),
 691     CProp ("add1",[CVar 23])])]));
 692 add (CProp
 693 ("equal",
 694  [CProp
 695   ("equal",
 696    [CProp ("difference",[CVar 23, CVar 24]),
 697     CProp ("difference",[CVar 25, CVar 24])]),
 698   CProp
 699   ("if",
 700    [CProp ("lt",[CVar 23, CVar 24]),
 701     CProp ("not",[CProp ("lt",[CVar 24, CVar 25])]),
 702     CProp
 703     ("if",
 704      [CProp ("lt",[CVar 25, CVar 24]),
 705       CProp ("not",[CProp ("lt",[CVar 24, CVar 23])]),
 706       CProp ("equal",[CProp ("fix",[CVar 23]), CProp ("fix",[CVar 25])])])])])
 707 );
 708 add (CProp
 709 ("equal",
 710  [CProp
 711   ("meaning",
 712    [CProp ("plus_tree",[CProp ("delete",[CVar 23, CVar 24])]), CVar 0]),
 713   CProp
 714   ("if",
 715    [CProp ("member",[CVar 23, CVar 24]),
 716     CProp
 717     ("difference",
 718      [CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0]),
 719       CProp ("meaning",[CVar 23, CVar 0])]),
 720     CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0])])]));
 721 add (CProp
 722 ("equal",
 723  [CProp ("times",[CVar 23, CProp ("add1",[CVar 24])]),
 724   CProp
 725   ("if",
 726    [CProp ("numberp",[CVar 24]),
 727     CProp
 728     ("plus",
 729      [CVar 23, CProp ("times",[CVar 23, CVar 24]),
 730       CProp ("fix",[CVar 23])])])]));
 731 add (CProp
 732 ("equal",
 733  [CProp ("nth",[CProp ("nil",[]), CVar 8]),
 734   CProp
 735   ("if",[CProp ("zerop",[CVar 8]), CProp ("nil",[]), CProp ("zero",[])])]));
 736 add (CProp
 737 ("equal",
 738  [CProp ("last",[CProp ("append",[CVar 0, CVar 1])]),
 739   CProp
 740   ("if",
 741    [CProp ("listp",[CVar 1]), CProp ("last",[CVar 1]),
 742     CProp
 743     ("if",
 744      [CProp ("listp",[CVar 0]),
 745       CProp ("cons",[CProp ("car",[CProp ("last",[CVar 0])]), CVar 1]),
 746       CVar 1])])]));
 747 add (CProp
 748 ("equal",
 749  [CProp ("equal",[CProp ("lt",[CVar 23, CVar 24]), CVar 25]),
 750   CProp
 751   ("if",
 752    [CProp ("lt",[CVar 23, CVar 24]),
 753     CProp ("equal",[CProp ("true",[]), CVar 25]),
 754     CProp ("equal",[CProp ("false",[]), CVar 25])])]));
 755 add (CProp
 756 ("equal",
 757  [CProp ("assignment",[CVar 23, CProp ("append",[CVar 0, CVar 1])]),
 758   CProp
 759   ("if",
 760    [CProp ("assignedp",[CVar 23, CVar 0]),
 761     CProp ("assignment",[CVar 23, CVar 0]),
 762     CProp ("assignment",[CVar 23, CVar 1])])]));
 763 add (CProp
 764 ("equal",
 765  [CProp ("car",[CProp ("gother",[CVar 23])]),
 766   CProp
 767   ("if",
 768    [CProp ("listp",[CVar 23]),
 769     CProp ("car",[CProp ("flatten",[CVar 23])]), CProp ("zero",[])])]));
 770 add (CProp
 771 ("equal",
 772  [CProp ("flatten",[CProp ("cdr",[CProp ("gother",[CVar 23])])]),
 773   CProp
 774   ("if",
 775    [CProp ("listp",[CVar 23]),
 776     CProp ("cdr",[CProp ("flatten",[CVar 23])]),
 777     CProp ("cons",[CProp ("zero",[]), CProp ("nil",[])])])]));
 778 add (CProp
 779 ("equal",
 780  [CProp ("quotient",[CProp ("times",[CVar 24, CVar 23]), CVar 24]),
 781   CProp
 782   ("if",
 783    [CProp ("zerop",[CVar 24]), CProp ("zero",[]),
 784     CProp ("fix",[CVar 23])])]));
 785 add (CProp
 786 ("equal",
 787  [CProp ("get",[CVar 9, CProp ("set",[CVar 8, CVar 21, CVar 12])]),
 788   CProp
 789   ("if",
 790    [CProp ("eqp",[CVar 9, CVar 8]), CVar 21,
 791     CProp ("get",[CVar 9, CVar 12])])])))
 792
 793   end; (* Rules *)
 794
 795 (* boyer.sml:
 796  *
 797  * Tautology checker
 798  *)
 799
 800 signature BOYER =
 801   sig
 802     include TERMS
 803     val tautp: term -> bool
 804   end
 805
 806 structure Boyer: BOYER =
 807   struct
 808
 809 open Terms
 810
 811 fun mem x [] = false
 812   | mem x (y::L) = x=y orelse mem x L
 813
 814 fun truep (x, lst) =
 815   case x of
 816     Prop(head, _) =>
 817       headname head = "true" orelse mem x lst
 818   | _ =>
 819       mem x lst
 820
 821 and falsep (x, lst) =
 822   case x of
 823     Prop(head, _) =>
 824       headname head = "false" orelse mem x lst
 825   | _ =>
 826       mem x lst
 827
 828 fun tautologyp (x, true_lst, false_lst) =
 829  if truep (x, true_lst) then true else
 830  if falsep (x, false_lst) then false else
 831  (case x of
 832      Var _ => false
 833    | Prop (head,[test, yes, no]) =>
 834         if headname head = "if" then
 835           if truep (test, true_lst) then
 836             tautologyp (yes, true_lst, false_lst)
 837           else if falsep (test, false_lst) then
 838             tautologyp (no, true_lst, false_lst)
 839           else tautologyp (yes, test::true_lst, false_lst) andalso
 840                tautologyp (no, true_lst, test::false_lst)
 841         else
 842           false)
 843
 844     fun tautp x = tautologyp(rewrite x, [], []);
 845
 846   end; (* Boyer *)
 847
 848 signature BMARK =
 849   sig
 850     val doit : unit -> unit
 851     val testit : TextIO.outstream -> unit
 852   end;
 853
 854 (* the benchmark *)
 855 structure Main : BMARK =
 856   struct
 857
 858     open Terms;
 859     open Boyer;
 860
 861 val subst =
 862 [Bind(23,
 863              Prop
 864               (get "f",
 865                [Prop
 866                 (get "plus",
 867                  [Prop (get "plus",[Var 0, Var 1]),
 868                   Prop (get "plus",[Var 2, Prop (get "zero",[])])])])),
 869  Bind(24,
 870              Prop
 871               (get "f",
 872                [Prop
 873                 (get "times",
 874                  [Prop (get "times",[Var 0, Var 1]),
 875                   Prop (get "plus",[Var 2, Var 3])])])),
 876  Bind(25,
 877              Prop
 878               (get "f",
 879                [Prop
 880                 (get "reverse",
 881                  [Prop
 882                   (get "append",
 883                    [Prop (get "append",[Var 0, Var 1]),
 884                     Prop (get "nil",[])])])])),
 885  Bind(20,
 886              Prop
 887               (get "equal",
 888                [Prop (get "plus",[Var 0, Var 1]),
 889                 Prop (get "difference",[Var 23, Var 24])])),
 890  Bind(22,
 891              Prop
 892               (get "lt",
 893                [Prop (get "remainder",[Var 0, Var 1]),
 894                 Prop (get "member",[Var 0, Prop (get "length",[Var 1])])]))]
 895
 896 val term =
 897            Prop
 898             (get "implies",
 899              [Prop
 900               (get "and",
 901                [Prop (get "implies",[Var 23, Var 24]),
 902                 Prop
 903                 (get "and",
 904                  [Prop (get "implies",[Var 24, Var 25]),
 905                   Prop
 906                   (get "and",
 907                    [Prop (get "implies",[Var 25, Var 20]),
 908                     Prop (get "implies",[Var 20, Var 22])])])]),
 909               Prop (get "implies",[Var 23, Var 22])])
 910
 911     fun testit outstrm = if tautp (apply_subst subst term)
 912           then TextIO.output (outstrm, "Proved!\n")
 913           else TextIO.output (outstrm, "Cannot prove!\n")
 914
 915     fun doit () = (tautp (apply_subst subst term); ())
 916
 917   end; (* Main *)
 918
 919 structure Main =
 920   struct
 921     val doit =
 922        fn n =>
 923        let
 924           fun loop n =
 925              if n = 0
 926                 then ()
 927              else (Main.doit ();
 928                    loop(n-1))
 929        in loop n
 930        end
 931   end;