;;; constraint net = ((x1 ... xn) p1 ... pm)
;;; theta expression = (theta (x1 ... xn) (y1 ... yk) . constraint net)
;;; equality = (= foo bar)

(declare (mapex t))

(declare (special *gentempnum*))

(setq *gentempnum* 0)

(defun gentemp (name)
       (implode (append (exploden name)
			'(55)
			(exploden (setq *gentempnum*
					(+ *gentempnum* 1))))))

(defun massage (cnet)
       (massage-cnet (alpha-cnet cnet nil)))

(defun alpha-cnet (cnet alist)
       (alpha-cset (cdr cnet)
		   (nconc (mapcar '(lambda (x) ((lambda (temp)
							(cons x temp))
						(gentemp x)))
				  (car cnet))
			  alist)))

(defun alpha-cset (cset alist)
       (mapcar '(lambda (x) (alpha-constraint x alist))
	       cset))

(defun alpha-constraint (con alist)			;= and ? better not be vars!
       (mapcar '(lambda (x) (alpha-frob x con alist)) con))

(defun alpha-frob (frob con alist)
       (cond ((atom frob)
	      ((lambda (slot)
		       (cond (slot
			      (putprop (cdr slot)
				       (cons con (get (cdr slot) 'references))
				       'references)
			      (cdr slot))
			     (t frob)))
	       (assq frob alist)))
	     ((eq (car frob) 'theta)
	      ((lambda (foo)
		       ((lambda (bar)
				(cons 'theta
				      (cons foo
					    (cons (mapcar '(lambda (x) (cdr (assq x bar)))
							  (caddr frob))
						  (alpha-cnet (cdddr frob)
							      (append bar alist))))))
			(mapcar 'cons (cadr frob) foo)))
	       (mapcar 'gentemp (cadr frob))))
	     ((eq (car frob) 'zeta)
	      (alpha-frob (cons 'theta (cons (cadr frob) (cons nil (cddr frob))))))
	     (t (error '|Disgusting Frob| frob 'fail-act))))

(declare (special *change*))

(defun massage-cnet (cnet)