(COMMENT FOR PLNR 159 AND GREATER, THPRINTC CAN BE ELIMINATED)

;SYSTEM FUNCTIONS SUCH AS THGOAL, THASSERT, THERASE AND THEOREM
;(ALL THMS) ARE TRACED IF THEY ARE ON 'THTRACE'.  THTRACES1 PUTS
;THEM THERE AND THUNTRACE TAKES THEM OFF. 

;THTRACE IS INITIALLY SET TO NIL BY TS PLNR

(DEFUN THTRACE FEXPR (L) (MAPC (FUNCTION THTRACE1) L))

(DEFUN
 THTRACE1
 (X)
 (PROG (Y)

	;VARIETY OF POSSIBLE INPUT FORMATS TRANSFORMED TO STANDARD 
	;3 ELEMENT LIST (OBJECT-TO-BE-TRACED TRACE-CONDITION BREAK CONDITION)
       (SETQ X (COND ((ATOM X) (LIST X T NIL))
		     ((CDDR X) X)
		     ((NULL (CDR X)) (PRINT X)
				     (PRINC 'BAD/ FORMAT)
				     (RETURN NIL))
		     ((LIST (CAR X) (CADR X) NIL))))

	;IF OBJECT-TO-BE-TRACED IS A PARTICULAR THEOREM, THEN THE TRIPLET
	;'(THEOREM (THSEL 'CADR)(THSEL 'CADDDR)) IS GUARANTEED TO 
	;BE ON THTRACE IN ADDITION TO THE STANDARD TRIPLET
       (COND ((GET (CAR X) 'THEOREM)
	      (COND ((SETQ Y (ASSQ 'THEOREM THTRACE))
		     (RPLACD Y '((THSEL 'CADR)
				       (THSEL 'CADDR))))
		    ((SETQ THTRACE
			   (LIST X
				 (APPEND '(THEOREM (THSEL 'CADR)
							 (THSEL 'CADDR))
					 THTRACE)))))))

	;THTRACE IS UPDATED. IF THE OBJECT-TO-BE-TRACED IS ALREADY ON
	;THTHRACE THEN THE TRACE AND BREAK CONDITIONS ARE UPDATED. 
	;ELSE THE WHOLE TRIPLET IS PLACED ON THTRACE
       (COND ((SETQ Y (ASSQ (CAR X) THTRACE)) (RPLACD Y (CDR X)))
	     ((SETQ THTRACE (CONS X THTRACE))))

       (RETURN X)))


;THUNTRACE REMOVES ELEMENTS OF ITS ARG FROM THTRACE
;IF NOT GIVEN ANY ARGS, THUNTRACE SETS THTRACE TO NIL
(DEFUN THUNTRACE
       FEXPR
       (L)
       (COND (L (SETQ THTRACE (MAPCAN (FUNCTION (LAMBDA (X)
							(COND ((MEMQ (CAR X) L)
							       (PRINT X)
							       NIL)
							      ((LIST X)))))
				      THTRACE)))
	     ((MAPC (FUNCTION PRINT) THTRACE) (SETQ THTRACE NIL)))
       'DONE)
;THTRACES IS ACTIVATED BY THGOAL, THASSERT, ... IF THTRACE IS NON-NIL
;THF IS SET TO THE PARTICULAR CANDIDATE FOR TRACEAGE, E.G.
;TO 'THGOAL IF THE PLANNER FUNCTION THGOAL ACTIVATED THTRACES
;THL = THE INSTANTIATED ARG OF THF. SEE DESC OF X ON NEXT PAGE

(DEFUN THTRACES (THF THL) (PROG (THY THZ THB)
				(AND
				     ;THY SET TO TRIPLET ON THTRACE. IF NOT THERE, NO TRACING
				     (SETQ THY (ASSQ THF THTRACE))

				     ;IF BOTH TRACE AND BREAK ARE FALSE, DON'T TRACE
				     ;SIDE EFFECT - THB SET TO VALUE OF BREAK
				     (OR (SETQ THB (THVAL (CADDR THY) THALIST))
					 (THVAL (CADR THY) THALIST))

				     ;THZ IS SET TO THE TRACE FUNCTION FOR THE OBJECT-TO-BE-TRACED
				     (OR (SETQ THZ (GET THF 'THTRACE))
					 (THERT THTRACES - TRACE LOSSAG))

				     ;THE TRACE FN IS EXECUTED
				     (THZ THL THB)

				     ;IF THB IS NON-NIL, BREAK
				     THB
				     (THERT))))

;THE CAR OF THE TREE IS '(THTRACES NAME-OF-TRACE-POINT OPTIONAL-PRINT-OF-THVALUE (THERT)-OR-NIL)
;THUS, THESE TWO FNS PRINT THE NAME OF THE TRACE POINT, "FAIL"-OR-"SUCCEED"
;PRINT THVALUE IF ANY, AND FINALLY BREAK IF (THERT) IS PRESENT, 
;THEN POP THE TREE

(DEFPROP THTRACES
	 (LAMBDA NIL
		 (PRINT (CADAR THTREE))
		 (PRINC 'FAILED/ )
		 (EVLIS (CDDAR THTREE))
		 (THPOPT)
		 NIL)
	 THFAIL)

(DEFPROP THTRACES
	 (LAMBDA NIL
		 (PRINT (CADAR THTREE))
		 (PRINC 'SUCCEEDED/ )
		 (EVLIS (CDDAR THTREE))
		 (THPOPT)
		 THVALUE)
	 THSUCCEED)
;THE TRACE FNS THBKPT, THGOAL, THEOREM, THASSERT, AND THERASE PUSH ONTO THE TREE
;'(THTRACES NAME-OF-TRACE-POINT OPTIONAL-PRINT-OF-THVALUE (THERT)-OR-NIL)
;X=THL=INSTANTIATED GOAL, ASSERTION OR ERASURE, NAME OF THE THM OR 
;MESSAGE OF THE BREAKPOINT

(DEFPROP THBKPT
	 (LAMBDA (X B)
		 (THPUSH THTREE (LIST 'THTRACES
				      (THGENS B)
				      (AND B '(THERT))))
		 (THPRINTC 'PASSING/ BKPT)
		 (PRIN1 (CADAR THTREE))
		 (PRINC '/ )
		 ;BY SETTING THBRANCH AND THABRANCH, A TRIPLE IS CREATED
		 ;BY THVAL FOR BACKTRACKING.  THEN, THE TREE IS POPPED
		 ;TO PREVENT THTRACES FROM TYPING OUT THE MEANINGLESS
		 ;THAT THE BREAKPOINT SUCCEEDED.
		 (SETQ THBRANCH THTREE)
		 (SETQ THABRANCH THALIST)
		 (THPOPT)
		 (PRIN1 X))
	 THTRACE)

(DEFPROP THGOAL
	 (LAMBDA (X B)
		 (THPUSH THTREE (LIST 'THTRACES
				      (THGENS G)
				      '(AND THVALUE (PRIN1 THVALUE))
				      (AND B '(THERT))))
		 (THPRINTC 'TRYING/ GOAL)
		 (PRIN1 (CADAR THTREE))
		 (PRINC '/ )
		 (PRIN1 X))
	 THTRACE)

(DEFPROP THEOREM
	 (LAMBDA (X B)
		 (THPUSH THTREE (LIST 'THTRACES
				      X
				      '(AND THVALUE (PRIN1 THVALUE))
				      (AND B '(THERT))))
		 (THPRINTC 'ENTERING/ THEOREM)
		 (PRIN1 X))
	 THTRACE)

(DEFPROP THASSERT
	 (LAMBDA (X B)
		 (THPUSH THTREE (LIST 'THTRACES
				      (THGENS A)
				      (AND B '(THERT))))
		 (PRINT 'ASSERTING)
		 (PRIN1 (CADAR THTREE))
		 (PRINC '/ )
		 (PRIN1 X))
	 THTRACE)

(DEFPROP THERASE
	 (LAMBDA (X B)
		 (THPUSH THTREE (LIST 'THTRACES
				      (THGENS E)
				      (AND B '(THERT))))
		 (PRINT 'ERASING)
		 (PRIN1 (CADAR THTREE))
		 (PRINC '/ )
		 (PRIN1 X))
	 THTRACE);UTILITY FNS

;FOR THE TRACE-OBJECT 'THEOREM, IF ANY SPECIFIC THMS ARE TRACED,
;	'(THSEL 'CADR) AND '(THSEL 'CADDDR)
;ARE THE TRACE AND BREAK PREDICATES.  HENCE THTRACES CAUSES
;THESE EXPR'S TO BE THVALED. THL IS SET TO THE SECOND ARG
;OF THTRACES WHICH IN THIS CASE IS PRESUMABLY THE NAME OF 
;THE PARTICULAR THM THAT ACTIVATED THTRACES. THSEL FIRST
;CHECKS TO SEE WHETHER THIS THM IS INDEPENDENTLY ON THTRACE. 
;IF NOT, IT DOES NO MORE. BUT IF IT IS, THX GETS SET TO THE THM'S 
;TRIPLET. THEN THX GETS SET TO EITHER THE TRACE (ARG='CADR) OR THE BREAK 
;(ARG='CADDDR) CONDITION OF THE TRIPLET. FINALLY, THESE CONDITIONS ARE THVALED
;THUS, THSEL SERVES THE PURPOSE OF REFERENCING THE TRACE AND BREAK
;PREDICATES OF PARTICULAR THMS ON THTRACE

(DEFUN THSEL (THF) (PROG (THX) (RETURN (AND (SETQ THX (ASSQ THL THTRACE))
					(SETQ THX (THF THX))
					(THVAL THX THALIST)))))


;MAKES A NAME WITH PREFIX X AND SUFFIX A UNIQUE NUMBER
(DEFUN THGENS FEXPR (X) (MAKNAM (NCONC (EXPLODE (CAR X))
				  (EXPLODE (SETQ THGENS (ADD1 THGENS))))))

(SETQ THGENS 0)


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