Update of /project/cl-unification/cvsroot/cl-unification In directory cl-net:/tmp/cvs-serv26579

Modified Files: apply-substitution.lisp Log Message: Added some functionality and comments.

--- /project/cl-unification/cvsroot/cl-unification/apply-substitution.lisp 2008/07/10 17:39:16 1.2 +++ /project/cl-unification/cvsroot/cl-unification/apply-substitution.lisp 2009/04/15 10:05:58 1.3 @@ -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))