plnr

;kset fonts;22fg kst,,,


(declare (genprefix plnr))

(COMMENT DO NOT GRIND THIS FILE WITH THE STANDARD GRIND)

(SETQ THVERSION (CADR (STATUS UREAD)))

(DECLARE (PRINT (LIST 'SETQ 'THVERSION (LIST 'QUOTE
					     (CADR (STATUS UREAD))))))


(DECLARE (*FEXPR THAPPLY
		 THGENAME
		 THSTATE
		 THANTE
		 THERASING
		 THCONSE
		 THDUMP
		 THRESTRICT
		 THBKPT
		 THUNIQUE
		 THVSETQ
		 THMESSAGE
		 THDO
		 THGOAL
		 THERASE
		 THAND
		 THNV
		 THSUCCEED
		 THAMONG
		 THCOND
		 THSETQ
		 THASSERT
		 THASVAL
		 THERT
		 THGO
		 THFAIL
		 THOR
		 THFIND
		 THFINALIZE
		 THRETURN
		 THPROG
		 THFLUSH
		 THNOT
		 THV))

(DECLARE (MACROS T) (GENPREFIX TH))

(SETQ SYMBOLS T)
(COND ((ERRSET (AND PURE (SETQ LOW (PAGEBPORG))))) (' (NOT PURIFIED)))


(DEFUN THREAD					;FUNCTION FOR THE /$ READ MACRO
       
       ;;EXPANDS _ TO (THNV (READ)) EXPANDS A TO ASSERT  ;EXPANDS G TO GOAL EXPANDS T TO THTBF THTRUE
       NIL					;EXPANDS ? TO (THV (READ)) EXPANDS E TO (THEV
						;(READ))					 
  (PROG (CHAR)					;EXPANDS R TO THRESTRICT			 
	
	;;TREATS & - - & AS A COMMENT
	(RETURN (COND ((EQ (SETQ CHAR (READCH)) (QUOTE ?))
		       (LIST (QUOTE THV) (READ)))
		      ((EQ CHAR (QUOTE E))
		       (LIST (QUOTE THEV) (READ)))
		      ((EQ CHAR (QUOTE _))
		       (LIST (QUOTE THNV) (READ)))
		      ((EQ CHAR (QUOTE &))
		       (PROG NIL
			  CHLP (COND ((EQ (QUOTE &) (READCH))
				      (RETURN (QUOTE (COMMENT)))))
			     (GO CHLP)))
		      ((EQ CHAR (QUOTE T))
		       (QUOTE (THTBF THTRUE)))
		      ((EQ CHAR (QUOTE R)) (QUOTE THRESTRICT))
		      ((EQ CHAR (QUOTE G)) (QUOTE THGOAL))
		      ((EQ CHAR (QUOTE A)) (QUOTE THASSERT))
		      ((EQ CHAR 'N) (LIST 'THANUM (READ)))
		      ((PRINT (QUOTE ILLEGAL-PREFIX))
		       (PRINC (QUOTE $))
		       (PRINC CHAR)
		       (PRINC (READ))
		       (ERR NIL))))))

(DEFUN THPUSH
       MACRO
       (A)							       ;(THPUSH THTREE NEWINFO) CONSES NEWINFO ONTO
       (LIST (QUOTE SETQ)					       ;THTREE
	     (CADR A)
	     (LIST (QUOTE CONS) (CADDR A) (CADR A))))

(DEFUN EVLIS
       (X)							       ;EVLIS EVALS ELEMENTS OF ARG THEN RETURNS ARG
       (MAPC (FUNCTION EVAL) X))

(DEFUN THPRINT2 (X) (PRINC (QUOTE / )) (PRINC X))

(DEFUN THPRINTC (X) (TERPRI) (PRINC X) (PRINC '/ ))

(DECLARE (SPECIAL THTT THFST THTTL THLAS THNF THWH THFSTP))
(DEFUN THADD							       ;THADD ADDS THEOREMS OR ASSERTION TO THE
       
       ;;INPUT - THPL - PROPERTY LIST TO BE PLACED ON    ;ASSERTION
       (THTT THPL)						       ;DATABASE INPUTS - THTT - NAME OF THM OR ACTUAL
								       ;ASSERTION					
       (PROG (THNF THWH THCK THLAS THTTL THT1 THFST THFSTP THFOO)      ;RETURNS NIL IF ALREADY THERE ELSE RETURNS THTT
	     (SETQ THCK
		   (COND ((ATOM THTT)
			  
			  ;;IF THTT IS ATOMIC WE ARE ASSERTING A THEOREM
			  (OR (SETQ THT1 (GET THTT (QUOTE THEOREM)))
			      
			      ;;IF NO THEOREM PROPERTY THE GUY MADE A MISTAKE
			      (PROG2 (PRINT THTT) (THERT CANT
							 THASSERT/,
							 NO
							 THEOREM
							 -
							 THADD)))
			  (SETQ THWH (CAR THT1))
			  
			  ;;THWH NOW SET TO KIND OF THEOREM, LIKE THERASING
			  (SETQ THTTL THTT)
			  
			  ;;MAKE AN EXTRA POINTER TO THTT
			  (AND THPL
			       
			       ;;IF WE HAVE A PL FOR OUR THEOREM, IT GOES ON
			       ;;THE ATOM WHICH IS THE NAME OF THE THEOREM
			       (PROG NIL
				     
				     ;;GO THROUGH ITEMS ON PL ONE BY ONE
				LP   (THPUTPROP THTT
						(CADR THPL)
						(CAR THPL))
				     (COND ((SETQ THPL (CDDR THPL))
					    (GO LP)))))
			  (CADDR THT1))
			 (T (SETQ THWH (QUOTE THASSERTION))
			    
			    ;;SO WE HAVE AN ASSERTION TO ASSERT, MAKE THWH REFLECT THIS FACT
			    (SETQ THTTL (CONS THTT THPL))
			    
			    ;;PROPERTY LIST IS "CDR" OF ASSERTION
			    THTT)))
	     (SETQ THNF 0.)
	     
	     ;;THNF IS COUNTER SAYING WHICH ATOM WE ARE FILING UNDER
	     (SETQ THLAS (LENGTH THCK))
	     
	     ;;THLAS IS THE NUMBER OF TOP LEVEL ITEMS
	     (SETQ THFST T)
	     
	     ;;THFST SAYS WE ARE TRYING TO PUT THE ITEM IN FOR THE FIRST TIME
	     ;;WE NEED TO KNOW THIS SINCE THE FIRST TIME THROUGH
	     ;;WE MUST TEST THAT THE ASSERTEE IS NOT ALREADY THERE
	     ;;THCK IS INITIALLY THE ASSERTION OR THEOREM PATTERN
	     ;;THE FIRST TIME WE GO INTO THE DATABASE WE CHECK TO
	     ;;SEE IF THE ITEM IS THERE
	     ;;THAT MEANS DOING AN EQUAL TEST ON EVERY
	     ;;ITEM IN THE BUCKET.  AFTER THE FIRST TIME THIS IS NOT
	     ;;NECESSARY.  SINCE VARIABLES WILL IN GENERAL HAVE MANY
	     ;;MORE ITEMS IN THEIR BUCKET WE WILL WANT TO DO OUR
	     ;;CHECK ON A NON VARIABLE ITEM IN THE PATTERN
	THP1 (COND ((NULL THCK) 
				;;THCK NIL MEANS THAT ALL THE ITEMS IN THE PATTERN ARE VARIABLES
				;;SO WE TRY AGAIN ONLY THIS TIME DOING EQUAL CHECK ON
				;;THE FIRST VARIABLE. THFOO NOW IS SIMPLY THE PATTERN
				(SETQ THCK THFOO)
				(SETQ THNF 0.)
				(SETQ THFOO (SETQ THFST NIL))
				
				;;THFIRSTP SAYS WE AGAIN NEED TO CHECK FOR ASSERTEE
				;;BEING IN DATA BASE, BUT NOW USE VARIABLES FOR EQ CHECK
				(SETQ THFSTP T)
				(GO THP1))
		   ((NULL (SETQ THT1 (THIP (CAR THCK)))) (RETURN NIL))
		   
		   ;;THIP IS THE WORKHORSE FOR THADD IF IT RETURNS NIL
		   ;;IT MEANS THE ASSERTEE IS ALREADY IN, SO FAIL
		   ((EQ THT1 (QUOTE THOK)))
		   
		   ;;THOK WHICH IS RETURN BY THIP
		   ;;SAYS THAT THE ASSERTEE IS NOT IN ALREADY
		   ((SETQ THFOO
			  
			  ;;OTHERWISE WE GO AROUND AGAIN, STILL LOOKING FOR A NON
			  ;;VARIABLE ITEM TO DO THE EQ CHECK
			  (NCONC THFOO
				 (LIST (COND ((EQ THT1 (QUOTE THVRB))
					      (CAR THCK))))))
		    (SETQ THCK (CDR THCK))
		    (GO THP1)))
	     (SETQ THFST NIL)
	     (MAPC (FUNCTION THIP) (CDR THCK))
	     (SETQ THNF 0.)
	     (MAPC (FUNCTION THIP) THFOO)
	     (RETURN THTTL)))

(DECLARE (UNSPECIAL THTT THFST THFSTP THTTL THLAS THNF THWH))

(DECLARE (SPECIAL THTREE THALIST THXX))

(DEFUN THAMONG
       FEXPR
  (THA)						;EXAMPLE - (THAMONG $?X (THFIND ... ))
  (COND						;$E - (THAMONG $E$?X (THFIND ... )) CAUSES THE
						;THVALUE OF 				 ;$?X    ;TO BE THE FIRST INPUT TO THAMONG. THXX SET ;TO
    ((EQ (CADR (SETQ THXX (THGAL (COND ((EQ (CAAR THA)	;OLD BINDING CELL OF $?X (OR $E$?X) IF $?X
					    
					    ;;VALUES PUSHED ONTO THTREE AND THAMONG FAILS TO
					    (QUOTE THEV))	;THUNASSIGNED, OLD VALUE AND LIST OF NEW 	
					(THVAL (CADAR THA)	;THAMONGF.
					       THALIST))
				       (T (CAR THA)))
				 THALIST)))
	 (QUOTE THUNASSIGNED))
     (THPUSH THTREE (LIST (QUOTE THAMONG)
			  THXX
			  (THVAL (CADR THA) THALIST)))
     NIL)					;IF $?X ASSIGNED, THAMONG REDUCES TO A
    (T (MEMBER (CADR THXX) (THVAL (CADR THA) THALIST)))))	;MEMBERSHIP TEST

(DECLARE (UNSPECIAL THTREE THALIST THXX))

(DECLARE (SPECIAL THALIST THBRANCH THABRANCH THTREE THML))

(DEFUN THAMONGF							       ;(CAR THTREE) = (THAMONG OLDBINDINGCELL (NEW
       NIL							       ;VALUES))
       (COND (THMESSAGE (THPOPT) NIL)
	     ((CADDAR THTREE)					       ;LIST OF NEW VALUES NON NIL
	      (RPLACA (CDADAR THTREE) (CAADDR (CAR THTREE)))	       ;REPLACE OLD VALUE WITH NEW VALUE
	      (RPLACA (CDDAR THTREE) (CDADDR (CAR THTREE)))	       ;POP NEW VALUES
	      (SETQ THBRANCH THTREE)				       ;STORE AWAY TREE FOR POSSIBLE BACKTRACKING
	      (SETQ THABRANCH THALIST)				       ;STORE AWAY THALIST FOR POSSIBLE BACKTRACKING
	      (THPOPT)						       ;POP TREE
	      T)						       ;SUCCEED
	     (T (RPLACA (CDADAR THTREE) (QUOTE THUNASSIGNED))	       ;NO NEW VALUES LEFT. RETURN X TO THUNASSIGNED,
		(THPOPT)					       ;POP TREE AND CONTINUE FAILING.		
		NIL)))

(DECLARE (UNSPECIAL THALIST THBRANCH THABRANCH THTREE THML))

(DECLARE (SPECIAL THTREE THEXP))

(DEFUN THAND FEXPR (A) (OR (NOT A)
			   (PROG2 (THPUSH THTREE
					  (LIST (QUOTE THAND) A NIL))
				  (SETQ THEXP (CAR A)))))

(DECLARE (UNSPECIAL THTREE THEXP))

(DEFUN THANDF NIL (THBRANCHUN) NIL)

(DECLARE (SPECIAL THTREE THVALUE THEXP))
(DEFUN THANDT
       NIL
       (COND ((CDADAR THTREE) (THBRANCH)
			      (SETQ THEXP (CADR (CADAR THTREE)))
			      (RPLACA (CDAR THTREE) (CDADAR THTREE)))
	     ((THPOPT)))
       THVALUE)

(DECLARE (UNSPECIAL THTREE THVALUE THEXP))

(DEFUN THANTE FEXPR
       (THX)							       ;DEFINES AND OPTIONALLY ASSERTS ANTECEDENT
       (THDEF (QUOTE THANTE) THX))				       ;THEOREMS)

(DECLARE (SPECIAL THTREE THTRACE THOLIST THALIST))

(DEFUN THAPPLY FEXPR (L) (THAPPLY1 (CAR L)
				   
				   ;;THAPPLY1 DOES THE REAL WORK, ALL WE DO IS GET THE THEOREM OFF THE
				   ;;PROPERTY LIST
				   (GET (CAR L) (QUOTE THEOREM))
				   (CADR L)))

(DEFUN THAPPLY1
       (THM THB DAT)
       
       ;;MAKE SURE THE THEOREM PATTERN MATCHES THE GOAL
       (COND ((AND (THBIND (CADR THB)) (THMATCH1 DAT (CADDR THB)))
	      (AND THTRACE (THTRACES (QUOTE THEOREM) THM))
	      
	      ;;AS FAR AS THTREE GOES, ALL THEOREMS LOOK LIKE THPROG, AND
	      ;;WHEN YOU COME DOWN TO IT, THEY ALL ACT LIKE THPROGS
	      (THPUSH THTREE
		      (LIST (QUOTE THPROG) (CDDR THB) NIL (CDDR THB)))
	      
	      ;;CALL THE MAIN THPROG WORKHORSE
	      (THPROGA)
	      T)
	     
	     ;;IF THE THEOREM PATTERN DIDN'T MATCH, START FAILING
	     (T (SETQ THALIST THOLIST) (THPOPT) NIL)))

(DECLARE (UNSPECIAL THTREE THTRACE THOLIST THALIST))

(DECLARE (SPECIAL THALIST TYPE THX THTREE THEXP THTRACE THY1 THY))
(DEFUN THASS1
 (THA P)
 (PROG (THX THY1 THY TYPE PSEUDO)
       (AND (CDR THA) (EQ (CAADR THA) (QUOTE THPSEUDO)) (SETQ PSEUDO
							      T))
       
       ;;IF YOU SEE "THPSEUDO" SET FLAG "PSEUDO" TO T
       (OR (ATOM (SETQ THX (CAR THA)))
	   
	   ;;IF (CAR THA) IS AN ATOM WE ARE ASSERTING (ERRASING) A THEOREM
	   (THPURE (SETQ THX (THVARSUBST THX NIL)))
	   
	   ;;THVARSUBST SUBSTITUTES THE ASSIGNMENTS FOR ALL ASSIGNED VARIABLES
	   ;;THPURE CHECKS THAT ALL VARIABLES ARE ASSIGNED
	   PSEUDO
	   
	   ;;IF WE ARE NOT REALLY ASSERTING, THE VARIABLES DO NOT ALL HAVE TO BE ASSIGNED
	   (PROG2 (PRINT THX)
		  (THERT IMPURE ASSERTION OR ERASURE - THASS1)))
       (AND THTRACE (NOT PSEUDO) (THTRACES (COND (P (QUOTE THASSERT))
						 ((QUOTE THERASE)))
					   THX))
       (SETQ THA (COND (PSEUDO (CDDR THA)) ((CDR THA))))
       
       ;;THX IS NOW WHAT WE ARE ASSERTING, AND THA IS THE RECOMMENDATION LIST
       (OR
	
	;;WE ARE NOW GOING TO PHYSICALLY ADD OR REMOVE ITEM
	(SETQ
	 THX
	 (COND (PSEUDO (LIST THX))
	       
	       ;;IF THPSEUDO, DON'T ALTER THE DATA BASE
	       ;;IF P IS "T" WE ARE ASSERTING SO USE THADD
	       (P (THADD THX
			 
			 ;;THADD TAKES TWO ARGS THE FIRST IS ITEM TO BE ADDED
			 ;;THE SECOND IS THE PROPERTY LIST FOR THE ITEM
			 (SETQ THY
			       (COND ((AND THA (EQ (CAAR THA)
						   
						   ;;THPROP SAYS "MY CADR IS TO BE EVALED TO GET THE PROPERTY LIST
						   (QUOTE THPROP)))
				      (PROG2 0.
					     (EVAL (CADAR THA))
					     
					     ;;AND REMOVE THPROP FROM THE RECOMENDATION LIST
					     (SETQ THA
						   (CDR THA))))))))
	       
	       ;;OTHERWISE WE ARE ERASING, SO USE THREMOVE
	       (T (THREMOVE THX))))
	
	;;THE LAST ITEM WILL BE NIL ONLY IF THADD OR THREMOVE FAILED. 
	;;THAT IS, IF THE ITEM TO BE ADDED WAS ALREADY THERE,
	;;OR THE ONE TO BE REMOVED, WASN'T.
	(RETURN NIL))
       
       ;;TYPE IS THE KIND OF THEOREM WE WILL BE LOOKING FOR
       (COND (P (SETQ TYPE (QUOTE THANTE)))
	     ((SETQ TYPE (QUOTE THERASING))))
       
       ;;IF WE ACTUALLY MUNGED THE DATABASE, PUT THE FACT IN THTREE
       (OR PSEUDO
	   (THPUSH THTREE
		   (LIST (COND (P (QUOTE THASSERT)) ((QUOTE THERASE)))
			 THX
			 THY)))
       (SETQ THY (MAPCAN (FUNCTION THTAE) THA))
       
       ;;MAPCAN IS A MAC-LISP FUNCTION, LIKE MAPCAR BUT USES NCONC
       ;;THTAE LOOKS AT THE RECOMENDATION LIST AND PRODUCES A
       ;;LIST OF INSTRUCTIONS ABOUT WHAT THEOREMS TO TRY
       (COND (THY (SETQ THEXP (CONS 'THDO THY))))
       
       ;;THEXP IS A HACK TELLING THVAL TO THVAL THIS ITEM
       ;;BEFORE IT GOES ON TO THE NEXT LINE OF PLANNER CODE
       ;;THEXP IS NOW (THDO  <APPROPRIATE ANTECEDENT OR ERASING THEOREMS>)
       (RETURN THX)))

(DECLARE (UNSPECIAL THALIST TYPE THX THTREE THEXP THTRACE THY1 THY))

(DEFUN THASSERT FEXPR (THA) (THASS1 THA T))			       ;THASS1 IS USED FOR BOTH ASSERTING AND ERASING,   ;THE "T" AS SECOND ARG TELLS IT THAT WE ARE       ;ASSERTING. 

(DECLARE (SPECIAL THTREE))

(DEFUN THASSERTF
       NIL
       (THREMOVE (COND ((ATOM (CADAR THTREE)) (CADAR THTREE))
		       (T (CAADAR THTREE))))
       (THPOPT)
       NIL)

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THTREE))

(DEFUN THASSERTT NIL (PROG2 0. (CADAR THTREE) (THPOPT)))

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THALIST))

(DEFUN THASVAL
       FEXPR
       (X)
       ((LAMBDA (X) (AND X (NOT (EQ (CADR X) (QUOTE THUNASSIGNED)))))
	(THGAL (CAR X) THALIST)))

(DECLARE (UNSPECIAL THALIST) (SPECIAL THPC))
(DEFUN THBA
       
       ;;JUST LIKE ASSQ IN LISP, ONLY RETURN WITH THE POINTER 1
       ;;ELEMENT PRIOR TO THE ONE ASKED FOR
       ;;USED ONLY BY THAD AND THREMOVE
       (TH1 TH2)
       (PROG (THP)
	     (SETQ THP TH2)
	THP1 (AND (EQ (COND (THPC (CADR THP)) (T (CAADR THP))) TH1)
		  (RETURN THP))
	     (OR (CDR (SETQ THP (CDR THP))) (RETURN NIL))
	     (GO THP1)))

(DEFUN THBAP
       
       ;;LIKE THBA, ONLY USED EQUAL RATHER THAN EQ
       (TH1 TH2)
       (PROG (THP)
	     (SETQ THP TH2)
	THP1 (AND (EQUAL (COND (THPC (CADR THP)) (T (CAADR THP))) TH1)
		  (RETURN THP))
	     (OR (CDR (SETQ THP (CDR THP))) (RETURN NIL))
	     (GO THP1)))

(DECLARE (UNSPECIAL THPC) (SPECIAL THTREE THOLIST THALIST))
(DEFUN THBIND
       
       ;;WHEN WE ENTER A NEW THEOREM OR THPROG
       ;;WE MUST BIND THE NEW VARIABLES.  A IS THE VARIABLE LIST
       (A)
       
       ;;THOLIST IS THE OLD THALIST
       (SETQ THOLIST THALIST)
       
       ;;IF A IS NIL THERE IS NOTHING TO DO
       (OR (NULL A)
	   (PROG NIL
	    GO	 (COND 
		       ;;WHEN A IS NIL WE ARE DONE AND JUST PUT A MARKER
		       ;;ON THTREE WITH A POINTER TO THE OLD THALIST
		       ;;SO IT CAN BE RESTORED
		       ((NULL A)
			(THPUSH THTREE
				(LIST (QUOTE THREMBIND) THOLIST))
			(RETURN T)))
		 
		 ;;OTHERWISE ADD TO THE ALIST THE NEW BINDING CELL
		 (THPUSH THALIST
			 (COND ((ATOM (CAR A))
				
				;;THE FIRST ELEMENT IS THE NAME OF THE VARIABLE
				;;IF THE ENTRY IS AN ATOM, THEN WE ARE JUST GIVEN THE
				;;VARIABLE AND ITS INITIAL ASSIGNMENT IS "THUNASSIGNED"
				;;I.E., NO INITIAL ASSIGNMENT
				(LIST (CAR A) (QUOTE THUNASSIGNED)))
			       
			       ;;OTHERWISE OUR ENTRY IS A LIST
			       ;;IF THE FIRST ELEMENT OF THE LIST IS $R OR THRESTRICT
			       ;;WE ADD THE RESTRICTION TO THE BINDING CELL
			       ;;THE CDDR OF THE CELL GIVES THE RESTRICTION LIST
			       ((EQ (CAAR A) (QUOTE THRESTRICT))
				(NCONC (THBI1 (CADAR A)) (CDDAR A)))
			       
			       ;;OTHERWISE WE ARE GIVEN BOTH THE VARIABLE AND ITS
			       ;;INITIAL ASSIGNMENT, SO MAKE THE SECOND ELEMENT OF THE
			       ;;BINDING CELL A POINTER TO THE INITIAL ASSIGNMENT
			       (T (LIST (CAAR A) (EVAL (CADAR A))))))
		 (SETQ A (CDR A))
		 
		 ;;REPEAT FOR THE NEXT VARIABLE IN THE LIST
		 (GO GO))))

(DECLARE (UNSPECIAL THOLIST THTREE THALIST))

(DEFUN THBI1 (X) (COND ((ATOM X) (LIST X (QUOTE THUNASSIGNED)))
		       (T (LIST (CAR X) (EVAL (CADR X))))))

(DECLARE (SPECIAL THTRACE THVALUE))

(DEFUN THBKPT FEXPR (L) (OR (AND THTRACE (THTRACES (QUOTE THBKPT) L))
			    THVALUE))

(DECLARE (UNSPECIAL THTRACE THVALUE))

(DECLARE (SPECIAL THBRANCH THABRANCH THTREE))

(DEFUN THBRANCH
       NIL
       
       ;;THBRANCH IS CALLED BY THPROGT
       ;;AND WE ARE SUCCEEDING BACKWARDS
       ;;CAR THTREE IS THE THPROG MARKING
       (COND ;;THERE ARE NO MORE EXPRESSIONS TO EXECUTE IN THE THPROG
	     ((NOT (CDADAR THTREE)))
	     ((EQ THBRANCH THTREE) (SETQ THBRANCH NIL))
	     
	     ;;NORMAL CASE
	     ;;CADDAR THTREE IS THE SECOND OF THE THREE ARGS ON THE THPROG MARK
	     ;;THBRANCH AND THABRANCH ARE POINTERS TO THE THTREE AND THALIST
	     ;;RESPECTIVELY AT THE POINT WHERE WE HAD JUST SUCCEEDED. 
	     ;;IN GENERAL, BY THE TIME WE GET BACK TO THE THPROG MARK ON THTREE
	     ;;WE HAVE REMOVED THE THINGS PUT ON THTREE BY THE SUCCESSFUL
	     ;;LAST LINE OF THE THPROG
	     ;;WE WILL NOW STORE THIS INFORMATION ON THE THPROG MARK SO
	     ;;THAT IF WE FAIL WE WILL HAVE RECORDS OF WHAT HAPPEND
	     ;;IT IS STORED BY HACKING THE SECOND ARG TO THE THPROG MARK
	     ((RPLACA (CDDAR THTREE)
		      (CONS (LIST THBRANCH THABRANCH (CADAR THTREE))
			    (CADDAR THTREE)))
	      
	      ;;WE NOW SETQ THBRANCH TO NIL.  IF THE NEXT LINE ALSO SUCCEEDS,
	      ;;THVAL WILL LOOK FOR A NIL THBRRANCH TO INDICATE THAT IT SHOULD
	      ;;SETQ IT AGAIN TO THE POINT OF SUCCESS
	      (SETQ THBRANCH NIL))))

(DECLARE (UNSPECIAL THBRANCH THABRANCH THTREE))

(DECLARE (SPECIAL THTREE THALIST))

(DEFUN THBRANCHUN
       NIL
       
       ;;WE ARE NOW FAILING.  THBRANCHUN IS CALLED BY THPROGF
       (PROG (X) (RETURN (COND ;;IF THE SECOND ARG
			       ;;TO THE PROG MARK IS NON-NIL IT MEANS THAT THERE ARE
			       ;;PREVIOUS LINES IN THE THPROG TO FAIL BACK TO
			       ((SETQ X (CADDAR THTREE))
				
				;;A COMPAIRISON OF THIS WITH WHAT HAPPEND IN THBRANCK
				;;WILL REVEAL THAT ALL WE ARE DOING HERE IS RESTORING
				;;THE PROG MARK TO IS STATE BEFORE THE LAST SUCCESS
				(RPLACA (CDAR THTREE) (CADDAR X))
				(RPLACA (CDDAR THTREE) (CDR X))
				
				;;RESET THALIST AND THTREE
				(SETQ THALIST (CADAR X))
				(SETQ THTREE (CAAR X))
				T)
			       
			       ;;THERE AREN'T ANY MORE THINGS IN THE THPROG TO TRY
			       ;;SO JUST RETURN NIL
			       (T (THPOPT) NIL)))))

(DECLARE (UNSPECIAL THTREE THALIST))
(DECLARE (SPECIAL THTREE THEXP))

(DEFUN THCOND
       FEXPR
       (THA)
       (THPUSH THTREE (LIST (QUOTE THCOND) THA NIL))
       (SETQ THEXP (CAAR THA)))

(DECLARE (UNSPECIAL THTREE THEXP))

(DEFUN THCONDF NIL (THOR2 NIL))

(DECLARE (SPECIAL THTREE THVALUE))

(DEFUN THCONDT
       NIL
       (RPLACA (CAR THTREE) (QUOTE THAND))
       (RPLACA (CDAR THTREE) (CAADAR THTREE))
       THVALUE)

(DECLARE (UNSPECIAL THTREE THVALUE))

(COMMENT THCONSE DEFINES AND OPTIONALLY ASSERTS CONSEQUENT THEOREMS)

(DEFUN THCONSE FEXPR (THX) (THDEF (QUOTE THCONSE) THX))

(DEFUN THDATA NIL (PROG (X)
		   GO	(TERPRI)
			(COND ((NULL (SETQ X (READ NIL))) (RETURN T))
			      ((PRINT (THADD (CAR X) (CDR X)))))
			(GO GO)))

(COMMENT THDEF DEFINES AND OPTIONALLY ASSERTS THEOREMS)
(DEFUN THDEF
 (THMTYPE THX)
 (PROG (THNOASSERT? THMNAME THMBODY)
       (COND ((NOT (ATOM (CAR THX)))
	      (SETQ THMBODY THX)
	      (COND ((EQ THMTYPE (QUOTE THCONSE))
		     (SETQ THMNAME (THGENAME TC-G)))
		    ((EQ THMTYPE (QUOTE THANTE))
		     (SETQ THMNAME (THGENAME TA-G)))
		    ((EQ THMTYPE (QUOTE THERASING))
		     (SETQ THMNAME (THGENAME TE-G)))))
	     ((SETQ THMNAME (CAR THX)) (SETQ THMBODY (CDR THX))))      ;THNOOASSERT FEATURE
       (COND ((EQ (CAR THMBODY) (QUOTE THNOASSERT))
	      (SETQ THNOASSERT? T)
	      (SETQ THMBODY (CDR THMBODY))))
       (THPUTPROP THMNAME (CONS THMTYPE THMBODY) (QUOTE THEOREM))
       (COND
	(THNOASSERT?
	 (PRINT (LIST THMNAME 'DEFINED 'BUT 'NOT 'ASSERTED)))
	((THASS1 (LIST THMNAME) T)
	 (PRINT (LIST THMNAME 'DEFINED 'AND 'ASSERTED)))
	(T (PRINT (LIST THMNAME 'REDEFINED))))
       (RETURN T)))

(DECLARE (SPECIAL THTREE THEXP))

(DEFUN THDO
       FEXPR
       (A)
       (OR (NOT A)
	   (PROG2 (THPUSH THTREE (LIST (QUOTE THDO) A NIL NIL))
		  (SETQ THEXP (CAR A)))))

(DECLARE (UNSPECIAL THTREE THEXP))

(DECLARE (SPECIAL THTREE THEXP THBRANCH THABRANCH))

(DEFUN THDO1
       NIL
       (RPLACA (CDAR THTREE) (CDADAR THTREE))
       (SETQ THEXP (CAADAR THTREE))
       (COND (THBRANCH (RPLACA (CDDAR THTREE)
			       (CONS THBRANCH (CADDAR THTREE)))
		       (SETQ THBRANCH NIL)
		       (RPLACA (CDDDAR THTREE)
			       (CONS THABRANCH
				     (CAR (CDDDAR THTREE)))))))

(DECLARE (UNSPECIAL THTREE THEXP THBRANCH THABRANCH))

(DECLARE (SPECIAL THTREE))
(DEFUN THDOB NIL (COND ((OR THMESSAGE (NULL (CDADAR THTREE)))
			(RPLACA (CAR THTREE) (QUOTE THUNDO))
			T)
		       ((THDO1))))

(DECLARE (UNSPECIAL THTREE))

(DEFUN THDUMP
       FEXPR
       (THFILE)
       (APPLY 'UWRITE (COND (THFILE (CDDR THFILE))))
       (IOC R)
       (THSTATE)
       (APPLY 'UFILE THFILE))

(DEFUN THERASE FEXPR (THA) (THASS1 THA NIL))

(DECLARE (SPECIAL THTREE))

(DEFUN THERASEF
       NIL
       (THADD (COND ((ATOM (CADAR THTREE)) (CADAR THTREE))
		    (T (CAADAR THTREE)))
	      (COND ((ATOM (CADAR THTREE)) NIL) (T (CDADAR THTREE))))
       (THPOPT)
       NIL)

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THTREE))

(DEFUN THERASET NIL (PROG2 0. (CADAR THTREE) (THPOPT)))

(DECLARE (UNSPECIAL THTREE))

(COMMENT THERASING DEFINES AND OPTIONALLY ASSERTS ERASING THEOREMS)

(DEFUN THERASING FEXPR (THX) (THDEF (QUOTE THERASING) THX))

(DECLARE (SPECIAL THINF THTREE THMESSAGE))
(DEFUN THFAIL
       FEXPR
       (THA)
       (AND THA
	    (PROG (THTREE1 THA1 THX)
	     F	  (SETQ THA1 (COND ((EQ (CAR THA) (QUOTE THEOREM))
				    (QUOTE THPROG))
				   ((EQ (CAR THA) (QUOTE THTAG))
				    (QUOTE THPROG))
				   ((EQ (CAR THA) (QUOTE THINF))
				    (SETQ THINF T)
				    (RETURN NIL))
				   ((EQ (CAR THA) (QUOTE THMESSAGE))
				    (SETQ THMESSAGE (CADR THA))
				    (RETURN NIL))
				   (T (CAR THA))))
		  (SETQ THTREE1 THTREE)
	     LP1  (COND ((NULL THTREE1)
			 (PRINT THA)
			 (COND ((ATOM (SETQ THA (THERT NOT
						       FOUND
						       -
						       THFAIL)))
				(RETURN THA))
			       (T (GO F))))
			((EQ (CAAR THTREE1) THA1) (GO ELP1)))
	     ALP1 (SETQ THTREE1 (CDR THTREE1))
		  (GO LP1)
	     ELP1 (COND ((EQ (CAR THA) (QUOTE THTAG))
			 (COND ((MEMQ (CADR THA)
				      (CADDDR (CAR THTREE1)))
				(GO TAGS))
			       (T (GO ALP1)))))
		  (SETQ THMESSAGE (LIST (CDR THTREE1)
					(AND (CDR THA) (CADR THA))))
		  (RETURN NIL)
	     TAGS (SETQ THX (CADDAR THTREE1))
	     LP2  (COND ((NULL THX) (GO ALP1))
			((EQ (CAADDR (CAR THX)) (CADR THA))
			 (SETQ THMESSAGE
			       (LIST (CAAR THX)
				     (AND (CDDR THA) (CADDR THA))))
			 (RETURN NIL)))
		  (SETQ THX (CDR THX))
		  (GO LP2))))

(DECLARE (UNSPECIAL THINF THTREE THMESSAGE))

(DECLARE (SPECIAL THTREE THVALUE))

(DEFUN THFAIL?
       (PRD ACT)
       (THPUSH THTREE (LIST (QUOTE THFAIL?) PRD ACT))
       THVALUE)

(DECLARE (UNSPECIAL THTREE THVALUE))

(DECLARE (SPECIAL THTREE THMESSAGE))
(DEFUN THFAIL?F NIL (COND ((EVAL (CADAR THTREE))
			   (EVAL (PROG2 (SETQ THMESSAGE NIL)
				  (CADDAR THTREE)
				  (THPOPT))))
			  (T (THPOPT) NIL)))

(DECLARE (UNSPECIAL THTREE THMESSAGE))

(DECLARE (SPECIAL THVALUE))

(DEFUN THFAIL?T NIL (THPOPT) THVALUE)

(DECLARE (UNSPECIAL THVALUE) (SPECIAL THTREE))

(DEFUN THFINALIZE
       FEXPR
       (THA)
       (PROG (THTREE1 THT THX)
	     (COND ((NULL THA)
		    (SETQ THA (THERT BAD CALL - THFINALIZE))))
	     (COND ((ATOM THA) (RETURN THA))
		   ((EQ (CAR THA) (QUOTE THTAG))
		    (SETQ THT (CADR THA)))
		   ((EQ (CAR THA) (QUOTE THEOREM))
		    (SETQ THA (LIST (QUOTE THPROG)))))
	     (SETQ THTREE (SETQ THTREE1 (CONS NIL THTREE)))
	PLUP (SETQ THX (CADR THTREE1))
	     (COND ((NULL (CDR THTREE1)) (PRINT THA)
					 (THERT OVERPOP - THFINALIZE))
		   ((AND THT
			 (EQ (CAR THX) (QUOTE THPROG))
			 (MEMQ THT (CADDDR THX)))
		    (GO RTLEV))
		   ((OR (EQ (CAR THX) (QUOTE THPROG))
			(EQ (CAR THX) (QUOTE THAND)))
		    (RPLACA (CDDR THX) NIL)
		    (SETQ THTREE1 (CDR THTREE1)))
		   ((EQ (CAR THX) (QUOTE THREMBIND))
		    (SETQ THTREE1 (CDR THTREE1)))
		   ((RPLACD THTREE1 (CDDR THTREE1))))
	     (COND ((EQ (CAR THX) (CAR THA)) (GO DONE)))
	     (GO PLUP)
	RTLEV(SETQ THX (CDDR THX))
	LEVLP(COND ((NULL (CAR THX)) (SETQ THTREE1 (CDR THTREE1))
				     (GO PLUP))
		   ((EQ (CAADDR (CAAR THX)) THT) (GO DONE)))
	     (RPLACA THX (CDAR THX))
	     (GO LEVLP)
	DONE (SETQ THTREE (CDR THTREE))
	     (RETURN T)))

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THTREE))
(DEFUN THFIND
 FEXPR
 (THA)
 (THBIND (CADDR THA))
 (THPUSH THTREE
	 (LIST (QUOTE THFIND)
	       (COND ((EQ (CAR THA) 'ALL) ' (1. NIL NIL))	       ;STANDARD ALL
		     ((NUMBERP (CAR THA))
		      (LIST (CAR THA) (CAR THA) T))		       ;SINGLE NUMBER
		     ((NUMBERP (CAAR THA)) (CAR THA))		       ;WINOGRAD CROCK FORMAT
		     ((EQ (CAAR THA) 'EXACTLY)
		      (LIST (CADAR THA) (ADD1 (CADAR THA)) NIL))
		     ((EQ (CAAR THA) 'AT-MOST)
		      (LIST 1. (ADD1 (CADAR THA)) NIL))
		     ((EQ (CAAR THA) 'AS-MANY-AS)
		      (LIST 1. (CADAR THA) T))
		     (T (CONS (CADAR THA)			       ;ONLY THING LEFT IS AT-LEAST
			      (COND ((NULL (CDDAR THA)) (LIST NIL T))  ;NO AT-MOST
				    ((EQ (CADDAR THA) 'AT-MOST)
				     (LIST (ADD1 (CAR (CDDDAR THA)))
					   NIL))
				    (T (LIST (CAR (CDDDAR THA))
					     T))))))
	       (CONS 0. NIL)
	       (CADR THA)))
 (THPUSH THTREE (LIST (QUOTE THPROG) (CDDR THA) NIL (CDDR THA)))
 (THPROGA))

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THTREE THBRANCH THXX))

(DEFUN THFINDF
       NIL
       (SETQ THBRANCH NIL)
       (COND ((OR THMESSAGE (LESSP (CAADR (SETQ THXX (CDAR THTREE)))
				   (CAAR THXX)))
	      (THPOPT)
	      NIL)
	     (T (THPOPT) (CDADR THXX))))

(DECLARE (UNSPECIAL THTREE THBRANCH THXX))

(DECLARE (SPECIAL THTREE THALIST THBRANCH THABRANCH))
(DEFUN THFINDT
       NIL
       (PROG (THX THY THZ THCDAR)
	     (SETQ THZ (CADDR (SETQ THCDAR (CDAR THTREE))))
	     (AND (MEMBER (SETQ THX (THVARSUBST THZ NIL))
			  (CDADR THCDAR))
		  (GO GO))
	     (RPLACD (CADR THCDAR) (CONS THX (CDADR THCDAR)))
	     (AND (EQ (SETQ THY (ADD1 (CAADR THCDAR))) (CADAR THCDAR))
		  (RETURN (PROG2 (SETQ THBRANCH NIL)
				 (AND (CADDAR THCDAR) (CDADR THCDAR))
				 (THPOPT))))
	     (RPLACA (CADR THCDAR) THY)
	GO   (SETQ THTREE THBRANCH)
	     (SETQ THALIST THABRANCH)
	     (SETQ THBRANCH NIL)
	     (RETURN NIL)))

(DECLARE (UNSPECIAL THTREE THALIST THBRANCH THABRANCH))

(DECLARE (SPECIAL B))
(DEFUN THFLUSH							       ;(THFLUSH) FLUSHES ALL ASSERTIONS AND THEOREMS
 FEXPR								       ;INPUT = SEQUENCE OF INDICATORS DEFAULT =
 
 ;;EFFECT = FLUSHES THE PROPERTIES OF THESE
 (A)								       ;(THASSERTION THCONSE THANTE THERASING)	 
 (MAPC								       ;INDICATORS FROM ALL ATOMS
  (FUNCTION
   (LAMBDA (B)
    (MAPC (FUNCTION (LAMBDA (C)
			    (MAPC (FUNCTION (LAMBDA (D)
						    (REMPROP D B)))
				  C)))
	  (MAKOBLIST NIL))))
  (COND (A) (' (THASSERTION THCONSE THANTE THERASING)))))

(DECLARE (UNSPECIAL B))

(DECLARE (SPECIAL THXX))

(DEFUN THGAL							       ;(THGAL $?X THALIST) RETURNS THE BINDING CELL (X
       (X Y)							       ;-) OF X ON THALIST
       (SETQ THXX X)
       (SASSQ (CADR X) Y (FUNCTION (LAMBDA NIL
					   (PRINT THXX)
					   (THERT THUNBOUND THGAL)))))

(DECLARE (UNSPECIAL THXX))

(DECLARE (SPECIAL THGENAME))

(DEFUN THGENAME
       FEXPR							       ;GENERATES UNIQUE NAME WITH ARG AS PREFIX
       (X)
       (READLIST (NCONC (EXPLODE (CAR X))
			(EXPLODE (SETQ THGENAME (ADD1 THGENAME))))))

(DECLARE (UNSPECIAL THGENAME))

(DEFUN THGO FEXPR (X) (APPLY (QUOTE THSUCCEED)
			     (CONS (QUOTE THTAG) X)))

(DECLARE (SPECIAL THTREE THTRACE THZ1 THZ THY1 THY THA2))
(DEFUN THGOAL
 FEXPR
 (THA)								       ;THA = (PATTERN RECOMMENDATION)
 (PROG (THY THY1 THZ THZ1 THA1 THA2)				       ;PATTERN IS EITHER EXPLICIT, THE VALUE OF A
       (SETQ THA2 (THVARSUBST (CAR THA) T))			       ;PLANNER VARIABLE OR THVAL OF $E... THA2 =
       (SETQ THA1 (CDR THA))					       ;INSTANTIATED PATTERN THA1 = RECOMMENDATIONS
       (COND ((OR (NULL THA1)					       ;SHOULD DATA BASE BE SEARCHED TRYED IF NO RECS
		  (AND (NOT (AND (EQ (CAAR THA1) 'THANUM)
				 (SETQ THA1
				       (CONS (LIST 'THNUM
						   (CADAR THA1))
					     (CONS (LIST 'THDBF
							 'THTRUE)
						   (CDR THA1))))))
		       (NOT (AND (EQ (CAAR THA1) (QUOTE THNODB))       ;TRIED IF REC NOT THNODB OR (THDBF PRED)
				 (PROG2 (SETQ THA1 (CDR THA1)) T)))
		       (NOT (EQ (CAAR THA1) (QUOTE THDBF)))))
	      (SETQ THA1
		    (CONS (LIST (QUOTE THDBF) (QUOTE THTRUE)) THA1))))
       (SETQ THA1 (MAPCAN (FUNCTION THTRY) THA1))		       ;THMS AND ASSERTIONS SATISFYING RECS APPENDED TO
       (AND THTRACE (THTRACES (QUOTE THGOAL) THA2))		       ;RECS
       (COND ((NULL THA1) (RETURN NIL)))
       (THPUSH THTREE (LIST (QUOTE THGOAL) THA2 THA1))		       ;(THGOAL PATTERN MATCHES)
       (RPLACD (CDDAR THTREE) 262143.)
       (RETURN NIL)))						       ;FAILS TO THGOALF

(DECLARE (UNSPECIAL THTREE THTRACE THZ1 THZ THY1 THY THA2))

(DECLARE (SPECIAL THMESSAGE))

(DEFUN THGOALF
       NIL
       
       ;;BASICALLY ALL IT DOES IS TO SEND OFF TO
       ;;THTRY1 TO TRY ANOTHER POSSIBILITY
       ;;IF THTRY1 RETURNS NIL IT MEANS THAT IT COULDN'T FIND ANOTHER
       ;;POSSIBILITY AND WE SHOULD TELL THVAL THAT WE HAVE FAILED
       ;;ALL THPOPT DOES IS TO LOB THE THGOAL ENTRY OFF THTREE
       (COND (THMESSAGE (THPOPT) NIL) ((THTRY1)) (T (THPOPT) NIL)))

(DECLARE (UNSPECIAL THMESSAGE))

(DECLARE (SPECIAL THTREE THVALUE))

(DEFUN THGOALT NIL (PROG2 0.
			  (COND ((EQ THVALUE (QUOTE THNOVAL))
				 (THVARSUBST (CADAR THTREE) NIL))
				(THVALUE))
			  (THPOPT)))

(DECLARE (UNSPECIAL THTREE THVALUE))

(DECLARE (SPECIAL THTT THFSTP THFST THTTL THLAS THNF THWH))
(DEFUN THIP
       (THI)
       
       ;;THI IS AN ITEM FROM THE ASSERTION OR PATTERN OF THE THEOREM BEING ENTERED
       (PROG (THT1 THT3 THSV THT2 THI1)
	     (SETQ THNF (ADD1 THNF))
	     
	     ;;THNF IS A FREE VARIABLE FROM THADD (WHO CALLS THIS BUGER)
	     ;;IT SAYS WE ARE LOOKING AT THE N'TH PLACE IN THE PATTERN
	     (COND ((AND (ATOM THI)
			 (NOT (EQ THI (QUOTE ?)))
			 (NOT (NUMBERP THI)))
		    
		    ;;THI1 IS THE NAME OF THE ATOM TO LOOK UNDER
		    ;;WHEN THI IS A USUAL ATOM THI1 = THI
		    ;;NUMBERS DON'T HAVE PROPERTY LISTS SO THEY DON'T COUNT
		    ;;AS NORMAL ATOMS, NOR DOES "?" SINCE IT IS A SORT OF
		    ;;VARIABLE IN PLANNER
		    (SETQ THI1 THI))
		   ((OR (EQ THI (QUOTE ?))
			(MEMQ (CAR THI) (QUOTE (THV THNV))))
		    
		    ;;SEE IF THI IS A VARIABLE
		    (COND (THFST (RETURN (QUOTE THVRB)))
			  
			  ;;IF WE ARE DOING THIS FOR THE FIRST TIME, DON'T CONSIDER VARIABLES
			  ;;FOR EXPLANATION WHY, SEE THADD
			  ((SETQ THI1 (QUOTE THVRB)))))
		   ((RETURN (QUOTE THVRB))))
	     
	     ;;OTHERWISE THI IS SOMETHING WITH NO PROPERTY LIST LIKE A NUMBER, OR LIST
	     ;;RETURNING THVRB TO THADD TELLS IT THAT EVERYTHING IS OK SO
	     ;;FAR, BUT NOTHING WAS DONE ON THIS ITEM
	     (COND ((NOT (SETQ THT1 (GET THI1 THWH)))
		    
		    ;;THWH IS THE NAME OF THE PROPERTY TO LOOK UNDER ON THE ATOM
		    ;;IF THIS PROPERTY IS NOT THERE THEN WE MUST PUT IT THERE
		    ;;IN PARTICULAR, NO PROPERTY MEANS THAT THE
		    ;;ASSERTEE HAS NEVER BEEN ASSERTED BEFORE
		    (PUTPROP THI1
			     (LIST NIL
				   (LIST THNF (LIST THLAS 1. THTTL)))
			     THWH))
		   ((EQ THT1 (QUOTE THNOHASH)) (RETURN (QUOTE THBQF)))
		   
		   ;;IF THE PROPERTY IS "THNOHASH" IT MEANS THAT WE
		   ;;SHOULD NOT BOTHER TO INDEX UNDER THIS ATOM, SO
		   ;;JUST RETURN TO THADD
		   ((NOT (SETQ THT2 (ASSQ THNF (CDR THT1))))
		    
		    ;;LOOK ON THE PROPERTY LIST ENTRY TO SEE
		    ;;IF THERE IS A SUB-ENTRY FOR PATTERNS WITH THIS ATOM 		;;IN THE THNF'TH POSITION
		    ;;IF NOT, HACK THE ENTRY SO THERE IS.
		    ;;AGAIN THIS IMPLIES THAT THE ASSERTEE HAS NEVER
		    ;;BEEN ASSERTED BEFORE
		    (NCONC THT1
			   (LIST (LIST THNF (LIST THLAS 1. THTTL)))))
		   ((NOT (SETQ THT3 (ASSQ THLAS (CDR THT2))))
		    
		    ;;NOW LOOK WITHIN THE SUB-ENTRY FOR A SUB-SUB-ENTRY.
		    ;;I.E. THOSE PATTERNS WHICH ARE ALSO OF THE CORRECT 
		    ;;TOTAL LENGTH
		    ;;THLAS IS A VARIABLE FROM THADD WHICH GIVES THE
		    ;;LENGTH OF THE ASSERTEE
		    ;;AGAIN, IF NOT THERE, HACK IT IN
		    (NCONC THT2 (LIST (LIST THLAS 1. THTTL))))
		   ((AND (OR THFST THFSTP)
			 
			 ;;THIS BRANCH SAYS THAT WE STILL NEED
			 ;;TO CHECK THAT THE ASSERTEE HAS
			 ;;NEVER BEEN ASSERTED BEFORE
			 ;;THIS MEANS THAT WE MUST LOOK DOWN THE REMAINING
			 ;;SUB-SUB-BUCKET LOOKING FOR THE ASSERTEE
			 (COND ((EQ THWH (QUOTE THASSERTION))
				(ASSOC THTT (CDDR THT3)))
			       
			       ;;RANDOMNESS DUE TO THE FACT THAT ASSERTIONS
			       ;;HAVE PROPERY LIST ON THEM, WHILE THEOREM NAMES
			       ;;ARE ATOMS WHOES PROPERTY LISTS ARE OF THE
			       ;;USUAL "INVISIBLE" VARIETY
			       (T (MEMQ THTT (CDDR THT3)))))
		    
		    ;;IF THE ASSERTEE IS FOUND RETURN NIL
		    ;;INDICATING FAILURE
		    (RETURN NIL))
		   ((SETQ THSV (CDDR THT3))
		    
		    ;;HACK IN THE LATEST ENTRY INTO THE SUB-SUB-BUCKET
		    (RPLACA (CDR THT3) (ADD1 (CADR THT3)))
		    (RPLACD (CDR THT3) (NCONC (LIST THTTL) THSV))))
	     
	     ;;IF WE GET TO THIS POINT EVERYTHING
	     ;;IS OK SO TELL THADD SO
	     (RETURN (QUOTE THOK))))

(DECLARE (UNSPECIAL THTT THFST THFSTP THTTL THLAS THNF THWH))

(DECLARE (SPECIAL THOLIST THALIST THX THY))
(DEFUN THMATCH2
 
 ;;THX IS ONE ITEM FROM THE PATTERN
 ;;THY IS THE CORESPONDING ITEM FROM THE CANDIDATE
 ;;THMATCH2 DECIDES IF THE TWO ITEMS REALLY MATCH
 (THX THY)
 
 ;;THOLIST IS THE "THALIST" WHICH WAS IN EXISTANCE BEFORE
 ;;WE STARTED WORKING ON THE CURRENT LINE OF PLANNER CODE
 ;;STANDARD CHECK FOR $E
 (AND (EQ (CAR THX) (QUOTE THEV))
      (SETQ THX (THVAL (CADR THX) THOLIST)))
 (AND (EQ (CAR THY) (QUOTE THEV))
      (SETQ THY (THVAL (CADR THY) THALIST)))
 (COND
  
  ;;IF EITHER IS A ? ANYTHING WILL MATCH, SO OK
  ((EQ THX (QUOTE ?)))
  ((EQ THY (QUOTE ?)))
  
  ;;IF EITHER IS A VARIABLE THINGS GET MESSY.
  ;;  EVERYTHING DOWN TO ***** IS
  ;;CONCERNED WITH THIS CASE
  ((OR (MEMQ (CAR THX) (QUOTE (THV THNV THRESTRICT)))
       (MEMQ (CAR THY) (QUOTE (THV THNV THRESTRICT))))
   ((LAMBDA (XPAIR YPAIR)
     
     ;;X AND Y PAIR ARE THE RESPECTIVE BINDING CELLS WHICH
     ;;WILL HAVE ANY NEW RESTRICTIONS MENTIONED.  IF THX OR
     ;;THY IS NOT A VARIABLE (I.E. THE OTHER IS ) THEN X OR Y PAIR WILL
     ;;BE NIL
     (COND ((AND XPAIR
		 
		 ;;THX IS A VARIABLE
		 ;;THIS SEES IF THX IS UNASSIGNED
		 (OR (EQ (CAR THX) (QUOTE THNV))
		     (AND (EQ (CAR THX) (QUOTE THV))
			  (EQ (CADR XPAIR) (QUOTE THUNASSIGNED))))
		 
		 ;;THCHECK MACKES SURE THE RESTRICTIONS (IF ANY) ON
		 ;;THX ARE COMPATIBLE WITH THY
		 (THCHECK (CDDR XPAIR)
			  (COND (YPAIR (CADR YPAIR)) (T THY))))
	    
	    ;;FURTHERMORE, THY IS ALSO A VARIABLE
	    ;;THIS MEANS WE MUST DO THE MYSTERIOUS VARIABLE LINKING
	    (COND (YPAIR (THRPLACAS (CDR XPAIR) (CADR YPAIR))
			 
			 ;;IF THY ALSO HAS RESTRICTIONS, WHEN WE
			 ;;LINK VARIABLES WE COMBINE RESTRICTIONS
			 (AND (CDDR YPAIR)
			      (THRPLACDS (CDR XPAIR)
					 (THUNION (CDDR XPAIR)
						  (CDDR YPAIR))))
			 (THRPLACDS YPAIR (CDR XPAIR)))
		  
		  ;;IF THY IS NOT A VARIALBE, JUST ASSIGN THX TO THY
		  ;;THRPLACAS WILL HACK THML THE FREE VARIABLE FROM THMATCH1
		  (T (THRPLACAS (CDR XPAIR) THY))))
	   
	   ;;IN THIS COND PAIR THY IS A VARIABLE AND THX IS EITHER
	   ;;A CONSTANT OR A PREVIOUSLY ASSIGNED VARIALBE
	   ((AND YPAIR
		 (OR (EQ (CAR THY) (QUOTE THNV))
		     
		     ;;FURTHERMORE THY IS UNASSIGNED
		     (AND (EQ (CAR THY) (QUOTE THV))
			  (EQ (CADR YPAIR) (QUOTE THUNASSIGNED))))
		 
		 ;;MAKE SURE RESTRICTIONS ARE OK
		 (THCHECK (CDDR YPAIR)
			  (COND (XPAIR (CADR XPAIR)) (T THX))))
	    
	    ;;IF THX IS A VARIABLE, LINK
	    (COND (XPAIR (THRPLACAS (CDR YPAIR) (CADR XPAIR)))
		  
		  ;;OTHERWISE JUST ASSIGN THY TO THX
		  (T (THRPLACAS (CDR YPAIR) THX))))
	   
	   ;;THX IS AN ASSIGED VARIABLE, SO JUST MAKE
	   ;;SURE ITS ASSIGNEMENT IS EQUAL TO THY
	   ((AND XPAIR (EQUAL (CADR XPAIR)
			      (COND (YPAIR (CADR YPAIR)) (T THY)))))
	   
	   ;;THX IS A CONSTANT, THY IS A VARIABLE, AND THEY ARE EQUAL
	   ((AND YPAIR (EQUAL (CADR YPAIR) THX)))
	   
	   ;;LOOSE, SO RETURN WITH AN ERROR
	   (T (ERR NIL))))
    
    ;;
    ;;THE FOLLOWING TWO CONDS BIND XPAIR AND YPAIR RESPECTIVELY
    ;;
    (COND ;;IF THX IS A NORMAL VARIALBE, IN PARTICULAR
	  ;;WE ARE NOT INTRODUCING NEW RESTRICTIONS AT THIS TIME,
	  ;;THEN X PAIR IS JUST THE BINDING LIST
	  ((THVAR THX) (THGAL THX THOLIST))
	  
	  ;;WE MUST HACK A NEW RESTRICTION ONTO THE
	  ;;BINDING LIST
	  ((EQ (CAR THX) (QUOTE THRESTRICT))
	   
	   ;;WE ARE "RESTRICTING" A ?.  SINCE ? HAS NO
	   ;;BINDING LIST, WE MAKE UP A PSEUDO BINDING LIST
	   (COND ((EQ (CADR THX) (QUOTE ?))
		  (PROG2 0.
			 (CONS (QUOTE ?)
			       (CONS (QUOTE THUNASSIGNED)
				     (APPEND (CDDR THX) NIL)))
			 (SETQ THX (QUOTE (THNV ?)))))
		 
		 ;;WE ARE RESTRICTING A VARIABLE.  THIS MEANS THAT
		 ;;WE MUST PUT IN ON THE BINDING LIST
		 (T ((LAMBDA (U)
			     (THRPLACDS (CDR U)
					
					;;THUNION MAKES SURE WE DON'T PUT THE SAME RESTRICTION ON TWICE
					(THUNION (CDDR U) (CDDR THX)))
			     (SETQ THX (CADR THX))
			     U)
		     (THGAL (CADR THX) THOLIST))))))
    
    ;;NOTE THAT IF THX IS NOT A VARIABLE THEN XPAIR IS ()
    ;;
    ;;WE DO THE EXACT SAME THING FOR THY AS WE JUST DID FOR THX
    ;;
    (COND ((THVAR THY) (THGAL THY THALIST))
	  ((EQ (CAR THY) (QUOTE THRESTRICT))
	   (COND ((EQ (CADR THY) (QUOTE ?))
		  (PROG2 0.
			 (CONS (QUOTE ?)
			       (CONS (QUOTE THUNASSIGNED)
				     (APPEND (CDDR THY) NIL)))
			 (SETQ THY (QUOTE (THNV ?)))))
		 (T ((LAMBDA (U)
			     (THRPLACDS (CDR U)
					(THUNION (CDDR U) (CDDR THY)))
			     (SETQ THY (CADR THY))
			     U)
		     (THGAL (CADR THY) THALIST))))))))
  
  ;;***************
  ;;IF THE TWO ARE EQUAL, NATURALLY THEY MATCH
  ((EQUAL THX THY))
  
  ;;IF NOT, THEY DON'T, SO REPORT FAILURE
  (T (ERR NIL))))

(DECLARE (UNSPECIAL THOLIST THALIST THX THY) (SPECIAL THX THPRD))

(DEFUN THCHECK
       (THPRD THX)
       (OR (NULL THPRD)
	   (EQ THX (QUOTE THUNASSIGNED))
	   (ERRSET (MAPC (FUNCTION (LAMBDA (THY)
					   (OR (THY THX) (ERR NIL))))
			 THPRD))))

(DECLARE (UNSPECIAL THX THPRD) (SPECIAL THY THX THTREE THOLIST THML))

(DECLARE (SPECIAL L2))

(DEFUN THUNION
       (L1 L2)
       (MAPC (FUNCTION (LAMBDA (THX)
			       (COND ((MEMBER THX L2))
				     (T (SETQ L2 (CONS THX L2))))))
	     L1)
       L2)

(DECLARE (UNSPECIAL L2))

(DECLARE (SPECIAL THX THALIST THOLIST))

(DEFUN THMATCH THX ((LAMBDA (THOLIST THALIST)
			    (THMATCH1 (ARG 1.) (ARG 2.)))
		    (COND ((GREATERP THX 2.) (ARG 3.)) (T THALIST))
		    (COND ((GREATERP THX 3.) (ARG 4.)) (T THALIST))))
(DEFUN THMATCH1
       
       ;;THX IS THE PATTERN TO BE MATCHED
       ;;THY IS THE POSSIBLE CANDIDATE 
       (THX THY)
       
       ;;THMATCH1 DOES PRELIMINARLY WORK BEFORE HANDING
       ;;THE PATTERN AND CANDIDATE OFF TO THMATCH2
       ;;WHO DOES THE REAL WORK
       (PROG (THML)
	     
	     ;;THML IS A FREE VARIABLE WHO WILL BE HACKED BY THMATCH2
	     ;;WHEN THMATCH2 IS DONE, THML WILL HAVE A RECORD OF ALL VARIABLE
	     ;;ASSIGNMENTS MADE DURING THE MATCH.  NATURALLY
	     ;;WE MUST KEEP TRACK SO IF WE FAIL BACK WE CAN UNDO THEM.
	     ;;WE HAVE TO CHECK THAT THE PATTERN AND CANDIDATE
	     ;;ARE OF THE SAME LENGTH SINCE THE USER MAY HAVE
	     ;;SPECIFIED THE CANDIDATE WITH A "THUSE" RECOMMENDATION
	     (COND ((AND (EQ (LENGTH (COND ((EQ (CAR THX)
						(QUOTE THEV))
					    (SETQ THX
						  (THVAL (CADR THX)
							 THOLIST)))
					   (THX)))
			     (LENGTH THY))
			 
			 ;;IF THE MATCH FAILS, THMATCH2 EXITS WITH AN ERR
			 ;;WILL BE "TRUE" PROVIDED THE MATCH WORKED
			 (ERRSET (MAPC (FUNCTION THMATCH2) THX THY)))
		    
		    ;;SO RECORD THE ASSIGNMENTS ON THTREE
		    (AND THML
			 (THPUSH THTREE (LIST (QUOTE THMUNG) THML)))
		    (RETURN T))
		   
		   ;;IF THE MATCH FAILED, WE MAY STILL HAVE
		   ;;SOME ASSIGNEMENTS ALREADY MADE.  THESE
		   ;;MUST IMMEDIATELY BE UNDONE.  EVLIS JUST EVALS
		   ;;EVERYTHING ON THML WHICH IS A LIST OF EXPRESSIONS
		   ;;WHICH, WHEN EVALED, UNASSIGN THE VARIABLES
		   (T (EVLIS THML) (RETURN NIL)))))

(DECLARE (UNSPECIAL THY THX THTREE THOLIST THML))

(DECLARE (SPECIAL THNF THWH THALIST))
(DEFUN THMATCHLIST
       (THTB THWH)
       
       ;;THTB IS A PATTERN WHICH EVENTUALLY IS TO BE MATCHED
       ;;THWH SAYS IF IT IS AN ASSERTION, CONSEQUENT THEOREM, ETC.
       ;;THMATCHLIST GOES THROUGH THE DATA BASE, LOOKING ON ALL
       ;;THE BUCKETS OF THE ATOMS IN THE PATTERN
       ;;IT RETURNS THE SHORTEST BUCKET TO THGOAL
       (PROG (THB1 THB2 THL THNF THAL THA1 THA2 THRN THL1 THL2 THRVC)
	     (SETQ THL 34359738367.)
	     
	     ;;THL IS THE LENGTH OF THE SHORTEST BUCKET FOUND SO FAR
	     ;;INITIALLY IT IS SET TO A VERY LARGE NUMBER
	     (SETQ THNF 0.)
	     
	     ;;COUNTER WHICH SAYS WHICH PATTERN ITEM WE ARE WORKING ON
	     (SETQ THAL (LENGTH THTB))
	     
	     ;;LENGTH OF PATTERN
	     (SETQ THB1 THTB)
	     
	     ;;THB1 WILL BE THE REMAINDER OF THE PATTERN TO YET BE WORKED ON
	     ;;WHEN IT IS NIL, WE ARE DONE
	     ;;SO RETURN THE BUCKET.  THL1 IS THE BUCKET UNDER THE ATOM
	     ;;THL2 IS THE BUCKET UNDER THE VARIABLE IN THAT POSITION
	     ;;IF WE ARE WORKING ON AN ASSERTION, THL2 WILL BE () SINCE
	     ;;THERE ARE NO VARIABLES IN ASSERTIONS
	     ;;IN THEOREMS, WE MUST TAKE INTO ACCOUNT THE FACT THAT
	     ;;THE THEOREM MAY HAVE EITHER THE CORRECT ATOM, OR A
	     ;;VARIALBE IN A GIVEN POSITION, AND STILL MATCH
	THP1 (OR THB1
		 (RETURN (COND (THL2 (APPEND THL1 THL2)) (THL1))))
	     
	     ;;ADD1 TO POSITION COUNTER
	     (SETQ THNF (ADD1 THNF))
	     
	     ;;THB2 IS THE ITEM WE ARE WORKING ON IN THIS PASS
	     (SETQ THB2 (CAR THB1))
	     
	     ;;UPDATE THB1
	     (SETQ THB1 (CDR THB1))
	THP3 (COND ((OR (NULL (ATOM THB2))
			
			;;IF THE ITEM IS NOT A NORMAL ATOM, SKIP IT AND
			;;GO TO NEXT PASS
			(NUMBERP THB2)
			(EQ THB2 (QUOTE ?)))
		    (GO THP1))
		   
		   ;;IF THE ITEM DOES NOT HAVE THE PROPERTY ON ITS PROPERTY
		   ;;LIST, THEN IT OBVIOUSLY DOSEN'T HAVE ANY BUCKET AT ALL
		   ;;SO THA1, WHICH RECORDS THE NUMBER IN THE BUCKET IS SET TO 0
		   ((NOT (SETQ THA1 (GET THB2 THWH)))
		    
		    ;;IF A BUCKET IS FOUND, THE FIRST THING
		    ;;IN THE BUCKET WILL BE THE NUMBER OF GOODIES THERE
		    ;;THE REST WILL BE THE GOODIES.  THE FIRST 0 IN THA1
		    ;;THEN SAYS THAT THERE WAS NO BUCKET.  THE SECOND
		    ;;0 IS JUST A DUMMY FOR THE GOODIES WHICH ARN'T THERE
		    (SETQ THA1 (QUOTE (0. 0.))))
		   
		   ;;IF IT IS A THNOHASH WE IGNOR IT JUST LIKE
		   ;;A LIST, OR NUMBER
		   ((EQ THA1 (QUOTE THNOHASH)) (GO THP1))
		   
		   ;;SAME IF THERE IS NO SUB-BUCKET FOR THE ATOM
		   ;;IN THE CORRECT POSITION
		   ((NOT (SETQ THA1 (ASSQ THNF (CDR THA1))))
		    (SETQ THA1 (QUOTE (0. 0.))))
		   
		   ;;SAME FOR SUB-SUB-BUCKET (PATTERN LENGTH)
		   ((NOT (SETQ THA1 (ASSQ THAL (CDR THA1))))
		    (SETQ THA1 (QUOTE (0. 0.)))))
	     (SETQ THRN (CADR THA1))
	     (SETQ THA1 (CDDR THA1))
	     
	     ;;IF ITS AN ASSERTION, THEN WE DONT HAVE TO LOOK FOR VARIABLES
	     (AND (EQ THWH (QUOTE THASSERTION)) (GO THP2))
	     
	     ;;THVRB IS THE ATOM WHICH HAS THE BUCKET FOR VARIABLES
	     ;;WE WILL NOW LOOK TO SEE IF THERE ARE ANY THEOREMS WHICH
	     ;;HAVE A VARIABLE IN THE CORRECT POSSITION
	     (COND ((NOT (SETQ THA2 (GET (QUOTE THVRB) THWH)))
		    (SETQ THA2 (QUOTE (0. 0.))))
		   ((NOT (SETQ THA2 (ASSQ THNF (CDR THA2))))
		    (SETQ THA2 (QUOTE (0. 0.))))
		   ((NOT (SETQ THA2 (ASSQ THAL (CDR THA2))))
		    (SETQ THA2 (QUOTE (0. 0.)))))
	     (SETQ THRVC (CADR THA2))
	     (SETQ THA2 (CDDR THA2))
	     
	     ;;SEE IF THE SUM OF THE NUMBER OF GOODIES IN THE ATOM BUCKET PLUS
	     ;;THE NUMBER IN THE VARIABLE BUCKET IS GREATER THAN THE SMALLEST
	     ;;NUMBER SO FAR.  IF SO WE KEEP THE PREVIOUS NUMBER
	     (AND (GREATERP (PLUS THRVC THRN) THL) (GO THP1))
	     
	     ;;OTHERWISE THIS BECOMES THE NEW SMALLEST
	     (SETQ THL (PLUS THRVC THRN))
	     
	     ;;AND THL1 AND THL2 ARE POINTERS TO THE NEWLY DISCOVERD BUCKETS
	     (SETQ THL1 THA1)
	     (SETQ THL2 THA2)
	     
	     ;;GO BACK FOR ANOTHER PASS
	     (GO THP1)
	     
	     ;;THIS SECTION IS FOR ASSERTIONS, I.E., DON'T HAVE TO CONSIDER VARIABLES
	THP2 (COND 
		   ;;IF THERE IS NO BUCKET THEN RETURN SINCE NOTHING WILL MATCH THE
		   ;;PATTERN
		   ((EQ THRN 0.) (RETURN NIL))
		   
		   ;;IF THE NEW BUCKET IS SMALLER, IT BECOMES THE SMALLEST SO FAR
		   ((GREATERP THL THRN) (SETQ THL1 THA1)
					(SETQ THL THRN)))
	     
	     ;;GO BACK FOR ANOTHER PASS
	     (GO THP1)))

(DECLARE (UNSPECIAL THNF THWH THALIST))

(DECLARE (SPECIAL THTREE THVALUE))

(DEFUN THMESSAGE
       FEXPR
       (THA)
       (THPUSH THTREE (CONS 'THMESSAGE THA))
       THVALUE)

(DECLARE (UNSPECIAL THTREE THVALUE))

(DECLARE (SPECIAL THALIST THOLIST THTREE THMESSAGE))

(DEFUN THMESSAGEF NIL (PROG (BOD)
			    (SETQ BOD (CAR THTREE))
			    (THPOPT)
			    (COND ((AND (THBIND (CADR BOD))
					(THMATCH1 (CADDR BOD)
						  THMESSAGE))
				   (THPUSH THTREE (LIST (QUOTE THPROG)
							(CDDR BOD)
							NIL
							(CDDR BOD)))
				   (SETQ THMESSAGE NIL)
				   (RETURN (THPROGA)))
				  (T (SETQ THALIST THOLIST) ))
			    (RETURN NIL)))

(DECLARE (UNSPECIAL THALIST THOLIST THTREE THMESSAGE))

(DECLARE (SPECIAL THVALUE))

(DEFUN THMESSAGET NIL (THPOPT) THVALUE)

(DECLARE (UNSPECIAL THVALUE))

(DECLARE (SPECIAL THTREE))

(DEFUN THMUNGF NIL (EVLIS (CADAR THTREE)) (THPOPT) NIL)

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THVALUE))

(DEFUN THMUNGT NIL (THPOPT) THVALUE)

(DECLARE (UNSPECIAL THVALUE))

(DEFUN THNOFAIL (THX) (COND (THX (DEFPROP THPROG THPROGT THFAIL))
			    (T (DEFPROP THPROG THPROGF THFAIL))))

(DECLARE (SPECIAL THA))
(DEFUN THNOHASH
       FEXPR
       (THA)
       (MAPC (FUNCTION (LAMBDA (X) (PUTPROP (CAR THA)
					    (QUOTE THNOHASH)
					    X)))
	     (OR (CDR THA)
		 (QUOTE (THASSERTION THCONSE THANTE THERASING)))))

(DECLARE (UNSPECIAL THA))

(DECLARE (SPECIAL THEXP))

(DEFUN THNOT FEXPR (THA) (SETQ THEXP
			       (LIST (QUOTE THCOND)
				     (LIST (CAR THA)
					   (QUOTE (THFAIL THAND)))
				     (QUOTE ((THSUCCEED))))))

(DECLARE (UNSPECIAL THEXP))

(DEFUN THNV FEXPR (X) (THV1 (CAR X)))

(DECLARE (SPECIAL THTREE THEXP))

(DEFUN THOR FEXPR (THA) (AND THA
			     (THPUSH THTREE (LIST (QUOTE THOR) THA))
			     (SETQ THEXP (CAR THA))))

(DECLARE (UNSPECIAL THTREE THEXP))

(DECLARE (SPECIAL THTREE THEXP))

(DEFUN THOR2 (P) (COND (THMESSAGE (THPOPT) NIL)
		       ((AND (CADAR THTREE) (CDADAR THTREE))
			(RPLACA (CDAR THTREE) (CDADAR THTREE))
			(SETQ THEXP (COND (P (PROG2 0.
						    (CAADAR THTREE)
						    (OR (CADAR THTREE)
							(THPOPT))))
					  ((CAR (CAADAR THTREE))))))
		       (T (THPOPT) NIL)))

(DECLARE (UNSPECIAL THTREE THEXP))

(DEFUN THORF NIL (THOR2 T))

(DECLARE (SPECIAL THVALUE))

(DEFUN THORT NIL (THPOPT) THVALUE)

(DECLARE (UNSPECIAL THVALUE))

(DECLARE (SPECIAL THTREE))

(DEFUN THPOPT NIL (SETQ THTREE (CDR THTREE)))

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THTREE))

(DEFUN THPROG
       FEXPR
       (THA)
       
       ;;THBIND HACKS THALIST TO BIND THE VARIABLES
       ;;IT ALSO HACKS THTREE SO WE CAN UNDO IT IF NEEDED
       (THBIND (CAR THA))
       
       ;;PUT THPROG MARK ON THTREE
       ;;THE FIRST THA IS A POINTER ONE BEFORE
       ;;THE NEXT PART OF THE THPROG TO BE HANDELED
       ;;THE SECOND ONE WILL BE KEPT WHOLE TO SEARCH FOR PROG TAGS
       (THPUSH THTREE (LIST (QUOTE THPROG) THA NIL THA))
       
       ;;CALL WORKHORSE
       (THPROGA))

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THEXP THVALUE THTREE))

(DEFUN THPROGA
       NIL
       ((LAMBDA (X) (COND 
			  ;;ODD CASE WHERE THE THPROG HAS NO SUBEXPRESSIONS
			  ;;RETURN SUCCESS
			  ((NULL (CDAR X)) (THPOPT) (QUOTE THNOVAL))
			  
			  ;;NEXT ITEM IS AN ATOM, HENCE A THPROG TAG
			  ((ATOM (CADAR X))
			   
			   ;;USE THEXP TO MARK IT ON THTREE
			   (SETQ THEXP (LIST (QUOTE THTAG) (CADAR X)))
			   
			   ;;MOVE POINTER TO NEXT EXPRESSION
			   (RPLACA X (CDAR X))
			   THVALUE)
			  
			  ;;OTHERWISE NEXT EXPRESSION TO BE EVALUATED IS
			  ;;THE NEXT EXPRESSION OF THE THPROG
			  (T (SETQ THEXP (CADAR X))
			     
			     ;;MOVE POINTER TO NEXT EXPRESSION
			     (RPLACA X (CDAR X))
			     THVALUE)))
	(CDAR THTREE)))

(DECLARE (UNSPECIAL THEXP THVALUE THTREE))


;;THBRANCH AND THBRANCHUN ARE THE MAIN FUNCTIONS
;;IN CHARGE OF HANDELING THE EFFECTS OF SUCCESS AND FAILURE
;;THEY ARE ONLY CALLED BY THPROGT AND F

(DEFUN THPROGF NIL (THBRANCHUN) NIL)

(DEFUN THPROGT NIL (THBRANCH) (THPROGA))

(DECLARE (SPECIAL XX))

(DEFUN THPURE
       
       ;;CHECKS TO MAKE SURE THAT THE PATTERN HAS NO
       ;;UNASSIGNED VARIABLES IN IT.
       (XX)
       
       ;;XX, NATURALLY ENOUGH IS THE PATTERN
       ;;SINCE THPURE IS ALWAYS CALLED AFTER THVARSUBST
       ;;ANY VARIABLES WHICH DO HAVE ASSIGNMENTS WILL HAVE
       ;;GONE AWAY, RREPLACED BY THEIR ASSIGNMENTS
       ;;SO ALL WE NEED DO IS LOOK FOR ANY VARIABLES APPEARING AT ALL
       (ERRSET (MAPC (FUNCTION (LAMBDA (Y) (AND (THVAR Y) (ERR NIL))))
		     XX)))

(DECLARE (UNSPECIAL XX))

(DECLARE (SPECIAL THTREE))

(DEFUN THPUTPROP
       (ATO VAL IND)
       (THPUSH THTREE
	       (LIST (QUOTE THMUNG)
		     (LIST (LIST (QUOTE PUTPROP)
				 (LIST (QUOTE QUOTE) ATO)
				 (LIST (QUOTE QUOTE) (GET ATO IND))
				 (LIST (QUOTE QUOTE) IND)))))
       (PUTPROP ATO VAL IND))

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THBS THON THAL THFST THNF THWH))

(DECLARE (SPECIAL THFSTP))

(DECLARE (SPECIAL THPC))
(DEFUN THREM1
       
       ;;THIS FUNCTION IS ROUGHLY THE SAME AS
       ;;THIP, EXCEPT WHILE THIP ADDS ASSERTIONS TO THE
       ;;DATABASE, THREM1 REMOVES THEM
       ;;HENCE ALL COMMENTS WILL BE GUIDES TO
       ;;THE CORRESPONDENCE BETWEEN THREM1 AND THIP
       (THB)
       
       ;;THB = THI IN THIP
       (PROG (THA THSV THA1 THA2 THA3 THA4 THA5 THONE THPC)
	     
	     ;;THA AND THA1 DO THE WORK OF THT1 IN THIP
	     ;;THA1 = THT2
	     ;;THA3 = THT3
	     ;;THA4,5 , THONE, AND THPC ARE NEW
	     (SETQ THNF (ADD1 THNF))
	     
	     ;;THIS COND SERVES THE SAME PURPOSE AS THE
	     ;;FIRST COND IN THIP
	     (COND ((AND (ATOM THB)
			 (NOT (EQ THB (QUOTE ?)))
			 (NOT (NUMBERP THB)))
		    (SETQ THA THB))
		   ((OR (EQ THB (QUOTE ?))
			(MEMQ (CAR THB) (QUOTE (THV THNV))))
		    (COND (THFST (RETURN (QUOTE THVRB)))
			  ((SETQ THA (QUOTE THVRB)))))
		   ((RETURN (QUOTE THVRB))))
	     
	     ;;ALL THE REST SERVES THE SAME PURPOSE AS THE
	     ;;SECOND COND IN THIP IT WAS ORRIGINALLY
	     ;;WRITTEN AS A SINGLE COND, BUT THE
	     ;;COMPILER BARFED ON IT SO IT
	     ;;WAS BROKEN UP INTO BITE SIZE PIECES
	     (SETQ THA1 (GET THA THWH))
	     (OR THA1 (RETURN NIL))
	     (AND (EQ THA1 (QUOTE THNOHASH)) (RETURN (QUOTE THBQF)))
	     (SETQ THA2 (THBA THNF THA1))
	     (OR THA2 (RETURN NIL))
	     (SETQ THA3 (THBA THAL (CADR THA2)))
	     (OR THA3 (RETURN NIL))
	     (SETQ THA4 (CADR THA3))
	     (SETQ THPC (NOT (EQ THWH (QUOTE THASSERTION))))
	     (SETQ THA5
		   (COND ((OR THFST THFSTP) (THBAP THBS (CDR THA4)))
			 ((THBA (COND (THPC THON) (T (CAR THON)))
				(CDR THA4)))))
	     (OR THA5 (RETURN NIL))
	     (SETQ THONE (CADR THA5))
	     (RPLACD THA5 (CDDR THA5))
	     (AND (NOT (EQ (CADR THA4) 1.))
		  (OR (SETQ THSV (CDDR THA4)) T)
		  (RPLACA (CDR THA4) (SUB1 (CADR THA4)))
		  (RETURN THONE))
	     (SETQ THSV (CDDR THA3))
	     (RPLACD THA3 THSV)
	     (AND (CDADR THA2) (RETURN THONE))
	     (SETQ THSV (CDDR THA2))
	     (RPLACD THA2 THSV)
	     (AND (CDR THA1) (RETURN THONE))
	     (REMPROP THA THWH)
	     (RETURN THONE)))

(DECLARE (UNSPECIAL THPC THBS THON THAL THFST THFSTP THNF THWH))

(DECLARE (SPECIAL THALIST THTREE))

(DEFUN THREMBINDF NIL (SETQ THALIST (CADAR THTREE)) (THPOPT) NIL)

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THTREE THVALUE))

(DEFUN THREMBINDT NIL (SETQ THALIST (CADAR THTREE)) (THPOPT) THVALUE)

(DECLARE (UNSPECIAL THALIST THTREE THVALUE))

(DECLARE (SPECIAL THBS THON THAL THFSTP THFST THNF THWH))
(DEFUN THREMOVE
       
       ;;THIS FUNCTION IS ANALAGOUS TO THADD EXCEPT
       ;;THREMOVE REMOVES RATHER THAN ADDS
       ;;AS WITH THREM1, ALL COMMENTS WILL EXPLICATE THE ANALOGY
       ;;SO ONE SHOULD FIRST BECOME FAMILIAR WITH THADD
       (THB)
       
       ;;THB = THTT IN THADD, THREMOVE TAKES ONLY ONE
       ;;ARG SINCE THE PROPERTY LIST FOR THE ASSERTION PLAYS NO ROLE
       ;;IN REMOVING THE ASSERTION
       (PROG (THB1 THWH THNF THAL THON THBS THFST THFSTP THFOO)
	     
	     ;;THB1 AND THON TOGETHER SHARE THE WORK OF THT1 AND THCK IN THADD
	     ;;THAL = THLAS
	     ;;THBS = THTTL
	     (SETQ THNF 0.)
	     
	     ;;THE STRUCTURE OF THE TWO PROGRAMS IS VIRTUALLY IDENTICAL
	     (SETQ THB1
		   (COND ((ATOM THB)
			  (SETQ THBS THB)
			  (SETQ THWH
				(CAR (SETQ THB1
					   (GET THB
						(QUOTE THEOREM)))))
			  (CADDR THB1))
			 ((SETQ THWH (QUOTE THASSERTION))
			  (SETQ THBS THB))))
	     (SETQ THAL (LENGTH THB1))
	     (SETQ THFST T)
	THP1 (COND ((NULL THB1) (SETQ THB1 THFOO)
				(SETQ THNF 0.)
				(SETQ THFST (SETQ THFOO NIL))
				(SETQ THFSTP T)
				(GO THP1))
		   ((NULL (SETQ THON (THREM1 (CAR THB1))))
		    (RETURN NIL))
		   ((MEMQ THON (QUOTE (THBQF THVRB)))
		    (SETQ THFOO
			  (NCONC THFOO
				 (LIST (COND ((EQ THON (QUOTE THVRB))
					      (CAR THB1))))))
		    (SETQ THB1 (CDR THB1))
		    (GO THP1)))
	     (SETQ THFST NIL)
	     (MAPC (FUNCTION THREM1) (CDR THB1))
	     (SETQ THNF 0.)
	     (MAPC (FUNCTION THREM1) THFOO)
	     (RETURN THON)))

(DECLARE (UNSPECIAL THBS THON THAL THFST THFSTP THNF THWH))

(DECLARE (SPECIAL THTREE))
(DEFUN THREMPROP
       (ATO IND)
       (THPUSH THTREE
	       (LIST (QUOTE THMUNG)
		     (LIST (LIST (QUOTE PUTPROP)
				 (LIST (QUOTE QUOTE) ATO)
				 (LIST (QUOTE QUOTE) (GET ATO IND))
				 (LIST (QUOTE QUOTE) IND)))))
       (REMPROP ATO IND))

(DECLARE (UNSPECIAL THTREE))

(DECLARE (SPECIAL THALIST))

(DEFUN THRESTRICT
       FEXPR
       (THB)
       (PROG (X)
	     (COND ((ATOM (SETQ X (THGAL (CAR THB) THALIST)))
		    (THPRINTC 'THRESTRICT/ IGNORED/ -/ CONTINUING))
		   ((THRPLACD (CDR X) (THUNION (CDDR X) (CDR THB)))))
	     (RETURN X)))

(DECLARE (UNSPECIAL THALIST))

(DEFUN THRETURN FEXPR (X) (APPLY (QUOTE THSUCCEED)
				 (CONS (QUOTE THPROG) X)))

(DECLARE (SPECIAL THTREE THML))

(DEFUN THRPLACA (X Y) (PROG (THML)
			    (THRPLACAS X Y)
			    (THPUSH THTREE (LIST (QUOTE THMUNG) THML))
			    (RETURN X)))

(DECLARE (UNSPECIAL THTREE THML))

(DECLARE (SPECIAL THML))

(DEFUN THRPLACAS
       (X Y)
       (THPUSH THML (LIST (QUOTE THURPLACA) X (CAR X)))
       (RPLACA X Y))

(DEFUN THURPLACA FEXPR (L) (RPLACA (CAR L) (CADR L)))

(DECLARE (UNSPECIAL THML))

(DECLARE (SPECIAL THTREE THML))

(DEFUN THRPLACD (X Y) (PROG (THML)
			    (THRPLACDS X Y)
			    (THPUSH THTREE (LIST (QUOTE THMUNG) THML))
			    (RETURN X)))

(DECLARE (UNSPECIAL THTREE THML))

(DECLARE (SPECIAL THML))
(DEFUN THRPLACDS
       (X Y)
       (THPUSH THML (LIST (QUOTE THURPLACD) X (CDR X)))
       (RPLACD X Y))

(DEFUN THURPLACD FEXPR (L) (RPLACD (CAR L) (CADR L)))

(DECLARE (UNSPECIAL THML))

(DECLARE (SPECIAL THTREE THALIST THVALUE THML))

(DEFUN THSETQ
       FEXPR
       (THL1)
       (PROG (THML THL)
	     (SETQ THL THL1)
	LOOP (COND ((NULL THL)
		    (THPUSH THTREE (LIST (QUOTE THMUNG) THML))
		    (RETURN THVALUE))
		   ((NULL (CDR THL))
		    (PRINT THL1)
		    (THERT ODD NUMBER OF GOODIES - THSETQ))
		   ((ATOM (CAR THL))
		    (THPUSH THML (LIST (QUOTE SETQ)
				       (CAR THL)
				       (LIST (QUOTE QUOTE)
					     (EVAL (CAR THL)))))
		    (SET (CAR THL) (SETQ THVALUE (EVAL (CADR THL)))))
		   (T (THRPLACAS (CDR (THSGAL (CAR THL)))
				 (SETQ THVALUE
				       (THVAL (CADR THL) THALIST)))))
	     (SETQ THL (CDDR THL))
	     (GO LOOP)))

(DECLARE (UNSPECIAL THTREE THALIST THVALUE THML))

(DECLARE (SPECIAL X THALIST))
(DEFUN THSGAL
 (X)
 (SASSQ (CADR X)
	THALIST
	(FUNCTION (LAMBDA NIL (PROG (Y)
				    (SETQ Y
					  (LIST (CADR X)
						(QUOTE THUNASSIGNED)))
				    (NCONC (GET (QUOTE THALIST)
						(QUOTE VALUE))
					   (LIST Y))
				    (RETURN Y))))))

(DECLARE (UNSPECIAL X THALIST))

(DECLARE (SPECIAL THINDICATORS THP THWH THATOM))

(DEFUN THSTATE
 FEXPR
 (THINDICATORS)							       ;PRINTS THAT PART OF THE STATE OF THE
								       ;MICRO-PLANNER WORLD SPECIFIED BY THE INDICATORS
								       ;IN REREADABLE FORM. NOTE THAT		 ;IT IS  ;BLIND TO ASSERTIONS THAT BEGIN WITH	 
 (PROG (THP)							       ;;EITHER NUMBERS, LIST STRUCTURE, NOHASHED ATOMS
       (PRINT (QUOTE (THDATA)))					       ;OR NON-INTERNED ATOMS.
       (MAPC
	(FUNCTION
	 (LAMBDA (BUCKET)
	  (MAPC
	   (FUNCTION
	    (LAMBDA (THATOM)
	     (MAPC
	      (FUNCTION
	       (LAMBDA (THWH)
		(AND
		 (SETQ THP (GET THATOM THWH))
		 (SETQ THP (ASSOC 1. (CDR THP)))
		 (MAPC
		  (FUNCTION
		   (LAMBDA (LENGTH-BUCKET)
		    (MAPC
		     (FUNCTION (LAMBDA (ASRT)
				       (COND ((EQ THWH
						  (QUOTE THASSERTION))
					      (PRINT ASRT))
					     ((PRINT (LIST ASRT))))))
		     (CDDR LENGTH-BUCKET))))
		  (CDR THP)))))
	      (COND (THINDICATORS)
		    (' (THASSERTION THANTE THCONSE THERASING))))))
	   BUCKET)))
	(MAKOBLIST NIL))
       (PRINT NIL)))

(DECLARE (UNSPECIAL THINDICATORS THP THWH THATOM))

(DECLARE (SPECIAL THTREE THALIST THBRANCH THABRANCH THA))
(DEFUN THSUCCEED
       FEXPR
       (THA)
       (OR (NOT THA)
	   (PROG (THX)
		 (AND (EQ (CAR THA) (QUOTE THEOREM))
		      (SETQ THA (CONS (QUOTE THPROG) (CDR THA))))
		 (SETQ THBRANCH THTREE)
		 (SETQ THABRANCH THALIST)
	    LOOP (COND ((NULL THTREE) (PRINT THA)
				      (THERT OVERPOP - THSUCCEED))
		       ((EQ (CAAR THTREE) (QUOTE THREMBIND))
			(SETQ THALIST (CADAR THTREE))
			(THPOPT)
			(GO LOOP))
		       ((EQ (CAAR THTREE) (CAR THA))
			(THPOPT)
			(RETURN (COND ((CDR THA) (EVAL (CADR THA)))
				      ((QUOTE THNOVAL)))))
		       ((AND (EQ (CAR THA) (QUOTE THTAG))
			     (EQ (CAAR THTREE) (QUOTE THPROG))
			     (SETQ THX (MEMQ (CADR THA)
					     (CADDDR (CAR THTREE)))))
			(RPLACA (CDAR THTREE) (CONS NIL THX))
			(RETURN (THPROGT)))
		       (T (THPOPT) (GO LOOP))))))

(DECLARE (UNSPECIAL THTREE THALIST THBRANCH THABRANCH THA))

(DECLARE (SPECIAL XX TYPE THX THY1 THY THXX))
(DEFUN THTAE
 (XX)
 (COND
  ((ATOM XX) NIL)
  ((EQ (CAR XX) (QUOTE THUSE))
   (MAPCAR
    (FUNCTION (LAMBDA (X)
		      (COND ((NOT (AND (SETQ THXX
					     (GET X (QUOTE THEOREM)))
				       (EQ (CAR THXX) TYPE)))
			     (PRINT X)
			     (LIST 'THAPPLY
				   (THERT BAD THEOREM /-THTAE)
				   (CAR THX)))
			    (T (LIST (QUOTE THAPPLY) X (CAR THX))))))
    (CDR XX)))
  ((EQ (CAR XX) (QUOTE THTBF))
   (MAPCAN (FUNCTION (LAMBDA (Y) (COND (((CADR XX) Y)
					(LIST (LIST (QUOTE THAPPLY)
						    Y
						    (CAR THX)))))))
	   (COND (THY1 THY) ((SETQ THY1 T)
			     (SETQ THY (THMATCHLIST (CAR THX) TYPE))))))
  (T (PRINT XX) (THTAE (THERT UNCLEAR RECCOMMENDATION /-THTAE)))))

(DECLARE (UNSPECIAL XX TYPE THX THY1 THY THXX))

(DECLARE (SPECIAL THTREE))

(DEFUN THTAG FEXPR (L) (AND (CAR L)
			    (THPUSH THTREE
				    (LIST (QUOTE THTAG) (CAR L)))))

(DECLARE (UNSPECIAL THTREE))

(DEFUN THTAGF NIL (THPOPT) NIL)

(DECLARE (SPECIAL THVALUE))

(DEFUN THTAGT NIL (THPOPT) THVALUE)

(DECLARE (UNSPECIAL THVALUE))

(DEFUN THTRUE (X) T)

(DECLARE (SPECIAL THTREE THOLIST THALIST))
(DEFUN THTRY1							       ;TRIES NEXT RECOMMENDATION ON TREE FOR THGOAL
       NIL
       (PROG (THX THY THZ THW THEOREM)
	     (SETQ THZ (CAR THTREE))				       ;= (THGOAL PATTERN EXPANDED-RECOMMENDATIONS)
	     (SETQ THY (CDDR THZ))				       ;= RECOMMENDATIONS
	     (RPLACD THY (SUB1 (CDR THY)))
	NXTREC
	     (COND ((OR (NULL (CAR THY)) (ZEROP (CDR THY)))
		    (RETURN NIL)))				       ;RECOMMENDATIONS EXHAUSTED. FAIL
	     (SETQ THX (CAAR THY))
	     (GO (CAR THX))
	THNUM(RPLACD THY (CADR THX))
	     (RPLACA THY (CDAR THY))
	     (GO NXTREC)
	THDBF(SETQ THOLIST THALIST)
	     (COND ((NULL (CADDR THX)) (RPLACA THY (CDAR THY))
				       (GO NXTREC))		       ;NO MORE CANDIDATES SATISFYING THIS REC.
		   ((PROG2 0.					       ;TRY NEXT REC
			   (AND ((CADR THX) (SETQ THW (CAADDR THX)))
				(THMATCH1 (CADR THZ) (CAR THW)))
			   (RPLACA (CDDR THX) (CDADDR THX)))
		    (RETURN THW))
		   (T (GO THDBF)))
	THTBF(COND ((NULL (CADDR THX)) (RPLACA THY (CDAR THY))
				       (GO NXTREC)))		       ;NO MORE CANDIDATES SATISFYING THIS REC.
	     (SETQ THEOREM (CAADDR THX))
	THTBF1
	     (COND ((NOT (AND (SETQ THW				       ;TRY NEXT REC
				    (GET THEOREM (QUOTE THEOREM)))
			      (EQ (CAR THW) (QUOTE THCONSE))))
		    (PRINT THEOREM)
		    (COND ((EQ (SETQ THEOREM
				     (THERT BAD THEOREM - THTRY1))
			       'T)
			   (GO NXTREC))
			  (T (GO THTBF1)))))
	     (COND ((PROG2 0.
			   (AND ((CADR THX) (CAADDR THX))
				(THAPPLY1 THEOREM THW (CADR THZ)))
			   (RPLACA (CDDR THX) (CDADDR THX)))
		    (RETURN T))
		   (T (GO THTBF)))))

(DECLARE (UNSPECIAL THTREE THOLIST THALIST))

(DECLARE (SPECIAL THZ1 THZ THY1 THY THA2))
(DEFUN THTRY
 
 ;;THTRY IS IN CHARGE OF MAKING UP THE "THINGS TO DO" LIST
 ;;WHICH IS PUT ON THTREE.  SO WHENEVER WE FAIL BACK
 ;;TO A THGOAL, WE GO TO THE NEXT "THING TO DO"
 (X)
 
 ;;X IS THE LIST OF RECOMMENDATIONS
 (COND ;;ANY ATOMIC RECOMMENDATION IS IGNORED,  THIS
       ;;IS USEFUL IN ERROR RECOVERY
       ((ATOM X) NIL)
       
       ;;HAVE A THEOREM BASE FILTER
       ((EQ (CAR X) (QUOTE THTBF))
	
	;;MAKE UP A LIST WHICH GIVES, 1 - THE INDICATOR "THTBF"
	;; 2 - THE ACTUAL FILTER (THTRUE IS THE MOST COMMON)
	;; 3 - THE BUCKET RETURNED BY THMATCHLIST
	(COND ((NOT THZ1) (SETQ THZ1 T) (SETQ THZ (THMATCHLIST THA2 'THCONSE))))
	(COND (THZ (LIST (LIST 'THTBF (CADR X) THZ))) (T NIL)))
       
       ;;DO THE SAME THING, ONLY FOR DATA BASE FILTERS
       ((EQ (CAR X) (QUOTE THDBF))
	(COND ((NOT THY1) (SETQ THY1 T) (SETQ THY (THMATCHLIST THA2 'THASSERTION))))
	(COND (THY (LIST (LIST 'THDBF (CADR X) THY))) (T NIL)))
       
       ;;THUSE STATEMENTS ARE TRANSLATED INTO THTBF THTRUE
       ;;STATEMENTS, WHICH THE "BUCKET" IS THE LIST GIVEN IN THE THUSE
       ((EQ (CAR X) (QUOTE THUSE))
	(LIST (LIST (QUOTE THTBF) (QUOTE THTRUE) (CDR X))))
       ((EQ (CAR X) 'THNUM) (LIST X))
       (T (PRINT X) (THTRY (THERT UNCLEAR RECOMMENDATION - THTRY)))))

(DECLARE (UNSPECIAL THZ1 THZ THY1 THY THA2))

(DECLARE (SPECIAL THTREE THALIST THXX))

(DEFUN THUNDOF
       NIL
       (COND ((NULL (CADDAR THTREE)) (THPOPT))
	     (T (SETQ THXX (CDDAR THTREE))
		(SETQ THALIST (CAADR THXX))
		(RPLACA (CDR THXX) (CDADR THXX))
		(SETQ THTREE (CAAR THXX))
		(RPLACA THXX (CDAR THXX))))
       NIL)

(DECLARE (UNSPECIAL THTREE THALIST THXX))

(DEFUN THUNDOT NIL (THPOPT) T)

(DECLARE (SPECIAL THALIST))

(DEFUN THUNIQUE
       FEXPR
       (THA)
       (SETQ THA (CONS (QUOTE THUNIQUE) (MAPCAR (FUNCTION EVAL) THA)))
       (PROG (X)
	     (SETQ X THALIST)
	LP   (COND ((NULL X) (THPUSH THALIST THA) (RETURN T))
		   ((EQ (CAAR X) (QUOTE THUNIQUE))
		    (COND ((EQUAL (CAR X) THA) (RETURN NIL)))))
	     (SETQ X (CDR X))
	     (GO LP)))

(DECLARE (UNSPECIAL THALIST))

(DECLARE (SPECIAL THALIST THXX))

(DEFUN THV1
 (X)								       ;(THV1 'X) IS THE VALUE OF THE PLANNER VARIABLE
 (SETQ THXX X)							       ;$?X RETURNS ERROR MESSAGE IF X UNBOUND OR
 (COND ((EQ (SETQ X (CADR (SASSQ X				       ;UNASSIGNED
				 THALIST
				 (FUNCTION (LAMBDA NIL
						   (PRINT THXX)
						   (THERT THUNBOUND
							  -
							  THV1))))))
	    (QUOTE THUNASSIGNED))
	(PRINT THXX)
	(THERT THUNASSIGNED - THV1))
       (T X)))

(DECLARE (UNSPECIAL THALIST THXX))

(DEFUN THV
       FEXPR
       (X)							       ;(THV X) IS THE VALUE OF THE PLANNER VARIABLE
       (THV1 (CAR X)))						       ;$?X

(DECLARE (SPECIAL THLEVEL
		  THSTEP
		  THSTEPF
		  THSTEPT
		  THSTEPD
		  THMESSAGE
		  ^A
		  THV
		  THINF
		  THE
		  THTREE
		  THOLIST
		  THEXP
		  THALIST
		  THVALUE
		  THBRANCH
		  THABRANCH))
(DEFUN THVAL
       
       ;;CORESPONDS TO LISP EVAL
       ;;THEXP IS THE EXPRESSION TO BE THVALUATED
       ;;THALIST IS THE VARIABLE BINDING LIST
       (THEXP THALIST)
       
       ;;ALL THPUSH DOES IS TO CONSE ON THE SSECOND ITEM TO THE FIRST
       (THPUSH THLEVEL (LIST THTREE THALIST))
       (PROG (THTREE THVALUE THBRANCH THOLIST THABRANCH THE THMESSAGE)
	     (SETQ THV (QUOTE (THV THNV)))
	     (SETQ THVALUE 'THNOVAL)
	     
	     ;;THE BECOMES THE CURRENT EXPRESSION
	     ;;THEXP IS RESERVED FOR FURTHER EXPRESSIONS
	     ;;WHICH SHOULD BE THVALED BEFORE WE GO TO THE NEXT
	     ;;ITEM OF ACTUAL CODE.  FOR EXAMPLE, THASSERT USES
	     ;;THIS FEATURE TO PROCESS ANTECEDENT THEOREMS
	GO   (SETQ THE THEXP)
	     (SETQ THEXP NIL)
	     
	     ;;TYPING ^A (CONTROL A) AT MAC-AI LISP CAUSES ^A (UPARROW A)
	     ;;TO BE SET TO T. THIS CAN BE DONE WHILE A FUNCTION
	     ;;IS BEING PROCESSED.  THE NET EFFECT IS TO TEMPORARILY
	     ;;HALT EVALUAION
	     (COND (^A (SETQ ^A NIL)
		       (OR (THERT ^A - THVAL) (GO FAIL))))
	     
	     ;;THSTEP AND ITS RELATIVES ARE FOR STEPPING THROUGH
	     ;;PLANNER FUNCTIONS IN A SPECIAL WAY.  TO THIS DATE
	     ;;ONLY SUSSMAN KNOWS EXACTLY WHAT IT IS SUPPOSE TO DO
	     ;;YOU CAN SAFELY IGNORE ANY EXPRESSION WHICH MENTIONS IT
	     (COND (THSTEP (EVAL THSTEP)))
	     
	     ;;EVAL THE CURRENT EXPRESSION TO BE THVALED.  NOTE
	     ;;THAT EACH PLANNER FUNCTION CORESPONDS TO THREE LISP FUNCTIONS
	     ;;ONE TO SET THINGS UP (THIS IS WHAT IS GETTING EVALED AT THIS POINT
	     ;;ONE TO HANDLE SUCCESS AND ONE FOR FAILURE 
	     (COND ((ERRSET (SETQ THVALUE (EVAL THE))))
		   
		   ;;IF THERE WAS A LISP ERROR, REPORT IT TO THE USER
		   (T (PRINT THE)
		      (SETQ THVALUE (THERT LISPERROR - THVAL))))
	GO1  (COND (THSTEPD (EVAL THSTEPD)))
	     
	     ;;USUALLY THEMESSAGE WILL BE NIL.  EXCEPTION IS WHEN
	     ;;USER HAS USED THE THMESSAGE FUNCTION
	     (COND (THMESSAGE (GO MFAIL))
		   
		   ;;IF THEXP IS NON NIL IT MEANS THAT WE HAVE
		   ;;MORE PLANNER TO WORK ON BEFORE GOING TO NEXT LINE OF USER CODE
		   (THEXP (GO GO))
		   
		   ;;IF THVALUE IS NON NIL IT MEANS THAT SO FAR THE THEOREM IS SUCCEEDING
		   (THVALUE (GO SUCCEED))
		   
		   ;;ELSE WE ARE IN A FAILURE SITUATION
		   (T (GO FAIL)))
	     
	     ;;HANDLES SUCCESS
	SUCCEED
	     (COND (THSTEPT (EVAL THSTEPT)))
	     
	     ;;SAVE CURRENT STATE OF THTREE AND THALIST IN CASE
	     ;;WE HAVE TO BACK UP
	     (COND ((NULL THBRANCH) (SETQ THBRANCH THTREE)
				    (SETQ THABRANCH THALIST)))
	     
	     ;;IF THE THTREE IS NIL IT MEANS THAT THE THPROG OR WHATEVER HAS BEEN
	     ;;COMPLETED SO THERE ARE NO MORE EXPRESSIONS TO DO,
	     ;;ALL THEOREMS ACT LIKE A THPROG, INCLUDING PUTTING
	     ;;ITS MARK ON THTREE SEE THAPPLY
	     ;;HENCE NO NEED TO GROW MORE BRANCHES ON THTREE
	     (COND ((NULL THTREE) (SETQ THLEVEL (CDR THLEVEL))
				  (RETURN THVALUE))
		   
		   ;;THIS IS THE NORMAL CASE.  WE EVAL THE SUCCEED-FUNCTION
		   ;;OF THE PLANNER FUNCTION WHICH JUST SUCCEEDED
		   ((SETQ THEXP (GET (CAAR THTREE) (QUOTE THSUCCEED)))
		    (GO GO2))
		   
		   ;;IN CASE OF LOSSAGE LETS THE USER SUCCEED ANYWAY
		   ((THERT BAD SUCCEED - THVAL) (GO SUCCEED))
		   ((GO FAIL)))
	     
	     ;;HAS TO DO WITH FAILURE + MESSAGE
	MFAIL(COND ((EQ (CAR THMESSAGE) THTREE)
		    (SETQ THEXP (CADR THMESSAGE))
		    (SETQ THMESSAGE NIL)
		    (GO GO)))
	FAIL (COND (THSTEPF (EVAL THSTEPF)))
	     
	     ;;IF THTREE IS NIL WE HAVE FAILED THE ENTIRE EXPRESSION
	     (COND ((NULL THTREE) (SETQ THLEVEL (CDR THLEVEL))
				  (RETURN NIL))
		   
		   ;;NORMAL CASE, EVAL THE FAILURE FUNCTION ASSOCIATED
		   ;;WITH THE PLANNER FUNCTION WHICH JUST FAILED
		   ((SETQ THEXP (GET (CAAR THTREE) (QUOTE THFAIL)))
		    (GO GO2))
		   ((THERT BAD FAIL - THVAL) (GO SUCCEED))
		   ((GO FAIL)))
	     
	     ;;THEXP AT THIS POINT IS THE APPROPRIATE SUCCESS OR
	     ;;FAILURE ASSOCIATED FUNCTION.  EVAL IT AND AT THE SAME
	     ;;TIME, SET IT TO NIL IN CASE WE NEED THEXP FOR MORE EXPRESSIONS
	     ;;TO BE PROCESSED
	GO2  (SETQ THVALUE ((PROG2 0. THEXP (SETQ THEXP NIL))))
	     
	     ;;GO THROUGH ENTIRE PROCESS AGAIN
	     ;;A TYPICAL PROCESS IN SUCCESS IS TO KEEP REMOVING EXPRESSIONS FROM THTREE UNTIL
	     ;;WE GET BACK TO THE THREE ENTRY PUT ON BY THPROG
	     ;;AT THIS POIN IT EVALS THPROGT, AND SEE THAT LISTING
	     (GO GO1)))
(DECLARE (UNSPECIAL THSTEP
		    THSTEPF
		    THSTEPT
		    THSTEPD
		    THLEVEL
		    THMESSAGE
		    ^A
		    THV
		    THINF
		    THE
		    THTREE
		    THOLIST
		    THEXP
		    THALIST
		    THVALUE
		    THBRANCH
		    THABRANCH))

(DEFUN THVAR
       (X)							       ;PREDICATE - IS ITS INPUT A PLANNER VARIABLE
       (MEMQ (CAR X) (QUOTE (THV THNV))))

(DECLARE (SPECIAL THALIST THY))

(DEFUN THVARS2
       
       ;;THIS IS THE WORKHORSE FOR THVARSUBST
       (X)
       
       ;;X IS A SINGLE ITEM FROM A PATTERN
       (PROG (A)
	     (AND (ATOM X) (RETURN X))
	     
	     ;;IF ITS AN ATOM NOTHING NEED BE DONE
	     (AND (EQ (CAR X) (QUOTE THEV))
		  (SETQ X (THVAL (CADR X) THALIST)))
	     
	     ;;IF THE EXPRESSION HAS A $E BEFORE IT, THVAL BEFORE GOING ON
	     (OR (THVAR X) (RETURN X))
	     
	     ;;IF THE ITEM IS NOT A VARIABLE IT MUST BE
	     ;;SOME RANDOM LIST, SO IT HAS NO  ASSIGNED VALUE
	     (SETQ A (THGAL X THALIST))
	     
	     ;;AT THIS POINT X MUST BE A VARIABLE, SO FIND ITS
	     ;;ASSIGNMENT, THATS WHAT THGAL DOES
	     ;;THALIST IS WHERE THE VARIABLE ASSIGNMENTS RESIDE
	     (RETURN (COND ((EQ (CADR A) (QUOTE THUNASSIGNED)) X)
			   
			   ;;IF THE VARIABLE IS UNASSIGNED
			   ;;THEN RETURN THE ACTUAL VARIABLE
			   ((AND THY (EQ (CAR X) 'THNV))
			    
			    ;;THY WILL BE T JUST IN THE CASES
			    ;;WHERE THVARSUBST WAS CALLED BY A THGOAL SITUATION
			    ;;IT IS THEN NECESSARY TO IMMEDIATELY HACK IN A
			    ;;THUNASSIGNED SO THAT IF THE SAME VARIABLE IS USED
			    ;;TWICE IN THE SAME PATTERN WE WON'T PUT
			    ;;IN ITS OLD VALUE THE SECOND TIME IT IS ENCOUNTERED
			    (THRPLACA (CDR A) 'THUNASSIGNED)
			    X)
			   
			   ;;OTHERWISE THE ASSIGNMENT IS THE SECOND ELEMENT
			   ;;IN THE BINDING LIST
			   (T (CADR A))))))

(DEFUN THVARSUBST
       (THX THY)
       
       ;;THX IS A GOAL OR ASSERTION PATTERN OR THEOREM NAME
       ;;THIS FUNCTION RETURNS THE SAME PATTERN, EXCEPT
       ;;IN PLACE OF ALL ASSIGNED VARIABLES WILL BE THE
       ;;VALUES THEY ARE ASSIGNED TO
       (COND ((EQ (CAR THX) (QUOTE THEV))
	      
	      ;;IF THE CAR IS THEV IT MEANS THAT THERE WAS
	      ;;A $E BEFORE THE PATTERN, IN WHICH CASE WE
	      ;;ARE TO GET THE REAL PATTERN BY THVALUATING WHAT
	      ;;IS THERE
	      (SETQ THX (THVAL (CADR THX) THALIST)))
	     ((THVAR THX) (SETQ THX (EVAL THX))))
       
       ;;THVAR TESTS TO SEE IF ARG IS A VARIABLE
       ;;IF THE PATTERN IS A SINGLE VARIABLE THE PROGRAM ASSUMES
       ;;THERE SHOULD BE AN IMPLICIT THVAL.
       ;;UNLESS THE ASSERTEE IS A THEOREM NAME
       ;;GO THROUGH IT PLACE BY PLACE WITH THVARS2
       (COND ((ATOM THX) THX) (T (MAPCAR (FUNCTION THVARS2) THX))))

(DECLARE (UNSPECIAL THALIST THY))

(DECLARE (SPECIAL THALIST THVALUE THA))

(DEFUN THVSETQ
       FEXPR
       (THA)
       (PROG (A)
	     (SETQ A THA)
	LOOP (COND ((NULL A) (RETURN THVALUE))
		   ((NULL (CDR A))
		    (PRINT THA)
		    (THERT ODD NUMBER OF GOODIES-THSETQ))
		   (T (SETQ THVALUE
			    (CAR (RPLACA (CDR (THSGAL (CAR A)))
					 (THVAL (CADR A) THALIST))))))
	     (SETQ A (CDDR A))
	     (GO LOOP)))

(DECLARE (UNSPECIAL THALIST THVALUE THA))

(DEFPROP THTAG THTAGF THFAIL)

(DEFPROP THTAG THTAGT THSUCCEED)

(DEFPROP THGOAL THGOALT THSUCCEED)

(DEFPROP THGOAL THGOALF THFAIL)

(DEFPROP THFAIL? THFAIL?F THFAIL)
(DEFPROP THFAIL? THFAIL?T THSUCCEED)

(DEFPROP THAMONG THAMONGF THFAIL)

(DEFPROP THFIND THFINDF THFAIL)

(DEFPROP THFIND THFINDT THSUCCEED)

(DEFPROP THPROG THPROGT THSUCCEED)

(DEFPROP THAND THANDT THSUCCEED)

(DEFPROP THMUNG THMUNGT THSUCCEED)

(DEFPROP THERASE THERASET THSUCCEED)

(DEFPROP THASSERT THASSERTT THSUCCEED)

(DEFPROP THOR THORT THSUCCEED)

(DEFPROP THCOND THCONDT THSUCCEED)

(DEFPROP THAND THANDF THFAIL)

(DEFPROP THPROG THPROGF THFAIL)

(DEFPROP THMUNG THMUNGF THFAIL)

(DEFPROP THASSERT THASSERTF THFAIL)

(DEFPROP THERASE THERASEF THFAIL)

(DEFPROP THCOND THCONDF THFAIL)

(DEFPROP THOR THORF THFAIL)

(DEFPROP THDO THDOB THSUCCEED)

(DEFPROP THDO THDOB THFAIL)

(DEFPROP THUNDO THUNDOF THFAIL)

(DEFPROP THUNDO THUNDOT THSUCCEED)

(DEFPROP THMESSAGE THMESSAGEF THFAIL)

(DEFPROP THMESSAGE THMESSAGET THSUCCEED)

(DEFPROP THREMBIND THREMBINDT THSUCCEED)

(DEFPROP THREMBIND THREMBINDF THFAIL)

(DECLARE (SPECIAL THALIST THLEVEL THINF))
(DEFUN THERT
       FEXPR
       
       ;;THERT IS THE BREAK FUNCTION, AND ALSO THE TOP LEVEL FUNCTION
       ;;IT IS CALLED DIRECTLY BY LISP BEFORE LISP
       ;;GOES INTO THE READ EVAL LOOP.
       ;;FOR HOW THIS IS DONE, SEE MAC-AI LISP DOCUMENTATION
       ;;IN ESSENCE THERT CONTAINS ITS OWN LOOP, WHICH IS READ THVAL.
       (/0ERTA)
       
       ;;/0ERTA IS THE ERROR MESSAGE TO BE PRINTED
       ;;OUT WHEN THERT IS USED FOR ERROR BREAKING
       (PROG (/0LISTEN ^W ^Q)
	     (PRINT (QUOTE >>>))
	     (COND 
		   ;;SPECIAL MESSAGE PRINTOUT
		   ((EQ (CAR /0ERTA) 'TH%0%)
		    (MAPC (FUNCTION THPRINT2) (CDR /0ERTA))
		    (IOC Q))
		   
		   ;;THE NORMAL MESSAGE PRINTOUT
		   ((MAPC (FUNCTION THPRINT2) /0ERTA)
		    (PRINT (QUOTE LISTENING))
		    
		    ;;IF WE ARE AT TOP LEVEL THLEVEL WILL BE NIL
		    (OR THLEVEL (THPRINT2 (QUOTE THVAL)))))
	     
	     ;;GO INTO READ LOOP
	/0LISTEN
	     (SETQ THINF NIL)
	     
	     ;;LINEFEED
	     (TERPRI)
	     
	     ;;READ IN S EXPRESSION.
	     (ERRSET (COND ((EQ (SETQ /0LISTEN (READ)) (QUOTE P))
			    (RETURN T))				       ;$P IMPLIES PROCEDE
			   ((AND (NOT (ATOM /0LISTEN))		       ;($P EXP) IMPLIES PROCEDE AND OUTPUT (EVAL EXP)
				 (EQ (CAR /0LISTEN) (QUOTE P)))
			    (RETURN (EVAL (CADR /0LISTEN))))
			   (THLEVEL (PRINT (EVAL /0LISTEN)))	       ;EVAL LISTENING IF NOT AT TOP LEVEL
			   (T (PRINT (THVAL /0LISTEN THALIST)))))      ;THVAL LISTENING AT TOP LEVEL
	     (GO /0LISTEN)))

(DECLARE (SPECIAL PURE
		  LOW
		  THXX
		  THTRACE
		  THALIST
		  THTREE
		  ERRLIST
		  THGENAME
		  THLEVEL))
(DEFUN THINIT
       FEXPR
       (L)
       (COND ((AND L PURE) (LAPPURIFY LOW (PAGEBPORG))
			   (SETQ PURE NIL)))
       (SETQ THGENAME 0.)
       (SETQ THSTEP NIL)
       (SETQ THSTEPD NIL)
       (SETQ THSTEPT NIL)
       (SETQ THSTEPF NIL)
       (SETQ THXX NIL)
       (SETQ THTRACE NIL)
       (SETQ THALIST (QUOTE ((NIL NIL))))
       (SSTATUS MACRO $ (QUOTE THREAD))
       (SETQ ERRLIST
	     (QUOTE ((PRINT (QUOTE MICRO-PLANNER))
		     (PRINC THVERSION)
		     (COND ((ERRSET (APPLY 'UREAD
					   (APPEND '(/.PLNR/.
						     /(INIT/))
						   (CRUNIT)))
				    NIL)
			    (SETQ ERRLIST (CDDDDR ERRLIST))
			    (SETQ THTREE NIL)
			    (SETQ THLEVEL NIL)
			    (THERT TH%0% READING /.PLNR/. /(INIT/))))
		     (SETQ ERRLIST (CDDDDR ERRLIST))
		     (SETQ THINF NIL)
		     (SETQ THTREE NIL)
		     (SETQ THLEVEL NIL)
		     (THERT TOP LEVEL)))))

(DECLARE (UNSPECIAL PURE
		    LOW
		    THXX
		    THTRACE
		    THALIST
		    ERRLIST
		    THTREE
		    THLEVEL
		    THGENAME
		    THINF))