/
Substitutions.sv
232 lines (189 loc) · 8.35 KB
/
Substitutions.sv
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
grammar silver:compiler:definition:type;
{--
- A representation of: (1) tyvar->type substitutions. (2) success/failure of unification
-
- History note: This code was written before Silver had polymorphism (it is
- what gave Silver polymorphism!) and so is incredibly archaic.
-
- TODO: Separate success/failure of unification from this type.
- Consider unify returning Maybe<Substitution> or Pair<Boolean Substitution> depending.
- TODO: More efficient type representations than a assoc-list, somehow.
-}
data nonterminal Substitution with substList, substErrors, failure;
synthesized attribute substList :: [Pair<TyVar Type>];
synthesized attribute substErrors :: [String];
synthesized attribute failure :: Boolean; -- this is a bad hack to work around unify being unable to return a pair
--------------------------------------------------------------------------------
abstract production goodSubst
top::Substitution ::= sublst::[Pair<TyVar Type>]
{
top.substList = sublst;
top.substErrors = [];
top.failure = false;
}
abstract production badSubst
top::Substitution ::= sublst::[Pair<TyVar Type>] errs::[String]
{
top.substList = sublst;
top.substErrors = errs;
top.failure = true;
}
fun emptySubst Substitution ::= = goodSubst([]);
fun errorSubst Substitution ::= e::String = badSubst([], [e]);
fun subst Substitution ::= tv::TyVar te::Type = goodSubst([(tv,te)]);
fun composeSubst Substitution ::= s1::Substitution s2::Substitution =
case s1, s2 of
| goodSubst(s1l), goodSubst(s2l) -> goodSubst(s1l ++ s2l)
| goodSubst(s1l), badSubst(s2l, s2e) -> badSubst(s1l ++ s2l, s2e)
| badSubst(s1l, s1e), goodSubst(s2l) -> badSubst(s1l ++ s2l, s1e)
| badSubst(s1l, s1e), badSubst(s2l, s2e) -> badSubst(s1l ++ s2l, s1e ++ s2e)
end;
fun ignoreFailure Substitution ::= s::Substitution =
case s of
| goodSubst(_) -> s
| badSubst(sl,_) -> goodSubst(sl)
end;
--------------------------------------------------------------------------------
fun findSubst Maybe<Type> ::= tv::TyVar s::Substitution = lookup(tv, s.substList);
--------------------------------------------------------------------------------
-- These are for ordinary tyvar substitutions.
inherited attribute substitution :: Substitution occurs on Context, Type;
functor attribute substituted occurs on Context, Type;
-- These are for flat, non-recursive replacement of tyvars with something else directly
functor attribute flatRenamed occurs on Context, Type;
propagate substitution on Context, Type;
propagate substituted, flatRenamed on Context, Type
excluding inhOccursContext, synOccursContext, annoOccursContext, varType, skolemType, ntOrDecType;
aspect production inhOccursContext
top::Context ::= attr::String args::[Type] atty::Type ntty::Type
{
top.substituted = inhOccursContext(attr, map(performSubstitution(_, top.substitution), args), atty.substituted, ntty.substituted);
top.flatRenamed = inhOccursContext(attr, map(performRenaming(_, top.substitution), args), atty.flatRenamed, ntty.flatRenamed);
}
aspect production synOccursContext
top::Context ::= attr::String args::[Type] atty::Type inhs::Type ntty::Type
{
top.substituted = synOccursContext(attr, map(performSubstitution(_, top.substitution), args), atty.substituted, inhs.substituted, ntty.substituted);
top.flatRenamed = synOccursContext(attr, map(performRenaming(_, top.substitution), args), atty.flatRenamed, inhs.flatRenamed, ntty.flatRenamed);
}
aspect production annoOccursContext
top::Context ::= attr::String args::[Type] atty::Type ntty::Type
{
top.substituted = annoOccursContext(attr, map(performSubstitution(_, top.substitution), args), atty.substituted, ntty.substituted);
top.flatRenamed = annoOccursContext(attr, map(performRenaming(_, top.substitution), args), atty.flatRenamed, ntty.flatRenamed);
}
aspect production varType
top::Type ::= tv::TyVar
{
-- Important: we recursively substitute, until no more substitutions happen!
-- This also means the substitution list must not be circular!
-- Perform one iteration of substitution
local partialsubst :: Maybe<Type> =
case findSubst(tv, top.substitution) of
| just(s) when s.kindrep != tv.kind -> error("Kind mismatch in applying substitution!")
| ps -> ps
end;
-- recursively substitute only if we changed!
top.substituted =
if partialsubst.isJust
then performSubstitution(partialsubst.fromJust, top.substitution)
else new(top);
top.flatRenamed =
if partialsubst.isJust
then partialsubst.fromJust
else new(top);
}
aspect production skolemType
top::Type ::= tv::TyVar
{
-- This may be counter intuitive! I don't know!
-- I'm allowing Skolem constants to be subtituted for.
-- Now, the "real" behavior of Skolem constants is all in unification:
-- there, they behave as you would expect. However, once we quantify over the
-- "Skolem constant type variables", they should sort of go back to behaving
-- like ordinary type variables. So to get this behavior, we allow them to be
-- substituted.
-- The only way we can construct a substitution for one though is by non-unification
-- means. (And there's only one way to do that: by quantifying over it.)
-- (See the only non-unification place where subst(...) is called directly at the bottom of this file.)
local partialsubst :: Maybe<Type> =
case findSubst(tv, top.substitution) of
| just(s) when s.kindrep != tv.kind -> nothing()
| ps -> ps
end;
-- recursively substitute only if we changed!
top.substituted =
if partialsubst.isJust
then performSubstitution(partialsubst.fromJust, top.substitution)
else new(top);
top.flatRenamed =
if partialsubst.isJust
then partialsubst.fromJust
else new(top);
}
aspect production ntOrDecType
top::Type ::= nt::Type inhs::Type hidden::Type
{
-- We rely very carefully on eliminating ourselves once we've specialized!
-- Note: we're matching on hidden.subsituted, not just hidden. Important!
top.substituted =
case hidden.substituted of
| varType(_) -> ntOrDecType(nt.substituted, inhs.substituted, hidden.substituted)
| _ -> hidden.substituted
end;
-- For a renaming, we don't need to specialize.
propagate substitution, flatRenamed;
}
--------------------------------------------------------------------------------
function performContextSubstitution
Context ::= c::Context s::Substitution
{
c.substitution = s;
return c.substituted;
}
function performSubstitution
Type ::= te::Type s::Substitution
{
te.substitution = s;
return te.substituted;
}
fun mapSubst [Type] ::= tes::[Type] s::Substitution = map(performSubstitution(_, s), tes);
----
function performContextRenaming
Context ::= c::Context s::Substitution
{
c.substitution = s;
return c.flatRenamed;
}
function performRenaming
Type ::= te::Type s::Substitution
{
te.substitution = s;
return te.flatRenamed;
}
fun mapRenameSubst [Type] ::= tes::[Type] s::Substitution = map(performRenaming(_, s), tes);
--------------------------------------------------------------------------------
-- Generate fresh type vars with the same kinds as tvs
fun freshTyVars [TyVar] ::= tvs::[TyVar] = map(freshTyVar, map((.kind), tvs));
fun zipVarsIntoSubstitution Substitution ::= original::[TyVar] sub::[TyVar] =
if null(original) || null(sub) then emptySubst()
else composeSubst(subst(head(original), varType(head(sub))),
zipVarsIntoSubstitution(tail(original), tail(sub)));
fun zipVarsIntoSkolemizedSubstitution Substitution ::= original::[TyVar] sub::[TyVar] =
if null(original) || null(sub) then emptySubst()
else composeSubst(subst(head(original), skolemType(head(sub))),
zipVarsIntoSkolemizedSubstitution(tail(original), tail(sub)));
fun zipVarsAndTypesIntoSubstitution Substitution ::= original::[TyVar] sub::[Type] =
if null(original) || null(sub) then emptySubst()
else composeSubst(subst(head(original), head(sub)),
zipVarsAndTypesIntoSubstitution(tail(original), tail(sub)));
fun freshenType Type ::= te::Type tvs::[TyVar] = freshenTypeWith(te, tvs, freshTyVars(tvs));
fun freshenContextWith Context ::= c::Context tvs::[TyVar] ntvs::[TyVar] =
performContextRenaming(c, zipVarsIntoSubstitution(tvs, ntvs));
fun freshenTypeWith Type ::= te::Type tvs::[TyVar] ntvs::[TyVar] =
performRenaming(te, zipVarsIntoSubstitution(tvs, ntvs));
function errorSubstitution
Substitution ::= t::Type
{
return zipVarsAndTypesIntoSubstitution(t.freeVariables, repeat(errorType(), length(t.freeVariables)));
}