unify.c
6.24 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
/* Unify.c *******************************************************************************
The Anubis Compiler.
Unification of types.
*****************************************************************************************/
#include "compil.h"
/* Environments are just A-lists ((v1 . T1) ...) where v_i are type unknowns and where T_i
are types. The environment just tells which type unknowns are already bound to
types. */
/* We use an auxiliary function */
static int unify_aux(Expr x, // first expression
Expr y , // second expression
Expr *env); // environment
/*
Note: In the Lips-like representation we have exceptional data which are not 'Expr's
but integers in C format: <Cint>. The functions below would not work if they encounter
a <Cint> (and probably would lead to a segmentation fault). However, since we are
unifying only types, not terms, we will never encounter a <Cint>. Anyway, this is not
very clean.
*/
/* 'depends_on' is used for circularity testing. It returns 1 if 'y' contains a reference
to 'x'. */
static int depends_on(Expr x, // x is an unknown
Expr y, // y is an expression
Expr env)
{
assert(is_unknown(x)); // only meaningful if 'x' is an unknown.
/* It is also assumed that 'x' is not a key of env. It is actually the case: check below
all calls to 'depends_on'. */
begin:
/* find if y contains the unknown x. This is relative to env: i.e. if y is an unknown
and y is bound in env, we must first replace y by its value. */
if (y == x) return 1;
if (is_unknown(y))
{
Expr yval = assoc(y,env);
if (yval != key_not_found)
{ /* replace y by its value */
y = yval;
goto begin; // and restart
}
}
if (!consp(y)) // y is a 'constant'
return 0;
else
{
if (depends_on(x,car(y),env))
return 1;
y = cdr(y);
goto begin;
}
}
/* Join two environments.
The two environments need not have the same keys, but they may have keys in common. The
result of the join will have all the keys from the two environments, but of course
without repetition.
So, the problem is just when they have a key in common. We unify thevalues of the two
keys. If they don't unify, the two environments are not joinable, and we return
'not_unifiable'.
*/
Expr join_envs(Expr e1, Expr e2)
{
Expr key, val, entry, val2;
while (consp(e1))
{
entry = car(e1);
key = car(entry);
val = cdr(entry);
e1 = cdr(e1);
/* if 'key' is not a key of e2, just add the entry to e2. Otherwise, if the values
of 'key' in e1 and e2 do not unify (with envs nil and e2), return
'not_unifiable'. If they unify, replace e2 by the result of this unification. */
val2 = assoc(key,e2);
if (val2 == key_not_found)
e2 = cons(entry,e2);
else
{
e2 = unify(val,nil,val2,e2);
if (e2 == not_unifiable)
{
return e2;
}
}
}
return e2;
}
/* interface to unification */
Expr /* returns a new environment */
_unify(Expr x, /* first expression to unify */
Expr ex, /* environment for first expression */
Expr y, /* second expression to unify */
Expr ey) /* environment for second expression */
{
Expr env, result;
int old_next_pair = next_pair;
/* the two environments must join together. I wonder if this case may actually
happen ? ? ? */
if ((env = join_envs(ex,ey)) == not_unifiable)
return env;
if (unify_aux(x,y,&env)) /* unify and record instanciations in env */
result = env;
else
{
next_pair = old_next_pair;
result = not_unifiable;
}
return result;
}
/* the unification itself */
static int unify_aux(Expr x,
Expr y,
Expr *env)
{
Expr aux;
begin:
/* dereference the aliases */
x = dereference_aliases(x);
y = dereference_aliases(y);
if (x == y)
return 1;
if (is_unknown(x))
{
Expr v = assoc(x,*env);
if (v == key_not_found)
{
/* x not instanciated */
/* pairs ($x . $y) in env must always satisfy $x > $y */
if (is_unknown(y) && x <= y)
{
/* exchange x and y, and try again */
aux = x;
x = y;
y = aux;
goto begin;
}
else
{
if (depends_on(x,y,*env))
return 0;
else
{
*env = cons(cons(x,y),*env);
return 1;
}
}
}
else
{
x = v;
goto begin;
}
}
if (is_unknown(y))
{
Expr v = assoc(y,*env);
if (v == key_not_found)
{
/* y not instanciated */
{
if (depends_on(y,x,*env))
return 0;
else
{
*env = cons(cons(y,x),*env);
return 1;
}
}
}
else
{
y = v;
goto begin;
}
}
if (!(consp(x) && consp(y)))
return 0;
/* now x and y are pairs */
if (!unify_aux(car(x),car(y),env))
return 0;
/* the two heads have unified */
/* A special action is needed if the two heads are 'forall_type'. We must rename the two
parameters so that they are identical. The simplest is to replace both by a fresh
system parameter. */
if (car(x) == forall_type) /* x = (forall_type <lc> <parm1> . <body1>)
y = (forall_type <lc> <parm2> . <body2>) */
{
Expr p = fresh_utvar();
x = substitute(cdr3(x),list1(cons(p,third(x))));
y = substitute(cdr3(y),list1(cons(p,third(y))));
}
else
{
x = cdr(x);
y = cdr(y);
}
goto begin;
}