nboyer.sch 28 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771
  1. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  2. ; File: nboyer.sch
  3. ; Description: The Boyer benchmark
  4. ; Author: Bob Boyer
  5. ; Created: 5-Apr-85
  6. ; Modified: 10-Apr-85 14:52:20 (Bob Shaw)
  7. ; 22-Jul-87 (Will Clinger)
  8. ; 2-Jul-88 (Will Clinger -- distinguished #f and the empty list)
  9. ; 13-Feb-97 (Will Clinger -- fixed bugs in unifier and rules,
  10. ; rewrote to eliminate property lists, and added
  11. ; a scaling parameter suggested by Bob Boyer)
  12. ; 19-Mar-99 (Will Clinger -- cleaned up comments)
  13. ; 4-Apr-01 (Will Clinger -- changed four 1- symbols to sub1)
  14. ; Language: Scheme
  15. ; Status: Public Domain
  16. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  17. ;;; NBOYER -- Logic programming benchmark, originally written by Bob Boyer.
  18. ;;; Fairly CONS intensive.
  19. ; Note: The version of this benchmark that appears in Dick Gabriel's book
  20. ; contained several bugs that are corrected here. These bugs are discussed
  21. ; by Henry Baker, "The Boyer Benchmark Meets Linear Logic", ACM SIGPLAN Lisp
  22. ; Pointers 6(4), October-December 1993, pages 3-10. The fixed bugs are:
  23. ;
  24. ; The benchmark now returns a boolean result.
  25. ; FALSEP and TRUEP use TERM-MEMBER? rather than MEMV (which is called MEMBER
  26. ; in Common Lisp)
  27. ; ONE-WAY-UNIFY1 now treats numbers correctly
  28. ; ONE-WAY-UNIFY1-LST now treats empty lists correctly
  29. ; Rule 19 has been corrected (this rule was not touched by the original
  30. ; benchmark, but is used by this version)
  31. ; Rules 84 and 101 have been corrected (but these rules are never touched
  32. ; by the benchmark)
  33. ;
  34. ; According to Baker, these bug fixes make the benchmark 10-25% slower.
  35. ; Please do not compare the timings from this benchmark against those of
  36. ; the original benchmark.
  37. ;
  38. ; This version of the benchmark also prints the number of rewrites as a sanity
  39. ; check, because it is too easy for a buggy version to return the correct
  40. ; boolean result. The correct number of rewrites is
  41. ;
  42. ; n rewrites peak live storage (approximate, in bytes)
  43. ; 0 95024 520,000
  44. ; 1 591777 2,085,000
  45. ; 2 1813975 5,175,000
  46. ; 3 5375678
  47. ; 4 16445406
  48. ; 5 51507739
  49. ; Nboyer is a 2-phase benchmark.
  50. ; The first phase attaches lemmas to symbols. This phase is not timed,
  51. ; but it accounts for very little of the runtime anyway.
  52. ; The second phase creates the test problem, and tests to see
  53. ; whether it is implied by the lemmas.
  54. (define (nboyer-benchmark . args)
  55. (let ((n (if (null? args) 0 (car args))))
  56. (setup-boyer)
  57. (run-benchmark (string-append "nboyer"
  58. (number->string n))
  59. 1
  60. (lambda () (test-boyer n))
  61. (lambda (rewrites)
  62. (and (number? rewrites)
  63. (case n
  64. ((0) (= rewrites 95024))
  65. ((1) (= rewrites 591777))
  66. ((2) (= rewrites 1813975))
  67. ((3) (= rewrites 5375678))
  68. ((4) (= rewrites 16445406))
  69. ((5) (= rewrites 51507739))
  70. ; If it works for n <= 5, assume it works.
  71. (else #t)))))))
  72. (define (setup-boyer) #t) ; assigned below
  73. (define (test-boyer) #t) ; assigned below
  74. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  75. ;
  76. ; The first phase.
  77. ;
  78. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  79. ; In the original benchmark, it stored a list of lemmas on the
  80. ; property lists of symbols.
  81. ; In the new benchmark, it maintains an association list of
  82. ; symbols and symbol-records, and stores the list of lemmas
  83. ; within the symbol-records.
  84. (let ()
  85. (define (setup)
  86. (add-lemma-lst
  87. (quote ((equal (compile form)
  88. (reverse (codegen (optimize form)
  89. (nil))))
  90. (equal (eqp x y)
  91. (equal (fix x)
  92. (fix y)))
  93. (equal (greaterp x y)
  94. (lessp y x))
  95. (equal (lesseqp x y)
  96. (not (lessp y x)))
  97. (equal (greatereqp x y)
  98. (not (lessp x y)))
  99. (equal (boolean x)
  100. (or (equal x (t))
  101. (equal x (f))))
  102. (equal (iff x y)
  103. (and (implies x y)
  104. (implies y x)))
  105. (equal (even1 x)
  106. (if (zerop x)
  107. (t)
  108. (odd (sub1 x))))
  109. (equal (countps- l pred)
  110. (countps-loop l pred (zero)))
  111. (equal (fact- i)
  112. (fact-loop i 1))
  113. (equal (reverse- x)
  114. (reverse-loop x (nil)))
  115. (equal (divides x y)
  116. (zerop (remainder y x)))
  117. (equal (assume-true var alist)
  118. (cons (cons var (t))
  119. alist))
  120. (equal (assume-false var alist)
  121. (cons (cons var (f))
  122. alist))
  123. (equal (tautology-checker x)
  124. (tautologyp (normalize x)
  125. (nil)))
  126. (equal (falsify x)
  127. (falsify1 (normalize x)
  128. (nil)))
  129. (equal (prime x)
  130. (and (not (zerop x))
  131. (not (equal x (add1 (zero))))
  132. (prime1 x (sub1 x))))
  133. (equal (and p q)
  134. (if p (if q (t)
  135. (f))
  136. (f)))
  137. (equal (or p q)
  138. (if p (t)
  139. (if q (t)
  140. (f))))
  141. (equal (not p)
  142. (if p (f)
  143. (t)))
  144. (equal (implies p q)
  145. (if p (if q (t)
  146. (f))
  147. (t)))
  148. (equal (fix x)
  149. (if (numberp x)
  150. x
  151. (zero)))
  152. (equal (if (if a b c)
  153. d e)
  154. (if a (if b d e)
  155. (if c d e)))
  156. (equal (zerop x)
  157. (or (equal x (zero))
  158. (not (numberp x))))
  159. (equal (plus (plus x y)
  160. z)
  161. (plus x (plus y z)))
  162. (equal (equal (plus a b)
  163. (zero))
  164. (and (zerop a)
  165. (zerop b)))
  166. (equal (difference x x)
  167. (zero))
  168. (equal (equal (plus a b)
  169. (plus a c))
  170. (equal (fix b)
  171. (fix c)))
  172. (equal (equal (zero)
  173. (difference x y))
  174. (not (lessp y x)))
  175. (equal (equal x (difference x y))
  176. (and (numberp x)
  177. (or (equal x (zero))
  178. (zerop y))))
  179. (equal (meaning (plus-tree (append x y))
  180. a)
  181. (plus (meaning (plus-tree x)
  182. a)
  183. (meaning (plus-tree y)
  184. a)))
  185. (equal (meaning (plus-tree (plus-fringe x))
  186. a)
  187. (fix (meaning x a)))
  188. (equal (append (append x y)
  189. z)
  190. (append x (append y z)))
  191. (equal (reverse (append a b))
  192. (append (reverse b)
  193. (reverse a)))
  194. (equal (times x (plus y z))
  195. (plus (times x y)
  196. (times x z)))
  197. (equal (times (times x y)
  198. z)
  199. (times x (times y z)))
  200. (equal (equal (times x y)
  201. (zero))
  202. (or (zerop x)
  203. (zerop y)))
  204. (equal (exec (append x y)
  205. pds envrn)
  206. (exec y (exec x pds envrn)
  207. envrn))
  208. (equal (mc-flatten x y)
  209. (append (flatten x)
  210. y))
  211. (equal (member x (append a b))
  212. (or (member x a)
  213. (member x b)))
  214. (equal (member x (reverse y))
  215. (member x y))
  216. (equal (length (reverse x))
  217. (length x))
  218. (equal (member a (intersect b c))
  219. (and (member a b)
  220. (member a c)))
  221. (equal (nth (zero)
  222. i)
  223. (zero))
  224. (equal (exp i (plus j k))
  225. (times (exp i j)
  226. (exp i k)))
  227. (equal (exp i (times j k))
  228. (exp (exp i j)
  229. k))
  230. (equal (reverse-loop x y)
  231. (append (reverse x)
  232. y))
  233. (equal (reverse-loop x (nil))
  234. (reverse x))
  235. (equal (count-list z (sort-lp x y))
  236. (plus (count-list z x)
  237. (count-list z y)))
  238. (equal (equal (append a b)
  239. (append a c))
  240. (equal b c))
  241. (equal (plus (remainder x y)
  242. (times y (quotient x y)))
  243. (fix x))
  244. (equal (power-eval (big-plus1 l i base)
  245. base)
  246. (plus (power-eval l base)
  247. i))
  248. (equal (power-eval (big-plus x y i base)
  249. base)
  250. (plus i (plus (power-eval x base)
  251. (power-eval y base))))
  252. (equal (remainder y 1)
  253. (zero))
  254. (equal (lessp (remainder x y)
  255. y)
  256. (not (zerop y)))
  257. (equal (remainder x x)
  258. (zero))
  259. (equal (lessp (quotient i j)
  260. i)
  261. (and (not (zerop i))
  262. (or (zerop j)
  263. (not (equal j 1)))))
  264. (equal (lessp (remainder x y)
  265. x)
  266. (and (not (zerop y))
  267. (not (zerop x))
  268. (not (lessp x y))))
  269. (equal (power-eval (power-rep i base)
  270. base)
  271. (fix i))
  272. (equal (power-eval (big-plus (power-rep i base)
  273. (power-rep j base)
  274. (zero)
  275. base)
  276. base)
  277. (plus i j))
  278. (equal (gcd x y)
  279. (gcd y x))
  280. (equal (nth (append a b)
  281. i)
  282. (append (nth a i)
  283. (nth b (difference i (length a)))))
  284. (equal (difference (plus x y)
  285. x)
  286. (fix y))
  287. (equal (difference (plus y x)
  288. x)
  289. (fix y))
  290. (equal (difference (plus x y)
  291. (plus x z))
  292. (difference y z))
  293. (equal (times x (difference c w))
  294. (difference (times c x)
  295. (times w x)))
  296. (equal (remainder (times x z)
  297. z)
  298. (zero))
  299. (equal (difference (plus b (plus a c))
  300. a)
  301. (plus b c))
  302. (equal (difference (add1 (plus y z))
  303. z)
  304. (add1 y))
  305. (equal (lessp (plus x y)
  306. (plus x z))
  307. (lessp y z))
  308. (equal (lessp (times x z)
  309. (times y z))
  310. (and (not (zerop z))
  311. (lessp x y)))
  312. (equal (lessp y (plus x y))
  313. (not (zerop x)))
  314. (equal (gcd (times x z)
  315. (times y z))
  316. (times z (gcd x y)))
  317. (equal (value (normalize x)
  318. a)
  319. (value x a))
  320. (equal (equal (flatten x)
  321. (cons y (nil)))
  322. (and (nlistp x)
  323. (equal x y)))
  324. (equal (listp (gopher x))
  325. (listp x))
  326. (equal (samefringe x y)
  327. (equal (flatten x)
  328. (flatten y)))
  329. (equal (equal (greatest-factor x y)
  330. (zero))
  331. (and (or (zerop y)
  332. (equal y 1))
  333. (equal x (zero))))
  334. (equal (equal (greatest-factor x y)
  335. 1)
  336. (equal x 1))
  337. (equal (numberp (greatest-factor x y))
  338. (not (and (or (zerop y)
  339. (equal y 1))
  340. (not (numberp x)))))
  341. (equal (times-list (append x y))
  342. (times (times-list x)
  343. (times-list y)))
  344. (equal (prime-list (append x y))
  345. (and (prime-list x)
  346. (prime-list y)))
  347. (equal (equal z (times w z))
  348. (and (numberp z)
  349. (or (equal z (zero))
  350. (equal w 1))))
  351. (equal (greatereqp x y)
  352. (not (lessp x y)))
  353. (equal (equal x (times x y))
  354. (or (equal x (zero))
  355. (and (numberp x)
  356. (equal y 1))))
  357. (equal (remainder (times y x)
  358. y)
  359. (zero))
  360. (equal (equal (times a b)
  361. 1)
  362. (and (not (equal a (zero)))
  363. (not (equal b (zero)))
  364. (numberp a)
  365. (numberp b)
  366. (equal (sub1 a)
  367. (zero))
  368. (equal (sub1 b)
  369. (zero))))
  370. (equal (lessp (length (delete x l))
  371. (length l))
  372. (member x l))
  373. (equal (sort2 (delete x l))
  374. (delete x (sort2 l)))
  375. (equal (dsort x)
  376. (sort2 x))
  377. (equal (length (cons x1
  378. (cons x2
  379. (cons x3 (cons x4
  380. (cons x5
  381. (cons x6 x7)))))))
  382. (plus 6 (length x7)))
  383. (equal (difference (add1 (add1 x))
  384. 2)
  385. (fix x))
  386. (equal (quotient (plus x (plus x y))
  387. 2)
  388. (plus x (quotient y 2)))
  389. (equal (sigma (zero)
  390. i)
  391. (quotient (times i (add1 i))
  392. 2))
  393. (equal (plus x (add1 y))
  394. (if (numberp y)
  395. (add1 (plus x y))
  396. (add1 x)))
  397. (equal (equal (difference x y)
  398. (difference z y))
  399. (if (lessp x y)
  400. (not (lessp y z))
  401. (if (lessp z y)
  402. (not (lessp y x))
  403. (equal (fix x)
  404. (fix z)))))
  405. (equal (meaning (plus-tree (delete x y))
  406. a)
  407. (if (member x y)
  408. (difference (meaning (plus-tree y)
  409. a)
  410. (meaning x a))
  411. (meaning (plus-tree y)
  412. a)))
  413. (equal (times x (add1 y))
  414. (if (numberp y)
  415. (plus x (times x y))
  416. (fix x)))
  417. (equal (nth (nil)
  418. i)
  419. (if (zerop i)
  420. (nil)
  421. (zero)))
  422. (equal (last (append a b))
  423. (if (listp b)
  424. (last b)
  425. (if (listp a)
  426. (cons (car (last a))
  427. b)
  428. b)))
  429. (equal (equal (lessp x y)
  430. z)
  431. (if (lessp x y)
  432. (equal (t) z)
  433. (equal (f) z)))
  434. (equal (assignment x (append a b))
  435. (if (assignedp x a)
  436. (assignment x a)
  437. (assignment x b)))
  438. (equal (car (gopher x))
  439. (if (listp x)
  440. (car (flatten x))
  441. (zero)))
  442. (equal (flatten (cdr (gopher x)))
  443. (if (listp x)
  444. (cdr (flatten x))
  445. (cons (zero)
  446. (nil))))
  447. (equal (quotient (times y x)
  448. y)
  449. (if (zerop y)
  450. (zero)
  451. (fix x)))
  452. (equal (get j (set i val mem))
  453. (if (eqp j i)
  454. val
  455. (get j mem)))))))
  456. (define (add-lemma-lst lst)
  457. (cond ((null? lst)
  458. #t)
  459. (else (add-lemma (car lst))
  460. (add-lemma-lst (cdr lst)))))
  461. (define (add-lemma term)
  462. (cond ((and (pair? term)
  463. (eq? (car term)
  464. (quote equal))
  465. (pair? (cadr term)))
  466. (put (car (cadr term))
  467. (quote lemmas)
  468. (cons
  469. (translate-term term)
  470. (get (car (cadr term)) (quote lemmas)))))
  471. (else (error "ADD-LEMMA did not like term: " term))))
  472. ; Translates a term by replacing its constructor symbols by symbol-records.
  473. (define (translate-term term)
  474. (cond ((not (pair? term))
  475. term)
  476. (else (cons (symbol->symbol-record (car term))
  477. (translate-args (cdr term))))))
  478. (define (translate-args lst)
  479. (cond ((null? lst)
  480. '())
  481. (else (cons (translate-term (car lst))
  482. (translate-args (cdr lst))))))
  483. ; For debugging only, so the use of MAP does not change
  484. ; the first-order character of the benchmark.
  485. (define (untranslate-term term)
  486. (cond ((not (pair? term))
  487. term)
  488. (else (cons (get-name (car term))
  489. (map untranslate-term (cdr term))))))
  490. ; A symbol-record is represented as a vector with two fields:
  491. ; the symbol (for debugging) and
  492. ; the list of lemmas associated with the symbol.
  493. (define (put sym property value)
  494. (put-lemmas! (symbol->symbol-record sym) value))
  495. (define (get sym property)
  496. (get-lemmas (symbol->symbol-record sym)))
  497. (define (symbol->symbol-record sym)
  498. (let ((x (assq sym *symbol-records-alist*)))
  499. (if x
  500. (cdr x)
  501. (let ((r (make-symbol-record sym)))
  502. (set! *symbol-records-alist*
  503. (cons (cons sym r)
  504. *symbol-records-alist*))
  505. r))))
  506. ; Association list of symbols and symbol-records.
  507. (define *symbol-records-alist* '())
  508. ; A symbol-record is represented as a vector with two fields:
  509. ; the symbol (for debugging) and
  510. ; the list of lemmas associated with the symbol.
  511. (define (make-symbol-record sym)
  512. (vector sym '()))
  513. (define (put-lemmas! symbol-record lemmas)
  514. (vector-set! symbol-record 1 lemmas))
  515. (define (get-lemmas symbol-record)
  516. (vector-ref symbol-record 1))
  517. (define (get-name symbol-record)
  518. (vector-ref symbol-record 0))
  519. (define (symbol-record-equal? r1 r2)
  520. (eq? r1 r2))
  521. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  522. ;
  523. ; The second phase.
  524. ;
  525. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  526. (define (test n)
  527. (let ((term
  528. (apply-subst
  529. (translate-alist
  530. (quote ((x f (plus (plus a b)
  531. (plus c (zero))))
  532. (y f (times (times a b)
  533. (plus c d)))
  534. (z f (reverse (append (append a b)
  535. (nil))))
  536. (u equal (plus a b)
  537. (difference x y))
  538. (w lessp (remainder a b)
  539. (member a (length b))))))
  540. (translate-term
  541. (do ((term
  542. (quote (implies (and (implies x y)
  543. (and (implies y z)
  544. (and (implies z u)
  545. (implies u w))))
  546. (implies x w)))
  547. (list 'or term '(f)))
  548. (n n (- n 1)))
  549. ((zero? n) term))))))
  550. (tautp term)))
  551. (define (translate-alist alist)
  552. (cond ((null? alist)
  553. '())
  554. (else (cons (cons (caar alist)
  555. (translate-term (cdar alist)))
  556. (translate-alist (cdr alist))))))
  557. (define (apply-subst alist term)
  558. (cond ((not (pair? term))
  559. (let ((temp-temp (assq term alist)))
  560. (if temp-temp
  561. (cdr temp-temp)
  562. term)))
  563. (else (cons (car term)
  564. (apply-subst-lst alist (cdr term))))))
  565. (define (apply-subst-lst alist lst)
  566. (cond ((null? lst)
  567. '())
  568. (else (cons (apply-subst alist (car lst))
  569. (apply-subst-lst alist (cdr lst))))))
  570. (define (tautp x)
  571. (tautologyp (rewrite x)
  572. '() '()))
  573. (define (tautologyp x true-lst false-lst)
  574. (cond ((truep x true-lst)
  575. #t)
  576. ((falsep x false-lst)
  577. #f)
  578. ((not (pair? x))
  579. #f)
  580. ((eq? (car x) if-constructor)
  581. (cond ((truep (cadr x)
  582. true-lst)
  583. (tautologyp (caddr x)
  584. true-lst false-lst))
  585. ((falsep (cadr x)
  586. false-lst)
  587. (tautologyp (cadddr x)
  588. true-lst false-lst))
  589. (else (and (tautologyp (caddr x)
  590. (cons (cadr x)
  591. true-lst)
  592. false-lst)
  593. (tautologyp (cadddr x)
  594. true-lst
  595. (cons (cadr x)
  596. false-lst))))))
  597. (else #f)))
  598. (define if-constructor '*) ; becomes (symbol->symbol-record 'if)
  599. (define rewrite-count 0) ; sanity check
  600. (define (rewrite term)
  601. (set! rewrite-count (+ rewrite-count 1))
  602. (cond ((not (pair? term))
  603. term)
  604. (else (rewrite-with-lemmas (cons (car term)
  605. (rewrite-args (cdr term)))
  606. (get-lemmas (car term))))))
  607. (define (rewrite-args lst)
  608. (cond ((null? lst)
  609. '())
  610. (else (cons (rewrite (car lst))
  611. (rewrite-args (cdr lst))))))
  612. (define (rewrite-with-lemmas term lst)
  613. (cond ((null? lst)
  614. term)
  615. ((one-way-unify term (cadr (car lst)))
  616. (rewrite (apply-subst unify-subst (caddr (car lst)))))
  617. (else (rewrite-with-lemmas term (cdr lst)))))
  618. (define unify-subst '*)
  619. (define (one-way-unify term1 term2)
  620. (begin (set! unify-subst '())
  621. (one-way-unify1 term1 term2)))
  622. (define (one-way-unify1 term1 term2)
  623. (cond ((not (pair? term2))
  624. (let ((temp-temp (assq term2 unify-subst)))
  625. (cond (temp-temp
  626. (term-equal? term1 (cdr temp-temp)))
  627. ((number? term2) ; This bug fix makes
  628. (equal? term1 term2)) ; nboyer 10-25% slower!
  629. (else
  630. (set! unify-subst (cons (cons term2 term1)
  631. unify-subst))
  632. #t))))
  633. ((not (pair? term1))
  634. #f)
  635. ((eq? (car term1)
  636. (car term2))
  637. (one-way-unify1-lst (cdr term1)
  638. (cdr term2)))
  639. (else #f)))
  640. (define (one-way-unify1-lst lst1 lst2)
  641. (cond ((null? lst1)
  642. (null? lst2))
  643. ((null? lst2)
  644. #f)
  645. ((one-way-unify1 (car lst1)
  646. (car lst2))
  647. (one-way-unify1-lst (cdr lst1)
  648. (cdr lst2)))
  649. (else #f)))
  650. (define (falsep x lst)
  651. (or (term-equal? x false-term)
  652. (term-member? x lst)))
  653. (define (truep x lst)
  654. (or (term-equal? x true-term)
  655. (term-member? x lst)))
  656. (define false-term '*) ; becomes (translate-term '(f))
  657. (define true-term '*) ; becomes (translate-term '(t))
  658. ; The next two procedures were in the original benchmark
  659. ; but were never used.
  660. (define (trans-of-implies n)
  661. (translate-term
  662. (list (quote implies)
  663. (trans-of-implies1 n)
  664. (list (quote implies)
  665. 0 n))))
  666. (define (trans-of-implies1 n)
  667. (cond ((equal? n 1)
  668. (list (quote implies)
  669. 0 1))
  670. (else (list (quote and)
  671. (list (quote implies)
  672. (- n 1)
  673. n)
  674. (trans-of-implies1 (- n 1))))))
  675. ; Translated terms can be circular structures, which can't be
  676. ; compared using Scheme's equal? and member procedures, so we
  677. ; use these instead.
  678. (define (term-equal? x y)
  679. (cond ((pair? x)
  680. (and (pair? y)
  681. (symbol-record-equal? (car x) (car y))
  682. (term-args-equal? (cdr x) (cdr y))))
  683. (else (equal? x y))))
  684. (define (term-args-equal? lst1 lst2)
  685. (cond ((null? lst1)
  686. (null? lst2))
  687. ((null? lst2)
  688. #f)
  689. ((term-equal? (car lst1) (car lst2))
  690. (term-args-equal? (cdr lst1) (cdr lst2)))
  691. (else #f)))
  692. (define (term-member? x lst)
  693. (cond ((null? lst)
  694. #f)
  695. ((term-equal? x (car lst))
  696. #t)
  697. (else (term-member? x (cdr lst)))))
  698. (set! setup-boyer
  699. (lambda ()
  700. (set! *symbol-records-alist* '())
  701. (set! if-constructor (symbol->symbol-record 'if))
  702. (set! false-term (translate-term '(f)))
  703. (set! true-term (translate-term '(t)))
  704. (setup)))
  705. (set! test-boyer
  706. (lambda (n)
  707. (set! rewrite-count 0)
  708. (let ((answer (test n)))
  709. (write rewrite-count)
  710. (display " rewrites")
  711. (newline)
  712. (if answer
  713. rewrite-count
  714. #f)))))