" (c) 1992 Copyright (c) University of Washington
  Written by Tony Barrett.

  All rights reserved. Use of this software is permitted for non-commercial
  research purposes, and it may be copied only for that use.  All copies must
  include this copyright message.  This software is made available AS IS, and
  neither the authors nor the University of Washington make any warranty about
  the software or its performance.

  When you first acquire this software please send mail to
  bug-snlp@cs.washington.edu; the same address should be used for problems."

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; The following code is used to implement variable codesignation constraints.
;;; This code was created after looking at Steve Hanks's use of varsets.
;;; 
;;;

(in-package 'variable)

(export '(not-unify unify bind-variable instantiate-term redundant-bind
	  add-bind instantiate-bind copy-bindings new-bindings
	  *unify-count* *compute-rank-unifies* 
	  *computing-rank* *add-bind-count*))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Outline of this file
;;;
;;; 1. Structures used for implementing constraints
;;; 2. A handy interface function to unify two lists using constraint sets
;;; 3. CONSTRAINT SETS (CS)
;;; 4. VARSETS:  Each VARSET represents a set of codesignating variables.
;;; 5. VARIABLES  -- 
;;; 6. Print functions

;;;***************************************************************************
;;; 1. Structures used for implementing constraints

(defstruct (varset (:print-function print-varset))
  const          ; the unique constant that codesignates with this varset.
  cd-set         ; the set of variables (and constant) that codesignate
  ncd-set)	 ; Vars and consts that must not codesignate with this set

(defvar *unify-count* 0)		; Number of variable unifications made
(defvar *compute-rank-unifies* nil)	; Number of unifications made while computing rank fn
(defvar *computing-rank* nil)		; flag: are we computing a rank?
(defvar *add-bind-count* 0)		; Number of times new bindings were added to a plan

;;;***************************************************************************
;;; 2. A handy interface function to unify two lists using constraint sets

(defun NOT-UNIFY (p1 p2 cs &aux ret)
  "Return a list of constaint sets where P1 and P2 do not unify.  
   Assumes that they can be unified in the constraint set CS."
  (labels
      ((not-unify* (p1 p2 cs)
	 (cond ((null p1) nil)
	       ((codesignates (car p1) (car p2) cs)
		(not-unify* (cdr p1) (cdr p2) cs))
	       (t (let ((cs1 (copy-cs cs)))
		    (when (constrain-eq (car p1) (car p2) cs)
		      (constrain-neq (car p1) (car p2) cs1)
		      (push cs1 ret)
		      (not-unify* (cdr p1) (cdr p2) cs1))
		    (not-unify* (cdr p1) (cdr p2) cs))))))
    (not-unify* (cdr p1) (cdr p2) (copy-cs cs)))
  ret)

;;;;;;;;;;;;;;;;;;;;;;;;                                                  
;;; Test whether two conditions can be unified consistent with plan bindings
;;; Returns a list of the list of bindings needed to unify, i.e. has an extra
;;; set of parentheses.  Returns nil if they cannot be unified.  Returns (nil)
;;; if they unify with no additional bindings.

