;;; -*- Mode:LISP; Package:USER; Readtable:CL; Base:10 -*-

;;;****************************************************************
;;; Doug, I move this here from *buffer-1*.  Peter Cerrato 7/14 8:58am
;;;****************************************************************
(defun c-proc-invert ()
  (let ((reset nil)
        (run nil)
        (halt nil)
        (step-i nil)
	(cm nil)
	(c2m nil))
    (not (and (or (and 'cm 'c2m) (and (not 'cm) (not 'c2m)))
	      (or 'reset
		  (and 'run (not 'halt))
		  (and (not 'run) 'step-i))))))
;;;****************************************************************

(defun invert (expr)
  (resimplify (sort-tree (expand expr))))

(defun expand (expr)
  (if (atom expr)
      expr
    (case (car expr)
      (and (let ((args (mapcar #'expand-remove-or (cdr expr))))
	     `(or ,@(reverse (apply #'expand-and args)))))
      (or (cons 'or (mapcar #'expand (cdr expr))))
      (not (cond ((not (null (cddr expr)))
		  (error "multi-arg NOT clause: ~s" expr))
		 ((and (consp (cadr expr))
		       (eq (caadr expr) 'not))
		  (expand (cadadr expr)))
		 ((and (consp (cadr expr))
		       (eq (caadr expr) 'and))
		  `(or ,@(mapcar #'(lambda (x) `(not ,(expand x))) (cdadr expr))))
		 ((and (consp (cadr expr))
		       (eq (caadr expr) 'or))
		  `(and ,@(mapcar #'(lambda (x) `(not ,(expand x))) (cdadr expr))))
		 (t `(or (not ,(expand (cadr expr)))))))
      (t (error "bad form ~s" expr)))))

(defun expand-and (&rest terms)
  (if (null (cdr terms))
      (car terms)
    (let ((expanded-others (apply #'expand-and (cdr terms)))
	  res)
      (dolist (x (car terms))
	(dolist (y expanded-others)
	  (cond ((and (consp x) (eq (car x) 'and))
		 (if (and (consp y) (eq (car y) 'and))
		     (push `(and ,(append (cdr x) (cdr y))) res)
		   `(and ,y ,@(cdr x))))
		((and (consp y) (eq (car y) 'and))
		 (push `(and ,x ,@(cdr y)) res))
		(t (push `(and ,x ,y) res)))))
      res)))

(defun expand-remove-or (expr)
  (if (and (consp expr) (eq (car expr) 'or))
      (cdr expr)
    (list (expand expr))))

(defun resimplify (expr)
  (if (atom expr) expr
    (let ((args (mapcar #'resimplify (cdr expr))))
      (do ((arg args (cdr arg))
	   new)
	  ((null (cdr arg))
	   (setq args (nreverse (cons (car arg) new))))
	(unless (equal (car arg) (cadr arg))
	  (push (car arg) new)))
      (case (car expr)
	(or (cond ((member 't args) 't)
		  ((null (cdr args))
		   (car args))
		  (t (do ((x args (cdr x)))
			 ((null (cdr x)))
		       (cond ((and (consp (car x))
				   (eq (caar x) 'not)
				   (equal (cadar x) (cadr x)))
			      (return-from resimplify 't))
			     ((and (consp (cadr x))
				   (eq (caadr x) 'not)
				   (equal (cadadr x) (car x)))
			      (return-from resimplify 't))))
		     `(or ,@(delete 'nil args)))))
	(and (cond ((member 'nil args) 'nil)
		   ((null (cdr args))
		    (car args))
		   (t (do ((x args (cdr x)))
			  ((null (cdr x)))
			(cond ((and (consp (car x))
				    (eq (caar x) 'not)
				    (equal (cadar x) (cadr x)))
			       (return-from resimplify 'nil))
			      ((and (consp (cadr x))
				    (eq (caadr x) 'not)
				    (equal (cadadr x) (car x)))
			       (return-from resimplify 'nil))))
		      `(and ,@(delete 't args)))))
	(t (cons (car expr) args))))))

(defun tree-sorted-p (x y)
  (/= +1 (tree-sorted x y)))

(defun tree-sorted (x y)
  ;; returns -1, 0, +1
  (cond ((and (atom x) (atom y))
	 (cond ((eq x y) 0)
	       ((alphalessp x y) -1)
	       (t +1)))
	((and (consp x) (eq (car x) 'not))
	 (tree-sorted (cadr x) y))
	((and (consp y) (eq (car y) 'not))
	 (tree-sorted x (cadr y)))
	((atom x) -1)
	((atom y) +1)
	(t (do ((sx (cdr x) (cdr sx))
		(sy (cdr y) (cdr sy))
		ret)
	       (nil)
	     (when (and (null sx) (null sy)) (return 0))
	     (when (null sx) (return -1))
	     (when (null sy) (return +1))
	     (setq ret (tree-sorted (car sx) (car sy)))
	     (unless (= ret 0) (return ret))))))

(defun sort-tree (tree)
  (if (atom tree) tree
    (let ((args (mapcar #'sort-tree (cdr tree))))
      (case (car tree)
	(not `(not ,@args))
	(and `(and ,@(sort args #'tree-sorted-p)))
	(or  `(or  ,@(sort args #'tree-sorted-p)))
	(t (error "bogus tree during sort: ~s" tree))))))