;;;; -*- Mode: Lisp -*-
;;;; apply-substitutions.lisp --
;;;; General CL structures unifier.
;;;; Substitution definitions.
;;;;
;;;; See the file COPYING for copyright and licensing information.
(in-package "CL.EXT.DACF.UNIFICATION") ; DACF = Data And Control Flow.
;;;---------------------------------------------------------------------------
;;; Substitution application.
;;; 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)
(:documentation "Applies a SUBSTITUTION to an ITEM."))
(defmethod apply-substitution ((s environment) (n number) &optional exclude-vars)
(declare (ignore exclude-vars))
n)
(defmethod apply-substitution ((substitution environment) (s symbol)
&optional (exclude-vars ()))
(declare (type list exclude-vars))
(cond ((variable-any-p s) s)
((variablep s)
(if (member s exclude-vars :test #'eq)
s
(multiple-value-bind (val foundp)
(find-variable-value s substitution)
(cond (foundp (apply-substitution substitution val exclude-vars))
(t (warn "~S is a free variable in the current environment."
s)
s))))
)
(t s)))
(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)
&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))
;;;; end of file -- apply-substitutions.lisp --