;;; -*- Syntax:Common-Lisp; Mode: LISP; Package: (TMS Lisp 1000.); Base: 10. -*-

(in-package 'tms)

"(c) Copyright 1986, 1987, 1988 Xerox Corporation.  All rights reserved.  Subject to
the following conditions, permission is granted to use and copy this
software and to prepare derivative works:  Such use, copying or
preparation of derivative works must be for non-commercial research or
educational purposes; each copy or derivative work must include this
copyright notice in full; a copy of each completed derivative work must
be returned to:  DEKLEER@XEROX.COM (Arpanet) or Johan de Kleer,
Xerox PARC, 3333 Coyote Hill Road, Palo Alto, CA 94304.  This software
is made available AS IS, and Xerox Corporation makes no warranty about
the software or its performance."

;;;; Note convention is that you will never see (n) 0 or 0 (n) or (n) (m)

;;;***** break coded is overused.

;;;****** Doesn't santize********

;;; The deal is this can't clobber anything of vector.
;;;;********* THIS IS BUGGY????????? it doesn't return anythjing
(defun remove-assumption-blots (vector assumption &aux word offset)
  (setq vector (fcopylist vector)
	offset (assumption-offset assumption))
  ;; Find the word.**** Doesn't exploite (2)(3) can't happen.
  (do ((tail vector (cdr tail))
       (preprevious nil previous)		; Need to kill trailing 0s.
       (previous nil tail))
      ((null tail))
    (cond ((= offset 0)
	   (cond ((listp (car tail)) (return nil))
		 (t (setq word (logandc2 (car tail) (assumption-bits assumption)))
		    (cond ((not (zerop word))
			   (rplaca tail word) (return nil))
			  ;; If we are end of the vector, we have to get rid of trailing 0s.
			  ((null (cdr tail))
			   (cond ((null previous) (return nil))
				 ((or (listp (car previous)) (zerop (car previous)))
				  (cond ((null preprevious) (return nil))
					(t (rplacd preprevious nil) (return nil))))))
			  ;; Is the previous 0?
			  (t (cond ((and previous (listp (car previous)))
				    (cond ((and (cdr tail) (zerop (cadr tail)))
					   (rplaca previous (list (+ (caar previous) 2)))
					   (rplacd previous (cddr tail))
					   (return nil))
					  ((and (cdr tail) (listp (cadr tail)))
					   (rplaca previous
						   (list (+ 1 (caar previous) (caadr tail))))
					   (rplacd previous (cddr tail))
					   (return nil))
					  (t (rplaca previous (list (+ 1 (caar previous))))
					     (rplacd previous (cdr tail))
					     (return nil))))
				   ((and previous (zerop (car previous)))
				    (cond ((and (cdr tail) (zerop (cadr tail)))
					   (rplaca previous (list 3))
					   (rplacd previous (cddr tail))
					   (return nil))
					  ((and (cdr tail) (listp (cadr tail)))
					   (rplaca previous (list (+ 2 (caadr tail))))
					   (rplacd previous (cddr tail))
					   (return nil))
					  (t (rplaca previous (list 2))
					     (rplacd previous (cdr tail))
					     (return nil))))
				   
				   (t (cond ((and (cdr tail) (listp (cadr tail)))
					     (rplaca tail (list (+ 1 (caadr tail))))
					     (rplacd tail (cddr tail))
					     (return nil))
					    ((and (cdr tail) (zerop (cadr tail)))
					     (rplaca tail (list 2))
					     (rplacd tail (cddr tail))
					     (return nil))
					    (t (rplaca tail 0)
					       (return nil))))))))))
	  ((not (listp (car tail))) (decf offset))
	  (t (setq offset (- offset (caar tail)))
	     (if (< offset 0) (return nil))))))

;;; Usually assumptions are sorted.****
(defun make-env-vector-blots (assumptions &optional max &aux vector blotsize)
  ;;; Max is irrelevant here.
  max
  (dolist (assumption assumptions)
    (do ((offset (assumption-offset assumption))
	 (v vector (cdr v))
	 (previous nil v))
	((null v)
	 (cond (previous
		(cond ((= offset 0) (rplacd previous
					    (cons (assumption-bits assumption) nil)))
		      ((= offset 1) (rplacd previous
					    (cons 0 (cons (assumption-bits assumption) nil))))
		      ((rplacd previous
			       (cons (list offset) (cons (assumption-bits assumption) nil))))))
	       (t (cond ((= offset 0) (setq vector
					    (cons (assumption-bits assumption) nil)))
		      ((= offset 1) (setq vector
					  (cons 0 (cons (assumption-bits assumption) nil))))
		      (t (setq vector
			       (cons (list offset)
				     (cons (assumption-bits assumption) nil)))))))
	 )
      (cond ((= offset 0)
	     (cond ((not (listp (car v)))
		    (rplaca v (logior (car v) (assumption-bits assumption))))
		   (t (if previous
			  (rplacd previous (cons (assumption-bits assumption) v))
			  (setq vector (cons (assumption-bits assumption) v)))
		      (cond ((= (caar v) 2) (rplaca v 0))
			    (t (rplaca (car v) (1- (caar v)))))))
	     (return nil))
	    ((not (listp (car v))) (decf offset))
	    ((>= offset (caar v))
	     (setq offset (- offset (caar v))))
	    ;; Last of run, dual of offset=0.
	    ((= (1- offset) (caar v))
	     (rplacd v (cons (assumption-bits assumption) (cdr v)))
	     (cond ((= (caar v) 2) (rplaca v 0))
		   (t (rplaca (car v) (1- (caar v)))))
	     (return nil))
	    (t (setq blotsize (caar v))
	       (cond ((= offset 1) (rplaca v 0))
		     (t (rplaca (car v) offset)))
	       (setq blotsize (- blotsize 1 offset))
	       (rplacd v
		       (cons (assumption-bits assumption)
			     (cond ((= blotsize 0) (cdr v))
				   ((= blotsize 1) (cons 0 (cdr v)))
				   (t (cons (list blotsize) (cdr v))))))
	       (return )))))

  vector)

(defun vector-intersection-blots? (v1 v2 &aux i1 i2 c1 c2)
  (prog nil
	
     START
	(unless v1 (return nil))
	(unless v2 (return nil))

	(setq i1 (car v1) i2 (car v2) v1 (cdr v1) v2 (cdr v2))

	(when (listp i1)
	  (setq c1 (car i1))
	  (go SKIP2))
	
	(when (listp i2)
	  (setq c2 (car i2))
	  (go skip1))
	   
     TEST

	   (unless (zerop (logand i1 i2))
	     (return T))
	   (go start)

	   ;; Skip c1 elements along in v2.

     SKIP2
	   (cond ((listp i2)
		  (setq c2 (car i2))
		  (cond ((= c2 c1) (setq i1 (car v1) i2 (car v2) v1 (cdr v1) v2 (cdr v2))
			 (go TEST))
			((> c1 c2)
			 (setq c1 (- c1 c2 1) v2 (cdr v2))
			 (if (= c1 0) (go START))	;**could optimize.
			 (or v2 (return nil))
			 (setq i2 (car v2) v2 (cdr v2))
			 (go SKIP2))
			(t (setq c2 (- c2 c1 1) v1 (cdr v1))
			 (if (= c2 0) (go START))
			 (or v1 (return nil))
			 (setq i1 (car v1) v1 (cdr v1) )
			 (go SKIP1))))
		 ((= c1 1) (go START))	;** canbe better.
		 ((null v2) (return nil))
		 (t (decf c1) (setq i2 (car v2) v2 (cdr v2)) (go skip2)))

;;;***** by symmetry could fold this into one.

     SKIP1
	   (cond ((listp i1)
		  (setq c1 (car i1))
		  (cond ((= c2 c1) (setq i2 (car v2) i1 (car v1) v1 (cdr v1) v2 (cdr v2))
			 (go TEST))
			((> c2 c1) (setq c2 (- c2 c1 1) v1 (cdr v1))
			 (if (= c2 0) (go START))
			 (or v1 (return nil))
			 (setq i1 (car v1) v1 (cdr v1))
			 (go SKIP1))
			(t (setq c1 (- c1 c2 1) v2 (cdr v2))
			 (if (= c1 0) (go START))
			 (or v2 (return nil))
			 (setq i2 (car v2) v2 (cdr v2) )
			 (go SKIP2))))
		 ((= c2 1) (go START));***
		 ((null v1) (return nil))
		 (t (decf c2) (setq i1 (car v1) v1 (cdr v1)) (go skip1)))))

(defun vector-cons3-blots () (error "Unimplemented"))

;;; This returns fresh list structure always.
(defun vector-cons4-blots (assumption vector &aux blotsize)
  ;;******* really remporary:
  (setq vector (fcopylist vector))

  (do ((offset (assumption-offset assumption))
       (v vector (cdr v))
       (previous nil v))
      ((null v)
       (cond (previous
	      (cond ((= offset 0) (rplacd previous
					  (cons (assumption-bits assumption) nil)))
		    ((= offset 1) (rplacd previous
					  (cons 0 (cons (assumption-bits assumption) nil))))
		    ((rplacd previous
			     (cons (list offset) (cons (assumption-bits assumption) nil))))))
	     (t (cond ((= offset 0) (setq vector
					  (cons (assumption-bits assumption) nil)))
		      ((= offset 1) (setq vector
					  (cons 0 (cons (assumption-bits assumption) nil))))
		      (t (setq vector
			       (cons (list offset)
				     (cons (assumption-bits assumption) nil))))))))
    (cond ((= offset 0)
	   (cond ((not (listp (car v)))
		  (rplaca v (logior (car v) (assumption-bits assumption))))
		 (t (if previous
			(rplacd previous (cons (assumption-bits assumption) v))
			(setq vector (cons (assumption-bits assumption) v)))
		    (cond ((= (caar v) 2) (rplaca v 0))
			  (t (rplaca v (list (1- (caar v))))))))
	   (return nil))
	  ((not (listp (car v))) (decf offset))
	  ((>= offset (caar v))
	   (setq offset (- offset (caar v))))
	  ;; Last of run, dual of offset=0.
	  ((= (1- offset) (caar v))
	   (rplacd v (cons (assumption-bits assumption) (cdr v)))
	   (cond ((= (caar v) 2) (rplaca v 0))
		 (t (rplaca v (list (1- (caar v))))))
	   (return nil))
	  (t (setq blotsize (caar v))
	     (cond ((= offset 1) (rplaca v 0))
		   (t (rplaca v (list offset))))
	     (setq blotsize (- blotsize 1 offset))
	     (rplacd v
		     (cons (assumption-bits assumption)
			   (cond ((= blotsize 0) (cdr v))
				 ((= blotsize 1) (cons 0 (cdr v)))
				 (t (cons (list blotsize) (cdr v))))))
	     (return ))))
  (fcopylist vector)
  )

;;; Must return fresh list structure.  Is it worth cdr-coding this??*******

;;; If the vectors get long, stepping with cddddr might be much more efficient.
(defun vector-member-blots (a v &aux word)
  (when v
    (prog ((i (assumption-offset a)))
       LOOP
	  (setq word (car v))
	  (cond ((listp word)
		 (if (= i 0) (return nil))
		 (setq i (- i (car word)))
		 (if (< i 0) (return-from VECTOR-MEMBER-BLOTS nil))
		 (setq v (cdr v)) (go LOOP))
		((= i 0) (return (not= 0 (logand (assumption-bits a) word))))
		((setq v (cdr v)) (decf i) (go LOOP))
		(t (return-from VECTOR-MEMBER-BLOTS nil))))))

;;;**** make this check-all-vectors 

(defun check-env-array-blots (&aux vector)
  (dotimes (i (array-length *environments*))
    (dolist (e (aref *environments* i))
      (unless (env-contradictory e)
	(setq vector (make-env-vector (env-assumptions e)))
	(unless (vector-equal vector (env-vector e))
	  (error "Bad env vector")))))
  (walk-contradictions 
    #'(lambda (env)
	#+Symbolics
	(declare (sys:downward-function))
	(setq vector (make-env-vector (env-assumptions env)))
	(unless (vector-equal vector (env-vector env))
	  (error "Bad env vector")))))

