(setq allrules
   '(((tom is a cat))
     ((jerry is a mouse))
     ((spike is a dog))
     ((1 would eat 2) (1 is a cat) (2 is a mouse))
     ((1 would chase 2) (1 is a dog) (2 is a cat))
     ((1 would chase 2) (1 would eat 2))
     ((1 likes 2) (3 would eat 1) (2 would chase 3))))

(setq generation 10)

(defun lookup (Var AL)
  (cond ((null AL)
              Var)
        ((eq Var (caar AL))
              (cadar AL))
        (t
              (lookup Var (cdr AL)))))

(defun rewrite (Term AL)
  (cond ((numberp Term)
              (lookup Term AL))
        ((consp Term)
              (cons (rewrite (car Term) AL)
                    (rewrite (cdr Term) AL)))
        (t    
              Term)))

(defun rewritecars (X AL)
  (if (null X)
      nil
      (cons (list (rewrite (caar X) AL)
                  (cadar X))
            (rewritecars (cdr X) AL))))

(defun occurs (Var Term)
  (cond ((eq Var Term)
               t)
        ((consp Term)
               (if (occurs Var (car Term))
                   t
                   (occurs Var (cdr Term))))
        (t     
               nil)))

(defun unify (A B)
  (cond ((numberp A)
             (if (occurs A B)
                 'fail
                 (list (list A B))))
        ((numberp B)
             (if (occurs B A)
                 'fail
                 (list (list B A))))
        ((and (consp A) (consp B))
             (let ((AL1 (unify (car A) (car B))))
                (if (eq AL1 'fail)
                    'fail
                    (let* ((restA (rewrite (cdr A) AL1))
                           (restB (rewrite (cdr B) Al1))
                           (AL2 (unify restA restB)))
                        (if (eq AL2 'fail)
                            'fail
                            (combine AL1 AL2))))))
        ((eq A B)
             nil)
        (t
             'fail)))
 
(defun combine (AL1 AL2)
  (if (null AL2)
      AL1
      (cons (list (caar AL2)
                  (rewrite (cadar AL2) AL1))
            (combine AL1 (cdr AL2)))))

(defun updatevars (A Inc)
   (cond ((numberp A)
              (+ A Inc))
         ((consp A)
              (cons (updatevars (car A) Inc)
                    (updatevars (cdr A) Inc)))
         (t 
              A)))

(defun pairallwith (Collection Item)
   (if (null Collection)
       nil
       (cons (list (car Collection) Item)
             (pairallwith (cdr Collection) Item))))

(defun findmatch (target rules)
   (if (null rules)
       'fail
       (let* ((firstrule (car rules))
              (rulehead (car firstrule))
              (requirements (cdr firstrule))
              (freshhead (updatevars rulehead generation))
              (AL (unify freshhead target)))
           (if (eq AL 'fail)
               (findmatch target (cdr rules))
               (let* ((freshreqs (updatevars requirements generation))
                      (newreqs (rewrite freshreqs AL))
                      (newgoals (pairallwith newreqs allrules)))
                   (setq generation (+ generation 10))
                   (list newgoals AL (cdr rules)))))))

(defun resolvestep (possibilitylist)
   (if (null possibilitylist)
       'fail
       (let* ((goallist (caar possibilitylist))
              (original (cadar possibilitylist))
              (otherposs (cdr possibilitylist)))
          (if (null goallist)
              (list t original otherposs)
              (let* ((predicate (caar goallist))
                     (rules (cadar goallist))
                     (othergoals (cdr goallist))
                     (match (findmatch predicate rules)))
   "The rest of this function is secret")))))
     
(defun start (query)
   (setq generation 10)
   (list (list (list (list query allrules)) query)))

(defun resolve (query)
   (let ((state (start query))
         (inp nil))
      (pr state)
      (princ "not there yet.")
      (terpri)
      (loop
         (setq inp (read-line))
         (if (string= inp "") 
             nil 
             (return 'bye))
         (setq state (resolvestep state))
         (if (eq state 'fail) 
             (progn (princ "no (more) solutions") 
                    (terpri)
                    (return 'fail))
             nil)
         (if (eq (car state) t)
             (progn (princ "solution: ")
                    (princ (cadr state))
                    (terpri)
                    (setq state (caddr state)))
             (progn (princ "not there yet.")
                    (terpri)
                    (setq state (cadr state))
                    (pr state))))))
   
(defun pr (all)
   (if (null all)
       nil
       (progn (princ "   possibility") (terpri)
              (prposs (car all))
              (pr (cdr all)))))
              
(defun prposs (po)
   (princ "      conditions") (terpri)
   (prgoals (car po))
   (princ "      solution ")
   (princ (cadr po))
   (terpri))
   
(defun prgoals (gs)
   (if (null gs)
       nil
       (progn (princ "         ")
              (princ (caar gs))
              (princ " using last ")
              (princ (length (cadar gs)))
              (princ " rules")
              (terpri)
              (prgoals (cdr gs)))))