;;;
;;; subst.lisp: Utility functions for manipulating substitutions
;;;
;;; By Philip W. L. Fong
;;;
;;;
;;; Definition:
;;;
;;; An "symbolic expression" is either a (non-NIL) symbol or a list of 
;;; symbolic expressions.  In the following, we refer to a symbolic expression
;;; as "expression" for short.
;;;

(defun collect-variables (exp)
  "Return a list of all variables occurring in symbolic expression EXP."
  (collect-variables-aux exp nil))

(defun collect-variables-aux (exp acc)
  "Helper function for accumulating variables occurring in symbolic
expression EXP."
  (if (listp exp)
      (if (null exp)
	  acc
	(collect-variables-aux (rest exp)
			       (collect-variables-aux (first exp) acc)))
    (if (variable-p exp)
	(adjoin exp acc)
      acc)))

;;
;; A binding is a pair (EXP SYM).
;;

(defun make-binding (sym exp)
  "Construct a binding that binds symbol SYM to expression EXP."
  (list exp sym))

(defun binding-sym (binding)
  "Select the SYM component from a binding."
  (second binding))

(defun binding-exp (binding)
  "Select the EXP component from a binding."
  (first binding))

;;
;; Substitutions:
;;
;; A substitution is a list of bindings.
;; 

(defun make-empty-substitution ()
  "Create an empty substitution."
  nil)

(defun make-unit-substitution (sym exp)
  "Create a substitution containing only one binding EXP/SYM."
  (list (make-binding sym exp)))

(defun substitution-look-up (sub sym)
  "Look up the expression to which symbol SYM is bound in substitution SUB."
  (if (null sub)
      sym
    (if (eq sym (binding-sym (first sub)))
	(binding-exp (first sub))
      (substitution-look-up (rest sub) sym))))

(defun apply-substitution (sub exp)
  "Apply substitution SUB to expression EXP."
  (if (listp exp)
      (mapcar #'(lambda (x) (apply-substitution sub x))
	      exp)
    (substitution-look-up sub exp)))

(defun rename-variables (exp)
  "Rename the variables in EXP to fresh variables."
  (apply-substitution (mapcar #'(lambda (var) 
				  (make-binding var (make-fresh-variable)))
			      (collect-variables exp))
		      exp))
;;
;; Unification Equations
;;

(defun make-equation (lhs rhs)
  "Construct a unification equation with left hand side LHS and
right hand side RHS."
  (list lhs rhs))

(defun equation-lhs (equation)
  "Select the LHS of a unification equation EQUATION."
  (first equation))

(defun equation-rhs (equation)
  "Select the RHS of a unification equation EQUATION."
  (second equation))