;;; I haven't experimented with this at all.*****
(defun hash-blots (vector size &aux (hash 0))
  (mapc #'(lambda (number mask) (if (listp number) (setq number (car number)))
				(setq hash (rem (logxor hash number mask) size)))
	vector *randoms*)
  (if (> hash 0)
      hash
      (rem (+ hash most-positive-fixnum) size)))

;(defun hash-blots (vector size &aux (hash 0))
;  (mapc #'(lambda (number mask)
;	    (if (listp number) (setq number (* size (car number))))
;	    (setq hash (rem (logxor hash number mask) size)))
;	vector *randoms*)
;  (if (> hash 0)
;      hash
;      (rem (+ hash most-positive-fixnum) size)))

(defun vector-subset-blots (v1 v2 &aux c1)
  (prog nil

	START
	   (if (null v1) (return T))
	   (if (null v2) (return nil))

	   (when (listp (car v1))
	     (setq c1 (caar v1) v1 (cdr v1))
	     (go SKIP2))

	   (when (listp (car v2)) (return nil))
	   
	   (if (not-subset-bits (car v1) (car v2)) (return nil))

	   (setq v1 (cdr v1) v2 (cdr v2))

	   (go START)

	SKIP2

	   (cond ((null v2) (return nil))	; Can't be trailing 0.
		 
		 ((= c1 0) (go START))

		 ((not (listp (car v2)))
		  (decf c1)
		  (setq v2 (cdr v2))
		  (go SKIP2))

		 ((> c1 (caar v2)) (return nil))
		 ((= c1 (caar v2)) (setq v2 (cdr v2)) (go START))
		 (t (return nil)))))

