* More benchmarks.
This commit is contained in:
parent
e76047cb47
commit
af7f6a5b7e
|
@ -1,6 +1,7 @@
|
||||||
|
|
||||||
(library (r6rs-benchmarks)
|
(library (r6rs-benchmarks)
|
||||||
(export run-benchmark fatal-error include-source
|
(export run-benchmark fatal-error include-source
|
||||||
|
call-with-output-file/truncate
|
||||||
ack-iters
|
ack-iters
|
||||||
array1-iters
|
array1-iters
|
||||||
boyer-iters
|
boyer-iters
|
||||||
|
@ -19,6 +20,7 @@
|
||||||
fib-iters
|
fib-iters
|
||||||
fibc-iters
|
fibc-iters
|
||||||
fibfp-iters
|
fibfp-iters
|
||||||
|
fpsum-iters
|
||||||
gcbench-iters
|
gcbench-iters
|
||||||
gcold-iters
|
gcold-iters
|
||||||
graphs-iters
|
graphs-iters
|
||||||
|
@ -34,9 +36,29 @@
|
||||||
perm9-iters
|
perm9-iters
|
||||||
pnpoly-iters
|
pnpoly-iters
|
||||||
peval-iters
|
peval-iters
|
||||||
pi-iters)
|
pi-iters
|
||||||
|
primes-iters
|
||||||
|
puzzle-iters
|
||||||
|
quicksort-iters
|
||||||
|
sboyer-iters
|
||||||
|
sum-iters
|
||||||
|
sum1-iters
|
||||||
|
string-iters
|
||||||
|
sumfp-iters
|
||||||
|
sumloop-iters
|
||||||
|
tail-iters
|
||||||
|
tak-iters
|
||||||
|
trav1-iters
|
||||||
|
trav2-iters
|
||||||
|
triangl-iters
|
||||||
|
wc-iters)
|
||||||
|
|
||||||
(import (ikarus))
|
(import (ikarus))
|
||||||
|
|
||||||
|
(define call-with-output-file/truncate
|
||||||
|
(lambda (file-name proc)
|
||||||
|
(call-with-output-file file-name proc 'truncate)))
|
||||||
|
|
||||||
(define-syntax include-source
|
(define-syntax include-source
|
||||||
(lambda (x)
|
(lambda (x)
|
||||||
(syntax-case x ()
|
(syntax-case x ()
|
||||||
|
@ -138,6 +160,9 @@
|
||||||
; New benchmarks
|
; New benchmarks
|
||||||
(define parsing-iters 1000)
|
(define parsing-iters 1000)
|
||||||
(define gcold-iters 10000)
|
(define gcold-iters 10000)
|
||||||
|
|
||||||
|
(define quicksort-iters 1)
|
||||||
|
(define fpsum-iters 10)
|
||||||
;(define nbody-iters 1) ; nondeterministic (order of evaluation)
|
;(define nbody-iters 1) ; nondeterministic (order of evaluation)
|
||||||
)
|
)
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,11 @@
|
||||||
* conform needs char-downcase.
|
* conform needs char-downcase.
|
||||||
* maze needs bitwise-and
|
* maze needs bitwise-and
|
||||||
* ray needs call-with-output-file/truncate.
|
* ray needs many fl procedures
|
||||||
|
* quicksort needs bignum modulo.
|
||||||
|
* scheme needs complex? and other stuff.
|
||||||
|
* simplex needs flpositive?
|
||||||
|
* slatex needs string-ci=?
|
||||||
|
* compiler needs string-downcase
|
||||||
|
|
||||||
* ctak crashes with a bus error.
|
* ctak crashes with a bus error.
|
||||||
* fibc crashes with a segfault.
|
* fibc crashes with a segfault.
|
||||||
|
@ -8,4 +13,5 @@
|
||||||
* mbrot too slow
|
* mbrot too slow
|
||||||
* ntakl kinda slow
|
* ntakl kinda slow
|
||||||
* pnpoly kinda slow
|
* pnpoly kinda slow
|
||||||
|
* sumfp/fpsum too slow
|
||||||
|
* string too slow
|
||||||
|
|
File diff suppressed because it is too large
Load Diff
|
@ -0,0 +1,18 @@
|
||||||
|
;;; FPSUM - Compute sum of integers from 0 to 1e6 using floating point
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks fpsum)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs arithmetic flonums) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (run)
|
||||||
|
(let loop ((i 1e6) (n 0.))
|
||||||
|
(if (fl<? i 0.)
|
||||||
|
n
|
||||||
|
(loop (fl- i 1.) (fl+ i n)))))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"fpsum"
|
||||||
|
fpsum-iters
|
||||||
|
(lambda (result) (equal? result 500000500000.))
|
||||||
|
(lambda () run))))
|
|
@ -0,0 +1,39 @@
|
||||||
|
;;; PRIMES -- Compute primes less than 100, written by Eric Mohr.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks primes)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (interval-list m n)
|
||||||
|
(if (> m n)
|
||||||
|
'()
|
||||||
|
(cons m (interval-list (+ 1 m) n))))
|
||||||
|
|
||||||
|
(define (sieve l)
|
||||||
|
(letrec ((remove-multiples
|
||||||
|
(lambda (n l)
|
||||||
|
(if (null? l)
|
||||||
|
'()
|
||||||
|
(if (= (modulo (car l) n) 0)
|
||||||
|
(remove-multiples n (cdr l))
|
||||||
|
(cons (car l)
|
||||||
|
(remove-multiples n (cdr l))))))))
|
||||||
|
(if (null? l)
|
||||||
|
'()
|
||||||
|
(cons (car l)
|
||||||
|
(sieve (remove-multiples (car l) (cdr l)))))))
|
||||||
|
|
||||||
|
(define (primes<= n)
|
||||||
|
(sieve (interval-list 2 n)))
|
||||||
|
|
||||||
|
(define (main)
|
||||||
|
(run-benchmark
|
||||||
|
"primes"
|
||||||
|
primes-iters
|
||||||
|
(lambda (result)
|
||||||
|
(equal? result
|
||||||
|
'(2 3 5 7 11 13 17 19 23 29 31 37 41
|
||||||
|
43 47 53 59 61 67 71 73 79 83 89 97)))
|
||||||
|
(lambda (n) (lambda () (primes<= n)))
|
||||||
|
100)))
|
||||||
|
|
|
@ -0,0 +1,148 @@
|
||||||
|
;;; PUZZLE -- Forest Baskett's Puzzle benchmark, originally written in Pascal.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks puzzle)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (my-iota n)
|
||||||
|
(do ((n n (- n 1))
|
||||||
|
(list '() (cons (- n 1) list)))
|
||||||
|
((zero? n) list)))
|
||||||
|
|
||||||
|
(define size 511)
|
||||||
|
(define classmax 3)
|
||||||
|
(define typemax 12)
|
||||||
|
|
||||||
|
(define *iii* 0)
|
||||||
|
(define *kount* 0)
|
||||||
|
(define *d* 8)
|
||||||
|
|
||||||
|
(define *piececount* (make-vector (+ classmax 1) 0))
|
||||||
|
(define *class* (make-vector (+ typemax 1) 0))
|
||||||
|
(define *piecemax* (make-vector (+ typemax 1) 0))
|
||||||
|
(define *puzzle* (make-vector (+ size 1)))
|
||||||
|
(define *p* (make-vector (+ typemax 1)))
|
||||||
|
|
||||||
|
(define (fit i j)
|
||||||
|
(let ((end (vector-ref *piecemax* i)))
|
||||||
|
(do ((k 0 (+ k 1)))
|
||||||
|
((or (> k end)
|
||||||
|
(and (vector-ref (vector-ref *p* i) k)
|
||||||
|
(vector-ref *puzzle* (+ j k))))
|
||||||
|
(if (> k end) #t #f)))))
|
||||||
|
|
||||||
|
(define (place i j)
|
||||||
|
(let ((end (vector-ref *piecemax* i)))
|
||||||
|
(do ((k 0 (+ k 1)))
|
||||||
|
((> k end))
|
||||||
|
(cond ((vector-ref (vector-ref *p* i) k)
|
||||||
|
(vector-set! *puzzle* (+ j k) #t)
|
||||||
|
#t)))
|
||||||
|
(vector-set! *piececount*
|
||||||
|
(vector-ref *class* i)
|
||||||
|
(- (vector-ref *piececount* (vector-ref *class* i)) 1))
|
||||||
|
(do ((k j (+ k 1)))
|
||||||
|
((or (> k size) (not (vector-ref *puzzle* k)))
|
||||||
|
(if (> k size) 0 k)))))
|
||||||
|
|
||||||
|
(define (puzzle-remove i j)
|
||||||
|
(let ((end (vector-ref *piecemax* i)))
|
||||||
|
(do ((k 0 (+ k 1)))
|
||||||
|
((> k end))
|
||||||
|
(cond ((vector-ref (vector-ref *p* i) k)
|
||||||
|
(vector-set! *puzzle* (+ j k) #f)
|
||||||
|
#f)))
|
||||||
|
(vector-set! *piececount*
|
||||||
|
(vector-ref *class* i)
|
||||||
|
(+ (vector-ref *piececount* (vector-ref *class* i)) 1))))
|
||||||
|
|
||||||
|
(define (trial j)
|
||||||
|
(let ((k 0))
|
||||||
|
(call-with-current-continuation
|
||||||
|
(lambda (return)
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((> i typemax) (set! *kount* (+ *kount* 1)) #f)
|
||||||
|
(cond
|
||||||
|
((not
|
||||||
|
(zero?
|
||||||
|
(vector-ref *piececount* (vector-ref *class* i))))
|
||||||
|
(cond
|
||||||
|
((fit i j)
|
||||||
|
(set! k (place i j))
|
||||||
|
(cond
|
||||||
|
((or (trial k) (zero? k))
|
||||||
|
(set! *kount* (+ *kount* 1))
|
||||||
|
(return #t))
|
||||||
|
(else (puzzle-remove i j))))))))))))
|
||||||
|
|
||||||
|
(define (definePiece iclass ii jj kk)
|
||||||
|
(let ((index 0))
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((> i ii))
|
||||||
|
(do ((j 0 (+ j 1)))
|
||||||
|
((> j jj))
|
||||||
|
(do ((k 0 (+ k 1)))
|
||||||
|
((> k kk))
|
||||||
|
(set! index (+ i (* *d* (+ j (* *d* k)))))
|
||||||
|
(vector-set! (vector-ref *p* *iii*) index #t))))
|
||||||
|
(vector-set! *class* *iii* iclass)
|
||||||
|
(vector-set! *piecemax* *iii* index)
|
||||||
|
(cond ((not (= *iii* typemax))
|
||||||
|
(set! *iii* (+ *iii* 1))))))
|
||||||
|
|
||||||
|
(define (start)
|
||||||
|
(set! *kount* 0)
|
||||||
|
(do ((m 0 (+ m 1)))
|
||||||
|
((> m size))
|
||||||
|
(vector-set! *puzzle* m #t))
|
||||||
|
(do ((i 1 (+ i 1)))
|
||||||
|
((> i 5))
|
||||||
|
(do ((j 1 (+ j 1)))
|
||||||
|
((> j 5))
|
||||||
|
(do ((k 1 (+ k 1)))
|
||||||
|
((> k 5))
|
||||||
|
(vector-set! *puzzle* (+ i (* *d* (+ j (* *d* k)))) #f))))
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((> i typemax))
|
||||||
|
(do ((m 0 (+ m 1)))
|
||||||
|
((> m size))
|
||||||
|
(vector-set! (vector-ref *p* i) m #f)))
|
||||||
|
(set! *iii* 0)
|
||||||
|
(definePiece 0 3 1 0)
|
||||||
|
(definePiece 0 1 0 3)
|
||||||
|
(definePiece 0 0 3 1)
|
||||||
|
(definePiece 0 1 3 0)
|
||||||
|
(definePiece 0 3 0 1)
|
||||||
|
(definePiece 0 0 1 3)
|
||||||
|
|
||||||
|
(definePiece 1 2 0 0)
|
||||||
|
(definePiece 1 0 2 0)
|
||||||
|
(definePiece 1 0 0 2)
|
||||||
|
|
||||||
|
(definePiece 2 1 1 0)
|
||||||
|
(definePiece 2 1 0 1)
|
||||||
|
(definePiece 2 0 1 1)
|
||||||
|
|
||||||
|
(definePiece 3 1 1 1)
|
||||||
|
|
||||||
|
(vector-set! *piececount* 0 13)
|
||||||
|
(vector-set! *piececount* 1 3)
|
||||||
|
(vector-set! *piececount* 2 1)
|
||||||
|
(vector-set! *piececount* 3 1)
|
||||||
|
(let ((m (+ (* *d* (+ *d* 1)) 1))
|
||||||
|
(n 0))
|
||||||
|
(cond ((fit 0 m) (set! n (place 0 m)))
|
||||||
|
(else (begin (newline) (display "Error."))))
|
||||||
|
(if (trial n)
|
||||||
|
*kount*
|
||||||
|
#f)))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"puzzle"
|
||||||
|
puzzle-iters
|
||||||
|
(lambda (result) (equal? result 2005))
|
||||||
|
(lambda () (lambda () (start)))))
|
||||||
|
|
||||||
|
(for-each (lambda (i) (vector-set! *p* i (make-vector (+ size 1))))
|
||||||
|
(my-iota (+ typemax 1))))
|
|
@ -0,0 +1,100 @@
|
||||||
|
; The quick-1 benchmark. (Figure 35, page 132.)
|
||||||
|
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks quicksort)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs mutable-pairs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (quick-1 v less?)
|
||||||
|
|
||||||
|
(define (helper left right)
|
||||||
|
(if (< left right)
|
||||||
|
(let ((median (partition v left right less?)))
|
||||||
|
(if (< (- median left) (- right median))
|
||||||
|
(begin (helper left (- median 1))
|
||||||
|
(helper (+ median 1) right))
|
||||||
|
(begin (helper (+ median 1) right)
|
||||||
|
(helper left (- median 1)))))
|
||||||
|
v))
|
||||||
|
|
||||||
|
(helper 0 (- (vector-length v) 1)))
|
||||||
|
|
||||||
|
|
||||||
|
(define (partition v left right less?)
|
||||||
|
(let ((mid (vector-ref v right)))
|
||||||
|
|
||||||
|
(define (uploop i)
|
||||||
|
(let ((i (+ i 1)))
|
||||||
|
(if (and (< i right) (less? (vector-ref v i) mid))
|
||||||
|
(uploop i)
|
||||||
|
i)))
|
||||||
|
|
||||||
|
(define (downloop j)
|
||||||
|
(let ((j (- j 1)))
|
||||||
|
(if (and (> j left) (less? mid (vector-ref v j)))
|
||||||
|
(downloop j)
|
||||||
|
j)))
|
||||||
|
|
||||||
|
(define (ploop i j)
|
||||||
|
(let* ((i (uploop i))
|
||||||
|
(j (downloop j)))
|
||||||
|
(let ((tmp (vector-ref v i)))
|
||||||
|
(vector-set! v i (vector-ref v j))
|
||||||
|
(vector-set! v j tmp)
|
||||||
|
(if (< i j)
|
||||||
|
(ploop i j)
|
||||||
|
(begin (vector-set! v j (vector-ref v i))
|
||||||
|
(vector-set! v i (vector-ref v right))
|
||||||
|
(vector-set! v right tmp)
|
||||||
|
i)))))
|
||||||
|
|
||||||
|
(ploop (- left 1) right)))
|
||||||
|
|
||||||
|
; minimal standard random number generator
|
||||||
|
; 32 bit integer version
|
||||||
|
; cacm 31 10, oct 88
|
||||||
|
;
|
||||||
|
|
||||||
|
(define *seed* (list 1))
|
||||||
|
|
||||||
|
(define (srand seed)
|
||||||
|
(set-car! *seed* seed))
|
||||||
|
|
||||||
|
(define (rand)
|
||||||
|
(let* ((hi (quotient (car *seed*) 127773))
|
||||||
|
(lo (modulo (car *seed*) 127773))
|
||||||
|
(test (- (* 16807 lo) (* 2836 hi))))
|
||||||
|
(if (> test 0)
|
||||||
|
(set-car! *seed* test)
|
||||||
|
(set-car! *seed* (+ test 2147483647)))
|
||||||
|
(car *seed*)))
|
||||||
|
|
||||||
|
;; return a random number in the interval [0,n)
|
||||||
|
(define random
|
||||||
|
(lambda (n)
|
||||||
|
(modulo (abs (rand)) n)))
|
||||||
|
|
||||||
|
|
||||||
|
(define (quicksort-benchmark)
|
||||||
|
(let* ((n 30000)
|
||||||
|
(v (make-vector n)))
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((= i n))
|
||||||
|
(vector-set! v i (random 4000)))
|
||||||
|
(quick-1 v (lambda (x y) (< x y)))))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"quicksort30"
|
||||||
|
quicksort-iters
|
||||||
|
(lambda (v)
|
||||||
|
(call-with-current-continuation
|
||||||
|
(lambda (return)
|
||||||
|
(do ((i 1 (+ i 1)))
|
||||||
|
((= i (vector-length v))
|
||||||
|
#t)
|
||||||
|
(if (not (<= (vector-ref v (- i 1))
|
||||||
|
(vector-ref v i)))
|
||||||
|
(return #f))))))
|
||||||
|
(lambda () quicksort-benchmark))))
|
||||||
|
|
|
@ -69,7 +69,7 @@
|
||||||
(let ((ray (unit-vector (fl- x (point-x eye))
|
(let ((ray (unit-vector (fl- x (point-x eye))
|
||||||
(fl- y (point-y eye))
|
(fl- y (point-y eye))
|
||||||
(fl- (point-z eye)))))
|
(fl- (point-z eye)))))
|
||||||
(flinexact->exact (flround (fl* (sendray eye ray) 255.0)))))
|
(inexact->exact (flround (fl* (sendray eye ray) 255.0)))))
|
||||||
|
|
||||||
(define (sendray pt ray)
|
(define (sendray pt ray)
|
||||||
(let* ((x (first-hit pt ray))
|
(let* ((x (first-hit pt ray))
|
||||||
|
|
|
@ -0,0 +1,788 @@
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
; File: sboyer.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)
|
||||||
|
; Language: Scheme
|
||||||
|
; Status: Public Domain
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
;;; SBOYER -- Logic programming benchmark, originally written by Bob Boyer.
|
||||||
|
;;; Much less CONS-intensive than NBOYER because it uses Henry Baker's
|
||||||
|
;;; "sharing cons".
|
||||||
|
|
||||||
|
; 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
|
||||||
|
; 1 591777
|
||||||
|
; 2 1813975
|
||||||
|
; 3 5375678
|
||||||
|
; 4 16445406
|
||||||
|
; 5 51507739
|
||||||
|
|
||||||
|
; Sboyer 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.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks sboyer)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(let ((n (if (null? args) 0 (car args))))
|
||||||
|
(setup-boyer)
|
||||||
|
(run-benchmark
|
||||||
|
(string-append "sboyer"
|
||||||
|
(number->string n))
|
||||||
|
sboyer-iters
|
||||||
|
(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))))
|
||||||
|
(lambda (alist term n) (lambda () (test-boyer alist term n)))
|
||||||
|
(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)))))
|
||||||
|
(quote (implies (and (implies x y)
|
||||||
|
(and (implies y z)
|
||||||
|
(and (implies z u)
|
||||||
|
(implies u w))))
|
||||||
|
(implies x w)))
|
||||||
|
n)))
|
||||||
|
|
||||||
|
(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 (_1- 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 (_1- 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 (_1- a)
|
||||||
|
(zero))
|
||||||
|
(equal (_1- 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 (fatal-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 alist term n)
|
||||||
|
(let ((term
|
||||||
|
(apply-subst
|
||||||
|
(translate-alist alist)
|
||||||
|
(translate-term
|
||||||
|
(do ((term term (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
|
||||||
|
|
||||||
|
; The next procedure is Henry Baker's sharing CONS, which avoids
|
||||||
|
; allocation if the result is already in hand.
|
||||||
|
; The REWRITE and REWRITE-ARGS procedures have been modified to
|
||||||
|
; use SCONS instead of CONS.
|
||||||
|
|
||||||
|
(define (scons x y original)
|
||||||
|
(if (and (eq? x (car original))
|
||||||
|
(eq? y (cdr original)))
|
||||||
|
original
|
||||||
|
(cons x y)))
|
||||||
|
|
||||||
|
(define (rewrite term)
|
||||||
|
(set! rewrite-count (+ rewrite-count 1))
|
||||||
|
(cond ((not (pair? term))
|
||||||
|
term)
|
||||||
|
(else (rewrite-with-lemmas (scons (car term)
|
||||||
|
(rewrite-args (cdr term))
|
||||||
|
term)
|
||||||
|
(get-lemmas (car term))))))
|
||||||
|
|
||||||
|
(define (rewrite-args lst)
|
||||||
|
(cond ((null? lst)
|
||||||
|
'())
|
||||||
|
(else (scons (rewrite (car lst))
|
||||||
|
(rewrite-args (cdr lst))
|
||||||
|
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 (alist term n)
|
||||||
|
(set! rewrite-count 0)
|
||||||
|
(let ((answer (test alist term n)))
|
||||||
|
; (write rewrite-count)
|
||||||
|
; (display " rewrites")
|
||||||
|
; (newline)
|
||||||
|
(if answer
|
||||||
|
rewrite-count
|
||||||
|
#f))))))
|
File diff suppressed because it is too large
Load Diff
|
@ -0,0 +1,192 @@
|
||||||
|
;;; SIMPLEX -- Simplex algorithm.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks simplex)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs arithmetic flonums) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (matrix-rows a) (vector-length a))
|
||||||
|
(define (matrix-columns a) (vector-length (vector-ref a 0)))
|
||||||
|
(define (matrix-ref a i j) (vector-ref (vector-ref a i) j))
|
||||||
|
(define (matrix-set! a i j x) (vector-set! (vector-ref a i) j x))
|
||||||
|
|
||||||
|
(define (fuck-up)
|
||||||
|
(fatal-error "This shouldn't happen"))
|
||||||
|
|
||||||
|
(define (simplex a m1 m2 m3)
|
||||||
|
;(define *epsilon* 1e-6)
|
||||||
|
(define *epsilon* 0.000001)
|
||||||
|
(if (not (and (>= m1 0)
|
||||||
|
(>= m2 0)
|
||||||
|
(>= m3 0)
|
||||||
|
(= (matrix-rows a) (+ m1 m2 m3 2))))
|
||||||
|
(fuck-up))
|
||||||
|
(let* ((m12 (+ m1 m2 1))
|
||||||
|
(m (- (matrix-rows a) 2))
|
||||||
|
(n (- (matrix-columns a) 1))
|
||||||
|
(l1 (make-vector n))
|
||||||
|
(l2 (make-vector m))
|
||||||
|
(l3 (make-vector m2))
|
||||||
|
(nl1 n)
|
||||||
|
(iposv (make-vector m))
|
||||||
|
(izrov (make-vector n))
|
||||||
|
(ip 0)
|
||||||
|
(kp 0)
|
||||||
|
(bmax 0.0)
|
||||||
|
(one? #f)
|
||||||
|
(pass2? #t))
|
||||||
|
(define (simp1 mm abs?)
|
||||||
|
(set! kp (vector-ref l1 0))
|
||||||
|
(set! bmax (matrix-ref a mm kp))
|
||||||
|
(do ((k 1 (+ k 1))) ((>= k nl1))
|
||||||
|
(if (flpositive?
|
||||||
|
(if abs?
|
||||||
|
(fl- (flabs (matrix-ref a mm (vector-ref l1 k)))
|
||||||
|
(flabs bmax))
|
||||||
|
(fl- (matrix-ref a mm (vector-ref l1 k)) bmax)))
|
||||||
|
(begin
|
||||||
|
(set! kp (vector-ref l1 k))
|
||||||
|
(set! bmax (matrix-ref a mm (vector-ref l1 k)))))))
|
||||||
|
(define (simp2)
|
||||||
|
(set! ip 0)
|
||||||
|
(let ((q1 0.0)
|
||||||
|
(flag? #f))
|
||||||
|
(do ((i 0 (+ i 1))) ((= i m))
|
||||||
|
(if flag?
|
||||||
|
(if (fl<? (matrix-ref a (vector-ref l2 i) kp) (fl- *epsilon*))
|
||||||
|
(begin
|
||||||
|
(let ((q (fl/ (fl- (matrix-ref a (vector-ref l2 i) 0))
|
||||||
|
(matrix-ref a (vector-ref l2 i) kp))))
|
||||||
|
(cond
|
||||||
|
((fl<? q q1)
|
||||||
|
(set! ip (vector-ref l2 i))
|
||||||
|
(set! q1 q))
|
||||||
|
((fl=? q q1)
|
||||||
|
(let ((qp 0.0)
|
||||||
|
(q0 0.0))
|
||||||
|
(let loop ((k 1))
|
||||||
|
(if (<= k n)
|
||||||
|
(begin
|
||||||
|
(set! qp (fl/ (fl- (matrix-ref a ip k))
|
||||||
|
(matrix-ref a ip kp)))
|
||||||
|
(set! q0 (fl/ (fl-
|
||||||
|
(matrix-ref a (vector-ref l2 i) k))
|
||||||
|
(matrix-ref a (vector-ref l2 i) kp)))
|
||||||
|
(if (fl=? q0 qp)
|
||||||
|
(loop (+ k 1))))))
|
||||||
|
(if (fl<? q0 qp)
|
||||||
|
(set! ip (vector-ref l2 i)))))))))
|
||||||
|
(if (fl<? (matrix-ref a (vector-ref l2 i) kp) (fl- *epsilon*))
|
||||||
|
(begin
|
||||||
|
(set! q1 (fl/ (fl- (matrix-ref a (vector-ref l2 i) 0))
|
||||||
|
(matrix-ref a (vector-ref l2 i) kp)))
|
||||||
|
(set! ip (vector-ref l2 i))
|
||||||
|
(set! flag? #t)))))))
|
||||||
|
(define (simp3 one?)
|
||||||
|
(let ((piv (fl/ (matrix-ref a ip kp))))
|
||||||
|
(do ((ii 0 (+ ii 1))) ((= ii (+ m (if one? 2 1))))
|
||||||
|
(if (not (= ii ip))
|
||||||
|
(begin
|
||||||
|
(matrix-set! a ii kp (fl* piv (matrix-ref a ii kp)))
|
||||||
|
(do ((kk 0 (+ kk 1))) ((= kk (+ n 1)))
|
||||||
|
(if (not (= kk kp))
|
||||||
|
(matrix-set! a ii kk (fl- (matrix-ref a ii kk)
|
||||||
|
(fl* (matrix-ref a ip kk)
|
||||||
|
(matrix-ref a ii kp)))))))))
|
||||||
|
(do ((kk 0 (+ kk 1))) ((= kk (+ n 1)))
|
||||||
|
(if (not (= kk kp))
|
||||||
|
(matrix-set! a ip kk (fl* (fl- piv) (matrix-ref a ip kk)))))
|
||||||
|
(matrix-set! a ip kp piv)))
|
||||||
|
(do ((k 0 (+ k 1))) ((= k n))
|
||||||
|
(vector-set! l1 k (+ k 1))
|
||||||
|
(vector-set! izrov k k))
|
||||||
|
(do ((i 0 (+ i 1))) ((= i m))
|
||||||
|
(if (flnegative? (matrix-ref a (+ i 1) 0))
|
||||||
|
(fuck-up))
|
||||||
|
(vector-set! l2 i (+ i 1))
|
||||||
|
(vector-set! iposv i (+ n i)))
|
||||||
|
(do ((i 0 (+ i 1))) ((= i m2)) (vector-set! l3 i #t))
|
||||||
|
(if (positive? (+ m2 m3))
|
||||||
|
(begin
|
||||||
|
(do ((k 0 (+ k 1))) ((= k (+ n 1)))
|
||||||
|
(do ((i (+ m1 1) (+ i 1)) (sum 0.0 (fl+ sum (matrix-ref a i k))))
|
||||||
|
((> i m) (matrix-set! a (+ m 1) k (fl- sum)))))
|
||||||
|
(let loop ()
|
||||||
|
(simp1 (+ m 1) #f)
|
||||||
|
(cond
|
||||||
|
((fl<=? bmax *epsilon*)
|
||||||
|
(cond ((fl<? (matrix-ref a (+ m 1) 0) (fl- *epsilon*))
|
||||||
|
(set! pass2? #f))
|
||||||
|
((fl<=? (matrix-ref a (+ m 1) 0) *epsilon*)
|
||||||
|
(let loop ((ip1 m12))
|
||||||
|
(if (<= ip1 m)
|
||||||
|
(cond ((= (vector-ref iposv (- ip1 1)) (+ ip n -1))
|
||||||
|
(simp1 ip1 #t)
|
||||||
|
(cond ((flpositive? bmax)
|
||||||
|
(set! ip ip1)
|
||||||
|
(set! one? #t))
|
||||||
|
(else
|
||||||
|
(loop (+ ip1 1)))))
|
||||||
|
(else
|
||||||
|
(loop (+ ip1 1))))
|
||||||
|
(do ((i (+ m1 1) (+ i 1))) ((>= i m12))
|
||||||
|
(if (vector-ref l3 (- i (+ m1 1)))
|
||||||
|
(do ((k 0 (+ k 1))) ((= k (+ n 1)))
|
||||||
|
(matrix-set! a i k (fl- (matrix-ref a i k)))))))))
|
||||||
|
(else (simp2) (if (zero? ip) (set! pass2? #f) (set! one? #t)))))
|
||||||
|
(else (simp2) (if (zero? ip) (set! pass2? #f) (set! one? #t))))
|
||||||
|
(if one?
|
||||||
|
(begin
|
||||||
|
(set! one? #f)
|
||||||
|
(simp3 #t)
|
||||||
|
(cond
|
||||||
|
((>= (vector-ref iposv (- ip 1)) (+ n m12 -1))
|
||||||
|
(let loop ((k 0))
|
||||||
|
(cond
|
||||||
|
((and (< k nl1) (not (= kp (vector-ref l1 k))))
|
||||||
|
(loop (+ k 1)))
|
||||||
|
(else
|
||||||
|
(set! nl1 (- nl1 1))
|
||||||
|
(do ((is k (+ is 1))) ((>= is nl1))
|
||||||
|
(vector-set! l1 is (vector-ref l1 (+ is 1))))
|
||||||
|
(matrix-set! a (+ m 1) kp (fl+ (matrix-ref a (+ m 1) kp) 1.0))
|
||||||
|
(do ((i 0 (+ i 1))) ((= i (+ m 2)))
|
||||||
|
(matrix-set! a i kp (fl- (matrix-ref a i kp))))))))
|
||||||
|
((and (>= (vector-ref iposv (- ip 1)) (+ n m1))
|
||||||
|
(vector-ref l3 (- (vector-ref iposv (- ip 1)) (+ m1 n))))
|
||||||
|
(vector-set! l3 (- (vector-ref iposv (- ip 1)) (+ m1 n)) #f)
|
||||||
|
(matrix-set! a (+ m 1) kp (fl+ (matrix-ref a (+ m 1) kp) 1.0))
|
||||||
|
(do ((i 0 (+ i 1))) ((= i (+ m 2)))
|
||||||
|
(matrix-set! a i kp (fl- (matrix-ref a i kp))))))
|
||||||
|
(let ((t (vector-ref izrov (- kp 1))))
|
||||||
|
(vector-set! izrov (- kp 1) (vector-ref iposv (- ip 1)))
|
||||||
|
(vector-set! iposv (- ip 1) t))
|
||||||
|
(loop))))))
|
||||||
|
(and pass2?
|
||||||
|
(let loop ()
|
||||||
|
(simp1 0 #f)
|
||||||
|
(cond
|
||||||
|
((f(run))lpositive? bmax)
|
||||||
|
(simp2)
|
||||||
|
(cond ((zero? ip) #t)
|
||||||
|
(else (simp3 #f)
|
||||||
|
(let ((t (vector-ref izrov (- kp 1))))
|
||||||
|
(vector-set! izrov (- kp 1) (vector-ref iposv (- ip 1)))
|
||||||
|
(vector-set! iposv (- ip 1) t))
|
||||||
|
(loop))))
|
||||||
|
(else (list iposv izrov)))))))
|
||||||
|
|
||||||
|
(define (test)
|
||||||
|
(simplex (vector (vector 0.0 1.0 1.0 3.0 -0.5)
|
||||||
|
(vector 740.0 -1.0 0.0 -2.0 0.0)
|
||||||
|
(vector 0.0 0.0 -2.0 0.0 7.0)
|
||||||
|
(vector 0.5 0.0 -1.0 1.0 -2.0)
|
||||||
|
(vector 9.0 -1.0 -1.0 -1.0 -1.0)
|
||||||
|
(vector 0.0 0.0 0.0 0.0 0.0))
|
||||||
|
2 1 1))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"simplex"
|
||||||
|
simplex-iters
|
||||||
|
(lambda (result) (equal? result '(#(4 1 3 2) #(0 5 7 6))))
|
||||||
|
(lambda () (lambda () (test))))))
|
File diff suppressed because it is too large
Load Diff
|
@ -0,0 +1,33 @@
|
||||||
|
;;; STRING -- One of the Kernighan and Van Wyk benchmarks.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks string)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define s "abcdef")
|
||||||
|
|
||||||
|
(define (grow)
|
||||||
|
(set! s (string-append "123" s "456" s "789"))
|
||||||
|
(set! s (string-append
|
||||||
|
(substring s (quotient (string-length s) 2) (string-length s))
|
||||||
|
(substring s 0 (+ 1 (quotient (string-length s) 2)))))
|
||||||
|
s)
|
||||||
|
|
||||||
|
(define (trial n)
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((> (string-length s) n) (string-length s))
|
||||||
|
(grow)))
|
||||||
|
|
||||||
|
(define (my-try n)
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((>= i 10) (string-length s))
|
||||||
|
(set! s "abcdef")
|
||||||
|
(trial n)))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"string"
|
||||||
|
string-iters
|
||||||
|
(lambda (result) (equal? result 524278))
|
||||||
|
(lambda (n) (lambda () (my-try n)))
|
||||||
|
500000)))
|
|
@ -0,0 +1,19 @@
|
||||||
|
;;; SUM -- Compute sum of integers from 0 to 10000
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks sum)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (run n)
|
||||||
|
(let loop ((i n) (sum 0))
|
||||||
|
(if (< i 0)
|
||||||
|
sum
|
||||||
|
(loop (- i 1) (+ i sum)))))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"sum"
|
||||||
|
sum-iters
|
||||||
|
(lambda (result) (equal? result 50005000))
|
||||||
|
(lambda (n) (lambda () (run n)))
|
||||||
|
10000)))
|
|
@ -0,0 +1,31 @@
|
||||||
|
;;; SUM1 -- One of the Kernighan and Van Wyk benchmarks.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks sum1)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs arithmetic flonums) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define inport #f)
|
||||||
|
|
||||||
|
(define (sumport port sum-so-far)
|
||||||
|
(let ((x (read port)))
|
||||||
|
(if (eof-object? x)
|
||||||
|
sum-so-far
|
||||||
|
(sumport port (fl+ x sum-so-far)))))
|
||||||
|
|
||||||
|
(define (sum port)
|
||||||
|
(sumport port 0.0))
|
||||||
|
|
||||||
|
(define (go)
|
||||||
|
(set! inport (open-input-file "r6rs-benchmarks/rn100"))
|
||||||
|
(let ((result (sum inport)))
|
||||||
|
(close-input-port inport)
|
||||||
|
result))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"sum1"
|
||||||
|
sum1-iters
|
||||||
|
(lambda (result) (and (fl>=? result 15794.974999999)
|
||||||
|
(fl<=? result 15794.975000001)))
|
||||||
|
(lambda () (lambda () (go))))))
|
||||||
|
|
|
@ -0,0 +1,19 @@
|
||||||
|
;;; SUMFP -- Compute sum of integers from 0 to 10000 using floating point
|
||||||
|
(library (r6rs-benchmarks sumfp)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs arithmetic flonums) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
|
||||||
|
(define (run n)
|
||||||
|
(let loop ((i n) (sum 0.))
|
||||||
|
(if (fl<? i 0.)
|
||||||
|
sum
|
||||||
|
(loop (fl- i 1.) (fl+ i sum)))))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"sumfp"
|
||||||
|
sumfp-iters
|
||||||
|
(lambda (result) (equal? result 50005000.))
|
||||||
|
(lambda (n) (lambda () (run n)))
|
||||||
|
10000.)))
|
|
@ -0,0 +1,31 @@
|
||||||
|
;;; SUMLOOP -- One of the Kernighan and Van Wyk benchmarks.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks sumloop)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define sum 0)
|
||||||
|
|
||||||
|
(define (tail-rec-aux i n)
|
||||||
|
(if (< i n)
|
||||||
|
(begin (set! sum (+ sum 1)) (tail-rec-aux (+ i 1) n))
|
||||||
|
sum))
|
||||||
|
|
||||||
|
(define (tail-rec-loop n)
|
||||||
|
(set! sum 0)
|
||||||
|
(tail-rec-aux 0 n)
|
||||||
|
sum)
|
||||||
|
|
||||||
|
(define (do-loop n)
|
||||||
|
(set! sum 0)
|
||||||
|
(do ((i 0 (+ i 1)))
|
||||||
|
((>= i n) sum)
|
||||||
|
(set! sum (+ sum 1))))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"sumloop"
|
||||||
|
sumloop-iters
|
||||||
|
(lambda (result) (equal? result 100000000))
|
||||||
|
(lambda (n) (lambda () (do-loop n)))
|
||||||
|
100000000)))
|
|
@ -0,0 +1,41 @@
|
||||||
|
;;; TAIL -- One of the Kernighan and Van Wyk benchmarks.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks tail)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define inport #f)
|
||||||
|
(define outport #f)
|
||||||
|
|
||||||
|
(define (readline port line-so-far)
|
||||||
|
(let ((x (read-char port)))
|
||||||
|
(cond ((eof-object? x)
|
||||||
|
x)
|
||||||
|
((char=? x #\newline)
|
||||||
|
(list->string (reverse
|
||||||
|
(cons x line-so-far))))
|
||||||
|
(#t (readline port (cons x line-so-far))))))
|
||||||
|
|
||||||
|
(define (tail-r-aux port file-so-far)
|
||||||
|
(let ((x (readline port '())))
|
||||||
|
(if (eof-object? x)
|
||||||
|
(begin
|
||||||
|
(display file-so-far outport)
|
||||||
|
(close-output-port outport))
|
||||||
|
(tail-r-aux port (cons x file-so-far)))))
|
||||||
|
|
||||||
|
(define (tail-r port)
|
||||||
|
(tail-r-aux port '()))
|
||||||
|
|
||||||
|
(define (go)
|
||||||
|
(set! inport (open-input-file "r6rs-benchmarks/bib"))
|
||||||
|
(set! outport (open-output-file "foo"))
|
||||||
|
(tail-r inport)
|
||||||
|
(close-input-port inport))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"tail"
|
||||||
|
tail-iters
|
||||||
|
(lambda (result) #t)
|
||||||
|
(lambda () (lambda () (go))))))
|
|
@ -0,0 +1,23 @@
|
||||||
|
;;; TAK -- A vanilla version of the TAKeuchi function.
|
||||||
|
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks tak)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (tak x y z)
|
||||||
|
(if (not (< y x))
|
||||||
|
z
|
||||||
|
(tak (tak (- x 1) y z)
|
||||||
|
(tak (- y 1) z x)
|
||||||
|
(tak (- z 1) x y))))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"tak"
|
||||||
|
tak-iters
|
||||||
|
(lambda (result) (equal? result 7))
|
||||||
|
(lambda (x y z) (lambda () (tak x y z)))
|
||||||
|
18
|
||||||
|
12
|
||||||
|
6)))
|
|
@ -0,0 +1,37 @@
|
||||||
|
;;; TAKL -- The TAKeuchi function using lists as counters.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks takl)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (listn n)
|
||||||
|
(if (= n 0)
|
||||||
|
'()
|
||||||
|
(cons n (listn (- n 1)))))
|
||||||
|
|
||||||
|
(define l18 (listn 18))
|
||||||
|
(define l12 (listn 12))
|
||||||
|
(define l6 (listn 6))
|
||||||
|
|
||||||
|
(define (mas x y z)
|
||||||
|
(if (not (shorterp y x))
|
||||||
|
z
|
||||||
|
(mas (mas (cdr x) y z)
|
||||||
|
(mas (cdr y) z x)
|
||||||
|
(mas (cdr z) x y))))
|
||||||
|
|
||||||
|
(define (shorterp x y)
|
||||||
|
(and (not (null? y))
|
||||||
|
(or (null? x)
|
||||||
|
(shorterp (cdr x)
|
||||||
|
(cdr y)))))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"takl"
|
||||||
|
takl-iters
|
||||||
|
(lambda (result) (equal? result '(7 6 5 4 3 2 1)))
|
||||||
|
(lambda (x y z) (lambda () (mas x y z)))
|
||||||
|
l18
|
||||||
|
l12
|
||||||
|
l6)))
|
File diff suppressed because it is too large
Load Diff
|
@ -1,14 +0,0 @@
|
||||||
;;; FPSUM - Compute sum of integers from 0 to 1e6 using floating point
|
|
||||||
|
|
||||||
(define (run)
|
|
||||||
(let loop ((i 1e6) (n 0.))
|
|
||||||
(if (FLOAT< i 0.)
|
|
||||||
n
|
|
||||||
(loop (FLOAT- i 1.) (FLOAT+ i n)))))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"fpsum"
|
|
||||||
fpsum-iters
|
|
||||||
(lambda () (run))
|
|
||||||
(lambda (result) (equal? result 500000500000.))))
|
|
|
@ -1,34 +0,0 @@
|
||||||
;;; PRIMES -- Compute primes less than 100, written by Eric Mohr.
|
|
||||||
|
|
||||||
(define (interval-list m n)
|
|
||||||
(if (> m n)
|
|
||||||
'()
|
|
||||||
(cons m (interval-list (+ 1 m) n))))
|
|
||||||
|
|
||||||
(define (sieve l)
|
|
||||||
(letrec ((remove-multiples
|
|
||||||
(lambda (n l)
|
|
||||||
(if (null? l)
|
|
||||||
'()
|
|
||||||
(if (= (modulo (car l) n) 0)
|
|
||||||
(remove-multiples n (cdr l))
|
|
||||||
(cons (car l)
|
|
||||||
(remove-multiples n (cdr l))))))))
|
|
||||||
(if (null? l)
|
|
||||||
'()
|
|
||||||
(cons (car l)
|
|
||||||
(sieve (remove-multiples (car l) (cdr l)))))))
|
|
||||||
|
|
||||||
(define (primes<= n)
|
|
||||||
(sieve (interval-list 2 n)))
|
|
||||||
|
|
||||||
(define (main)
|
|
||||||
(run-benchmark
|
|
||||||
"primes"
|
|
||||||
primes-iters
|
|
||||||
(lambda (result)
|
|
||||||
(equal? result
|
|
||||||
'(2 3 5 7 11 13 17 19 23 29 31 37 41
|
|
||||||
43 47 53 59 61 67 71 73 79 83 89 97)))
|
|
||||||
(lambda (n) (lambda () (primes<= n)))
|
|
||||||
100))
|
|
|
@ -1,144 +0,0 @@
|
||||||
;;; PUZZLE -- Forest Baskett's Puzzle benchmark, originally written in Pascal.
|
|
||||||
|
|
||||||
(define (my-iota n)
|
|
||||||
(do ((n n (- n 1))
|
|
||||||
(list '() (cons (- n 1) list)))
|
|
||||||
((zero? n) list)))
|
|
||||||
|
|
||||||
(define size 511)
|
|
||||||
(define classmax 3)
|
|
||||||
(define typemax 12)
|
|
||||||
|
|
||||||
(define *iii* 0)
|
|
||||||
(define *kount* 0)
|
|
||||||
(define *d* 8)
|
|
||||||
|
|
||||||
(define *piececount* (make-vector (+ classmax 1) 0))
|
|
||||||
(define *class* (make-vector (+ typemax 1) 0))
|
|
||||||
(define *piecemax* (make-vector (+ typemax 1) 0))
|
|
||||||
(define *puzzle* (make-vector (+ size 1)))
|
|
||||||
(define *p* (make-vector (+ typemax 1)))
|
|
||||||
|
|
||||||
(define (fit i j)
|
|
||||||
(let ((end (vector-ref *piecemax* i)))
|
|
||||||
(do ((k 0 (+ k 1)))
|
|
||||||
((or (> k end)
|
|
||||||
(and (vector-ref (vector-ref *p* i) k)
|
|
||||||
(vector-ref *puzzle* (+ j k))))
|
|
||||||
(if (> k end) #t #f)))))
|
|
||||||
|
|
||||||
(define (place i j)
|
|
||||||
(let ((end (vector-ref *piecemax* i)))
|
|
||||||
(do ((k 0 (+ k 1)))
|
|
||||||
((> k end))
|
|
||||||
(cond ((vector-ref (vector-ref *p* i) k)
|
|
||||||
(vector-set! *puzzle* (+ j k) #t)
|
|
||||||
#t)))
|
|
||||||
(vector-set! *piececount*
|
|
||||||
(vector-ref *class* i)
|
|
||||||
(- (vector-ref *piececount* (vector-ref *class* i)) 1))
|
|
||||||
(do ((k j (+ k 1)))
|
|
||||||
((or (> k size) (not (vector-ref *puzzle* k)))
|
|
||||||
(if (> k size) 0 k)))))
|
|
||||||
|
|
||||||
(define (puzzle-remove i j)
|
|
||||||
(let ((end (vector-ref *piecemax* i)))
|
|
||||||
(do ((k 0 (+ k 1)))
|
|
||||||
((> k end))
|
|
||||||
(cond ((vector-ref (vector-ref *p* i) k)
|
|
||||||
(vector-set! *puzzle* (+ j k) #f)
|
|
||||||
#f)))
|
|
||||||
(vector-set! *piececount*
|
|
||||||
(vector-ref *class* i)
|
|
||||||
(+ (vector-ref *piececount* (vector-ref *class* i)) 1))))
|
|
||||||
|
|
||||||
(define (trial j)
|
|
||||||
(let ((k 0))
|
|
||||||
(call-with-current-continuation
|
|
||||||
(lambda (return)
|
|
||||||
(do ((i 0 (+ i 1)))
|
|
||||||
((> i typemax) (set! *kount* (+ *kount* 1)) #f)
|
|
||||||
(cond
|
|
||||||
((not
|
|
||||||
(zero?
|
|
||||||
(vector-ref *piececount* (vector-ref *class* i))))
|
|
||||||
(cond
|
|
||||||
((fit i j)
|
|
||||||
(set! k (place i j))
|
|
||||||
(cond
|
|
||||||
((or (trial k) (zero? k))
|
|
||||||
(set! *kount* (+ *kount* 1))
|
|
||||||
(return #t))
|
|
||||||
(else (puzzle-remove i j))))))))))))
|
|
||||||
|
|
||||||
(define (definePiece iclass ii jj kk)
|
|
||||||
(let ((index 0))
|
|
||||||
(do ((i 0 (+ i 1)))
|
|
||||||
((> i ii))
|
|
||||||
(do ((j 0 (+ j 1)))
|
|
||||||
((> j jj))
|
|
||||||
(do ((k 0 (+ k 1)))
|
|
||||||
((> k kk))
|
|
||||||
(set! index (+ i (* *d* (+ j (* *d* k)))))
|
|
||||||
(vector-set! (vector-ref *p* *iii*) index #t))))
|
|
||||||
(vector-set! *class* *iii* iclass)
|
|
||||||
(vector-set! *piecemax* *iii* index)
|
|
||||||
(cond ((not (= *iii* typemax))
|
|
||||||
(set! *iii* (+ *iii* 1))))))
|
|
||||||
|
|
||||||
(define (start)
|
|
||||||
(set! *kount* 0)
|
|
||||||
(do ((m 0 (+ m 1)))
|
|
||||||
((> m size))
|
|
||||||
(vector-set! *puzzle* m #t))
|
|
||||||
(do ((i 1 (+ i 1)))
|
|
||||||
((> i 5))
|
|
||||||
(do ((j 1 (+ j 1)))
|
|
||||||
((> j 5))
|
|
||||||
(do ((k 1 (+ k 1)))
|
|
||||||
((> k 5))
|
|
||||||
(vector-set! *puzzle* (+ i (* *d* (+ j (* *d* k)))) #f))))
|
|
||||||
(do ((i 0 (+ i 1)))
|
|
||||||
((> i typemax))
|
|
||||||
(do ((m 0 (+ m 1)))
|
|
||||||
((> m size))
|
|
||||||
(vector-set! (vector-ref *p* i) m #f)))
|
|
||||||
(set! *iii* 0)
|
|
||||||
(definePiece 0 3 1 0)
|
|
||||||
(definePiece 0 1 0 3)
|
|
||||||
(definePiece 0 0 3 1)
|
|
||||||
(definePiece 0 1 3 0)
|
|
||||||
(definePiece 0 3 0 1)
|
|
||||||
(definePiece 0 0 1 3)
|
|
||||||
|
|
||||||
(definePiece 1 2 0 0)
|
|
||||||
(definePiece 1 0 2 0)
|
|
||||||
(definePiece 1 0 0 2)
|
|
||||||
|
|
||||||
(definePiece 2 1 1 0)
|
|
||||||
(definePiece 2 1 0 1)
|
|
||||||
(definePiece 2 0 1 1)
|
|
||||||
|
|
||||||
(definePiece 3 1 1 1)
|
|
||||||
|
|
||||||
(vector-set! *piececount* 0 13)
|
|
||||||
(vector-set! *piececount* 1 3)
|
|
||||||
(vector-set! *piececount* 2 1)
|
|
||||||
(vector-set! *piececount* 3 1)
|
|
||||||
(let ((m (+ (* *d* (+ *d* 1)) 1))
|
|
||||||
(n 0))
|
|
||||||
(cond ((fit 0 m) (set! n (place 0 m)))
|
|
||||||
(else (begin (newline) (display "Error."))))
|
|
||||||
(if (trial n)
|
|
||||||
*kount*
|
|
||||||
#f)))
|
|
||||||
|
|
||||||
(for-each (lambda (i) (vector-set! *p* i (make-vector (+ size 1))))
|
|
||||||
(my-iota (+ typemax 1)))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"puzzle"
|
|
||||||
puzzle-iters
|
|
||||||
(lambda (result) (equal? result 2005))
|
|
||||||
(lambda () (lambda () (start)))))
|
|
|
@ -1,94 +0,0 @@
|
||||||
; The quick-1 benchmark. (Figure 35, page 132.)
|
|
||||||
|
|
||||||
(define (quick-1 v less?)
|
|
||||||
|
|
||||||
(define (helper left right)
|
|
||||||
(if (< left right)
|
|
||||||
(let ((median (partition v left right less?)))
|
|
||||||
(if (< (- median left) (- right median))
|
|
||||||
(begin (helper left (- median 1))
|
|
||||||
(helper (+ median 1) right))
|
|
||||||
(begin (helper (+ median 1) right)
|
|
||||||
(helper left (- median 1)))))
|
|
||||||
v))
|
|
||||||
|
|
||||||
(helper 0 (- (vector-length v) 1)))
|
|
||||||
|
|
||||||
|
|
||||||
(define (partition v left right less?)
|
|
||||||
(let ((mid (vector-ref v right)))
|
|
||||||
|
|
||||||
(define (uploop i)
|
|
||||||
(let ((i (+ i 1)))
|
|
||||||
(if (and (< i right) (less? (vector-ref v i) mid))
|
|
||||||
(uploop i)
|
|
||||||
i)))
|
|
||||||
|
|
||||||
(define (downloop j)
|
|
||||||
(let ((j (- j 1)))
|
|
||||||
(if (and (> j left) (less? mid (vector-ref v j)))
|
|
||||||
(downloop j)
|
|
||||||
j)))
|
|
||||||
|
|
||||||
(define (ploop i j)
|
|
||||||
(let* ((i (uploop i))
|
|
||||||
(j (downloop j)))
|
|
||||||
(let ((tmp (vector-ref v i)))
|
|
||||||
(vector-set! v i (vector-ref v j))
|
|
||||||
(vector-set! v j tmp)
|
|
||||||
(if (< i j)
|
|
||||||
(ploop i j)
|
|
||||||
(begin (vector-set! v j (vector-ref v i))
|
|
||||||
(vector-set! v i (vector-ref v right))
|
|
||||||
(vector-set! v right tmp)
|
|
||||||
i)))))
|
|
||||||
|
|
||||||
(ploop (- left 1) right)))
|
|
||||||
|
|
||||||
; minimal standard random number generator
|
|
||||||
; 32 bit integer version
|
|
||||||
; cacm 31 10, oct 88
|
|
||||||
;
|
|
||||||
|
|
||||||
(define *seed* (list 1))
|
|
||||||
|
|
||||||
(define (srand seed)
|
|
||||||
(set-car! *seed* seed))
|
|
||||||
|
|
||||||
(define (rand)
|
|
||||||
(let* ((hi (quotient (car *seed*) 127773))
|
|
||||||
(lo (modulo (car *seed*) 127773))
|
|
||||||
(test (- (* 16807 lo) (* 2836 hi))))
|
|
||||||
(if (> test 0)
|
|
||||||
(set-car! *seed* test)
|
|
||||||
(set-car! *seed* (+ test 2147483647)))
|
|
||||||
(car *seed*)))
|
|
||||||
|
|
||||||
;; return a random number in the interval [0,n)
|
|
||||||
(define random
|
|
||||||
(lambda (n)
|
|
||||||
(modulo (abs (rand)) n)))
|
|
||||||
|
|
||||||
|
|
||||||
(define (quicksort-benchmark)
|
|
||||||
(let* ((n 30000)
|
|
||||||
(v (make-vector n)))
|
|
||||||
(do ((i 0 (+ i 1)))
|
|
||||||
((= i n))
|
|
||||||
(vector-set! v i (random 4000)))
|
|
||||||
(quick-1 v (lambda (x y) (< x y)))))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"quicksort30"
|
|
||||||
quicksort-iters
|
|
||||||
quicksort-benchmark
|
|
||||||
(lambda (v)
|
|
||||||
(call-with-current-continuation
|
|
||||||
(lambda (return)
|
|
||||||
(do ((i 1 (+ i 1)))
|
|
||||||
((= i (vector-length v))
|
|
||||||
#t)
|
|
||||||
(if (not (<= (vector-ref v (- i 1))
|
|
||||||
(vector-ref v i)))
|
|
||||||
(return #f))))))))
|
|
|
@ -1,784 +0,0 @@
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
; File: sboyer.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)
|
|
||||||
; Language: Scheme
|
|
||||||
; Status: Public Domain
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
|
|
||||||
;;; SBOYER -- Logic programming benchmark, originally written by Bob Boyer.
|
|
||||||
;;; Much less CONS-intensive than NBOYER because it uses Henry Baker's
|
|
||||||
;;; "sharing cons".
|
|
||||||
|
|
||||||
; 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
|
|
||||||
; 1 591777
|
|
||||||
; 2 1813975
|
|
||||||
; 3 5375678
|
|
||||||
; 4 16445406
|
|
||||||
; 5 51507739
|
|
||||||
|
|
||||||
; Sboyer 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 (main . args)
|
|
||||||
(let ((n (if (null? args) 0 (car args))))
|
|
||||||
(setup-boyer)
|
|
||||||
(run-benchmark
|
|
||||||
(string-append "sboyer"
|
|
||||||
(number->string n))
|
|
||||||
sboyer-iters
|
|
||||||
(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))))
|
|
||||||
(lambda (alist term n) (lambda () (test-boyer alist term n)))
|
|
||||||
(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)))))
|
|
||||||
(quote (implies (and (implies x y)
|
|
||||||
(and (implies y z)
|
|
||||||
(and (implies z u)
|
|
||||||
(implies u w))))
|
|
||||||
(implies x w)))
|
|
||||||
n)))
|
|
||||||
|
|
||||||
(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 (_1- 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 (_1- 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 (_1- a)
|
|
||||||
(zero))
|
|
||||||
(equal (_1- 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 (fatal-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 alist term n)
|
|
||||||
(let ((term
|
|
||||||
(apply-subst
|
|
||||||
(translate-alist alist)
|
|
||||||
(translate-term
|
|
||||||
(do ((term term (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
|
|
||||||
|
|
||||||
; The next procedure is Henry Baker's sharing CONS, which avoids
|
|
||||||
; allocation if the result is already in hand.
|
|
||||||
; The REWRITE and REWRITE-ARGS procedures have been modified to
|
|
||||||
; use SCONS instead of CONS.
|
|
||||||
|
|
||||||
(define (scons x y original)
|
|
||||||
(if (and (eq? x (car original))
|
|
||||||
(eq? y (cdr original)))
|
|
||||||
original
|
|
||||||
(cons x y)))
|
|
||||||
|
|
||||||
(define (rewrite term)
|
|
||||||
(set! rewrite-count (+ rewrite-count 1))
|
|
||||||
(cond ((not (pair? term))
|
|
||||||
term)
|
|
||||||
(else (rewrite-with-lemmas (scons (car term)
|
|
||||||
(rewrite-args (cdr term))
|
|
||||||
term)
|
|
||||||
(get-lemmas (car term))))))
|
|
||||||
|
|
||||||
(define (rewrite-args lst)
|
|
||||||
(cond ((null? lst)
|
|
||||||
'())
|
|
||||||
(else (scons (rewrite (car lst))
|
|
||||||
(rewrite-args (cdr lst))
|
|
||||||
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 (alist term n)
|
|
||||||
(set! rewrite-count 0)
|
|
||||||
(let ((answer (test alist term n)))
|
|
||||||
; (write rewrite-count)
|
|
||||||
; (display " rewrites")
|
|
||||||
; (newline)
|
|
||||||
(if answer
|
|
||||||
rewrite-count
|
|
||||||
#f)))))
|
|
File diff suppressed because it is too large
Load Diff
|
@ -1,188 +0,0 @@
|
||||||
;;; SIMPLEX -- Simplex algorithm.
|
|
||||||
|
|
||||||
(define (matrix-rows a) (vector-length a))
|
|
||||||
(define (matrix-columns a) (FLOATvector-length (vector-ref a 0)))
|
|
||||||
(define (matrix-ref a i j) (FLOATvector-ref (vector-ref a i) j))
|
|
||||||
(define (matrix-set! a i j x) (FLOATvector-set! (vector-ref a i) j x))
|
|
||||||
|
|
||||||
(define (fuck-up)
|
|
||||||
(fatal-error "This shouldn't happen"))
|
|
||||||
|
|
||||||
(define (simplex a m1 m2 m3)
|
|
||||||
(define *epsilon* 1e-6)
|
|
||||||
;(define *epsilon* 0.000001)
|
|
||||||
(if (not (and (>= m1 0)
|
|
||||||
(>= m2 0)
|
|
||||||
(>= m3 0)
|
|
||||||
(= (matrix-rows a) (+ m1 m2 m3 2))))
|
|
||||||
(fuck-up))
|
|
||||||
(let* ((m12 (+ m1 m2 1))
|
|
||||||
(m (- (matrix-rows a) 2))
|
|
||||||
(n (- (matrix-columns a) 1))
|
|
||||||
(l1 (make-vector n))
|
|
||||||
(l2 (make-vector m))
|
|
||||||
(l3 (make-vector m2))
|
|
||||||
(nl1 n)
|
|
||||||
(iposv (make-vector m))
|
|
||||||
(izrov (make-vector n))
|
|
||||||
(ip 0)
|
|
||||||
(kp 0)
|
|
||||||
(bmax 0.0)
|
|
||||||
(one? #f)
|
|
||||||
(pass2? #t))
|
|
||||||
(define (simp1 mm abs?)
|
|
||||||
(set! kp (vector-ref l1 0))
|
|
||||||
(set! bmax (matrix-ref a mm kp))
|
|
||||||
(do ((k 1 (+ k 1))) ((>= k nl1))
|
|
||||||
(if (FLOATpositive?
|
|
||||||
(if abs?
|
|
||||||
(FLOAT- (FLOATabs (matrix-ref a mm (vector-ref l1 k)))
|
|
||||||
(FLOATabs bmax))
|
|
||||||
(FLOAT- (matrix-ref a mm (vector-ref l1 k)) bmax)))
|
|
||||||
(begin
|
|
||||||
(set! kp (vector-ref l1 k))
|
|
||||||
(set! bmax (matrix-ref a mm (vector-ref l1 k)))))))
|
|
||||||
(define (simp2)
|
|
||||||
(set! ip 0)
|
|
||||||
(let ((q1 0.0)
|
|
||||||
(flag? #f))
|
|
||||||
(do ((i 0 (+ i 1))) ((= i m))
|
|
||||||
(if flag?
|
|
||||||
(if (FLOAT< (matrix-ref a (vector-ref l2 i) kp) (FLOAT- *epsilon*))
|
|
||||||
(begin
|
|
||||||
(let ((q (FLOAT/ (FLOAT- (matrix-ref a (vector-ref l2 i) 0))
|
|
||||||
(matrix-ref a (vector-ref l2 i) kp))))
|
|
||||||
(cond
|
|
||||||
((FLOAT< q q1)
|
|
||||||
(set! ip (vector-ref l2 i))
|
|
||||||
(set! q1 q))
|
|
||||||
((FLOAT= q q1)
|
|
||||||
(let ((qp 0.0)
|
|
||||||
(q0 0.0))
|
|
||||||
(let loop ((k 1))
|
|
||||||
(if (<= k n)
|
|
||||||
(begin
|
|
||||||
(set! qp (FLOAT/ (FLOAT- (matrix-ref a ip k))
|
|
||||||
(matrix-ref a ip kp)))
|
|
||||||
(set! q0 (FLOAT/ (FLOAT-
|
|
||||||
(matrix-ref a (vector-ref l2 i) k))
|
|
||||||
(matrix-ref a (vector-ref l2 i) kp)))
|
|
||||||
(if (FLOAT= q0 qp)
|
|
||||||
(loop (+ k 1))))))
|
|
||||||
(if (FLOAT< q0 qp)
|
|
||||||
(set! ip (vector-ref l2 i)))))))))
|
|
||||||
(if (FLOAT< (matrix-ref a (vector-ref l2 i) kp) (FLOAT- *epsilon*))
|
|
||||||
(begin
|
|
||||||
(set! q1 (FLOAT/ (FLOAT- (matrix-ref a (vector-ref l2 i) 0))
|
|
||||||
(matrix-ref a (vector-ref l2 i) kp)))
|
|
||||||
(set! ip (vector-ref l2 i))
|
|
||||||
(set! flag? #t)))))))
|
|
||||||
(define (simp3 one?)
|
|
||||||
(let ((piv (FLOAT/ (matrix-ref a ip kp))))
|
|
||||||
(do ((ii 0 (+ ii 1))) ((= ii (+ m (if one? 2 1))))
|
|
||||||
(if (not (= ii ip))
|
|
||||||
(begin
|
|
||||||
(matrix-set! a ii kp (FLOAT* piv (matrix-ref a ii kp)))
|
|
||||||
(do ((kk 0 (+ kk 1))) ((= kk (+ n 1)))
|
|
||||||
(if (not (= kk kp))
|
|
||||||
(matrix-set! a ii kk (FLOAT- (matrix-ref a ii kk)
|
|
||||||
(FLOAT* (matrix-ref a ip kk)
|
|
||||||
(matrix-ref a ii kp)))))))))
|
|
||||||
(do ((kk 0 (+ kk 1))) ((= kk (+ n 1)))
|
|
||||||
(if (not (= kk kp))
|
|
||||||
(matrix-set! a ip kk (FLOAT* (FLOAT- piv) (matrix-ref a ip kk)))))
|
|
||||||
(matrix-set! a ip kp piv)))
|
|
||||||
(do ((k 0 (+ k 1))) ((= k n))
|
|
||||||
(vector-set! l1 k (+ k 1))
|
|
||||||
(vector-set! izrov k k))
|
|
||||||
(do ((i 0 (+ i 1))) ((= i m))
|
|
||||||
(if (FLOATnegative? (matrix-ref a (+ i 1) 0))
|
|
||||||
(fuck-up))
|
|
||||||
(vector-set! l2 i (+ i 1))
|
|
||||||
(vector-set! iposv i (+ n i)))
|
|
||||||
(do ((i 0 (+ i 1))) ((= i m2)) (vector-set! l3 i #t))
|
|
||||||
(if (positive? (+ m2 m3))
|
|
||||||
(begin
|
|
||||||
(do ((k 0 (+ k 1))) ((= k (+ n 1)))
|
|
||||||
(do ((i (+ m1 1) (+ i 1)) (sum 0.0 (FLOAT+ sum (matrix-ref a i k))))
|
|
||||||
((> i m) (matrix-set! a (+ m 1) k (FLOAT- sum)))))
|
|
||||||
(let loop ()
|
|
||||||
(simp1 (+ m 1) #f)
|
|
||||||
(cond
|
|
||||||
((FLOAT<= bmax *epsilon*)
|
|
||||||
(cond ((FLOAT< (matrix-ref a (+ m 1) 0) (FLOAT- *epsilon*))
|
|
||||||
(set! pass2? #f))
|
|
||||||
((FLOAT<= (matrix-ref a (+ m 1) 0) *epsilon*)
|
|
||||||
(let loop ((ip1 m12))
|
|
||||||
(if (<= ip1 m)
|
|
||||||
(cond ((= (vector-ref iposv (- ip1 1)) (+ ip n -1))
|
|
||||||
(simp1 ip1 #t)
|
|
||||||
(cond ((FLOATpositive? bmax)
|
|
||||||
(set! ip ip1)
|
|
||||||
(set! one? #t))
|
|
||||||
(else
|
|
||||||
(loop (+ ip1 1)))))
|
|
||||||
(else
|
|
||||||
(loop (+ ip1 1))))
|
|
||||||
(do ((i (+ m1 1) (+ i 1))) ((>= i m12))
|
|
||||||
(if (vector-ref l3 (- i (+ m1 1)))
|
|
||||||
(do ((k 0 (+ k 1))) ((= k (+ n 1)))
|
|
||||||
(matrix-set! a i k (FLOAT- (matrix-ref a i k)))))))))
|
|
||||||
(else (simp2) (if (zero? ip) (set! pass2? #f) (set! one? #t)))))
|
|
||||||
(else (simp2) (if (zero? ip) (set! pass2? #f) (set! one? #t))))
|
|
||||||
(if one?
|
|
||||||
(begin
|
|
||||||
(set! one? #f)
|
|
||||||
(simp3 #t)
|
|
||||||
(cond
|
|
||||||
((>= (vector-ref iposv (- ip 1)) (+ n m12 -1))
|
|
||||||
(let loop ((k 0))
|
|
||||||
(cond
|
|
||||||
((and (< k nl1) (not (= kp (vector-ref l1 k))))
|
|
||||||
(loop (+ k 1)))
|
|
||||||
(else
|
|
||||||
(set! nl1 (- nl1 1))
|
|
||||||
(do ((is k (+ is 1))) ((>= is nl1))
|
|
||||||
(vector-set! l1 is (vector-ref l1 (+ is 1))))
|
|
||||||
(matrix-set! a (+ m 1) kp (FLOAT+ (matrix-ref a (+ m 1) kp) 1.0))
|
|
||||||
(do ((i 0 (+ i 1))) ((= i (+ m 2)))
|
|
||||||
(matrix-set! a i kp (FLOAT- (matrix-ref a i kp))))))))
|
|
||||||
((and (>= (vector-ref iposv (- ip 1)) (+ n m1))
|
|
||||||
(vector-ref l3 (- (vector-ref iposv (- ip 1)) (+ m1 n))))
|
|
||||||
(vector-set! l3 (- (vector-ref iposv (- ip 1)) (+ m1 n)) #f)
|
|
||||||
(matrix-set! a (+ m 1) kp (FLOAT+ (matrix-ref a (+ m 1) kp) 1.0))
|
|
||||||
(do ((i 0 (+ i 1))) ((= i (+ m 2)))
|
|
||||||
(matrix-set! a i kp (FLOAT- (matrix-ref a i kp))))))
|
|
||||||
(let ((t (vector-ref izrov (- kp 1))))
|
|
||||||
(vector-set! izrov (- kp 1) (vector-ref iposv (- ip 1)))
|
|
||||||
(vector-set! iposv (- ip 1) t))
|
|
||||||
(loop))))))
|
|
||||||
(and pass2?
|
|
||||||
(let loop ()
|
|
||||||
(simp1 0 #f)
|
|
||||||
(cond
|
|
||||||
((FLOATpositive? bmax)
|
|
||||||
(simp2)
|
|
||||||
(cond ((zero? ip) #t)
|
|
||||||
(else (simp3 #f)
|
|
||||||
(let ((t (vector-ref izrov (- kp 1))))
|
|
||||||
(vector-set! izrov (- kp 1) (vector-ref iposv (- ip 1)))
|
|
||||||
(vector-set! iposv (- ip 1) t))
|
|
||||||
(loop))))
|
|
||||||
(else (list iposv izrov)))))))
|
|
||||||
|
|
||||||
(define (test)
|
|
||||||
(simplex (vector (FLOATvector 0.0 1.0 1.0 3.0 -0.5)
|
|
||||||
(FLOATvector 740.0 -1.0 0.0 -2.0 0.0)
|
|
||||||
(FLOATvector 0.0 0.0 -2.0 0.0 7.0)
|
|
||||||
(FLOATvector 0.5 0.0 -1.0 1.0 -2.0)
|
|
||||||
(FLOATvector 9.0 -1.0 -1.0 -1.0 -1.0)
|
|
||||||
(FLOATvector 0.0 0.0 0.0 0.0 0.0))
|
|
||||||
2 1 1))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"simplex"
|
|
||||||
simplex-iters
|
|
||||||
(lambda (result) (equal? result '(#(4 1 3 2) #(0 5 7 6))))
|
|
||||||
(lambda () (lambda () (test)))))
|
|
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
|
@ -1,29 +0,0 @@
|
||||||
;;; STRING -- One of the Kernighan and Van Wyk benchmarks.
|
|
||||||
|
|
||||||
(define s "abcdef")
|
|
||||||
|
|
||||||
(define (grow)
|
|
||||||
(set! s (string-append "123" s "456" s "789"))
|
|
||||||
(set! s (string-append
|
|
||||||
(substring s (quotient (string-length s) 2) (string-length s))
|
|
||||||
(substring s 0 (+ 1 (quotient (string-length s) 2)))))
|
|
||||||
s)
|
|
||||||
|
|
||||||
(define (trial n)
|
|
||||||
(do ((i 0 (+ i 1)))
|
|
||||||
((> (string-length s) n) (string-length s))
|
|
||||||
(grow)))
|
|
||||||
|
|
||||||
(define (my-try n)
|
|
||||||
(do ((i 0 (+ i 1)))
|
|
||||||
((>= i 10) (string-length s))
|
|
||||||
(set! s "abcdef")
|
|
||||||
(trial n)))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"string"
|
|
||||||
string-iters
|
|
||||||
(lambda (result) (equal? result 524278))
|
|
||||||
(lambda (n) (lambda () (my-try n)))
|
|
||||||
500000))
|
|
|
@ -1,10 +0,0 @@
|
||||||
;;; SUCCEED - Test of success condition.
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"succeed"
|
|
||||||
1
|
|
||||||
(lambda (result)
|
|
||||||
(equal? result #f))
|
|
||||||
(lambda (f) (lambda () f))
|
|
||||||
#f))
|
|
|
@ -1,15 +0,0 @@
|
||||||
;;; SUM -- Compute sum of integers from 0 to 10000
|
|
||||||
|
|
||||||
(define (run n)
|
|
||||||
(let loop ((i n) (sum 0))
|
|
||||||
(if (< i 0)
|
|
||||||
sum
|
|
||||||
(loop (- i 1) (+ i sum)))))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"sum"
|
|
||||||
sum-iters
|
|
||||||
(lambda (result) (equal? result 50005000))
|
|
||||||
(lambda (n) (lambda () (run n)))
|
|
||||||
10000))
|
|
|
@ -1,26 +0,0 @@
|
||||||
;;; SUM1 -- One of the Kernighan and Van Wyk benchmarks.
|
|
||||||
|
|
||||||
(define inport #f)
|
|
||||||
|
|
||||||
(define (sumport port sum-so-far)
|
|
||||||
(let ((x (read port)))
|
|
||||||
(if (eof-object? x)
|
|
||||||
sum-so-far
|
|
||||||
(sumport port (FLOAT+ x sum-so-far)))))
|
|
||||||
|
|
||||||
(define (sum port)
|
|
||||||
(sumport port 0.0))
|
|
||||||
|
|
||||||
(define (go)
|
|
||||||
(set! inport (open-input-file "../../src/rn100"))
|
|
||||||
(let ((result (sum inport)))
|
|
||||||
(close-input-port inport)
|
|
||||||
result))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"sum1"
|
|
||||||
sum1-iters
|
|
||||||
(lambda (result) (and (FLOAT>= result 15794.974999999)
|
|
||||||
(FLOAT<= result 15794.975000001)))
|
|
||||||
(lambda () (lambda () (go)))))
|
|
|
@ -1,15 +0,0 @@
|
||||||
;;; SUMFP -- Compute sum of integers from 0 to 10000 using floating point
|
|
||||||
|
|
||||||
(define (run n)
|
|
||||||
(let loop ((i n) (sum 0.))
|
|
||||||
(if (FLOAT< i 0.)
|
|
||||||
sum
|
|
||||||
(loop (FLOAT- i 1.) (FLOAT+ i sum)))))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"sumfp"
|
|
||||||
sumfp-iters
|
|
||||||
(lambda (result) (equal? result 50005000.))
|
|
||||||
(lambda (n) (lambda () (run n)))
|
|
||||||
10000.))
|
|
|
@ -1,27 +0,0 @@
|
||||||
;;; SUMLOOP -- One of the Kernighan and Van Wyk benchmarks.
|
|
||||||
|
|
||||||
(define sum 0)
|
|
||||||
|
|
||||||
(define (tail-rec-aux i n)
|
|
||||||
(if (< i n)
|
|
||||||
(begin (set! sum (+ sum 1)) (tail-rec-aux (+ i 1) n))
|
|
||||||
sum))
|
|
||||||
|
|
||||||
(define (tail-rec-loop n)
|
|
||||||
(set! sum 0)
|
|
||||||
(tail-rec-aux 0 n)
|
|
||||||
sum)
|
|
||||||
|
|
||||||
(define (do-loop n)
|
|
||||||
(set! sum 0)
|
|
||||||
(do ((i 0 (+ i 1)))
|
|
||||||
((>= i n) sum)
|
|
||||||
(set! sum (+ sum 1))))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"sumloop"
|
|
||||||
sumloop-iters
|
|
||||||
(lambda (result) (equal? result 100000000))
|
|
||||||
(lambda (n) (lambda () (do-loop n)))
|
|
||||||
100000000))
|
|
|
@ -1,37 +0,0 @@
|
||||||
;;; TAIL -- One of the Kernighan and Van Wyk benchmarks.
|
|
||||||
|
|
||||||
(define inport #f)
|
|
||||||
(define outport #f)
|
|
||||||
|
|
||||||
(define (readline port line-so-far)
|
|
||||||
(let ((x (read-char port)))
|
|
||||||
(cond ((eof-object? x)
|
|
||||||
x)
|
|
||||||
((char=? x #\newline)
|
|
||||||
(list->string (reverse
|
|
||||||
(cons x line-so-far))))
|
|
||||||
(#t (readline port (cons x line-so-far))))))
|
|
||||||
|
|
||||||
(define (tail-r-aux port file-so-far)
|
|
||||||
(let ((x (readline port '())))
|
|
||||||
(if (eof-object? x)
|
|
||||||
(begin
|
|
||||||
(display file-so-far outport)
|
|
||||||
(close-output-port outport))
|
|
||||||
(tail-r-aux port (cons x file-so-far)))))
|
|
||||||
|
|
||||||
(define (tail-r port)
|
|
||||||
(tail-r-aux port '()))
|
|
||||||
|
|
||||||
(define (go)
|
|
||||||
(set! inport (open-input-file "../../src/bib"))
|
|
||||||
(set! outport (open-output-file "foo"))
|
|
||||||
(tail-r inport)
|
|
||||||
(close-input-port inport))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"tail"
|
|
||||||
tail-iters
|
|
||||||
(lambda (result) #t)
|
|
||||||
(lambda () (lambda () (go)))))
|
|
|
@ -1,27 +0,0 @@
|
||||||
;;; TAK -- A vanilla version of the TAKeuchi function.
|
|
||||||
|
|
||||||
(define (tak x y z)
|
|
||||||
(if (not (< y x))
|
|
||||||
z
|
|
||||||
(tak (tak (- x 1) y z)
|
|
||||||
(tak (- y 1) z x)
|
|
||||||
(tak (- z 1) x y))))
|
|
||||||
|
|
||||||
;;; (define (tak x y z)
|
|
||||||
;;; (if (not (#%$fx< y x))
|
|
||||||
;;; z
|
|
||||||
;;; (tak (tak (fxsub1 x) y z)
|
|
||||||
;;; (tak (fxsub1 y) z x)
|
|
||||||
;;; (tak (fxsub1 z) x y))))
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"tak"
|
|
||||||
tak-iters
|
|
||||||
(lambda (result) (equal? result 7))
|
|
||||||
(lambda (x y z) (lambda () (tak x y z)))
|
|
||||||
18
|
|
||||||
12
|
|
||||||
6))
|
|
|
@ -1,33 +0,0 @@
|
||||||
;;; TAKL -- The TAKeuchi function using lists as counters.
|
|
||||||
|
|
||||||
(define (listn n)
|
|
||||||
(if (= n 0)
|
|
||||||
'()
|
|
||||||
(cons n (listn (- n 1)))))
|
|
||||||
|
|
||||||
(define l18 (listn 18))
|
|
||||||
(define l12 (listn 12))
|
|
||||||
(define l6 (listn 6))
|
|
||||||
|
|
||||||
(define (mas x y z)
|
|
||||||
(if (not (shorterp y x))
|
|
||||||
z
|
|
||||||
(mas (mas (cdr x) y z)
|
|
||||||
(mas (cdr y) z x)
|
|
||||||
(mas (cdr z) x y))))
|
|
||||||
|
|
||||||
(define (shorterp x y)
|
|
||||||
(and (not (null? y))
|
|
||||||
(or (null? x)
|
|
||||||
(shorterp (cdr x)
|
|
||||||
(cdr y)))))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"takl"
|
|
||||||
takl-iters
|
|
||||||
(lambda (result) (equal? result '(7 6 5 4 3 2 1)))
|
|
||||||
(lambda (x y z) (lambda () (mas x y z)))
|
|
||||||
l18
|
|
||||||
l12
|
|
||||||
l6))
|
|
|
@ -1,28 +0,0 @@
|
||||||
;;; TFIB -- Like FIB but using threads.
|
|
||||||
|
|
||||||
(define (tfib n)
|
|
||||||
(if (< n 2)
|
|
||||||
1
|
|
||||||
(let ((x (make-thread (lambda () (tfib (- n 2))))))
|
|
||||||
(thread-start! x)
|
|
||||||
(let ((y (tfib (- n 1))))
|
|
||||||
(+ (thread-join! x) y)))))
|
|
||||||
|
|
||||||
(define (go n repeat)
|
|
||||||
(let loop ((repeat repeat)
|
|
||||||
(result '()))
|
|
||||||
(if (> repeat 0)
|
|
||||||
(let ((x (make-thread (lambda () (tfib n)))))
|
|
||||||
(thread-start! x)
|
|
||||||
(let ((r (thread-join! x)))
|
|
||||||
(loop (- repeat 1) r)))
|
|
||||||
result)))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"tfib"
|
|
||||||
tfib-iters
|
|
||||||
(lambda (result) (equal? result 610))
|
|
||||||
(lambda (n repeat) (lambda () (go n repeat)))
|
|
||||||
14
|
|
||||||
100))
|
|
|
@ -1,144 +0,0 @@
|
||||||
;;; TRAV1 -- Benchmark which creates and traverses a tree structure.
|
|
||||||
|
|
||||||
(define (make-node)
|
|
||||||
(vector 'node '() '() (snb) #f #f #f #f #f #f #f))
|
|
||||||
|
|
||||||
(define (node-parents node) (vector-ref node 1))
|
|
||||||
(define (node-sons node) (vector-ref node 2))
|
|
||||||
(define (node-sn node) (vector-ref node 3))
|
|
||||||
(define (node-entry1 node) (vector-ref node 4))
|
|
||||||
(define (node-entry2 node) (vector-ref node 5))
|
|
||||||
(define (node-entry3 node) (vector-ref node 6))
|
|
||||||
(define (node-entry4 node) (vector-ref node 7))
|
|
||||||
(define (node-entry5 node) (vector-ref node 8))
|
|
||||||
(define (node-entry6 node) (vector-ref node 9))
|
|
||||||
(define (node-mark node) (vector-ref node 10))
|
|
||||||
|
|
||||||
(define (node-parents-set! node v) (vector-set! node 1 v))
|
|
||||||
(define (node-sons-set! node v) (vector-set! node 2 v))
|
|
||||||
(define (node-sn-set! node v) (vector-set! node 3 v))
|
|
||||||
(define (node-entry1-set! node v) (vector-set! node 4 v))
|
|
||||||
(define (node-entry2-set! node v) (vector-set! node 5 v))
|
|
||||||
(define (node-entry3-set! node v) (vector-set! node 6 v))
|
|
||||||
(define (node-entry4-set! node v) (vector-set! node 7 v))
|
|
||||||
(define (node-entry5-set! node v) (vector-set! node 8 v))
|
|
||||||
(define (node-entry6-set! node v) (vector-set! node 9 v))
|
|
||||||
(define (node-mark-set! node v) (vector-set! node 10 v))
|
|
||||||
|
|
||||||
(define *sn* 0)
|
|
||||||
(define *rand* 21)
|
|
||||||
(define *count* 0)
|
|
||||||
(define *marker* #f)
|
|
||||||
(define *root* '())
|
|
||||||
|
|
||||||
(define (snb)
|
|
||||||
(set! *sn* (+ 1 *sn*))
|
|
||||||
*sn*)
|
|
||||||
|
|
||||||
(define (seed)
|
|
||||||
(set! *rand* 21)
|
|
||||||
*rand*)
|
|
||||||
|
|
||||||
(define (traverse-random)
|
|
||||||
(set! *rand* (remainder (* *rand* 17) 251))
|
|
||||||
*rand*)
|
|
||||||
|
|
||||||
(define (traverse-remove n q)
|
|
||||||
(cond ((eq? (cdr (car q)) (car q))
|
|
||||||
(let ((x (caar q))) (set-car! q '()) x))
|
|
||||||
((= n 0)
|
|
||||||
(let ((x (caar q)))
|
|
||||||
(do ((p (car q) (cdr p)))
|
|
||||||
((eq? (cdr p) (car q))
|
|
||||||
(set-cdr! p (cdr (car q)))
|
|
||||||
(set-car! q p)))
|
|
||||||
x))
|
|
||||||
(else (do ((n n (- n 1))
|
|
||||||
(q (car q) (cdr q))
|
|
||||||
(p (cdr (car q)) (cdr p)))
|
|
||||||
((= n 0) (let ((x (car q))) (set-cdr! q p) x))))))
|
|
||||||
|
|
||||||
(define (traverse-select n q)
|
|
||||||
(do ((n n (- n 1))
|
|
||||||
(q (car q) (cdr q)))
|
|
||||||
((= n 0) (car q))))
|
|
||||||
|
|
||||||
(define (add a q)
|
|
||||||
(cond ((null? q)
|
|
||||||
`(,(let ((x `(,a)))
|
|
||||||
(set-cdr! x x) x)))
|
|
||||||
((null? (car q))
|
|
||||||
(let ((x `(,a)))
|
|
||||||
(set-cdr! x x)
|
|
||||||
(set-car! q x)
|
|
||||||
q))
|
|
||||||
; the CL version had a useless set-car! in the next line (wc)
|
|
||||||
(else (set-cdr! (car q) `(,a ,@(cdr (car q))))
|
|
||||||
q)))
|
|
||||||
|
|
||||||
(define (create-structure n)
|
|
||||||
(let ((a `(,(make-node))))
|
|
||||||
(do ((m (- n 1) (- m 1))
|
|
||||||
(p a))
|
|
||||||
((= m 0)
|
|
||||||
(set! a `(,(begin (set-cdr! p a) p)))
|
|
||||||
(do ((unused a)
|
|
||||||
(used (add (traverse-remove 0 a) '()))
|
|
||||||
(x '())
|
|
||||||
(y '()))
|
|
||||||
((null? (car unused))
|
|
||||||
(find-root (traverse-select 0 used) n))
|
|
||||||
(set! x (traverse-remove (remainder (traverse-random) n) unused))
|
|
||||||
(set! y (traverse-select (remainder (traverse-random) n) used))
|
|
||||||
(add x used)
|
|
||||||
(node-sons-set! y `(,x ,@(node-sons y)))
|
|
||||||
(node-parents-set! x `(,y ,@(node-parents x))) ))
|
|
||||||
(set! a (cons (make-node) a)))))
|
|
||||||
|
|
||||||
(define (find-root node n)
|
|
||||||
(do ((n n (- n 1)))
|
|
||||||
((or (= n 0) (null? (node-parents node)))
|
|
||||||
node)
|
|
||||||
(set! node (car (node-parents node)))))
|
|
||||||
|
|
||||||
(define (travers node mark)
|
|
||||||
(cond ((eq? (node-mark node) mark) #f)
|
|
||||||
(else (node-mark-set! node mark)
|
|
||||||
(set! *count* (+ 1 *count*))
|
|
||||||
(node-entry1-set! node (not (node-entry1 node)))
|
|
||||||
(node-entry2-set! node (not (node-entry2 node)))
|
|
||||||
(node-entry3-set! node (not (node-entry3 node)))
|
|
||||||
(node-entry4-set! node (not (node-entry4 node)))
|
|
||||||
(node-entry5-set! node (not (node-entry5 node)))
|
|
||||||
(node-entry6-set! node (not (node-entry6 node)))
|
|
||||||
(do ((sons (node-sons node) (cdr sons)))
|
|
||||||
((null? sons) #f)
|
|
||||||
(travers (car sons) mark)))))
|
|
||||||
|
|
||||||
(define (traverse root)
|
|
||||||
(let ((*count* 0))
|
|
||||||
(travers root (begin (set! *marker* (not *marker*)) *marker*))
|
|
||||||
*count*))
|
|
||||||
|
|
||||||
(define (init-traverse) ; Changed from defmacro to defun \bs
|
|
||||||
(set! *root* (create-structure 100))
|
|
||||||
#f)
|
|
||||||
|
|
||||||
(define (run-traverse) ; Changed from defmacro to defun \bs
|
|
||||||
(do ((i 50 (- i 1)))
|
|
||||||
((= i 0))
|
|
||||||
(traverse *root*)
|
|
||||||
(traverse *root*)
|
|
||||||
(traverse *root*)
|
|
||||||
(traverse *root*)
|
|
||||||
(traverse *root*)))
|
|
||||||
|
|
||||||
;;; to initialize, call: (init-traverse)
|
|
||||||
;;; to run traverse, call: (run-traverse)
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"trav1"
|
|
||||||
trav1-iters
|
|
||||||
(lambda (result) #t)
|
|
||||||
(lambda () (lambda () (init-traverse)))))
|
|
|
@ -1,146 +0,0 @@
|
||||||
;;; TRAV2 -- Benchmark which creates and traverses a tree structure.
|
|
||||||
|
|
||||||
(define (make-node)
|
|
||||||
(vector 'node '() '() (snb) #f #f #f #f #f #f #f))
|
|
||||||
|
|
||||||
(define (node-parents node) (vector-ref node 1))
|
|
||||||
(define (node-sons node) (vector-ref node 2))
|
|
||||||
(define (node-sn node) (vector-ref node 3))
|
|
||||||
(define (node-entry1 node) (vector-ref node 4))
|
|
||||||
(define (node-entry2 node) (vector-ref node 5))
|
|
||||||
(define (node-entry3 node) (vector-ref node 6))
|
|
||||||
(define (node-entry4 node) (vector-ref node 7))
|
|
||||||
(define (node-entry5 node) (vector-ref node 8))
|
|
||||||
(define (node-entry6 node) (vector-ref node 9))
|
|
||||||
(define (node-mark node) (vector-ref node 10))
|
|
||||||
|
|
||||||
(define (node-parents-set! node v) (vector-set! node 1 v))
|
|
||||||
(define (node-sons-set! node v) (vector-set! node 2 v))
|
|
||||||
(define (node-sn-set! node v) (vector-set! node 3 v))
|
|
||||||
(define (node-entry1-set! node v) (vector-set! node 4 v))
|
|
||||||
(define (node-entry2-set! node v) (vector-set! node 5 v))
|
|
||||||
(define (node-entry3-set! node v) (vector-set! node 6 v))
|
|
||||||
(define (node-entry4-set! node v) (vector-set! node 7 v))
|
|
||||||
(define (node-entry5-set! node v) (vector-set! node 8 v))
|
|
||||||
(define (node-entry6-set! node v) (vector-set! node 9 v))
|
|
||||||
(define (node-mark-set! node v) (vector-set! node 10 v))
|
|
||||||
|
|
||||||
(define *sn* 0)
|
|
||||||
(define *rand* 21)
|
|
||||||
(define *count* 0)
|
|
||||||
(define *marker* #f)
|
|
||||||
(define *root* '())
|
|
||||||
|
|
||||||
(define (snb)
|
|
||||||
(set! *sn* (+ 1 *sn*))
|
|
||||||
*sn*)
|
|
||||||
|
|
||||||
(define (seed)
|
|
||||||
(set! *rand* 21)
|
|
||||||
*rand*)
|
|
||||||
|
|
||||||
(define (traverse-random)
|
|
||||||
(set! *rand* (remainder (* *rand* 17) 251))
|
|
||||||
*rand*)
|
|
||||||
|
|
||||||
(define (traverse-remove n q)
|
|
||||||
(cond ((eq? (cdr (car q)) (car q))
|
|
||||||
(let ((x (caar q))) (set-car! q '()) x))
|
|
||||||
((= n 0)
|
|
||||||
(let ((x (caar q)))
|
|
||||||
(do ((p (car q) (cdr p)))
|
|
||||||
((eq? (cdr p) (car q))
|
|
||||||
(set-cdr! p (cdr (car q)))
|
|
||||||
(set-car! q p)))
|
|
||||||
x))
|
|
||||||
(else (do ((n n (- n 1))
|
|
||||||
(q (car q) (cdr q))
|
|
||||||
(p (cdr (car q)) (cdr p)))
|
|
||||||
((= n 0) (let ((x (car q))) (set-cdr! q p) x))))))
|
|
||||||
|
|
||||||
(define (traverse-select n q)
|
|
||||||
(do ((n n (- n 1))
|
|
||||||
(q (car q) (cdr q)))
|
|
||||||
((= n 0) (car q))))
|
|
||||||
|
|
||||||
(define (add a q)
|
|
||||||
(cond ((null? q)
|
|
||||||
`(,(let ((x `(,a)))
|
|
||||||
(set-cdr! x x) x)))
|
|
||||||
((null? (car q))
|
|
||||||
(let ((x `(,a)))
|
|
||||||
(set-cdr! x x)
|
|
||||||
(set-car! q x)
|
|
||||||
q))
|
|
||||||
; the CL version had a useless set-car! in the next line (wc)
|
|
||||||
(else (set-cdr! (car q) `(,a ,@(cdr (car q))))
|
|
||||||
q)))
|
|
||||||
|
|
||||||
(define (create-structure n)
|
|
||||||
(let ((a `(,(make-node))))
|
|
||||||
(do ((m (- n 1) (- m 1))
|
|
||||||
(p a))
|
|
||||||
((= m 0)
|
|
||||||
(set! a `(,(begin (set-cdr! p a) p)))
|
|
||||||
(do ((unused a)
|
|
||||||
(used (add (traverse-remove 0 a) '()))
|
|
||||||
(x '())
|
|
||||||
(y '()))
|
|
||||||
((null? (car unused))
|
|
||||||
(find-root (traverse-select 0 used) n))
|
|
||||||
(set! x (traverse-remove (remainder (traverse-random) n) unused))
|
|
||||||
(set! y (traverse-select (remainder (traverse-random) n) used))
|
|
||||||
(add x used)
|
|
||||||
(node-sons-set! y `(,x ,@(node-sons y)))
|
|
||||||
(node-parents-set! x `(,y ,@(node-parents x))) ))
|
|
||||||
(set! a (cons (make-node) a)))))
|
|
||||||
|
|
||||||
(define (find-root node n)
|
|
||||||
(do ((n n (- n 1)))
|
|
||||||
((or (= n 0) (null? (node-parents node)))
|
|
||||||
node)
|
|
||||||
(set! node (car (node-parents node)))))
|
|
||||||
|
|
||||||
(define (travers node mark)
|
|
||||||
(cond ((eq? (node-mark node) mark) #f)
|
|
||||||
(else (node-mark-set! node mark)
|
|
||||||
(set! *count* (+ 1 *count*))
|
|
||||||
(node-entry1-set! node (not (node-entry1 node)))
|
|
||||||
(node-entry2-set! node (not (node-entry2 node)))
|
|
||||||
(node-entry3-set! node (not (node-entry3 node)))
|
|
||||||
(node-entry4-set! node (not (node-entry4 node)))
|
|
||||||
(node-entry5-set! node (not (node-entry5 node)))
|
|
||||||
(node-entry6-set! node (not (node-entry6 node)))
|
|
||||||
(do ((sons (node-sons node) (cdr sons)))
|
|
||||||
((null? sons) #f)
|
|
||||||
(travers (car sons) mark)))))
|
|
||||||
|
|
||||||
(define (traverse root)
|
|
||||||
(let ((*count* 0))
|
|
||||||
(travers root (begin (set! *marker* (not *marker*)) *marker*))
|
|
||||||
*count*))
|
|
||||||
|
|
||||||
(define (init-traverse) ; Changed from defmacro to defun \bs
|
|
||||||
(set! *root* (create-structure 100))
|
|
||||||
#f)
|
|
||||||
|
|
||||||
(define (run-traverse) ; Changed from defmacro to defun \bs
|
|
||||||
(do ((i 50 (- i 1)))
|
|
||||||
((= i 0))
|
|
||||||
(traverse *root*)
|
|
||||||
(traverse *root*)
|
|
||||||
(traverse *root*)
|
|
||||||
(traverse *root*)
|
|
||||||
(traverse *root*)))
|
|
||||||
|
|
||||||
;;; to initialize, call: (init-traverse)
|
|
||||||
;;; to run traverse, call: (run-traverse)
|
|
||||||
|
|
||||||
(init-traverse)
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"trav2"
|
|
||||||
trav2-iters
|
|
||||||
(lambda (result) #t)
|
|
||||||
(lambda () (lambda () (run-traverse)))))
|
|
|
@ -1,60 +0,0 @@
|
||||||
;;; TRIANGL -- Board game benchmark.
|
|
||||||
|
|
||||||
(define *board*
|
|
||||||
(list->vector '(1 1 1 1 1 0 1 1 1 1 1 1 1 1 1 1)))
|
|
||||||
|
|
||||||
(define *sequence*
|
|
||||||
(list->vector '(0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
|
|
||||||
|
|
||||||
(define *a*
|
|
||||||
(list->vector '(1 2 4 3 5 6 1 3 6 2 5 4 11 12
|
|
||||||
13 7 8 4 4 7 11 8 12 13 6 10
|
|
||||||
15 9 14 13 13 14 15 9 10
|
|
||||||
6 6)))
|
|
||||||
|
|
||||||
(define *b*
|
|
||||||
(list->vector '(2 4 7 5 8 9 3 6 10 5 9 8
|
|
||||||
12 13 14 8 9 5 2 4 7 5 8
|
|
||||||
9 3 6 10 5 9 8 12 13 14
|
|
||||||
8 9 5 5)))
|
|
||||||
|
|
||||||
(define *c*
|
|
||||||
(list->vector '(4 7 11 8 12 13 6 10 15 9 14 13
|
|
||||||
13 14 15 9 10 6 1 2 4 3 5 6 1
|
|
||||||
3 6 2 5 4 11 12 13 7 8 4 4)))
|
|
||||||
|
|
||||||
(define *answer* '())
|
|
||||||
|
|
||||||
(define (attempt i depth)
|
|
||||||
(cond ((= depth 14)
|
|
||||||
(set! *answer*
|
|
||||||
(cons (cdr (vector->list *sequence*)) *answer*))
|
|
||||||
#t)
|
|
||||||
((and (= 1 (vector-ref *board* (vector-ref *a* i)))
|
|
||||||
(= 1 (vector-ref *board* (vector-ref *b* i)))
|
|
||||||
(= 0 (vector-ref *board* (vector-ref *c* i))))
|
|
||||||
(vector-set! *board* (vector-ref *a* i) 0)
|
|
||||||
(vector-set! *board* (vector-ref *b* i) 0)
|
|
||||||
(vector-set! *board* (vector-ref *c* i) 1)
|
|
||||||
(vector-set! *sequence* depth i)
|
|
||||||
(do ((j 0 (+ j 1))
|
|
||||||
(depth (+ depth 1)))
|
|
||||||
((or (= j 36) (attempt j depth)) #f))
|
|
||||||
(vector-set! *board* (vector-ref *a* i) 1)
|
|
||||||
(vector-set! *board* (vector-ref *b* i) 1)
|
|
||||||
(vector-set! *board* (vector-ref *c* i) 0) #f)
|
|
||||||
(else #f)))
|
|
||||||
|
|
||||||
(define (test i depth)
|
|
||||||
(set! *answer* '())
|
|
||||||
(attempt i depth)
|
|
||||||
(car *answer*))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"triangl"
|
|
||||||
triangl-iters
|
|
||||||
(lambda (result) (equal? result '(22 34 31 15 7 1 20 17 25 6 5 13 32)))
|
|
||||||
(lambda (i depth) (lambda () (test i depth)))
|
|
||||||
22
|
|
||||||
1))
|
|
|
@ -1,43 +0,0 @@
|
||||||
;;; WC -- One of the Kernighan and Van Wyk benchmarks.
|
|
||||||
|
|
||||||
(define inport #f)
|
|
||||||
|
|
||||||
(define nl #f)
|
|
||||||
(define nw #f)
|
|
||||||
(define nc #f)
|
|
||||||
(define inword #f)
|
|
||||||
|
|
||||||
(define (wcport port)
|
|
||||||
(let ((x (read-char port)))
|
|
||||||
(if (eof-object? x)
|
|
||||||
(begin
|
|
||||||
(list nl nw nc))
|
|
||||||
(begin
|
|
||||||
(set! nc (+ nc 1))
|
|
||||||
(if (char=? x #\newline)
|
|
||||||
(set! nl (+ nl 1)))
|
|
||||||
(if (or (char=? x #\space)
|
|
||||||
(char=? x #\newline))
|
|
||||||
(set! inword #f)
|
|
||||||
(if (not inword)
|
|
||||||
(begin
|
|
||||||
(set! nw (+ nw 1))
|
|
||||||
(set! inword #t))))
|
|
||||||
(wcport port)))))
|
|
||||||
|
|
||||||
(define (go)
|
|
||||||
(set! inport (open-input-file "../../src/bib"))
|
|
||||||
(set! nl 0)
|
|
||||||
(set! nw 0)
|
|
||||||
(set! nc 0)
|
|
||||||
(set! inword #f)
|
|
||||||
(let ((result (wcport inport)))
|
|
||||||
(close-input-port inport)
|
|
||||||
result))
|
|
||||||
|
|
||||||
(define (main . args)
|
|
||||||
(run-benchmark
|
|
||||||
"wc"
|
|
||||||
wc-iters
|
|
||||||
(lambda (result) (equal? result '(31102 851820 4460056)))
|
|
||||||
(lambda () (lambda () (go)))))
|
|
|
@ -0,0 +1,148 @@
|
||||||
|
;;; TRAV1 -- Benchmark which creates and traverses a tree structure.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks trav1)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs mutable-pairs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (make-node)
|
||||||
|
(vector 'node '() '() (snb) #f #f #f #f #f #f #f))
|
||||||
|
|
||||||
|
(define (node-parents node) (vector-ref node 1))
|
||||||
|
(define (node-sons node) (vector-ref node 2))
|
||||||
|
(define (node-sn node) (vector-ref node 3))
|
||||||
|
(define (node-entry1 node) (vector-ref node 4))
|
||||||
|
(define (node-entry2 node) (vector-ref node 5))
|
||||||
|
(define (node-entry3 node) (vector-ref node 6))
|
||||||
|
(define (node-entry4 node) (vector-ref node 7))
|
||||||
|
(define (node-entry5 node) (vector-ref node 8))
|
||||||
|
(define (node-entry6 node) (vector-ref node 9))
|
||||||
|
(define (node-mark node) (vector-ref node 10))
|
||||||
|
|
||||||
|
(define (node-parents-set! node v) (vector-set! node 1 v))
|
||||||
|
(define (node-sons-set! node v) (vector-set! node 2 v))
|
||||||
|
(define (node-sn-set! node v) (vector-set! node 3 v))
|
||||||
|
(define (node-entry1-set! node v) (vector-set! node 4 v))
|
||||||
|
(define (node-entry2-set! node v) (vector-set! node 5 v))
|
||||||
|
(define (node-entry3-set! node v) (vector-set! node 6 v))
|
||||||
|
(define (node-entry4-set! node v) (vector-set! node 7 v))
|
||||||
|
(define (node-entry5-set! node v) (vector-set! node 8 v))
|
||||||
|
(define (node-entry6-set! node v) (vector-set! node 9 v))
|
||||||
|
(define (node-mark-set! node v) (vector-set! node 10 v))
|
||||||
|
|
||||||
|
(define *sn* 0)
|
||||||
|
(define *rand* 21)
|
||||||
|
(define *count* 0)
|
||||||
|
(define *marker* #f)
|
||||||
|
(define *root* '())
|
||||||
|
|
||||||
|
(define (snb)
|
||||||
|
(set! *sn* (+ 1 *sn*))
|
||||||
|
*sn*)
|
||||||
|
|
||||||
|
(define (seed)
|
||||||
|
(set! *rand* 21)
|
||||||
|
*rand*)
|
||||||
|
|
||||||
|
(define (traverse-random)
|
||||||
|
(set! *rand* (remainder (* *rand* 17) 251))
|
||||||
|
*rand*)
|
||||||
|
|
||||||
|
(define (traverse-remove n q)
|
||||||
|
(cond ((eq? (cdr (car q)) (car q))
|
||||||
|
(let ((x (caar q))) (set-car! q '()) x))
|
||||||
|
((= n 0)
|
||||||
|
(let ((x (caar q)))
|
||||||
|
(do ((p (car q) (cdr p)))
|
||||||
|
((eq? (cdr p) (car q))
|
||||||
|
(set-cdr! p (cdr (car q)))
|
||||||
|
(set-car! q p)))
|
||||||
|
x))
|
||||||
|
(else (do ((n n (- n 1))
|
||||||
|
(q (car q) (cdr q))
|
||||||
|
(p (cdr (car q)) (cdr p)))
|
||||||
|
((= n 0) (let ((x (car q))) (set-cdr! q p) x))))))
|
||||||
|
|
||||||
|
(define (traverse-select n q)
|
||||||
|
(do ((n n (- n 1))
|
||||||
|
(q (car q) (cdr q)))
|
||||||
|
((= n 0) (car q))))
|
||||||
|
|
||||||
|
(define (add a q)
|
||||||
|
(cond ((null? q)
|
||||||
|
`(,(let ((x `(,a)))
|
||||||
|
(set-cdr! x x) x)))
|
||||||
|
((null? (car q))
|
||||||
|
(let ((x `(,a)))
|
||||||
|
(set-cdr! x x)
|
||||||
|
(set-car! q x)
|
||||||
|
q))
|
||||||
|
; the CL version had a useless set-car! in the next line (wc)
|
||||||
|
(else (set-cdr! (car q) `(,a ,@(cdr (car q))))
|
||||||
|
q)))
|
||||||
|
|
||||||
|
(define (create-structure n)
|
||||||
|
(let ((a `(,(make-node))))
|
||||||
|
(do ((m (- n 1) (- m 1))
|
||||||
|
(p a))
|
||||||
|
((= m 0)
|
||||||
|
(set! a `(,(begin (set-cdr! p a) p)))
|
||||||
|
(do ((unused a)
|
||||||
|
(used (add (traverse-remove 0 a) '()))
|
||||||
|
(x '())
|
||||||
|
(y '()))
|
||||||
|
((null? (car unused))
|
||||||
|
(find-root (traverse-select 0 used) n))
|
||||||
|
(set! x (traverse-remove (remainder (traverse-random) n) unused))
|
||||||
|
(set! y (traverse-select (remainder (traverse-random) n) used))
|
||||||
|
(add x used)
|
||||||
|
(node-sons-set! y `(,x ,@(node-sons y)))
|
||||||
|
(node-parents-set! x `(,y ,@(node-parents x))) ))
|
||||||
|
(set! a (cons (make-node) a)))))
|
||||||
|
|
||||||
|
(define (find-root node n)
|
||||||
|
(do ((n n (- n 1)))
|
||||||
|
((or (= n 0) (null? (node-parents node)))
|
||||||
|
node)
|
||||||
|
(set! node (car (node-parents node)))))
|
||||||
|
|
||||||
|
(define (travers node mark)
|
||||||
|
(cond ((eq? (node-mark node) mark) #f)
|
||||||
|
(else (node-mark-set! node mark)
|
||||||
|
(set! *count* (+ 1 *count*))
|
||||||
|
(node-entry1-set! node (not (node-entry1 node)))
|
||||||
|
(node-entry2-set! node (not (node-entry2 node)))
|
||||||
|
(node-entry3-set! node (not (node-entry3 node)))
|
||||||
|
(node-entry4-set! node (not (node-entry4 node)))
|
||||||
|
(node-entry5-set! node (not (node-entry5 node)))
|
||||||
|
(node-entry6-set! node (not (node-entry6 node)))
|
||||||
|
(do ((sons (node-sons node) (cdr sons)))
|
||||||
|
((null? sons) #f)
|
||||||
|
(travers (car sons) mark)))))
|
||||||
|
|
||||||
|
(define (traverse root)
|
||||||
|
(let ((*count* 0))
|
||||||
|
(travers root (begin (set! *marker* (not *marker*)) *marker*))
|
||||||
|
*count*))
|
||||||
|
|
||||||
|
(define (init-traverse) ; Changed from defmacro to defun \bs
|
||||||
|
(set! *root* (create-structure 100))
|
||||||
|
#f)
|
||||||
|
|
||||||
|
(define (run-traverse) ; Changed from defmacro to defun \bs
|
||||||
|
(do ((i 50 (- i 1)))
|
||||||
|
((= i 0))
|
||||||
|
(traverse *root*)
|
||||||
|
(traverse *root*)
|
||||||
|
(traverse *root*)
|
||||||
|
(traverse *root*)
|
||||||
|
(traverse *root*)))
|
||||||
|
|
||||||
|
;;; to initialize, call: (init-traverse)
|
||||||
|
;;; to run traverse, call: (run-traverse)
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"trav1"
|
||||||
|
trav1-iters
|
||||||
|
(lambda (result) #t)
|
||||||
|
(lambda () (lambda () (init-traverse))))))
|
|
@ -0,0 +1,150 @@
|
||||||
|
;;; TRAV2 -- Benchmark which creates and traverses a tree structure.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks trav2)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs mutable-pairs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define (make-node)
|
||||||
|
(vector 'node '() '() (snb) #f #f #f #f #f #f #f))
|
||||||
|
|
||||||
|
(define (node-parents node) (vector-ref node 1))
|
||||||
|
(define (node-sons node) (vector-ref node 2))
|
||||||
|
(define (node-sn node) (vector-ref node 3))
|
||||||
|
(define (node-entry1 node) (vector-ref node 4))
|
||||||
|
(define (node-entry2 node) (vector-ref node 5))
|
||||||
|
(define (node-entry3 node) (vector-ref node 6))
|
||||||
|
(define (node-entry4 node) (vector-ref node 7))
|
||||||
|
(define (node-entry5 node) (vector-ref node 8))
|
||||||
|
(define (node-entry6 node) (vector-ref node 9))
|
||||||
|
(define (node-mark node) (vector-ref node 10))
|
||||||
|
|
||||||
|
(define (node-parents-set! node v) (vector-set! node 1 v))
|
||||||
|
(define (node-sons-set! node v) (vector-set! node 2 v))
|
||||||
|
(define (node-sn-set! node v) (vector-set! node 3 v))
|
||||||
|
(define (node-entry1-set! node v) (vector-set! node 4 v))
|
||||||
|
(define (node-entry2-set! node v) (vector-set! node 5 v))
|
||||||
|
(define (node-entry3-set! node v) (vector-set! node 6 v))
|
||||||
|
(define (node-entry4-set! node v) (vector-set! node 7 v))
|
||||||
|
(define (node-entry5-set! node v) (vector-set! node 8 v))
|
||||||
|
(define (node-entry6-set! node v) (vector-set! node 9 v))
|
||||||
|
(define (node-mark-set! node v) (vector-set! node 10 v))
|
||||||
|
|
||||||
|
(define *sn* 0)
|
||||||
|
(define *rand* 21)
|
||||||
|
(define *count* 0)
|
||||||
|
(define *marker* #f)
|
||||||
|
(define *root* '())
|
||||||
|
|
||||||
|
(define (snb)
|
||||||
|
(set! *sn* (+ 1 *sn*))
|
||||||
|
*sn*)
|
||||||
|
|
||||||
|
(define (seed)
|
||||||
|
(set! *rand* 21)
|
||||||
|
*rand*)
|
||||||
|
|
||||||
|
(define (traverse-random)
|
||||||
|
(set! *rand* (remainder (* *rand* 17) 251))
|
||||||
|
*rand*)
|
||||||
|
|
||||||
|
(define (traverse-remove n q)
|
||||||
|
(cond ((eq? (cdr (car q)) (car q))
|
||||||
|
(let ((x (caar q))) (set-car! q '()) x))
|
||||||
|
((= n 0)
|
||||||
|
(let ((x (caar q)))
|
||||||
|
(do ((p (car q) (cdr p)))
|
||||||
|
((eq? (cdr p) (car q))
|
||||||
|
(set-cdr! p (cdr (car q)))
|
||||||
|
(set-car! q p)))
|
||||||
|
x))
|
||||||
|
(else (do ((n n (- n 1))
|
||||||
|
(q (car q) (cdr q))
|
||||||
|
(p (cdr (car q)) (cdr p)))
|
||||||
|
((= n 0) (let ((x (car q))) (set-cdr! q p) x))))))
|
||||||
|
|
||||||
|
(define (traverse-select n q)
|
||||||
|
(do ((n n (- n 1))
|
||||||
|
(q (car q) (cdr q)))
|
||||||
|
((= n 0) (car q))))
|
||||||
|
|
||||||
|
(define (add a q)
|
||||||
|
(cond ((null? q)
|
||||||
|
`(,(let ((x `(,a)))
|
||||||
|
(set-cdr! x x) x)))
|
||||||
|
((null? (car q))
|
||||||
|
(let ((x `(,a)))
|
||||||
|
(set-cdr! x x)
|
||||||
|
(set-car! q x)
|
||||||
|
q))
|
||||||
|
; the CL version had a useless set-car! in the next line (wc)
|
||||||
|
(else (set-cdr! (car q) `(,a ,@(cdr (car q))))
|
||||||
|
q)))
|
||||||
|
|
||||||
|
(define (create-structure n)
|
||||||
|
(let ((a `(,(make-node))))
|
||||||
|
(do ((m (- n 1) (- m 1))
|
||||||
|
(p a))
|
||||||
|
((= m 0)
|
||||||
|
(set! a `(,(begin (set-cdr! p a) p)))
|
||||||
|
(do ((unused a)
|
||||||
|
(used (add (traverse-remove 0 a) '()))
|
||||||
|
(x '())
|
||||||
|
(y '()))
|
||||||
|
((null? (car unused))
|
||||||
|
(find-root (traverse-select 0 used) n))
|
||||||
|
(set! x (traverse-remove (remainder (traverse-random) n) unused))
|
||||||
|
(set! y (traverse-select (remainder (traverse-random) n) used))
|
||||||
|
(add x used)
|
||||||
|
(node-sons-set! y `(,x ,@(node-sons y)))
|
||||||
|
(node-parents-set! x `(,y ,@(node-parents x))) ))
|
||||||
|
(set! a (cons (make-node) a)))))
|
||||||
|
|
||||||
|
(define (find-root node n)
|
||||||
|
(do ((n n (- n 1)))
|
||||||
|
((or (= n 0) (null? (node-parents node)))
|
||||||
|
node)
|
||||||
|
(set! node (car (node-parents node)))))
|
||||||
|
|
||||||
|
(define (travers node mark)
|
||||||
|
(cond ((eq? (node-mark node) mark) #f)
|
||||||
|
(else (node-mark-set! node mark)
|
||||||
|
(set! *count* (+ 1 *count*))
|
||||||
|
(node-entry1-set! node (not (node-entry1 node)))
|
||||||
|
(node-entry2-set! node (not (node-entry2 node)))
|
||||||
|
(node-entry3-set! node (not (node-entry3 node)))
|
||||||
|
(node-entry4-set! node (not (node-entry4 node)))
|
||||||
|
(node-entry5-set! node (not (node-entry5 node)))
|
||||||
|
(node-entry6-set! node (not (node-entry6 node)))
|
||||||
|
(do ((sons (node-sons node) (cdr sons)))
|
||||||
|
((null? sons) #f)
|
||||||
|
(travers (car sons) mark)))))
|
||||||
|
|
||||||
|
(define (traverse root)
|
||||||
|
(let ((*count* 0))
|
||||||
|
(travers root (begin (set! *marker* (not *marker*)) *marker*))
|
||||||
|
*count*))
|
||||||
|
|
||||||
|
(define (init-traverse) ; Changed from defmacro to defun \bs
|
||||||
|
(set! *root* (create-structure 100))
|
||||||
|
#f)
|
||||||
|
|
||||||
|
(define (run-traverse) ; Changed from defmacro to defun \bs
|
||||||
|
(do ((i 50 (- i 1)))
|
||||||
|
((= i 0))
|
||||||
|
(traverse *root*)
|
||||||
|
(traverse *root*)
|
||||||
|
(traverse *root*)
|
||||||
|
(traverse *root*)
|
||||||
|
(traverse *root*)))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"trav2"
|
||||||
|
trav2-iters
|
||||||
|
(lambda (result) #t)
|
||||||
|
(lambda () (lambda () (run-traverse)))))
|
||||||
|
|
||||||
|
;;; to initialize, call: (init-traverse)
|
||||||
|
;;; to run traverse, call: (run-traverse)
|
||||||
|
|
||||||
|
(init-traverse))
|
|
@ -0,0 +1,64 @@
|
||||||
|
;;; TRIANGL -- Board game benchmark.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks triangl)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define *board*
|
||||||
|
(list->vector '(1 1 1 1 1 0 1 1 1 1 1 1 1 1 1 1)))
|
||||||
|
|
||||||
|
(define *sequence*
|
||||||
|
(list->vector '(0 0 0 0 0 0 0 0 0 0 0 0 0 0)))
|
||||||
|
|
||||||
|
(define *a*
|
||||||
|
(list->vector '(1 2 4 3 5 6 1 3 6 2 5 4 11 12
|
||||||
|
13 7 8 4 4 7 11 8 12 13 6 10
|
||||||
|
15 9 14 13 13 14 15 9 10
|
||||||
|
6 6)))
|
||||||
|
|
||||||
|
(define *b*
|
||||||
|
(list->vector '(2 4 7 5 8 9 3 6 10 5 9 8
|
||||||
|
12 13 14 8 9 5 2 4 7 5 8
|
||||||
|
9 3 6 10 5 9 8 12 13 14
|
||||||
|
8 9 5 5)))
|
||||||
|
|
||||||
|
(define *c*
|
||||||
|
(list->vector '(4 7 11 8 12 13 6 10 15 9 14 13
|
||||||
|
13 14 15 9 10 6 1 2 4 3 5 6 1
|
||||||
|
3 6 2 5 4 11 12 13 7 8 4 4)))
|
||||||
|
|
||||||
|
(define *answer* '())
|
||||||
|
|
||||||
|
(define (attempt i depth)
|
||||||
|
(cond ((= depth 14)
|
||||||
|
(set! *answer*
|
||||||
|
(cons (cdr (vector->list *sequence*)) *answer*))
|
||||||
|
#t)
|
||||||
|
((and (= 1 (vector-ref *board* (vector-ref *a* i)))
|
||||||
|
(= 1 (vector-ref *board* (vector-ref *b* i)))
|
||||||
|
(= 0 (vector-ref *board* (vector-ref *c* i))))
|
||||||
|
(vector-set! *board* (vector-ref *a* i) 0)
|
||||||
|
(vector-set! *board* (vector-ref *b* i) 0)
|
||||||
|
(vector-set! *board* (vector-ref *c* i) 1)
|
||||||
|
(vector-set! *sequence* depth i)
|
||||||
|
(do ((j 0 (+ j 1))
|
||||||
|
(depth (+ depth 1)))
|
||||||
|
((or (= j 36) (attempt j depth)) #f))
|
||||||
|
(vector-set! *board* (vector-ref *a* i) 1)
|
||||||
|
(vector-set! *board* (vector-ref *b* i) 1)
|
||||||
|
(vector-set! *board* (vector-ref *c* i) 0) #f)
|
||||||
|
(else #f)))
|
||||||
|
|
||||||
|
(define (test i depth)
|
||||||
|
(set! *answer* '())
|
||||||
|
(attempt i depth)
|
||||||
|
(car *answer*))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"triangl"
|
||||||
|
triangl-iters
|
||||||
|
(lambda (result) (equal? result '(22 34 31 15 7 1 20 17 25 6 5 13 32)))
|
||||||
|
(lambda (i depth) (lambda () (test i depth)))
|
||||||
|
22
|
||||||
|
1)))
|
|
@ -0,0 +1,47 @@
|
||||||
|
;;; WC -- One of the Kernighan and Van Wyk benchmarks.
|
||||||
|
|
||||||
|
(library (r6rs-benchmarks wc)
|
||||||
|
(export main)
|
||||||
|
(import (r6rs) (r6rs-benchmarks))
|
||||||
|
|
||||||
|
(define inport #f)
|
||||||
|
|
||||||
|
(define nl #f)
|
||||||
|
(define nw #f)
|
||||||
|
(define nc #f)
|
||||||
|
(define inword #f)
|
||||||
|
|
||||||
|
(define (wcport port)
|
||||||
|
(let ((x (read-char port)))
|
||||||
|
(if (eof-object? x)
|
||||||
|
(begin
|
||||||
|
(list nl nw nc))
|
||||||
|
(begin
|
||||||
|
(set! nc (+ nc 1))
|
||||||
|
(if (char=? x #\newline)
|
||||||
|
(set! nl (+ nl 1)))
|
||||||
|
(if (or (char=? x #\space)
|
||||||
|
(char=? x #\newline))
|
||||||
|
(set! inword #f)
|
||||||
|
(if (not inword)
|
||||||
|
(begin
|
||||||
|
(set! nw (+ nw 1))
|
||||||
|
(set! inword #t))))
|
||||||
|
(wcport port)))))
|
||||||
|
|
||||||
|
(define (go)
|
||||||
|
(set! inport (open-input-file "r6rs-benchmarks/bib"))
|
||||||
|
(set! nl 0)
|
||||||
|
(set! nw 0)
|
||||||
|
(set! nc 0)
|
||||||
|
(set! inword #f)
|
||||||
|
(let ((result (wcport inport)))
|
||||||
|
(close-input-port inport)
|
||||||
|
result))
|
||||||
|
|
||||||
|
(define (main . args)
|
||||||
|
(run-benchmark
|
||||||
|
"wc"
|
||||||
|
wc-iters
|
||||||
|
(lambda (result) (equal? result '(31102 851820 4460056)))
|
||||||
|
(lambda () (lambda () (go))))))
|
|
@ -66,4 +66,5 @@
|
||||||
(define gcold-iters 10000)
|
(define gcold-iters 10000)
|
||||||
;(define nbody-iters 1) ; nondeterministic (order of evaluation)
|
;(define nbody-iters 1) ; nondeterministic (order of evaluation)
|
||||||
|
|
||||||
|
(define fpsum-iters 10)
|
||||||
|
|
||||||
|
|
|
@ -6009,3 +6009,316 @@ Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified
|
||||||
|
|
||||||
|
|
||||||
>
|
>
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 16:38:27 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing primes under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 92273280
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 7489 ms (User: 7401 ms; System: 48 ms)
|
||||||
|
Elapsed GC time: 130 ms (CPU: 131 in 352 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 16:41:06 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing puzzle under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 8126378
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 1975 ms (User: 1813 ms; System: 149 ms)
|
||||||
|
Elapsed GC time: 9 ms (CPU: 13 in 31 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 16:53:49 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing fpsum under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
> bench DIED!
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 16:55:25 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing fpsum under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
bench DIED!
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 16:55:48 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing fpsum under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 79953918
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 370 ms (User: 362 ms; System: 3 ms)
|
||||||
|
Elapsed GC time: 112 ms (CPU: 110 in 305 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 16:58:22 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing sboyer under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 16514966
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 1328 ms (User: 1313 ms; System: 10 ms)
|
||||||
|
Elapsed GC time: 41 ms (CPU: 40 in 63 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:07:50 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing sum under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 0
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 608 ms (User: 604 ms; System: 1 ms)
|
||||||
|
Elapsed GC time: 0 ms (CPU: 0 in 0 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:08:14 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing sum under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 0
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 611 ms (User: 604 ms; System: 2 ms)
|
||||||
|
Elapsed GC time: 0 ms (CPU: 0 in 0 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:11:01 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing sum1 under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 6553338
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 3540 ms (User: 2078 ms; System: 1418 ms)
|
||||||
|
Elapsed GC time: 10 ms (CPU: 7 in 25 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:12:55 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing string under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 7834818
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 430 ms (User: 400 ms; System: 22 ms)
|
||||||
|
Elapsed GC time: 45 ms (CPU: 39 in 30 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:19:06 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing sumloop under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 0
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 862 ms (User: 854 ms; System: 3 ms)
|
||||||
|
Elapsed GC time: 0 ms (CPU: 0 in 0 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:22:10 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing tail under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 19136474
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 717 ms (User: 578 ms; System: 133 ms)
|
||||||
|
Elapsed GC time: 50 ms (CPU: 42 in 73 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:23:32 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing tail under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 19136474
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 711 ms (User: 577 ms; System: 131 ms)
|
||||||
|
Elapsed GC time: 46 ms (CPU: 48 in 73 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:26:01 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing tak under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 0
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 1260 ms (User: 1236 ms; System: 6 ms)
|
||||||
|
Elapsed GC time: 0 ms (CPU: 0 in 0 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:31:32 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing trav1 under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 12320448
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 1362 ms (User: 1312 ms; System: 40 ms)
|
||||||
|
Elapsed GC time: 195 ms (CPU: 200 in 47 collections.)
|
||||||
|
|
||||||
|
****************************
|
||||||
|
Benchmarking Larceny-r6rs on Wed Jun 13 17:31:45 AST 2007 under Darwin Vesuvius.local 8.9.1 Darwin Kernel Version 8.9.1: Thu Feb 22 20:55:00 PST 2007; root:xnu-792.18.15~1/RELEASE_I386 i386 i386
|
||||||
|
|
||||||
|
Testing trav2 under Larceny-r6rs
|
||||||
|
Compiling...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
>
|
||||||
|
Running...
|
||||||
|
Larceny v0.93 "Deviated Prevert" (Nov 10 2006 04:27:45, precise:BSD Unix:unified)
|
||||||
|
|
||||||
|
|
||||||
|
>
|
||||||
|
Words allocated: 0
|
||||||
|
Words reclaimed: 0
|
||||||
|
Elapsed time...: 1264 ms (User: 1253 ms; System: 4 ms)
|
||||||
|
Elapsed GC time: 0 ms (CPU: 0 in 0 collections.)
|
||||||
|
|
|
@ -10,5 +10,5 @@
|
||||||
(run-benchmark
|
(run-benchmark
|
||||||
"fpsum"
|
"fpsum"
|
||||||
fpsum-iters
|
fpsum-iters
|
||||||
(lambda () (run))
|
(lambda (result) (equal? result 500000500000.))
|
||||||
(lambda (result) (equal? result 500000500000.))))
|
(lambda () run)))
|
||||||
|
|
Loading…
Reference in New Issue