repos
/
cl-unification
/ annotate_shade
summary
|
shortlog
|
log
|
tree
|
commit
|
commitdiff
|
headdiff
|
annotate
|
headblob
|
headfilediff
|
filehistory
normal
|
plain
|
shade
|
zebra
Minor changes (added COPYING information and other minutiae).
Annotate for file /apply-substitution.lisp
2011-04-02 mantoniotti
1
;;;; -*- Mode: Lisp -*-
2004-11-17 mantoniotti
2
2011-04-02 mantoniotti
3
;;;; apply-substitutions.lisp --
04:05:18 '
4
;;;; General CL structures unifier.
'
5
;;;; Substitution definitions.
'
6
;;;;
'
7
;;;; See the file COPYING for copyright and licensing information.
2004-11-17 mantoniotti
8
22:19:54 '
9
(in-package "CL.EXT.DACF.UNIFICATION") ; DACF = Data And Control Flow.
'
10
'
11
;;;---------------------------------------------------------------------------
'
12
;;; Substitution application.
'
13
2009-04-15 mantoniotti
14
;;; apply-substitution --
10:05:58 '
15
;;;
'
16
;;; EXCLUDE-VARS are variables that will just pass through (a list for
'
17
;;; the time being).
2004-11-17 mantoniotti
18
2009-04-15 mantoniotti
19
(defgeneric apply-substitution (substitution item &optional exclude-vars))
2004-11-17 mantoniotti
20
2009-04-15 mantoniotti
21
2009-04-17 mantoniotti
22
(defmethod apply-substitution ((s environment) (n number) &optional exclude-vars)
07:52:25 '
23
(declare (ignore exclude-vars))
'
24
n)
'
25
'
26
2009-04-15 mantoniotti
27
(defmethod apply-substitution ((substitution environment) (s symbol)
10:05:58 '
28
&optional (exclude-vars ()))
'
29
(declare (type list exclude-vars))
2004-11-17 mantoniotti
30
(cond ((variable-any-p s) s)
22:19:54 '
31
((variablep s)
2009-04-15 mantoniotti
32
(if (member s exclude-vars :test #'eq)
10:05:58 '
33
s
'
34
(multiple-value-bind (val foundp)
'
35
(find-variable-value s substitution)
2009-04-17 mantoniotti
36
(cond (foundp (apply-substitution substitution val exclude-vars))
2009-04-15 mantoniotti
37
(t (warn "~S is a free variable in the current environment."
10:05:58 '
38
s)
'
39
s))))
'
40
)
2004-11-17 mantoniotti
41
(t s)))
22:19:54 '
42
'
43
2009-04-15 mantoniotti
44
(defmethod apply-substitution ((substitution environment) (l cons)
10:05:58 '
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
2004-11-17 mantoniotti
50
2009-04-15 mantoniotti
51
(defmethod apply-substitution ((substitution environment) (l null)
10:05:58 '
52
&optional exclude-vars)
'
53
(declare (ignore exclude-vars))
2004-11-17 mantoniotti
54
'())
22:19:54 '
55
2009-04-15 mantoniotti
56
10:05:58 '
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))))
2011-04-02 rbrown
75
03:50:19 '
76
2009-04-15 mantoniotti
77
10:05:58 '
78
'
79
;;; ground-term --
'
80
2004-11-17 mantoniotti
81
(defun ground-term (term &optional (substitution (make-empty-environment)))
22:19:54 '
82
(apply-substitution substitution term))
'
83
'
84
2011-04-02 mantoniotti
85
;;;; end of file -- apply-substitutions.lisp --