;;;***** pick shortest first?  IS that worth it?
;;; Remember this version is permitted to recycle old structure, but not side afect.

;;; Is (n) ever clobbered.  This assumes yes.  But that is probably not right.***

(defun vector-union-blots (v1 v2 &aux vector c d)
  (prog nil
     START

	(cond ((null v1) (return (nreconc vector v2)))
	      ((null v2) (return (nreconc vector v1))))

     START1

	(cond ((listp (car v1))
	       (setq c (caar v1) v1 (cdr v1))
	       (go V1-IS-ZERO))
	      ((listp (car v2))
	       (setq c (caar v2) v2 (cdr v2))
	       (go V2-IS-ZERO)))

     START2

	(push (logior (car v1) (car v2)) vector)
	(setq v1 (cdr v1))
	(setq v2 (cdr v2))
	(go START)

     V1-IS-ZERO
	(cond ((= c 0) (go START))
	      ((null v2) (return (nreconc vector (cons (if (= c 1) 0 (list c)) v1))))
	      ((not (listp (car v2)))
	       (decf c) (push (car v2) vector) (setq v2 (cdr v2)) (go V1-IS-ZERO))
	      ((= 0 (setq d (- (caar v2) c)))
	       (push (car v2) vector) (setq v2 (cdr v2)) (go START2))
	      ((> d 0) (push (if (= c 1) 0 (list c)) vector) (setq c d v2 (cdr v2))
	       (go v2-is-zero))
	      (t (push (car v2) vector)
		 (setq c (- d)) ;;;**** d not neesary.
		 (setq v2 (cdr v2))
		 (go v1-is-zero)))
     V2-IS-ZERO
	(psetq v1 v2 v2 v1)
	(GO V1-IS-ZERO)))

