/
apply-substitution.lisp
 1 ;;;; -*- Mode: Lisp -*-
 2 
 3 ;;;; apply-substitutions.lisp --
 4 ;;;; General CL structures unifier.
 5 ;;;; Substitution definitions.
 6 ;;;;
 7 ;;;; See the file COPYING for copyright and licensing information.
 8 
 9 (in-package "CL.EXT.DACF.UNIFICATION") ; DACF = Data And Control Flow.
10 
11 ;;;---------------------------------------------------------------------------
12 ;;; Substitution application.
13 
14 ;;; apply-substitution --
15 ;;;
16 ;;; EXCLUDE-VARS are variables that will just pass through (a list for
17 ;;; the time being).
18 
19 (defgeneric apply-substitution (substitution item &optional exclude-vars))
20 
21 
22 (defmethod apply-substitution ((s environment) (n number) &optional exclude-vars)
23   (declare (ignore exclude-vars))
24   n)
25 
26 
27 (defmethod apply-substitution ((substitution environment) (s symbol)
28                                &optional (exclude-vars ()))
29   (declare (type list exclude-vars))
30   (cond ((variable-any-p s) s)
31         ((variablep s)
32          (if (member s exclude-vars :test #'eq)
33              s
34              (multiple-value-bind (val foundp)
35                  (find-variable-value s substitution)
36                (cond (foundp (apply-substitution substitution val exclude-vars))
37                      (t (warn "~S is a free variable in the current environment."
38                               s)
39                         s))))
40          )
41         (t s)))
42 
43 
44 (defmethod apply-substitution ((substitution environment) (l cons)
45                                &optional (exclude-vars ()))
46   (declare (type list exclude-vars))
47   (cons (apply-substitution substitution (first l) exclude-vars)
48         (apply-substitution substitution (rest l) exclude-vars)))
49 
50 
51 (defmethod apply-substitution ((substitution environment) (l null)
52                                &optional exclude-vars)
53   (declare (ignore exclude-vars))
54   '())
55 
56 
57 ;;; compose-substitions --
58 ;;; The definition is a direct translation of TPL's definition at page 318.
59 ;;; Usually these are done by directly composing and currying
60 ;;; functions in ML/Haskell derivatives, but that is just being "lazy".
61 ;;; The current definition may be too "eager", but the "correct"
62 ;;; semantics should be preserved.
63 
64 (defun compose-substitutions (env2 env1) ; note the order.
65   (declare (type environment env2 env1))
66 
67   (loop for env1-frame in (environment-frames env1)
68         collect
69         (loop for (var . term) in (frame-bindings env1-frame)
70               collect (make-binding var (apply-substitution env2 term))
71               into result-bindings
72               finally (return (make-frame result-bindings)))
73         into frames
74         finally (return (make-environment :frames frames))))
75 
76 
77 
78 
79 ;;; ground-term --
80 
81 (defun ground-term (term &optional (substitution (make-empty-environment)))
82   (apply-substitution substitution term))
83 
84 
85 ;;;; end of file -- apply-substitutions.lisp --