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