(defun UNIFY (cond1 cond2 bindings)
  ;; fix Jscott's bug
  (when (and (eq (car cond1) 'not) (eq (car cond2) 'not)) 
    (setf cond1 (cadr cond1)
	  cond2 (cadr cond2)))
  (when (and (= (list-length cond1)       ; elseif same length and 
		(list-length cond2))      ;      same predicate
	     (eq (car cond1) (car cond2)))
    (let ((result nil)
	  (a1 nil)
	  (a2 nil)
	  (cs (list (car bindings))))
      (do ((b1 (cdr cond1) (cdr b1))
	   (b2 (cdr cond2) (cdr b2)))
	  ((null b1) (list result))
	(incf *unify-count*)
	(if *computing-rank* (incf *compute-rank-unifies*))
	(setf a1 (get-vset (car b1) cs))
	(setf a2 (get-vset (car b2) cs))
	(when (not (eq a1 a2))
	  (push (list (car b1) (car b2)) result)
	  (let ((c (combine-varset a1 a2)))
	    (if c (push c (car cs))
		  (return nil))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Replace variable with associated constant from plan-bindings
;;; Leave as a variable if not bound to a constant
(defun BIND-VARIABLE (var bindings)
  (cond ((null var) nil)
	((listp var) (mapcar #'(lambda (x) (bind-variable x bindings))
			     var))
	(t (value var bindings))))

(defun NEW-BINDINGS ()
  (new-cs))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; mapcar-la acts like mapcar except that it expects the function to
;;; take two arguments and it makes a second list (same length as l)
;;; by repeating the atom
(defun MAPCAR-LA (funct l atom)
  (mapcar funct l (make-sequence 'list 
                                 (length l)
                                 :initial-element atom)))

;;;;;;;;;;;;;;;;;;;;;;;;
;;; Adds the integer high-step to the id of any variables
;;; Returns constants unchanged
(defun INSTANTIATE-TERM (term num)
  (cond
    ((variable? term) (make-variable term num))
    ((atom term)      term)
    (t (cons (instantiate-term (car term) num) 
	     (instantiate-term (cdr term) num)))))

;;;;;;;;;;;;;;;;;;;;;;;;                                                  
;;;  Add new entries to bindings
;;;  Input is list of pairs of two terms, each pair possibly preceded by 'not
;;;  Finds their entries E1 and E2 in binding hash table.  If necessary, 
;;;  entries are created.  If an entry has a constant in its value field,
;;;  the entry for that value is used.  If the original pair has 'not, 
;;;  then add-constraint is called.  Otherwise add-bind2 is called.
(defun ADD-BIND (new-bind
		 bindings)
  (when bindings
    (dolist (pair new-bind bindings)        ; 
      (incf *add-bind-count*)
      (if (not (if (eql 'not (car pair))
		   (constrain-neq (caadr pair) (cadadr pair) bindings)
		   (constrain-eq (car pair) (cadr pair) bindings)))
	  (return nil))))
  bindings)

;;;;;;;;;;;;;;;;;;;;;;;;
;;; Input is a list of new bind-pairs and a bindings hash table.
;;; Returns true if all bind-pairs are already synonyms in the
;;; hash table.
(defun REDUNDANT-BIND (new-bind bindings)
  (when new-bind
    (dolist (pair (car new-bind) t)
      (when (not (eq (get-vset (car pair) bindings)
		     (get-vset (cadr pair) bindings)))
	(return nil)))))

;;;;;;;;;;;;;;;;;;;;;;;;
;;; Add new high step number to each variable id for every term in
;;; bindings from template.
(defun INSTANTIATE-BIND (bind num)
  (mapcar-la #'instantiate-term bind num))

(defun COPY-BINDINGS (old-bind)
  (copy-cs old-bind))

;;;***************************************************************************
;;; 3. CONSTRAINT SETS (CS) --
;;;   A constraint set is a hash table mapping each variable/constant 
;;;   into its VARSET
;;;

(defun new-cs () 
  "Create a new constraint set."
  (list nil))

(defun copy-cs (cs) 
  (list (copy-list (car cs))))

(defun constrain-eq (sym1 sym2 cs)
  "Ensure that two symbols codesignate in a constraint set.
   Returns nil if symbols cannot codesignate."
  (let* ((v1 (get-vset sym1 cs))
	 (v2 (get-vset sym2 cs))
	 (vs (combine-varset v1 v2)))
    (when vs
      (setf (car cs)
	    (cons vs (delete-if #'(lambda (x) (or (eq x v1)(eq x v2))) 
				(car cs) :count 2)))
      t)))

(defun constrain-neq (sym1 sym2 cs)
  "Make sure that two symbols never codesignate in a constraint set.
   Returns nil if symbols already codesignate."
  (let* ((r1 (get-vset sym1 cs))
	 (v1 (restrict-varset r1 sym2))
	 (r2 (get-vset sym2 cs))
	 (v2 (restrict-varset r2 sym1)))
    (when (and v1 v2)
      (setf (car cs) 
	    (nsubstitute v1 r1 (car cs) :test #'eq :count 1))
      (setf (car cs) 
	    (nsubstitute v2 r2 (car cs) :test #'eq :count 1))
      t)))

(defun codesignates (sym1 sym2 cs)
  "Test to see if two symbols explicitely codesignate."
  (member sym2 (varset-cd-set (get-vset sym1 cs))))

(defun value (sym cs)
  "Get the value of a symbol.  It might be a constant or variable."
  (let ((v (get-vset sym cs)))
    (if (varset-const v) (varset-const v) (first (varset-cd-set v)))))

(defun get-vset (sym cs)
  "Get the varset associated with a symbol.  Might have to create it."
  (do ((c (car cs) (cdr c)))
    ((or (null c) (member sym (varset-cd-set (car c)) :test #'eql))
     (if c (car c)
	 (car (push (make-empty-varset sym) (car cs)))))))

;;;***************************************************************************
;;; 4. VARSETS:  Each VARSET represents a set of codesignating variables.
;;; Store for each 
;;;    (1) the constant (if any) they codesignate with, and 
;;;    (2) a set of codesignating variables and possibly a constant
;;;    (3) a set of constants and variables they CANNOT codesignate with.
;;;
;;; Some thoughts on VARSETs...
;;;   - The codesignation sets form equivalence classes.  This means that
;;;     the cd sets in the varsets are disjoint.
;;;   - Constants have varsets too!  This means that the only place that we
;;;     have to explicitely reason about a constant is to make sure that no
;;;     two unique constants codesignate.
;;;   - Since the cd sets in each varset contain all codesignating symbols,
;;;     there is no need to make sure that all symbols that must not 
;;;     codesignate are in the ncd lists.  Puting only one element of a 
;;;     codesignating varset in the ncd is enough to ensure that the
;;;     noncodesignating varsets can never get combined.
;;;

(defun make-empty-varset (symb)
  "Make a new varset for SYMB (if it has never been seen before).
   Constants appear in varsets too!"
  (make-varset :cd-set (list symb)
               :const (if (variable? symb) nil symb)
               :ncd-set nil))

(defun combine-varset (a b)
  "Combine two varsets.  (called for each codesignation constraint)"
  (if (eq a b) a
      (when (or (null (varset-const a))
		(null (varset-const b)))
	(let ((cd-set  (var-union (varset-cd-set a) (varset-cd-set b)))
	      (ncd-set (var-union (varset-ncd-set a) (varset-ncd-set b)))
	      (const   (if (varset-const a) (varset-const a)
			   (varset-const b))))
	  (when (and (not (member const ncd-set :test #'eql))
		     (not (var-intersect? cd-set ncd-set)))
	    (make-varset :const const
			 :cd-set cd-set
			 :ncd-set ncd-set))))))

(defun restrict-varset (vset restricter)
  "Make sure that VSET never codesignats with a varset containing RESTRICTER."
  (when (not (member restricter (varset-cd-set vset) :test #'eql))
    (make-varset :const (varset-const vset)
                 :cd-set (varset-cd-set vset)
                 :ncd-set (var-union (list restricter) 
				     (varset-ncd-set vset)))))

(defun var-union (a b) ; &aux ret
  (union a b :test #'eql))

(defun var-intersect? (a b)
  (intersection a b :test #'eql))

;;;**************************************************************
;;; 5. VARIABLES  -- This code was written by Steve Hanks 
;;;                            and modified by J Scott Penberthy
;;;

(defvar *variable-cache* (make-hash-table :test #'equal))

(defun variable? (thing)
  (and (symbolp thing)
       (char= #\? (elt (symbol-name thing) 0))))

(defun strip-prepended-? (thing)
  (cond ((symbolp thing)
	 (let ((name (symbol-name thing)))
	   (if (char= #\? (elt (symbol-name thing) 0))
	       (subseq name 1)
	     name)))
	(t (princ-to-string thing))))

(defun make-variable (&rest id)
  (multiple-value-bind (val got-it) (gethash id *variable-cache*)
   (unless got-it
    (setf (gethash id *variable-cache*)
	  (setq val
		(intern
		 (apply #'concatenate 'string "?"
			(mapcar #'strip-prepended-? id))
		 (symbol-package (first id))))))
   (values val)))

;;;***************************************************************************
;;; 6. Print functions
;;;

(defun print-hash-table (table &optional (stream *terminal-io*) (indent 0))
  (let ((format-string (concatenate 'string 
				    "~" (write-to-string indent) "T~a  ~a~%")))
    (maphash #'(lambda (key val) (format stream format-string key val))
	     table)))

(defun print-varset (self stream depth)
  (declare (ignore depth))
  (format stream "<VARSET {~a} = ~a not~a>" 
          (varset-cd-set self) 
          (varset-const self) 
          (varset-ncd-set self)))