;;; This returns FRESH list structure always.
;;; Must return fresh list structure.  Is it worth cdr-coding this??*******

(defun vector-union-new-blots (v1 v2 &aux vector c d)
  (prog nil
     START

	(cond ((null v1) (return (nreconc vector (fcopylist v2))))
	      ((null v2) (return (nreconc vector (fcopylist v1)))))

     START1

	(cond ((listp (car v1))
	       (setq c (caar v1) v1 (cdr v1))
	       (go V1-IS-ZERO))
	      ((listp (car v2))
	       (setq c (caar v2) v2 (cdr v2))
	       (go V2-IS-ZERO)))

     START2

	(push (logior (car v1) (car v2)) vector)
	(setq v1 (cdr v1))
	(setq v2 (cdr v2))
	(go START)

     V1-IS-ZERO
	(cond ((= c 0) (go START))
	      ((null v2) (return (nreconc vector (cons (if (= c 1) 0 (list c)) v1))))
	      ((not (listp (car v2)))
	       (decf c) (push (car v2) vector) (setq v2 (cdr v2)) (go V1-IS-ZERO))
	      ((= 0 (setq d (- (caar v2) c)))
	       (push (list (caar v2)) vector) (setq v2 (cdr v2)) (go START2))
	      ((> d 0) (push (if (= c 1) 0 (list c)) vector) (setq c d v2 (cdr v2))
	       (go v2-is-zero))
	      (t (push (list (caar v2)) vector)
		 (setq c (- d)) ;;;**** d not neesary.
		 (setq v2 (cdr v2))
		 (go v1-is-zero)))
     V2-IS-ZERO
	(psetq v1 v2 v2 v1)
	(GO V1-IS-ZERO)))

