;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - NFS Share File - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(in-package 'user :use '(lisp))

(export '(type-declarations
	   make-declaration
	   expression-type
	   combination-type
	   if-equal
	   immediate-binding
	   create-expression
	   equal?
	   known-equal?
	   ensuring
	   some-such-that
	   expression-variables-of
	   gensym-var-of-type
	   apply-substitution
	   nd-some
	   nd-every
	   nd-every2
	   convert-exp-vars
	   alpha-rename))

(defun export-nondeterministic (symbols)
  (mapcar (lambda (sym)
	    (export
	      (intern (format nil "~A-NONDETERMINISTIC"  sym)
		      (symbol-package sym)))
	    (export sym))
	  (if (listp symbols) symbols (list symbols))))

(export-nondeterministic '(member? determine-matches))

(defstruct (expression-variable (:conc-name nil)
				(:print-function print-expression-var)
				(:predicate expression-variable?))
  variable-pname
  variable-type
  variable-binding
  binding-noticers)

(defun print-expression-var (variable stream x)
  (declare (ignore x))
  (if (variable-binding variable)
      (format stream "~s" (variable-binding variable))
      (format stream "[~s]" (variable-pname variable))))

(defun create-expression-variable (name-symbol type)
  (make-expression-variable :variable-pname name-symbol :variable-type type))

(defun apply-substitution (exp)
  (let ((imm (immediate-binding exp)))
    (if (consp imm)
	(cons (apply-substitution (car imm))
	      (apply-substitution (cdr imm)))
	imm)))

(defun immediate-binding (exp)
  (if (not (expression-variable? exp))
      exp
      (let ((binding (variable-binding exp)))
	(if binding
	    (immediate-binding binding)
	    exp))))

(defun bind! (variable expression)
  (when (occurs-in? variable expression)
    (fail))
  (when (not (equal (expression-type variable) (expression-type expression)))
    (fail))
  (when (variable-binding variable)
    (error "attempt to bind a variable that is already bound"))
  (locally-setf (variable-binding variable) expression)
  (mapc 'funcall (binding-noticers variable)))

(defun occurs-in? (var expression)
  (let ((imm (immediate-binding expression)))
    (cond ((eq var imm) t)
	  ((consp imm)
	   (or (occurs-in? var (car imm))
	       (occurs-in? var (cdr imm))))
	  (t nil))))



(defun assert-equal! (exp1 exp2)
  (let ((imm1 (immediate-binding exp1))
	(imm2 (immediate-binding exp2)))
    (cond ((equal imm1 imm2) t)
	  ((expression-variable? imm1)
	   (bind! imm1 imm2))
	  ((expression-variable? imm2)
	   (bind! imm2 imm1))
	  ((and (consp imm1) (consp imm2))
	   (assert-equal! (car imm1) (car imm2))
	   (assert-equal! (cdr imm1) (cdr imm2)))
	  ((not (and (atom imm1) (atom imm2) (eq imm1 imm2)))
	   (fail)))))

(defun known-equal? (exp1 exp2)
  (let ((imm1 (immediate-binding exp1))
	(imm2 (immediate-binding exp2)))
    (or (eq imm1 imm2)
	(and (consp imm1)
	     (consp imm2)
	     (known-equal? (car imm1) (car imm2))
	     (known-equal? (cdr imm1) (cdr imm2))))))

(defun possibly-equal? (exp1 exp2)
  (one-value (progn (assert-equal! exp1 exp2) t)
	     nil))

(defun assert-not-equal! (exp1 exp2)
  (when (possibly-equal? exp1 exp2)
    (let ((pair (cons exp1 exp2))
	  (self nil))
      (let ((noticer (lambda ()
		       (when (known-equal? exp1 exp2)
			 (fail))
		       (dolist (var (expression-variables-of pair))
			 (unless (member self (binding-noticers var))
			   (locally-setf (binding-noticers var)
					 (cons self (binding-noticers var))))))))
	(setf self noticer)
	(funcall noticer)))))

(defun expression-variables-of (exp)
  (let ((variables nil))
    (labels ((variables-of-2 (exp2)
	       (let ((imm (immediate-binding exp2)))
		 (cond ((expression-variable? imm)
			(pushnew imm variables))
		       ((consp exp2)
			(variables-of-2 (car exp2))
			(variables-of-2 (cdr exp2)))))))			
      (variables-of-2 exp))
    variables))

(defmacro if-equal (exp1 exp2 &body cases)
  (let ((exp1var (gensym "EXP1-"))
	(exp2var (gensym "EXP2-")))
    `(let ((,exp1var ,exp1)
	   (,exp2var ,exp2))
       (either (progn (assert-not-equal! ,exp1var ,exp2var)
		      ,(second cases))
	       (progn (assert-equal! ,exp1var ,exp2var)
		      ,(first cases))))))


(defun create-expression (template)
  (let ((subst nil))
    (labels ((create-copy2 (template)
	       (cond ((variable? template)
		      (or (cdr (assoc template subst))
			  (let ((new-var
				  (create-expression-variable (copy-var template)
							      (expression-type template))))
			    (push (cons template new-var) subst)
			    new-var)))
		     ((consp template)
		      (cons (create-copy2 (car template))
			    (create-copy2 (cdr template))))
		     (t template))))
      (create-copy2 template))))

(defun variable? (x)
  (and (symbolp x) (string= "?" (subseq (string x) 0 1))))

(defun copy-var (var)
  (let ((string (string var)))
    (let ((pos (position #\- string)))
      (if pos
	  (gensym (subseq string 0 (1+ pos)))
	  (gensym (concatenate 'string string "-"))))))



(defun test-unify (e1 e2)
  (one-value
    (progn (assert-equal! e1 e2)
	   (apply-substitution e1))
    'fail))


(defmacro type-declarations (&body declarations)
  (let ((decl (gensym "DACEL-")))
    `(dolist (,decl ',declarations)
       (make-declaration (first ,decl) (second ,decl)))))

(defun make-declaration (symbol type)
  (setf (get symbol 'symbol-type) type))

(defun expression-type (expression)
  (cond ((expression-variable? expression) (variable-type expression))
	((symbolp expression)
	 (let ((type (get expression 'symbol-type)))
	   (unless type
	     (error "~s has no declared type" expression))
	   type))
	(t (selectmatch (expression-type (first expression))
	     ((?input-types ?output-type)
	      (unless (= (length ?input-types) (length (cdr expression)))
		(error "wrong number of arguments in ~s" expression))
	      (mapc (lambda (input input-type)
		      (unless (eq (expression-type input) input-type)
			(error "~s is an illegal argument in ~s"
			       input
			       expression)))
		    (cdr expression)
		    ?input-types)
	      ?output-type)))))

(defun combination-type (types)
  (selectmatch (first types)
    ((?input-types ?output-type)
     (when (and (= (length ?input-types) (length (cdr types)))
		(every #'equal
		       (cdr types)
		       ?input-types))
       ?output-type))))


;;;  utilities built on exp-con and screamer


(defun-nondeterministic member? (x set)
  (and (not (null set))
       (if-equal x (car set)
	 t
	 (member? x (cdr set)))))


(defun-nondeterministic determine-matches (x set)
  (and (not (null set))
       (let ((cdr-result (determine-matches x (cdr set))))
	 (if-equal x (car set)
	   t
	   cdr-result))))

(defun-nondeterministic subset? (set1 set2)
  (or (null set1)
      (and (member? (car set1) set2)
	   (subset? (cdr set1) set2))))

(defun-nondeterministic intersects? (set1 set2)
  (and (not (null set1))
       (or (member? (car set1) set2)
	   (intersects? (cdr set1) set2))))

(defun-nondeterministic set-diff (set1 set2)
  (cond ((null set1) nil)
	((member? (car set1) set2)
	 (set-diff (cdr set1) set2))
	(t
	 (cons (car set1)
	       (set-diff (cdr set1) set2)))))

(defun-nondeterministic rem-dups (set)
  (when set
    (if (member? (car set) (cdr set))
	(rem-dups (cdr set))
	(cons (car set) (rem-dups (cdr set))))))

(defun-nondeterministic set-union (set1 set2)
  (cond ((null set1)
	 set2)
	((member? (car set1) set2)
	 (set-union (cdr set1) set2))
	(t
	 (cons (car set1) (set-union (cdr set1) set2)))))

(defmacro equal? (x y)
  `(if-equal ,x ,y
     t
     nil))

(emacs-indent ensuring 1)
(defmacro ensuring (phi &body body)
  `(if ,phi
       (progn ,@body)
       (fail)))

(defmacro some-such-that (type var phi)
  `(let ((,var ,type))
     (if ,phi
	 ,var
	 (fail))))

(defun gensym-var-of-type (type &optional (string "VAR-") (package *package*))
  (let ((var
	  (loop
	    (let ((var-string (format nil "?~s" (gentemp string))))
	      (when (not (find-symbol var-string package))
		(return (intern var-string package)))))))
    (make-declaration var type)
    var))

(defun-nondeterministic nd-some (pred list)
  (when list
    (if (funcall-nondeterministic pred (first list))
	t
	(nd-some pred (rest list)))))

(defun-nondeterministic nd-every (pred list)
  (or (null list)
      (and (funcall-nondeterministic pred (first list))
	   (nd-every pred (rest list)))))

(defun-nondeterministic nd-every2 (pred list1 list2)
  (or (and (null list1)
	   (null list2))
      (and (not (null list1))
	   (not (null list2))
	   (funcall-nondeterministic pred (first list1) (first list2))
	   (nd-every2 pred (rest list1) (rest list2)))))


(defun convert-exp-vars (exp)
  (let ((exp (immediate-binding exp)))
    (cond ((consp exp) (cons (convert-exp-vars (car exp))
			     (convert-exp-vars (cdr exp))))
	  ((expression-variable? exp)
	   (let ((var-sym (intern (symbol-name (variable-pname exp)))))
	     (make-declaration var-sym (variable-type exp))
	     var-sym))
	  (t exp))))

(defun alpha-rename (expression)
  (create-expression (convert-exp-vars expression)))