;;;-*- Mode:LISP; Package:user; Base:8; Source-Optimizations:T; Readtable:ZL -*-
;;; From the "Dick Gabriel" Benchmark Series.
;;; Enhancements (C) Copyright 1983, Lisp Machine, Inc.
;;;BEGIN
;;;BOYER
;;; The Maclisp Code


;(SPECIAL UNIFY-SUBST TEMP-TEMP)
;evaluate these manually in LISPM environment.
;call (setup) manually.
;then (test) to do it.

(defvar boyer-setup-p nil)
(defvar unify-subst nil)
(defvar temp-temp nil)

;(DEFUN PTIME NIL (LIST (RUNTIME) (STATUS GCTIME)))

(defun my-putprop (a b c) (setf (get a c) b))
(defun my-member (thing list)
  (dolist (e list)
    (cond ((equal thing e) (return e)))))
(defun my-assq (thing list)
  (dolist (item list)
    (when (eq (car item) thing)
      (return item))))

(DEFUN ADD-LEMMA (TERM)
       (COND ((AND (NOT (ATOM TERM))
		   (EQ (CAR TERM)
		       (QUOTE EQUAL))
		   (NOT (ATOM (CADR TERM))))
	      (MY-PUTPROP (CAR (CADR TERM))
		       (CONS TERM (GET (CAR (CADR TERM))
					   (QUOTE LEMMAS)))
		       (QUOTE LEMMAS)))
	     (T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM)
		       TERM))))
(DEFUN ADD-LEMMA-LST (LST)
       (COND ((NULL LST)
	      T)
	     (T (ADD-LEMMA (CAR LST))
		(ADD-LEMMA-LST (CDR LST)))))
(DEFUN APPLY-SUBST (ALIST TERM)
       (COND ((ATOM TERM)
	      (COND ((SETQ TEMP-TEMP (MY-ASSQ TERM ALIST))
		     (CDR TEMP-TEMP))
		    (T TERM)))
	     (T (CONS (CAR TERM)
		      (APPLY-SUBST-LST ALIST (CDR TERM))))))
(DEFUN APPLY-SUBST-LST (ALIST LST)
       (COND ((NULL LST)
	      NIL)
	     (T (CONS (APPLY-SUBST ALIST (CAR LST))
		      (APPLY-SUBST-LST ALIST (CDR LST))))))
(DEFUN FALSEP (X LST)
       (OR (EQUAL X (QUOTE (F)))
	   (MY-MEMBER X LST)))
(DEFUN ONE-WAY-UNIFY (TERM1 TERM2)
       (PROGN (SETQ UNIFY-SUBST NIL)
	      (ONE-WAY-UNIFY1 TERM1 TERM2)))
(DEFUN ONE-WAY-UNIFY1 (TERM1 TERM2)
       (COND ((ATOM TERM2)
	      (COND ((SETQ TEMP-TEMP (MY-ASSQ TERM2 UNIFY-SUBST))
		     (EQUAL TERM1 (CDR TEMP-TEMP)))
		    (T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
					       UNIFY-SUBST))
		       T)))
	     ((ATOM TERM1)
	      NIL)
	     ((EQ (CAR TERM1)
		  (CAR TERM2))
	      (ONE-WAY-UNIFY1-LST (CDR TERM1)
				  (CDR TERM2)))
	     (T NIL)))
(DEFUN ONE-WAY-UNIFY1-LST (LST1 LST2)
       (COND ((NULL LST1)
	      T)
	     ((ONE-WAY-UNIFY1 (CAR LST1)
			      (CAR LST2))
	      (ONE-WAY-UNIFY1-LST (CDR LST1)
				  (CDR LST2)))
	     (T NIL)))
(DEFUN REWRITE (TERM)
       (COND ((ATOM TERM)
	      TERM)
	     (T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
					   (REWRITE-ARGS (CDR TERM)))
				     (GET (CAR TERM)
					      (QUOTE LEMMAS))))))
(DEFUN REWRITE-ARGS (LST)
       (COND ((NULL LST)
	      NIL)
	     (T (CONS (REWRITE (CAR LST))
		      (REWRITE-ARGS (CDR LST))))))
