;;; -*- Mode: LISP; Syntax: Common-lisp; Base: 10; -*-


;;; This is the little ATMS

(defun delq (x l) (delete x l :TEST #'EQ))

(defun assq (x l) (assoc x l :TEST #'EQ))

(defun memq (x l) (member x l :TEST #'EQ))

(defstruct (node (:print-function
		      (lambda (node stream ignore)
			(format stream "<NODE: ~A>" (node-datum node)))))
	   (datum nil)
	   (label nil)
	   (justifications nil)
	   (consequences nil))

(defstruct (assumption 
	     (:print-function
	       (lambda (assumption stream ignore)
		 (format stream "<ASSUMPTION: ~A>" 
			 (assumption-datum assumption)))))
	   (datum nil)
	   (label nil)
	   (justifications nil)
	   (consequences nil)
	   (env nil))

(defstruct (env 
	     (:print-function
	       (lambda (env stream ignore)
		 (format stream "<ENV: ~A>" 
			 (mapcar #'assumption-datum (env-assumptions env))))))
	   (size nil) 
	   (assumptions nil) 
	   (nodes nil) 
	   (contradictory nil) 
	   (unions nil))

(defvar *empty-env*)

(defvar *nogoods*)

(defvar *envs*)

(defvar *contra-node*)

(defun init-tms () (setq *empty-env* (make-env :SIZE 0 :ASSUMPTIONS nil)
                         *envs* nil 
                         *nogoods* nil
			 *contra-node* (make-node :LABEL (list *empty-env*))
			 *contra-env* (make-env :SIZE 0
						:ASSUMPTIONS nil
						:CONTRADICTORY T)))

(defun create-node (datum) (make-node :DATUM datum))

(defun create-assumption (datum &aux assumption env)
  (setq assumption (make-assumption :DATUM datum)
 	env (make-env :SIZE 1 
                      :ASSUMPTIONS (list assumption) 
	              :NODES (list assumption)))
  (setf (assumption-env assumption) env)
  (setf (assumption-label assumption) (list env))
  assumption)

(defun justify-node (node justification &aux consequent)
  (unless (eq node *contra-node*)
    (setq consequent (cons node justification))
    (dolist (antecedent (cdr justification))
      (push consequent (node-consequences antecedent))))
  (justify-node-1 node justification))

(defun justify-node-1 (node justification &aux old-envs change)
  (setq old-envs (node-label node) new-envs old-envs)
  (dolist (env (justification-envs justification))
    (cond ((eq node *contra-node*) (contradictory-env env))
          ((memq env old-envs))
	  ((dolist (old-env old-envs)
	     (cond ((subset-env? old-env env) (return T))
		   ((subset-env? env old-env) 
		    (setq new-envs (delq old-env new-envs) change T)
		    (remove-node-env old-env node)))))
	  (t (push env new-envs)
	     (setq change T)
	     (add-node-env env node))))
  (cond ((eq node *contra-node*))
	(change (setf (node-label node) new-envs)
		(update-node-consequences node))))

(defun subset-env? (e1 e2)
  (cond ((eq e1 e2) T)
	((< (env-size e1) (env-size e2))
	 (not (dolist (assumption (env-assumptions e1))
		(unless (member assumption (env-assumptions e2)
				:TEST #'eq)
		  (return T)))))))

(defun remove-node-env (env node) 
  (setf (env-nodes env) (delq node (env-nodes env))))

(defun add-node-env (env node) (push node (env-nodes env)))

(defun update-node-consequences (node)
  (dolist (consequent (node-consequences node))
    (justify-node-1 (car consequent) (cdr consequent))))

(defun justification-envs (justification)
  (cond ((null (cdr justification)) (list *empty-env*))
	(t (do ((envs (node-label (cadr justification)))
		(justification (cddr justification) (cdr justification)))
	       ((null justification) envs)
	     (setq node (car justification)
	           envs (cross-product envs
			               (if (typep node 'NODE)
					   (node-label node)
					   (list (assumption-env node)))))
	     (if (null envs) (return envs))))))

(defun cross-product (envs1 envs2 &aux union result)
  (cond ((null envs1) nil)
	((null envs2) nil)
	((eq (car envs1) *empty-env*) envs2)
	((eq (car envs2) *empty-env*) envs1)
	(t (dolist (e1 envs1)
	     (dolist (e2 envs2)
	       (setq union (union-env e1 e2))
	       (unless (env-contradictory union) (push union result))))
	   (minimize result))))

(defun minimize (envs)
  (do ((e1 envs (cdr e1)))
      ((null e1) envs)
    (do ((e2 envs (cdr e2)))
	((null e2))
      (cond ((eq e1 e2))
	    ((and (car e1) (car e2) (subset-env? (car e1) (car e2)))
	     (rplaca e2 nil)))))
  (delq nil envs))


(defun union-env (e1 e2 &aux c1 c2)
  (cond ((eq e1 e2) e1)
	((env-contradictory e1) *contra-env*)
	((env-contradictory e2) *contra-env*)
	(t (setq c1 (env-size e1) c2 (env-size e2))
	   (cond ((> c1 c2)
		  (if (subset-env? e2 e1) e1
		      (union-env-1 e1 e2)))
		 ((< c1 c2)
		  (if (subset-env? e1 e2) e2
		      (union-env-1 e2 e1)))
		 (t (union-env-1 e1 e2))))))

(defun union-env-1 (e1 e2 &aux assumptions result)
  (cond ((cdr (assoc e2 (env-unions e1) :TEST #'eq)))
	(t (setq assumptions (env-assumptions e1))
	   (dolist (a (env-assumptions e2))
	     (unless (member a assumptions :TEST #'eq) (push a assumptions)))
	   (setq result (find-environment assumptions))
	   (push (cons e2 result) (env-unions e1))
	   result)))

(defun find-environment (assumptions &aux count new-env)
  (setq count (length assumptions))
  (cond ((= count 0) *empty-env*)
	((= count 1) (assumption-env (car assumptions)))
	((dolist (e *envs*) 
	   (and (= count (env-size e))
		(not (dolist (a (env-assumptions e)) 
		       (unless (member a assumptions :TEST #'EQ) (return t))))
		(return e))))
	((dolist (e *nogoods*)
	   (and (<= (env-size e) count)
		(not (dolist (a (env-assumptions e))
		       (unless (member a assumptions :TEST #'EQ)
			 (return t))))
		(return *contra-env*))))
	(t (setq new-env (make-env :SIZE count
			           :ASSUMPTIONS assumptions))
	   (push new-env *envs*)
	   new-env)))
	
(defun contradictory-env (env)
  (unless (env-contradictory env)
    (setq *nogoods* (delete env *nogoods* :TEST #'subset-env?))
    (push env *nogoods*)
    (contradictory-mark env)
    (setq *envs* (delete env *envs* :TEST #'(lambda (e1 e2)
					      (when (subset-env? e1 e2)
						(contradictory-mark env)
						T))))))

(defun contradictory-mark (env)
  (setf (env-contradictory env) T)
  (dolist (node (env-nodes env)) 
    (setf (node-label node) (delq env (node-label node)))))

;;; Interface to KDF's theory of function names.
(defun build-tms-node (datum) (create-node datum))	
		     
;;;; ******* really the alternativs should be assumptions.
(defun interpretations (sets &aux new-solutions new-interp counter)
  (setq counter 0 solutions (list *empty-env*))
  (dolist (alternatives sets solutions)
    (incf counter)
    (dolist (alternative alternatives)
      (dolist (old-e solutions)
	(setq new-interp (union-env old-e (car (node-label alternative))))
	(unless (env-contradictory new-interp)
	  (push new-interp new-solutions))))
    (setq solutions new-solutions
	  new-solutions nil)
	(print solutions)
    (format t "~%  Round ~D, ~D solutions."
	    counter (length solutions))))
    
(defun get-solutions (sets) (interpretations sets))

(defun assume-node (node &aux a)
  (setq a (create-assumption node))
  (justify-node node (list 'ASSUME a)))

(defun build-justification (type consequent antecedents)
  (justify-node consequent (cons type antecedents)))

(defun nogood-nodes (nodes) (justify-node *contra-node* (cons 'NG nodes)))
  
(defun tms-node-datum (node) (node-datum node))