(defun vector-equal-blots (l1 l2 &aux t1 t2)
  (do ((l1 l1 (cdr l1))
       (l2 l2 (cdr l2)))
      ((eq l1 l2) T)
    (cond ((null l1) (return (null l2)))
	  ((null l2) (return nil))
	  (t (setq t1 (car l1) t2 (car l2))
	     ;; Which type tests are faster, interger, consp, listp?
	     (cond ((integerp t1)
		    (if (integerp t2) (unless (= t1 t2) (return nil)) (return nil)))
		   ((integerp t2) (return nil))
		   ((not (= (car t1) (car t2))) (return nil)))))))

(defun install-blots ()
  (setq *break-coded* nil)
  (setf (symbol-function 'vector-subset-info) #'vector-subset-blits)
  (setf (symbol-function 'vector-equal) #'vector-equal-blots)

  (setf (symbol-function 'nmap-assumptions) #'error)
  (setf (symbol-function 'nnvector-assumptions) #'error)
  ;****** temporary.
  (setf (symbol-function 'vector-cons4) #'vector-cons4-blots)
;  (setf (symbol-function 'vector-cons4) #'vector-cons4-bits*)
  (setf (symbol-function 'vector-intersection2?) #'error)
  (setf (symbol-function 'vector-intersection?) #'vector-intersection-blots?)
;  (setf (symbol-function 'vector-intersection?) #'vector-intersection-bits?)
  (setf (symbol-function 'vector-subset) #'vector-subset-blots)
  (setf (symbol-function 'vector-subset2) #'error)
  (setf (symbol-function 'vector-union) #'vector-union-blots)
  (setf (symbol-function 'vector-union-new) #'vector-union-new-blots)
  ;**** old clobbers its first arg.  Maybe wide-union should use it?
  (setf (symbol-function 'vector-union-old) #'vector-union-new-blots)
  (setf (symbol-function 'make-env-vector) #'make-env-vector-blots)
;  (setf (symbol-function 'make-env-vector) #'make-env-vector-bits)
  (setf (symbol-function 'vector-member) #'vector-member-blots)
;  (setf (symbol-function 'vector-member) #'vector-member-bits)

  (setf (symbol-function 'make-env-vector*) #'make-env-vector-blots)
;  (setf (symbol-function 'make-env-vector*) #'make-env-vector-bits*)

  (setf (symbol-function 'vector-cons1) #'error)
  (setf (symbol-function 'vector-cons3) #'vector-cons4-blots)
;  (setf (symbol-function 'vector-cons3) #'vector-cons3-bits)

  (setf (symbol-function 'basic-make-assumption-internal)
	#'basic-make-assumption-internal-bits)
  (setf (symbol-function 'construct-vector-run) #'error)
  #-Symbolics
  (format T "~% Warning, you need to write a decent hash function (blhash) for your machine.")
  ;;;**** this hash is wierd check it out if it works for blots.
  (setf (symbol-function 'hash) #'hash-blots)
  (setf (symbol-function 'vector-andc2) #'error)
  (setf (symbol-function 'remove-assumption) #'remove-assumption-blots)
;   (setf (symbol-function 'remove-assumption) #'remove-assumption-bits)
  )
    
(defun count-bits-blots (vector &aux (total 0))
  (dolist (v vector)
    (cond ((listp v) (if (< (car v) 0) (incf total #.*word-size*)))
	  ((= v 0))
	  ((> v 0) (incf total (logcount v)))
	  ;;****** must be a better way.
	  ((< v 0) (incf total (- #.*word-size* (logcount (- v)))))))
  total)