Wed Apr 15 10:05:58 UTC 2009  mantoniotti
  * Added some functionality and comments.
diff -rN -u old-cl-unification-1/apply-substitution.lisp new-cl-unification-1/apply-substitution.lisp
--- old-cl-unification-1/apply-substitution.lisp	2013-07-01 12:48:18.000000000 +0000
+++ new-cl-unification-1/apply-substitution.lisp	2013-07-01 12:48:18.000000000 +0000
@@ -9,28 +9,68 @@
 ;;;---------------------------------------------------------------------------
 ;;; Substitution application.
 
-(defgeneric apply-substitution (substitution item))
+;;; apply-substitution --
+;;;
+;;; EXCLUDE-VARS are variables that will just pass through (a list for
+;;; the time being).
 
+(defgeneric apply-substitution (substitution item &optional exclude-vars))
 
-(defmethod apply-substitution ((substitution environment) (s symbol))
+
+(defmethod apply-substitution ((substitution environment) (s symbol)
+                               &optional (exclude-vars ()))
+  (declare (type list exclude-vars))
   (cond ((variable-any-p s) s)
         ((variablep s)
-         (multiple-value-bind (val foundp)
-             (find-variable-value s substitution)
-           (cond (foundp val)
-                 (t (warn "~S is a free variable in the current environment."
-			  s)
-                    s))))
+         (if (member s exclude-vars :test #'eq)
+             s
+             (multiple-value-bind (val foundp)
+                 (find-variable-value s substitution)
+               (cond (foundp val)
+                     (t (warn "~S is a free variable in the current environment."
+                              s)
+                        s))))
+         )
         (t s)))
 
 
-(defmethod apply-substitution ((substitution environment) (l cons))
-  (cons (apply-substitution substitution (first l))
-        (apply-substitution substitution (rest l))))
+(defmethod apply-substitution ((substitution environment) (l cons)
+                               &optional (exclude-vars ()))
+  (declare (type list exclude-vars))
+  (cons (apply-substitution substitution (first l) exclude-vars)
+        (apply-substitution substitution (rest l) exclude-vars)))
+
 
-(defmethod apply-substitution ((substitution environment) (l null))
+(defmethod apply-substitution ((substitution environment) (l null)
+                               &optional exclude-vars)
+  (declare (ignore exclude-vars))
   '())
 
+
+;;; compose-substitions --
+;;; The definition is a direct translation of TPL's definition at page 318.
+;;; Usually these are done by directly composing and currying
+;;; functions in ML/Haskell derivatives, but that is just being "lazy".
+;;; The current definition may be too "eager", but the "correct"
+;;; semantics should be preserved.
+
+(defun compose-substitutions (env2 env1) ; note the order.
+  (declare (type environment env2 env1))
+
+  (loop for env1-frame in (environment-frames env1)
+        collect
+        (loop for (var . term) in (frame-bindings env1-frame)
+              collect (make-binding var (apply-substitution env2 term))
+              into result-bindings
+              finally (return (make-frame result-bindings)))
+        into frames
+        finally (return (make-environment :frames frames))))
+                      
+        
+
+
+;;; ground-term --
+
 (defun ground-term (term &optional (substitution (make-empty-environment)))
   (apply-substitution substitution term))