(DEFUN REWRITE-WITH-LEMMAS (TERM LST)
       (COND ((NULL LST)
	      TERM)
	     ((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
	      (REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
	     (T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))
(DEFUN  SETUP NIL
  (ADD-LEMMA-LST
    (QUOTE ((EQUAL (COMPILE FORM)
		   (REVERSE (CODEGEN (OPTIMIZE FORM)
				     (NIL))))
	    (EQUAL (EQP X Y)
		   (EQUAL (FIX X)
			  (FIX Y)))
	    (EQUAL (GREATERP X Y)
		   (LESSP Y X))
	    (EQUAL (LESSEQP X Y)
		   (NOT (LESSP Y X)))
	    (EQUAL (GREATEREQP X Y)
		   (NOT (LESSP X Y)))
	    (EQUAL (BOOLEAN X)
		   (OR (EQUAL X (T))
		       (EQUAL X (F))))
	    (EQUAL (IFF X Y)
		   (AND (IMPLIES X Y)
			(IMPLIES Y X)))
	    (EQUAL (EVEN1 X)
		   (IF (ZEROP X)
		       (T)
		       (ODD (SUB1 X))))
	    (EQUAL (COUNTPS- L PRED)
		   (COUNTPS-LOOP L PRED (ZERO)))
	    (EQUAL (FACT- I)
		   (FACT-LOOP I 1))
	    (EQUAL (REVERSE- X)
		   (REVERSE-LOOP X (NIL)))
	    (EQUAL (DIVIDES X Y)
		   (ZEROP (REMAINDER Y X)))
	    (EQUAL (ASSUME-TRUE VAR ALIST)
		   (CONS (CONS VAR (T))
			 ALIST))
	    (EQUAL (ASSUME-FALSE VAR ALIST)
		   (CONS (CONS VAR (F))
			 ALIST))
	    (EQUAL (TAUTOLOGY-CHECKER X)
		   (TAUTOLOGYP (NORMALIZE X)
			       (NIL)))
	    (EQUAL (FALSIFY X)
		   (FALSIFY1 (NORMALIZE X)
			     (NIL)))
	    (EQUAL (PRIME X)
		   (AND (NOT (ZEROP X))
			(NOT (EQUAL X (ADD1 (ZERO))))
			(PRIME1 X (SUB1 X))))
	    (EQUAL (AND P Q)
		   (IF P (IF Q (T)
			     (F))
		       (F)))
	    (EQUAL (OR P Q)
		   (IF P (T)
		       (IF Q (T)
			   (F))
		       (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 (MY-MEMBER X (APPEND A B))
		   (OR (MY-MEMBER X A)
		       (MY-MEMBER X B)))
	    (EQUAL (MY-MEMBER X (REVERSE Y))
		   (MY-MEMBER X Y))
	    (EQUAL (LENGTH (REVERSE X))
		   (LENGTH X))
	    (EQUAL (MY-MEMBER A (INTERSECT B C))
		   (AND (MY-MEMBER A B)
			(MY-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 (GREATEREQPR X Y)
		   (NOT (LESSP X Y)))
	    (EQUAL (EQUAL X (TIMES X Y))
		   (OR (EQUAL X (ZERO))
		       (AND (NUMBERP X)
			    (EQUAL Y 1))))
	    (EQUAL (REMAINDER (TIMES Y X)
			      Y)
		   (ZERO))
	    (EQUAL (EQUAL (TIMES A B)
			  1)
		   (AND (NOT (EQUAL A (ZERO)))
			(NOT (EQUAL B (ZERO)))
			(NUMBERP A)
			(NUMBERP B)
			(EQUAL (SUB1 A)
			       (ZERO))
			(EQUAL (SUB1 B)
			       (ZERO))))
	    (EQUAL (LESSP (LENGTH (DELETE X L))
			  (LENGTH L))
		   (MY-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 (MY-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)))))))
(DEFUN TAUTOLOGYP (X TRUE-LST FALSE-LST)
       (COND ((TRUEP X TRUE-LST)
	      T)
	     ((FALSEP X FALSE-LST)
	      NIL)
	     ((ATOM X)
	      NIL)
	     ((EQ (CAR X)
		  (QUOTE IF))
	      (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))
		    (T (AND (TAUTOLOGYP (CADDR X)
					(CONS (CADR X)
					      TRUE-LST)
					FALSE-LST)
			    (TAUTOLOGYP (CADDDR X)
					TRUE-LST
					(CONS (CADR X)
					      FALSE-LST))))))
	     (T NIL)))
(DEFUN TAUTP (X)
       (TAUTOLOGYP (REWRITE X)
		   NIL NIL))
(DEFUN TEST NIL
       (PROG (ANS TERM)
	     (SETQ TERM
		   (APPLY-SUBST
		     (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)
				(MY-MEMBER A (LENGTH B)))))
		     (QUOTE (IMPLIES (AND (IMPLIES X Y)
					  (AND (IMPLIES Y Z)
					       (AND (IMPLIES Z U)
						    (IMPLIES U W))))
				     (IMPLIES X W)))))
	     (SETQ ANS (TAUTP TERM))))

(DEFUN TRANS-OF-IMPLIES (N)
       (LIST (QUOTE IMPLIES)
	     (TRANS-OF-IMPLIES1 N)
	     (LIST (QUOTE IMPLIES)
		   0 N)))
(DEFUN TRANS-OF-IMPLIES1 (N)
       (COND ((EQUAL N 1)
	      (LIST (QUOTE IMPLIES)
		    0 1))
	     (T (LIST (QUOTE AND)
		      (LIST (QUOTE IMPLIES)
			    (SUB1 N)
			    N)
		      (TRANS-OF-IMPLIES1 (SUB1 N))))))
(DEFUN TRUEP (X LST)
       (OR (EQUAL X (QUOTE (T)))
	   (MY-MEMBER X LST)))

;(INCLUDE "TIMER.LSP")

;(TIMER TIMIT (TEST))
;(SETUP)
;;;END

(defun do-boyer-setup ()
  (setup)
  (loop))

(defun do-boyer ()
 ;will delay approx 10 seconds, flash light, run boyer three times, and flash light again.
;  (cond ((not boyer-setup-p)
;	 (setup)
;	 (setq boyer-setup-p t)))
  (delay 10.)
  (boot:modify-memory-control
    #'(lambda (memory-control)
	(hw:dpb-xor 1. hw:%%memory-control-led-1 memory-control)))
  (dotimes (c 3.)
    (test))
  (boot:modify-memory-control
    #'(lambda (memory-control)
	(hw:dpb-xor 1. hw:%%memory-control-led-1 memory-control)))
  (loop))


(defun test-delay ()
  (delay 10.)
  (boot:modify-memory-control
    #'(lambda (memory-control)
	(hw:dpb-xor 1. hw:%%memory-control-led-1 memory-control)))
  (loop))

(defun delay (approx-seconds)
  (dotimes (c approx-seconds)
    (dotimes (c1 2.)
      (dotimes (c2 1000.)
	(dotimes (c3 1000.))))))