Artifact 492e3d8e5142b31cc5597d4f78db849a6f78cb61c53c82975c41b5edafce2ad7:

• File psl-1983/3-1/tests/irewrite.sl — part of check-in [eb17ceb7f6] at 2020-04-21 19:40:01 on branch master — Add Reduce 3.0 to the historical section of the archive, and some more
  files relating to version sof PSL from the early 1980s. Thanks are due to
  Paul McJones and Nelson Beebe for these, as well as to all the original
  authors.

  git-svn-id: https://svn.code.sf.net/p/reduce-algebra/code/historical@5328 2bfe0521-f11c-4a00-b80e-6202646ff360 (user: arthurcnorman@users.sourceforge.net, size: 12423) [annotate] [blame] [check-ins using] [more...]

• File psl-1983/tests/irewrite.sl — part of check-in [eb17ceb7f6] at 2020-04-21 19:40:01 on branch master — Add Reduce 3.0 to the historical section of the archive, and some more
  files relating to version sof PSL from the early 1980s. Thanks are due to
  Paul McJones and Nelson Beebe for these, as well as to all the original
  authors.

  git-svn-id: https://svn.code.sf.net/p/reduce-algebra/code/historical@5328 2bfe0521-f11c-4a00-b80e-6202646ff360 (user: arthurcnorman@users.sourceforge.net, size: 12423) [annotate] [blame] [check-ins using]

% {DSK}IREWRITE.PSL;2  6-JAN-83 10:08:06 
(FLUID '(unify-subst))
(FLAG '(
ADD-LEMMA
ADD-LEMMA-LST
Apply-subst
Apply-subst-lst
false
one-way-unify
one-way-unify1
one-way-unify1-lst
ptime
rewrite
rewrite-with-lemmas
tautologyP
tautp
trans-of-implies
trans-of-implies1
truep

) 'InternalFunction)


(DE ADD-LEMMA (TERM)
(COND ((AND (NOT (ATOM TERM))
	    (EQ (CAR TERM)
		'EQUAL)
	    (NOT (ATOM (CADR TERM))))
       (PUT (CAR (CADR TERM))
	    'LEMMAS
	    (CONS TERM (GET (CAR (CADR TERM))
			    'LEMMAS))))
      (T (ERROR 0 (LIST 'ADD-LEMMA-DID-NOT-LIKE-TERM
			TERM)))))


(DE ADD-LEMMA-LST (LST)
(COND ((NULL LST)
       T)
      (T (ADD-LEMMA (CAR LST))
	 (ADD-LEMMA-LST (CDR LST)))))


% lmm  7-JUN-81 10:07 
(DE APPLY-SUBST (ALIST TERM)
(COND ((NOT (PAIRP TERM))
       ((LAMBDA (TEM)
	  (COND
	    (TEM (CDR TEM))
	    (T TERM)))
	(ASSOC TERM ALIST)))
      (T (CONS (CAR TERM)
	       (MAPCAR (CDR TERM)
		       (FUNCTION (LAMBDA (X)
				   (APPLY-SUBST ALIST X))))))))


(DE APPLY-SUBST-LST (ALIST LST)
(COND ((NULL LST)
       NIL)
      (T (CONS (APPLY-SUBST ALIST (CAR LST))
	       (APPLY-SUBST-LST ALIST (CDR LST))))))


(DE FALSEP (X LST)
(OR (EQUAL X '(F))
    (MEMBER X LST)))


(DE ONE-WAY-UNIFY (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
       (ONE-WAY-UNIFY1 TERM1 TERM2)))


% lmm  7-JUN-81 09:47 
(DE ONE-WAY-UNIFY1 (TERM1 TERM2)
(COND ((NOT (PAIRP TERM2))
       ((LAMBDA (TEM)
	  (COND
	    (TEM (EQUAL TERM1 (CDR TEM)))
	    (T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
				       UNIFY-SUBST))
	       T)))
	(ASSOC TERM2 UNIFY-SUBST)))
      ((NOT (PAIRP TERM1))
       NIL)
      ((EQ (CAR TERM1)
	   (CAR TERM2))
       (ONE-WAY-UNIFY1-LST (CDR TERM1)
			   (CDR TERM2)))
      (T NIL)))


(DE 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)))


(DE PTIME NIL
(PROG (GCTM)
      (SETQ GCTM 0)
      (RETURN (CONS (time)
		    GCTM))))


% lmm  7-JUN-81 10:04 
(DE REWRITE (TERM)
(COND ((NOT (PAIRP TERM))
       TERM)
      (T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
				    (MAPCAR (CDR TERM)
					    (FUNCTION REWRITE)))
			      (GET (CAR TERM)
				   'LEMMAS)))))


(DE 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)))))


(DE SETUP NIL
(ADD-LEMMA-LST
  '((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 (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 (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))
	   (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))))))


% lmm  7-JUN-81 09:44 
(DE TAUTOLOGYP (X TRUE-LST FALSE-LST)
(COND ((TRUEP X TRUE-LST)
       T)
      ((FALSEP X FALSE-LST)
       NIL)
      ((NOT (PAIRP X))
       NIL)
      ((EQ (CAR X)
	   '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)))


(DE TAUTP (X)
(TAUTOLOGYP (REWRITE X)
	    NIL NIL))


(DE TEST NIL
(PROG (TM1 TM2 ANS TERM)
      (SETQ TM1 (PTIME))
      (SETQ TERM (APPLY-SUBST '((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))))
			      '(IMPLIES (AND (IMPLIES X Y)
					     (AND (IMPLIES Y Z)
						  (AND (IMPLIES Z U)
						       (IMPLIES U W))))
					(IMPLIES X W))))
      (SETQ ANS (TAUTP TERM))
      (SETQ TM2 (PTIME))
      (RETURN (LIST ANS (DIFFERENCE (CAR TM2)
				    (CAR TM1))
		    (DIFFERENCE (CDR TM2)
				(CDR TM1))))))


(DE TRANS-OF-IMPLIES (N)
(LIST 'IMPLIES
      (TRANS-OF-IMPLIES1 N)
      (LIST 'IMPLIES
	    0 N)))


(DE TRANS-OF-IMPLIES1 (N)
(COND ((EQUAL N 1)
       (LIST 'IMPLIES
	     0 1))
      (T (LIST 'AND
	       (LIST 'IMPLIES
		     (SUB1 N)
		     N)
	       (TRANS-OF-IMPLIES1 (SUB1 N))))))


(DE TRUEP (X LST)
(OR (EQUAL X '(T))
    (MEMBER X LST)))