code:
;  This is adapted from a benchmark written by John Ellis and Pete Kovac
;  of Post Communications.
;  It was modified by Hans Boehm of Silicon Graphics.
;  It was translated into Scheme by William D Clinger of Northeastern Univ;
;    the Scheme version uses (RUN-BENCHMARK <string> <thunk>)
;  It was later hacked by Lars T Hansen of Northeastern University;
;    this version has a fixed tree height but accepts a number of
;    iterations to run.
;
;  Modified 2000-02-15 / lth: changed gc-benchmark to only stretch once,
;     and to have a different interface (now accepts iteration numbers,
;     not tree height)
;  Last modified 2000-07-14 / lth -- fixed a buggy comment about storage
;     use in Larceny.
;
;       This is no substitute for real applications.  No actual application
;       is likely to behave in exactly this way.  However, this benchmark was
;       designed to be more representative of real applications than other
;       Java GC benchmarks of which we are aware.
;       It attempts to model those properties of allocation requests that
;       are important to current GC techniques.
;       It is designed to be used either to obtain a single overall performance
;       number, or to give a more detailed estimate of how collector
;       performance varies with object lifetimes.  It prints the time
;       required to allocate and collect balanced binary trees of various
;       sizes.  Smaller trees result in shorter object lifetimes.  Each cycle
;       allocates roughly the same amount of memory.
;       Two data structures are kept around during the entire process, so
;       that the measured performance is representative of applications
;       that maintain some live in-memory data.  One of these is a tree
;       containing many pointers.  The other is a large array containing
;       double precision floating point numbers.  Both should be of comparable
;       size.
;
;       The results are only really meaningful together with a specification
;       of how much memory was used.  It is possible to trade memory for
;       better time performance.  This benchmark should be run in a 32 MB
;       heap, though we don't currently know how to enforce that uniformly.

; In the Java version, this routine prints the heap size and the amount
; of free memory.  There is no portable way to do this in Scheme; each
; implementation needs its own version.

(define (PrintDiagnostics)
  (display " Total memory available= ???????? bytes")
  (display "  Free memory= ???????? bytes")
  (newline))

