apply-substitution.lisp 2.8 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
;;;; -*- 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).

Marco Antoniotti's avatar
Marco Antoniotti committed
19 20
(defgeneric apply-substitution (substitution item &optional exclude-vars)
  (:documentation "Applies a SUBSTITUTION to an ITEM."))
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86


(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 --