;;;; Rewriting
;;;; ND
;;;; 18 Feb 2004

;;;; Innermost and outermost rewriting
;;;; Terms are s-expressions
;;;; Rules are dotted pairs (l . r)
;;;; Variables start with u,v,w,x,y,z
;;;; Systems are lists
;;;; (Substitutions are lists of dotted pairs)

(defun var? (x) 
  ;; Is x a variable (start with u,v,w,x,y,z)?
  (and (atom x)
       (member (aref (prin1-to-string x) 0) 
               '(#\U #\V #\W #\X #\Y #\Z))))

(defun subs (s z)
  ;; Apply substitution s to z
  (if (null s)
      z
    (subs (cdr s)
          (subst (cdar s) (caar s) z))))
  
(defun match? (pat arg)
  ;; Does the pattern pat match the term arg?
  (cond ((var? pat) t)
        ((atom pat) (equal pat arg))
        ((atom arg) nil)
        (t (and (match? (car pat) (car arg))
                (match? (subs (match (car pat) (car arg)) 
                              (cdr pat))
                        (cdr arg))))))

(defun match (pat arg)
  ;; Return substitution s such that s(pat)=arg
  (cond ((var? pat) (list (cons pat arg)))
        ((atom pat) nil)
        ((atom arg) nil)
        (t (append (match (car pat) (car arg))
                   (match (subs (match (car pat) (car arg)) 
                                (cdr pat))
                          (cdr arg))))))

(defun rule (r x)
  ;; Top rewrite of term x by rule r
  ;; Presumes match
  (subs (match (car r) x) (cdr r)))

(defun tops (s x)
  ;; Top rewrite of term x by system s
  (cond ((null s) x)
        ((match? (caar s) x) (rule (car s) x))
        (t (tops (cdr s) x))))
  
(defun redex? (s x)
  ;; Is term x a redex of system s?
  (cond ((null s) nil)
        ((match? (caar s) x) t)
        (t (redex? (cdr s) x))))

(defun nf? (s x)
  ;; Is term x a normal form of system s?
  (cond ((redex? s x) nil)
        ((atom x) t)
        ((redex? s (car x)) nil)
        (t (and (nf? s (car x)) (nf? s (cdr x))))))

(defun outer1 (s x)
  ;; Outermost reduct of term x by system s
  (cond ((null x) nil)
        ((redex? s x) (tops s x))
        ((nf? s (car x)) (cons (car x) (outer1 s (cdr x))))
        (t (cons (outer1 s (car x)) (cdr x)))))

(defun outer (s x)
  ;; Outermost normal form of term x by system s
    (if (nf? s x)
        x
      (outer s (outer1 s x))))

(defun inner (s x)
  ;; Innermost normal form of term x by system s
  (cond ((nf? s x) x)
        ((atom x) (if (match? (caar s) x) 
                      (inner s (rule (car s) x))
                    (inner (cdr s) x)))
        (t (inner s (tops s (cons (inner s (car x)) 
                                  (inner s (cdr x))))))))