perm filename ATC.LSP[MRS,LSP] blob sn#709274 filedate 1983-05-02 generic text, type T, neo UTF8
(DECLARE (fasload struct fas dsk (mac lsp))
;(declare (fasload struct ofa dsk (mac lsp)))
;	 (*rset (nouuo t))
	 (mapex t)
	 (setq defmacro-for-compiling nil)
	 (*lexpr λ-UNSUBST QV-QUASI-UNSUBST NORMALIZE-CMPD-CONCEPT
		 ANALYZE-CMPD-CONCEPT NRML-ANL-YZE-LINFORMULA
		 DISPLAY POSPRINC )

	 (special QV-SUBSTLIST QUANT-LIST CURRENTPOS SUBSTLISTPTR GENVARINDEX
		  GENVAR-RANGES *CONCEPTS* ALPHABET REVERSE-ALPHABET
		  2-ALPHABETS ALPHA-NCONSES *NOPOINT -EM:LINEL- ANALYSIS-LIST
		  CNCPT-ANALYSIS-LIST ↑-MATRIX-ANALYSIS-LIST JUNCT-ANALYSIS-LIST
		  SUBSTPAIRS TERMCOPIES QUANTCOPIES *-ASCII AL-VARS RO-INDEX
		  YHπ-FLAG *WRITE-DO-LIST* )

	 (fixnum -EM:LINEL- CURRENTPOS TABVAL KEYNUM FORM-LENGTH CHARINDEX
		 COMPNUM EXPRS-LENGTH N LEAF-COUNTER LINK-COUNTER NUMBER
		 ↑-TALLY POS KL1-LENGTH KL2-LENGTH TALLY )

	 (SETQ *WRITE-DO-LIST*
		     '(SPACES DISPLAY POSPRINC GO TAB BREAK ERROR SETQ)
	       IBASE 10. BASE 10. )

	 (load '|nsublis.lsp|) )  ;; NOTE : This file must contain up-to-date
		;; copies of all *DEFUN definitions in both NWREP and DNET.

(SETQ *WRITE-DO-LIST* '(SPACES DISPLAY POSPRINC GO TAB BREAK ERROR SETQ))
(SETQ IBASE 10.  BASE 10.)
(SETQ PRINLEVEL 3.  PRINLENGTH 60.  -EM:LINEL- 65.)
				    ;; (this can cause a JONL compiler error)
(SETQ BACKQUOTE-EXPAND-WHEN 'READ)
(LINEL NIL 80)
(SETQ BREAK-POINTS '(|, |  | ∧ |  | ∨ |)	;; possibly also /:
      BREAK-BEFORE-POINTS '(|↑[|) )

(DEFSTRUCT (↑↓-TERM (TYPE TREE))
	   ↑↓-MARKER ↑↓-MATRIX )

(DEFSTRUCT (LT-QUANTIFIER (TYPE HUNK) (CONC-NAME LT-))
	   Q-DEPENDENCIES Q-DETERMINER QSORT-EXPR Q-SCOPE )

(DEFSTRUCT (ROLELINK (TYPE TREE))
	   ROLEMARK ARGUMENT )

(DEFSTRUCT (PFC-FORMULA (TYPE TREE))
	   PFC-CONCEPT ROLELINKS )
; PFC-FORMULA => (pred rlnk1 rlnk2 ... rlnkn) or (func rlnk1 rlnk2 ... rlnkn)
;		   or (connective rlnk1 rlnk2 ... rlnkn)

(DEFSTRUCT (ROLEXENTRY (TYPE TREE))
	   ROLENAME ROLEPHRASE )

(DEFSTRUCT (LT-λ-EXPR (TYPE TREE) (CONC-NAME LT-))
	   (λ-PREFIX (MAKE-LT-λ-PREFIX)) λ-SCOPE )

(DEFSTRUCT (LT-λ-PREFIX (TYPE TREE) (BUT-FIRST LT-λ-PREFIX) (CONC-NAME LT-))
	   (λ-MARK 'λ) PATHKEYLISTS )
; PATHKEYLISTS => ((<termsort> <pathkey> {<pathkey>} ... ) ... )

(DEFSTRUCT (PATHKEYLIST (TYPE TREE))
	   λ-TERMSORT PATHKEYS )

(DEFMACRO (ANTECEDENT defmacro-for-compiling 't) (LT-⊃-PROPO)
  `(ARGUMENT (ASSQ 'ANTECEDENT (ROLELINKS ,LT-⊃-PROPO))) )

(DEFMACRO (CONSEQUENT defmacro-for-compiling 't) (LT-⊃-PROPO)
  `(ARGUMENT (ASSQ 'CONSEQUENT (ROLELINKS ,LT-⊃-PROPO))) )

(DEFMACRO (CONSP defmacro-for-compiling 't) (EXPR)
   `(EQ (TYPEP ,EXPR) 'LIST) )

(DEFMACRO (*DEFUN defmacro-for-compiling 't) ((F-TYPE . F-NAME) ARGLIST . BODY)
  `(PROGN
      (PUTPROP (OR (GET ',F-NAME 'FUNCTIONS) 
		   (PUTPROP ',F-NAME (NCONS '|*DEFUN-plist|) 'FUNCTIONS))
	       ,(COND ((EQ (CAR BODY) '*SYN) `',(CADR BODY))
		      (T `'(LAMBDA ,ARGLIST ,@BODY)) )
	       ',F-TYPE )
      (LET ((OLDMACRO (GET ',F-TYPE 'MACRO))
	    (NEWMACRO '(LAMBDA (FORM)
			`(GET (GET ',(CDR FORM) 'FUNCTIONS) ',',F-TYPE) )) )
	   (COND ((AND OLDMACRO 
		       (NOT (EQUAL OLDMACRO NEWMACRO)) )
		  (TERPRI) (PRINC '|Macro |) (PRIN1 ',F-TYPE)
		  (PRINC '| already defined differently!|)
		  (BREAK *DEFUN) )) )
      (DEFUN ,F-TYPE MACRO (FORM)
	 `(GET (GET ',(CDR FORM) 'FUNCTIONS) ',',F-TYPE) ) ) )

(*DEFUN (ISA . COREROLE) (ROLEMARK LT-FORM)
   (MEMQ ROLEMARK (GET (PFC-CONCEPT LT-FORM) 'COREROLES)) )

(*DEFUN (THE-FOR:ROLELINK . ROLEPHRASE) (ROLELINK LT-FORM)
   (CDR (ASSQ (ROLEMARK ROLELINK) (GET (PFC-CONCEPT LT-FORM) 'ROLEXICON))) )

(*DEFUN (THE-OF:LT-QUANT . QSORT) (LT-QUANT)
   (LET* ((QSORTEXPR (LT-QSORT-EXPR LT-QUANT))
	  (ATOMICQSORTEXPR
	    (CASEQ (LT-TYPE QSORTEXPR)
	       (ATOMICPROPO QSORTEXPR)
	       (CONJ-PROPO (ARGUMENT (CAR (ROLELINKS QSORTEXPR)))) ) ) )
	 (COND ((EQ (PFC-CONCEPT ATOMICQSORTEXPR) 'CONCEPT) 
		  (NORMALIZE-TERMSORTEXPR
		   (CONS '↑
			 (COND ((ARGUMENT (ASSQ 'OBJECT-CATEGORY*
						(ROLELINKS ATOMICQSORTEXPR) )))
			       (T (TERMSORT
				   (ARGUMENT
				    (ASSQ 'OBJECT
					  (ROLELINKS ATOMICQSORTEXPR) ) ) )) ) ) ) )
	       (T (PFC-CONCEPT ATOMICQSORTEXPR)) )) )

(*DEFUN (THE-OF:LT-QUANT . DETERMINER) (LT-QUANT)
    *SYN CAR )
;   *SYN LT-Q-DETERMINER )  This usage causes an "; IMPROPER USE OF MACRO - EVAL"
; error message; what LISP doesn't like here is simply the fact that 
; LT-Q-DETERMINER is a macro.

(*DEFUN (THE-OF:LT-λ-PREFIX . PATHKEYLISTS) (λ-PREFIX)
    *SYN CDR )

(*DEFUN (THE-OF:LT-QUANT . QSORTEXPR) (LT-QUANTIFIER)
    (CXR 2 LT-QUANTIFIER) )

(*DEFUN (THE-OF:LT-QUANT . SCOPE) (LT-QUANTIFIER)
    (CXR 3 LT-QUANTIFIER) )

(*DEFUN (THE-OF:LINQUANT . DETERMINER) (LINQUANT)
    (CAR LINQUANT) )

(*DEFUN (ISA-OF:LT . λ-EXPR) (LT-FORM)
   (AND (CONSP LT-FORM) (CONSP (CAR LT-FORM)) (MEMQ (CAAR LT-FORM) '(λ LAMBDA))) )

; λ-pair: (<λ-mark> . <termsort-indicator>)
; λ-mark: λ
; termsort-indicator: either <termsort-atom> or (<↑-marker> . <termsort-atom>)
; ↑-marker: either ↑ or ↑n , n being a digit such that 2≤n≤9.
(*DEFUN (ISA . λ-PAIR) (LT-FORM)
  (AND (CONSP LT-FORM)
       (EQ 'λ (CAR LT-FORM))
       (OR (SYMBOLP (CDR LT-FORM))
	   (AND (SYMBOLP (CADR LT-FORM))
		(EQ '↑ (GETCHAR (CADR LT-FORM) 1)) ) ) ) )

;; QUANT-TERMs are also known as a QT-PAIRs.
(DEFMACRO (ISA-QUANT-TERM defmacro-for-compiling 't) (LT-FORM)
 `(AND (CONSP ,LT-FORM)
       (EQ 'QUANT-TERM (CAR ,LT-FORM)) ) )

(*DEFUN (ISA-OF:LT . SORT) (PFC-CONCEPT)
  (LET  ((CONCEPT-CATEGORY (GET PFC-CONCEPT 'CATEGORY)))
	(OR (EQ 'SORT CONCEPT-CATEGORY)
	    (SUPERSORT* 'SORT CONCEPT-CATEGORY) ) ) )

(*DEFUN (ISA . SORT-ATTR-CATEGORY) (CATEGORY)
   (OR (MEMQ CATEGORY '(SORT ATTRIBUTE))
       (SUPERSORT* 'SORT CATEGORY)
       (SUPERSORT* 'ATTRIBUTE CATEGORY) ) )

(*DEFUN (ISA-OF:LT . PFC-FORMULA) (LT-FORM)
  (COND ((NOT (CONSP LT-FORM)) NIL)
	(T (LET ((CARFORM-CATEGORY (GET (CAR LT-FORM) 'CATEGORY)))
		(AND CARFORM-CATEGORY
		     (OR (MEMQ CARFORM-CATEGORY '(FUNCTION CONNECTIVE))
			 (#.(ISA . SORT-ATTR-CATEGORY) CARFORM-CATEGORY) ) ) )) ) )

; this fn tests whether FORM is a pattern-variable (either simple or complex).
(DEFUN ISA-PATT-VARIABLE? (FORM)
  (OR (AND (SYMBOLP FORM)
	   (MEMQ (GETCHAR FORM 1) '(? *)) )
      (AND (CONSP FORM)
	   (MEMQ (CAR FORM) '($R $IR $CHOOSE)) ) ) )

(*DEFUN (ISA . PATT-VARIABLE) (FORM)
   (OR (AND (SYMBOLP FORM)
	    (MEMQ (GETCHAR FORM 1) '(? *)) )
       (AND (CONSP FORM)
	    (MEMQ (CAR FORM) '($R $IR $CHOOSE)) ) ) )
;	    (MEMQ (CAR FORM) '($R $IR $CHOOSE RESTRICT IRESTRICT)) ) ) )

(*DEFUN (ISA . *-PATT-VARIABLE) (FORM)
   (OR (AND (SYMBOLP FORM)
	    (EQ (GETCHAR FORM 1) '*) )
       (AND (CONSP FORM)
	    (MEMQ (CAR FORM) '($R $IR))
	    (EQ (GETCHAR (CADR FORM) 1) '*) ) ) )

(*DEFUN (ISA . BREAK-BEFORE-POINT) (PRINTATOM)
   (AND (SYMBOLP PRINTATOM)
	(EQ '↑ (GETCHAR PRINTATOM 1))
	(OR (EQ '/[ (GETCHAR PRINTATOM 2))
	    (EQ '/[ (GETCHAR PRINTATOM 3)) ) ) )
;	(EQ '/[ (CAR (LAST (EXPLODE PRINATOM)))) ) ) ;; too much consing

(*DEFUN (ISA . BREAK-POINT) (PRINTATOM)
   (MEMQ PRINTATOM BREAK-POINTS) )

(*DEFUN (ISA . ROLELINK) (LT-FORM)
   (AND (CONSP LT-FORM) (EQ (GET (CAR LT-FORM) 'CATEGORY) 'ROLEMARK)) )

(*DEFUN (ISA-OF:LIN . QUANTIFIER) (LINFORM)
   (EQ (GET (CAR LINFORM) 'CATEGORY) 'DETERMINER) )

(*DEFUN (ISA-OF:LT . QUANTIFIER) (LT-FORM)
   (EQ (GET (#.(THE-OF:LT-QUANT . DETERMINER) LT-FORM) 'CATEGORY) 'DETERMINER) )

(DEFMACRO LAMBDA-OPR (OBJ)
   `(MEMQ (CAAR ,OBJ) '(LAMBDA λ)) )

(DEFMACRO (E:DO defmacro-for-compiling 't) (STRING)
  `(EM:ECOMMANDS (EXPLODEC ,STRING)) )

(DEFMACRO (E:VAR defmacro-for-compiling 't) (VARNAME)
  `(CDAR (EM:READONLY-VARS '(,VARNAME))) )

(DEFUN E:SETLINE (NUMBER)
  (LET ((CHAR-LIST))
       (SETQ *NOPOINT T)
       (SETQ CHAR-LIST (APPEND (MAPCAN #'(LAMBDA (P D) (LIST P D))
				       '(α α α α α)
				       (EXPLODEC NUMBER) )
			       '(α L) ))
       (SETQ *NOPOINT NIL)
       (EM:ECOMMANDS CHAR-LIST) ) )

(DEFMACRO (ADDCONC defmacro-for-compiling 't) (ADDLIST BASELISTATOM)
   `(SETQ ,BASELISTATOM (NCONC ,ADDLIST ,BASELISTATOM)) )

(DEFMACRO (ENDCONC defmacro-for-compiling 't) (ADDLIST BASELISTATOM)
   `(COND (,BASELISTATOM (NCONC ,BASELISTATOM ,ADDLIST))
	  (T (SETQ ,BASELISTATOM ,ADDLIST)) ) )

(DEFMACRO (ENDADD defmacro-for-compiling 't) (ADDITEM BASELISTATOM)
  `(COND (,BASELISTATOM (NCONC ,BASELISTATOM (NCONS ,ADDITEM)))
	 (T (SETQ ,BASELISTATOM (NCONS ,ADDITEM))) ) )

(DEFMACRO (RASSQ defmacro-for-compiling 't) (KEY A-LIST)
   `(DO ((A-TAIL ,A-LIST (CDR A-TAIL)))
	((NULL A-TAIL))
	(COND ((EQ (CDAR A-TAIL) ,KEY) (RETURN (CAR A-TAIL)))) ) )

(DEFMACRO (EDITXDO defmacro-for-compiling 't) (EXPR &rest BODY)
  `(PROGN (EDIT1 ,EXPR) . 
	 ,(MAPCAR '(LAMBDA (CMD) `(%EVALUATE ',CMD)) BODY) ) )

(DEFMACRO (EDITDO defmacro-for-compiling 't) (&rest BODY)
  `(PROGN . ,(MAPCAR '(LAMBDA (CMD) `(%EVALUATE ',CMD)) BODY) ) )

(DEFMACRO (COPYLIST defmacro-for-compiling 't) (LIST)
  `(APPEND ,LIST NIL) )

(DEFMACRO (BUTLAST defmacro-for-compiling 't) (LIST)
  `(NREVERSE (CDR (REVERSE ,LIST))) )

(DEFMACRO (REPEAT defmacro-for-compiling 't) (NUMBERVAR FORM)
  `(DO ((TALLY ,NUMBERVAR (1- TALLY)))
       ((ZEROP TALLY))
       ,FORM ) )

(DEFMACRO (SETF* defmacro-for-compiling 't) (SETFORM VALUEFORM)
  (LIST 'SETF SETFORM (NSUBLIS `((-*- . ,SETFORM)) VALUEFORM)) )

(DEFMACRO (SOME defmacro-for-compiling 't) (LIST PREDICATE . &opt:STEP-FUNCTION)
  (SETF* PREDICATE (EVAL -*-))
  (COND (&opt:STEP-FUNCTION (SETF* &opt:STEP-FUNCTION (EVAL -*-))))
  `(DO ((LISTAIL ,LIST (,(COND (&opt:STEP-FUNCTION
				 (CAR &opt:STEP-FUNCTION) )
			       (T 'CDR) )
			  LISTAIL )))
       ((NULL LISTAIL) NIL)
       (COND ((,PREDICATE (CAR LISTAIL)) (RETURN LISTAIL))) ) )

(DEFMACRO (ALL defmacro-for-compiling 't) (LIST PREDICATE . &opt:STEP-FUNCTION)
  (SETF* PREDICATE (EVAL -*-))
  (COND (&opt:STEP-FUNCTION (SETF* &opt:STEP-FUNCTION (EVAL -*-))))
  `(DO ((LISTAIL ,LIST (,(COND (&opt:STEP-FUNCTION
				 (CAR &opt:STEP-FUNCTION) )
			       (T 'CDR) )
			  LISTAIL )))
       ((NULL LISTAIL) T)
       (COND ((NOT (,PREDICATE (CAR LISTAIL))) (RETURN NIL))) ) )

; Definition of SUBSET for LISP-Machine:
;  (DEFMACRO SUBSET (LIST PREDICATE)
;    `(REM-IF-NOT ,PREDICATE ,LIST) )

(DEFMACRO (SUBSET defmacro-for-compiling 't) (LIST PREDICATE)
  (SETQ PREDICATE (EVAL PREDICATE))
  `(MAPCAN #'(LAMBDA (MEMBER)
	       (COND ((,PREDICATE MEMBER) (NCONS MEMBER))) )
	   ,LIST ) )

(DEFUN GOOD-NREVERSE (LIST)
   (COND ((OR (NULL LIST) (NULL (CDR LIST))) LIST)
	 ((OR (NULL (CDDR LIST)) (NULL (CDDDR LIST)))
	     (LET ((REMEM (CAR (LAST LIST))))
		  (RPLACA (LAST LIST) (CAR LIST))
		  (RPLACA LIST REMEM) ) )
	 (T (PROG (TRAILER POINTER LEADER)
		  (SETQ TRAILER (CDR LIST)
			POINTER (CDR TRAILER)
			LEADER (CDR POINTER) )
	      RPT (RPLACD POINTER TRAILER)
		  (COND ((CDR LEADER) (SETQ TRAILER POINTER
					    POINTER LEADER
					    LEADER (CDR LEADER) )
				      (GO RPT) ))
		  (RPLACD (CDR LIST) LEADER)
		  (RPLACD LIST POINTER)
		  (SETQ TRAILER (CAR LEADER))
		  (RPLACA LEADER (CAR LIST))
		  (RETURN (RPLACA LIST TRAILER)) ) ) ) )

(DEFUN NSUBLIS (A-LIST S-EXPR &aux SUBSTPAIR)
  (COND ((CONSP S-EXPR)
	   (COND ((CONSP (CAR S-EXPR)) (NSUBLIS A-LIST (CAR S-EXPR)))
		 ((SETQ SUBSTPAIR (ASSQ (CAR S-EXPR) A-LIST))
		    (RPLACA S-EXPR (CDR SUBSTPAIR)) ) )
	   (COND ((CONSP (CDR S-EXPR)) (NSUBLIS A-LIST (CDR S-EXPR)))
		 ((SETQ SUBSTPAIR (ASSQ (CDR S-EXPR) A-LIST))
		    (RPLACD S-EXPR (CDR SUBSTPAIR)) ) )
	   S-EXPR )
	((COND ((SETQ SUBSTPAIR (ASSQ S-EXPR A-LIST)) (CDR SUBSTPAIR))
	       (S-EXPR) )) ) )

(DEFMACRO (HUNKQUANTP defmacro-for-compiling 't) (LT-FORM)
   `(AND (HUNKP ,LT-FORM)
	 (EQ 'DETERMINER (GET (LT-Q-DETERMINER ,LT-FORM) 'CATEGORY)) ) )

(DEFMACRO HUNK-UQUANTP (LT-FORM)
   `(AND (HUNKP ,LT-FORM)
	 (EQ '∀ (LT-Q-DETERMINER ,LT-FORM)) ) )

; QNSUBLIS is used to replace variables with qt-pairs in input formulas.
(DEFUN QNSUBLIS (A-LIST S-EXPR)
  (COND ((CONSP S-EXPR)
	  (COND ((CONSP (CAR S-EXPR)) (QNSUBLIS A-LIST (CAR S-EXPR)))
		((AND (SYMBOLP (CAR S-EXPR))
		      (MEMQ (GET (GETCHAR (CAR S-EXPR) 1) 'LT-TYPE)
			    '(VARIABLE SYNTACTIC-MARKER) ) )
		 ;;(currently, this is used only when S-EXPR is a FIXNUM-VECTOR)
		  (LET ((SUBSTPAIR (ASSQ (CAR S-EXPR) A-LIST)))
		       (COND (SUBSTPAIR (RPLACA S-EXPR (CDR SUBSTPAIR)))) ) ) )
	  (COND ((OR (CONSP (CDR S-EXPR)) (HUNKQUANTP (CDR S-EXPR)))
		  (QNSUBLIS A-LIST (CDR S-EXPR)) )
		((AND (SYMBOLP (CDR S-EXPR))
		      (MEMQ (GET (GETCHAR (CDR S-EXPR) 1) 'LT-TYPE)
			    '(VARIABLE SYNTACTIC-MARKER) ) )
		  (LET ((SUBSTPAIR (ASSQ (CDR S-EXPR) A-LIST)))
		       (COND (SUBSTPAIR (RPLACD S-EXPR (CDR SUBSTPAIR)))) ) ) )
	  S-EXPR )
	((HUNKQUANTP S-EXPR)
	  (QNSUBLIS A-LIST (LT-QSORT-EXPR S-EXPR))
	  (QNSUBLIS A-LIST (LT-Q-SCOPE S-EXPR))
	  S-EXPR )
	((ATOM S-EXPR) S-EXPR)
	(T (BREAK |QNSUBLIS - unrecognized type of S-EXPR.|)) ) )

(DEFMACRO CONDCARPUSH (PREDEXPR PUSHEXPR STACKEXPR)
  (SETQ PUSHEXPR (NSUBLIS `((-*- . ,PREDEXPR)) PUSHEXPR))
  (SETQ STACKEXPR (NSUBLIS `((-*- . ,PREDEXPR)) STACKEXPR))
  `(COND (,PREDEXPR (CAR (PUSH ,PUSHEXPR ,STACKEXPR)))
	 (T ,PUSHEXPR) ) )

(DEFMACRO (WRITE defmacro-for-compiling 't) BODY
 `(PROGN
    ,@(MAPCAN #'(LAMBDA (X)
		  (COND ((EQ X 'T) (NCONS '(TERPRI)))
			((EQ X 'T*) (LIST '(TERPRI) '(SETQ CURRENTPOS 1)))
			((ATOM X) (NCONS `(PRINC ,X)))
			((CONSP X)
			   (COND ((MEMQ (CAR X) *WRITE-DO-LIST*)
				    (NCONS X) )
				 ((EQ '1* (CAR X))
				    (NCONS `(PRIN1 ,(CDR X))) )
				 ((EQ 'IF* (CAR X))
				    (NCONS `(LET ((VAL ,(CDR X)))
						 (COND (VAL (PRINC VAL))) )) )
				 (T (NCONS `(PRINC ,X))) ) ) ) )
	      BODY ) ) )

(DEFUN SPACES (N)
  (DO ((TALLY N (1- TALLY)))
      ((ZEROP TALLY) T)
      (PRINC '/ ) ) )

(DEFMACRO NORMALIZE-CONNECTIVE (PFC-CONCEPT)
   `(LET ((PFC-CONCEPT ,PFC-CONCEPT))
	 (CASEQ PFC-CONCEPT
	   ((∧ & AND) '∧)
	   ((∨ OR) '∨)
	   ((¬ ~ NOT) '¬)
	   ((⊃ M-ONLYIF) '⊃)
	   (T PFC-CONCEPT) ) ) )

(DEFUN E-LIN (INPUTFORM)
  (ENCODE-LINFORMULA INPUTFORM) )

; E-LIN-C preserves INPUTFORM unchanged by encoding a copy of it.
(DEFUN E-LIN-C (INPUTFORM)
  (ENCODE-LINFORMULA (SUBST () () INPUTFORM)) )

; To avoid unnecessary CONSing, ENCODE-LINFORMULA destructively fashions the
;  encoded formula directly from the input formula.  In the rare cases where
;  this might cause a problem, one should use E-LIN-C instead.
(DEFUN ENCODE-LINFORMULA (FORM &aux QV-SUBSTLIST)
   (LET ((ENCODED-LINFORMULA-S (ENCODE-LINFORMULA-S FORM NIL)))
	(QNSUBLIS QV-SUBSTLIST ENCODED-LINFORMULA-S) ) )

(DEFMACRO SETUPQUANTS (QUANTLIST NEWMATRIX)
   `(DO ((QUANTAIL ,QUANTLIST (CDR QUANTAIL)))
	((NULL (CDR QUANTAIL))
	   (PUSH (CONS (LT-Q-SCOPE (CAR QUANTAIL))
		       (CONS 'QUANT-TERM (CAR QUANTAIL)) )
		 QV-SUBSTLIST )
	   ;; QV-SUBSTLIST: ((<variable> . <qt-pair>) ...)
	   (SETF (LT-Q-SCOPE (CAR QUANTAIL)) ,NEWMATRIX) )
	(PUSH (CONS (LT-Q-SCOPE (CAR QUANTAIL))
		    (CONS 'QUANT-TERM (CAR QUANTAIL)) )
	      QV-SUBSTLIST )
	(SETF (LT-Q-SCOPE (CAR QUANTAIL)) (CADR QUANTAIL)) ) )

(DEFMACRO ORDER-PATHKEYS (PATHKEYLIST)
  `(SORT ,PATHKEYLIST #'ALPHALESSP) )

; ENCODE-LINFORMULA-S uses the variable QV-SUBSTLIST freely.
(DEFUN ENCODE-LINFORMULA-S (FORM QUANT-LIST)
    ;; QUANT-LIST is used to record quantifier dependencies (see ENCODE-QUANT).
  (CASEQ (LINTYPE FORM)
     ((ATOMICPROPO F-TERM)
	(TRANSFORM-ROLELINKS FORM)
        (MAPC #'(LAMBDA (RLNK) 
		  (COND ((#.(ISA . *-PATT-VARIABLE) RLNK))
			((NULL (ARGUMENT RLNK)))
			(T (SETF* (ARGUMENT RLNK)
				  (ENCODE-LINFORMULA-S -*- QUANT-LIST) )) ) )
	      (ROLELINKS FORM))
	(SETF (ROLELINKS FORM) (ORDER-ROLELINKS FORM))
	;; note that the rolelinks of all contained wffs will already have been
	;;  ordered by recursive calls to ENCODE-LINFORMULA-S, and so will be
	;;  usable to help normalize the order of rolelinks at this level.
	FORM )
     (CONNPROPO
        (RPLACA FORM (NORMALIZE-CONNECTIVE (CAR FORM)))
	(TRANSFORM-ROLELINKS FORM)
        (MAPC #'(LAMBDA (RLNK) 
		  (SETF* (ARGUMENT RLNK) (ENCODE-LINFORMULA-S -*- QUANT-LIST)) )
	      (ROLELINKS FORM) )
	FORM )
     (QUANTPROPO
        (LET ((QUANTLIST (MAPCAN (FUNCTION ENCODE-QUANT) (BUTLAST FORM)))
	      (NEWMATRIX (ENCODE-LINFORMULA-S (CAR (LAST FORM)) QUANT-LIST)) )
;	     (break E-L:test0)
	     (SETUPQUANTS QUANTLIST NEWMATRIX)
;	     (break E-L:test1)
	     (CAR QUANTLIST) ) )
     ((SIMPLETERM FIXNUM-VECTOR PATT-VARIABLE BQ-TERM)
	FORM)
     (↑↓-TERM
 	(RPLACD FORM (CADR FORM))
	(SETF* (↑↓-MATRIX FORM) (ENCODE-LINFORMULA-S -*- QUANT-LIST))
	FORM )
     (λ-EXPR
        (RPLACD FORM (ENCODE-LINFORMULA-S (CADR FORM) QUANT-LIST))
	(MAP #'(LAMBDA (VARLISTAIL)
		 (LET ((PKEYLIST
			 (MAKE-PATHKEYLIST PATHKEYS
					   (ORDER-PATHKEYS
					     (MAPCAR #'IMPLODE
						     (QV-QUASI-UNSUBST
						           (CAR VARLISTAIL)
							   (LT-λ-SCOPE FORM) ) ) ) ) ))
		      (ADJUST-λ-TERMSORT PKEYLIST FORM)
		      (SETF (CAR VARLISTAIL) PKEYLIST) ) )
	     (CDAR FORM) )
	(SETF* (LT-PATHKEYLISTS FORM) (ORDER-PATHKEYLISTS -*-))
	(λ-UNSUBST FORM NIL) )
     (T (BREAK |ENCODE-LINFORMULA-S - unrecognized formula type.|)) ) )

; TRANSFORM-ROLELINKS needs to be generalized to deal with the case in which
; a pfc-formula has variably many identical coreroles, and also several
; different non-core role arguments.
; (TRANSFORM-ROLELINKS <pfc-formula>)
(DEFUN TRANSFORM-ROLELINKS (PFC-FORM &aux VARGFLAG)
  (COND ((EQ (GET (PFC-CONCEPT PFC-FORM) 'COREROLE-NUMBER) 'VARIABLE)
	   (SETQ VARGFLAG T) ))
  (DO ((ROLINKS (ROLELINKS PFC-FORM) (CDR ROLINKS))
       (CR-MARKS (GET (PFC-CONCEPT PFC-FORM) 'COREROLES) 
		 (COND (VARGFLAG CR-MARKS) (T (CDR CR-MARKS))) ) )
      ((NULL ROLINKS))
      (COND ((#.(ISA . *-PATT-VARIABLE) (CAR ROLINKS)))
	    (CR-MARKS (RPLACA ROLINKS (MAKE-ROLELINK ROLEMARK (CAR CR-MARKS) 
						     ARGUMENT (CAR ROLINKS) )))
	    (T (RPLACD (CAR ROLINKS) (CADAR ROLINKS))
	       (COND ((NOT (#.(ISA . PATT-VARIABLE) (CAAR ROLINKS)))
		       (RPLACA (CAR ROLINKS) 
			       (CAR (RASSQ (CAAR ROLINKS)
					   (GET (PFC-CONCEPT PFC-FORM)
						'ROLEXICON ) )) ) )) ) ) ) )

(DEFMACRO NORMALIZE-DETERMINER (DET)
   `(CASEQ ,DET
       ((∀ ALL EVERY) '∀)
       ((∃ SOME EXIST) '∃)
       ((GREAT-MAJORITY MOST) ,DET)
       (THE ,DET)
       (!1 ,DET)
       (T (WRITE T '|; unrecognized determiner: | ,DET
		 (BREAK NORMALIZE-DETERMINER) )) ) )

;(declare (gc))

; ENCODE-QUANT accesses and updates the freevar QUANT-LIST.  The information
;  in the Q-DEPENDENCIES slot of a quantifier is currently used by
;  ANALYZE-CMPD-CONCEPT in calling QV-QUASI-UNSUBST.  (LGC  2-29-83)
(DEFUN ENCODE-QUANT (QUANT)
   (DO ((DET (CAR QUANT))
	(VS-PAIRS (CDR QUANT) (CDDR VS-PAIRS)) 
	;; vs-pairs: (<variable> <qsortexpr> ...1 ...2 )
	(VAR-RANGE) (QSORTEXP) (QLIST) )
       ((NULL VS-PAIRS) (GOOD-NREVERSE QLIST))
       (SETQ VAR-RANGE (VARIABLE-RANGE (CAR VS-PAIRS)))
       (SETQ QSORTEXP (COND ((ATOM (CADR VS-PAIRS)) 
			       (LIST (CADR VS-PAIRS) (CAR VS-PAIRS)) )
			    (T (CADR VS-PAIRS)) ))
       (ENCODE-LINFORMULA-S QSORTEXP QUANT-LIST)
       (PUSH (MAKE-LT-QUANTIFIER 
		Q-DETERMINER (NORMALIZE-DETERMINER DET)
		QSORT-EXPR QSORTEXP
		Q-SCOPE (CAR VS-PAIRS) ; variable here temporarily
		Q-DEPENDENCIES (COPYLIST QUANT-LIST) )
	     QLIST )
       (COND (QUANT-LIST (NCONC QUANT-LIST (NCONS (CAR QLIST))))
	     (T (SETQ QUANT-LIST (NCONS (CAR QLIST)))) ) ) )

(DEFUN CREATE-LT-WFF-NEGATION (LT-FORM)
  (COND ((EQ 'NEGPROPO (LT-TYPE LT-FORM))
	   (ARGUMENT (CAR (ROLELINKS LT-FORM))) )
	(T (MAKE-PFC-FORMULA
	      PFC-CONCEPT '¬
	      ROLELINKS (NCONS (MAKE-ROLELINK
				  ROLEMARK 'JUNCT
				  ARGUMENT LT-FORM )) )) ) )

(DEFUN VARIABLE-RANGE (VARIABLE &aux ↑-MARK)
   (SETQ VARIABLE (EXPLODEC VARIABLE))
   (COND ((EQ '↑ (CAR VARIABLE))
	   (COND ((EQ 'VARIABLE (GET (CADR VARIABLE) 'LT-TYPE))
		   ;; (we assume an ↑-number of at most one digit)
		    (SETQ ↑-MARK '(↑)
			  VARIABLE (CDR VARIABLE) ))
		 (T (SETQ ↑-MARK (LIST '↑ (CADR VARIABLE))
			  VARIABLE (CDDR VARIABLE) )) ) ))
   (COND (↑-MARK (CONS (IMPLODE ↑-MARK) (GET (CAR VARIABLE) 'RANGE)))
	 (T (GET VARIABLE 'RANGE)) ) )

(DEFUN GETFORMULA (SOURCE)
  (COND ((EQ SOURCE 'TTY) (WRITE T '|LISP-form input, please: |) 
			  (PROG1 (READ) (WRITE T '|Thank you. |)) )
	(T (BREAK |GETFORMULA - unrecognized input source.|)) ) )

; the 'Q' connotes "EQ" and "ASSQ"
(DEFMACRO A-Q-GET (A-LIST INDICATOR)
  `(CDR (ASSQ ,INDICATOR ,A-LIST)) )

(DEFMACRO (ATC-GET defmacro-for-compiling 't) (GENL-PLIST INDICATOR)
  `(LET ((GENL-PLIST ,GENL-PLIST))
	(COND ((AND YHπ-FLAG (π-YH-UNITP GENL-PLIST))
	         (π-GET GENL-PLIST ,INDICATOR) )
	      (T (GET GENL-PLIST ,INDICATOR)) ) ) )

(DEFMACRO GET-F-DESCRIPT (LT-UNIT ATTRIBUTE)
 `(A-Q-GET (ATC-GET ,LT-UNIT 'F-DESCRIPTS) ,ATTRIBUTE) )

; An alternative, less efficient definition of ATC-GET
;(DEFMACRO ATC-GET (GENL-PLIST INDICATOR)
; `(LET ((GENL-PLIST ,GENL-PLIST))
;	(COND ((OR (AND (CONSP GENL-PLIST) (EQ '*CC-PLIST* (CAR GENL-PLIST)))
;		   (NULL YHπ-FLAG)
;		   (AND YHπ-FLAG (NOT (π-YH-UNITP GENL-PLIST))) )
;	         (GET GENL-PLIST ,INDICATOR) )
;	      (T (π-GET GENL-PLIST ,INDICATOR)) ) ) )

(DEFMACRO (ATC-PLIST defmacro-for-compiling 't) (GENL-PLIST)
  `(LET ((GENL-PLIST ,GENL-PLIST))
	(COND ((AND YHπ-FLAG (π-YH-UNITP GENL-PLIST))
	         (π-PLIST GENL-PLIST) )
	      (T (PLIST GENL-PLIST)) ) ) )
(DEFUN LINTYPE (LISPINPUTFORM &aux CAR:FORM-CATEGORY)
  (COND ((NULL LISPINPUTFORM) (BREAK |LINTYPE - null input form!|)) 
	((#.(ISA . PATT-VARIABLE) LISPINPUTFORM) 'PATT-VARIABLE)
	((ATOM LISPINPUTFORM) 'SIMPLETERM) 
	((NOT (CONSP LISPINPUTFORM))
	   (WRITE T '|; unexpected input form: | LISPINPUTFORM
		  (BREAK LINTYPE) ) )
	((SYMBOLP (CAR LISPINPUTFORM)) 
	   (COND ((EQ '|`| (GETCHAR (CAR LISPINPUTFORM) 1)) 'BQ-TERM)
		 ((EQ 'SYNTACTIC-MARKER
		      (GET (GETCHAR (CAR LISPINPUTFORM) 1) 'LT-TYPE) )
		    '↑↓-TERM )
		 ((NULL (SETQ CAR:FORM-CATEGORY
			      (GET (NORMALIZE-CONNECTIVE (CAR LISPINPUTFORM))
				   'CATEGORY ) ) )
		    (WRITE T '|; No category for: | (CAR LISPINPUTFORM)
			   (BREAK LINTYPE) ) )
		 ((EQ 'FUNCTION CAR:FORM-CATEGORY) 'F-TERM)
		 ((EQ 'CONNECTIVE CAR:FORM-CATEGORY) 'CONNPROPO)
		 ((#.(ISA . SORT-ATTR-CATEGORY) CAR:FORM-CATEGORY)
		    'ATOMICPROPO )
		 (T (WRITE T '|; unrecognized input form: | LISPINPUTFORM
			   (BREAK LINTYPE) )) ) )
	((FIXP (CAR LISPINPUTFORM)) 'FIXNUM-VECTOR)
	(T (COND ((EQ 'DETERMINER
		      (GET (#.(THE-OF:LINQUANT . DETERMINER) (CAR LISPINPUTFORM))
			   'CATEGORY ) ) 'QUANTPROPO )
		 ((EQ 'LAMBDA-DETERMINER
		      (GET (#.(THE-OF:LINQUANT . DETERMINER) (CAR LISPINPUTFORM))
			   'CATEGORY ) ) 'λ-EXPR )
		 (T (WRITE T '|; unrecognized input form: | LISPINPUTFORM
			   (BREAK LINTYPE) )) )) ) )

; This *-version of LINTYPE does not break, and can serve as part of a
;  recognizer for input LISP-form logical formulas.
(DEFUN LINTYPE* (LISPINPUTFORM &aux CAR:FORM-CATEGORY)
  (COND ((NULL LISPINPUTFORM) (WRITE '|; null linformula!|) NIL) 
	((#.(ISA . PATT-VARIABLE) LISPINPUTFORM) 'PATT-VARIABLE)
	((ATOM LISPINPUTFORM) 'SIMPLETERM) 
	((NOT (CONSP LISPINPUTFORM)) 'UNRECOGNIZED)
	((SYMBOLP (CAR LISPINPUTFORM)) 
	   (COND ((EQ '|`| (GETCHAR (CAR LISPINPUTFORM) 1)) 'BQ-TERM)
		 ((EQ 'SYNTACTIC-MARKER
		      (GET (GETCHAR (CAR LISPINPUTFORM) 1) 'LT-TYPE) )
		    '↑↓-TERM )
		 ((NULL (SETQ CAR:FORM-CATEGORY
			      (GET (NORMALIZE-CONNECTIVE (CAR LISPINPUTFORM))
				   'CATEGORY ) ) ) 'UNRECOGNIZED )
		 ((EQ 'FUNCTION CAR:FORM-CATEGORY) 'F-TERM)
		 ((EQ 'CONNECTIVE CAR:FORM-CATEGORY) 'CONNPROPO)
		 ((#.(ISA . SORT-ATTR-CATEGORY) CAR:FORM-CATEGORY)
		    'ATOMICPROPO )
		 (T 'UNRECOGNIZED) ) )
	((FIXP (CAR LISPINPUTFORM)) 'FIXNUM-VECTOR)
	(T (COND ((EQ 'DETERMINER
		      (GET (#.(THE-OF:LINQUANT . DETERMINER) (CAR LISPINPUTFORM))
			   'CATEGORY ) ) 'QUANTPROPO )
		 ((EQ 'LAMBDA-DETERMINER
		      (GET (#.(THE-OF:LINQUANT . DETERMINER) (CAR LISPINPUTFORM))
			   'CATEGORY ) ) 'λ-EXPR )
		 (T 'UNRECOGNIZED) )) ) )

(DEFMACRO (UQ-KERNEL defmacro-for-compiling 't) (LT-QUANTIFIERFORM)
 `(DO ((CURR-SUB-EXPR ,LT-QUANTIFIERFORM (LT-Q-SCOPE CURR-SUB-EXPR)))
      ((NOT (HUNK-UQUANTP CURR-SUB-EXPR))
         CURR-SUB-EXPR ) ) )

(DEFMACRO (UQ-⊃-KERNEL defmacro-for-compiling 't) (LT-QUANTIFIERFORM)
 `(DO ((CURR-SUB-EXPR ,LT-QUANTIFIERFORM (LT-Q-SCOPE CURR-SUB-EXPR)))
      ((NOT (HUNK-UQUANTP CURR-SUB-EXPR))
         (CONSEQUENT CURR-SUB-EXPR) ) ) )

(DEFMACRO UQ-KERNEL-LT-TYPE (LT-QUANTIFIERFORM)
 `(LT-TYPE (UQ-KERNEL ,LT-QUANTIFIERFORM)) )

(declare (gc))

(DEFUN LT-TYPE (LT-FORM)
  (COND ((NULL LT-FORM) (WRITE T  '|; LT-FORM is null!|  (BREAK LT-TYPE)))
	((#.(ISA . PATT-VARIABLE) LT-FORM) 'PATT-VARIABLE)
	((ATOM LT-FORM) 'SIMPLEFORM) 
	((#.(ISA-OF:LT . QUANTIFIER) LT-FORM) 'QUANTIFIERFORM) 
	((NOT (CONSP LT-FORM)) (WRITE T  '|; LT-form |  LT-FORM
				      '| is unacceptable!| (BREAK LT-TYPE:ua1) ))
	((SYMBOLP (CAR LT-FORM)) 
	  (LET ((CARFORM-CATEGORY (GET (CAR LT-FORM) 'CATEGORY)))
	       (CASEQ CARFORM-CATEGORY
		 (FUNCTION 'F-TERM)
		 (CONNECTIVE
		   (CASEQ (CAR LT-FORM)
		     (¬ 'NEGPROPO)
		     (∧ 'CONJ-PROPO)
		     (∨ 'DISJ-PROPO)
		     (⊃ '⊃-PROPO)
		     (⊃-THEN '⊃-THEN-PROPO)
		     (IF-WOULD 'IF-WOULD-PROPO)
		     (IF-THENWOULD 'IF-THENWOULD-PROPO)
		     (T (BREAK |LT-TYPE - unacceptable connective!|)) ) )
		 (ROLEMARK 'ROLELINK)
		 (T (COND ((EQ 'QUANT-TERM (CAR LT-FORM)) 'QT-PAIR)
			  ((EQ 'λ (CAR LT-FORM)) 'λ-PAIR)
			  ((CASEQ (GETCHAR (CAR LT-FORM) 1)
			     (↑ '↑-TERM)
			     (↓ '↓-TERM)
			     (T NIL) ))
			  ((AND CARFORM-CATEGORY
				(#.(ISA . SORT-ATTR-CATEGORY) CARFORM-CATEGORY))
			     'ATOMICPROPO )
			  (T (BREAK |LT-TYPE - unrecognized type:1|)) )) ) ) )
	((FIXP (CAR LT-FORM)) 'FIXNUM-VECTOR)
	((AND (CONSP (CAR  LT-FORM)) (MEMQ (CAAR LT-FORM) '(λ LAMBDA))) 'λ-EXPR)
	(T (BREAK |LT-TYPE - unrecognized type:2|)) ) )

; This *-version of LT-TYPE does not break, and can serve as part of a
;  recognizer for logical formulas in the internal Language of Thought.
(DEFUN LT-TYPE* (LT-FORM)
  (COND ((NULL LT-FORM) (WRITE T  '|; LT-FORM is null!|) NIL)
	((#.(ISA . PATT-VARIABLE) LT-FORM) 'PATT-VARIABLE)
	((ATOM LT-FORM) 'SIMPLEFORM) 
	((#.(ISA-OF:LT . QUANTIFIER) LT-FORM) 'QUANTIFIERFORM) 
	((NOT (CONSP LT-FORM)) 'UNRECOGNIZED)
	((SYMBOLP (CAR LT-FORM)) 
	  (LET ((CARFORM-CATEGORY (GET (CAR LT-FORM) 'CATEGORY)))
	       (CASEQ CARFORM-CATEGORY
		 (FUNCTION 'F-TERM)
		 (CONNECTIVE
		   (CASEQ (CAR LT-FORM)
		     (¬ 'NEGPROPO)
		     (∧ 'CONJ-PROPO)
		     (∨ 'DISJ-PROPO)
		     (⊃ '⊃-PROPO)
		     (⊃-THEN '⊃-THEN-PROPO)
		     (IF-WOULD 'IF-WOULD-PROPO)
		     (IF-THENWOULD 'IF-THENWOULD-PROPO)
		     (T 'UNRECOGNIZED) ) )
		 (ROLEMARK 'ROLELINK)
		 (T (COND ((EQ 'QUANT-TERM (CAR LT-FORM)) 'QT-PAIR)
			  ((EQ 'λ (CAR LT-FORM)) 'λ-PAIR)
			  ((CASEQ (GETCHAR (CAR LT-FORM) 1)
			     (↑ '↑-TERM)
			     (↓ '↓-TERM)
			     (T NIL) ))
			  ((AND CARFORM-CATEGORY
				(#.(ISA . SORT-ATTR-CATEGORY) CARFORM-CATEGORY))
			     'ATOMICPROPO )
			  (T 'UNRECOGNIZED) )) ) ) )
	((FIXP (CAR LT-FORM)) 'FIXNUM-VECTOR)
	((AND (CONSP (CAR  LT-FORM)) (MEMQ (CAAR LT-FORM) '(λ LAMBDA))) 'λ-EXPR)
	(T 'UNRECOGNIZED) ) )

; A simplification of LT-TYPE for use in QV-QUASI-UNSUBST.  Does not distinguish
;  the various CONN-PROPOs, and omits some other discriminations.
(DEFUN LT-QQU-TYPE (LT-FORM)
  (COND ((NULL LT-FORM) (WRITE T  '|; LT-FORM is null!|  (BREAK LT-TYPE)))
;	((#.(ISA . PATT-VARIABLE) LT-FORM) 'PATT-VARIABLE)
	((ATOM LT-FORM) 'SIMPLEFORM) 
	((#.(ISA-OF:LT . QUANTIFIER) LT-FORM) 'QUANTIFIERFORM) 
	((NOT (CONSP LT-FORM)) (WRITE T  '|; LT-form |  LT-FORM
				      '| is unacceptable!| (BREAK LT-QQU-TYPE:ua1) ))
	((SYMBOLP (CAR LT-FORM)) 
	  (LET ((CARFORM-CATEGORY (GET (CAR LT-FORM) 'CATEGORY)))
	       (CASEQ CARFORM-CATEGORY
		 (FUNCTION 'F-TERM)
		 (CONNECTIVE 'CONN-PROPO)
;		 (ROLEMARK 'ROLELINK)
		 (T (COND ((EQ 'QUANT-TERM (CAR LT-FORM)) 'QT-PAIR)
			  ((EQ 'λ (CAR LT-FORM)) 'λ-PAIR)
			  ((CASEQ (GETCHAR (CAR LT-FORM) 1)
			     (↑ '↑-TERM)
			     (↓ '↓-TERM)
			     (T NIL) ))
			  ((AND CARFORM-CATEGORY
				(#.(ISA . SORT-ATTR-CATEGORY) CARFORM-CATEGORY))
			     'ATOMICPROPO )
			  (T (BREAK |LT-QQU-TYPE - unrecognized type:1|)) )) ) ) )
	((FIXP (CAR LT-FORM)) 'FIXNUM-VECTOR)
	((AND (CONSP (CAR  LT-FORM)) (MEMQ (CAAR LT-FORM) '(λ LAMBDA))) 'λ-EXPR)
	(T (BREAK |LT-QQU-TYPE - unrecognized type:2|)) ) )

; The var CURRENTPOS is used freely by DISPLAY and lower level print functions.
(DEFUN DISPLAY (LT-FORM &optional (CURRENTPOS 1) &aux (*NOPOINT T)
						      (-EM:LINEL- 85.) )
   (STRAIGHTPRIN (DPYLIST LT-FORM))
   CURRENTPOS )

(DEFUN DPYLIST (LT-FORM &aux (SUBSTLISTPTR (NCONS NIL))
			     (DPYLIST-SUBST (DPYLIST-S LT-FORM)) )
  (COND ((CAR SUBSTLISTPTR)
	   (VNSUBLIS (MAKE-QVLIST (CAR SUBSTLISTPTR)) DPYLIST-SUBST))
	(T DPYLIST-SUBST) ) )

(DEFUN VNSUBLIS (A-LIST DPYLIST)
;  (PRINT DPYLIST) (break vnsublis:test)
   (DO ((DPYTAIL DPYLIST (CDR DPYTAIL))
	(QV-PAIR) )
       ((NULL DPYTAIL) DPYLIST)
       (COND ((AND (NOT (ATOM (CAR DPYTAIL)))
		   (SETQ QV-PAIR (ASSQ (CAR DPYTAIL) A-LIST)) )
	        (RPLACA DPYTAIL (CDR QV-PAIR)) ) ) ) )

(DEFMACRO INITIALIZE-GENVARINDEX ()
   `(MAPC (FUNCTION (LAMBDA (RANGENTRY)
		       (RPLACA (CDR RANGENTRY) (CAADDR RANGENTRY))
		       (MAPC (FUNCTION (LAMBDA (VPAIR)
					  (RPLACD VPAIR 0) ))
			     (CDDR RANGENTRY) ) ))
	  GENVARINDEX ) )

(declare (gc))

; GENVAR accesses and updates the global variable GENVARINDEX
(DEFUN GENVAR (VARANGE &optional INITFLAG 
	    ;; VARANGE : either <varsort-atom> or (<↑-mark> . <varsort-atom>)
		       &aux VARLIST CURRENTBASEVAR CURRENTVAR ↑-MARK)
       (COND (INITFLAG (INITIALIZE-GENVARINDEX))
	     (T (COND ((CONSP VARANGE)
		         (SETQ ↑-MARK (CAR VARANGE)
			       VARANGE (CDR VARANGE) ) ) )
		(SETQ VARLIST (CDR (ASSQ VARANGE GENVARINDEX))
		      CURRENTBASEVAR (CAR VARLIST)
		      CURRENTVAR (ASSQ CURRENTBASEVAR (CDR VARLIST)) )
		;; varlist: (currentbasevar (basevar . current-subscript) ...)
		(OR VARLIST (WRITE T '|; no entry for variable-sort: | VARANGE
				   '| in GENVARINDEX.| (BREAK GENVAR) ))
		(PROG1 (COND ((AND (NULL ↑-MARK) (= 0 (CDR CURRENTVAR)))
			        CURRENTBASEVAR )
			     (T (IMPLODE `(,.(COND (↑-MARK (EXPLODE ↑-MARK)))
					   ,CURRENTBASEVAR 
					   ,.(COND
					       ((= 0 (CDR CURRENTVAR)) NIL)
					       (T (EXPLODE (CDR CURRENTVAR)))
						    			) ))) )
		       (RPLACD CURRENTVAR (1+ (CDR CURRENTVAR)))
		       (RPLACA VARLIST 
			       (COND ((CAADR (MEMQ CURRENTVAR (CDR VARLIST))))
				     (T (CAADR VARLIST)) ) ) ) ) ) )

(declare (gc))

(DEFMACRO TERMSORT-VARANGE (TERMFORM)
  `(LET* ((TERMFORM ,TERMFORM)
	  (TERMSORT
	    (COND ((#.(ISA-OF:LT . QUANTIFIER) TERMFORM)
		     (#.(THE-OF:LT-QUANT . QSORT) TERMFORM) )
		  ((#.(ISA . λ-PAIR) TERMFORM)
		     (CDR TERMFORM) )
		  (T (BREAK |TERMSORT-VARANGE - unrecognized termform type.|)) )) )
	 (OR TERMSORT (WRITE T '|; Null termsort for | TERMFORM
			  (BREAK TERMSORT-VARANGE) ))
	 (LET* ((↑-MARKER (COND ((CONSP TERMSORT) (CAR TERMSORT))))
		(BASE-RANGE (COND ((CONSP TERMSORT) (CDR TERMSORT))
				  (T TERMSORT) ))
		(BASE-VARANGE
		  (DO ((VARANGE? BASE-RANGE
				 (OR (GET VARANGE? 'SUPERSORT)
				     (WRITE T '|; No supersort for | VARANGE? 
					    (BREAK TERMSORT-VARANGE) ) ) ))
		      ((MEMQ VARANGE? GENVAR-RANGES) VARANGE?) ) ) )
	       (COND (↑-MARKER (CONS ↑-MARKER BASE-VARANGE))
		     (T BASE-VARANGE) ) ) ) )

;(declare (gc))

(DEFUN MAKE-QVLIST (SUBSTLIST)
   (GENVAR NIL T)
   (MAP #'(LAMBDA (SUBST-TAIL)
		  (RPLACA SUBST-TAIL 
			  (CONS (CAR SUBST-TAIL)
				(GENVAR (TERMSORT-VARANGE (CAR SUBST-TAIL))) ) ) )
	SUBSTLIST ) )

(SETQ GENVARINDEX '((TIME T (T . 0))
		    (LOCATION L (L . 0))
		    (AFFAIRSTATE S (S . 0))
		    (PERSON P (P . 0))
		    (THING V (V . 0) (W . 0))
		    (NUMBER N (N . 0) (M . 0) (J . 0))
		    (PHYSOB X (X . 0) (Y . 0) (Z . 0))
		    (ATTRIBUTE A (A . 0)) ))

(SETQ GENVAR-RANGES (MAPCAR #'CAR GENVARINDEX))

(DEFMACRO UNARY-ATOMIC (LT-FORM)
  `(AND (EQ (LT-TYPE ,LT-FORM) 'ATOMICPROPO)
	(= 1 (LENGTH (ROLELINKS ,LT-FORM))) ) )

(DEFMACRO NOPAREN-DISJUNCT ()
   `(OR (MEMQ ARGTYPE '(SIMPLEFORM NEGPROPO QUANTIFIERFORM λ-PAIR))
	(AND (EQ ARGTYPE 'ATOMICPROPO)
	     (NOT (EQ '= (CAR DISJUNCT))) )
	(AND (EQ ARGTYPE 'CONJ-PROPO)
	     (> 3 (LENGTH (ROLELINKS LT-FORM)))
	     ;;?(EACH CONJUCT (MEMQ ARGTYPE '(ATOMICPROPO SIMPLEFORM NEGPROPO)))
	       ) ) )

(DEFMACRO DPYLIST-ROLINK (ROLINK LT-FORM)
   `(NCONC (COND ((NOT (#.(ISA . COREROLE) (ROLEMARK ,ROLINK) ,LT-FORM))
		    (LIST (#.(THE-FOR:ROLELINK . ROLEPHRASE) ,ROLINK ,LT-FORM)
			  '/: ) ))
	   (COND ((ARGUMENT ,ROLINK)
		    (DPYLIST-S (ARGUMENT ,ROLINK)) )) ) )

(DEFMACRO MAKE-↑↓-/[-ATOM (↑↓-MARKER)
  `(IMPLODE (NCONC (EXPLODE ,↑↓-MARKER) '(/[))) )

(DEFMACRO (Z-BASE-EQUIV defmacro-for-compiling 't) (LETTER)
  `(- (CAR (EXPLODEN ,LETTER)) 65.) )

; DPYLIST-S updates the freevar SUBSTLISTPTR
(DEFUN DPYLIST-S (LT-FORM)
  (CASEQ (LT-TYPE LT-FORM)
    (ATOMICPROPO 
     (*CATCH '|=PROPO|
      (COND ((AND (EQ '= (CAR LT-FORM)) (= 2 (LENGTH (ROLELINKS LT-FORM))))
	       (*THROW '|=PROPO|
		 (LET* ((ROLINKS (ROLELINKS LT-FORM))
			(ARG1 (ARGUMENT (CAR ROLINKS)))
			(ARG2 (ARGUMENT (CADR ROLINKS))) )
		       (NCONC (DPYLIST-S ARG1)
			      (NCONS '| = |)
			      (DPYLIST-S ARG2) ) ) ) ))
      (LET ((PARENFLAG (COND ((< 1 (LENGTH (ROLELINKS LT-FORM))) T))))
	   (NCONC (LIST (PFC-CONCEPT LT-FORM))
		  (LIST (COND (PARENFLAG '/( ) (T '/  )))
		  (DO ((RL-LIST (ROLELINKS LT-FORM) (CDR RL-LIST))
		       (COMMAFLG NIL T)
		       (PRINTLISTPTR (NCONS NIL)) )
		      ((NULL RL-LIST) (CAR PRINTLISTPTR))
		      (COND (COMMAFLG (TCONC '|, | PRINTLISTPTR)))
		      (LCONC (DPYLIST-ROLINK (CAR RL-LIST) LT-FORM) PRINTLISTPTR) )
		  (COND (PARENFLAG (LIST '/) ))) ) ) ) )
    (F-TERM
      (LET ((PARENFLAG (COND ((< 1 (LENGTH (ROLELINKS LT-FORM))) T))))
	   (NCONC (LIST (PFC-CONCEPT LT-FORM))
		  (LIST (COND (PARENFLAG '/( ) (T '/  )))
		  (DO ((RL-LIST (ROLELINKS LT-FORM) (CDR RL-LIST))
		       (COMMAFLG NIL T)
		       (PRINTLISTPTR (NCONS NIL)) )
		      ((NULL RL-LIST) (CAR PRINTLISTPTR))
		      (COND (COMMAFLG (TCONC '|, | PRINTLISTPTR)))
		      (LCONC (DPYLIST-ROLINK (CAR RL-LIST) LT-FORM) PRINTLISTPTR) )
		  (COND (PARENFLAG (LIST '/) ))) ) ) )
    ((SIMPLEFORM λ-PAIR) (LIST LT-FORM))
    (QT-PAIR (LIST (CDR LT-FORM)))	;; quantifier-term
    (QUANTIFIERFORM
       (DO ((THISFORM LT-FORM (#.(THE-OF:LT-QUANT . SCOPE) THISFORM))
	    (DETERMINER (#.(THE-OF:LT-QUANT . DETERMINER) LT-FORM))
	    (DETFLAG T NIL) (OUTLISTPTR (NCONS NIL)) )
	   ((NOT (AND (#.(ISA-OF:LT . QUANTIFIER) THISFORM)
		      (EQ (#.(THE-OF:LT-QUANT . DETERMINER) THISFORM)
			  DETERMINER ) ))
	      (TCONC '/} OUTLISTPTR)
	      (LET ((PERIODFLAG (NOT (EQ (LT-TYPE THISFORM) 
					  'QUANTIFIERFORM ))))
		   (COND (PERIODFLAG
			    (TCONC '/. OUTLISTPTR)
			    (LCONC (DPYLIST-S THISFORM) OUTLISTPTR)
			    (TCONC '/. OUTLISTPTR) )
			 (T (LCONC (DPYLIST-S THISFORM) OUTLISTPTR)) )
		   (CAR OUTLISTPTR) ) )
	   (COND (DETFLAG (LCONC (LIST '/{ DETERMINER) OUTLISTPTR)))
	   (CASEQ DETERMINER ((GREAT-MAJORITY MOST THE !1)
			        (TCONC '| | OUTLISTPTR) ))
	   (TCONC THISFORM SUBSTLISTPTR)
	   (LCONC (LIST '$VAR$ THISFORM '/.) OUTLISTPTR)
	   (LCONC (COND ((UNARY-ATOMIC (LT-QSORT-EXPR THISFORM))
			   (LIST (PFC-CONCEPT (LT-QSORT-EXPR THISFORM))) )
			(T (DPYLIST-S (LT-QSORT-EXPR THISFORM))))
		  OUTLISTPTR ) ) )
    (λ-EXPR
       (DO ((PK-TAIL (LT-PATHKEYLISTS LT-FORM) (CDR PK-TAIL))
	    ;; PK-TAIL: ((<termsort> <pathkey1> <pathkey2> ...) ...)
	    (λ-SCOPE (LT-λ-SCOPE LT-FORM))
	    (PRINTLISTPTR (NCONS NIL))
	    (COMMAFLAG NIL T) (λ-PAIR-ROLINK) (λ-PAIR) )
	   ((NULL PK-TAIL)
	      (TCONC '|).| PRINTLISTPTR)
	      (LCONC (DPYLIST-S λ-SCOPE) PRINTLISTPTR)
	      (CONS '|(λ| (CAR PRINTLISTPTR)) )
	   (SETQ λ-PAIR-ROLINK (GET-ROLELINK
				  (CAR (PATHKEYS (CAR PK-TAIL))) λ-SCOPE ))
	   (SETQ λ-PAIR (COND ((EQ 'FN-VECTOR-LINK (ROLEMARK λ-PAIR-ROLINK))
				 (NTH (Z-BASE-EQUIV (CADR λ-PAIR-ROLINK))
				      (CADDR λ-PAIR-ROLINK) ) )
			      (T (ARGUMENT λ-PAIR-ROLINK)) ))
	   (COND ((MEMQ (LT-TYPE λ-PAIR) '(↓-TERM ↑-TERM))
		    (SETF* λ-PAIR (↑↓-MATRIX -*-)) ) )
	   (LCONC (COND (COMMAFLAG (LIST '/, λ-PAIR)) (T (LIST λ-PAIR)))
		  PRINTLISTPTR )
	   (TCONC λ-PAIR SUBSTLISTPTR) ) )
    (NEGPROPO
       (LET* ((BODY (ARGUMENT (CAR (ROLELINKS LT-FORM))))
	      (ARGTYPE (LT-TYPE BODY))
	      (PARENFLAG (COND ((MEMQ ARGTYPE '(QUANTIFIERFORM SIMPLEFORM))
				  NIL )
			       ((AND (EQ ARGTYPE 'ATOMICPROPO)
				     (NOT (EQ '= (CAR BODY))) )
				  NIL )
			       (T T) )) )
	     (NCONC (NCONS '/¬ )
		    (COND (PARENFLAG (NCONS '/( )))
		    (DPYLIST-S BODY)
		    (COND (PARENFLAG (NCONS '/) ))) ) ) )
    (CONJ-PROPO
       (DO ((RL-TAIL (ROLELINKS LT-FORM) (CDR RL-TAIL))
	    (CONNFLAG NIL T) (OUTLISTPTR (NCONS NIL)) )
	   ((NULL RL-TAIL) (CAR OUTLISTPTR))
	   (LET* ((CONJUNCT (ARGUMENT (CAR RL-TAIL)))
		  (ARGTYPE (LT-TYPE CONJUNCT))
		  (PARENFLAG (COND ((MEMQ ARGTYPE
					  '(SIMPLEFORM NEGPROPO QT-PAIR
					    QUANTIFIERFORM λ-PAIR ) )
				      NIL )
				   ((AND (EQ ARGTYPE 'ATOMICPROPO)
					 (NOT (EQ '= (CAR CONJUNCT))) )
				      NIL )
				   (T T) )) )
		 (COND (CONNFLAG (TCONC '| ∧ | OUTLISTPTR)))
		 (COND (PARENFLAG (TCONC '/( OUTLISTPTR)))
		 (LCONC (DPYLIST-S (ARGUMENT (CAR RL-TAIL)))
			OUTLISTPTR)
		 (COND (PARENFLAG (TCONC '/) OUTLISTPTR))) ) ) )
    (DISJ-PROPO
       (DO ((RL-TAIL (ROLELINKS LT-FORM) (CDR RL-TAIL))
	    (CONNFLAG NIL T) (OUTLISTPTR (NCONS NIL)) )
	   ((NULL RL-TAIL) (CAR OUTLISTPTR))
	   (LET* ((DISJUNCT (ARGUMENT (CAR RL-TAIL)))
		  (ARGTYPE (LT-TYPE DISJUNCT))
		  (PARENFLAG (COND ((NOPAREN-DISJUNCT) NIL)
				   (T T) )) )
		 (COND (CONNFLAG (TCONC '| ∧ | OUTLISTPTR)))
		 (COND (PARENFLAG (TCONC '/( OUTLISTPTR)))
		 (LCONC (DPYLIST-S (ARGUMENT (CAR RL-TAIL)))
			OUTLISTPTR)
		 (COND (PARENFLAG (TCONC '/) OUTLISTPTR))) ) ) )
    ((⊃-PROPO ⊃-THEN-PROPO IF-WOULD-PROPO IF-THENWOULD-PROPO)
       (LET ((ANTE (ANTECEDENT LT-FORM))
	     (CONSE (CONSEQUENT LT-FORM))
	     (CONNECTIVE (CASEQ (LT-TYPE LT-FORM)
			   (⊃-PROPO '| ⊃ |)
			   (⊃-THEN-PROPO '| T⊃ |)
			   (IF-WOULD-PROPO '| W→ |)
			   (IF-THENWOULD-PROPO '| TW→ |)
			   (T (BREAK |DPYLIST-S: impossible break!!|)) )) )
	    (NCONC (NCONS '/( )
		   (DPYLIST-S ANTE)
		   (NCONS CONNECTIVE)
		   (DPYLIST-S CONSE)
		   (NCONS '/) ) ) ) )
    ((↑-TERM ↓-TERM)
       (NCONC (LIST (MAKE-↑↓-/[-ATOM (↑↓-MARKER LT-FORM)))
	      ;; ↑↓-/[-atom:  |↑[|, |↓[|, |↑2[|, |↑3[|, etc.
	      ;; STRAIGHTPRIN may want the ↑↓-marker and leftbracket merged.
	      (DPYLIST-S (↑↓-MATRIX LT-FORM)) 
	      (LIST '/] ) ) )
    (FIXNUM-VECTOR
       (NCONC (LIST '/( (CAR LT-FORM))
	      (MAPCAN #'(LAMBDA (ELEMENT)
			  (LIST '| | ELEMENT) )
		      (CDR LT-FORM) )
	      (LIST '/) ) ) )
    (T (WRITE T  '|; LT-type |  (LT-TYPE LT-FORM)
	      '| not acceptable to DPYLIST-S !| (BREAK DPYLIST-S) )) ) )

; Adds an item onto the end of a list that is maintained via the cons-cell PTR.
; The list itself is (CAR PTR), while (CDR PTR) is (LAST list), the last cons
; of the list.  To start such a list, PTR should be initialized to (NCONS NIL).
(DEFUN TCONC (ADDITEM PTR)
       (OR (CONSP PTR) (BREAK |TCONC - PTR not a CONS-cell!|))
       (COND ((CDR PTR)
	      (RPLACD PTR (CDR (RPLACD (CDR PTR) (NCONS ADDITEM)))) )
	     (T (RPLACD PTR (CAR (RPLACA PTR (NCONS ADDITEM))))) ) )

(DEFUN LCONC (ADDLIST PTR)
       (OR (CONSP PTR) (BREAK |LCONC - PTR not a CONS-cell!|))
       (COND ((NULL ADDLIST) PTR)
	     (T (COND ((CDR PTR)
		       (RPLACD PTR (LAST (RPLACD (CDR PTR)
						     ADDLIST ))) )
		      (T (RPLACD PTR 
				 (LAST (CAR (RPLACA PTR 
						    ADDLIST ))) )) )) ) )

(DEFUN TERMSORT (LT-TERM)
  (LET ((TERMSORT (CASEQ (LT-QQU-TYPE LT-TERM)
		    (QT-PAIR (#.(THE-OF:LT-QUANT . QSORT) (CDR LT-TERM)))
		    (SIMPLEFORM (OR (GET LT-TERM 'PROPERSORT)
				    (GET LT-TERM 'CATEGORY) ))
		    (F-TERM (GET (PFC-CONCEPT LT-TERM) 'VALUE-SORT))
		    ((ATOMICPROPO CONN-PROPO QUANTIFIERFORM) 'AFFAIRSTATE)
		    (↑-TERM (CONS (↑↓-MARKER LT-TERM)
				  (TERMSORT (↑↓-MATRIX LT-TERM)) ))
		    (↓-TERM (TERMSORT (↑↓-MATRIX LT-TERM)))
		    (λ-PAIR (CDR LT-TERM))
		    (T (BREAK |TERMSORT - unexpected term-type|)) )) )
       (OR TERMSORT (WRITE T "; No termsort for " LT-TERM
			   (BREAK TERMSORT) )) ) )

(DEFUN NORMALIZE-TERMSORTEXPR (TERMSORTEXPR)
  (DO ((TS-TAIL TERMSORTEXPR (CDR TS-TAIL))
       (TALLY 0 (1+ TALLY)) )
      ((ATOM TS-TAIL) 
	 (COND ((> TALLY 1)
		  (RPLACA TERMSORTEXPR (IMPLODE (LIST '↑ (+ 48. TALLY))))
		  (RPLACD TERMSORTEXPR TS-TAIL) ))
	 TERMSORTEXPR )
      (OR (EQ '↑ (CAR TS-TAIL))
	  (BREAK |NORMALIZE-TERMSORTEXPR - unexpected CAR|) ) ) )
(DECLARE (special BREAK-POINTS BREAK-BEFORE-POINTS)
	 (fixnum SIZE IMAGE-SIZE PCHUNKSIZE NEWPCHUNKSIZE TCHUNKSIZE
		 REMNANTSIZE BRACECOUNT ) )

(DEFMACRO (PRINCLIST defmacro-for-compiling 't) (PRINTLIST)
  `(MAPC (FUNCTION PRINC) ,PRINTLIST) )

; CURRENTPOS is a special variable used to keep internal track of where we
;  are in the printline; CHARPOS should do this, but doesn't, apparently
;  because the E/MACLISP interface does not preserve CHARPOS-type information
;  when it handles output from programs.  By definition, CURRENTPOS is the
;  first unfilled print-position on the current line, or in other words,
;  the print-position of the next character to be printed (should there be one)
;  on the current line.

(DEFMACRO CHECK-TAKEPTR ()
 '(*CATCH 'CHECK-TAKEPTR
    (OR TAKEPTR (BREAK |CHECK-TAKEPTR - null TAKEPTR !|))
    (MAP #'(LAMBDA (SORCETAIL)
	     (COND ((EQ TAKEPTR SORCETAIL) (*THROW 'CHECK-TAKEPTR T))) )
	 SOURCELIST )
    (BREAK |CHECK-TAKEPTR - TAKEPTR is not a tail of SOURCELIST !|) ) )

; This macro takes an initial segment (chunk) out of SOURCELIST [running through
;  (CAR TAKEPTR)] and prints it, resetting SOURCETAIL to the shortened SOURCELIST
;  and TAKEPTR to NIL.
(DEFMACRO PRINSOURCECHUNK ()
   '(PROGN (CHECK-TAKEPTR) 
	   (SETQ PLINE SOURCELIST
		 SOURCELIST (CDR TAKEPTR)
		 SOURCETAIL SOURCELIST
		 CURRENTPOS (+ CURRENTPOS TCHUNKSIZE)
		 TCHUNKSIZE 0
		 PCHUNKSIZE 0 )
	   (RPLACD TAKEPTR NIL)
	   (SETQ TAKEPTR NIL)
	   (PRINCLIST PLINE) ) )

(DEFMACRO GETSBQLINE (SOURCEATOM)
   `(DO ((SOURCETAIL (COND ((EQ '/{ (CAR ,SOURCEATOM)) (CDDDR ,SOURCEATOM))
			   (T ,SOURCEATOM) )
		     (CDR SOURCETAIL) )
	 (OUTLINE ,SOURCEATOM) )
	((OR (NULL SOURCETAIL) (EQ (CADR SOURCETAIL) '$VAR$))
	    (SETQ ,SOURCEATOM (CDDR SOURCETAIL))
	    (COND (SOURCETAIL (RPLACD SOURCETAIL NIL)))
	    OUTLINE ) ) )

(DEFMACRO (NEXTITEMSIZE defmacro-for-compiling 't) (LIST)
   `(FLATC (CAR ,LIST)) )

(DEFMACRO PRINLIST-IMAGE-SIZE (PRINLIST)
 `(DO ((LISTAIL ,PRINLIST (CDR LISTAIL))
       (SIZE 0) )
      ((NULL LISTAIL) SIZE)
      (SETQ SIZE (+ SIZE (FLATC (CAR LISTAIL)))) ) )

(DEFMACRO λ-PREFIX-IMAGE-SIZE (PRINLIST)
 `(DO ((LISTAIL ,PRINLIST (CDR LISTAIL))
       (SIZE 0) )
      ((EQ '|).| (CAR LISTAIL)) (+ 2 SIZE))	;(
      (SETQ SIZE (+ SIZE (FLATC (CAR LISTAIL)))) ) )

(DEFMACRO (PRINITEMS defmacro-for-compiling 't) (NUMATOM SOURCEATOM)
  `(DO ((RPT ,NUMATOM (1- RPT)))
       ((ZEROP RPT))
       (SETQ CURRENTPOS (+ CURRENTPOS (NEXTITEMSIZE ,SOURCEATOM)))
       (PRINC (POP ,SOURCEATOM)) ) ) 

(DEFMACRO PRINSUBQUANT1 (QLINEATOM)
  `(LET ((SBQLINE (GETSBQLINE ,QLINEATOM)))
	(PRINITEMS 2 SBQLINE)  ;; '/{ , <determiner>
	(COND ((EQ (CAR SBQLINE) '/  ) (PRINITEMS 1 SBQLINE)))  ;; if space, print it
	(POP SBQLINE)		;; jettison '$VAR$
	(SETQ PERIODCOL (+ CURRENTPOS MAXVARLENGTH))
;	(BREAK PSBQ1)
	(TAB (- PERIODCOL (NEXTITEMSIZE SBQLINE)))
	(PRINITEMS 2 SBQLINE)	;; <variable>, '/.
	(STRAIGHTPRIN SBQLINE) ) )

(DEFMACRO PRINSUBQUANT2 (QLINEATOM)
  `(LET ((SBQLINE (GETSBQLINE ,QLINEATOM)))
;	(BREAK PSBQ2)
	(TAB (- PERIODCOL (NEXTITEMSIZE SBQLINE)))
	(PRINITEMS 2 SBQLINE)  ;; <variable>, '/.
	(STRAIGHTPRIN SBQLINE) ) )

(DEFMACRO GETQUANTLINE (SOURCEATOM)
   `(DO ((SOURCETAIL ,SOURCEATOM (CDR SOURCETAIL))
	 (OUTLINE ,SOURCEATOM)
	 (BRACECOUNT 1) )
	((ZEROP BRACECOUNT) (SETQ ,SOURCEATOM (CDR SOURCETAIL))
			    (RPLACD SOURCETAIL NIL)
			    OUTLINE )
	(CASEQ (CADR SOURCETAIL)
	   (/{ (SETQ BRACECOUNT (1+ BRACECOUNT)))
	   (/} (SETQ BRACECOUNT (1- BRACECOUNT))) ) ) )

(DEFMACRO GETλ-LINE (SOURCEATOM)
   `(DO ((SOURCETAIL ,SOURCEATOM (CDR SOURCETAIL))
	 (OUTLINE ,SOURCEATOM) )
	((EQ (CAR SOURCETAIL) '|).|) (SETQ ,SOURCEATOM (CDR SOURCETAIL))    ;(
				     (RPLACD SOURCETAIL NIL)
				     OUTLINE ) ) )

(DEFMACRO MAXVARIABLENGTH (QLINEATOM)
  `(LET ((VARLIST (MAPCON (FUNCTION (LAMBDA (QLTAIL)
			     (COND ((EQ (CAR QLTAIL) '$VAR$)
				      (NCONS (CADR QLTAIL)) )) ))
			  ,QLINEATOM )))
	(APPLY (FUNCTION MAX) (MAPCAR (FUNCTION (LAMBDA (VAR)
					(FLATC VAR) ))
				      VARLIST )) ) )

;(DEFMACRO TAB (POS &optional FILENAME)
;   `(CHARPOS ,FILENAME ,POS) )
; CHARPOS doesn't work as advertised in the Moonual, and won't take
; a second fixnum argument without giving a "non-fixnum-arg" error.

;(PROGN (TERPRI)(TERPRI)(TAB 6)(PRIN1 (CHARPOS T))(PRIN1 'AB)(CHARPOS T))
;(PROGN (TERPRI)(TERPRI)(TAB 6)(TAB 4)(PRIN1 (CHARPOS T))(PRIN1 'AB)(CHARPOS T))

(DEFMACRO (SPACELEFT defmacro-for-compiling 't) ()
  `(- (LINEL NIL) CURRENTPOS) )

(DEFUN STRAIGHTPRIN (SOURCELIST)
   (DO ((SOURCETAIL SOURCELIST (CDR SOURCETAIL))
	(LAGPTR NIL SOURCETAIL) ;; - points to SOURCETAIL of previous iteration.
	(PCHUNKSIZE 0 NEWPCHUNKSIZE) ;; - NEWPCHUNKSIZE less the size of the
			  ;;   symbol in NEXT-ITEM [i.e., (CAR SOURCETAIL)].
	(NEWPCHUNKSIZE 0) ;; - the size of the sourcechunk beginning with
			  ;;   (CAR SOURCELIST) and running through (CAR SOURCETAIL).
	(TCHUNKSIZE 0)  ;; - the size of what PRINSOURCECHUNK would print if called.
	(REMNANTSIZE 0) ;; - the size of the chunk between the last breakpoint
			;;   symbol and the beginning of a quantifier or λ-expr.
	(PLINE)	     ;; - PRINSOURCECHUNK's list of symbols to print.
	(TAKEPTR)    ;; - points to a tail of SOURCELIST whose CAR is the last
		     ;;   symbol that PRINSOURCECHUNK would print if called.
		     ;;   It is set either when a breakpoint or break-before-point
		     ;;   is encountered, or just before calling PRINSOURCECHUNK.
	(NEXT-ITEM) )
       ((NULL SOURCETAIL) (SETQ CURRENTPOS (+ CURRENTPOS PCHUNKSIZE))
			  (PRINCLIST SOURCELIST) )
     A (SETQ NEXT-ITEM (CAR SOURCETAIL))
       (COND ((MEMQ NEXT-ITEM '( /{ |(λ| ))		   ;)
	      ;; left brace signals the beginning of a quantifier,
	      ;; left-paren-λ signals the beginning of a λ-expr.
	        (SETQ REMNANTSIZE (- PCHUNKSIZE TCHUNKSIZE))
		(COND (TAKEPTR 		;; (princ '|call-1:psch|)
		      ;; Print through or to the last breakpoint or
		      ;;  break-before-point (respectively), if any.
			(PRINSOURCECHUNK) ))
		(COND ((OR (AND (EQ '|{| NEXT-ITEM) (> 25. (SPACELEFT)))
			   (AND (EQ '|(λ| NEXT-ITEM)	;)
				(> (λ-PREFIX-IMAGE-SIZE SOURCETAIL) (SPACELEFT))) )
   ;; If there is insufficient space left on the current line, go to the next.
   ;; The test here could be more sophisticated, taking into account the
   ;; length and structure of the next quantifier.
		         (TERPRI) 
			 (SETQ CURRENTPOS 1)
			 (TAB 2) ))
	        (COND ((> REMNANTSIZE 0) (SETQ TAKEPTR LAGPTR
					       TCHUNKSIZE REMNANTSIZE )
		;; Print any characters accumulated after the last breakpoint
		;;  or break-before-point-predecessor, but before new q- or
		;;  λ-expr (these chars should come on the new line, if any).
;					 (princ '|call-1:psch|)
					 (PRINSOURCECHUNK) ))
		(SETQ SOURCETAIL (SETQ SOURCELIST
				       (CASEQ NEXT-ITEM
					 (/{ (PRINQUANT SOURCETAIL))
					 (|(λ| (PRIN-λ-PREFIX SOURCETAIL))    ;)
					 (T (BREAK |STRAIGHTPRIN:Q∨λBRANCH|)))))
		(GO A) ))
     (SETQ NEWPCHUNKSIZE (+ PCHUNKSIZE (FLATC NEXT-ITEM)))
;(break prin:test-inc)
     (COND ((> (+ CURRENTPOS NEWPCHUNKSIZE)
	       (1+ (LINEL NIL)) )
	    ;; If the next item would run beyond the end of the line, print a
	    ;;  chunk up to or through (respectively) the last break-before-point
	    ;;  or breakpoint (else if no such points have occurred,
	    ;;  up to the next item), and then start a new line.
	      (COND ((ZEROP PCHUNKSIZE)	;; nothing to print on current line.
		       (TERPRI) (SETQ CURRENTPOS 1) (TAB 2) (GO A) )
		    ((NULL TAKEPTR)
		     ;; If no break-before-point or breakpoint has occurred,
		     ;;  and the line starts at the beginning, take a
		     ;;  chunk up to the next item.
		       (COND ((< 2 CURRENTPOS)
			        (TERPRI) (SETQ CURRENTPOS 1) (TAB 2) (GO A) )
			     (T (SETQ TAKEPTR LAGPTR
			     ;; since PCHUNKSIZE > 0, LAGPTR must be non-null.
				      TCHUNKSIZE PCHUNKSIZE ) ) ) ) )
;	      (princ '|call-3:psch|)
	      (PRINSOURCECHUNK) 
	      (TERPRI)
	      (SETQ CURRENTPOS 1)
	      (TAB 2)
	      (GO A) )
 	   ((AND (#.(ISA . BREAK-BEFORE-POINT) NEXT-ITEM)
		 (NOT (EQ SOURCETAIL SOURCELIST)) )
;	      (princ '|setting takeptr-before|)
	      (SETQ TAKEPTR LAGPTR
		    TCHUNKSIZE PCHUNKSIZE ) )
	   ((#.(ISA . BREAK-POINT) NEXT-ITEM)
;	      (princ '|setting takeptr-end|)
	      (SETQ TAKEPTR SOURCETAIL
		    TCHUNKSIZE NEWPCHUNKSIZE ) ) ) ) )

(DEFUN PRINQUANT (SOURCELIST &aux (QLINE (GETQUANTLINE SOURCELIST))
			     	  (MAXVARLENGTH (MAXVARIABLENGTH QLINE))
				  PERIODCOL )
   (PRINSUBQUANT1 QLINE)
   (COND (QLINE (DO () ((NULL QLINE)) (PRINSUBQUANT2 QLINE))))
   SOURCELIST )

(DEFUN PRIN-λ-PREFIX (SOURCELIST)
  (LET* ((λ-LINE (GETλ-LINE SOURCELIST))
	 (IMAGE-SIZE (PRINLIST-IMAGE-SIZE λ-LINE)) )
	(COND ((> (+ CURRENTPOS IMAGE-SIZE) (1+ (LINEL NIL)))
	         (TERPRI)  (SETQ CURRENTPOS 1)  (TAB 2) ))
	(SETQ CURRENTPOS (+ CURRENTPOS IMAGE-SIZE))
	(MAPC #'PRINC λ-LINE)
	SOURCELIST ) )

(DEFUN TAB (POS)
   (COND ((ZEROP POS) (TERPRI) (PRINC ";TAB to 0 ??!") (BREAK TAB))
	 ((< POS CURRENTPOS) (TERPRI) (SETQ CURRENTPOS 1)) )
   (DO ()
       ((= POS CURRENTPOS))
       (SETQ CURRENTPOS (1+ CURRENTPOS))
       (PRINC '/ ) ) )

(DEFUN CURRENTPOS (&optional (FILENAME T))
    (CHARPOS FILENAME) )
(SETQ YHπ-FLAG NIL)

(SETQ *CONCEPTS* '(*TOP*))

(SETQ ALPHABET '(A B C D E F G H I J K L M N O P Q R S T U V W X Y Z)
      REVERSE-ALPHABET (REVERSE ALPHABET)
      2-ALPHABETS (APPEND ALPHABET
			 '(/a /b /c /d /e /f /g /h /i /j /k /l /m /n
			      /o /p /q /r /s /t /u /v /w /x /y /z ) ) )

(SETQ ALPHA-NCONSES (MAPCAR #'NCONS ALPHABET))

(SETQ *-ASCII 42.)

(DEFSTRUCT (LINK-NODE (TYPE TREE) (CONC-NAME LINK-))
	   KEY A-LIST )

(DEFSTRUCT (LEAF-NODE (TYPE TREE) (CONC-NAME LEAF-))
	   KEY PLIST )

(DEFSTRUCT (LTCC-PLIST (TYPE TREE) (CONC-NAME LTCC-))
	   (PLIST-IDENT '*CC-PLIST*) PROPLIST )

; This function presupposes that LINFORMULA is not a LISP atom.  Provided that
;  the global variable YHπ-FLAG is non-null, this fn will return the name of
;  a YH-UNIT having the internal translation of LINFORMULA as value of the
;  property LT-FORMULA, and an appropriate atom as value of the property LT-TYPE.
(DEFUN NRML-ANL-YZE-LINFORMULA (LINFORMULA &optional YH-UNIT)
  (LET ((LT-FORM (ENCODE-LINFORMULA LINFORMULA)))
       (NORMALIZE-CMPD-CONCEPT
	    LT-FORM (ANALYZE-CMPD-CONCEPT LT-FORM) NIL YH-UNIT ) ) )

(DEFMACRO (NRML-FORMULA defmacro-for-compiling 't) (LT-FORM)
  `(ATC-GET (NRML-ANL-YZE ,LT-FORM) 'LT-FORMULA) )

(DEFMACRO (NRML-ANL-YZE defmacro-for-compiling 't) (LT-FORM . AL-VARS-TAIL)
 `(LET ((LT-FORM ,LT-FORM))
       (COND ((ATOM LT-FORM) LT-FORM)
	     (T (LET ((AL-VARS ,(CAR AL-VARS-TAIL)))
		     (NORMALIZE-CMPD-CONCEPT
		            LT-FORM
			    (ANALYZE-CMPD-CONCEPT LT-FORM AL-VARS)
			    AL-VARS ) )) ) ) )

(DEFMACRO (LT-CONCEPT-TYPE defmacro-for-compiling 't) (LT-FORM)
  `(LET ((LT-TYPE (LT-TYPE ,LT-FORM)))
	(CASEQ LT-TYPE
	   (λ-EXPR (LT-TYPE (LT-λ-SCOPE ,LT-FORM)))
	   (T LT-TYPE) ) ) )

(DEFMACRO ADD-NEWLINK (NEWKEY LINK)
  `(CAR (SETF* (LINK-A-LIST ,LINK) (CONS (MAKE-LINK-NODE KEY ,NEWKEY 
							A-LIST NIL )
					-*- ))) )

(DEFMACRO (LEAF-UNIT defmacro-for-compiling 't) (LEAF-NODE)
  `(LEAF-PLIST ,LEAF-NODE) )

(DEFUN NORMALIZE-CMPD-CONCEPT (LT-FORM CC-INDEX-KEYS
				       &optional ANALYSIS-LIST-VARS YH-UNIT )
  (CASEQ (LT-CONCEPT-TYPE LT-FORM)
    (SIMPLEFORM LT-FORM)
			   ;; is more code needed here - to make LT-FORM
			   ;;  an atomic concept if it isn't one already?
    (T (DO ((INDEX-KEYS CC-INDEX-KEYS (CDR INDEX-KEYS))
	    (NC-CURRENTNODE *CONCEPTS*)  ;; the NC- prefix connotes "normalize concept".
	    (CURRENTKEY) )
	   ((NULL INDEX-KEYS)
;	    (BREAK INDX-CPT:TEST)
	    (PROG1 (COND ((LEAF-PLIST NC-CURRENTNODE))
			 (T (INITIALIZE-CMPD-CONCEPT
				NC-CURRENTNODE LT-FORM CC-INDEX-KEYS YH-UNIT ) ) )
		   (COND (ANALYSIS-LIST-VARS
			  (MAPC #'(LAMBDA (ANALYSIS-LIST-VAR)
				   (SET ANALYSIS-LIST-VAR
					(CONS (CONS (LEAF-PLIST NC-CURRENTNODE)
						    CC-INDEX-KEYS )
					      (SYMEVAL ANALYSIS-LIST-VAR) ) ) )
				ANALYSIS-LIST-VARS ) )) ) )
	   (SETQ CURRENTKEY (CAR INDEX-KEYS)
		 NC-CURRENTNODE
		  (COND ((ASSQ CURRENTKEY (LINK-A-LIST NC-CURRENTNODE)))
			(T (ADD-NEWLINK CURRENTKEY NC-CURRENTNODE)) ))))))

(DEFUN INITIALIZE-CMPD-CONCEPT (LEAF-NODE LT-FORMULA D-NET-KEYS YH-UNIT)
  (LET ((F-DESCRIPTS (CREATE-F-DESCRIPTS LT-FORMULA D-NET-KEYS)))
       (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORMULA)
	      (SETQ LT-FORMULA (λ-UNSUBST LT-FORMULA)) ))
       (COND (YHπ-FLAG (OR YH-UNIT (SETQ YH-UNIT (π-MAKE-UNIT NIL)))
		       (π-PUTPROP YH-UNIT LT-FORMULA 'LT-FORMULA)
		       (π-PUTPROP YH-UNIT F-DESCRIPTS 'F-DESCRIPTS)
		       (SETF (LEAF-PLIST LEAF-NODE) YH-UNIT) )
	     (T (LET ((CC-PROPLIST (MAKE-LTCC-PLIST)))
		     (PUTPROP CC-PROPLIST LT-FORMULA 'LT-FORMULA)
		     (PUTPROP CC-PROPLIST F-DESCRIPTS 'F-DESCRIPTS)
		     (SETF (LEAF-PLIST LEAF-NODE) CC-PROPLIST) )) ) ) )

(DEFUN CREATE-F-DESCRIPTS (LT-FORM D-NET-KEYS)
  (LET* ((LT-TYPE (LT-TYPE LT-FORM))
	 (F-DESCRIPTS `((LT-TYPE . ,LT-TYPE))) )
	(COND ((EQ 'QUANTIFIERFORM LT-TYPE)
		 (NCONC F-DESCRIPTS `((LT-Q-DETERMINER .
					,(LT-Q-DETERMINER LT-FORM) )))
		 (LET* ((UQ-KERNL (UQ-KERNEL LT-FORM))
			(LT-TYPE*UQ-KERNEL (LT-TYPE UQ-KERNL)) )
		       (COND ((EQ '⊃-PROPO LT-TYPE*UQ-KERNEL)
				(NCONC F-DESCRIPTS
				       `((LT-TYPE*UQ-⊃-KERNEL .
					   ,(LT-TYPE (CONSEQUENT UQ-KERNL)) ) ) ) )
			     (T (NCONC F-DESCRIPTS
				       `((LT-TYPE*UQ-KERNEL .
					   ,LT-TYPE*UQ-KERNEL )) )) ))))
	(NCONC F-DESCRIPTS `((D-NET-KEYS . ,D-NET-KEYS)))
	F-DESCRIPTS ) )

(DEFMACRO (CONCEPT-BODY defmacro-for-compiling 't) (LT-FORM)
  `(COND ((#.(ISA-OF:LT . λ-EXPR) ,LT-FORM) (LT-λ-SCOPE ,LT-FORM))
	 (T ,LT-FORM) ) )

(DEFMACRO 1ST-PROCESS-↑-MATRIX (↑-MATRIX-EXPR λ-EXPR-FLAG)
  `(LET ((↑-MATRIX-ANALYSIS-LIST))
	(NRML-ANL-YZE ,↑-MATRIX-EXPR (NCONS '↑-MATRIX-ANALYSIS-LIST))
	(FIX-AL ↑-MATRIX-ANALYSIS-LIST)
   ;; ↑-MATRIX-ANALYSIS-LIST :
   ;;  ((<normalized-concept-expr> <cc-op> <component-concept-expr> ... ) ... )
	(COND (,λ-EXPR-FLAG
	         (NORMRAISE-CC (CDAR ↑-MATRIX-ANALYSIS-LIST)
			       (LT-λ-PREFIX ,↑-MATRIX-EXPR) ) )
	      (T (NORMRAISE-CC (CDAR ↑-MATRIX-ANALYSIS-LIST))) ) ) )

(DEFMACRO PROCESS-↑-MATRIX (↑-MATRIX-EXPR λ-EXPR-FLAG)
 `(PROGN (NRML-ANL-YZE ,↑-MATRIX-EXPR AL-VARS)
	 (FIX-AL ↑-MATRIX-ANALYSIS-LIST)
	 (COND (,λ-EXPR-FLAG
		  (NORMRAISE-CC (CDAR ↑-MATRIX-ANALYSIS-LIST)
				(LT-λ-PREFIX ,↑-MATRIX-EXPR) ) )
	       (T (NORMRAISE-CC (CDAR ↑-MATRIX-ANALYSIS-LIST))) ) ) )

(DEFMACRO COLLECT-IMAGES (MATCH-PKLS LT-FORM)
 `(COND ((#.(ISA-OF:LT . λ-EXPR) ,LT-FORM)
	   (DO ((MATCH-PKL-TAIL ,MATCH-PKLS (CDR MATCH-PKL-TAIL))
		(PKL-POOL (LT-PATHKEYLISTS ,LT-FORM))
		(IMAGES-PTR (NCONS NIL))
		(REFLECTION) )
	       ((NULL MATCH-PKL-TAIL) (CAR IMAGES-PTR))
	       (SETQ REFLECTION
		     (CAR (SOME PKL-POOL
				#'(LAMBDA (PKL)
				    (EQUAL (PATHKEYS PKL)
					   (PATHKEYS (CAR MATCH-PKL-TAIL)) ) ) )) )
	       (COND (REFLECTION
		       (SETF (λ-TERMSORT (CAR MATCH-PKL-TAIL))
			     (COPYALLCONS (λ-TERMSORT REFLECTION)) )
		       (TCONC (CAR MATCH-PKL-TAIL) IMAGES-PTR) )) ) )) )

; A "pathkey" is a string of one or more letters representing the decomposition
;  path through an lt-expression to a single rolelink occurring within that
;  expression.  A "pathkey digit" is one of the component letters of a pathkey.
;  An "xpathkey"  is an exploded (or more often, an unimploded) pathkey.
;  A "pathkeylist" is a list with CAR a termsort, and CDR a list of pathkeys,
;  corresponding to a set of rolelinks that share the same argument.  Thus, a
;  pathkeylist plays a role similar to that of a variable in the external
;  logical notation.  A LISP variable whose name contains the plural
;  "pathkeylists" is used to store a list of pathkeylists.

(DEFMACRO MERGED-PKLS (PATHKEYLISTS)
    ;; rolemerged criterion: the presence in a multi-pathkey pathkeylist
    ;;  of pathkeys having different first digits.
  `(MAPCAN #'(LAMBDA (PKEYLIST)
	       (COND ((AND (CDR (PATHKEYS PKEYLIST))
			   (DO ((1STDIGIT (GETCHAR (CAR (PATHKEYS PKEYLIST)) 1))
				(PKLTAIL (CDR (PATHKEYS PKEYLIST)) (CDR PKLTAIL)) )
			       ((NULL PKLTAIL) NIL)
			       (OR (EQ (GETCHAR (CAR PKLTAIL) 1) 1STDIGIT)
				   (RETURN T) ) ) )
		        (NCONS PKEYLIST) )) )
	   ,PATHKEYLISTS ) )

(DEFMACRO SETUP-λ-EXPR (NEWPKEYLIST OLDPKEYLISTS KEYDIGIT λ-SCOPE)
 `(LET* ((λ-SCOPE ,λ-SCOPE)
	 (PATHKEYLISTS
	   (ORDER-PATHKEYLISTS
	     (CONS ,NEWPKEYLIST
		   (COND (,OLDPKEYLISTS
			    (SELECT&SHORTEN ,KEYDIGIT 
					    ,OLDPKEYLISTS
					    λ-SCOPE ) )) ) ) ) )
	(COND ((AND (EQ 'ATOMICPROPO (LT-TYPE λ-SCOPE))
		    (ATOM-CONVERTIBLE PATHKEYLISTS λ-SCOPE) )
	         (PFC-CONCEPT λ-SCOPE) )
	      (T (MAKE-LT-λ-EXPR
		    λ-PREFIX (MAKE-LT-λ-PREFIX PATHKEYLISTS PATHKEYLISTS)
		    λ-SCOPE λ-SCOPE ) ) ) ) )

(DEFMACRO (ALPHA-NTH defmacro-for-compiling 't) (ALPHAKEY LIST)
  `(DO ((LISTAIL ,LIST (CDR LISTAIL))
	(ALPHATAIL ALPHABET (CDR ALPHATAIL)) )
       ((EQ ,ALPHAKEY (CAR ALPHATAIL)) (CAR LISTAIL))
       (OR ALPHATAIL (BREAK |ALPHA-NTH - off the end|)) ) )

(DEFMACRO (PREVIOUS-LETTER defmacro-for-compiling 't) (LETTER)
  `(OR (CADR (MEMQ ,LETTER REVERSE-ALPHABET))
       (BREAK |PREVIOUS-LETTER - off the beginning|) ) )

(DEFMACRO ANALYZE-ADVERBIALIZATION (LT-PF-FORM)
  `(LET* ((PF-ATOM (PFC-CONCEPT (CONCEPT-BODY ,LT-PF-FORM)))
	  (ROLEXICON (GET PF-ATOM 'ROLEXICON)) )
	 (OR ROLEXICON (WRITE T "; no rolexicon for " PF-ATOM
			      (BREAK ANALYZE-ADVERBIALIZATION) ))
	 (LET* ((ADV-COMPONENTS
		  (MAPCAR #'(LAMBDA (ROLINK)
			      (CDR (ASSQ (ROLEMARK ROLINK) ROLEXICON)) )
			  (NTHCDR (LENGTH (GET PF-ATOM 'COREROLES))
				  (ROLELINKS (CONCEPT-BODY ,LT-PF-FORM)) ) ) )
		(CC-OP (IMPLODE (APPEND '(A D V B *)
					(NCONS (NTH (1- (LENGTH ADV-COMPONENTS))
						    ALPHABET )) ))) )
	       (LIST* CC-OP PF-ATOM ADV-COMPONENTS) ) ) )

(DEFMACRO INST-KEYS (LT-PF-FORM)
  ;; Instantiation criterion: The absence of a λ-prefix in LT-PF-FORM containing
  ;;  a pathkeylist of the form (<1-digit-pathkey>) for each rolelink in the
  ;;  λ-scope with a non-null rolesort.  This fn returns a list of the missing
  ;;  <1-digit-pathkey>s.
 `(LET ((CNCPT-BODY (CONCEPT-BODY ,LT-PF-FORM)))
       (DO ((ROLINKTAIL (ROLELINKS CNCPT-BODY) (CDR ROLINKTAIL))
	    (TESTPKLTAIL ALPHA-NCONSES (CDR TESTPKLTAIL))
	    (PKEYLISTS (COND ((#.(ISA-OF:LT . λ-EXPR) ,LT-PF-FORM)
			      (LT-PATHKEYLISTS ,LT-PF-FORM) )))
	    (PF-ROLESORTS (OR (GET (PFC-CONCEPT CNCPT-BODY) 'ROLESORTS)
			      (WRITE T "; No rolesorts for concept "
				     (PFC-CONCEPT CNCPT-BODY) "."
				     (BREAK INST-KEYS) ) ))
	    (INST-KEYS) )
	   ((NULL ROLINKTAIL) (GOOD-NREVERSE INST-KEYS))
	   (COND ((AND (NOT (SOME PKEYLISTS #'(LAMBDA (PKL)
						(EQUAL (CAR TESTPKLTAIL)
						       (PATHKEYS PKL) ) )))
		       (CDR (ASSQ (ROLEMARK (CAR ROLINKTAIL)) PF-ROLESORTS)) )
		    (PUSH (CAAR TESTPKLTAIL) INST-KEYS) )) ) ) )

(DEFUN ORDER-CNCPTS (NORML-CNCPT-LIST CNCPT-ANALYSIS-LIST)
 ;; NORML-CNCPT-LIST : (<normalized component-cncpt-ccplist> ... )
 ;; CNCPT-ANALYSIS-LIST :
 ;;  ((<normalized-concept-expr> <cc-op> <component-concept-expr> ... ) ... )
  (SORT NORML-CNCPT-LIST #'PRECEDES-CNCPT) )

; This fn uses freely the special variable CNCPT-ANALYSIS-LIST
(DEFUN PRECEDES-CNCPT (CNCPT1 CNCPT2)
  (COND ((EQ CNCPT1 CNCPT2) NIL)
	((EQ 'SIMPLEFORM (ATC-GET CNCPT1 'LT-TYPE))
	   (COND ((EQ 'SIMPLEFORM (ATC-GET CNCPT2 'LT-TYPE))
		    (ALPHALESSP CNCPT1 CNCPT2) )
		 (T T) ) )
	(T (COND ((EQ 'SIMPLEFORM (ATC-GET CNCPT2 'LT-TYPE)) NIL)
		 (T ;;(the following DO loop is too big to indent properly)
 (*CATCH 'PRE-CPT
   (DO ((KEYLIST1 (CDR (ASSQ (ATC-GET CNCPT1 'LT-FORMULA)
			     CNCPT-ANALYSIS-LIST )))
	(KEYLIST2 (CDR (ASSQ (ATC-GET CNCPT2 'LT-FORMULA)
			     CNCPT-ANALYSIS-LIST )))
	(COMPOUNDKEY-PAIRS) (KL1-LENGTH) (KL2-LENGTH) )
       ()
     A (SETQ KL1-LENGTH (LENGTH KEYLIST1)
	     KL2-LENGTH (LENGTH KEYLIST2) )
       (COND ((< KL1-LENGTH KL2-LENGTH) (*THROW 'PRE-CPT T))
	     ((< KL2-LENGTH KL1-LENGTH) (*THROW 'PRE-CPT NIL)) )
       (MAPC #'(LAMBDA (KEY1 KEY2)
		 (COND ((EQ 'SIMPLEFORM (OR (ATC-GET KEY1 'LT-TYPE)
					    (LT-TYPE KEY1) ))
			 ;; Some keys (cc-ops and raised atoms) don't have an
			 ;;  LT-TYPE property.  Examples: INST*B, ↑DRIVE, ↑2TRY.
			  (COND ((EQ 'SIMPLEFORM (OR (ATC-GET KEY2 'LT-TYPE)
						     (LT-TYPE KEY2) ))
				   (COND ((EQ KEY1 KEY2) NIL)
					 ((ALPHALESSP KEY1 KEY2)
					    (*THROW 'PRE-CPT T) )
					 (T (*THROW 'PRE-CPT NIL)) ) )
				(T (*THROW 'PRE-CPT T)) ) )
		       (T (COND ((EQ 'SIMPLEFORM (OR (ATC-GET KEY2 'LT-TYPE)
						     (LT-TYPE KEY2) ))
				   (*THROW 'PRE-CPT NIL) )
				(T (ENDADD (CONS (ATC-GET KEY1 'LT-FORMULA)
						 (ATC-GET KEY2 'LT-FORMULA) )
					   COMPOUNDKEY-PAIRS )) )) ) )
	     KEYLIST1 KEYLIST2 )
       (COND (COMPOUNDKEY-PAIRS
		(SETQ KEYLIST1 (CDR (ASSQ (CAAR COMPOUNDKEY-PAIRS)
					  CNCPT-ANALYSIS-LIST ))
		      KEYLIST2 (CDR (ASSQ (CDR (POP COMPOUNDKEY-PAIRS))
					  CNCPT-ANALYSIS-LIST )) )
		(OR (AND KEYLIST1 KEYLIST2)
		    (BREAK |PRECEDES-CNCPT - can't find new keylists!|))
		(GO A) )
	     (T (BREAK |PRECEDES-CNCPT - error: can't order concepts!|)) )
							     ) ) ) )) ) )

; this fn gets the position of PKLIST among the pathkeylists of λ-EXPR;
;  if λ-EXPR has been converted to an atom, then PKLIST will have just one
;  member, consisting of a single pathkey digit representing the right
;  corerole position.
(DEFMACRO (GET-PKL-POSITION defmacro-for-compiling 't) (PKLIST λ-EXPR)
  `(COND ((ATOM ,λ-EXPR) (CAR (PATHKEYS ,PKLIST)))
	 (T (DO ((PKLISTAIL (LT-PATHKEYLISTS ,λ-EXPR) (CDR PKLISTAIL))
		 (TALLYTAIL ALPHABET (CDR TALLYTAIL)) (PKLIST ,PKLIST) )
		((EQUAL PKLIST (CAR PKLISTAIL)) (CAR TALLYTAIL))
		(OR PKLISTAIL (BREAK |GET-PKL-POSITION - error|)) )) ) )

(DEFMACRO GET-Q-OP (PKLIST1 λ-EXPR1 PKLIST2 λ-EXPR2)
  `(LET ((QUANTKEY1 (GET-PKL-POSITION ,PKLIST1 ,λ-EXPR1))
	 (QUANTKEY2 (GET-PKL-POSITION ,PKLIST2 ,λ-EXPR2)) )
	(IMPLODE (NCONC (EXPLODE 'QUANT*) (LIST QUANTKEY1 QUANTKEY2))) ) )

(DEFMACRO ↑-ASCII (DECNUMBER)
  `(= 94. ,DECNUMBER) )

(DEFMACRO λ-ASCII (DECNUMBER)
  `(= 8. ,DECNUMBER) )

(DEFMACRO *-OR-↑-ASCII (DECNUMBER)
  `(MEMBER ,DECNUMBER '(42. 94.)) )

(DEFMACRO *-OR-C-ASCII (DECNUMBER)
  `(MEMBER ,DECNUMBER '(42. 67.)) )

(DEFMACRO C-ASCII (DECNUMBER)
  `(= 67. ,DECNUMBER) )

(DEFMACRO 2:9-ASCII (DECNUMBER)
  `(AND (> ,DECNUMBER 49.) (< ,DECNUMBER 58.)) )

(DEFMACRO NUMERAL-ASCII (DECNUMBER)
  `(AND (> ,DECNUMBER 47.) (< ,DECNUMBER 58.)) )

(DEFMACRO λ↑-RAISE-CC-OP (CC-OP)
 `(LET ((XPL-OP (EXPLODEN ,CC-OP)))
       (COND ((↑-ASCII (CAR XPL-OP)) (IMPLODE (APPEND '(λ ↑) XPL-OP)))
	     ((AND (λ-ASCII (CAR XPL-OP))
		   (↑-ASCII (CADR XPL-OP)) )
	        (COND ((*-OR-↑-ASCII (CADDR XPL-OP))
		         (SETF* (CDDR XPL-OP) (CONS 50. -*-))
			 (IMPLODE XPL-OP) )
		      ((2:9-ASCII (CADDR XPL-OP))
		         (SETF* (CADDR XPL-OP) (1+ -*-))
			 (OR (2:9-ASCII (CADDR XPL-OP))
			     (BREAK |λ↑-RAISE-CC-OP - not enough numerals.|) )
			 (IMPLODE XPL-OP) )
		      (T (IMPLODE (APPEND '(λ ↑ *) XPL-OP))) ) )
	     (T (IMPLODE (APPEND '(λ ↑ *) XPL-OP))) ) ) )

(DEFMACRO RAISE-CC (LT-FORM)
  `(COND ((EQ (LT-TYPE ,LT-FORM) '↑-TERM) (RAISE↑-TERM ,LT-FORM))
	 (T (MAKE-↑↓-TERM ↑↓-MARKER '↑
			  ↑↓-MATRIX ,LT-FORM )) ) )

(DEFMACRO RAISE-CC-OP (CC-OP)
 `(LET ((XPL-OP (EXPLODEN ,CC-OP)))
       (COND ((↑-ASCII (CAR XPL-OP))
	        (COND ((*-OR-C-ASCII (CADR XPL-OP))
		         (SETF* (CDR XPL-OP) (CONS 50. -*-))
			 (IMPLODE XPL-OP) )
		      ((2:9-ASCII (CADR XPL-OP))
		         (SETF* (CADR XPL-OP) (1+ -*-))
			 (OR (2:9-ASCII (CADR XPL-OP))
			     (BREAK |RAISE-CC-OP - not enough numerals.|) )
			 (IMPLODE XPL-OP) )
		      (T (BREAK |RAISE-CC-OP - improper cc-op.|)) ) )
	     ((AND (λ-ASCII (CAR XPL-OP))
		   (↑-ASCII (CADR XPL-OP)) )
	        (COND ((OR (*-OR-↑-ASCII (CADDR XPL-OP))
			   (2:9-ASCII (CADDR XPL-OP)) )
		         (IMPLODE (CONS '↑ XPL-OP)) )
		      (T (IMPLODE (APPEND '(↑ *) XPL-OP))) ) )
	     (T (IMPLODE (APPEND '(↑ *) XPL-OP))) ) ) )

(DEFMACRO GET-BASE-OP (CC-OP)
 `(LET* ((XPL-OP (NREVERSE (CDR (MEMQ *-ASCII (NREVERSE (EXPLODEN ,CC-OP))))))
	 (SHORT-XPL-OP (CDR (MEMQ *-ASCII XPL-OP))) )
	(IMPLODE (COND (SHORT-XPL-OP) (T XPL-OP))) ) )

(DEFMACRO  GET-S&S-KEY (CC-OP CC-KEYNUM)
 `(LET ((BASE-OP (GET-BASE-OP ,CC-OP)))
       (CASEQ BASE-OP
	  ((INST QUANT CNCT) (NTH (- ,CC-KEYNUM 2) ALPHABET))
	  (T (BREAK |GET-S&S-KEY - unrecognized base-cc-op.|)) ) ) )

(DEFUN NORMRAISE-CC (CC-KEYS &optional λ-PREFIX)
		  ;; CC-KEYS: (<cc-op> <component-concept-expr> ... )
 (DO ((CC-KEYTAIL CC-KEYS (CDR CC-KEYTAIL))
      (KEYNUM 0 (1+ KEYNUM))
      (NORMRAISEDKEYS) )
     ((NULL CC-KEYTAIL) (NREVERSE NORMRAISEDKEYS))
     (PUSH
      (COND
        ((ATOM (CAR CC-KEYTAIL))
	   (COND ((= KEYNUM 0)
		    (COND (λ-PREFIX (λ↑-RAISE-CC-OP (CAR CC-KEYTAIL)))
			  (T (RAISE-CC-OP (CAR CC-KEYTAIL))) ) )
		 (T (RAISEATOM (CAR CC-KEYTAIL))) ))
	(T (LET* ((MATCH-PKLS
		    (COND (λ-PREFIX (COND ((= 1 KEYNUM)
					     (COPYALLCONS (CDR λ-PREFIX)) )
					  (T (SELECT&SHORTEN
						(GET-S&S-KEY (CAR CC-KEYS)
							     KEYNUM )
						(CDR λ-PREFIX)
						(LT-λ-SCOPE (CAR CC-KEYTAIL)) )) ))) )
		  (ORIG-λPKL-IMAGES
		    (COND (MATCH-PKLS
			    (COLLECT-IMAGES MATCH-PKLS (CAR CC-KEYTAIL)) )) )
		  (NON-IMAGE-λPKLS
		    (COND ((#.(ISA-OF:LT . λ-EXPR) (CAR CC-KEYTAIL))
			     (SUBSET (LT-PATHKEYLISTS (CAR CC-KEYTAIL))
				     #'(LAMBDA (PKEYLIST)
					 (NOT (MEMBER PKEYLIST
						      ORIG-λPKL-IMAGES))) ) )) )
		  (NEW-CC-EXPR
		    (COND (ORIG-λPKL-IMAGES
			      (MAKE-LT-λ-EXPR
				λ-PREFIX (MAKE-LT-λ-PREFIX
					    PATHKEYLISTS
					    (ORDER-PATHKEYLISTS
					      (RAISE-λ-TERMSORTS
					         ORIG-λPKL-IMAGES ) ) )
				λ-SCOPE
				 (RAISE-CC
				   (COND (NON-IMAGE-λPKLS
					  (MAKE-LT-λ-EXPR
					    λ-PREFIX
					      (MAKE-LT-λ-PREFIX
						 PATHKEYLISTS
						 (ORDER-PATHKEYLISTS
						       NON-IMAGE-λPKLS ) )
					    λ-SCOPE
					      (LT-λ-SCOPE (CAR CC-KEYTAIL)) ) )
					 (T (LT-λ-SCOPE (CAR CC-KEYTAIL))) ))))
			  (T (RAISE-CC (CAR CC-KEYTAIL))) ) )
		  (NEW-λ-PREFIX
		    (COND ((#.(ISA-OF:LT . λ-EXPR) NEW-CC-EXPR)
			     (LT-λ-PREFIX NEW-CC-EXPR) )) )
		  (NEW-CC-KEYS (CDR (ASSQ (CAR CC-KEYTAIL)
					  ↑-MATRIX-ANALYSIS-LIST ))) )
		 (COND (NEW-λ-PREFIX
			 (NORMALIZE-CMPD-CONCEPT
			      NEW-CC-EXPR
			      (NORMRAISE-CC NEW-CC-KEYS NEW-λ-PREFIX)
			      AL-VARS ) )
		       (T (NORMALIZE-CMPD-CONCEPT
			      NEW-CC-EXPR
			      (NORMRAISE-CC NEW-CC-KEYS)
			      AL-VARS )) ) )) )
      NORMRAISEDKEYS ) ) )

; QV-QUASI-UNSUBST searches out each occurrence of the quantifier or variable
; UNSUBSTERM in LT-FORM, [a previous version removed UNSUBSTERM from the
; dependency lists of any quantifiers occurring within LT-FORM,] and returns a
; list of xpathkeys (i.e., unimploded pathkeys), one for each place in LT-FORM
; in which UNSUBSTERM occurs.  QV-QUASI-UNSUBST is called with 2 arguments by
; ANALYZE-CMPD-CONCEPT and ENCODE-LINFORMULA-S, and in turn calls itself with
; 3 arguments.  The third argument, KEYDIGIT, represents the alphabetic argument
; position of LT-FORM within the form that immediately contains it.  In
; general, KEYDIGIT is consed onto the xpathkeys returned by recursive calls to
; QV-QUASI-UNSUBST.  In particular, if UNSUBSTERM occurs as the jth argument of
; LT-FORM, then the partial xpathkey (<keydigit> <jth-letter>) is included in
; the list of such xpathkeys returned by that call to QV-QUASI-UNSUBST.

(DEFUN QV-QUASI-UNSUBST (UNSUBSTERM LT-FORM &optional KEYDIGIT)
  (CASEQ (LT-QQU-TYPE LT-FORM)
    ((ATOMICPROPO F-TERM)
      (DO ((RL-TAIL (ROLELINKS LT-FORM) (CDR RL-TAIL))
	   (NEWKEYDIGITAIL ALPHABET (CDR NEWKEYDIGITAIL))
	   (OUTXPKLIST) (NEWFORM) (XPATHKEYLIST) )
	  ((NULL RL-TAIL) OUTXPKLIST)
	  (SETQ NEWFORM (ARGUMENT (CAR RL-TAIL)))
	  (COND ((AND NEWFORM
		      (SETQ XPATHKEYLIST
			    (QV-QUASI-UNSUBST UNSUBSTERM  NEWFORM
					      (CAR NEWKEYDIGITAIL) )) )
		   (ADDCONC (COND (KEYDIGIT 
				   (MAP #'(LAMBDA (XPATHKEYTAIL)
					    (SETF* (CAR XPATHKEYTAIL)
						   (CONS KEYDIGIT -*-) ) )
					XPATHKEYLIST ) )
				  (T XPATHKEYLIST) )
			    OUTXPKLIST ) )) ) )
    (SIMPLEFORM
       (COND ((EQ LT-FORM UNSUBSTERM) (NCONS (NCONS KEYDIGIT)))
	     (T NIL) ) )
    (QT-PAIR
       (COND ((EQ (CDR LT-FORM) UNSUBSTERM) (NCONS (NCONS KEYDIGIT)))
	     (T NIL) ) )
    (CONN-PROPO		;; i.e., any connective
       (DO ((RL-TAIL (ROLELINKS LT-FORM) (CDR RL-TAIL))
	    (NEWKEYDIGITAIL ALPHABET (CDR NEWKEYDIGITAIL))
	    (OUTXPKLIST) (XPATHKEYLIST) )
	   ((NULL RL-TAIL) OUTXPKLIST)
	   (COND ((SETQ XPATHKEYLIST
			(QV-QUASI-UNSUBST UNSUBSTERM
					  (ARGUMENT (CAR RL-TAIL))
					  (CAR NEWKEYDIGITAIL) ) )
		    (ADDCONC (COND (KEYDIGIT 
				    (MAP #'(LAMBDA (XPATHKEYTAIL)
					     (SETF* (CAR XPATHKEYTAIL)
						    (CONS KEYDIGIT -*-) ) )
					 XPATHKEYLIST ) )
				   (T XPATHKEYLIST) )
			     OUTXPKLIST ) )) ) )
    ((↑-TERM ↓-TERM)
      (QV-QUASI-UNSUBST UNSUBSTERM (↑↓-MATRIX LT-FORM) KEYDIGIT) )
    (λ-PAIR NIL)
    (λ-EXPR
      (QV-QUASI-UNSUBST UNSUBSTERM (LT-λ-SCOPE LT-FORM) KEYDIGIT) )
    (QUANTIFIERFORM
     (LET ((XPATHKEYLIST 
	    (NCONC (QV-QUASI-UNSUBST UNSUBSTERM
				     (#.(THE-OF:LT-QUANT . QSORTEXPR) LT-FORM)
				     'A )
		   (QV-QUASI-UNSUBST UNSUBSTERM
				     (#.(THE-OF:LT-QUANT . SCOPE) LT-FORM)
				     'B ) ) ))
;	  (COND ((LT-Q-DEPENDENCIES LT-FORM)
;		   (SETF* (LT-Q-DEPENDENCIES LT-FORM)
;			  (DELQ UNSUBSTERM -*-) ) ) )
	  (COND (XPATHKEYLIST
		 (COND (KEYDIGIT 
			(MAP #'(LAMBDA (XPATHKEYTAIL)
				 (SETF* (CAR XPATHKEYTAIL)
					(CONS KEYDIGIT -*-) ) )
			     XPATHKEYLIST ) )
		       (T XPATHKEYLIST) ) )) ))
    (FIXNUM-VECTOR
       (DO ((VECTAIL LT-FORM (CDR VECTAIL))
	    (NEWKEYDIGITAIL ALPHABET (CDR NEWKEYDIGITAIL))
	    (OUTXPKLIST) )
	   ((NULL VECTAIL) OUTXPKLIST)
	   (COND ((EQ UNSUBSTERM (CAR VECTAIL))
		  (ENDADD (COND (KEYDIGIT 
				   (LIST KEYDIGIT (CAR NEWKEYDIGITAIL)) )
				 (T (NCONS (CAR NEWKEYDIGITAIL))) )
			   OUTXPKLIST ) )) ) )
    (T (BREAK |QV-QUASI-UNSUBST - unrecognized LT-FORM qqu-type.|)) ) )

(DEFUN ANALYZE-CMPD-CONCEPT (LT-FORM &optional AL-VARS)
;(break a-c-c:test)
  (CASEQ (LT-CONCEPT-TYPE LT-FORM)
    ((ATOMICPROPO F-TERM)
;     (SETF (ROLELINKS (CONCEPT-BODY LT-FORM)) ;; move this to construction points.
;	    (ORDER-ROLELINKS (CONCEPT-BODY LT-FORM)) )
      (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
	      (LET ((DO-LIST))
		   (COND ((SETQ DO-LIST (MERGED-PKLS (LT-PATHKEYLISTS LT-FORM)))
			    (ANALYZE-ROLEMERGE DO-LIST LT-FORM) )
			 ((SETQ DO-LIST (INST-KEYS LT-FORM))
			    (ANALYZE-INSTANTIATION DO-LIST LT-FORM) )
			 (T (ANALYZE-ADVERBIALIZATION LT-FORM)) ) ) )
	    (T (ANALYZE-INSTANTIATION (INST-KEYS LT-FORM) LT-FORM)) ) )
    (QUANTIFIERFORM
     (*CATCH 'Q-F
; The following rolemerge check is essential here because one of the λ-bound
; variables in a λ-expression with quantified λ-scope might occur free in both
; the QSORT-expr and the Q-SCOPE-expr of the outermost quantifier, which would
; require that a rolemerge operation take place subsequent to the quantification
; cc-op, in order to create the unified λ-variable reference in question.  The
; most intuitive role-unmerging at this point would be the minimal one of merely
; separating the QSORT occurrences from the Q-SCOPE ones, but in order to get a
; shorter overall analysis, we currently do the maximum amount of role-unmerging
; possible on a given variable all at once.
      (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
	      (LET ((DO-LIST (MERGED-PKLS (LT-PATHKEYLISTS LT-FORM))))
		   (COND (DO-LIST
			   (*THROW 'Q-F (ANALYZE-ROLEMERGE DO-LIST LT-FORM)) )) ) ))
      (LET* ((QUANTBODY (CONCEPT-BODY LT-FORM))
	     (OLDPATHKEYLISTS (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
				        (LT-PATHKEYLISTS LT-FORM))) )
	     (QSORT-NEWPATHKEYLIST
	      (ADJUST-λ-TERMSORT
	       (CONS NIL
		(ORDER-PATHKEYS
	         (MAPCAR #'IMPLODE
			 (QV-QUASI-UNSUBST
			     QUANTBODY
			     (#.(THE-OF:LT-QUANT . QSORTEXPR) QUANTBODY) ) ) ) )
	       (#.(THE-OF:LT-QUANT . QSORTEXPR) QUANTBODY) ) )
      	     (SCOPE-NEWPATHKEYLIST
	      (ADJUST-λ-TERMSORT
	       (CONS NIL
		(ORDER-PATHKEYS
		 (MAPCAR #'IMPLODE
			 (QV-QUASI-UNSUBST
			     QUANTBODY
			     (#.(THE-OF:LT-QUANT . SCOPE) QUANTBODY) ) ) ) )
	       (#.(THE-OF:LT-QUANT . SCOPE) QUANTBODY) ) )
	     (QSORTλ-EXPR (SETUP-λ-EXPR QSORT-NEWPATHKEYLIST
					OLDPATHKEYLISTS  'A
			          (#.(THE-OF:LT-QUANT . QSORTEXPR) QUANTBODY) ))
	     (SCOPEλ-EXPR (SETUP-λ-EXPR SCOPE-NEWPATHKEYLIST
					OLDPATHKEYLISTS  'B
			          (#.(THE-OF:LT-QUANT . SCOPE) QUANTBODY) ))
	     (NRML-QSORTλ-CCPLIST (NRML-ANL-YZE QSORTλ-EXPR AL-VARS))
	     (NRML-SCOPEλ-CCPLIST (NRML-ANL-YZE SCOPEλ-EXPR AL-VARS))
	     (Q-OPERATOR (GET-Q-OP QSORT-NEWPATHKEYLIST
				   (ATC-GET NRML-QSORTλ-CCPLIST 'LT-FORMULA)
				   SCOPE-NEWPATHKEYLIST
				   (ATC-GET NRML-SCOPEλ-CCPLIST 'LT-FORMULA) )) )
	    (LIST Q-OPERATOR
		  (#.(THE-OF:LT-QUANT . DETERMINER) QUANTBODY)
		  NRML-QSORTλ-CCPLIST
		  NRML-SCOPEλ-CCPLIST ) ) ) )
    (↑-TERM
     (LET* ((λ-EXPR-FLAG (#.(ISA-OF:LT . λ-EXPR) LT-FORM))
	    (↑-MATRIX-EXPR
	      (COND
		(λ-EXPR-FLAG
		  (LET ((λ-SCOPE (↑↓-MATRIX (LT-λ-SCOPE LT-FORM))))
		       (COND ((AND (EQ 'ATOMICPROPO (LT-TYPE λ-SCOPE))
				   (ATOM-CONVERTIBLE (LT-PATHKEYLISTS LT-FORM)
						     λ-SCOPE ) )
			        (PFC-CONCEPT λ-SCOPE) )
			     (T (SETQ λ-EXPR-FLAG 'UNCONVERTED)
				(MAKE-LT-λ-EXPR
				  λ-PREFIX (MAKE-LT-λ-PREFIX
					      PATHKEYLISTS 
					       (COPYALLCONS
						 (LT-PATHKEYLISTS LT-FORM) ) )
				  λ-SCOPE λ-SCOPE )) ) ) )
		(T (↑↓-MATRIX LT-FORM)) ) ) )
	   (COND ((EQ λ-EXPR-FLAG 'UNCONVERTED)
		    (LOWER-λ-TERMSORTS (LT-PATHKEYLISTS ↑-MATRIX-EXPR)) ))
	   (COND ((AND (EQ λ-EXPR-FLAG 'UNCONVERTED)
		       (EQ 'λ-EXPR (LT-TYPE (LT-λ-SCOPE ↑-MATRIX-EXPR))) )
		    (SETF* (LT-PATHKEYLISTS ↑-MATRIX-EXPR)
			   (ORDER-PATHKEYLISTS
			    (NCONC -*- (COPYALLCONS
					(LT-PATHKEYLISTS
					 (LT-λ-SCOPE ↑-MATRIX-EXPR) ) )) ) )
		    (SETF* (LT-λ-SCOPE ↑-MATRIX-EXPR) (LT-λ-SCOPE -*-)) ))
	   (COND ((MEMQ '↑-MATRIX-ANALYSIS-LIST AL-VARS)
		    (PROCESS-↑-MATRIX ↑-MATRIX-EXPR λ-EXPR-FLAG) )
		 (T (1ST-PROCESS-↑-MATRIX ↑-MATRIX-EXPR λ-EXPR-FLAG)) ) ) )
    (NEGPROPO
     (OR (INST-KEYS LT-FORM)
	  ;; We analyze the argument only if it is not implicitly λ-bound
	  ;;  (i.e., only if there is an INST-KEY).
	 (BREAK |ANALYZE-CMPD-CONCEPT - negation should have been atom-converted.|) )
     (LET* ((JUNCT-MATRIX (ARGUMENT (CAR (ROLELINKS (CONCEPT-BODY LT-FORM)))))
	    (JUNCT-EXPR
	      (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
		     (LET ((NEWPATHKEYLISTS
			     (ORDER-PATHKEYLISTS
			       (SELECT&SHORTEN 'A (LT-PATHKEYLISTS LT-FORM)
					          JUNCT-MATRIX ) ) ))
			  (COND ((AND (EQ 'ATOMICPROPO (LT-TYPE JUNCT-MATRIX))
				      (ATOM-CONVERTIBLE NEWPATHKEYLISTS
							JUNCT-MATRIX ) )
				   (PFC-CONCEPT JUNCT-MATRIX) )
				(T (MAKE-LT-λ-EXPR
				     λ-PREFIX (MAKE-LT-λ-PREFIX
						PATHKEYLISTS NEWPATHKEYLISTS )
				     λ-SCOPE JUNCT-MATRIX )) ) ) )
		    (T JUNCT-MATRIX) ) ) )
	   (LIST 'CNCT*A '¬ (NRML-ANL-YZE JUNCT-EXPR AL-VARS)) ) )
    ((CONJ-PROPO DISJ-PROPO)
      (*CATCH 'CD-P
       (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
	       (LET ((DO-LIST (MERGED-PKLS (LT-PATHKEYLISTS LT-FORM))))
		    (COND (DO-LIST
			    (*THROW 'CD-P (ANALYZE-ROLEMERGE DO-LIST LT-FORM)) )) ) ))
       (PUSH 'JUNCT-ANALYSIS-LIST AL-VARS)
       (LET ((CONN-KEYS (INST-KEYS LT-FORM)))
	      ;; We analyze only those arguments that are not implicitly λ-bound
	      ;;  (i.e., only those specified by CONN-KEYS).
       ;; DO loop text is too wide to indent fully
       (DO ((KEYTAIL CONN-KEYS (CDR KEYTAIL)) ;; rolelink-keys
	    (ROLINKS (ROLELINKS (CONCEPT-BODY LT-FORM)))
	    (JUNCT-MATRIX) (JUNCT-EXPR) (JUNCT-PATHKEYLISTS)
	    (NORML-JUNCT-LIST) (JUNCT-ANALYSIS-LIST) )
	   ((NULL KEYTAIL)
	     (FIX-AL JUNCT-ANALYSIS-LIST)
	     (SETQ NORML-JUNCT-LIST (ORDER-CNCPTS (CULL-EQS NORML-JUNCT-LIST)
						  JUNCT-ANALYSIS-LIST ) )
	     ;; for elegance, we should also prune and order the rolelinks of
	     ;;  (CONCEPT-BODY LT-FORM) in accordance with NORML-JUNCT-LIST,
	     ;;  making appropriate adjustments to (LT-λ-PREFIX LT-FORM), if any
	     ;;  (but only if there isn't already a norml-formula in the dnet).
	     (LIST* (IMPLODE (NCONC (EXPLODE 'CNCT*) CONN-KEYS))
		    (PFC-CONCEPT (CONCEPT-BODY LT-FORM))
		    ;; connectives are always atom-convertible -- no adverbs.
		    NORML-JUNCT-LIST ) )
	   (SETQ JUNCT-MATRIX (ARGUMENT (ALPHA-NTH (CAR KEYTAIL) ROLINKS))
		 JUNCT-EXPR
		  (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
			   (SETQ JUNCT-PATHKEYLISTS
				 (ORDER-PATHKEYLISTS
				   (SELECT&SHORTEN (CAR KEYTAIL)
						   (LT-PATHKEYLISTS LT-FORM)
						   JUNCT-MATRIX ) ) )
			   (COND ((AND (EQ 'ATOMICPROPO (LT-TYPE JUNCT-MATRIX))
				       (ATOM-CONVERTIBLE JUNCT-PATHKEYLISTS
							 JUNCT-MATRIX ) )
				    (PFC-CONCEPT JUNCT-MATRIX) )
				 (T (MAKE-LT-λ-EXPR
				      λ-PREFIX (MAKE-LT-λ-PREFIX
						 PATHKEYLISTS JUNCT-PATHKEYLISTS )
				      λ-SCOPE JUNCT-MATRIX )) ) )
			(T JUNCT-MATRIX) ) )
	   (ENDADD (NRML-ANL-YZE JUNCT-EXPR AL-VARS) NORML-JUNCT-LIST) ) ) ) )
    ((⊃-PROPO ⊃-THEN-PROPO IF-WOULD-PROPO IF-THENWOULD-PROPO)
      (*CATCH 'CD-P
       (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
	       (LET ((DO-LIST (MERGED-PKLS (LT-PATHKEYLISTS LT-FORM))))
		    (COND (DO-LIST
			    (*THROW 'CD-P (ANALYZE-ROLEMERGE DO-LIST LT-FORM)) )) ) ))
       (LET ((ARG-KEYS (INST-KEYS LT-FORM)))
	      ;; We analyze only those arguments that are not implicitly λ-bound
	      ;;  (i.e., only those specified by ARG-KEYS).
       ;; DO loop text is too wide to indent fully
       (DO ((KEYTAIL ARG-KEYS (CDR KEYTAIL)) ;; rolelink-keys
	    (ROLINKS (ROLELINKS (CONCEPT-BODY LT-FORM)))
	    (ARG-MATRIX) (ARG-EXPR) (ARG-PATHKEYLISTS) (NORML-ARG-LIST) )
	   ((NULL KEYTAIL)
	     (LIST* (IMPLODE (NCONC (EXPLODE 'CNCT*) ARG-KEYS))
		    (PFC-CONCEPT (CONCEPT-BODY LT-FORM))
		    ;; connectives are always atom-convertible -- no adverbs.
		    NORML-ARG-LIST ) )
	   (SETQ ARG-MATRIX (ARGUMENT (ALPHA-NTH (CAR KEYTAIL) ROLINKS))
		 ARG-EXPR
		 (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
			  (SETQ ARG-PATHKEYLISTS
 				(ORDER-PATHKEYLISTS
				  (SELECT&SHORTEN 'A (LT-PATHKEYLISTS LT-FORM)
						     ARG-MATRIX ) ) )
			  (COND ((AND (EQ 'ATOMICPROPO (LT-TYPE ARG-MATRIX))
				      (ATOM-CONVERTIBLE ARG-PATHKEYLISTS
							ARG-MATRIX ) )
				   (PFC-CONCEPT ARG-MATRIX) )
				(T (MAKE-LT-λ-EXPR
				     λ-PREFIX (MAKE-LT-λ-PREFIX
						PATHKEYLISTS ARG-PATHKEYLISTS )
				     λ-SCOPE ARG-MATRIX )) ) )
		       (T ARG-MATRIX) ) )
	   (ENDADD (NRML-ANL-YZE ARG-EXPR AL-VARS) NORML-ARG-LIST) ) ) ) )
    (FIXNUM-VECTOR
     (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
	     (LET* ((V-BODY (CONCEPT-BODY LT-FORM))
		    (SIZE-LETTER (NTH (1- (LENGTH V-BODY)) ALPHABET)))
		   (DO ((V-TAIL V-BODY (CDR V-TAIL))
			(ALPHATAIL ALPHABET (CDR ALPHATAIL))
			(COMPONENT-KEYS-PTR (NCONS NIL))
			(COMPONENTS-PTR (NCONS NIL)) )
		       ((NULL V-TAIL)
			  (LIST* (IMPLODE (NCONC (EXPLODE 'VECT*)
						 (LIST SIZE-LETTER '*)
						 (CAR COMPONENT-KEYS-PTR) ))
				 (CAR COMPONENTS-PTR) ) )
		       (COND ((FIXP (CAR V-TAIL))
				(TCONC (CAR ALPHATAIL) COMPONENT-KEYS-PTR)
				(TCONC (CAR V-TAIL) COMPONENTS-PTR) )) ) ) )
	   (T (LET ((SIZE-LETTER (NTH (1- (LENGTH LT-FORM)) ALPHABET)))
		   (LIST* (IMPLODE (NCONC (EXPLODE 'VECT*) (NCONS SIZE-LETTER)))
			  LT-FORM ) )) ) )
    (T (BREAK |ANALYZE-CMPD-CONCEPT - unrecognized form type|)) ) )

(DEFUN NACC (LT-FORM &optional AL-VARS)
  (NRML-ANL-YZE LT-FORM AL-VARS) )


(DEFMACRO GET-PK-POSITION (PATHKEY PKEYLISTS)
  `(DO ((PKLISTAIL ,PKEYLISTS (CDR PKLISTAIL))
	(TALLYTAIL 2-ALPHABETS (CDR TALLYTAIL)) (PATHKEY ,PATHKEY) )
       ((NULL PKLISTAIL)
	  (BREAK |GET-PK-POSITION - PATHKEY not found!|) )
       (COND ((EQ PATHKEY (CAR (PATHKEYS (CAR PKLISTAIL))))
	       (RETURN
		(COND ((CAR TALLYTAIL))
		      (T (BREAK |GET-PK-POSITION - not enough indices!|)) ) ) )) ) )

(DEFMACRO GET-MERGEKEYS (MERGED-PKLS NEWPKLISTS LT-λ-EXPR)
  `(ORDER-PATHKEYLISTS
     (DO ((OLDPKL-TAIL (LT-PATHKEYLISTS ,LT-λ-EXPR) (CDR OLDPKL-TAIL))
	  (MKEYLISTS) )
	 ((NULL OLDPKL-TAIL) MKEYLISTS)
	  ;; MKEYLISTS : ((<1-digit-merge-position-key> ... ) ... )
	 (COND ((MEMQ (CAR OLDPKL-TAIL) ,MERGED-PKLS)
		 ;; if pathkeylist is rolemerged, then collect the
		 ;;  merge-position keys corresponding to its members.
		 (PUSH (ORDER-PATHKEYS
			 (MAPCAR #'(LAMBDA (OLDPKEY)
				     (GET-PK-POSITION OLDPKEY ,NEWPKLISTS) )
				 (PATHKEYS (CAR OLDPKL-TAIL)) ) )
		       MKEYLISTS ) )) ) ) )

(DEFMACRO EXPAND-MERGED-PKEYLISTS (MERGED-PKLS LT-λ-EXPR)
  `(ORDER-PATHKEYLISTS
     (DO ((OLDPKL-TAIL (LT-PATHKEYLISTS ,LT-λ-EXPR) (CDR OLDPKL-TAIL))
	  (NEWPKLISTPTR (NCONS NIL)) )
	 ((NULL OLDPKL-TAIL) (CAR NEWPKLISTPTR))
	 (COND ((MEMQ (CAR OLDPKL-TAIL) ,MERGED-PKLS)
		  (LCONC (MAPCAR #'(LAMBDA (PATHKEY)
				     (LIST (λ-TERMSORT (CAR OLDPKL-TAIL))
					   PATHKEY ) )
				 (PATHKEYS (CAR OLDPKL-TAIL)) )
			 NEWPKLISTPTR ) )
	       ((TCONC (COPYLIST (CAR OLDPKL-TAIL)) NEWPKLISTPTR)) ) ) ) )
		 ;; no need to ORDER-PATHKEYS here, since each new pathkeylist
		 ;;  has just one member.

(DEFUN ANALYZE-ROLEMERGE (MERGED-PKLS LT-λ-EXPR)
  (LET* ((NEWPKEYLISTS (ORDER-PATHKEYLISTS
			  (EXPAND-MERGED-PKEYLISTS MERGED-PKLS LT-λ-EXPR) ))
	 (MERGEKEYLISTS (GET-MERGEKEYS MERGED-PKLS NEWPKEYLISTS LT-λ-EXPR))
	 (RLMRG-OP (DO ((MKL-TAIL (CDR MERGEKEYLISTS) (CDR MKL-TAIL))
			(IMPLISTPTR (NCONS NIL)) )
		       ((NULL MKL-TAIL)
			  (IMPLODE (NCONC (EXPLODE 'RLMRG*)
					  (CAR MERGEKEYLISTS)
					  (CAR IMPLISTPTR) )) )
		       (LCONC (CONS '+ (CAR MKL-TAIL)) IMPLISTPTR) ) )
	 (λ-SCOPE (LT-λ-SCOPE LT-λ-EXPR))
	 (NEWEXPR (COND ((AND (EQ 'ATOMICPROPO (LT-TYPE λ-SCOPE))
			      (ATOM-CONVERTIBLE NEWPKEYLISTS λ-SCOPE) )
			   (PFC-CONCEPT λ-SCOPE) )
			((MAKE-LT-λ-EXPR
			  λ-PREFIX (MAKE-LT-λ-PREFIX PATHKEYLISTS NEWPKEYLISTS)
			  λ-SCOPE λ-SCOPE )) )) )
	(LIST RLMRG-OP
	      (NRML-ANL-YZE NEWEXPR AL-VARS) ) ) )

(DEFUN ATOM-CONVERTIBLE (PATHKEYLISTS λ-SCOPE 
				 &aux (PKL-LENGTH (LENGTH PATHKEYLISTS)) )
       ;; there are as many pathkeylists as coreroles, and as rolelinks;
  (AND (= PKL-LENGTH (LENGTH (GET (PFC-CONCEPT λ-SCOPE) 'COREROLES)))
       (= PKL-LENGTH (LENGTH (ROLELINKS λ-SCOPE)))
	;; and each pathkeylist has just one member, which is EQ to the
	;;  proper pathkey-digit.
       (DO ((PKL-TAIL PATHKEYLISTS (CDR PKL-TAIL))
	    (ALPHA-TAIL ALPHABET (CDR ALPHA-TAIL)) )
	   ((NULL PKL-TAIL) T)
	   (COND ((AND (MEMQ (CAR ALPHA-TAIL) (PATHKEYS (CAR PKL-TAIL)))
		       (NULL (CDR (PATHKEYS (CAR PKL-TAIL)))) ))
		 ((RETURN NIL)) ) ) ) )

(DEFUN ADJUST-λ-TERMSORT (PKEYLIST LT-FORM &aux PKEYSORT PKEYSORTS)
  (MAPC #'(LAMBDA (PATHKEY)
	    (SETQ PKEYSORT (PATHKEY-SORT PATHKEY LT-FORM))
	    (COND ((NOT (MEMBER PKEYSORT PKEYSORTS))
		     (PUSH PKEYSORT PKEYSORTS) )) )
	(PATHKEYS PKEYLIST) )
  (SETF (λ-TERMSORT PKEYLIST) (COMMON-SUBSORT* PKEYSORTS))
  (COND ((NULL (λ-TERMSORT PKEYLIST))
	   (BREAK |ADJUST-λ-TERMSORT - null λ-termsort!|) ))
  PKEYLIST )

(DEFUN COMMON-SUBSORT* (SORTLIST) ;; (presupposes no duplicates in SORTLIST)
  (COND ((NULL (CDR SORTLIST)) (CAR SORTLIST))
	(T (DO ((COMMON-SS*? (COND ((SUPERSORT* (CAR SORTLIST) (CADR SORTLIST))
				      (CADR SORTLIST) )
				   ((SUPERSORT* (CADR SORTLIST) (CAR SORTLIST))
				      (CAR SORTLIST) )
				   (T NIL) ))
		(SORTAIL (CDR SORTLIST)) )
	       ()
	       (COND ((NULL COMMON-SS*?) (RETURN NIL)))
	     A (SETF* SORTAIL (CDR -*-))
	       (COND ((NULL SORTAIL) (RETURN COMMON-SS*?))
		     ((SUPERSORT* (CAR SORTAIL) COMMON-SS*?) (GO A))
		     ((SUPERSORT* COMMON-SS*? (CAR SORTAIL))
		        (SETQ COMMON-SS*? (CAR SORTAIL))
			(GO A) )
		     (T (RETURN NIL)) ) )) ) )

; This fn returns T if SORT1 is a supersort* of (i.e., is more general than)
;  SORT2, and otherwise returns NIL.
(DEFUN SUPERSORT* (SORT1 SORT2)    ;; This relation is strict, i.e., asymmetric.
 (*CATCH 'SS*
  (COND ((AND (CONSP SORT1) (SYMBOLP (CAR SORT1)) (SYMBOLP (CDR SORT1))
	      (EQ '↑ (GETCHAR (CAR SORT1) 1)) )
	   (COND ((AND (CONSP SORT2) (SYMBOLP (CDR SORT2)))
		    (COND ((EQ (CAR SORT1) (CAR SORT2))
			     (*THROW 'SS* (SUPERSORT* (CDR SORT1) (CDR SORT2))) )) )
		 ((AND SORT2 (SYMBOLP SORT2)) (*THROW 'SS* NIL)) ) )
	((AND (EQ 'CONCEPT SORT1)  (CONSP SORT2)  (SYMBOLP (CAR SORT2))
	      (EQ '↑ (GETCHAR (CAR SORT2) 1))  (SYMBOLP (CDR SORT2)) )
	   (*THROW 'SS* 'T) )
	((NOT (AND (SYMBOLP SORT1) (SYMBOLP SORT2)))
	   (WRITE T "; Sort mismatch... "
		  T "; SORT1: " SORT1 " ,   SORT2: " SORT2 "."
		  (BREAK SUPERSORT*) ) ) )
  (PROG (SS*-CANDIDATE CURRENT-SS) 
	(COND ((OR (EQ SORT1 SORT2) (EQ SORT2 'THING)) (RETURN NIL)))
	(SETQ SS*-CANDIDATE (OR SORT1 (WRITE T "; SORT1 is null!"
					     (BREAK SUPERSORT*) )))
	(SETQ CURRENT-SS (OR (GET SORT2 'SUPERSORT)
			     (WRITE T "; No supersort for " SORT2 "."
				    (BREAK SUPERSORT*) ) ))
      A (COND ((EQ CURRENT-SS SS*-CANDIDATE) (RETURN T))
	      ((EQ CURRENT-SS 'THING) (RETURN NIL)) )
	(SETQ CURRENT-SS (OR (GET CURRENT-SS 'SUPERSORT)
			     (WRITE T "; No supersort for " CURRENT-SS "."
				    (BREAK SUPERSORT*) ) ))
	(GO A) ) ) )

(DEFMACRO (ISA-SUPERSORT-OF defmacro-for-compiling 't) (SORT1 SORT2)
 `(LET ((SORT1 ,SORT1)
	(SORT2 ,SORT2) )
       (OR (EQ SORT1 SORT2) (SUPERSORT* SORT1 SORT2)) ) )

(DEFMACRO MAKE-↑-MARKER (NUMBER-ATOM)
  `(COND ((= ,NUMBER-ATOM 1) '↑)
	 ((> ,NUMBER-ATOM 1)
	    (SETQ *NOPOINT T)	      ;; assumes *NOPOINT is null to start with.
	    (PROG1 (IMPLODE (APPEND '(↑) (EXPLODE ,NUMBER-ATOM)))
		   (SETQ *NOPOINT NIL) ) )
	 (T (BREAK |MAKE-↑-MARKER - zero ↑-value!|)) ) )

(DEFUN PATHKEY-SORT (PATHKEY LT-FORM)
  (DO ((KEYLIST (EXPLODE PATHKEY) (CDR KEYLIST))
       (NEW-CURRENTFORM LT-FORM)
       (↑-TALLY 0)
       (CURRENTFORM) (CURRENTYPE) (PFC-ROLESORTS) (BASE-ROLESORT) )
      ((NULL KEYLIST)
        (*CATCH 'P-S-DO
	 (COND ((EQ CURRENTYPE 'FIXNUM-VECTOR) (*THROW 'P-S-DO 'NUMBER)))
         (SETQ PFC-ROLESORTS (OR (GET (PFC-CONCEPT CURRENTFORM) 'ROLESORTS)
				 (WRITE T "; No rolesorts for concept "
					(PFC-CONCEPT CURRENTFORM) "."
					(BREAK PATHKEY-SORT) ) )
	       BASE-ROLESORT (OR (CDR (ASSQ (ROLEMARK NEW-CURRENTFORM)
					    PFC-ROLESORTS ))
				 (WRITE T "; No rolesort for role "
					(ROLEMARK NEW-CURRENTFORM)
					T "; of concept "
					(PFC-CONCEPT CURRENTFORM) "."
					(BREAK PATHKEY-SORT) ) ) )
	 (COND ((CONSP BASE-ROLESORT)
		  (SETQ ↑-TALLY (+ ↑-TALLY (GET-↑-TALLY (CAR BASE-ROLESORT)))
			BASE-ROLESORT (CDR BASE-ROLESORT) ) ))
	 (COND ((> ↑-TALLY 0)
		  (CONS (MAKE-↑-MARKER ↑-TALLY) BASE-ROLESORT) )
	       (T BASE-ROLESORT) ) ) )
      (SETQ CURRENTFORM NEW-CURRENTFORM)
    A (SETQ CURRENTYPE (LT-TYPE CURRENTFORM))
      (CASEQ CURRENTYPE
	 ((ROLELINK λ-EXPR) (SETQ CURRENTFORM (CDR CURRENTFORM)) (GO A))
	 (↑-TERM (SETQ ↑-TALLY (+ ↑-TALLY (GET-↑-TALLY (↑↓-MARKER CURRENTFORM)))
		       CURRENTFORM (CDR CURRENTFORM) ) (GO A) ) )
	 ;; "CDR" here is indifferent between the equivalent accessor
	 ;;   macros "ARGUMENT", "↑↓-MATRIX", and "λ-SCOPE".
      (SETQ NEW-CURRENTFORM (TERM-SUBRANCH (CAR KEYLIST)
				       CURRENTYPE
				       CURRENTFORM )) ) )

(DEFUN GET-ROLELINK (PATHKEY LT-FORM)
  (DO ((KEYLIST (EXPLODE PATHKEY) (CDR KEYLIST))
       (CURRENTFORM LT-FORM)
       (CURRENTYPE) )
      ((NULL KEYLIST) CURRENTFORM)
    A (SETQ CURRENTYPE (LT-TYPE CURRENTFORM))
      (COND ((MEMQ CURRENTYPE '(ROLELINK ↑-TERM λ-EXPR))
	       (SETQ CURRENTFORM (CDR CURRENTFORM))  (GO A) ))
		;; "CDR" here is indifferent between the equivalent accessor
		;;   macros "ARGUMENT", "↑↓-MATRIX", and "λ-SCOPE".
      (SETQ CURRENTFORM (TERM-SUBRANCH (CAR KEYLIST)
				       CURRENTYPE
				       CURRENTFORM )) ) )

(DEFUN TERM-SUBRANCH (KEY TYPE LT-FORM)
  (COND ((CASEQ TYPE
	   ((ATOMICPROPO F-TERM CONJ-PROPO DISJ-PROPO ⊃-PROPO ⊃-THEN-PROPO
			 IF-WOULD-PROPO IF-THENWOULD-PROPO )
	      (ALPHA-NTH KEY (ROLELINKS LT-FORM)) )
	   (NEGPROPO (CAR (ROLELINKS LT-FORM)))
	   (QUANTIFIERFORM (CASEQ KEY
			     (A (#.(THE-OF:LT-QUANT . QSORTEXPR) LT-FORM))
			     (B (#.(THE-OF:LT-QUANT . SCOPE) LT-FORM)) ))
	   (FIXNUM-VECTOR (LIST 'FN-VECTOR-LINK KEY LT-FORM))
	   (T (BREAK |TERM-SUBRANCH - unrecognized form-type|)) ))
	(T (BREAK |TERM-SUBRANCH - missing sub-branch!|)) ) )

(DEFUN COPYALLCONS (S-EXPR)
  (COND ((ATOM S-EXPR) S-EXPR)
	(T (CONS (COPYALLCONS (CAR S-EXPR)) (COPYALLCONS (CDR S-EXPR)))) ) )

(DEFUN COPY-1-1-PKLS (PATHKEYLISTS)
  (MAPCAN #'(LAMBDA (PKEYLIST)
	      (COND ((AND (NULL (CDR (PATHKEYS PKEYLIST)))
			  (NOT (GETCHAR (CAR (PATHKEYS PKEYLIST)) 2)) )
		       (NCONS (COPYLIST PKEYLIST)))) )
	  PATHKEYLISTS ) )

(DEFUN LT-COPYALL (LT-FORM &aux SUBSTPAIRS TERMCOPIES QUANTCOPIES)
  (LT-SUBST* LT-FORM) )

;; LT-SUBST produces a modified copy of LT-FORM that preserves EQ-ness of
;;  logical subexpressions, with the CAR of each SUBSTPAIR being substituted
;;  for its CDR throughout the copy.
(DEFUN LT-SUBST (SUBSTPAIRS LT-FORM &aux TERMCOPIES QUANTCOPIES)
  (LT-SUBST* LT-FORM) )

;; LT-SUBST* uses the freevars SUBSTPAIRS, TERMCOPIES, and QUANTCOPIES.
(DEFUN LT-SUBST* (LT-FORM &aux SUBSTPAIR)
 (COND ((SETQ SUBSTPAIR (OR (RASSQ LT-FORM SUBSTPAIRS)
			    (RASSQ LT-FORM TERMCOPIES) ))
	  (CAR SUBSTPAIR) )
       ((NULL LT-FORM) LT-FORM)
       (T ;; the following CASEQ is too wide to indent fully...
  (CASEQ (LT-TYPE LT-FORM)
    ((SIMPLEFORM PATT-VARIABLE) LT-FORM)
    (λ-PAIR
      (LET ((λ-PAIR-COPY (CONS 'λ (CDR LT-FORM))))
	   (PUSH (CONS λ-PAIR-COPY LT-FORM) TERMCOPIES)
	   λ-PAIR-COPY ) )
    (QT-PAIR
      (SETQ SUBSTPAIR (OR (RASSQ (CDR LT-FORM) QUANTCOPIES)
			  (CAR (PUSH (CONS '|unfound qt-pair cdr - LT-SUBST*|
					   (CDR LT-FORM) )
				     QUANTCOPIES )) ))
      (LET ((QT-PAIR-COPY (CONS 'QUANT-TERM (CAR SUBSTPAIR))))
	   (PUSH (CONS QT-PAIR-COPY LT-FORM) TERMCOPIES)
	   QT-PAIR-COPY ) )
    (QUANTIFIERFORM
      (LET ((QUANTCOPY (MAKE-LT-QUANTIFIER
			  Q-DETERMINER (LT-Q-DETERMINER LT-FORM) )))
	      ;; the first occurrence of a quantifierform is a proposition,
	      ;;  and is copied; subsequent occurrences of that same
	      ;;  quantifierform occur within qt-pairs that play the role of
	      ;;  quantified variables, and are NOT copied, but reproduced (EQ).
	   (PUSH (CONS QUANTCOPY LT-FORM) QUANTCOPIES)
	   (SETF (LT-QSORT-EXPR QUANTCOPY)
		 (LT-SUBST* (LT-QSORT-EXPR LT-FORM)) )
	   (SETF (LT-Q-SCOPE QUANTCOPY) (LT-SUBST* (LT-Q-SCOPE LT-FORM)))
	   (SETF (LT-Q-DEPENDENCIES QUANTCOPY)
		 (MAPCAN #'(LAMBDA (DEP)
			     (LET ((DEP-PAIR (RASSQ DEP QUANTCOPIES)))
				  (COND (DEP-PAIR (NCONS (CDR DEP-PAIR)))
					(T NIL) ) ) )
				   ;; In the null case, we are copying the
				   ;; Q-SCOPE of a λ-fied containing quantifier,
				   ;; and such "ghost" quantifiers should not
				   ;; appear in the new dependency list.
			 (LT-Q-DEPENDENCIES LT-FORM) ) )
	   QUANTCOPY ) )
    ((ATOMICPROPO F-TERM CONJ-PROPO NEGPROPO DISJ-PROPO ⊃-PROPO ⊃-THEN-PROPO
		  IF-WOULD-PROPO IF-THENWOULD-PROPO )
       (LET ((PFC-TERM-COPY
	      (MAKE-PFC-FORMULA
		PFC-CONCEPT (PFC-CONCEPT LT-FORM)
		ROLELINKS
		 (MAPCAR #'(LAMBDA (ROLINK)
			    (MAKE-ROLELINK
			       ROLEMARK (ROLEMARK ROLINK)
			       ARGUMENT (LT-SUBST* (ARGUMENT ROLINK)) ))
			 (ROLELINKS LT-FORM) ) ) ))
	    (PUSH (CONS PFC-TERM-COPY LT-FORM) TERMCOPIES)
	    PFC-TERM-COPY ) )
    ((λ-EXPR ↑-TERM ↓-TERM)
       (LET ((λ↑↓-TERM-COPY
	       (CONS (CAR LT-FORM) (LT-SUBST* (CDR LT-FORM))) ))
	    (PUSH (CONS λ↑↓-TERM-COPY LT-FORM) TERMCOPIES)
	    λ↑↓-TERM-COPY ) )
    (FIXNUM-VECTOR
      (LET ((VECTOR-COPY (MAPCAR #'(LAMBDA (ELEMENT)
				     (LT-SUBST* ELEMENT) )
				 LT-FORM )))
	   (PUSH (CONS VECTOR-COPY LT-FORM) TERMCOPIES)
	   VECTOR-COPY ) )
    (T (BREAK |LT-SUBST* - unrecognized lt-type.|)) ) ) ) )

(DEFUN SELECT&SHORTEN (KEYDIGIT PATHKEYLISTS NEW-λ-SCOPE)
 (MAPCAN
   #'(LAMBDA (PKEYLIST)
      (LET ((S&S-PATHKEYS
	     (ORDER-PATHKEYS
	      (MAPCAN #'(LAMBDA (PATHKEY)
			  (COND ((EQ KEYDIGIT (GETCHAR PATHKEY 1))
				 (NCONS (IMPLODE (CDR (EXPLODE PATHKEY)))) )) )
		      (PATHKEYS PKEYLIST) ) ) ))
	   (COND (S&S-PATHKEYS
		   (NCONS (COND ((λ-TERMSORT PKEYLIST)
				   (MAKE-PATHKEYLIST
				      PATHKEYS S&S-PATHKEYS
				      λ-TERMSORT (λ-TERMSORT PKEYLIST) ) )
				(T (ADJUST-λ-TERMSORT
				      (MAKE-PATHKEYLIST PATHKEYS S&S-PATHKEYS)
				      NEW-λ-SCOPE )) )) )) ) )
   PATHKEYLISTS ) )

; The policy on ordering pathkeys and pathkeylists is to order them immediately
;  upon construction, so that thereafter they can be assumed normally ordered.

; ORDER-PATHKEYLISTS should be used ONLY for its VALUE.  Since it uses
;  MACLISP's SORT function, its bare side-effect is incorrect.
(DEFUN ORDER-PATHKEYLISTS (PATHKEYLISTS)
  (SORT PATHKEYLISTS #'(LAMBDA (PKL1 PKL2)
			 (ALPHALESSP (CAR (PATHKEYS PKL1))
				     (CAR (PATHKEYS PKL2)) ) )) )

(DEFMACRO PRECEDES-ARG (ARG1 ARG2)
  `(LET ((COMPARISON (COMPARE-ARGS ,ARG1 ,ARG2)))
	(CASEQ COMPARISON (LESS T) (T NIL)) ) )

; This fn will have to compare only arguments of a PFC-FORMULA that have the
;  same rolemark.  The result of comparison is that ARG1 is either LESS, EQUAL,
;  or GREATER than ARG2, or INCOMPARABLE with ARG2.
(DEFUN COMPARE-ARGS (ARG1 ARG2)
 (LET ((TYPE1 (OR (ATC-GET ARG1 'LT-TYPE)
		  (GET-F-DESCRIPT ARG1 'LT-TYPE)
		  (LT-TYPE ARG1) ))
       (TYPE2 (OR (ATC-GET ARG2 'LT-TYPE)
		  (GET-F-DESCRIPT ARG2 'LT-TYPE)
		  (LT-TYPE ARG2) )) )
      (COND ((EQUAL ARG1 ARG2) 'EQUAL)
	    ((EQ 'VARIABLE TYPE1)
	       (COND ((EQ 'VARIABLE TYPE2)
		        (PRINC '|COMPARE-ARGS can't compare two variables!|)
			'INCOMPARABLE )
		     (T 'GREATER) ) )
	    ((EQ 'VARIABLE TYPE2) 'LESS)
	    ((EQ 'PATT-VARIABLE TYPE1)
	       (COND ((EQ 'PATT-VARIABLE TYPE2)
			(COND ((ALPHALESSP ARG1 ARG2) 'LESS)
		         ;; recall that at this point (NOT (EQUAL ARG1 ARG2))
			      (T 'GREATER) ) )
		     (T 'GREATER) ) )
	    ((EQ 'PATT-VARIABLE TYPE2) 'LESS)
	    ((MEMQ TYPE1 '(↑-TERM ↓-TERM))
	       (COND ((MEMQ TYPE2 '(↑-TERM ↓-TERM))
			(COMPARE-ARGS (↑↓-MATRIX ARG1) (↑↓-MATRIX ARG2)) )
		     (T 'GREATER) ) )
	    ((MEMQ TYPE2 '(↑-TERM ↓-TERM)) 'LESS)
	    ((#.(ISA-OF:LT . PFC-FORMULA) ARG1)
	       (COND ((#.(ISA-OF:LT . PFC-FORMULA) ARG2)
			(COMPARE-PFC-FORMULAS ARG1 ARG2) )
		     (T 'GREATER) ) )
	    ((#.(ISA-OF:LT . PFC-FORMULA) ARG2) 'LESS)
	    ((EQ 'FIXNUM-VECTOR TYPE1)
	       (COND ((EQ 'FIXNUM-VECTOR TYPE2)
			(COMPARE-VECTORS ARG1 ARG2) )
		     (T 'GREATER) ) )
	    ((EQ 'FIXNUM-VECTOR TYPE2) 'LESS)
	    ((EQ 'SIMPLEFORM TYPE1)
	       (COND ((EQ 'SIMPLEFORM TYPE2)
			(COND ((ALPHALESSP ARG1 ARG2) 'LESS)
		         ;; recall that at this point (NOT (EQUAL ARG1 ARG2))
			      (T 'GREATER) ) )
		     (T (CA-PUNT TYPE1 TYPE2)) ) )
	    (T (CA-PUNT TYPE1 TYPE2)) ) ) )

(DEFUN CA-PUNT (T1 T2)
  (WRITE T "; Unanticipated arg-types: " T1 '|, | T2 (BREAK COMPARE-ARGS)) )

; The results of comparison are LESS, GREATER, or 'INCOMPARABLE.
(DEFUN COMPARE-PFC-FORMULAS (PFC-F1 PFC-F2)
  (COND ((NOT (EQ (PFC-CONCEPT PFC-F1) (PFC-CONCEPT PFC-F2)))
	   (COND ((ALPHALESSP (PFC-CONCEPT PFC-F1) (PFC-CONCEPT PFC-F2)) 'LESS)
		 (T 'GREATER) ) )
	(T (DO ((ROLINKS1 (ROLELINKS PFC-F1) (CDR ROLINKS1))
		(ROLINKS2 (ROLELINKS PFC-F2) (CDR ROLINKS2))
		(ROLINK1) (ROLINK2) (RO-INDEX) (COMPARISONS) )
	       ((OR (NULL ROLINKS1) (NULL ROLINKS2))
		  (COND ((MEMQ 'INCOMPARABLE COMPARISONS) 'INCOMPARABLE)
			(ROLINKS2 'LESS)
			(ROLINKS1 'GREATER)
			(T (BREAK |COMPARE-PFC-FORMULAS - formulas c-equal!|)) ) )
	       (SETQ ROLINK1 (CAR ROLINKS1) ROLINK2 (CAR ROLINKS2))
	       (COND ((NOT (EQ (ROLEMARK ROLINK1) (ROLEMARK ROLINK2)))
		       (SETQ RO-INDEX (GET (PFC-CONCEPT PFC-F1)
					   'ROLEORDERINDEX ))
		       (RETURN (COND ((COMPARE-ROLEORDER (ROLEMARK ROLINK1)
							 (ROLEMARK ROLINK2) )
				      ;; COMPARE-ROLEORDER uses RO-INDEX freely.
				        'LESS )
				     (T 'GREATER) )) ))
	       (LET ((COMPARISON (COMPARE-ARGS (ARGUMENT (CAR ROLINKS1))
					       (ARGUMENT (CAR ROLINKS2)) )))
		    (CASEQ COMPARISON
		       ((LESS GREATER) (RETURN COMPARISON))
		       (T (PUSH COMPARISON COMPARISONS) NIL) ) ) )) ) )

(DEFUN COMPARE-VECTORS (V1 V2)
  (COND ((EQUAL V1 V2) 'EQUAL)
	(T (DO ((VECTAIL1 V1 (CDR VECTAIL1))
		(VECTAIL2 V2 (CDR VECTAIL2)) )
	       ((OR (NULL VECTAIL1) (NULL VECTAIL2))
		  (COND (VECTAIL2 'LESS)
			(VECTAIL1 'GREATER)
			(T (BREAK |COMPARE-VECTORS - vectors appear equal!|)) ) )
	       (COND ((< (CAR VECTAIL1) (CAR VECTAIL2)) (RETURN 'LESS))
		     ((> (CAR VECTAIL1) (CAR VECTAIL2)) (RETURN 'GREATER)) ) )) ) )

(DEFMACRO SOME-DUPLICATE-ROLEMARKS (ROLINKS)
  `(DO ((ROLINKTAIL ,ROLINKS (CDR ROLINKTAIL)))
       ((NULL (CDR ROLINKTAIL)) NIL)
       (COND ((ASSQ (ROLEMARK (CAR ROLINKTAIL)) (CDR ROLINKTAIL))
	        (RETURN T) )) ) )

(DEFUN ORDER-ROLELINKS (PFC-FORM)
   ;; PFC-FORM is the argument here, rather than the rolelinks to be ordered,
   ;;  because we need to access the pfc-concept to get the roleorderindex.
  (LET ((RO-INDEX (GET (PFC-CONCEPT PFC-FORM) 'ROLEORDERINDEX))
	(IDENT-ROLES (GET (PFC-CONCEPT PFC-FORM) 'IDENTICAL-ROLES)) )
       (COND ((AND IDENT-ROLES (SOME-DUPLICATE-ROLEMARKS (ROLELINKS PFC-FORM)))
	        (SORT (ROLELINKS PFC-FORM)
		      #'(LAMBDA (ROLINK1 ROLINK2)
			  (COND ((EQ (ROLEMARK ROLINK1) (ROLEMARK ROLINK2))
				   (PRECEDES-ARG (ARGUMENT ROLINK1)
						 (ARGUMENT ROLINK2) ) )
				(T (COMPARE-ROLEORDER (ROLEMARK ROLINK1)
						      (ROLEMARK ROLINK2))) ) ) ) )
			    ;; COMPARE-ROLEORDER uses RO-INDEX freely.
	     (T (SORTCAR (ROLELINKS PFC-FORM) #'COMPARE-ROLEORDER)) ) ) )

;; COMPARE-ROLEORDER uses the variable RO-INDEX freely.
(DEFUN COMPARE-ROLEORDER (ROLEMARK1 ROLEMARK2)
  (MEMQ ROLEMARK2 (CDR (MEMQ ROLEMARK1 RO-INDEX))) )

(DEFUN CULL-EQS (LIST)
  (MAP #'(LAMBDA (LISTAIL)
	   (SETF* (CDR LISTAIL) (DELQ (CAR LISTAIL) -*-)) )
       LIST ) )

(DEFMACRO CONDENSE-RL-KEYLISTS (RL-KEYLISTS)
 `(DO ((RL-KEYLISTAIL ,RL-KEYLISTS (CDR RL-KEYLISTAIL))
       (DUPLISTAIL) )
      ((NULL RL-KEYLISTAIL) ,RL-KEYLISTS)
    A (COND ((SETQ DUPLISTAIL
		   (SOME (CDR RL-KEYLISTAIL)
			 #'(LAMBDA (RL-KEYLIST)
			     (AND (EQ (CAR RL-KEYLIST) (CAAR RL-KEYLISTAIL))
				  (NOT (OR (EQ 'λ-EXPR
					       (GET-F-DESCRIPT (CAR RL-KEYLIST)
							       'LT-TYPE ))
					   (ATC-GET (CAR RL-KEYLIST)
						    'COREROLES ) )) ) ) ) )
		    ;; (argument-taking concepts all have a COREROLES property.)
	       (NCONC (CAR RL-KEYLISTAIL) (CDAR DUPLISTAIL))
	       (DELQ (CAR DUPLISTAIL) RL-KEYLISTAIL)
	       (GO A) )) ) )
; Here we rely on the fact that rolemerges are analyzed out before
;  instantiations in ANALYZE-CMPD-CONCEPT, which implies that no argument-taking
;  concept should be condensed out of an rl-keylist.

(DEFUN SOME-DUPLICATE-IK-ROLEMARKS (INST-KEYS PFC-FORMULA)
 (*CATCH 'S-D-R
  (LET ((IDENT-ROLES (GET (PFC-CONCEPT PFC-FORMULA) 'IDENTICAL-ROLES)))
       (OR IDENT-ROLES (*THROW 'S-D-R NIL))
       (LET* ((ROLINKS (ROLELINKS PFC-FORMULA))
	      (CANDIDATES	;; a list of possibly duplicate rolemarks
		(MAPCAN #'(LAMBDA (INST-KEY)
			   (LET ((R-MARK (ROLEMARK (ALPHA-NTH INST-KEY ROLINKS))))
				(COND ((MEMQ R-MARK IDENT-ROLES) (NCONS R-MARK))
				      (T NIL) ) ) )
			INST-KEYS ) ) )
	     (MAP #'(LAMBDA (CAND-TAIL)
		      (COND ((MEMQ (CAR CAND-TAIL) (CDR CAND-TAIL))
			       (*THROW 'S-D-R CANDIDATES) )) )
		  CANDIDATES )
	     NIL ) ) ) )

(DEFMACRO ATOM-QUASI-UNSUBST (INST-KEYS λ-SCOPE)
   ;; INST-KEYS: (<1-digit-pathkey> ... )
 `(PROGN
   (DO ((INSTKEYTAIL ,INST-KEYS (CDR INSTKEYTAIL))
	(RL-KEYLISTSPTR (NCONS NIL))
	(λ-SCOPE-ROLINKS (ROLELINKS ,λ-SCOPE))
	(ARG-PKEYLISTS) (ARG-λ-SCOPE) (ARG-λ-EXPR) (NRML-ARG-λ-EXPR) )
       ((NULL INSTKEYTAIL)
	  (CONDENSE-RL-KEYLISTS (CAR RL-KEYLISTSPTR)) )
       (SETQ ARG-λ-SCOPE (ARGUMENT (ALPHA-NTH (CAR INSTKEYTAIL)
					      λ-SCOPE-ROLINKS )))
       (SETQ ARG-PKEYLISTS
	     (COND (OLDPKEYLISTS
		     (ORDER-PATHKEYLISTS
		       (SELECT&SHORTEN (CAR INSTKEYTAIL)
				       OLDPKEYLISTS
				       ARG-λ-SCOPE ) ) )) )
       (SETQ ARG-λ-EXPR 
	     (COND ((OR (NULL ARG-PKEYLISTS)
			(EQ (LT-TYPE ARG-λ-SCOPE) 'SIMPLEFORM) )
		      ARG-λ-SCOPE )
		   ((AND (MEMQ (LT-TYPE ARG-λ-SCOPE) '(ATOMICPROPO F-TERM))
			 (ATOM-CONVERTIBLE ARG-PKEYLISTS ARG-λ-SCOPE) )
		      (PFC-CONCEPT ARG-λ-SCOPE) )
		   (T (MAKE-LT-λ-EXPR
			 λ-PREFIX (MAKE-LT-λ-PREFIX PATHKEYLISTS ARG-PKEYLISTS)
			 λ-SCOPE ARG-λ-SCOPE )) ) )
       (SETQ NRML-ARG-λ-EXPR (NRML-ANL-YZE ARG-λ-EXPR AL-VARS))
       (COND ((NOT (OR (EQ 'λ-EXPR (GET-F-DESCRIPT NRML-ARG-λ-EXPR 'LT-TYPE))
		       (ATC-GET NRML-ARG-λ-EXPR 'COREROLES ) ))
	       ;; if NRML-ARG-λ-EXPR is neither an explicit nor implicit λ-EXPR,
	       ;; nor an atomic term, then normalize the corresponding sub-formula.
;	        (break a-q-u:test1)
		(SETF (ARGUMENT (ALPHA-NTH (CAR INSTKEYTAIL) λ-SCOPE-ROLINKS))
		      (COND ((ATOM ARG-λ-EXPR) ARG-λ-EXPR)
			    (T (ATC-GET NRML-ARG-λ-EXPR 'LT-FORMULA)) ) )
;		(break a-q-u:test2)
 ))
	  ;; For elegance, we should also prune and order the rolelinks of
	  ;;  λ-SCOPE in accordance with an ordered ARGSORT-INDEX (if non-NIL),
	  ;;  making appropriate adjustments to (LT-λ-PREFIX LT-FORM), if any
	  ;;  (but only if there isn't already a norml-formula in the dnet).
          ;;  (This would have to be done in ANALYZE-INSTANTIATION).
       (TCONC (LIST NRML-ARG-λ-EXPR (CAR INSTKEYTAIL)) RL-KEYLISTSPTR) ) ) )

(DEFUN ANALYZE-INSTANTIATION (INST-KEYS LT-FORM)
   ;; INST-KEYS: (<1-digit-pathkey> ... ); they determine the argument positions
   ;;		   that must be instantiated in a λ-expression to yield LT-FORM.
  (LET* ((λ-SCOPE (CONCEPT-BODY LT-FORM))
	 (OLDPKEYLISTS (COND ((#.(ISA-OF:LT . λ-EXPR) LT-FORM)
			         (LT-PATHKEYLISTS LT-FORM))) )
	 (RL-KEYLISTS (ATOM-QUASI-UNSUBST INST-KEYS λ-SCOPE))
	  ;; RL-KEYLISTS: ((<normalized component-concept> <pathkey> ...) ...)
	 (ADDPKEYLISTS (MAPCAR #'(LAMBDA (RL-KEYLIST)
				   (SETF* (CDR RL-KEYLIST)
					  (ADJUST-λ-TERMSORT
					       (CONS NIL
						     (ORDER-PATHKEYS -*-) )
					       λ-SCOPE ) ) )
			       RL-KEYLISTS ))
	 ;; RL-KEYLISTS:
	 ;;     ((<normalized component-concept> <termsort> <pathkey> ...) ...)
	 (NEWPKEYLISTS (ORDER-PATHKEYLISTS
			 (NCONC ADDPKEYLISTS (COPY-1-1-PKLS OLDPKEYLISTS)) ))
	 (NEW-PFC-EXPR 
	   (COND ((ATOM-CONVERTIBLE NEWPKEYLISTS λ-SCOPE) (PFC-CONCEPT λ-SCOPE))
		 (T (MAKE-LT-λ-EXPR
		       λ-PREFIX (MAKE-LT-λ-PREFIX PATHKEYLISTS NEWPKEYLISTS)
		       λ-SCOPE λ-SCOPE )) ) )
	 (NRML-NEW-PFC-EXPR (NRML-ANL-YZE NEW-PFC-EXPR AL-VARS))
	 (ARG-CONCEPTS (MAPCAR #'CAR RL-KEYLISTS))
;	 (test (break anal-inst:test))
	 ;; whereas INST-KEYS give the positions in the pfc-rolelinks that are
	 ;;  to be "unsubsted", OP-KEYS give the positions in the new λ-prefix
	 ;;  corresponding to the new ARG-CONCEPTS.  If the distinction were
	 ;;  necessary, it would be because other pathkeylists might intervene
	 ;;  between two INST-KEYS in the new λ-prefix.  But can this happen?
	 (OP-KEYS (MAPCAR #'(LAMBDA (RL-KEYLIST)
			      (GET-PKL-POSITION (CDR RL-KEYLIST)
						NEW-PFC-EXPR ) )
			  RL-KEYLISTS ))
	 (INST-OP (IMPLODE (NCONC (EXPLODE 'INST*) OP-KEYS))) )
	(OR (EQUAL INST-KEYS OP-KEYS)
	    ;; INST-KEYS, being shorter, should all come at the beginning.
	    (BREAK |ANAL-INST - INST-KEYS differs from OP-KEYS.|) )
	(LIST* INST-OP NRML-NEW-PFC-EXPR
		       ARG-CONCEPTS ) ) )

(DEFUN λ-UNSUBST (LT-λ-EXPR &optional (COPYFLAG 'COPY)
		   &aux (λ-SCOPE (COND (COPYFLAG
					  (LT-COPYALL (LT-λ-SCOPE LT-λ-EXPR)) )
				       (T (LT-λ-SCOPE LT-λ-EXPR)) ))
		   	ROLINK )
  (MAPC #'(LAMBDA (PKEYLIST)
	    (LET* ((λ-TERMSORT (λ-TERMSORT PKEYLIST))
		   (λ-PAIR (CONS 'λ λ-TERMSORT))
		   (↑-λ-TERMSORTFLAG
		      (AND (CONSP λ-TERMSORT)
			   (EQ '↑ (GETCHAR (CAR λ-TERMSORT) 1 )) ) ) )
		  (MAPC #'(LAMBDA (PATHKEY)
			   (SETQ ROLINK (GET-ROLELINK PATHKEY λ-SCOPE))
			   (COND ((AND ↑-λ-TERMSORTFLAG
				       (EQ (LT-TYPE (ARGUMENT ROLINK)) '↓-TERM) )
				    (SETQ ROLINK (ARGUMENT ROLINK)) ))
			   (COND ((EQ 'FN-VECTOR-LINK (ROLEMARK ROLINK))
				    (SETF (NTH (Z-BASE-EQUIV (CADR ROLINK))
					       (CADDR ROLINK) )
					  λ-PAIR ) )
				 (T (SETF (ARGUMENT ROLINK)
					  (COND ((AND ↑-λ-TERMSORTFLAG
						      (NOT (EQ (LT-TYPE ROLINK)
							       '↓-TERM ))
						      (EQ (LT-TYPE λ-SCOPE)
							  '↑-TERM ) )
						   (MAKE-↑↓-TERM
						     ↑↓-MARKER '↓
						     ↑↓-MATRIX λ-PAIR ) )
						(T λ-PAIR) ) ) ) ) )
			(PATHKEYS PKEYLIST) ) ) )
	(LT-PATHKEYLISTS LT-λ-EXPR) )
  (COND (COPYFLAG
	  (MAKE-LT-λ-EXPR λ-PREFIX (LT-λ-PREFIX LT-λ-EXPR)
			  λ-SCOPE λ-SCOPE ) )
	(T LT-λ-EXPR) ) )

(DEFMACRO CC-KEY-ROLINK-NUMBER (LT-FORM)
  `(COND ((ATOM ,LT-FORM) (LENGTH (GET ,LT-FORM 'COREROLES)))
	     ((LENGTH (LT-PATHKEYLISTS ,LT-FORM))) ) )

(DEFMACRO INITSTR= (TESTRING TARGETSTRING)
  `(DO ((TESTRING ,TESTRING)
	(TARGETSTRING ,TARGETSTRING)
	(TESTCHAR (GETCHAR ,TESTRING 1))
	(CHARINDEX 1 (1+ CHARINDEX)) )
       ((NULL TESTCHAR) T)
       (COND ((EQ TESTCHAR (GETCHAR TARGETSTRING CHARINDEX)))
	     (T (RETURN NIL)) )
       (SETQ TESTCHAR (GETCHAR TESTRING (1+ CHARINDEX))) ) )

; λ-INST-KEY returns a c-prefixed cc-op if CC-KEYLIST corresponds to a λ-expr.
(DEFUN λ-INST-KEY (CC-KEYLIST)
  (COND ((AND (INITSTR= 'INST* (CAR CC-KEYLIST))
	      (LET* ((CC-OP-CHARS (EXPLODE (CAR CC-KEYLIST)))
		     (ARGCHARS (CDR (MEMQ '* CC-OP-CHARS))) )
		    (COND ((< (LENGTH ARGCHARS)
			      (CC-KEY-ROLINK-NUMBER (CADR CC-KEYLIST)) )
			     (IMPLODE (CONS 'C CC-OP-CHARS)) )) ) ))) )

(DEFUN RAISEATOM (ATOM &aux (PNAMEASCIIS (EXPLODEN ATOM)))
  (COND ((↑-ASCII (CAR PNAMEASCIIS))
	   (COND ((NULL (CDR PNAMEASCIIS))
		    (SETF (CDR PNAMEASCIIS) (NCONS 50.)))
		 ((2:9-ASCII (CADR PNAMEASCIIS))
		    (SETF* (CADR PNAMEASCIIS) (1+ -*-))
		    (OR (2:9-ASCII (CADR PNAMEASCIIS))
			(BREAK |RAISEATOM - not enough numerals|) ) )
		 (T (SETF* (CDR PNAMEASCIIS) (CONS 50. -*-))) ) )
	(T (SETF* PNAMEASCIIS (CONS 94. -*-))) )
  (IMPLODE PNAMEASCIIS) )

(DEFUN GET-↑-MARKER (ATOM &aux (PNAMEASCIIS (EXPLODEN ATOM)))
  (OR (ATOM ATOM) (WRITE T "; ATOM non-atomic! => " ATOM (BREAK GET-↑-MARKER)))
  (COND ((↑-ASCII (CAR PNAMEASCIIS))
	   (COND ((AND (CDR PNAMEASCIIS)
		       (2:9-ASCII (CADR PNAMEASCIIS)) )
		    (SETF* (CDDR PNAMEASCIIS) NIL) )
		 (T (SETF* (CDR PNAMEASCIIS) NIL)) )
	   (IMPLODE PNAMEASCIIS) )
	(T NIL) ) )

(DEFUN GET-↑-TALLY (↑-ATOM)
 (*CATCH 'G↑T
  (COND ((NOT (AND (SYMBOLP ↑-ATOM) (EQ '↑ (GETCHAR ↑-ATOM 1))))
	   (WRITE T "; Bad argument: " ↑-ATOM (BREAK GET-↑-TALLY)) ))
  (LET ((ASCII2 (GETCHARN ↑-ATOM 2)))
       (COND ((OR (ZEROP ASCII2) (NOT (NUMERAL-ASCII ASCII2)))
	        (*THROW 'G↑T 1) )
	     (T (LET ((ASCII3 (GETCHARN ↑-ATOM 3)))
		     (COND ((OR (ZEROP ASCII3) (NOT (NUMERAL-ASCII ASCII3)))
			      (*THROW 'G↑T (- ASCII2 48.)) )) )) ) )
  (LET ((ASCIIS (EXPLODEN ↑-ATOM)))
       (DO ((ASCII-TAIL ASCIIS (CDR ASCII-TAIL)))
	   ((NULL ASCII-TAIL) NIL)
	   (COND ((AND (CDR ASCII-TAIL)
		       (NOT (NUMERAL-ASCII (CADR ASCII-TAIL))) )
		    (RPLACD ASCII-TAIL NIL)
		    (RETURN T) )) )
       (DO ((NUMASCII-TAIL (NREVERSE (CDR ASCIIS)) (CDR NUMASCII-TAIL))
	    (TALLY 0)
	    (TENS-FACTOR 1 (* TENS-FACTOR 10.)) )
	   ((NULL NUMASCII-TAIL) TALLY)
	   (SETQ TALLY (+ TALLY (* (- (CAR NUMASCII-TAIL) 48) TENS-FACTOR))) ))))

(DEFUN LOWER-↑-ATOM (ATOM &aux (PNAMEASCIIS (EXPLODEN ATOM)))
  (COND ((↑-ASCII (CAR PNAMEASCIIS))
	   (COND ((CADR PNAMEASCIIS)
		    (COND ((2:9-ASCII (CADR PNAMEASCIIS))
			     (SETF* (CADR PNAMEASCIIS) (1- -*-))
			     (OR (2:9-ASCII (CADR PNAMEASCIIS))
				 (SETF* (CDR PNAMEASCIIS) (CDDR -*-)) ) )
			  ((SETF* PNAMEASCIIS (CDR -*-))) ) )
		 ((SETF* PNAMEASCIIS (CDR -*-))) ) )
	((BREAK |LOWER-↑-ATOM - ATOM not an ↑-atom!|)) )
  (IMPLODE PNAMEASCIIS) )

(DEFUN LOWER-λ-TERMSORTS (PATHKEYLISTS)
  (MAPC #'(LAMBDA (PKEYLIST)
	    (LET ((TERMSORT (λ-TERMSORT PKEYLIST)))
		 (OR (AND (CONSP TERMSORT)
			  (EQ '↑ (GETCHAR (CAR TERMSORT) 1)) )
		     (BREAK |LOWER-λ-TERMSORT - improper ↑-λ-termsort.|) )
		 (COND ((EQ '↑ (CAR TERMSORT))
			  (SETF* (λ-TERMSORT PKEYLIST) (CDR -*-)) )
		       (T (SETF* (CAR TERMSORT) (LOWER-↑-ATOM -*-))) ) ) )
	PATHKEYLISTS ) )

(DEFUN RAISE-λ-TERMSORTS (PATHKEYLISTS)
  (MAPC #'(LAMBDA (PKEYLIST)
	    (LET ((TERMSORT (λ-TERMSORT PKEYLIST)))
		 (COND ((ATOM TERMSORT)
			  (SETF* (λ-TERMSORT PKEYLIST) (CONS '↑ -*-)) )
		       ((EQ '↑ (GETCHAR (CAR TERMSORT) 1))
			  (SETF* (CAR TERMSORT) (RAISEATOM -*-)) )
		       (T (BREAK |RAISE-λ-TERMSORT - improper λ-termsort.|)) ) ) )
	PATHKEYLISTS ) )

(DEFUN RAISE↑-TERM (↑-TERM &aux (↑-MARKASCIIS (EXPLODEN (↑↓-MARKER ↑-TERM))))
  (COND ((CDR ↑-MARKASCIIS)
	  (SETF* (CADR ↑-MARKASCIIS) (1+ -*-))
	  (OR (2:9-ASCII (CADR ↑-MARKASCIIS))
	      (BREAK |RAISE↑-TERM - not enough numerals|) ) )
	((SETF* (CDR ↑-MARKASCIIS) (CONS 50. -*-))) )
  (MAKE-↑↓-TERM ↑↓-MARKER (IMPLODE ↑-MARKASCIIS)
		↑↓-MATRIX (↑↓-MATRIX ↑-TERM) ) )

(DEFMACRO NEXTLETTER (LETTER)
  `(OR (CADR (MEMQ ,LETTER ALPHABET))
       (BREAK |NEXTLETTER - off the end|) ) )

(DEFUN KEYNUMBER (LETTER)
  (DO ((ALPHATAIL ALPHABET (CDR ALPHATAIL))
       (TALLY 1 (1+ TALLY)) )
      ((EQ LETTER (CAR ALPHATAIL)) TALLY) ) )

;  Processes to Expound Concept-Analyses and Explore a CC-Discrimination-Net

(DECLARE (special VERBOSITY V C |cc-op: |  |=>|  | - |  |.|
		  |. |  | .|  |, |  | ;|  | |  |  | )

	 (*lexpr ANALYZE&EXPOUND) )

(SETQ  V 'V  C 'C  |cc-op: | '|cc-op: |  |=>| '|=>|  | - | '| - |  |.| '|.|
       |. | '|. |  | .| '| .|  |, | '|, |  | ;| '| ;|  | | '| |  |  | '|  | )
  
;; LISTCOMPS uses the variable CURRENTPOS freely.
(DEFMACRO LISTCOMPS (COMPLIST)
 `(DO ((CC-COMPTAIL ,COMPLIST (CDR CC-COMPTAIL))
       (COMPNUM 1 (1+ COMPNUM)) )
      ((NULL CC-COMPTAIL) T)
      (SETQ CURRENTPOS 1)
      (WRITE T (POSPRINC COMPNUM |  |))
      (COND ((ATOM (CAR CC-COMPTAIL))
	       (WRITE (CAR CC-COMPTAIL)) )
	    (T (DISPLAY (CAR CC-COMPTAIL) CURRENTPOS)) ) ) )

(DEFMACRO EXPOUND-ANALYSIS-MODULE-1 (MODULE)
`(CASEQ VERBOSITY
  ((V VERBOSE)
   (WRITE T "The resulting normalized concept-formula is represented externally as: "
	  T (DISPLAY (CAR ,MODULE))
	  T "The concept thus represented has been analyzed as follows:" 
	  T "Concept-construction operator: " (CADR ,MODULE) | ;|
	  T "Component concepts: " )
   (LISTCOMPS (CDDR ,MODULE))
   (WRITE | .|) )
  ((C CONCISE)
   (WRITE T (DISPLAY (CAR ,MODULE)) |  | |=>|
	  T |cc-op: | (CADR ,MODULE) )
   (LISTCOMPS (CDDR ,MODULE))
   (WRITE | .|) ) ) )

;; POSPRINC uses the variable CURRENTPOS freely.
(DEFUN POSPRINC (&rest EXPRS
		 &aux (EXPRS-LENGTH (APPLY #'PLUS (MAPCAR #'FLATC EXPRS))) )
  (OR (> 81. EXPRS-LENGTH) (BREAK |POSPRINC - EXPRS too long for 1 line.|))
  (SETQ CURRENTPOS (+ CURRENTPOS EXPRS-LENGTH))
  (COND ((> 82. CURRENTPOS) (MAPC #'PRINC EXPRS))
	(T (SETQ CURRENTPOS (1+ EXPRS-LENGTH)) (TERPRI) (MAPC #'PRINC EXPRS)) ) )

(DEFUN A&E (CC-CONCEPT &optional (VERBOSITY 'V))
  (ANALYZE&EXPOUND CC-CONCEPT VERBOSITY) )

(DEFUN ANALYZE&EXPOUND (CC-CONCEPT &optional (VERBOSITY 'V)
				   &aux (CURRENTPOS 1) ANALYSIS-LIST )
  (NRML-ANL-YZE CC-CONCEPT (NCONS 'ANALYSIS-LIST))
  (FIX-AL ANALYSIS-LIST)
   ;; ANALYSIS-LIST :
   ;;  ((<normalized-concept-expr> <cc-op> <component-concept-expr> ... ) ... )
  (EXPOUND-ANALYSIS-MODULE-1 (CAR ANALYSIS-LIST))
  (MAPC #'EXPOUND-ANALYSIS-MODULE-2 (CDR ANALYSIS-LIST))
  (CASEQ VERBOSITY
    ((V VERBOSE)
       (WRITE T "This finishes the analysis of "
	      T (DISPLAY (CAAR ANALYSIS-LIST)) | .|) )
    ((C CONCISE)
       (WRITE T (DISPLAY (CAAR ANALYSIS-LIST)) " - analysis finished.") ) ) )

; FIX-AL accesses the global variable YHπ-FLAG.
(DEFUN FIX-AL (ANALYSIS-LIST)
; ANALYSIS-MODULE:     (<cmpd-lt-form-genl-plist> <cc-index-key> ... )
;		       or  (<compound lt-formula> <cc-index-key> ... )
  (MAPC #'(LAMBDA (ANALYSIS-MODULE)
	    (MAP #'(LAMBDA (CC-LINKS)
		     (COND ((AND (CONSP (CAR CC-LINKS))
				 (EQ '*CC-PLIST* (CAAR CC-LINKS)) )
			      (SETF* (CAR CC-LINKS)
				     (GET -*- 'LT-FORMULA) ) )
			   ((AND (ATOM (CAR CC-LINKS))
				 (LET ((LT-TYPE (OR (ATC-GET (CAR CC-LINKS)
							     'LT-TYPE )
						    (GET-F-DESCRIPT (CAR CC-LINKS)
								    'LT-TYPE ) )))
				      (AND LT-TYPE
					   (NOT (EQ LT-TYPE 'SIMPLEFORM)) ) ) )
			      (SETF* (CAR CC-LINKS)
				     (π-GET -*- 'LT-FORMULA) ) ) ) )
		 ANALYSIS-MODULE ) )
	ANALYSIS-LIST )
  ANALYSIS-LIST )

(DEFUN EXPOUND-ANALYSIS-MODULE-2 (MODULE)
 (CASEQ VERBOSITY
  ((V VERBOSE)
   (WRITE T (DISPLAY (CAR MODULE)) T "has, in turn, been analyzed as follows:" 
	  T "Concept-construction operator: " (CADR MODULE) | ;|
	  T "Component concepts: " )
   (LISTCOMPS (CDDR MODULE))
   (WRITE | .|) )
  ((C CONCISE)
   (WRITE T (DISPLAY (CAR MODULE)) |  | |=>|
	  T |cc-op: | (CADR MODULE) )
   (LISTCOMPS (CDDR MODULE))
   (WRITE | .|) ) ) )

;((EQ (TYPEP X) 'STRING) `(PRINC ,X))   ;;  This doesn't work in our maclisp.
; (ATOM X) is true of strings, and (TYPEP X) yields SYMBOL.
; STRINGP could be defined as follows, but that would be excessively wasteful
;  of conses, since most of the strings tested will be quite long.
;(DEFUN STRINGP (FORM)
;  (AND (ATOM FORM) (EQ '/" (CAR (EXPLODE FORM)))) )

;;;	Processes to Explore a Compound-Concept-Discrimination-Net

(DECLARE (special *WELCOMED-LIST* *IPC-PROGRAM-CMDS* IPC:ERRSET-FLAG
		  CURRENTNODE CURRENT-NODE-PATH TABVAL1 TABVAL2 
		  IPC:HELP-VERBOSITY IPC-HELP-TABLE XPDN-HELP-TABLE
		  *IPC:PROG-TASK-CMND-LISTS* TERMINAL-TYPE -EM:LINEL- )

	 (fixnum TABVAL1 TABVAL2 1ST-TABVAL 2ND-TABVAL N -EM:LINEL-)

	 (*lexpr EXPLORE-DNET DISPLAY-HELP-TABLE-ENTRY) )

(SETQ  *WELCOMED-LIST* NIL  *IPC-PROGRAM-CMDS* NIL  IPC:ERRSET-FLAG NIL
       IPC:HELP-VERBOSITY 'TERSE  IPC-HELP-TABLE NIL  TERMINAL-TYPE 'DM
       *IPC:PROG-TASK-CMND-LISTS* NIL  -EM:LINEL- 65. )

(DEFMACRO TRANSFER-CHECK (CMD-ATOM)
 `(COND ((MEMQ ,CMD-ATOM *IPC-PROGRAM-CMDS*)
	   (SETQ *NOPOINT NIL)  (RETURN COMMAND) )
	(T NIL) ) )

(DEFUN INADVERTENT-TRANSFER-CHECK (COMMND OWN-TASKNAME-LIST)
  (MULTIPLE-VALUE-BIND (TASKNAME-ATOM TRANS-CMD-LIST)
		       (COND ((SYMBOLP COMMND)
				(VALUES COMMND (NCONS COMMND)) )
			     ((CONSP COMMND)
				(VALUES (CAR COMMND) COMMND) ) )
       (MAPC #'(LAMBDA (TASKNAME-LIST)
		 (COND ((AND (NOT (EQ OWN-TASKNAME-LIST TASKNAME-LIST))
			     (MEMQ TASKNAME-ATOM (SYMEVAL TASKNAME-LIST)) )
			  (LET ((TRANS-PROG (CASEQ TASKNAME-LIST
					      (XCSR-TASK-CMNDS 'XCR)
					      (XPTR-TASK-CMNDS 'XTR)
					      (XPRG-TASK-CMNDS 'XRG)
					      (XPDN-TASK-CMNDS 'XDN) )) )
			       (*THROW 'IPC (LIST* TRANS-PROG
						   '1ST-COMMAND
						   TRANS-CMD-LIST )) ) )) )
	     *IPC:PROG-TASK-CMND-LISTS* ) ) )

(DEFMACRO GET-INT-PROG-COMMAND ()
 '(PROGN (WRITE T PROMPT-STRING)
	 (READ) ) )

(DEFUN XPDN (&optional INITIAL-KEYPATH (DNET *CONCEPTS*))
  (EXPLORE-DNET DNET NIL INITIAL-KEYPATH) )

;; The global variables CURRENTNODE and CURRENT-NODE-PATH are used freely 
;;  by EXPLORE-DNET and several subsidiary functions.
;; CURRENT-NODE-PATH: ({<leaf-node>} {<link-node>} ... {<*TOP*-link-node>})
;;  i.e., a PUSHed list of successive "currentnodes", in reverse order.
;; CURRENTNODE: maintained EQ to (CAR CURRENT-NODE-PATH).
(DEFUN EXPLORE-DNET (&optional DNET 1ST-COMMAND INITIAL-KEYPATH 
							&aux (-EM:LINEL- 85.) )
  (PROG (COMMAND PROMPT-STRING)
	(OR DNET (SETQ DNET *CONCEPTS*))
	(COND ((OR (NOT (BOUNDP 'CURRENT-NODE-PATH)) (NULL CURRENT-NODE-PATH))
	         (SETQ CURRENT-NODE-PATH (NCONS DNET)) ))
	(COND ((OR (NOT (BOUNDP 'CURRENTNODE)) (NULL CURRENTNODE))
	         (SETQ CURRENTNODE (TRAVERSE-LINKS DNET INITIAL-KEYPATH)) ))
	(SETQ PROMPT-STRING 'DN**)
	(COND ((OR (MEMQ 'XDN *WELCOMED-LIST*)
		   (EQ 'TERSE IPC:HELP-VERBOSITY) )
	         (WRITE T 'EXPLORE-DNET |.|) )
	      (T (PUSH 'XDN *WELCOMED-LIST*)
		 (WRITE T "Welcome to EXPLORE-DNET."
;; line too wide to indent fully
T "This program permits convenient interactive examination of a discrimination"
T "net that uniquely indexes logically compound concepts and propositions."
			T "Please type commands to the prompt DN**." ) ) )
	(COND (1ST-COMMAND (SETQ COMMAND 1ST-COMMAND) (GO CK)))
     A  (SETQ COMMAND (GET-INT-PROG-COMMAND))
     CK	(COND ((SYMBOLP COMMAND)
		 (TRANSFER-CHECK COMMAND) )
	      ((AND (CONSP COMMAND)
		    (SYMBOLP (CAR COMMAND))
		    (ALL (CDR COMMAND)
			 #'(LAMBDA (ARG) (OR (FIXP ARG) (SYMBOLP ARG))) ) )
		 (TRANSFER-CHECK (CAR COMMAND)) )
	      (T (WRITE T
		    '| - improper command or argument -- please try again ...| )
		 (GO A) ) )
	(OR (ERRSET
	 (CASEQ (COND ((SYMBOLP COMMAND) COMMAND) (T (CAR COMMAND)))
	   (CP (DISPLAY-KEYPATH CURRENT-NODE-PATH))
	   (CN (DISPLAY-NODE CURRENTNODE))
	   ((CPN PN) (DISPLAY-KEYPATH CURRENT-NODE-PATH)
		     (DISPLAY-NODE CURRENTNODE) )
	   (XP (COND ((OR (ATOM COMMAND) (NULL (CDR COMMAND)))
		         ;; missing argument defaults to 1.
		        (EXTEND-CURRENT-KEYPATH (NCONS 1)) )
		     (T (EXTEND-CURRENT-KEYPATH (CDR COMMAND))) ))
	   (SP (COND ((OR (ATOM COMMAND) (NULL (CDR COMMAND)))
		         ;; missing argument defaults to 1.
		        (SHORTEN-CURRENT-NODEPATH 1) )
		     (T (SHORTEN-CURRENT-NODEPATH (CADR COMMAND))) ))
	   (CLL (COUNT-LINKS&LEAVES CURRENTNODE))
	   ((PPV PPL) (OR (CONSP COMMAND) (SETF* COMMAND (NCONS -*-)))
		      (PRINT-PROPERTIES COMMAND) )
	   ((Q QUIT EXIT) (SETQ *NOPOINT NIL) (RETURN COMMAND))
	   ((? H) (XPDN-SHORT-HELP (COND ((ATOM COMMAND) NIL)
					 (T (CDR COMMAND)) )))
	   ((?? HH HELP) (XPDN-HELP (COND ((ATOM COMMAND) NIL)
					  (T (CDR COMMAND)) )))
	   (T (INADVERTENT-TRANSFER-CHECK COMMAND 'XPDN-TASK-CMNDS)
	      (WRITE T '| - unrecognized command| '| -- please try again ...|)) )
	IPC:ERRSET-FLAG )
	   (WRITE T '| - bad command//argument combination|
		    '| -- please try again ...| ) )
       (GO A) ) )

(*DEFUN (ISA . LEAF-NODE) (NODE)
   (OR (ATOM (LEAF-UNIT NODE))
       (EQ '*CC-PLIST* (CAR (LEAF-PLIST NODE))) ) )

(*DEFUN (ISA . CC-OP) (ATOM)
   (LET ((BASE-OP (GET-BASE-OP ATOM)))
	(MEMQ BASE-OP '(INST ADVB QUANT CNCT RLMRG VECT)) ) )

;; TRAVERSE-LINKS sets the freevar CURRENT-NODE-PATH
(DEFUN TRAVERSE-LINKS (START-NODE KEYS)
  (DO ((INDEX-KEYS KEYS (COND ((EQ '* (CAR INDEX-KEYS)) INDEX-KEYS)
			      (T (CDR INDEX-KEYS)) ))
       (NEW-CURRENTNODE START-NODE)
       (CURRENTKEY) (PATH-ADDITION) )
      ((NULL INDEX-KEYS) (ADDCONC PATH-ADDITION CURRENT-NODE-PATH)
			 NEW-CURRENTNODE )
    A (SETQ CURRENTKEY (CAR INDEX-KEYS))
       ;; check for special termination conditions.
      (COND ((#.(ISA . LEAF-NODE) NEW-CURRENTNODE)
	       (COND ((AND (EQ '* CURRENTKEY)
			   (NULL (CDR INDEX-KEYS)) )
		        (ADDCONC PATH-ADDITION CURRENT-NODE-PATH)
			(RETURN NEW-CURRENTNODE) )
		     (T (WRITE T
			  " - at leaf-node, but still have more keys specified!"
			  " -- please try again ..." )
			(RETURN START-NODE) ) ) )
	    ((AND (EQ '* CURRENTKEY) (< 1 (LENGTH (LINK-A-LIST NEW-CURRENTNODE))))
	       (COND ((CDR INDEX-KEYS)
		        (SETQ INDEX-KEYS (CDR INDEX-KEYS)) (GO A) )
		     ((EQ NEW-CURRENTNODE START-NODE)
		       (WRITE T
			"multiple keys currently available - keypath unchanged." ) ))
	       (ADDCONC PATH-ADDITION CURRENT-NODE-PATH)
	       (RETURN NEW-CURRENTNODE) ) )
      (SETQ NEW-CURRENTNODE (CASEQ (TYPEP CURRENTKEY)
			 (FIXNUM
			   (COND ((< CURRENTKEY 1)
				    (WRITE T
					 " - keynumber: " CURRENTKEY
					 " too small -- please try again ..." )
				    (RETURN START-NODE) )
				 ((NTH (1- CURRENTKEY)
				       (LINK-A-LIST NEW-CURRENTNODE) ))
				 (T (WRITE T
					 " - there is no a-list entry for keynumber: "
					 CURRENTKEY " -- please try again ..." )
				    (RETURN START-NODE) ) ) )
			 (SYMBOL
			   (COND ((EQ '* CURRENTKEY)
				    (CAR (LINK-A-LIST NEW-CURRENTNODE)) )
				 ((ASSQ CURRENTKEY (LINK-A-LIST NEW-CURRENTNODE)))
				 (T (WRITE T
					" - there is no a-list entry for key: "
					CURRENTKEY " -- please try again ..." )
				    (RETURN START-NODE) ) ) )
 			 (T (BREAK |TRAVERSE-LINKS - unacceptable key|)) ))
      (PUSH NEW-CURRENTNODE PATH-ADDITION) ) )

(DEFUN DISPLAY-KEYPATH (NODE-PATH &aux (CURRENTPOS 1) *NOPOINT )
;; NODE-PATH: ({<leaf-node>} {<link-node>} ... {<*TOP*-link-node>})
;;  i.e., a PUSHed list of successive "currentnodes", in reverse order,
;;  whose length is 1 greater than the displayed list of node-keys.
  (COND ((NULL (CDR NODE-PATH)) (WRITE T " - keypath currently empty -"))
	(T (WRITE T (POSPRINC "Current Keypath:"))
	   (DO ((DPYLIST (CDR (REVERSE NODE-PATH)) (CDR DPYLIST))
		(KEYNUM 0 (1+ KEYNUM))  (KEY)  (CC-FORM) )
	       ((NULL DPYLIST) T)
	       (SETQ KEY (LINK-KEY (CAR DPYLIST)))
	       (COND ((SETQ CC-FORM (ATC-GET KEY 'LT-FORMULA))
			(WRITE T* (POSPRINC KEYNUM  | |)
			       (DISPLAY CC-FORM CURRENTPOS) ) )
		     ((FIXP KEY) (SETQ *NOPOINT T)
				 (COND ((< CURRENTPOS 76.) (POSPRINC |  |)))
				 (POSPRINC KEYNUM |. | KEY)
				 (SETQ *NOPOINT NIL) )
		     (T (COND ((< CURRENTPOS 76.) (POSPRINC |  |)))
			(POSPRINC KEYNUM | | KEY) ) ) )) ) )

(DEFUN DISPLAY-NODE (NODE &aux (TALLY 1) *NOPOINT)
  (COND ((AND (NULL (LINK-A-LIST NODE))
	      (EQ '*TOP* (LINK-KEY NODE)) )
	   (WRITE T " - discrimination net currently empty -") )
	((#.(ISA . LEAF-NODE) NODE)
	   (WRITE T "Leaf-Node Formula:"
		  T  (DISPLAY (ATC-GET (LEAF-PLIST NODE) 'LT-FORMULA)) ) )
	(T (LET ((CURRENTPOS 1))
		(WRITE T (POSPRINC "Available New Keys:"))
		(MAPC #'(LAMBDA (A-PAIR)
			 (LET* ((KEY (CAR A-PAIR))
				(CC-FORM (ATC-GET KEY 'LT-FORMULA)) )
			       (COND (CC-FORM
				       (WRITE T* (POSPRINC TALLY | |)
					      (DISPLAY CC-FORM CURRENTPOS ) )
				       (SETF* TALLY (1+ -*-)) )
				     ((FIXP KEY) (SETQ *NOPOINT T)
						 (COND ((< CURRENTPOS 76.)
							  (POSPRINC |  |) ))
						 (POSPRINC TALLY |. | KEY)
						 (SETQ *NOPOINT NIL)
						 (SETF* TALLY (1+ -*-)) )
				     (T (COND ((< CURRENTPOS 76.) (POSPRINC |  |)))
					(POSPRINC TALLY | | KEY)
					(SETF* TALLY (1+ -*-)) ) ) ) )
		      (LINK-A-LIST NODE) ) )) ) )

;; EXTEND-CURRENT-KEYPATH uses the freevars CURRENTNODE and CURRENT-NODE-PATH.
(DEFUN EXTEND-CURRENT-KEYPATH (NEWKEYS &aux NEW-CURRENTNODE)
 (COND ((NULL (LINK-A-LIST CURRENTNODE))
	  (WRITE T " - can't extend keypath; null a-list!") )
       ((#.(ISA . LEAF-NODE) CURRENTNODE)
	  (WRITE T " - can't extend keypath; already at a leaf-node.") )
       (T (SETQ NEW-CURRENTNODE (TRAVERSE-LINKS CURRENTNODE NEWKEYS))
	  (COND ((NOT (EQ NEW-CURRENTNODE CURRENTNODE))
		  (SETQ CURRENTNODE NEW-CURRENTNODE)
		  (DISPLAY-KEYPATH CURRENT-NODE-PATH)
		  (DISPLAY-NODE CURRENTNODE) ) ) ) ) )

;; SHORTEN-CURRENT-NODEPATH accesses and sets
;;   the freevars CURRENTNODE and CURRENT-NODE-PATH.
(DEFUN SHORTEN-CURRENT-NODEPATH (PARAM)
 (*CATCH 'S-C-N
  (COND ((AND (FIXP PARAM) (> PARAM 0))
	  (COND ((< PARAM (LENGTH CURRENT-NODE-PATH))
		   (REPEAT PARAM (POP CURRENT-NODE-PATH)) )
		(T (WRITE T "SP-argument: " PARAM 
			    " is too large -- please try again ..." )
		   (*THROW 'S-C-N NIL) ) ) )
	((EQ '* PARAM)
	   (COND ((EQ '*TOP* (LINK-KEY (CAR CURRENT-NODE-PATH)))
		    (WRITE T " - already at root-node -- keypath unchanged.")
		    (*THROW 'S-C-N NIL) )
		 (T (POP CURRENT-NODE-PATH)) )
	   (DO ()
	       ((< 1 (LENGTH (LINK-A-LIST (CAR CURRENT-NODE-PATH)))))
	       (COND ((EQ '*TOP* (LINK-KEY (CAR CURRENT-NODE-PATH)))
		        (WRITE T "now at root-node, but no multiple keys found.")
			(RETURN T) ))
	       (POP CURRENT-NODE-PATH) ) )
	((EQ '** PARAM)
	   (COND ((EQ '*TOP* (LINK-KEY (CAR CURRENT-NODE-PATH)))
		    (WRITE T " - already at root-node -- keypath unchanged.")
		    (*THROW 'S-C-N NIL) )
		 (T (SETQ CURRENT-NODE-PATH (LAST CURRENT-NODE-PATH))) ) )
	(T (WRITE T "SP-argument: " PARAM 
		    " is unacceptable -- please try again ..." )
	   (*THROW 'S-C-N NIL) ) )
  (SETQ CURRENTNODE (CAR CURRENT-NODE-PATH))
  (DISPLAY-KEYPATH CURRENT-NODE-PATH)
  (DISPLAY-NODE CURRENTNODE) ) )

(DEFUN COUNT-LINKS&LEAVES (NODE)
  (DO ((LINK-COUNTER 0)
       (LEAF-COUNTER 0)
       (UNCOUNTED-A-LISTS (NCONS (NCONS NODE)) (CDR UNCOUNTED-A-LISTS)) )
      ((NULL UNCOUNTED-A-LISTS) (WRITE T "Number of Link-nodes: " LINK-COUNTER
				       T "Number of Leaf-nodes: " LEAF-COUNTER ))
      (MAPC #'(LAMBDA (NODE-TO-COUNT)
		(COND ((#.(ISA . LEAF-NODE) NODE-TO-COUNT)
		         (SETF* LEAF-COUNTER (1+ -*-)))
		      (T (ENDADD (LINK-A-LIST NODE-TO-COUNT) UNCOUNTED-A-LISTS)
			 (SETF* LINK-COUNTER (1+ -*-)) ) ) )
	    (CAR UNCOUNTED-A-LISTS) ) ) )

(DEFUN PRINT-PROPERTIES (COMMAND &aux PROPNAME KEYTYPE NUM∨NIL (-EM:LINEL- 65.))
 (*CATCH 'P-P
  (COND ((CDR COMMAND)
	   (CASEQ (CAR COMMAND)
	     (PPV (SETQ PROPNAME (NTH 1 COMMAND)
			KEYTYPE (NTH 2 COMMAND)
			NUM∨NIL (NTH 3 COMMAND) ))
	     (PPL (SETQ KEYTYPE (NTH 1 COMMAND)
			NUM∨NIL (NTH 2 COMMAND) )) ) )
	(T (COND ((AND (EQ (CAR COMMAND) 'PPL)
		       (NOT (#.(ISA . LEAF-NODE) CURRENTNODE)))
		    (WRITE T
		     " - current node is not a leaf -- please try again..." )
		    (*THROW 'P-P NIL) )
		 ((EQ (CAR COMMAND) 'PPV)
		    (WRITE T " - missing property name -- please try again..." )
		    (*THROW 'P-P NIL) ) ) ))
  (COND ((AND (EQ KEYTYPE 'C) (NULL (CDR CURRENT-NODE-PATH)))
	   (WRITE T " - keypath is currently empty -- please try again..")
	   (*THROW 'P-P NIL) )
	((AND (EQ KEYTYPE 'A) (#.(ISA . LEAF-NODE) CURRENTNODE))
	   (WRITE T
	      " - no keys are available at a leaf-node -- please try again..." )
	   (*THROW 'P-P NIL) ))
  (COND ((AND NUM∨NIL
	      (NOT (AND (FIXP NUM∨NIL)
			(> NUM∨NIL (CASEQ KEYTYPE (C -1) (A 0)
				    (T (WRITE T
				  " - improper keytype -- please try again..." )
				       (*THROW 'P-P NIL) ) ))
			(< NUM∨NIL (CASEQ KEYTYPE
				    (C (1- (LENGTH CURRENT-NODE-PATH)))
				    (A (1+ (LENGTH (LINK-A-LIST CURRENTNODE)))) )) )) )
	   (WRITE T " - bad keynumber -- please try again...")
	   (*THROW 'P-P NIL) ))
  (LET ((PRINT-NODE (CASEQ KEYTYPE
		      (C (LINK-KEY (NTH (- (LENGTH CURRENT-NODE-PATH) 2 NUM∨NIL)
					CURRENT-NODE-PATH )))
		      (A (LINK-KEY (NTH (1- NUM∨NIL) (LINK-A-LIST CURRENTNODE))))
		      (NIL (LEAF-PLIST CURRENTNODE)) )))
       (CASEQ (CAR COMMAND)
	 (PPV (WRITE T (ATC-GET PRINT-NODE PROPNAME)))
	 (PPL (WRITE T (ATC-PLIST PRINT-NODE))) ) ) ) )

(DEFSTRUCT (HELP-TABLE-ENTRY (TYPE LIST))
	  COMMAND-KEY COMMAND-NAME ARG-SUMMARY 2ND-ARG-SUMMARY HELP-TEXT-LINE1 )

(DEFMACRO HELP-TEXT-LINES (HELP-TABLE-ENTRY)
  `(NTHCDR 4. ,HELP-TABLE-ENTRY) )

;(declare (gc))

; uses freely the variables TABVAL1 and TABVAL2
(DEFUN DISPLAY-HELP-TABLE-ENTRY (ENTRY &optional (TEXT-FLAG 'NO-TEXT))
  (LET ((1ST-TABVAL (CASEQ (CAR ENTRY)
		      ((|Q,QUIT| |??,HH,HELP|) 13.)
		      (T TABVAL1) ))
	(2ND-TABVAL (COND ((AND (MEMQ (CAR ENTRY) '(|Q,QUIT| |??,HH,HELP|))
				(< TABVAL2 38.) )
			     38. )
			  (T TABVAL2) )) )
       (SETQ CURRENTPOS 1)
       (WRITE T (POSPRINC (COMMAND-KEY ENTRY))
		(TAB 1ST-TABVAL)
		(POSPRINC (COMMAND-NAME ENTRY))
		(TAB 2ND-TABVAL)
		| - |
		(POSPRINC (ARG-SUMMARY ENTRY)) )
       (COND ((2ND-ARG-SUMMARY ENTRY)
		(TAB (+ 3. 2ND-TABVAL))
		(POSPRINC (2ND-ARG-SUMMARY ENTRY)) ))
       (COND ((AND (EQ 'TEXT TEXT-FLAG)
		   (HELP-TEXT-LINES ENTRY) )
	        (MAPC #'(LAMBDA (TEXT-LINE)
			  (SETQ CURRENTPOS 1)
			  (WRITE T (TAB TABVAL1) TEXT-LINE) )
		      (HELP-TEXT-LINES ENTRY) ) )) ) )

(DEFUN DISPLAY-TRANSFER-COMMANDS (DETAIL-KEY EXCEPTION-KEY
					&aux (TABVAL1 6.) (TABVAL2 39.) )
  (COND ((NULL DETAIL-KEY)
	   (WRITE T '|Transfer-commands:  |) )
	((EQ '* DETAIL-KEY)
	   (WRITE T '|Transfer command summaries:|) )
	((EQ '** DETAIL-KEY)
	   (WRITE T '|Transfer command information:|) ) )
  (DO ((N (LENGTH IPC-HELP-TABLE) (1- N))
       (TABLE-TAIL IPC-HELP-TABLE (CDR TABLE-TAIL)) )
      ((< N 5.) (TERPRI))
      (LET ((ENTRY (CAR TABLE-TAIL)))
	   (COND ((NOT (EQ EXCEPTION-KEY (CAR ENTRY)))
		    (COND ((NULL DETAIL-KEY)
			     (WRITE (CAR ENTRY) |  |) )
			  ((EQ '* DETAIL-KEY)
			     (DISPLAY-HELP-TABLE-ENTRY ENTRY 'NO-TEXT) )
			  ((EQ '** DETAIL-KEY)
			     (DISPLAY-HELP-TABLE-ENTRY ENTRY 'TEXT) ) )) ) ) ) )

(DEFUN XPDN-SHORT-HELP (CMD-TAIL)
 (COND ((NULL CMD-TAIL)
	  (DISPLAY-XPDN-COMMANDS) )
       ((MEMQ (CAR CMD-TAIL) '(← TRAN TRANS))
	  (DISPLAY-TRANSFER-COMMANDS NIL 'XDN) )
       ((EQ '* (CAR CMD-TAIL))
	  (DISPLAY-XPDN-COMMANDS)
	  (DISPLAY-TRANSFER-COMMANDS NIL 'XDN) )
       (T (XPDN-HELP (CONS 'SHORT-HELP CMD-TAIL))) ) )

(DEFUN DISPLAY-XPDN-COMMANDS ()
 (WRITE T
; line too wide to indent fully
'|Task-commands:  CP  CN  CPN  XP  SP  CLL  PPV  PPL  ?,H  ??,HH,HELP  Q,QUIT| ) )

;(declare (gc))

(DEFUN XPDN-HELP (CMD-TAIL
		      &aux (CURRENTPOS 1) (TABVAL1 5.) (TABVAL2 33.) TEXT-FLAG )
  (COND ((OR (NULL CMD-TAIL) (EQ '* (CAR CMD-TAIL)))
	   (SETQ CURRENTPOS 1)
	   (WRITE T (POSPRINC '|Command Summary - | 'EXPLORE-DNET |.|)
		  (TAB 34.) '|Syntax -- <cmd> or (<cmd> {<arg>} ... {*{*}})| )
	   (SETQ TEXT-FLAG (COND (CMD-TAIL 'TEXT) (T 'NO-TEXT)))
	   (MAPC #'(LAMBDA (ENTRY)
		     (COND ((EQ 'DD TERMINAL-TYPE) (WRITE T T)))
		     (DISPLAY-HELP-TABLE-ENTRY ENTRY TEXT-FLAG) )
		 XPDN-HELP-TABLE ) )
	((MEMQ (CAR CMD-TAIL) '(← TRAN TRANS))
	   (DISPLAY-TRANSFER-COMMANDS
			(COND ((EQ '* (CADR CMD-TAIL)) '**) (T '*))
			'XDN ) )
	(T (SETQ CURRENTPOS 1)
	   (COND ((EQ 'SHORT-HELP (CAR CMD-TAIL))
		    (SETQ TEXT-FLAG 'NO-TEXT   CMD-TAIL (CDR CMD-TAIL)) )
		 ((EQ 'VERBOSE IPC:HELP-VERBOSITY)
		    (SETQ TEXT-FLAG 'TEXT)
		    (WRITE T* (POSPRINC "Some command info - EXPLORE-DNET.")
			   (TAB 34.)
			   '|Syntax -- <cmd> or (<cmd> {<arg>} ... {*{*}})| T T ) )
		 (T (SETQ TEXT-FLAG 'TEXT)) )
	   (MAPC #'(LAMBDA (CMD)
		     (LET* ((CMD-KEY (CASEQ CMD
				       ((Q QUIT) '|Q,QUIT|)
				       ((? H) '|?,H|)
				       ((?? HH HELP) '|??,HH,HELP|)
				       (T CMD) ))
			    (ENTRY (ASSQ CMD-KEY XPDN-HELP-TABLE)) )
			   (COND (ENTRY
				  (DISPLAY-HELP-TABLE-ENTRY ENTRY TEXT-FLAG) )) ) )
		 CMD-TAIL )) ) )

(SETQ XPDN-HELP-TABLE
'((CP "display Current keyPath" |no arguments|)
  (CN "display Current Node" |no arguments|)
  (CPN "display Current Path & Node" |no arguments|)
  (XP "eXtend current keyPath" "argument(s): a list of key-indicators"
			       "key-indicator: a number, a key, or *"
  "Extends the current keypath into the dnet, using the keys specified."
  "A key-indicator n specifies the nth key available at a given"
  "choice-point.  A key-indicator * requests an extension of the"
  "keypath as far as possible using uniquely available keys"
  "(i.e., extension as far as the next choice-point)."
  "Argument-list defaults to (1)." )
  (SP "Shorten current keyPath" "argument: a number, *, or **" NIL
  "With argument n, removes n items from the current keypath."
  "With argument *, shortens the keypath back to the last choice-point."
  "With argument **, shortens the keypath back to the beginning."
  "Argument defaults to 1." )
  (CLL "Count Links & Leaves" |no arguments| NIL
   "Counts and reports the number of link-nodes and leaf-nodes in the"
   "current discrimination net." )
  (PPV "Print Property Value" "argument list: (<propname> <keytype> <num>),"
			      "or (<propname>).  <keytype>: C or A"
   "With argument <propname>, displays the value of the property-indicator"
   "<propname> for the current leaf-node.  With arguments <propname>, <keytype>,"
   "and <num>, displays for the <num>th key of type <keytype> the value of"
   "the property-indicator <propname>.  Keys on the Current-keypath"
   "are of type C, while currently Available keys are of type A." )
  (PPL "Print Property List" "arg list: [as for PPV, but sans <propname>]" NIL
   "Like PPV, except that ALL values on the property-list of the"
   "current leaf-node or specified key are displayed." )
  (|?,H| "mini-Help" |arguments: none, ← , *, or cmds| NIL
   |With no arguments, lists all task-commands.|
   |With argument ← , lists all transfer-commands.|
   |With argument *, lists all task- and transfer-commands.|
   |With command-args, prints help-summaries for the task-commands specified.| )
  (|??,HH,HELP| |Help: command information| |arguments: none, cmds, ← , or *|
   NIL |With no arguments, prints help-summaries for all task-commands.|
   |With command-args, prints full help-texts for the task-commands specified.|
   |With argument *, prints full help-texts for all task-commands.|
   |With argument ← , prints help-summaries for all transfer-commands.|
   |With arguments ← *, prints full help-texts for all transfer-commands.| )
  (|Q,QUIT| |Quit| |arguments: none, or *| NIL
   |With no arguments, returns to IPC; with argument *, exits from IPC.| ) ) )
;		Processes for Logically Evaluating an LT-form

; this macro returns non-NIL iff LT-TERM is demonstrably of the sort LT-SORT,
;  reasoning only from the sort-hierarchy.
(DEFMACRO SORT-MEMBER (LT-TERM LT-SORTATOM)
 `(LET ((LT-TERMSORT (TERMSORT ,LT-TERM)))
       (OR (EQ ,LT-SORTATOM LT-TERMSORT)
	   (SUPERSORT* ,LT-SORTATOM LT-TERMSORT) ) ) )

; this macro returns non-NIL iff LT-TERM is demonstrably NOT of the sort LT-SORT,
;  reasoning only from the sort-hierarchy and sortfamily information.
(DEFMACRO SORT-EXCLUSIVE (LT-TERM LT-SORTATOM)
 `(PROG (LT-TERMSORT CURRENT-FAMCAND SORTFAMILY) 
	(SETQ LT-TERMSORT (TERMSORT ,LT-TERM))
	(COND ((OR (EQ ,LT-SORTATOM LT-TERMSORT)
		   (SUPERSORT* ,LT-SORTATOM LT-TERMSORT) )
	         (RETURN NIL) ))
	(SETQ CURRENT-FAMCAND LT-TERMSORT)
      A (COND ((EQ CURRENT-FAMCAND 'THING) (RETURN NIL)))
	(SETQ SORTFAMILY (GET CURRENT-FAMCAND 'SORTFAMILY))
	(COND ((AND SORTFAMILY
		    (SETQ SORTFAMILY
			  (SOME SORTFAMILY
				#'(LAMBDA (SIBLING)
				    (AND (NOT (EQ SIBLING CURRENT-FAMCAND))
					 (OR (EQ SIBLING ,LT-SORTATOM)
					     (SUPERSORT* SIBLING ,LT-SORTATOM) ) ) ) ) ) )
	         (RETURN SORTFAMILY) ))
	(SETQ CURRENT-FAMCAND
	      (OR (GET CURRENT-FAMCAND 'SUPERSORT)
		  (WRITE T "; No supersort for " CURRENT-FAMCAND "."
			 (BREAK SORT-EXCLUSIVE) ) ))
	(GO A) ) )

(DEFMACRO ES-FILTER (EPISTEMIC-STATUS)
 `(CASEQ ,EPISTEMIC-STATUS
     ((CERTAINLY-TRUE) T)
     ((CERTAINLY-FALSE CURRENTLY-UNKNOWN) NIL)
     (T (BREAK |; ES-FILTER: Unrecognized EPISTEMIC-STATUS.|)) ) )

(DEFMACRO WEAKEST-STATUS (STATUS-LIST)
 `(LET ((TAIL (COND ((MEMQ 'CERTAINLY-FALSE ,STATUS-LIST))
		    ((MEMQ 'CURRENTLY-UNKNOWN ,STATUS-LIST))
		    ((MEMQ 'CERTAINLY-TRUE ,STATUS-LIST))
		    (T (BREAK |; WEAKEST-STATUS -- unrecognized epistemic status.|)) )))
       (CAR TAIL) ) )

(DEFUN ISA-SIMPLE-SORT-PROPO (LT-FORM)
 (AND (CONSP LT-FORM)
      (SYMBOLP (CAR LT-FORM))
      (ISA-SUPERSORT-OF 'SORT (GET (CAR LT-FORM) 'CATEGORY)) ) )

(DEFUN SORTALLY-CERTAIN? (LT-FORM)
  (COND ((SORT-MEMBER (ARGUMENT (CAR (ROLELINKS LT-FORM)))
	       (PFC-CONCEPT LT-FORM) )
	   'SORTALLY-CERTAIN )) )

(DEFUN SORTALLY-NEG-CERTAIN? (LT-FORM)
  (COND ((SORT-EXCLUSIVE (ARGUMENT (CAR (ROLELINKS LT-FORM)))
		  (PFC-CONCEPT LT-FORM) )
	   'SORTALLY-NEG-CERTAIN )) )

(DEFMACRO LT-GROSSEVAL (LT-FORM)
 `(ES-FILTER (LT-EVAL LT-FORM)) )

; this fn LOGICALLY evaluates an lt-form, and returns its epistemic status;
; it is in principle an open-ended, specialized, knowledge-based problem-solver,
; and will be developed greatly over time.
(DEFUN LT-EVAL (LT-FORM)
  (CASEQ (LT-TYPE LT-FORM)
    (ATOMICPROPO
      (LET* ((PRED (PFC-CONCEPT LT-FORM))
	     (EVALD-ROLINKS (MAPCAR #'(LAMBDA (ROLINK)
				       (MAKE-ROLELINK
					 ROLEMARK (ROLEMARK ROLINK)
					 ARGUMENT (LT-EVAL (ARGUMENT ROLINK)) ) )
				    (ROLELINKS LT-FORM) )) )
	    (COND ((AND (= 1 (LENGTH EVALD-ROLINKS))
			(#.(ISA-OF:LT . SORT) PRED) )
		     (COND ((SORT-MEMBER (ARGUMENT (CAR EVALD-ROLINKS)) PRED)
			      'CERTAINLY-TRUE )
			   ((SORT-EXCLUSIVE (ARGUMENT (CAR EVALD-ROLINKS)) PRED)
			      'CERTAINLY-FALSE ) ) )
		  (T 'CURRENTLY-UNKNOWN) ) ) )
    (SIMPLEFORM LT-FORM)
    (F-TERM LT-FORM)  ;; this should involve a search for equalities, at least.
    (NEGPROPO
      (LET ((EVALD-SCOPE (LT-EVAL (CAR (ROLELINKS LT-FORM)))))
	   (CASEQ EVALD-SCOPE
	      (CERTAINLY-TRUE 'CERTAINLY-FALSE)
	      (CERTAINLY-FALSE 'CERTAINLY-TRUE)
	      (CURRENTLY-UNKNOWN)
	      (T (BREAK |; LT-EVAL:Negpropo -- unrecognized epistemic status.|)) ) ) )
    (CONJ-PROPO
      (LET ((EVALD-JUNCTS (MAPCAR #'(LAMBDA (ROLINK)
				      (LT-EVAL (ARGUMENT ROLINK)) )
				  (ROLELINKS LT-FORM) )))
	   (WEAKEST-STATUS EVALD-JUNCTS) ) )
    ((QUANTPROPO DISJ-PROPO ⊃-PROPO ≡-PROPO)
       'CURRENTLY-UNKNOWN )
    (↑-TERM 'CURRENTLY-UNKNOWN)
    (T (BREAK |LT-EVAL: LT-FORM is of improper type for lt-evaluation!|)) ) )