(define (yes answer) #t)

; Should we implement a Java class as procedures or hygienic macros?
; Take your pick.

(define-syntax let-class
  (syntax-rules
   ()
   ; Put this rule first to implement a class using hygienic macros.
   ((let-class (((method . args) . method-body) ...) . body)
    (letrec-syntax ((method (syntax-rules ()
                              ((method . args) (begin . method-body))))
                    ...)
      . body))
   ; Put this rule first to implement a class using procedures.
   ((let-class (((method . args) . method-body) ...) . body)
    (let () (define (method . args) . method-body) ... . body))
   ))

(define stretch #t)                ; Controls whether stretching phase is run

(define (gcbench kStretchTreeDepth)

  ; Use for inner calls to reduce noise.

  (define (run-benchmark name iters thunk test)
    (do ((i 0 (+ i 1)))
        ((= i iters))
      (thunk)))

  ;  Nodes used by a tree of a given size
  (define (TreeSize i)
    (- (expt 2 (+ i 1)) 1))

  ;  Number of iterations to use for a given tree depth
  (define (NumIters i)
    (quotient (* 2 (TreeSize kStretchTreeDepth))
              (TreeSize i)))

  ;  Parameters are determined by kStretchTreeDepth.
  ;  In Boehm's version the parameters were fixed as follows:
  ;    public static final int kStretchTreeDepth    = 18;  // about 16Mb
  ;    public static final int kLongLivedTreeDepth  = 16;  // about 4Mb
  ;    public static final int kArraySize  = 500000;       // about 4Mb
  ;    public static final int kMinTreeDepth = 4;
  ;    public static final int kMaxTreeDepth = 16;
  ;  wdc: In Larceny the storage numbers above would be 12 Mby, 3 Mby, 6 Mby.
  ;  lth: No they would not.  A flonum requires 16 bytes, so the size
  ;  of array + flonums would be 500,000*4 + 500,000*16=10 Mby.

  (let* ((kLongLivedTreeDepth (- kStretchTreeDepth 2))
         (kArraySize          (* 4 (TreeSize kLongLivedTreeDepth)))
         (kMinTreeDepth       4)
         (kMaxTreeDepth       kLongLivedTreeDepth))

    ; Elements 3 and 4 of the allocated vectors are useless.

    (let-class (((make-node l r)
                 (let ((v (make-empty-node)))
                   (vector-set! v 0 l)
                   (vector-set! v 1 r)
                   v))
                ((make-empty-node) (make-vector 4 0))
                ((node.left node) (vector-ref node 0))
                ((node.right node) (vector-ref node 1))
                ((node.left-set! node x) (vector-set! node 0 x))
                ((node.right-set! node x) (vector-set! node 1 x)))

      ;  Build tree top down, assigning to older objects.
      (define (Populate iDepth thisNode)
        (if (<= iDepth 0)
            #f
            (let ((iDepth (- iDepth 1)))
              (node.left-set! thisNode (make-empty-node))
              (node.right-set! thisNode (make-empty-node))
              (Populate iDepth (node.left thisNode))
              (Populate iDepth (node.right thisNode)))))

      ;  Build tree bottom-up
      (define (MakeTree iDepth)
        (if (<= iDepth 0)
            (make-empty-node)
            (make-node (MakeTree (- iDepth 1))
                       (MakeTree (- iDepth 1)))))

      (define (TimeConstruction depth)
        (let ((iNumIters (NumIters depth)))
          (display (string-append "Creating "
                                  (number->string iNumIters)
                                  " trees of depth "
                                  (number->string depth)))
          (newline)
          (run-benchmark "GCBench: Top down construction"
                         1
                         (lambda ()
                           (do ((i 0 (+ i 1)))
                               ((>= i iNumIters))
                               (Populate depth (make-empty-node))))
                         yes)
          (run-benchmark "GCBench: Bottom up construction"
                         1
                         (lambda ()
                           (do ((i 0 (+ i 1)))
                               ((>= i iNumIters))
                               (MakeTree depth)))
                         yes)))

      (define (main)
        (display "Garbage Collector Test")
        (newline)
        (if stretch
            (begin
              (display (string-append
                        " Stretching memory with a binary tree of depth "
                        (number->string kStretchTreeDepth)))
              (newline)))
        (PrintDiagnostics)
        (run-benchmark "GCBench: Main"
                       1
                       (lambda ()
                         ;  Stretch the memory space quickly
                         (if stretch
                             (MakeTree kStretchTreeDepth))

                         ;  Create a long lived object
                         (display
                          (string-append
                           " Creating a long-lived binary tree of depth "
                           (number->string kLongLivedTreeDepth)))
                         (newline)
                         (let ((longLivedTree (make-empty-node)))
                           (Populate kLongLivedTreeDepth longLivedTree)

                           ;  Create long-lived array, filling half of it
                           (display (string-append
                                     " Creating a long-lived array of "
                                     (number->string kArraySize)
                                     " inexact reals"))
                           (newline)
                           (let ((array (make-vector kArraySize 0.0)))
                             (do ((i 0 (+ i 1)))
                                 ((>= i (quotient kArraySize 2)))
                                 (vector-set! array i
                                              (/ 1.0 (exact->inexact i))))
                             (PrintDiagnostics)

                             (do ((d kMinTreeDepth (+ d 2)))
                                 ((> d kMaxTreeDepth))
                                 (TimeConstruction d))

                             (if (or (eq? longLivedTree '())
                                     (let ((n (min 1000
                                                   (- (quotient (vector-length array)
                                                                2)
                                                      1))))
                                       (not (= (vector-ref array n)
                                               (/ 1.0 (exact->inexact n))))))
                                 (begin (display "Failed") (newline)))
                             ;  fake reference to LongLivedTree
                             ;  and array
                             ;  to keep them from being optimized away
                             )))
                       yes)
        (PrintDiagnostics))

      (main))))

(define (gc-benchmark . rest)
  (let ((k 18)
        (n (if (null? rest) 1 (car rest))))
    (display "The garbage collector should touch about ")
    (display (expt 2 (- k 13)))
    (display " megabytes of heap storage.")
    (newline)
    (display "The use of more or less memory will skew the results.")
    (newline)
    (set! stretch #t)
    (run-benchmark (string-append "GCBench" (number->string k))
                   n
                   (lambda ()
                     (gcbench k)
                     (set! stretch #f))
                   yes)
    (set! stretch #t)))


code:
;
;  GCOld.sch x.x 00/08/03
;  translated from GCOld.java 2.0a 00/08/23
;
; Copyright 2000 Sun Microsystems, Inc. All rights reserved.
;
;

; Should be good enough for this benchmark.

(define (newRandom)
  (letrec ((random14
            (lambda (n)
              (set! x (remainder (+ (* a x) c) m))
              (remainder (quotient x 8) n)))
           (a 701)
           (x 1)
           (c 743483)
           (m 524288)
           (loop
            (lambda (q r n)
              (if (zero? q)
                  (remainder r n)
                  (loop (quotient q 16384)
                        (+ (* 16384 r) (random14 16384))
                        n)))))
    (lambda (n)
      (if (and (exact? n) (integer? n) (< n 16384))
          (random14 n)
          (loop n (random14 16384) n)))))

; A TreeNode is a record with three fields: left, right, val.
; The left and right fields contain a TreeNode or 0, and the
; val field will contain the integer height of the tree.

(define-syntax newTreeNode
  (syntax-rules ()
    ((newTreeNode left right val)
     (vector left right val))
    ((newTreeNode)
     (vector 0 0 0))))

(define-syntax TreeNode.left
  (syntax-rules ()
    ((TreeNode.left node)
     (vector-ref node 0))))

(define-syntax TreeNode.right
  (syntax-rules ()
    ((TreeNode.right node)
     (vector-ref node 1))))

(define-syntax TreeNode.val
  (syntax-rules ()
    ((TreeNode.val node)
     (vector-ref node 2))))

(define-syntax setf
  (syntax-rules (TreeNode.left TreeNode.right TreeNode.val)
    ((setf (TreeNode.left node) x)
     (vector-set! node 0 x))
    ((setf (TreeNode.right node) x)
     (vector-set! node 1 x))
    ((setf (TreeNode.val node) x)
     (vector-set! node 2 x))))

;  Args:
;  live-data-size: in megabytes.
;  work: units of mutator non-allocation work per byte allocated,
;    (in unspecified units.  This will affect the promotion rate
;     printed at the end of the run: more mutator work per step implies
;     fewer steps per second implies fewer bytes promoted per second.)
;  short/long ratio: ratio of short-lived bytes allocated to long-lived
;     bytes allocated.
;  pointer mutation rate: number of pointer mutations per step.
;  steps: number of steps to do.
;

(define (GCOld size workUnits promoteRate ptrMutRate steps)

  (define (println . args)
    (for-each display args)
    (newline))

  ; Rounds an inexact real to two decimal places.

  (define (round2 x)
    (/ (round (* 100.0 x)) 100.0))

  ; Returns the height of the given tree.

  (define (height t)
    (if (eqv? t 0)
        0
        (+ 1 (max (height (TreeNode.left t))
                  (height (TreeNode.right t))))))

  ; Returns the length of the shortest path in the given tree.

  (define (shortestPath t)
    (if (eqv? t 0)
        0
        (+ 1 (min (shortestPath (TreeNode.left t))
                  (shortestPath (TreeNode.right t))))))

  ; Returns the number of nodes in a balanced tree of the given height.

  (define (heightToNodes h)
    (- (expt 2 h) 1))

  ; Returns the height of the largest balanced tree
  ; that has no more than the given number of nodes.

  (define (nodesToHeight nodes)
    (do ((h 1 (+ h 1))
         (n 1 (+ n n)))
        ((> (+ n n -1) nodes)
         (- h 1))))

  (let* (

         ; Constants.

         (null 0)            ; Java's null
         (pathBits 65536)    ; to generate 16 random bits

         (MEG 1000000)
         (INSIGNIFICANT 999) ; this many bytes don't matter
         (bytes/word 4)
         (bytes/node 20)     ; bytes per tree node in typical JVM
         (words/dead 100)    ; size of young garbage objects

         ; Returns the number of bytes in a balanced tree of the given height.

         (heightToBytes
           (lambda (h)
             (* bytes/node (heightToNodes h))))

         ; Returns the height of the largest balanced tree
         ; that occupies no more than the given number of bytes.

         (bytesToHeight
           (lambda (bytes)
             (nodesToHeight (/ bytes bytes/node))))

         (treeHeight 14)
         (treeSize (heightToBytes treeHeight))

         (msg1 "Usage: java GCOld <size> <work> <ratio> <mutation> <steps>")
         (msg2 "  where <size> is the live storage in megabytes")
         (msg3 "        <work> is the mutator work per step (arbitrary units)")
         (msg4 "        <ratio> is the ratio of short-lived to long-lived allocation")
         (msg5 "        <mutation> is the mutations per step")
         (msg6 "        <steps> is the number of steps")

         ; Counters (and global variables that discourage optimization).

         (youngBytes 0)
         (nodes 0)
         (actuallyMut 0)
         (mutatorSum 0)
         (aexport '#())

         ; Global variables.

         (trees '#())
         (where 0)
         (rnd (newRandom))

         )

    ; Returns a newly allocated balanced binary tree of height h.

    (define (makeTree h)
      (if (zero? h)
          null
          (let ((res (newTreeNode)))
            (set! nodes (+ nodes 1))
            (setf (TreeNode.left res) (makeTree (- h 1)))
            (setf (TreeNode.right res) (makeTree (- h 1)))
            (setf (TreeNode.val res) h)
            res)))

    ; Allocates approximately size megabytes of trees and stores
    ; them into a global array.

    (define (init)
      ; Each tree will be about a megabyte.
      (let ((ntrees (quotient (* size MEG) treeSize)))
	(set! trees (make-vector ntrees null))
	(println "Allocating " ntrees " trees.")
        (println "  (" (* ntrees treeSize) " bytes)")
	(do ((i 0 (+ i 1)))
	    ((>= i ntrees))
	  (vector-set! trees i (makeTree treeHeight))
	  (doYoungGenAlloc (* promoteRate ntrees treeSize) words/dead))
	(println "  (" nodes " nodes)")))

    ; Confirms that all trees are balanced and have the correct height.

    (define (checkTrees)
      (let ((ntrees (vector-length trees)))
        (do ((i 0 (+ i 1)))
            ((>= i ntrees))
          (let* ((t (vector-ref trees i))
                 (h1 (height t))
                 (h2 (shortestPath t)))
            (if (or (not (= h1 treeHeight))
                    (not (= h2 treeHeight)))
                (println "*****BUG: " h1 " " h2))))))

    ; Called only by replaceTree (below) and by itself.

    (define (replaceTreeWork full partial dir)
      (let ((canGoLeft (and (not (eq? (TreeNode.left full) null))
			    (> (TreeNode.val (TreeNode.left full))
			       (TreeNode.val partial))))
	    (canGoRight (and (not (eq? (TreeNode.right full) null))
			     (> (TreeNode.val (TreeNode.right full))
			        (TreeNode.val partial)))))
	(cond ((and canGoLeft canGoRight)
	       (if dir
		   (replaceTreeWork (TreeNode.left full)
				    partial
				    (not dir))
		   (replaceTreeWork (TreeNode.right full)
				    partial
				    (not dir))))
	      ((and (not canGoLeft) (not canGoRight))
	       (if dir
		   (setf (TreeNode.left full) partial)
		   (setf (TreeNode.right full) partial)))
	      ((not canGoLeft)
	       (setf (TreeNode.left full) partial))
	      (else
	       (setf (TreeNode.right full) partial)))))

    ; Given a balanced tree full and a smaller balanced tree partial,
    ; replaces an appropriate subtree of full by partial, taking care
    ; to preserve the shape of the full tree.

    (define (replaceTree full partial)
      (let ((dir (zero? (modulo (TreeNode.val partial) 2))))
        (set! actuallyMut (+ actuallyMut 1))
	(replaceTreeWork full partial dir)))

    ; Allocates approximately n bytes of long-lived storage,
    ; replacing oldest existing long-lived storage.

    (define (oldGenAlloc n)
      (let ((full (quotient n treeSize))
	    (partial (modulo n treeSize)))
	;(println "In oldGenAlloc, doing "
	;         full
	;         " full trees and one partial tree of size "
	;         partial)
	(do ((i 0 (+ i 1)))
	    ((>= i full))
	  (vector-set! trees where (makeTree treeHeight))
	  (set! where
                (modulo (+ where 1) (vector-length trees))))
	(let loop ((partial partial))
          (if (> partial INSIGNIFICANT)
              (let* ((h (bytesToHeight partial))
                     (newTree (makeTree h)))
                (replaceTree (vector-ref trees where) newTree)
                (set! where
                      (modulo (+ where 1) (vector-length trees)))
                (loop (- partial (heightToBytes h))))))))

    ; Interchanges two randomly selected subtrees (of same size and depth).

    (define (oldGenSwapSubtrees)
      ; Randomly pick:
      ;   * two tree indices
      ;   * A depth
      ;   * A path to that depth.
      (let* ((index1 (rnd (vector-length trees)))
	     (index2 (rnd (vector-length trees)))
	     (depth (rnd treeHeight))
	     (path (rnd pathBits))
	     (tn1 (vector-ref trees index1))
	     (tn2 (vector-ref trees index2)))
	(do ((i 0 (+ i 1)))
	    ((>= i depth))
	  (if (even? path)
	      (begin (set! tn1 (TreeNode.left tn1))
		     (set! tn2 (TreeNode.left tn2)))
	      (begin (set! tn1 (TreeNode.right tn1))
		     (set! tn2 (TreeNode.right tn2))))
	  (set! path (quotient path 2)))
	(if (even? path)
	    (let ((tmp (TreeNode.left tn1)))
	      (setf (TreeNode.left tn1) (TreeNode.left tn2))
	      (setf (TreeNode.left tn2) tmp))
	    (let ((tmp (TreeNode.right tn1)))
	      (setf (TreeNode.right tn1) (TreeNode.right tn2))
	      (setf (TreeNode.right tn2) tmp)))
	(set! actuallyMut (+ actuallyMut 2))))

    ; Update "n" old-generation pointers.

    (define (oldGenMut n)
      (do ((i 0 (+ i 1)))
	  ((>= i (quotient n 2)))
	(oldGenSwapSubtrees)))

    ; Does the amount of mutator work appropriate for n bytes of young-gen
    ; garbage allocation.

    (define (doMutWork n)
      (let ((limit (quotient (* workUnits n) 10)))
	(do ((k 0 (+ k 1))
	     (sum 0 (+ sum 1)))
	    ((>= k limit)
             ; We don't want dead code elimination to eliminate this loop.
	     (set! mutatorSum (+ mutatorSum sum))))))

    ; Allocate n bytes of young-gen garbage, in units of "nwords"
    ; words.

    (define (doYoungGenAlloc n nwords)
      (let ((nbytes (* nwords bytes/word)))
	(do ((allocated 0 (+ allocated nbytes)))
	    ((>= allocated n)
             (set! youngBytes (+ youngBytes allocated)))
	  (set! aexport (make-vector nwords 0)))))

    ; Allocate "n" bytes of young-gen data; and do the
    ; corresponding amount of old-gen allocation and pointer
    ; mutation.

    ; oldGenAlloc may perform some mutations, so this code
    ; takes those mutations into account.

    (define (doStep n)
      (let ((mutations actuallyMut))
	(doYoungGenAlloc n words/dead)
	(doMutWork n)
	; Now do old-gen allocation
	(oldGenAlloc (quotient n promoteRate))
	(oldGenMut (max 0 (- (+ mutations ptrMutRate) actuallyMut)))))

    (println size " megabytes")
    (println workUnits " work units per step.")
    (println "promotion ratio is 1:" promoteRate)
    (println "pointer mutation rate is " ptrMutRate)
    (println steps " steps")

    (init)
    (checkTrees)
    (set! youngBytes 0)
    (set! nodes 0)

    (println "Initialization complete...")

    (run-benchmark "GCOld"
		   1
		   (lambda ()
                     (lambda ()
                       (do ((step 0 (+ step 1)))
                           ((>= step steps))
                         (doStep MEG))))
                   (lambda (result) #t))

    (checkTrees)

    (println "Allocated " steps " Mb of young gen garbage")
    (println "    (actually allocated "
             (round2 (/ youngBytes MEG))
             " megabytes)")
    (println "Promoted " (round2 (/ steps promoteRate)) " Mb")
    (println "    (actually promoted "
             (round2 (/ (* nodes bytes/node) MEG))
             " megabytes)")
    (if (not (zero? ptrMutRate))
        (println "Mutated " actuallyMut " pointers"))

    ; This output serves mainly to discourage optimization.

    (+ mutatorSum (vector-length aexport))))

(define (gcold-benchmark . args)
  (define gcold-iters 1)

  (GCOld 25 0 10 10 gcold-iters))

license: mit


code:
; Modified 2 March 1997 by Will Clinger to add graphs-benchmark
; and to expand the four macros below.
; Modified 11 June 1997 by Will Clinger to eliminate assertions
; and to replace a use of "recur" with a named let.
;
; Performance note: (graphs-benchmark 7) allocates
;   34509143 pairs
;     389625 vectors with 2551590 elements
;   56653504 closures (not counting top level and known procedures)

(define (graphs-benchmark . rest)
  (let ((N (if (null? rest) 7 (car rest))))
    (run-benchmark (string-append "graphs" (number->string N))
                   (lambda ()
                     (fold-over-rdg N
                                    2
                                    cons
                                    '())))))

; End of new code.

;;; ==== std.ss ====

; (define-syntax assert
;     (syntax-rules ()
; 	((assert test info-rest ...)
; 	    #F)))
;
; (define-syntax deny
;     (syntax-rules ()
; 	((deny test info-rest ...)
; 	    #F)))
;
; (define-syntax when
;     (syntax-rules ()
; 	((when test e-first e-rest ...)
; 	    (if test
; 		(begin e-first
; 		    e-rest ...)))))
;
; (define-syntax unless
;     (syntax-rules ()
; 	((unless test e-first e-rest ...)
; 	    (if (not test)
; 		(begin e-first
; 		    e-rest ...)))))

(define assert
  (lambda (test . info)
    #f))

;;; ==== util.ss ====

; Fold over list elements, associating to the left.
(define fold
    (lambda (lst folder state)
	'(assert (list? lst)
	    lst)
	'(assert (procedure? folder)
	    folder)
	(do ((lst lst
		    (cdr lst))
		(state state
		    (folder (car lst)
			state)))
	    ((null? lst)
		state))))

; Given the size of a vector and a procedure which
; sends indicies to desired vector elements, create
; and return the vector.
(define proc->vector
  (lambda (size f)
    '(assert (and (integer? size)
                 (exact? size)
                 (>= size 0))
      size)
    '(assert (procedure? f)
      f)
    (if (zero? size)
        (vector)
        (let ((x (make-vector size (f 0))))
          (let loop ((i 1))
            (if (< i size) (begin               ; [wdc - was when]
              (vector-set! x i (f i))
              (loop (+ i 1)))))
          x))))

(define vector-fold
    (lambda (vec folder state)
	'(assert (vector? vec)
	    vec)
	'(assert (procedure? folder)
	    folder)
	(let ((len
		    (vector-length vec)))
	    (do ((i 0
			(+ i 1))
		    (state state
			(folder (vector-ref vec i)
			    state)))
		((= i len)
		    state)))))

(define vector-map
    (lambda (vec proc)
	(proc->vector (vector-length vec)
	    (lambda (i)
		(proc (vector-ref vec i))))))

; Given limit, return the list 0, 1, ..., limit-1.
(define giota
    (lambda (limit)
	'(assert (and (integer? limit)
		(exact? limit)
		(>= limit 0))
	    limit)
	(let -*-
	    ((limit
		    limit)
		(res
		    '()))
	    (if (zero? limit)
		res
		(let ((limit
			    (- limit 1)))
		    (-*- limit
			(cons limit res)))))))

; Fold over the integers [0, limit).
(define gnatural-fold
    (lambda (limit folder state)
	'(assert (and (integer? limit)
		(exact? limit)
		(>= limit 0))
	    limit)
	'(assert (procedure? folder)
	    folder)
	(do ((i 0
		    (+ i 1))
		(state state
		    (folder i state)))
	    ((= i limit)
		state))))

; Iterate over the integers [0, limit).
(define gnatural-for-each
    (lambda (limit proc!)
	'(assert (and (integer? limit)
		(exact? limit)
		(>= limit 0))
	    limit)
	'(assert (procedure? proc!)
	    proc!)
	(do ((i 0
		    (+ i 1)))
	    ((= i limit))
	    (proc! i))))

(define natural-for-all?
    (lambda (limit ok?)
	'(assert (and (integer? limit)
		(exact? limit)
		(>= limit 0))
	    limit)
	'(assert (procedure? ok?)
	    ok?)
	(let -*-
	    ((i 0))
	    (or (= i limit)
		(and (ok? i)
		    (-*- (+ i 1)))))))

(define natural-there-exists?
    (lambda (limit ok?)
	'(assert (and (integer? limit)
		(exact? limit)
		(>= limit 0))
	    limit)
	'(assert (procedure? ok?)
	    ok?)
	(let -*-
	    ((i 0))
	    (and (not (= i limit))
		(or (ok? i)
		    (-*- (+ i 1)))))))

(define there-exists?
    (lambda (lst ok?)
	'(assert (list? lst)
	    lst)
	'(assert (procedure? ok?)
	    ok?)
	(let -*-
	    ((lst lst))
	    (and (not (null? lst))
		(or (ok? (car lst))
		    (-*- (cdr lst)))))))

;;; ==== ptfold.ss ====

; Fold over the tree of permutations of a universe.
; Each branch (from the root) is a permutation of universe.
; Each node at depth d corresponds to all permutations which pick the
; elements spelled out on the branch from the root to that node as
; the first d elements.
; Their are two components to the state:
;	The b-state is only a function of the branch from the root.
;	The t-state is a function of all nodes seen so far.
; At each node, b-folder is called via
;	(b-folder elem b-state t-state deeper accross)
; where elem is the next element of the universe picked.
; If b-folder can determine the result of the total tree fold at this stage,
; it should simply return the result.
; If b-folder can determine the result of folding over the sub-tree
; rooted at the resulting node, it should call accross via
;	(accross new-t-state)
; where new-t-state is that result.
; Otherwise, b-folder should call deeper via
;	(deeper new-b-state new-t-state)
; where new-b-state is the b-state for the new node and new-t-state is
; the new folded t-state.
; At the leaves of the tree, t-folder is called via
;	(t-folder b-state t-state accross)
; If t-folder can determine the result of the total tree fold at this stage,
; it should simply return that result.
; If not, it should call accross via
;	(accross new-t-state)
; Note, fold-over-perm-tree always calls b-folder in depth-first order.
; I.e., when b-folder is called at depth d, the branch leading to that
; node is the most recent calls to b-folder at all the depths less than d.
; This is a gross efficiency hack so that b-folder can use mutation to
; keep the current branch.
(define fold-over-perm-tree
    (lambda (universe b-folder b-state t-folder t-state)
	'(assert (list? universe)
	    universe)
	'(assert (procedure? b-folder)
	    b-folder)
	'(assert (procedure? t-folder)
	    t-folder)
	(let -*-
	    ((universe
		    universe)
		(b-state
		    b-state)
		(t-state
		    t-state)
		(accross
		    (lambda (final-t-state)
			final-t-state)))
	    (if (null? universe)
		(t-folder b-state t-state accross)
		(let -**-
		    ((in
			    universe)
			(out
			    '())
			(t-state
			    t-state))
		    (let* ((first
				(car in))
			    (rest
				(cdr in))
			    (accross
				(if (null? rest)
				    accross
				    (lambda (new-t-state)
					(-**- rest
					    (cons first out)
					    new-t-state)))))
			(b-folder first
			    b-state
			    t-state
			    (lambda (new-b-state new-t-state)
				(-*- (fold out cons rest)
				    new-b-state
				    new-t-state
				    accross))
			    accross)))))))

;;; ==== minimal.ss ====

; A directed graph is stored as a connection matrix (vector-of-vectors)
; where the first index is the `from' vertex and the second is the `to'
; vertex.  Each entry is a bool indicating if the edge exists.
; The diagonal of the matrix is never examined.
; Make-minimal? returns a procedure which tests if a labelling
; of the verticies is such that the matrix is minimal.
; If it is, then the procedure returns the result of folding over
; the elements of the automoriphism group.  If not, it returns #F.
; The folding is done by calling folder via
;	(folder perm state accross)
; If the folder wants to continue, it should call accross via
;	(accross new-state)
; If it just wants the entire minimal? procedure to return something,
; it should return that.
; The ordering used is lexicographic (with #T > #F) and entries
; are examined in the following order:
;	1->0, 0->1
;
;	2->0, 0->2
;	2->1, 1->2
;
;	3->0, 0->3
;	3->1, 1->3
;	3->2, 2->3
;	...
(define make-minimal?
    (lambda (max-size)
	'(assert (and (integer? max-size)
		(exact? max-size)
		(>= max-size 0))
	    max-size)
	(let ((iotas
		    (proc->vector (+ max-size 1)
			giota))
		(perm
		    (make-vector max-size 0)))
	    (lambda (size graph folder state)
		'(assert (and (integer? size)
			(exact? size)
			(<= 0 size max-size))
		    size
		    max-size)
		'(assert (vector? graph)
		    graph)
		'(assert (procedure? folder)
		    folder)
		(fold-over-perm-tree (vector-ref iotas size)
		    (lambda (perm-x x state deeper accross)
			(case (cmp-next-vertex graph perm x perm-x)
			    ((less)
				#F)
			    ((equal)
				(vector-set! perm x perm-x)
				(deeper (+ x 1)
				    state))
			    ((more)
				(accross state))
			    (else
				(assert #F))))
		    0
		    (lambda (leaf-depth state accross)
			'(assert (eqv? leaf-depth size)
			    leaf-depth
			    size)
			(folder perm state accross))
		    state)))))

; Given a graph, a partial permutation vector, the next input and the next
; output, return 'less, 'equal or 'more depending on the lexicographic
; comparison between the permuted and un-permuted graph.
(define cmp-next-vertex
    (lambda (graph perm x perm-x)
	(let ((from-x
		    (vector-ref graph x))
		(from-perm-x
		    (vector-ref graph perm-x)))
	    (let -*-
		((y
			0))
		(if (= x y)
		    'equal
		    (let ((x->y?
				(vector-ref from-x y))
			    (perm-y
				(vector-ref perm y)))
			(cond ((eq? x->y?
				    (vector-ref from-perm-x perm-y))
				(let ((y->x?
					    (vector-ref (vector-ref graph y)
						x)))
				    (cond ((eq? y->x?
						(vector-ref (vector-ref graph perm-y)
						    perm-x))
					    (-*- (+ y 1)))
					(y->x?
					    'less)
					(else
					    'more))))
			    (x->y?
				'less)
			    (else
				'more))))))))

;;; ==== rdg.ss ====

; Fold over rooted directed graphs with bounded out-degree.
; Size is the number of verticies (including the root).  Max-out is the
; maximum out-degree for any vertex.  Folder is called via
;	(folder edges state)
; where edges is a list of length size.  The ith element of the list is
; a list of the verticies j for which there is an edge from i to j.
; The last vertex is the root.
(define fold-over-rdg
    (lambda (size max-out folder state)
	'(assert (and (exact? size)
		(integer? size)
		(> size 0))
	    size)
	'(assert (and (exact? max-out)
		(integer? max-out)
		(>= max-out 0))
	    max-out)
	'(assert (procedure? folder)
	    folder)
	(let* ((root
		    (- size 1))
		(edge?
		    (proc->vector size
			(lambda (from)
			    (make-vector size #F))))
		(edges
		    (make-vector size '()))
		(out-degrees
		    (make-vector size 0))
		(minimal-folder
		    (make-minimal? root))
		(non-root-minimal?
		    (let ((cont
				(lambda (perm state accross)
				    '(assert (eq? state #T)
					state)
				    (accross #T))))
			(lambda (size)
			    (minimal-folder size
				edge?
				cont
				#T))))
		(root-minimal?
		    (let ((cont
				(lambda (perm state accross)
				    '(assert (eq? state #T)
					state)
				    (case (cmp-next-vertex edge? perm root root)
					((less)
					    #F)
					((equal more)
					    (accross #T))
					(else
					    (assert #F))))))
			(lambda ()
			    (minimal-folder root
				edge?
				cont
				#T)))))
	    (let -*-
		((vertex
			0)
		    (state
			state))
		(cond ((not (non-root-minimal? vertex))
			state)
		    ((= vertex root)
			'(assert
			    (begin
				(gnatural-for-each root
				    (lambda (v)
					'(assert (= (vector-ref out-degrees v)
						(length (vector-ref edges v)))
					    v
					    (vector-ref out-degrees v)
					    (vector-ref edges v))))
				#T))
			(let ((reach?
				    (make-reach? root edges))
				(from-root
				    (vector-ref edge? root)))
			    (let -*-
				((v
					0)
				    (outs
					0)
				    (efr
					'())
				    (efrr
					'())
				    (state
					state))
				(cond ((not (or (= v root)
						(= outs max-out)))
					(vector-set! from-root v #T)
					(let ((state
						    (-*- (+ v 1)
							(+ outs 1)
							(cons v efr)
							(cons (vector-ref reach? v)
							    efrr)
							state)))
					    (vector-set! from-root v #F)
					    (-*- (+ v 1)
						outs
						efr
						efrr
						state)))
				    ((and (natural-for-all? root
						(lambda (v)
						    (there-exists? efrr
							(lambda (r)
							    (vector-ref r v)))))
					    (root-minimal?))
					(vector-set! edges root efr)
					(folder
					    (proc->vector size
						(lambda (i)
						    (vector-ref edges i)))
					    state))
				    (else
					state)))))
		    (else
			(let ((from-vertex
				    (vector-ref edge? vertex)))
			    (let -**-
				((sv
					0)
				    (outs
					0)
				    (state
					state))
				(if (= sv vertex)
				    (begin
					(vector-set! out-degrees vertex outs)
					(-*- (+ vertex 1)
					    state))
				    (let* ((state
						; no sv->vertex, no vertex->sv
						(-**- (+ sv 1)
						    outs
						    state))
					    (from-sv
						(vector-ref edge? sv))
					    (sv-out
						(vector-ref out-degrees sv))
					    (state
						(if (= sv-out max-out)
						    state
						    (begin
							(vector-set! edges
							    sv
							    (cons vertex
								(vector-ref edges sv)))
							(vector-set! from-sv vertex #T)
							(vector-set! out-degrees sv (+ sv-out 1))
							(let* ((state
								    ; sv->vertex, no vertex->sv
								    (-**- (+ sv 1)
									outs
									state))
								(state
								    (if (= outs max-out)
									state
									(begin
									    (vector-set! from-vertex sv #T)
									    (vector-set! edges
										vertex
										(cons sv
										    (vector-ref edges vertex)))
									    (let ((state
											; sv->vertex, vertex->sv
											(-**- (+ sv 1)
											    (+ outs 1)
											    state)))
										(vector-set! edges
										    vertex
										    (cdr (vector-ref edges vertex)))
										(vector-set! from-vertex sv #F)
										state)))))
							    (vector-set! out-degrees sv sv-out)
							    (vector-set! from-sv vertex #F)
							    (vector-set! edges
								sv
								(cdr (vector-ref edges sv)))
							    state)))))
					(if (= outs max-out)
					    state
					    (begin
						(vector-set! edges
						    vertex
						    (cons sv
							(vector-ref edges vertex)))
						(vector-set! from-vertex sv #T)
						(let ((state
							    ; no sv->vertex, vertex->sv
							    (-**- (+ sv 1)
								(+ outs 1)
								state)))
						    (vector-set! from-vertex sv #F)
						    (vector-set! edges
							vertex
							(cdr (vector-ref edges vertex)))
						    state)))))))))))))

; Given a vector which maps vertex to out-going-edge list,
; return a vector  which gives reachability.
(define make-reach?
    (lambda (size vertex->out)
	(let ((res
		    (proc->vector size
			(lambda (v)
			    (let ((from-v
					(make-vector size #F)))
				(vector-set! from-v v #T)
				(for-each
				    (lambda (x)
					(vector-set! from-v x #T))
				    (vector-ref vertex->out v))
				from-v)))))
	    (gnatural-for-each size
		(lambda (m)
		    (let ((from-m
				(vector-ref res m)))
			(gnatural-for-each size
			    (lambda (f)
				(let ((from-f
					    (vector-ref res f)))
				    (if (vector-ref from-f m); [wdc - was when]
                                       (begin
					(gnatural-for-each size
					    (lambda (t)
						(if (vector-ref from-m t)
                                                   (begin ; [wdc - was when]
						    (vector-set! from-f t #T)))))))))))))
	    res)))

;;; ==== test input ====

; Produces all directed graphs with N verticies, distinguished root,
; and out-degree bounded by 2, upto isomorphism (there are 44).

;(define go
;  (let ((N 7))
;    (fold-over-rdg N
;      2
;      cons
;      '())))


code:
; This benchmark was obtained from Andrew Wright.
; 970215 / wdc Added lattice-benchmark.

; Given a comparison routine that returns one of
;	less
;	more
;	equal
;	uncomparable
; return a new comparison routine that applies to sequences.
(define lexico
    (lambda (base)
	(define lex-fixed
	    (lambda (fixed lhs rhs)
		(define check
		    (lambda (lhs rhs)
			(if (null? lhs)
			    fixed
			    (let ((probe
					(base (car lhs)
					    (car rhs))))
				(if (or (eq? probe 'equal)
					(eq? probe fixed))
				    (check (cdr lhs)
					(cdr rhs))
				    'uncomparable)))))
		(check lhs rhs)))
	(define lex-first
	    (lambda (lhs rhs)
		(if (null? lhs)
		    'equal
		    (let ((probe
				(base (car lhs)
				    (car rhs))))
			(case probe
			    ((less more)
				(lex-fixed probe
				    (cdr lhs)
				    (cdr rhs)))
			    ((equal)
				(lex-first (cdr lhs)
				    (cdr rhs)))
			    ((uncomparable)
				'uncomparable))))))
	lex-first))

(define (make-lattice elem-list cmp-func)
    (cons elem-list cmp-func))

(define lattice->elements car)

(define lattice->cmp cdr)

; Select elements of a list which pass some test.
(define zulu-select
    (lambda (test lst)
	(define select-a
	    (lambda (ac lst)
		(if (null? lst)
		    (reverse! ac)
		    (select-a
			(let ((head (car lst)))
			    (if (test head)
				(cons head ac)
				ac))
			(cdr lst)))))
	(select-a '() lst)))

(define reverse!
    (letrec ((rotate
		(lambda (fo fum)
		    (let ((next (cdr fo)))
			(set-cdr! fo fum)
			(if (null? next)
			    fo
			    (rotate next fo))))))
	(lambda (lst)
	    (if (null? lst)
		'()
		(rotate lst '())))))

; Select elements of a list which pass some test and map a function
; over the result.  Note, only efficiency prevents this from being the
; composition of select and map.
(define select-map
    (lambda (test func lst)
	(define select-a
	    (lambda (ac lst)
		(if (null? lst)
		    (reverse! ac)
		    (select-a
			(let ((head (car lst)))
			    (if (test head)
				(cons (func head)
				    ac)
				ac))
			(cdr lst)))))
	(select-a '() lst)))

; This version of map-and tail-recurses on the last test.
(define map-and
    (lambda (proc lst)
	(if (null? lst)
	    #T
	    (letrec ((drudge
			(lambda (lst)
			    (let ((rest (cdr lst)))
				(if (null? rest)
				    (proc (car lst))
				    (and (proc (car lst))
					(drudge rest)))))))
		(drudge lst)))))

(define (maps-1 source target pas new)
    (let ((scmp (lattice->cmp source))
	    (tcmp (lattice->cmp target)))
	(let ((less
		    (select-map
			(lambda (p)
			    (eq? 'less
				(scmp (car p) new)))
			cdr
			pas))
		(more
		    (select-map
			(lambda (p)
			    (eq? 'more
				(scmp (car p) new)))
			cdr
			pas)))
	    (zulu-select
		(lambda (t)
		    (and
			(map-and
			    (lambda (t2)
				(memq (tcmp t2 t) '(less equal)))
			    less)
			(map-and
			    (lambda (t2)
				(memq (tcmp t2 t) '(more equal)))
			    more)))
		(lattice->elements target)))))

(define (maps-rest source target pas rest to-1 to-collect)
    (if (null? rest)
	(to-1 pas)
	(let ((next (car rest))
		(rest (cdr rest)))
	    (to-collect
		(map
		    (lambda (x)
			(maps-rest source target
			    (cons
				(cons next x)
				pas)
			    rest
			    to-1
			    to-collect))
		    (maps-1 source target pas next))))))

(define (maps source target)
    (make-lattice
	(maps-rest source
	    target
	    '()
	    (lattice->elements source)
	    (lambda (x) (list (map cdr x)))
	    (lambda (x) (apply append x)))
	(lexico (lattice->cmp target))))

(define print-frequency 10000)

(define (count-maps source target)
    (let ((count 0))
	(maps-rest source
	    target
	    '()
	    (lattice->elements source)
	    (lambda (x)
		(set! count (+ count 1))
		(if (= 0 (remainder count print-frequency))
		    (begin #f))
		1)
	    (lambda (x) (apply + x)))))

(define (lattice-benchmark)
  (run-benchmark "Lattice"
    (lambda ()
      (let* ((l2
	      (make-lattice '(low high)
			    (lambda (lhs rhs)
			      (case lhs
				((low)
				 (case rhs
				   ((low)
				    'equal)
				   ((high)
				    'less)
				   (else
				    (error 'make-lattice "base" rhs))))
				((high)
				 (case rhs
				   ((low)
				    'more)
				   ((high)
				    'equal)
				   (else
				    (error 'make-lattice "base" rhs))))
				(else
				 (error 'make-lattice "base" lhs))))))
	     (l3 (maps l2 l2))
	     (l4 (maps l3 l3)))
	(count-maps l2 l2)
	(count-maps l3 l3)
	(count-maps l2 l3)
	(count-maps l3 l2)
	(count-maps l4 l4)))))


code:
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; File:         nboyer.sch
; Description:  The Boyer benchmark
; Author:       Bob Boyer
; Created:      5-Apr-85
; Modified:     10-Apr-85 14:52:20 (Bob Shaw)
;               22-Jul-87 (Will Clinger)
;               2-Jul-88 (Will Clinger -- distinguished #f and the empty list)
;               13-Feb-97 (Will Clinger -- fixed bugs in unifier and rules,
;                          rewrote to eliminate property lists, and added
;                          a scaling parameter suggested by Bob Boyer)
;               19-Mar-99 (Will Clinger -- cleaned up comments)
;               4-Apr-01 (Will Clinger -- changed four 1- symbols to sub1)
; Language:     Scheme
; Status:       Public Domain
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; NBOYER -- Logic programming benchmark, originally written by Bob Boyer.
;;; Fairly CONS intensive.

; Note:  The version of this benchmark that appears in Dick Gabriel's book
; contained several bugs that are corrected here.  These bugs are discussed
; by Henry Baker, "The Boyer Benchmark Meets Linear Logic", ACM SIGPLAN Lisp
; Pointers 6(4), October-December 1993, pages 3-10.  The fixed bugs are:
;
;    The benchmark now returns a boolean result.
;    FALSEP and TRUEP use TERM-MEMBER? rather than MEMV (which is called MEMBER
;         in Common Lisp)
;    ONE-WAY-UNIFY1 now treats numbers correctly
;    ONE-WAY-UNIFY1-LST now treats empty lists correctly
;    Rule 19 has been corrected (this rule was not touched by the original
;         benchmark, but is used by this version)
;    Rules 84 and 101 have been corrected (but these rules are never touched
;         by the benchmark)
;
; According to Baker, these bug fixes make the benchmark 10-25% slower.
; Please do not compare the timings from this benchmark against those of
; the original benchmark.
;
; This version of the benchmark also prints the number of rewrites as a sanity
; check, because it is too easy for a buggy version to return the correct
; boolean result.  The correct number of rewrites is
;
;     n      rewrites       peak live storage (approximate, in bytes)
;     0         95024           520,000
;     1        591777         2,085,000
;     2       1813975         5,175,000
;     3       5375678
;     4      16445406
;     5      51507739

; Nboyer is a 2-phase benchmark.
; The first phase attaches lemmas to symbols.  This phase is not timed,
; but it accounts for very little of the runtime anyway.
; The second phase creates the test problem, and tests to see
; whether it is implied by the lemmas.

(define (nboyer-benchmark . args)
  (let ((n (if (null? args) 0 (car args))))
    (setup-boyer)
    (run-benchmark (string-append "nboyer"
                                  (number->string n))
                   1
                   (lambda () (test-boyer n))
                   (lambda (rewrites)
                     (and (number? rewrites)
                          (case n
                           ((0)  (= rewrites 95024))
                           ((1)  (= rewrites 591777))
                           ((2)  (= rewrites 1813975))
                           ((3)  (= rewrites 5375678))
                           ((4)  (= rewrites 16445406))
                           ((5)  (= rewrites 51507739))
                           ; If it works for n <= 5, assume it works.
                           (else #t)))))))

(define (setup-boyer) #t) ; assigned below
(define (test-boyer) #t)  ; assigned below

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; The first phase.
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; In the original benchmark, it stored a list of lemmas on the
; property lists of symbols.
; In the new benchmark, it maintains an association list of
; symbols and symbol-records, and stores the list of lemmas
; within the symbol-records.

(let ()

  (define (setup)
    (add-lemma-lst
     (quote ((equal (compile form)
                    (reverse (codegen (optimize form)
                                      (nil))))
             (equal (eqp x y)
                    (equal (fix x)
                           (fix y)))
             (equal (greaterp x y)
                    (lessp y x))
             (equal (lesseqp x y)
                    (not (lessp y x)))
             (equal (greatereqp x y)
                    (not (lessp x y)))
             (equal (boolean x)
                    (or (equal x (t))
                        (equal x (f))))
             (equal (iff x y)
                    (and (implies x y)
                         (implies y x)))
             (equal (even1 x)
                    (if (zerop x)
                        (t)
                        (odd (sub1 x))))
             (equal (countps- l pred)
                    (countps-loop l pred (zero)))
             (equal (fact- i)
                    (fact-loop i 1))
             (equal (reverse- x)
                    (reverse-loop x (nil)))
             (equal (divides x y)
                    (zerop (remainder y x)))
             (equal (assume-true var alist)
                    (cons (cons var (t))
                          alist))
             (equal (assume-false var alist)
                    (cons (cons var (f))
                          alist))
             (equal (tautology-checker x)
                    (tautologyp (normalize x)
                                (nil)))
             (equal (falsify x)
                    (falsify1 (normalize x)
                              (nil)))
             (equal (prime x)
                    (and (not (zerop x))
                         (not (equal x (add1 (zero))))
                         (prime1 x (sub1 x))))
             (equal (and p q)
                    (if p (if q (t)
                                (f))
                          (f)))
             (equal (or p q)
                    (if p (t)
                          (if q (t)
                                (f))))
             (equal (not p)
                    (if p (f)
                          (t)))
             (equal (implies p q)
                    (if p (if q (t)
                                (f))
                          (t)))
             (equal (fix x)
                    (if (numberp x)
                        x
                        (zero)))
             (equal (if (if a b c)
                        d e)
                    (if a (if b d e)
                          (if c d e)))
             (equal (zerop x)
                    (or (equal x (zero))
                        (not (numberp x))))
             (equal (plus (plus x y)
                          z)
                    (plus x (plus y z)))
             (equal (equal (plus a b)
                           (zero))
                    (and (zerop a)
                         (zerop b)))
             (equal (difference x x)
                    (zero))
             (equal (equal (plus a b)
                           (plus a c))
                    (equal (fix b)
                           (fix c)))
             (equal (equal (zero)
                           (difference x y))
                    (not (lessp y x)))
             (equal (equal x (difference x y))
                    (and (numberp x)
                         (or (equal x (zero))
                             (zerop y))))
             (equal (meaning (plus-tree (append x y))
                             a)
                    (plus (meaning (plus-tree x)
                                   a)
                          (meaning (plus-tree y)
                                   a)))
             (equal (meaning (plus-tree (plus-fringe x))
                             a)
                    (fix (meaning x a)))
             (equal (append (append x y)
                            z)
                    (append x (append y z)))
             (equal (reverse (append a b))
                    (append (reverse b)
                            (reverse a)))
             (equal (times x (plus y z))
                    (plus (times x y)
                          (times x z)))
             (equal (times (times x y)
                           z)
                    (times x (times y z)))
             (equal (equal (times x y)
                           (zero))
                    (or (zerop x)
                        (zerop y)))
             (equal (exec (append x y)
                          pds envrn)
                    (exec y (exec x pds envrn)
                            envrn))
             (equal (mc-flatten x y)
                    (append (flatten x)
                            y))
             (equal (member x (append a b))
                    (or (member x a)
                        (member x b)))
             (equal (member x (reverse y))
                    (member x y))
             (equal (length (reverse x))
                    (length x))
             (equal (member a (intersect b c))
                    (and (member a b)
                         (member a c)))
             (equal (nth (zero)
                         i)
                    (zero))
             (equal (exp i (plus j k))
                    (times (exp i j)
                           (exp i k)))
             (equal (exp i (times j k))
                    (exp (exp i j)
                         k))
             (equal (reverse-loop x y)
                    (append (reverse x)
                            y))
             (equal (reverse-loop x (nil))
                    (reverse x))
             (equal (count-list z (sort-lp x y))
                    (plus (count-list z x)
                          (count-list z y)))
             (equal (equal (append a b)
                           (append a c))
                    (equal b c))
             (equal (plus (remainder x y)
                          (times y (quotient x y)))
                    (fix x))
             (equal (power-eval (big-plus1 l i base)
                                base)
                    (plus (power-eval l base)
                          i))
             (equal (power-eval (big-plus x y i base)
                                base)
                    (plus i (plus (power-eval x base)
                                  (power-eval y base))))
             (equal (remainder y 1)
                    (zero))
             (equal (lessp (remainder x y)
                           y)
                    (not (zerop y)))
             (equal (remainder x x)
                    (zero))
             (equal (lessp (quotient i j)
                           i)
                    (and (not (zerop i))
                         (or (zerop j)
                             (not (equal j 1)))))
             (equal (lessp (remainder x y)
                           x)
                    (and (not (zerop y))
                         (not (zerop x))
                         (not (lessp x y))))
             (equal (power-eval (power-rep i base)
                                base)
                    (fix i))
             (equal (power-eval (big-plus (power-rep i base)
                                          (power-rep j base)
                                          (zero)
                                          base)
                                base)
                    (plus i j))
             (equal (gcd x y)
                    (gcd y x))
             (equal (nth (append a b)
                         i)
                    (append (nth a i)
                            (nth b (difference i (length a)))))
             (equal (difference (plus x y)
                                x)
                    (fix y))
             (equal (difference (plus y x)
                                x)
                    (fix y))
             (equal (difference (plus x y)
                                (plus x z))
                    (difference y z))
             (equal (times x (difference c w))
                    (difference (times c x)
                                (times w x)))
             (equal (remainder (times x z)
                               z)
                    (zero))
             (equal (difference (plus b (plus a c))
                                a)
                    (plus b c))
             (equal (difference (add1 (plus y z))
                                z)
                    (add1 y))
             (equal (lessp (plus x y)
                           (plus x z))
                    (lessp y z))
             (equal (lessp (times x z)
                           (times y z))
                    (and (not (zerop z))
                         (lessp x y)))
             (equal (lessp y (plus x y))
                    (not (zerop x)))
             (equal (gcd (times x z)
                         (times y z))
                    (times z (gcd x y)))
             (equal (value (normalize x)
                           a)
                    (value x a))
             (equal (equal (flatten x)
                           (cons y (nil)))
                    (and (nlistp x)
                         (equal x y)))
             (equal (listp (gopher x))
                    (listp x))
             (equal (samefringe x y)
                    (equal (flatten x)
                           (flatten y)))
             (equal (equal (greatest-factor x y)
                           (zero))
                    (and (or (zerop y)
                             (equal y 1))
                         (equal x (zero))))
             (equal (equal (greatest-factor x y)
                           1)
                    (equal x 1))
             (equal (numberp (greatest-factor x y))
                    (not (and (or (zerop y)
                                  (equal y 1))
                              (not (numberp x)))))
             (equal (times-list (append x y))
                    (times (times-list x)
                           (times-list y)))
             (equal (prime-list (append x y))
                    (and (prime-list x)
                         (prime-list y)))
             (equal (equal z (times w z))
                    (and (numberp z)
                         (or (equal z (zero))
                             (equal w 1))))
             (equal (greatereqp x y)
                    (not (lessp x y)))
             (equal (equal x (times x y))
                    (or (equal x (zero))
                        (and (numberp x)
                             (equal y 1))))
             (equal (remainder (times y x)
                               y)
                    (zero))
             (equal (equal (times a b)
                           1)
                    (and (not (equal a (zero)))
                         (not (equal b (zero)))
                         (numberp a)
                         (numberp b)
                         (equal (sub1 a)
                                (zero))
                         (equal (sub1 b)
                                (zero))))
             (equal (lessp (length (delete x l))
                           (length l))
                    (member x l))
             (equal (sort2 (delete x l))
                    (delete x (sort2 l)))
             (equal (dsort x)
                    (sort2 x))
             (equal (length (cons x1
                                  (cons x2
                                        (cons x3 (cons x4
                                                       (cons x5
                                                             (cons x6 x7)))))))
                    (plus 6 (length x7)))
             (equal (difference (add1 (add1 x))
                                2)
                    (fix x))
             (equal (quotient (plus x (plus x y))
                              2)
                    (plus x (quotient y 2)))
             (equal (sigma (zero)
                           i)
                    (quotient (times i (add1 i))
                              2))
             (equal (plus x (add1 y))
                    (if (numberp y)
                        (add1 (plus x y))
                        (add1 x)))
             (equal (equal (difference x y)
                           (difference z y))
                    (if (lessp x y)
                        (not (lessp y z))
                        (if (lessp z y)
                            (not (lessp y x))
                            (equal (fix x)
                                   (fix z)))))
             (equal (meaning (plus-tree (delete x y))
                             a)
                    (if (member x y)
                        (difference (meaning (plus-tree y)
                                             a)
                                    (meaning x a))
                        (meaning (plus-tree y)
                                 a)))
             (equal (times x (add1 y))
                    (if (numberp y)
                        (plus x (times x y))
                        (fix x)))
             (equal (nth (nil)
                         i)
                    (if (zerop i)
                        (nil)
                        (zero)))
             (equal (last (append a b))
                    (if (listp b)
                        (last b)
                        (if (listp a)
                            (cons (car (last a))
                                  b)
                            b)))
             (equal (equal (lessp x y)
                           z)
                    (if (lessp x y)
                        (equal (t) z)
                        (equal (f) z)))
             (equal (assignment x (append a b))
                    (if (assignedp x a)
                        (assignment x a)
                        (assignment x b)))
             (equal (car (gopher x))
                    (if (listp x)
                        (car (flatten x))
                        (zero)))
             (equal (flatten (cdr (gopher x)))
                    (if (listp x)
                        (cdr (flatten x))
                        (cons (zero)
                              (nil))))
             (equal (quotient (times y x)
                              y)
                    (if (zerop y)
                        (zero)
                        (fix x)))
             (equal (get j (set i val mem))
                    (if (eqp j i)
                        val
                        (get j mem)))))))

  (define (add-lemma-lst lst)
    (cond ((null? lst)
           #t)
          (else (add-lemma (car lst))
                (add-lemma-lst (cdr lst)))))

  (define (add-lemma term)
    (cond ((and (pair? term)
                (eq? (car term)
                     (quote equal))
                (pair? (cadr term)))
           (put (car (cadr term))
                (quote lemmas)
                (cons
                 (translate-term term)
                 (get (car (cadr term)) (quote lemmas)))))
          (else (error "ADD-LEMMA did not like term:  " term))))

  ; Translates a term by replacing its constructor symbols by symbol-records.

  (define (translate-term term)
    (cond ((not (pair? term))
           term)
          (else (cons (symbol->symbol-record (car term))
                      (translate-args (cdr term))))))

  (define (translate-args lst)
    (cond ((null? lst)
           '())
          (else (cons (translate-term (car lst))
                      (translate-args (cdr lst))))))

  ; For debugging only, so the use of MAP does not change
  ; the first-order character of the benchmark.

  (define (untranslate-term term)
    (cond ((not (pair? term))
           term)
          (else (cons (get-name (car term))
                      (map untranslate-term (cdr term))))))

  ; A symbol-record is represented as a vector with two fields:
  ; the symbol (for debugging) and
  ; the list of lemmas associated with the symbol.

  (define (put sym property value)
    (put-lemmas! (symbol->symbol-record sym) value))

  (define (get sym property)
    (get-lemmas (symbol->symbol-record sym)))

  (define (symbol->symbol-record sym)
    (let ((x (assq sym *symbol-records-alist*)))
      (if x
          (cdr x)
          (let ((r (make-symbol-record sym)))
            (set! *symbol-records-alist*
                  (cons (cons sym r)
                        *symbol-records-alist*))
            r))))

  ; Association list of symbols and symbol-records.

  (define *symbol-records-alist* '())

  ; A symbol-record is represented as a vector with two fields:
  ; the symbol (for debugging) and
  ; the list of lemmas associated with the symbol.

  (define (make-symbol-record sym)
    (vector sym '()))

  (define (put-lemmas! symbol-record lemmas)
    (vector-set! symbol-record 1 lemmas))

  (define (get-lemmas symbol-record)
    (vector-ref symbol-record 1))

  (define (get-name symbol-record)
    (vector-ref symbol-record 0))

  (define (symbol-record-equal? r1 r2)
    (eq? r1 r2))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;
  ; The second phase.
  ;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (test n)
    (let ((term
           (apply-subst
            (translate-alist
             (quote ((x f (plus (plus a b)
                                (plus c (zero))))
                     (y f (times (times a b)
                                 (plus c d)))
                     (z f (reverse (append (append a b)
                                           (nil))))
                     (u equal (plus a b)
                              (difference x y))
                     (w lessp (remainder a b)
                              (member a (length b))))))
            (translate-term
             (do ((term
                   (quote (implies (and (implies x y)
                                        (and (implies y z)
                                             (and (implies z u)
                                                  (implies u w))))
                                   (implies x w)))
                   (list 'or term '(f)))
                  (n n (- n 1)))
                 ((zero? n) term))))))
    (tautp term)))

  (define (translate-alist alist)
    (cond ((null? alist)
           '())
          (else (cons (cons (caar alist)
                            (translate-term (cdar alist)))
                      (translate-alist (cdr alist))))))

  (define (apply-subst alist term)
    (cond ((not (pair? term))
           (let ((temp-temp (assq term alist)))
             (if temp-temp
                 (cdr temp-temp)
                 term)))
          (else (cons (car term)
                      (apply-subst-lst alist (cdr term))))))

  (define (apply-subst-lst alist lst)
    (cond ((null? lst)
           '())
          (else (cons (apply-subst alist (car lst))
                      (apply-subst-lst alist (cdr lst))))))

  (define (tautp x)
    (tautologyp (rewrite x)
                '() '()))

  (define (tautologyp x true-lst false-lst)
    (cond ((truep x true-lst)
           #t)
          ((falsep x false-lst)
           #f)
          ((not (pair? x))
           #f)
          ((eq? (car x) if-constructor)
           (cond ((truep (cadr x)
                         true-lst)
                  (tautologyp (caddr x)
                              true-lst false-lst))
                 ((falsep (cadr x)
                          false-lst)
                  (tautologyp (cadddr x)
                              true-lst false-lst))
                 (else (and (tautologyp (caddr x)
                                        (cons (cadr x)
                                              true-lst)
                                        false-lst)
                            (tautologyp (cadddr x)
                                        true-lst
                                        (cons (cadr x)
                                              false-lst))))))
          (else #f)))

  (define if-constructor '*) ; becomes (symbol->symbol-record 'if)

  (define rewrite-count 0) ; sanity check

  (define (rewrite term)
    (set! rewrite-count (+ rewrite-count 1))
    (cond ((not (pair? term))
           term)
          (else (rewrite-with-lemmas (cons (car term)
                                           (rewrite-args (cdr term)))
                                     (get-lemmas (car term))))))

  (define (rewrite-args lst)
    (cond ((null? lst)
           '())
          (else (cons (rewrite (car lst))
                      (rewrite-args (cdr lst))))))

  (define (rewrite-with-lemmas term lst)
    (cond ((null? lst)
           term)
          ((one-way-unify term (cadr (car lst)))
           (rewrite (apply-subst unify-subst (caddr (car lst)))))
          (else (rewrite-with-lemmas term (cdr lst)))))

  (define unify-subst '*)

  (define (one-way-unify term1 term2)
    (begin (set! unify-subst '())
           (one-way-unify1 term1 term2)))

  (define (one-way-unify1 term1 term2)
    (cond ((not (pair? term2))
           (let ((temp-temp (assq term2 unify-subst)))
             (cond (temp-temp
                    (term-equal? term1 (cdr temp-temp)))
                   ((number? term2)          ; This bug fix makes
                    (equal? term1 term2))    ; nboyer 10-25% slower!
                   (else
                    (set! unify-subst (cons (cons term2 term1)
                                            unify-subst))
                    #t))))
          ((not (pair? term1))
           #f)
          ((eq? (car term1)
                (car term2))
           (one-way-unify1-lst (cdr term1)
                               (cdr term2)))
          (else #f)))

  (define (one-way-unify1-lst lst1 lst2)
    (cond ((null? lst1)
           (null? lst2))
          ((null? lst2)
           #f)
          ((one-way-unify1 (car lst1)
                           (car lst2))
           (one-way-unify1-lst (cdr lst1)
                               (cdr lst2)))
          (else #f)))

  (define (falsep x lst)
    (or (term-equal? x false-term)
        (term-member? x lst)))

  (define (truep x lst)
    (or (term-equal? x true-term)
        (term-member? x lst)))

  (define false-term '*)  ; becomes (translate-term '(f))
  (define true-term '*)   ; becomes (translate-term '(t))

  ; The next two procedures were in the original benchmark
  ; but were never used.

  (define (trans-of-implies n)
    (translate-term
     (list (quote implies)
           (trans-of-implies1 n)
           (list (quote implies)
                 0 n))))

  (define (trans-of-implies1 n)
    (cond ((equal? n 1)
           (list (quote implies)
                 0 1))
          (else (list (quote and)
                      (list (quote implies)
                            (- n 1)
                            n)
                      (trans-of-implies1 (- n 1))))))

  ; Translated terms can be circular structures, which can't be
  ; compared using Scheme's equal? and member procedures, so we
  ; use these instead.

  (define (term-equal? x y)
    (cond ((pair? x)
           (and (pair? y)
                (symbol-record-equal? (car x) (car y))
                (term-args-equal? (cdr x) (cdr y))))
          (else (equal? x y))))

  (define (term-args-equal? lst1 lst2)
    (cond ((null? lst1)
           (null? lst2))
          ((null? lst2)
           #f)
          ((term-equal? (car lst1) (car lst2))
           (term-args-equal? (cdr lst1) (cdr lst2)))
          (else #f)))

  (define (term-member? x lst)
    (cond ((null? lst)
           #f)
          ((term-equal? x (car lst))
           #t)
          (else (term-member? x (cdr lst)))))

  (set! setup-boyer
        (lambda ()
          (set! *symbol-records-alist* '())
          (set! if-constructor (symbol->symbol-record 'if))
          (set! false-term (translate-term '(f)))
          (set! true-term  (translate-term '(t)))
          (setup)))

  (set! test-boyer
        (lambda (n)
          (set! rewrite-count 0)
          (let ((answer (test n)))
            (write rewrite-count)
            (display " rewrites")
            (newline)
            (if answer
                rewrite-count
                #f)))))