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

(defun put (key1 key2 value)
  (setf (get key1 key2) value))

;;; Printing utility

(defun print-chain-elements-on-separate-lines (chain)
  (if (empty-chain? chain)
      (format t "~%Done.")
      (progn (format t "~%~S" (head chain))
	     (print-chain-elements-on-separate-lines (tail chain)))))

;;; Frame access operations

(defsubst make-binding (variable value)
  (cons variable value))

(defsubst binding-variable (binding)
  (car binding))

(defsubst binding-value (binding)
  (cdr binding))

(defsubst binding-in-frame (variable frame)
  (assoc variable frame :test #'equal))

(defun lookup-in-frame (variable frame)
  (binding-value (binding-in-frame variable frame)))

(defsubst extend (variable value frame)
  (cons (make-binding variable value) frame))

;;; Abstract query syntax

(defun type (exp)
  (if (atom exp)
      (error "Unknown expression in TYPE")
      (if (symbolp (car exp)) (car exp) nil)))

(defun t-contents (exp)
  (if (atom exp)
      (error "Unknown expression in T-CONTENTS")
      (cdr exp)))

(defun assertion-to-be-added? (exp)
  (eq (type exp) 'ASSERT!))

(defun add-assertion-body (exp)
  (car (t-contents exp)))

(defsynonym empty-conjunction? null)
(defsynonym first-conjunct     car)
(defsynonym rest-conjuncts     cdr)

(defsynonym empty-disjunction? null)
(defsynonym first-disjunct     car)
(defsynonym rest-disjuncts     cdr)

(defsynonym negated-query car)

(defsynonym predicate car)
(defsynonym args      cdr)

(defun rule? (statement)
  (if (atom statement)
      nil
      (eq (car statement) 'RULE)))

(defsynonym conclusion cadr)

(defun rule-body (rule)
  (if (null (cddr rule))
      '(ALWAYS-TRUE)
      (caddr rule)))

(defun query-syntax-process (exp)
  (map-over-atoms #'expand-question-mark exp))

(defun map-over-atoms (proc exp)
  (if (atom exp)
      (funcall proc exp)
      (cons (map-over-atoms proc (car exp))
	    (map-over-atoms proc (cdr exp)))))

(defun expand-question-mark (atom)
  (if (symbolp atom)
      (let ((name (symbol-name atom)))
	(if (eql (elt name 0) #\?)
	    (list '? (intern (substring name 1)))
	    atom))
      atom))

(defun var? (exp)
  (if (atom exp)
      nil
      (eq (car exp) '?)))

(defsynonym constant?           atom)
(defsynonym constant-symbol? symbolp)
(defsynonym same-constant?     equal)

(defvar *rule-counter* 0)

(defun new-rule-application-id ()
  (incf *rule-counter*)
  *rule-counter*)

(defun make-new-variable (var rule-application-id)
  (cons '? (cons rule-application-id (cdr var))))

(defun contract-question-mark (var)
  (intern (string-append "?"
			 (symbol-name (if (numberp (cadr var))
					  (caddr var)
					  (cadr var))))))

;;; The data base

(defvar *the-assertions* the-empty-chain)

(defun fetch-assertions (pattern frame)
  (if (use-index? pattern)
      (get-indexed-assertions pattern)
      (get-all-assertions)))

(defun get-all-assertions ()  *the-assertions*)

(defun get-indexed-assertions (pattern)
  (get-chain (index-key-of pattern) 'ASSERTION-CHAIN))

(defun get-chain (key1 key2)
  (let ((s (get key1 key2)))
    (if (null s) the-empty-chain s)))

(defvar *the-rules* the-empty-chain)

(defun fetch-rules (pattern frame)
  (if (use-index? pattern)
      (get-indexed-rules pattern)
      (get-all-rules)))

(defun get-all-rules () *the-rules*)

(defun get-indexed-rules (pattern)
  (append-chains
    (get-chain (index-key-of pattern) 'RULE-CHAIN)
    (get-chain '? 'RULE-CHAIN)))

(defun add-rule-or-assertion! (assertion)
  (if (rule? assertion)
      (add-rule! assertion)
      (add-assertion! assertion)))

(defun add-assertion! (assertion)
  (store-assertion-in-index assertion)
  (let ((old-assertions *the-assertions*))
    (setq *the-assertions* (cons-chain assertion old-assertions))
    'ok))

(defun add-rule! (rule)
  (store-rule-in-index rule)
  (let ((old-rules *the-rules*))
    (setq *the-rules* (cons-chain rule old-rules))
    'ok))

(defun store-assertion-in-index (assertion)
  (if (indexable? assertion)
      (let ((key (index-key-of assertion)))
	(let ((current-assertion-chain
		(get-chain key 'ASSERTION-CHAIN)))
	  (put key 'ASSERTION-CHAIN
	       (cons-chain assertion current-assertion-chain))))))

(defun store-rule-in-index (rule)
  (let ((pattern (conclusion rule)))
    (if (indexable? pattern)
	(let ((key (index-key-of pattern)))
	  (let ((current-rule-chain
		  (get-chain key 'RULE-CHAIN)))
	    (put key 'RULE-CHAIN
		 (cons-chain rule current-rule-chain)))))))

(defun indexable? (pat)
  (or (constant-symbol? (car pat))
      (var? (car pat))))

(defun index-key-of (pat)
  (let ((key (car pat)))
    (if (var? key) '? key)))

(defun use-index? (pat)
  (constant-symbol? (car pat)))

;;; Rules and unification

(defun apply-rules (pattern frame)
  (flatmap #'(lambda (rule) (apply-a-rule rule pattern frame))
	   (fetch-rules pattern frame)))

(defun apply-a-rule (rule query-pattern query-frame)
  (let ((clean-rule (rename-variables-in rule)))
    (let ((unify-result (unify-match query-pattern
				     (conclusion clean-rule)
				     query-frame)))
      (if (empty-chain? unify-result)
	  the-empty-chain
	  (qeval (rule-body clean-rule) unify-result)))))

(defun rename-variables-in (rule)
  (let ((rule-application-id (new-rule-application-id)))
    (labels ((tree-walk (exp)
	       (cond ((constant? exp) exp)
		     ((var? exp)
		      (make-new-variable exp rule-application-id))
		     (t (cons (tree-walk (car exp))
			      (tree-walk (cdr exp)))))))
      (tree-walk rule))))

(defun unify-match (p1 p2 frame)
  (let ((result (internal-unify p1 p2 frame)))
    (if (eq result 'failed)
	the-empty-chain
	(singleton-chain result))))

(defun internal-unify (p1 p2 frame)
  (cond ((eq frame 'failed) 'failed)
	((var? p1) (extend-if-possible p1 p2 frame))
	((var? p2) (extend-if-possible p2 p1 frame))
	((constant? p1)
	 (if (constant? p2)
	     (if (same-constant? p1 p2) frame 'failed)
	     'failed))
	((constant? p2) 'failed)
	(t (internal-unify (cdr p1)
			   (cdr p2)
			   (internal-unify (car p1)
					   (car p2)
					   frame)))))

(defun extend-if-possible (var val frame)
  (if (equal var val)
      frame
      (let ((value-cell (binding-in-frame var frame)))
	(if (null value-cell)
	    (if (freefor? var val frame)
		(extend var val frame)
		'failed)
	    (internal-unify (binding-value value-cell)
			    val
			    frame)))))

(defun freefor? (var exp frame)
  (labels ((freewalk (e)
	     (cond ((constant? e) t)
		   ((var? e)
		    (if (equal? var e)
			nil
			(freewalk (lookup-in-frame e frame))))
		   ((freewalk (car e)) (freewalk (cdr e)))
		   (t nil))))
    (freewalk exp)))

;;; Finding assertions by pattern matching

(defun find-assertions (pattern frame)
  (flatmap #'(lambda (datum)
	       (pattern-match pattern datum frame))
	   (fetch-assertions pattern frame)))

(defun pattern-match (pat dat frame)
  (let ((result (internal-match pat dat frame)))
    (if (eq result 'failed)
	the-empty-chain
	(singleton-chain result))))

(defun internal-match (pat dat frame)
  (cond ((eq frame 'failed) 'failed)
	((var? pat) (extend-if-consistent pat dat frame))
	((constant? pat)
	 (if (constant? dat)
	     (if (same-constant? pat dat) frame 'failed)
	     'failed))
	((constant? dat) 'failed)
	(t (internal-match (cdr pat)
			   (cdr dat)
			   (internal-match (car pat)
					   (car dat)
					   frame)))))

(defun extend-if-consistent (var dat frame)
  (let ((value (binding-in-frame var frame)))
    (if (null value)
	(extend var dat frame)
	(internal-match (binding-value value) dat frame))))

;;; Top level and special forms

(defun query-driver-loop ()
  (loop 
	(let ((q (query-syntax-process (prompt-and-read :read "~&Query ==> "))))
	      (progn (print-chain-elements-on-separate-lines
		       (map-chain #'(lambda (frame)
				(instantiate q
					     frame
					     #'(lambda (v f)
						 (contract-question-mark v))))
			    (qeval q (singleton-chain '()))))))))

(defun instantiate (exp frame unbound-var-handler)
  (labels ((copy (exp)
	     (cond ((constant? exp) exp)
		   ((var? exp) (let ((vcell (binding-in-frame exp frame)))
				 (if (null vcell)
				     (funcall unbound-var-handler exp frame)
				     (copy (binding-value vcell)))))
		   (t (cons (copy (car exp))
			    (copy (cdr exp)))))))
    (copy exp)))

(defun qeval (query frame-chain)
  (if (atom query)
      the-empty-chain
  (let ((form (type query))
	(contents (t-contents query)))
    (cond ((eq form 'ASSERT!)     (add-rule-or-assertion! (add-assertion-body query)))
	  ((eq form 'ALWAYS-TRUE) (always-true contents frame-chain))
	  ((eq form 'QUOTE)       (singleton-chain contents))
	  (t (asserted? query (append-chains
				(list->chain
				  (mapcar #'(lambda (element)
					      (qeval element frame-chain))
					  contents))
				frame-chain)))))))

(defun asserted? (query-pattern frame-chain)
  (append-chains
    (flatmap #'(lambda (frame) (find-assertions query-pattern frame))
	     frame-chain)
    (flatmap #'(lambda (frame) (apply-rules query-pattern frame))
	     frame-chain)))

(defun always-true (ignore frame-stream)
  frame-stream)

(put 'always-true 'qeval #'always-true)