;;;
;;; 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))