1 : |
jhr |
69 |
(* typechecker.sml
|
2 : |
|
|
*
|
3 : |
jhr |
2149 |
* COPYRIGHT (c) 2013 The Diderot Project (http://diderot-language.cs.uchicago.edu)
|
4 : |
jhr |
69 |
* All rights reserved.
|
5 : |
jhr |
228 |
*
|
6 : |
jhr |
1116 |
* TODO:
|
7 : |
jhr |
2149 |
* check for unreachable code and prune it (see simplify/simplify.sml)
|
8 : |
|
|
* error recovery so that we can detect multiple errors in a single compile
|
9 : |
|
|
* check that functions have a return on all paths
|
10 : |
jhr |
2151 |
* check that the args of strand creation have the same type and number as the params
|
11 : |
jhr |
69 |
*)
|
12 : |
|
|
|
13 : |
|
|
structure Typechecker : sig
|
14 : |
|
|
|
15 : |
jhr |
86 |
val check : Error.err_stream -> ParseTree.program -> AST.program
|
16 : |
jhr |
69 |
|
17 : |
|
|
end = struct
|
18 : |
|
|
|
19 : |
jhr |
1116 |
structure BV = BasisVars
|
20 : |
jhr |
70 |
structure PT = ParseTree
|
21 : |
jhr |
69 |
structure Ty = Types
|
22 : |
jhr |
96 |
structure TU = TypeUtil
|
23 : |
jhr |
81 |
structure U = Util
|
24 : |
jhr |
69 |
|
25 : |
jhr |
2149 |
(* exception to abort typechecking when we hit an error. Eventually, we should continue
|
26 : |
|
|
* checking for more errors and not use this.
|
27 : |
|
|
*)
|
28 : |
|
|
exception TypeError
|
29 : |
|
|
|
30 : |
jhr |
2133 |
datatype scope
|
31 : |
|
|
= GlobalScope
|
32 : |
|
|
| FunctionScope of Ty.ty
|
33 : |
|
|
| StrandScope
|
34 : |
|
|
| MethodScope
|
35 : |
|
|
| InitScope
|
36 : |
jhr |
169 |
|
37 : |
jhr |
1116 |
type env = {
|
38 : |
|
|
scope : scope,
|
39 : |
|
|
bindings : Error.location AtomMap.map,
|
40 : |
|
|
env : Env.env
|
41 : |
|
|
}
|
42 : |
jhr |
228 |
|
43 : |
jhr |
1116 |
type context = Error.err_stream * Error.span
|
44 : |
jhr |
228 |
|
45 : |
jhr |
1116 |
(* start a new scope *)
|
46 : |
jhr |
2133 |
(* QUESTION: do we want to restrict access to globals from a function? *)
|
47 : |
|
|
fun functionScope ({scope, bindings, env}, ty) =
|
48 : |
jhr |
2149 |
{scope=FunctionScope ty, bindings=AtomMap.empty, env=env}
|
49 : |
jhr |
1116 |
fun strandScope {scope, bindings, env} =
|
50 : |
|
|
{scope=StrandScope, bindings=AtomMap.empty, env=env}
|
51 : |
|
|
fun methodScope {scope, bindings, env} =
|
52 : |
|
|
{scope=MethodScope, bindings=AtomMap.empty, env=env}
|
53 : |
|
|
fun initScope {scope, bindings, env} =
|
54 : |
|
|
{scope=InitScope, bindings=AtomMap.empty, env=env}
|
55 : |
|
|
fun blockScope {scope, bindings, env} =
|
56 : |
|
|
{scope=scope, bindings=AtomMap.empty, env=env}
|
57 : |
|
|
|
58 : |
|
|
fun inStrand {scope=StrandScope, bindings, env} = true
|
59 : |
jhr |
511 |
| inStrand {scope=MethodScope, ...} = true
|
60 : |
|
|
| inStrand _ = false
|
61 : |
jhr |
228 |
|
62 : |
jhr |
2133 |
fun insertFunc ({scope, bindings, env}, cxt, f, f') = {
|
63 : |
|
|
scope=scope,
|
64 : |
|
|
bindings = AtomMap.insert(bindings, f, Error.location cxt),
|
65 : |
|
|
env=Env.insertFunc(env, f, Env.UserFun f')
|
66 : |
|
|
}
|
67 : |
jhr |
1116 |
fun insertLocal ({scope, bindings, env}, cxt, x, x') = {
|
68 : |
|
|
scope=scope,
|
69 : |
|
|
bindings = AtomMap.insert(bindings, x, Error.location cxt),
|
70 : |
|
|
env=Env.insertLocal(env, x, x')
|
71 : |
|
|
}
|
72 : |
|
|
fun insertGlobal ({scope, bindings, env}, cxt, x, x') = {
|
73 : |
|
|
scope=scope,
|
74 : |
|
|
bindings = AtomMap.insert(bindings, x, Error.location cxt),
|
75 : |
|
|
env=Env.insertGlobal(env, x, x')
|
76 : |
|
|
}
|
77 : |
jhr |
228 |
|
78 : |
jhr |
86 |
fun withContext ((errStrm, _), {span, tree}) =
|
79 : |
|
|
((errStrm, span), tree)
|
80 : |
|
|
fun withEnvAndContext (env, (errStrm, _), {span, tree}) =
|
81 : |
|
|
(env, (errStrm, span), tree)
|
82 : |
|
|
|
83 : |
jhr |
88 |
fun error ((errStrm, span), msg) = (
|
84 : |
|
|
Error.errorAt(errStrm, span, msg);
|
85 : |
jhr |
2149 |
raise TypeError)
|
86 : |
jhr |
86 |
|
87 : |
jhr |
88 |
datatype token
|
88 : |
|
|
= S of string | A of Atom.atom
|
89 : |
|
|
| V of AST.var | TY of Types.ty | TYS of Types.ty list
|
90 : |
|
|
|
91 : |
jhr |
1925 |
fun tysToString tys = String.concat[
|
92 : |
|
|
"(", String.concatWith " * " (List.map TU.toString tys), ")"
|
93 : |
|
|
]
|
94 : |
|
|
|
95 : |
jhr |
88 |
fun err (cxt, toks) = let
|
96 : |
|
|
fun tok2str (S s) = s
|
97 : |
jhr |
2050 |
| tok2str (A a) = concat["'", Atom.toString a, "'"]
|
98 : |
|
|
| tok2str (V x) = concat["'", Var.nameOf x, "'"]
|
99 : |
jhr |
96 |
| tok2str (TY ty) = TU.toString ty
|
100 : |
jhr |
88 |
| tok2str (TYS []) = "()"
|
101 : |
jhr |
96 |
| tok2str (TYS[ty]) = TU.toString ty
|
102 : |
jhr |
1925 |
| tok2str (TYS tys) = tysToString tys
|
103 : |
jhr |
88 |
in
|
104 : |
|
|
error(cxt, List.map tok2str toks)
|
105 : |
|
|
end
|
106 : |
|
|
|
107 : |
jhr |
1116 |
fun checkForRedef (env : env, cxt : context, x) = (case AtomMap.find(#bindings env,x)
|
108 : |
|
|
of SOME loc => err (cxt, [
|
109 : |
|
|
S "redefinition of ", A x, S ", previous definition at ",
|
110 : |
|
|
S(Error.locToString loc)
|
111 : |
|
|
])
|
112 : |
|
|
| NONE => ()
|
113 : |
|
|
(* end case *))
|
114 : |
|
|
|
115 : |
jhr |
83 |
val realZero = AST.E_Lit(Literal.Float(FloatLit.zero true))
|
116 : |
|
|
|
117 : |
jhr |
2149 |
(* check a differentiation level, which must be >= 0 *)
|
118 : |
jhr |
70 |
fun checkDiff (cxt, k) =
|
119 : |
|
|
if (k < 0)
|
120 : |
jhr |
1116 |
then err (cxt, [S "differentiation must be >= 0"])
|
121 : |
jhr |
75 |
else Ty.DiffConst(IntInf.toInt k)
|
122 : |
jhr |
70 |
|
123 : |
jhr |
2134 |
(* check a sequence dimension, which must be > 0 *)
|
124 : |
|
|
fun checkSeqDim (cxt, d) =
|
125 : |
|
|
if (d < 0)
|
126 : |
|
|
then err (cxt, [S "invalid dimension; must be positive"])
|
127 : |
|
|
else Ty.DimConst(IntInf.toInt d)
|
128 : |
|
|
|
129 : |
jhr |
1116 |
(* check a dimension, which must be 1, 2 or 3 *)
|
130 : |
jhr |
70 |
fun checkDim (cxt, d) =
|
131 : |
jhr |
1116 |
if (d < 1) orelse (3 < d)
|
132 : |
|
|
then err (cxt, [S "invalid dimension; must be 1, 2, or 3"])
|
133 : |
jhr |
75 |
else Ty.DimConst(IntInf.toInt d)
|
134 : |
jhr |
70 |
|
135 : |
|
|
(* check a shape *)
|
136 : |
jhr |
1116 |
fun checkShape (cxt, shape) = let
|
137 : |
|
|
fun checkDim d =
|
138 : |
|
|
if (d <= 1)
|
139 : |
|
|
then err (cxt, [S "invalid tensor-shape dimension; must be > 1"])
|
140 : |
|
|
else Ty.DimConst(IntInf.toInt d)
|
141 : |
jhr |
70 |
in
|
142 : |
jhr |
1116 |
Ty.Shape(List.map checkDim shape)
|
143 : |
jhr |
70 |
end
|
144 : |
|
|
|
145 : |
jhr |
69 |
(* check the well-formedness of a type and translate it to an AST type *)
|
146 : |
jhr |
70 |
fun checkTy (cxt, ty) = (case ty
|
147 : |
jhr |
86 |
of PT.T_Mark m => checkTy(withContext(cxt, m))
|
148 : |
jhr |
70 |
| PT.T_Bool => Ty.T_Bool
|
149 : |
|
|
| PT.T_Int => Ty.T_Int
|
150 : |
|
|
| PT.T_Real => Ty.realTy
|
151 : |
|
|
| PT.T_String => Ty.T_String
|
152 : |
|
|
| PT.T_Vec n => (* NOTE: the parser guarantees that 2 <= n <= 4 *)
|
153 : |
|
|
Ty.vecTy(IntInf.toInt n)
|
154 : |
|
|
| PT.T_Kernel k => Ty.T_Kernel(checkDiff(cxt, k))
|
155 : |
|
|
| PT.T_Field{diff, dim, shape} => Ty.T_Field{
|
156 : |
|
|
diff = checkDiff (cxt, diff),
|
157 : |
|
|
dim = checkDim (cxt, dim),
|
158 : |
|
|
shape = checkShape (cxt, shape)
|
159 : |
|
|
}
|
160 : |
|
|
| PT.T_Tensor shape => Ty.T_Tensor(checkShape(cxt, shape))
|
161 : |
|
|
| PT.T_Image{dim, shape} => Ty.T_Image{
|
162 : |
|
|
dim = checkDim (cxt, dim),
|
163 : |
|
|
shape = checkShape (cxt, shape)
|
164 : |
|
|
}
|
165 : |
jhr |
1640 |
| PT.T_Seq(ty, dim) => let
|
166 : |
|
|
val ty = checkTy(cxt, ty)
|
167 : |
|
|
in
|
168 : |
jhr |
1687 |
if TU.isFixedSizeType ty
|
169 : |
jhr |
2134 |
then Ty.T_Sequence(ty, checkSeqDim (cxt, dim))
|
170 : |
jhr |
1687 |
else err(cxt, [S "elements of sequence types must be fixed-size types"])
|
171 : |
jhr |
1640 |
end
|
172 : |
jhr |
1687 |
| PT.T_DynSeq ty => let
|
173 : |
|
|
val ty = checkTy(cxt, ty)
|
174 : |
|
|
in
|
175 : |
|
|
if TU.isFixedSizeType ty
|
176 : |
|
|
then Ty.T_DynSequence(ty)
|
177 : |
|
|
else err(cxt, [S "elements of sequence types must be fixed-size types"])
|
178 : |
|
|
end
|
179 : |
jhr |
69 |
(* end case *))
|
180 : |
|
|
|
181 : |
jhr |
71 |
fun checkLit lit = (case lit
|
182 : |
|
|
of (Literal.Int _) => (AST.E_Lit lit, Ty.T_Int)
|
183 : |
|
|
| (Literal.Float _) => (AST.E_Lit lit, Ty.realTy)
|
184 : |
|
|
| (Literal.String s) => (AST.E_Lit lit, Ty.T_String)
|
185 : |
|
|
| (Literal.Bool _) => (AST.E_Lit lit, Ty.T_Bool)
|
186 : |
|
|
(* end case *))
|
187 : |
|
|
|
188 : |
jhr |
2117 |
fun coerceExp (Ty.T_Tensor(Ty.Shape[]), Ty.T_Int, AST.E_Lit(Literal.Int n)) =
|
189 : |
|
|
AST.E_Lit(Literal.Float(FloatLit.fromInt n))
|
190 : |
|
|
| coerceExp (ty1, ty2, e) = AST.E_Coerce{srcTy=ty2, dstTy=ty1, e=e}
|
191 : |
|
|
|
192 : |
jhr |
2133 |
fun coerceType (dstTy, srcTy, e) = (case U.matchType(dstTy, srcTy)
|
193 : |
jhr |
1971 |
of U.EQ => SOME e
|
194 : |
jhr |
2133 |
| U.COERCE => SOME(coerceExp (dstTy, srcTy, e))
|
195 : |
jhr |
1971 |
| U.FAIL => NONE
|
196 : |
|
|
(* end case *))
|
197 : |
|
|
|
198 : |
|
|
fun realType (ty as Ty.T_Tensor(Ty.Shape[])) = ty
|
199 : |
|
|
| realType (ty as Ty.T_Int) = Ty.realTy
|
200 : |
|
|
| realType ty = ty
|
201 : |
|
|
|
202 : |
jhr |
85 |
(* resolve overloading: we use a simple scheme that selects the first operator in the
|
203 : |
|
|
* list that matches the argument types.
|
204 : |
|
|
*)
|
205 : |
jhr |
1116 |
fun resolveOverload (_, rator, _, _, []) = raise Fail(concat[
|
206 : |
|
|
"resolveOverload: \"", Atom.toString rator, "\" has no candidates"
|
207 : |
|
|
])
|
208 : |
|
|
| resolveOverload (cxt, rator, argTys, args, candidates) = let
|
209 : |
jhr |
1971 |
(* FIXME: we could be more efficient by just checking for coercion matchs the first pass
|
210 : |
|
|
* and remembering those that are not pure EQ matches.
|
211 : |
|
|
*)
|
212 : |
|
|
(* try to match candidates while allowing type coercions *)
|
213 : |
|
|
fun tryMatchCandidates [] = err(cxt, [
|
214 : |
jhr |
91 |
S "unable to resolve overloaded operator \"", A rator, S "\"\n",
|
215 : |
|
|
S " argument type is: ", TYS argTys, S "\n"
|
216 : |
jhr |
85 |
])
|
217 : |
jhr |
1971 |
| tryMatchCandidates (x::xs) = let
|
218 : |
|
|
val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf x)
|
219 : |
|
|
in
|
220 : |
jhr |
1973 |
case U.tryMatchArgs (domTy, args, argTys)
|
221 : |
|
|
of SOME args' => (AST.E_Apply(x, tyArgs, args', rngTy), rngTy)
|
222 : |
|
|
| NONE => tryMatchCandidates xs
|
223 : |
|
|
(* end case *)
|
224 : |
jhr |
1971 |
end
|
225 : |
|
|
fun tryCandidates [] = tryMatchCandidates candidates
|
226 : |
jhr |
85 |
| tryCandidates (x::xs) = let
|
227 : |
|
|
val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf x)
|
228 : |
|
|
in
|
229 : |
jhr |
1971 |
if U.tryEqualTypes(domTy, argTys)
|
230 : |
jhr |
85 |
then (AST.E_Apply(x, tyArgs, args, rngTy), rngTy)
|
231 : |
|
|
else tryCandidates xs
|
232 : |
|
|
end
|
233 : |
|
|
in
|
234 : |
|
|
tryCandidates candidates
|
235 : |
|
|
end
|
236 : |
|
|
|
237 : |
jhr |
70 |
(* typecheck an expression and translate it to AST *)
|
238 : |
jhr |
169 |
fun checkExpr (env : env, cxt, e) = (case e
|
239 : |
jhr |
86 |
of PT.E_Mark m => checkExpr (withEnvAndContext (env, cxt, m))
|
240 : |
jhr |
169 |
| PT.E_Var x => (case Env.findVar (#env env, x)
|
241 : |
jhr |
171 |
of SOME x' => (AST.E_Var x', Var.monoTypeOf x')
|
242 : |
jhr |
88 |
| NONE => err(cxt, [S "undeclared variable ", A x])
|
243 : |
jhr |
71 |
(* end case *))
|
244 : |
|
|
| PT.E_Lit lit => checkLit lit
|
245 : |
jhr |
81 |
| PT.E_OrElse(e1, e2) => let
|
246 : |
|
|
val (e1', ty1) = checkExpr(env, cxt, e1)
|
247 : |
|
|
val (e2', ty2) = checkExpr(env, cxt, e2)
|
248 : |
|
|
in
|
249 : |
|
|
case (ty1, ty2)
|
250 : |
|
|
of (Ty.T_Bool, Ty.T_Bool) =>
|
251 : |
jhr |
416 |
(AST.E_Cond(e1', AST.E_Lit(Literal.Bool true), e2', Ty.T_Bool), Ty.T_Bool)
|
252 : |
jhr |
99 |
| _ => err (cxt, [S "arguments to \"||\" must have bool type"])
|
253 : |
jhr |
81 |
(* end case *)
|
254 : |
|
|
end
|
255 : |
|
|
| PT.E_AndAlso(e1, e2) => let
|
256 : |
|
|
val (e1', ty1) = checkExpr(env, cxt, e1)
|
257 : |
|
|
val (e2', ty2) = checkExpr(env, cxt, e2)
|
258 : |
|
|
in
|
259 : |
|
|
case (ty1, ty2)
|
260 : |
|
|
of (Ty.T_Bool, Ty.T_Bool) =>
|
261 : |
jhr |
416 |
(AST.E_Cond(e1', e2', AST.E_Lit(Literal.Bool false), Ty.T_Bool), Ty.T_Bool)
|
262 : |
jhr |
99 |
| _ => err (cxt, [S "arguments to \"&&\" must have bool type"])
|
263 : |
jhr |
81 |
(* end case *)
|
264 : |
|
|
end
|
265 : |
jhr |
370 |
| PT.E_Cond(e1, cond, e2) => let
|
266 : |
|
|
val (e1', ty1) = checkExpr(env, cxt, e1)
|
267 : |
|
|
val (e2', ty2) = checkExpr(env, cxt, e2)
|
268 : |
|
|
in
|
269 : |
|
|
case checkExpr(env, cxt, cond)
|
270 : |
|
|
of (cond', Ty.T_Bool) =>
|
271 : |
jhr |
1687 |
if U.equalType(ty1, ty2)
|
272 : |
jhr |
416 |
then (AST.E_Cond(cond', e1', e2', ty1), ty1)
|
273 : |
jhr |
370 |
else err (cxt, [
|
274 : |
jhr |
2133 |
S "types do not match in conditional expression\n",
|
275 : |
jhr |
1116 |
S " true branch: ", TY ty1, S "\n",
|
276 : |
jhr |
370 |
S " false branch: ", TY ty2
|
277 : |
|
|
])
|
278 : |
|
|
| (_, ty') => err (cxt, [S "expected bool type, but found ", TY ty'])
|
279 : |
|
|
(* end case *)
|
280 : |
|
|
end
|
281 : |
jhr |
81 |
| PT.E_BinOp(e1, rator, e2) => let
|
282 : |
|
|
val (e1', ty1) = checkExpr(env, cxt, e1)
|
283 : |
|
|
val (e2', ty2) = checkExpr(env, cxt, e2)
|
284 : |
|
|
in
|
285 : |
jhr |
1116 |
if Atom.same(rator, BasisNames.op_dot)
|
286 : |
|
|
(* we have to handle inner product as a special case, because out type
|
287 : |
|
|
* system cannot express the constraint that the type is
|
288 : |
|
|
* ALL[sigma1, d1, sigma2] . tensor[sigma1, d1] * tensor[d1, sigma2] -> tensor[sigma1, sigma2]
|
289 : |
|
|
*)
|
290 : |
|
|
then (case (TU.prune ty1, TU.prune ty2)
|
291 : |
|
|
of (Ty.T_Tensor(s1 as Ty.Shape(dd1 as _::_)), Ty.T_Tensor(s2 as Ty.Shape(d2::dd2))) => let
|
292 : |
|
|
val (dd1, d1) = let
|
293 : |
|
|
fun splitLast (prefix, [d]) = (List.rev prefix, d)
|
294 : |
|
|
| splitLast (prefix, d::dd) = splitLast (d::prefix, dd)
|
295 : |
|
|
| splitLast (_, []) = raise Fail "impossible"
|
296 : |
|
|
in
|
297 : |
|
|
splitLast ([], dd1)
|
298 : |
|
|
end
|
299 : |
|
|
val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_inner)
|
300 : |
|
|
val resTy = Ty.T_Tensor(Ty.Shape(dd1@dd2))
|
301 : |
|
|
in
|
302 : |
jhr |
1687 |
if U.equalDim(d1, d2)
|
303 : |
|
|
andalso U.equalTypes(domTy, [ty1, ty2])
|
304 : |
|
|
andalso U.equalType(rngTy, resTy)
|
305 : |
jhr |
1116 |
then (AST.E_Apply(BV.op_inner, tyArgs, [e1', e2'], rngTy), rngTy)
|
306 : |
|
|
else err (cxt, [
|
307 : |
|
|
S "type error for arguments of binary operator \"•\"\n",
|
308 : |
|
|
S " found: ", TYS[ty1, ty2], S "\n"
|
309 : |
|
|
])
|
310 : |
|
|
end
|
311 : |
|
|
| (ty1, ty2) => err (cxt, [
|
312 : |
|
|
S "type error for arguments of binary operator \"•\"\n",
|
313 : |
|
|
S " found: ", TYS[ty1, ty2], S "\n"
|
314 : |
|
|
])
|
315 : |
|
|
(* end case *))
|
316 : |
jhr |
1945 |
else if Atom.same(rator, BasisNames.op_colon)
|
317 : |
|
|
then (case (TU.prune ty1, TU.prune ty2)
|
318 : |
|
|
of (Ty.T_Tensor(s1 as Ty.Shape(dd1 as _::_::_)), Ty.T_Tensor(s2 as Ty.Shape(d21::d22::dd2))) => let
|
319 : |
|
|
val (dd1, d11, d12) = let
|
320 : |
|
|
fun splitLast (prefix, [d1, d2]) = (List.rev prefix, d1, d2)
|
321 : |
|
|
| splitLast (prefix, d::dd) = splitLast (d::prefix, dd)
|
322 : |
|
|
| splitLast (_, []) = raise Fail "impossible"
|
323 : |
|
|
in
|
324 : |
|
|
splitLast ([], dd1)
|
325 : |
|
|
end
|
326 : |
|
|
val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_colon)
|
327 : |
|
|
val resTy = Ty.T_Tensor(Ty.Shape(dd1@dd2))
|
328 : |
|
|
in
|
329 : |
|
|
if U.equalDim(d11, d21) andalso U.equalDim(d12, d22)
|
330 : |
|
|
andalso U.equalTypes(domTy, [ty1, ty2])
|
331 : |
|
|
andalso U.equalType(rngTy, resTy)
|
332 : |
|
|
then (AST.E_Apply(BV.op_colon, tyArgs, [e1', e2'], rngTy), rngTy)
|
333 : |
|
|
else err (cxt, [
|
334 : |
|
|
S "type error for arguments of binary operator \":\"\n",
|
335 : |
|
|
S " found: ", TYS[ty1, ty2], S "\n"
|
336 : |
|
|
])
|
337 : |
|
|
end
|
338 : |
|
|
| (ty1, ty2) => err (cxt, [
|
339 : |
|
|
S "type error for arguments of binary operator \":\"\n",
|
340 : |
|
|
S " found: ", TYS[ty1, ty2], S "\n"
|
341 : |
|
|
])
|
342 : |
|
|
(* end case *))
|
343 : |
jhr |
1116 |
else (case Env.findFunc (#env env, rator)
|
344 : |
jhr |
2133 |
of Env.PrimFun[rator] => let
|
345 : |
jhr |
1116 |
val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf rator)
|
346 : |
|
|
in
|
347 : |
jhr |
1975 |
case U.matchArgs(domTy, [e1', e2'], [ty1, ty2])
|
348 : |
|
|
of SOME args => (AST.E_Apply(rator, tyArgs, args, rngTy), rngTy)
|
349 : |
|
|
| NONE => err (cxt, [
|
350 : |
|
|
S "type error for binary operator \"", V rator, S "\"\n",
|
351 : |
|
|
S " expected: ", TYS domTy, S "\n",
|
352 : |
|
|
S " but found: ", TYS[ty1, ty2]
|
353 : |
|
|
])
|
354 : |
|
|
(* end case *)
|
355 : |
jhr |
1116 |
end
|
356 : |
jhr |
2133 |
| Env.PrimFun ovldList =>
|
357 : |
|
|
resolveOverload (cxt, rator, [ty1, ty2], [e1', e2'], ovldList)
|
358 : |
|
|
| _ => raise Fail "impossible"
|
359 : |
jhr |
1116 |
(* end case *))
|
360 : |
jhr |
81 |
end
|
361 : |
|
|
| PT.E_UnaryOp(rator, e) => let
|
362 : |
|
|
val (e', ty) = checkExpr(env, cxt, e)
|
363 : |
|
|
in
|
364 : |
jhr |
1116 |
case Env.findFunc (#env env, rator)
|
365 : |
jhr |
2133 |
of Env.PrimFun[rator] => let
|
366 : |
jhr |
381 |
val (tyArgs, Ty.T_Fun([domTy], rngTy)) = U.instantiate(Var.typeOf rator)
|
367 : |
jhr |
81 |
in
|
368 : |
jhr |
1975 |
case coerceType (domTy, ty, e')
|
369 : |
|
|
of SOME e' => (AST.E_Apply(rator, tyArgs, [e'], rngTy), rngTy)
|
370 : |
|
|
| NONE => err (cxt, [
|
371 : |
|
|
S "type error for unary operator \"", V rator, S "\"\n",
|
372 : |
|
|
S " expected: ", TY domTy, S "\n",
|
373 : |
|
|
S " but found: ", TY ty
|
374 : |
|
|
])
|
375 : |
|
|
(* end case *)
|
376 : |
jhr |
81 |
end
|
377 : |
jhr |
2133 |
| Env.PrimFun ovldList => resolveOverload (cxt, rator, [ty], [e'], ovldList)
|
378 : |
|
|
| _ => raise Fail "impossible"
|
379 : |
jhr |
81 |
(* end case *)
|
380 : |
|
|
end
|
381 : |
jhr |
381 |
| PT.E_Slice(e, indices) => let
|
382 : |
|
|
val (e', ty) = checkExpr (env, cxt, e)
|
383 : |
|
|
fun checkIndex NONE = NONE
|
384 : |
|
|
| checkIndex (SOME e) = let
|
385 : |
|
|
val (e', ty) = checkExpr (env, cxt, e)
|
386 : |
|
|
in
|
387 : |
jhr |
1687 |
if U.equalType(ty, Ty.T_Int)
|
388 : |
jhr |
381 |
then (SOME e')
|
389 : |
|
|
else err (cxt, [
|
390 : |
|
|
S "type error in index expression\n",
|
391 : |
jhr |
1116 |
S " expected int, but found: ", TY ty
|
392 : |
jhr |
381 |
])
|
393 : |
|
|
end
|
394 : |
|
|
val indices' = List.map checkIndex indices
|
395 : |
|
|
val order = List.length indices'
|
396 : |
jhr |
399 |
val expectedTy = TU.mkTensorTy order
|
397 : |
|
|
val resultTy = TU.slice(expectedTy, List.map Option.isSome indices')
|
398 : |
jhr |
381 |
in
|
399 : |
jhr |
1687 |
if U.equalType(ty, expectedTy)
|
400 : |
jhr |
381 |
then ()
|
401 : |
|
|
else err (cxt, [
|
402 : |
|
|
S "type error in slice operation\n",
|
403 : |
|
|
S " expected: ", S(Int.toString order), S "-order tensor\n",
|
404 : |
jhr |
1116 |
S " but found: ", TY ty
|
405 : |
jhr |
381 |
]);
|
406 : |
jhr |
399 |
(AST.E_Slice(e', indices', resultTy), resultTy)
|
407 : |
jhr |
381 |
end
|
408 : |
jhr |
1116 |
| PT.E_Subscript(e1, e2) => let
|
409 : |
|
|
val (e1', ty1) = checkExpr (env, cxt, e1)
|
410 : |
|
|
val (e2', ty2) = checkExpr (env, cxt, e2)
|
411 : |
jhr |
1991 |
fun chkIndex () = if U.equalType(ty2, Ty.T_Int)
|
412 : |
|
|
then ()
|
413 : |
|
|
else err (cxt, [
|
414 : |
|
|
S "expected int type for subscript index\n",
|
415 : |
|
|
S " but found: ", TY ty2
|
416 : |
|
|
])
|
417 : |
|
|
fun finish rator = let
|
418 : |
|
|
val (tyArgs, Ty.T_Fun(domTy, rngTy)) = U.instantiate(Var.typeOf rator)
|
419 : |
|
|
in
|
420 : |
|
|
if U.equalTypes(domTy, [ty1, ty2])
|
421 : |
|
|
then let
|
422 : |
jhr |
2019 |
val exp = AST.E_Apply(rator, tyArgs, [e1', e2'], rngTy)
|
423 : |
jhr |
1991 |
in
|
424 : |
|
|
(exp, rngTy)
|
425 : |
|
|
end
|
426 : |
|
|
else raise Fail "unexpected unification failure"
|
427 : |
|
|
end
|
428 : |
jhr |
1116 |
in
|
429 : |
jhr |
1991 |
case TU.pruneHead ty1
|
430 : |
|
|
of Ty.T_DynSequence _ => (
|
431 : |
|
|
chkIndex ();
|
432 : |
|
|
finish BV.dynSubscript)
|
433 : |
|
|
| Ty.T_Sequence _ => (
|
434 : |
|
|
chkIndex ();
|
435 : |
|
|
finish BV.subscript)
|
436 : |
|
|
| _ => err (cxt, [
|
437 : |
|
|
S "expected sequence type for subscript\n",
|
438 : |
|
|
S " but found: ", TY ty1
|
439 : |
|
|
])
|
440 : |
|
|
(* end case *)
|
441 : |
jhr |
1116 |
end
|
442 : |
|
|
| PT.E_Apply(e, args) => let
|
443 : |
|
|
fun stripMark (PT.E_Mark{tree, ...}) = stripMark tree
|
444 : |
|
|
| stripMark e = e
|
445 : |
|
|
val (args, tys) = checkExprList (env, cxt, args)
|
446 : |
jhr |
2133 |
fun checkFunApp f = (case Util.instantiate(Var.typeOf f)
|
447 : |
|
|
of (tyArgs, Ty.T_Fun(domTy, rngTy)) => (
|
448 : |
|
|
case U.matchArgs (domTy, args, tys)
|
449 : |
|
|
of SOME args => (AST.E_Apply(f, tyArgs, args, rngTy), rngTy)
|
450 : |
|
|
| NONE => err(cxt, [
|
451 : |
|
|
S "type error in application of ", V f, S "\n",
|
452 : |
|
|
S " expected: ", TYS domTy, S "\n",
|
453 : |
|
|
S " but found: ", TYS tys
|
454 : |
|
|
])
|
455 : |
|
|
(* end case *))
|
456 : |
|
|
| _ => err(cxt, [S "application of non-function ", V f])
|
457 : |
|
|
(* end case *))
|
458 : |
jhr |
1116 |
fun checkFieldApp (e1', ty1) = (case (args, tys)
|
459 : |
|
|
of ([e2'], [ty2]) => let
|
460 : |
jhr |
1975 |
val (tyArgs, Ty.T_Fun([fldTy, domTy], rngTy)) =
|
461 : |
jhr |
1687 |
Util.instantiate(Var.typeOf BV.op_probe)
|
462 : |
jhr |
1975 |
fun tyError () = err (cxt, [
|
463 : |
jhr |
1116 |
S "type error for field application\n",
|
464 : |
jhr |
1975 |
S " expected: ", TYS[fldTy, domTy], S "\n",
|
465 : |
jhr |
1116 |
S " but found: ", TYS[ty1, ty2]
|
466 : |
|
|
])
|
467 : |
jhr |
1975 |
in
|
468 : |
|
|
if U.equalType(fldTy, ty1)
|
469 : |
|
|
then (case coerceType(domTy, ty2, e2')
|
470 : |
|
|
of SOME e2' => (AST.E_Apply(BV.op_probe, tyArgs, [e1', e2'], rngTy), rngTy)
|
471 : |
|
|
| NONE => tyError()
|
472 : |
|
|
(* end case *))
|
473 : |
|
|
else tyError()
|
474 : |
jhr |
1116 |
end
|
475 : |
|
|
| _ => err(cxt, [S "badly formed field application"])
|
476 : |
|
|
(* end case *))
|
477 : |
|
|
in
|
478 : |
|
|
case stripMark e
|
479 : |
|
|
of PT.E_Var f => (case Env.findVar (#env env, f)
|
480 : |
|
|
of SOME f' => checkFieldApp (AST.E_Var f', Var.monoTypeOf f')
|
481 : |
|
|
| NONE => (case Env.findFunc (#env env, f)
|
482 : |
jhr |
2133 |
of Env.PrimFun[] => err(cxt, [S "unknown function ", A f])
|
483 : |
|
|
| Env.PrimFun[f'] =>
|
484 : |
|
|
if (inStrand env) andalso (Basis.isRestricted f')
|
485 : |
jhr |
1116 |
then err(cxt, [
|
486 : |
jhr |
2133 |
S "use of restricted operation ", V f',
|
487 : |
jhr |
1116 |
S " in strand body"
|
488 : |
|
|
])
|
489 : |
jhr |
2133 |
else checkFunApp f'
|
490 : |
|
|
| Env.PrimFun ovldList =>
|
491 : |
|
|
resolveOverload (cxt, f, tys, args, ovldList)
|
492 : |
|
|
| Env.UserFun f' => checkFunApp f'
|
493 : |
jhr |
1116 |
(* end case *))
|
494 : |
|
|
(* end case *))
|
495 : |
|
|
| _ => checkFieldApp (checkExpr (env, cxt, e))
|
496 : |
|
|
(* end case *)
|
497 : |
|
|
end
|
498 : |
jhr |
81 |
| PT.E_Tuple args => let
|
499 : |
|
|
val (args, tys) = checkExprList (env, cxt, args)
|
500 : |
|
|
in
|
501 : |
jhr |
1116 |
raise Fail "E_Tuple not yet implemented" (* FIXME *)
|
502 : |
jhr |
81 |
end
|
503 : |
jhr |
1116 |
| PT.E_Sequence args => let
|
504 : |
jhr |
1640 |
val (args, ty::tys) = checkExprList (env, cxt, args)
|
505 : |
jhr |
81 |
in
|
506 : |
jhr |
1687 |
if TU.isFixedSizeType(TU.pruneHead ty)
|
507 : |
jhr |
1640 |
then let
|
508 : |
jhr |
1687 |
fun chkTy ty' = U.equalType(ty, ty')
|
509 : |
jhr |
1640 |
val resTy = Ty.T_Sequence(ty, Ty.DimConst(List.length args))
|
510 : |
|
|
in
|
511 : |
|
|
if List.all chkTy tys
|
512 : |
jhr |
1688 |
then (AST.E_Seq args, resTy)
|
513 : |
jhr |
1640 |
else err(cxt, [S "arguments of sequence expression must have same type"])
|
514 : |
|
|
end
|
515 : |
|
|
else err(cxt, [S "sequence expression of non-value argument type"])
|
516 : |
jhr |
81 |
end
|
517 : |
jhr |
86 |
| PT.E_Cons args => let
|
518 : |
jhr |
1971 |
val (args, tys as ty::_) = checkExprList (env, cxt, args)
|
519 : |
jhr |
81 |
in
|
520 : |
jhr |
1971 |
case realType(TU.pruneHead ty)
|
521 : |
jhr |
475 |
of ty as Ty.T_Tensor shape => let
|
522 : |
|
|
val Ty.Shape dd = TU.pruneShape shape (* NOTE: this may fail if we allow user polymorphism *)
|
523 : |
|
|
val resTy = Ty.T_Tensor(Ty.Shape(Ty.DimConst(List.length args) :: dd))
|
524 : |
jhr |
1971 |
fun chkArgs (arg::args, argTy::tys, args') = (case coerceType(ty, argTy, arg)
|
525 : |
|
|
of SOME arg' => chkArgs (args, tys, arg'::args')
|
526 : |
|
|
| NONE => err(cxt, [S "arguments of tensor construction must have same type"])
|
527 : |
|
|
(* end case *))
|
528 : |
|
|
| chkArgs ([], [], args') = (AST.E_Cons(List.rev args'), resTy)
|
529 : |
jhr |
83 |
in
|
530 : |
jhr |
1971 |
chkArgs (args, tys, [])
|
531 : |
jhr |
83 |
end
|
532 : |
jhr |
99 |
| _ => err(cxt, [S "Invalid argument type for tensor construction"])
|
533 : |
jhr |
83 |
(* end case *)
|
534 : |
jhr |
81 |
end
|
535 : |
jhr |
86 |
| PT.E_Real e => (case checkExpr (env, cxt, e)
|
536 : |
|
|
of (e', Ty.T_Int) =>
|
537 : |
jhr |
1116 |
(AST.E_Apply(BV.i2r, [], [e'], Ty.realTy), Ty.realTy)
|
538 : |
jhr |
99 |
| _ => err(cxt, [S "argument of real conversion must be int"])
|
539 : |
jhr |
86 |
(* end case *))
|
540 : |
jhr |
1116 |
| PT.E_Id d => let
|
541 : |
|
|
val (tyArgs, Ty.T_Fun(_, rngTy)) =
|
542 : |
|
|
Util.instantiate(Var.typeOf(BV.identity))
|
543 : |
|
|
in
|
544 : |
jhr |
1687 |
if U.equalType(Ty.T_Tensor(checkShape(cxt, [d,d])), rngTy)
|
545 : |
jhr |
1116 |
then (AST.E_Apply(BV.identity, tyArgs, [], rngTy), rngTy)
|
546 : |
|
|
else raise Fail "impossible"
|
547 : |
|
|
end
|
548 : |
|
|
| PT.E_Zero dd => let
|
549 : |
|
|
val (tyArgs, Ty.T_Fun(_, rngTy)) =
|
550 : |
|
|
Util.instantiate(Var.typeOf(BV.zero))
|
551 : |
|
|
in
|
552 : |
jhr |
1687 |
if U.equalType(Ty.T_Tensor(checkShape(cxt, dd)), rngTy)
|
553 : |
jhr |
1116 |
then (AST.E_Apply(BV.zero, tyArgs, [], rngTy), rngTy)
|
554 : |
|
|
else raise Fail "impossible"
|
555 : |
|
|
end
|
556 : |
jhr |
1992 |
| PT.E_Image nrrd => let
|
557 : |
jhr |
2011 |
val (tyArgs, Ty.T_Fun(_, rngTy)) = Util.instantiate(Var.typeOf(BV.fn_image))
|
558 : |
jhr |
1992 |
in
|
559 : |
|
|
(AST.E_LoadNrrd(tyArgs, nrrd, rngTy), rngTy)
|
560 : |
|
|
end
|
561 : |
|
|
| PT.E_Load nrrd => let
|
562 : |
jhr |
2011 |
val (tyArgs, Ty.T_Fun(_, rngTy)) = Util.instantiate(Var.typeOf(BV.fn_load))
|
563 : |
jhr |
1992 |
in
|
564 : |
|
|
(AST.E_LoadNrrd(tyArgs, nrrd, rngTy), rngTy)
|
565 : |
|
|
end
|
566 : |
jhr |
70 |
(* end case *))
|
567 : |
|
|
|
568 : |
jhr |
81 |
(* typecheck a list of expressions returning a list of AST expressions and a list
|
569 : |
|
|
* of types of the expressions.
|
570 : |
|
|
*)
|
571 : |
|
|
and checkExprList (env, cxt, exprs) = let
|
572 : |
|
|
fun chk (e, (es, tys)) = let
|
573 : |
|
|
val (e, ty) = checkExpr (env, cxt, e)
|
574 : |
|
|
in
|
575 : |
|
|
(e::es, ty::tys)
|
576 : |
|
|
end
|
577 : |
|
|
in
|
578 : |
|
|
List.foldr chk ([], []) exprs
|
579 : |
|
|
end
|
580 : |
|
|
|
581 : |
jhr |
72 |
fun checkVarDecl (env, cxt, kind, d) = (case d
|
582 : |
jhr |
86 |
of PT.VD_Mark m => checkVarDecl (env, (#1 cxt, #span m), kind, #tree m)
|
583 : |
jhr |
72 |
| PT.VD_Decl(ty, x, e) => let
|
584 : |
jhr |
81 |
val ty = checkTy (cxt, ty)
|
585 : |
jhr |
72 |
val x' = Var.new (x, kind, ty)
|
586 : |
|
|
val (e', ty') = checkExpr (env, cxt, e)
|
587 : |
|
|
in
|
588 : |
jhr |
1687 |
case coerceType (ty, ty', e')
|
589 : |
jhr |
1971 |
of SOME e' => (x, x', e')
|
590 : |
jhr |
1687 |
| NONE => err(cxt, [
|
591 : |
jhr |
99 |
S "type of variable ", A x,
|
592 : |
|
|
S " does not match type of initializer\n",
|
593 : |
|
|
S " expected: ", TY ty, S "\n",
|
594 : |
jhr |
1116 |
S " but found: ", TY ty'
|
595 : |
jhr |
99 |
])
|
596 : |
jhr |
1687 |
(* end case *)
|
597 : |
jhr |
72 |
end
|
598 : |
|
|
(* end case *))
|
599 : |
|
|
|
600 : |
jhr |
70 |
(* typecheck a statement and translate it to AST *)
|
601 : |
jhr |
71 |
fun checkStmt (env, cxt, s) = (case s
|
602 : |
jhr |
86 |
of PT.S_Mark m => checkStmt (withEnvAndContext (env, cxt, m))
|
603 : |
jhr |
72 |
| PT.S_Block stms => let
|
604 : |
|
|
fun chk (_, [], stms) = AST.S_Block(List.rev stms)
|
605 : |
|
|
| chk (env, s::ss, stms) = let
|
606 : |
|
|
val (s', env') = checkStmt (env, cxt, s)
|
607 : |
|
|
in
|
608 : |
jhr |
81 |
chk (env', ss, s'::stms)
|
609 : |
jhr |
72 |
end
|
610 : |
|
|
in
|
611 : |
jhr |
1116 |
(chk (blockScope env, stms, []), env)
|
612 : |
jhr |
72 |
end
|
613 : |
|
|
| PT.S_Decl vd => let
|
614 : |
jhr |
1116 |
val (x, x', e) = checkVarDecl (env, cxt, Var.LocalVar, vd)
|
615 : |
jhr |
72 |
in
|
616 : |
jhr |
1116 |
checkForRedef (env, cxt, x);
|
617 : |
|
|
(AST.S_Decl(AST.VD_Decl(x', e)), insertLocal(env, cxt, x, x'))
|
618 : |
jhr |
72 |
end
|
619 : |
|
|
| PT.S_IfThen(e, s) => let
|
620 : |
jhr |
228 |
val (e', ty) = checkExpr (env, cxt, e)
|
621 : |
jhr |
81 |
val (s', _) = checkStmt (env, cxt, s)
|
622 : |
jhr |
72 |
in
|
623 : |
|
|
(* check that condition has bool type *)
|
624 : |
|
|
case ty
|
625 : |
|
|
of Ty.T_Bool => ()
|
626 : |
jhr |
99 |
| _ => err(cxt, [S "condition not boolean type"])
|
627 : |
jhr |
72 |
(* end case *);
|
628 : |
|
|
(AST.S_IfThenElse(e', s', AST.S_Block[]), env)
|
629 : |
|
|
end
|
630 : |
|
|
| PT.S_IfThenElse(e, s1, s2) => let
|
631 : |
jhr |
228 |
val (e', ty) = checkExpr (env, cxt, e)
|
632 : |
jhr |
81 |
val (s1', _) = checkStmt (env, cxt, s1)
|
633 : |
|
|
val (s2', _) = checkStmt (env, cxt, s2)
|
634 : |
jhr |
72 |
in
|
635 : |
|
|
(* check that condition has bool type *)
|
636 : |
|
|
case ty
|
637 : |
|
|
of Ty.T_Bool => ()
|
638 : |
jhr |
99 |
| _ => err(cxt, [S "condition not boolean type"])
|
639 : |
jhr |
72 |
(* end case *);
|
640 : |
|
|
(AST.S_IfThenElse(e', s1', s2'), env)
|
641 : |
|
|
end
|
642 : |
jhr |
228 |
| PT.S_Assign(x, e) => (case Env.findVar (#env env, x)
|
643 : |
jhr |
99 |
of NONE => err(cxt, [
|
644 : |
|
|
S "undefined variable ", A x
|
645 : |
|
|
])
|
646 : |
jhr |
72 |
| SOME x' => let
|
647 : |
jhr |
99 |
(* FIXME: check for polymorphic variables *)
|
648 : |
|
|
val ([], ty) = Var.typeOf x'
|
649 : |
jhr |
228 |
val (e', ty') = checkExpr (env, cxt, e)
|
650 : |
jhr |
1975 |
(* check for promotion *)
|
651 : |
|
|
val e' = (case coerceType(ty, ty', e')
|
652 : |
|
|
of SOME e' => e'
|
653 : |
|
|
| NONE => err(cxt, [
|
654 : |
|
|
S "type of assigned variable ", A x,
|
655 : |
|
|
S " does not match type of rhs\n",
|
656 : |
|
|
S " expected: ", TY ty, S "\n",
|
657 : |
|
|
S " but found: ", TY ty'
|
658 : |
|
|
])
|
659 : |
|
|
(* end case *))
|
660 : |
jhr |
72 |
in
|
661 : |
|
|
(* check that x' is mutable *)
|
662 : |
|
|
case Var.kindOf x'
|
663 : |
jhr |
511 |
of Var.StrandStateVar => ()
|
664 : |
|
|
| Var.StrandOutputVar => ()
|
665 : |
jhr |
72 |
| Var.LocalVar => ()
|
666 : |
jhr |
99 |
| _ => err(cxt, [
|
667 : |
|
|
S "assignment to immutable variable ", A x
|
668 : |
|
|
])
|
669 : |
jhr |
72 |
(* end case *);
|
670 : |
|
|
(AST.S_Assign(x', e'), env)
|
671 : |
|
|
end
|
672 : |
|
|
(* end case *))
|
673 : |
jhr |
1296 |
| PT.S_OpAssign(x, rator, e) => (case Env.findVar (#env env, x)
|
674 : |
|
|
of SOME x' => let
|
675 : |
|
|
val e1' = AST.E_Var x'
|
676 : |
|
|
val ty1 = Var.monoTypeOf x'
|
677 : |
|
|
val (e2', ty2) = checkExpr(env, cxt, e)
|
678 : |
jhr |
2133 |
val Env.PrimFun ovldList = Env.findFunc (#env env, rator)
|
679 : |
jhr |
1296 |
val (rhs, _) = resolveOverload (cxt, rator, [ty1, ty2], [e1', e2'], ovldList)
|
680 : |
|
|
in
|
681 : |
|
|
(AST.S_Assign(x', rhs), env)
|
682 : |
|
|
end
|
683 : |
|
|
| NONE => err(cxt, [S "undeclared variable ", A x, S " on lhs of ", A rator])
|
684 : |
|
|
(* end case *))
|
685 : |
jhr |
511 |
| PT.S_New(strand, args) => let
|
686 : |
jhr |
228 |
val argsAndTys' = List.map (fn e => checkExpr(env, cxt, e)) args
|
687 : |
jhr |
81 |
val (args', tys') = ListPair.unzip argsAndTys'
|
688 : |
jhr |
72 |
in
|
689 : |
jhr |
228 |
case #scope env
|
690 : |
|
|
of MethodScope => ()
|
691 : |
|
|
| InitScope => ()
|
692 : |
jhr |
511 |
| _ => err(cxt, [S "invalid scope for new strand"])
|
693 : |
jhr |
228 |
(* end case *);
|
694 : |
jhr |
511 |
(* FIXME: check that strand is defined and has the argument types match *)
|
695 : |
|
|
(AST.S_New(strand, args'), env)
|
696 : |
jhr |
72 |
end
|
697 : |
jhr |
228 |
| PT.S_Die => (
|
698 : |
|
|
case #scope env
|
699 : |
jhr |
235 |
of MethodScope => ()
|
700 : |
|
|
| _ => err(cxt, [S "\"die\" statment outside of method"])
|
701 : |
jhr |
228 |
(* end case *);
|
702 : |
|
|
(AST.S_Die, env))
|
703 : |
|
|
| PT.S_Stabilize => (
|
704 : |
|
|
case #scope env
|
705 : |
jhr |
235 |
of MethodScope => ()
|
706 : |
|
|
| _ => err(cxt, [S "\"stabilize\" statment outside of method"])
|
707 : |
jhr |
228 |
(* end case *);
|
708 : |
|
|
(AST.S_Stabilize, env))
|
709 : |
jhr |
2133 |
| PT.S_Return e => let
|
710 : |
|
|
val (e', ty) = checkExpr (env, cxt, e)
|
711 : |
|
|
in
|
712 : |
|
|
case #scope env
|
713 : |
|
|
of FunctionScope ty' => (case coerceType(ty', ty, e')
|
714 : |
|
|
of SOME e' => (AST.S_Return e', env)
|
715 : |
|
|
| NONE => err(cxt, [
|
716 : |
|
|
S "type of return expression does not match function's return type\n",
|
717 : |
|
|
S " expected: ", TY ty', S "\n",
|
718 : |
|
|
S " but found: ", TY ty
|
719 : |
|
|
])
|
720 : |
|
|
(* end case *))
|
721 : |
|
|
| _ => err(cxt, [S "\"return\" statment outside of function"])
|
722 : |
|
|
(* end case *)
|
723 : |
|
|
end
|
724 : |
jhr |
1640 |
| PT.S_Print args => let
|
725 : |
|
|
fun chkArg e = let
|
726 : |
|
|
val (e', ty) = checkExpr (env, cxt, e)
|
727 : |
|
|
in
|
728 : |
|
|
if TU.isValueType ty
|
729 : |
|
|
then ()
|
730 : |
|
|
else err(cxt, [
|
731 : |
|
|
S "expected value type in print, but found ", TY ty
|
732 : |
|
|
]);
|
733 : |
|
|
e'
|
734 : |
|
|
end
|
735 : |
|
|
val args' = List.map chkArg args
|
736 : |
|
|
in
|
737 : |
|
|
(AST.S_Print args', env)
|
738 : |
|
|
end
|
739 : |
jhr |
70 |
(* end case *))
|
740 : |
|
|
|
741 : |
jhr |
82 |
fun checkParams (env, cxt, params) = let
|
742 : |
|
|
fun chkParam (env, cxt, param) = (case param
|
743 : |
jhr |
86 |
of PT.P_Mark m => chkParam (withEnvAndContext (env, cxt, m))
|
744 : |
jhr |
82 |
| PT.P_Param(ty, x) => let
|
745 : |
jhr |
511 |
val x' = Var.new(x, AST.StrandParam, checkTy (cxt, ty))
|
746 : |
jhr |
82 |
in
|
747 : |
jhr |
2149 |
(* FIXME: should use an empty bindings list for the parameters *)
|
748 : |
jhr |
1116 |
checkForRedef (env, cxt, x);
|
749 : |
|
|
(x', insertLocal(env, cxt, x, x'))
|
750 : |
jhr |
82 |
end
|
751 : |
|
|
(* end case *))
|
752 : |
|
|
fun chk (param, (xs, env)) = let
|
753 : |
|
|
val (x, env) = chkParam (env, cxt, param)
|
754 : |
|
|
in
|
755 : |
|
|
(x::xs, env)
|
756 : |
|
|
end
|
757 : |
|
|
in
|
758 : |
|
|
List.foldr chk ([], env) params
|
759 : |
|
|
end
|
760 : |
|
|
|
761 : |
|
|
fun checkMethod (env, cxt, meth) = (case meth
|
762 : |
jhr |
86 |
of PT.M_Mark m => checkMethod (withEnvAndContext (env, cxt, m))
|
763 : |
jhr |
82 |
| PT.M_Method(name, body) => let
|
764 : |
jhr |
228 |
val (body, _) = checkStmt(methodScope env, cxt, body)
|
765 : |
jhr |
82 |
in
|
766 : |
|
|
AST.M_Method(name, body)
|
767 : |
|
|
end
|
768 : |
|
|
(* end case *))
|
769 : |
|
|
|
770 : |
jhr |
511 |
fun checkStrand (env, cxt, {name, params, state, methods}) = let
|
771 : |
|
|
(* check the strand parameters *)
|
772 : |
jhr |
82 |
val (params, env) = checkParams (env, cxt, params)
|
773 : |
jhr |
511 |
(* check the strand state variable definitions *)
|
774 : |
jhr |
2151 |
val (vds, hasOutput, env) = let
|
775 : |
|
|
fun checkStateVar ((isOut, vd), (vds, hasOut, env)) = let
|
776 : |
jhr |
511 |
val kind = if isOut then AST.StrandOutputVar else AST.StrandStateVar
|
777 : |
jhr |
228 |
val (x, x', e') = checkVarDecl (env, cxt, kind, vd)
|
778 : |
jhr |
82 |
in
|
779 : |
jhr |
228 |
(* check that output variables have value types *)
|
780 : |
|
|
if isOut andalso not(TU.isValueType(Var.monoTypeOf x'))
|
781 : |
|
|
then err(cxt, [
|
782 : |
|
|
S "output variable ", V x', S " has non-value type ",
|
783 : |
|
|
TY(Var.monoTypeOf x')
|
784 : |
|
|
])
|
785 : |
|
|
else ();
|
786 : |
jhr |
1116 |
checkForRedef (env, cxt, x);
|
787 : |
jhr |
2151 |
(AST.VD_Decl(x', e')::vds, hasOut orelse isOut, insertLocal(env, cxt, x, x'))
|
788 : |
jhr |
82 |
end
|
789 : |
jhr |
2151 |
val (vds, hasOutput, env) = List.foldl checkStateVar ([], false, env) state
|
790 : |
jhr |
82 |
in
|
791 : |
jhr |
2151 |
(List.rev vds, hasOutput, env)
|
792 : |
jhr |
82 |
end
|
793 : |
jhr |
511 |
(* check the strand methods *)
|
794 : |
jhr |
82 |
val methods = List.map (fn m => checkMethod (env, cxt, m)) methods
|
795 : |
jhr |
1444 |
(* get the list of methods defined by the user *)
|
796 : |
|
|
val methodNames = List.map (fn (AST.M_Method(name, _)) => name) methods
|
797 : |
jhr |
1116 |
(* if the stabilize method is not provided, add one *)
|
798 : |
jhr |
1640 |
val methods = if List.exists (fn StrandUtil.Stabilize => true | _ => false) methodNames
|
799 : |
jhr |
1116 |
then methods
|
800 : |
jhr |
1640 |
else methods @ [AST.M_Method(StrandUtil.Stabilize, AST.S_Block[])]
|
801 : |
jhr |
82 |
in
|
802 : |
jhr |
2151 |
(* FIXME: once there are global outputs, then it should be okay to have not strand outputs! *)
|
803 : |
|
|
(* check that there is at least one output variable *)
|
804 : |
|
|
if not hasOutput
|
805 : |
|
|
then err(cxt, [S "strand ", A name, S " does not have any outputs"])
|
806 : |
|
|
else ();
|
807 : |
jhr |
1444 |
(* FIXME: should check for duplicate method definitions *)
|
808 : |
jhr |
1640 |
if not(List.exists (fn StrandUtil.Update => true | _ => false) methodNames)
|
809 : |
jhr |
1116 |
then err(cxt, [S "strand ", A name, S " is missing an update method"])
|
810 : |
|
|
else ();
|
811 : |
jhr |
511 |
AST.D_Strand{name = name, params = params, state = vds, methods = methods}
|
812 : |
jhr |
82 |
end
|
813 : |
|
|
|
814 : |
jhr |
89 |
fun checkCreate (env, cxt, PT.C_Mark m) = checkCreate (withEnvAndContext (env, cxt, m))
|
815 : |
jhr |
511 |
| checkCreate (env, cxt, PT.C_Create(strand, args)) = let
|
816 : |
jhr |
228 |
val (args, tys) = checkExprList (env, cxt, args)
|
817 : |
jhr |
89 |
in
|
818 : |
jhr |
2151 |
(* FIXME: check args against strand definition *)
|
819 : |
jhr |
511 |
AST.C_Create(strand, args)
|
820 : |
jhr |
89 |
end
|
821 : |
|
|
|
822 : |
jhr |
1116 |
fun checkIters (env0, cxt, iters) = let
|
823 : |
|
|
(* check an iteration range specification from the initially clause. We do the checking
|
824 : |
|
|
* of the expressions using env0, which does not have any of the iteration variables in
|
825 : |
|
|
* it (the iteration is rectangular), but we also accumulate the iteration bindings,
|
826 : |
|
|
* which are used to create the final environment for checking the create call.
|
827 : |
|
|
*)
|
828 : |
|
|
fun checkIter (env, cxt, PT.I_Mark m) = checkIter (withEnvAndContext (env, cxt, m))
|
829 : |
|
|
| checkIter (env, cxt, PT.I_Range(x, e1, e2)) = let
|
830 : |
|
|
val (e1', ty1) = checkExpr (env, cxt, e1)
|
831 : |
|
|
val (e2', ty2) = checkExpr (env, cxt, e2)
|
832 : |
|
|
val x' = Var.new(x, Var.LocalVar, Ty.T_Int)
|
833 : |
jhr |
89 |
in
|
834 : |
jhr |
1116 |
case (ty1, ty2)
|
835 : |
|
|
of (Ty.T_Int, Ty.T_Int) => (AST.I_Range(x', e1', e2'), (x, x'))
|
836 : |
|
|
| _ => err(cxt, [
|
837 : |
|
|
S "range expressions must have integer type\n",
|
838 : |
|
|
S " but found: ", TY ty1, S " .. ", TY ty2
|
839 : |
|
|
])
|
840 : |
|
|
(* end case *)
|
841 : |
jhr |
89 |
end
|
842 : |
jhr |
1116 |
fun chk ([], iters, bindings) =
|
843 : |
|
|
(List.rev iters, List.foldl (fn ((x, x'), env) => insertLocal(env, cxt, x, x')) env0 bindings)
|
844 : |
|
|
| chk (iter::rest, iters, bindings) = let
|
845 : |
|
|
val (iter, binding) = checkIter (env0, cxt, iter)
|
846 : |
|
|
in
|
847 : |
|
|
chk (rest, iter::iters, binding::bindings)
|
848 : |
|
|
end
|
849 : |
jhr |
89 |
in
|
850 : |
jhr |
1116 |
chk (iters, [], [])
|
851 : |
jhr |
89 |
end
|
852 : |
|
|
|
853 : |
jhr |
71 |
fun checkDecl (env, cxt, d) = (case d
|
854 : |
jhr |
86 |
of PT.D_Mark m => checkDecl (withEnvAndContext (env, cxt, m))
|
855 : |
jhr |
1301 |
| PT.D_Input(ty, x, desc, optExp) => let
|
856 : |
|
|
(* FIXME: need to do something with the description *)
|
857 : |
jhr |
71 |
val ty = checkTy(cxt, ty)
|
858 : |
|
|
val x' = Var.new(x, Var.InputVar, ty)
|
859 : |
|
|
val dcl = (case optExp
|
860 : |
jhr |
1301 |
of NONE => AST.D_Input(x', desc, NONE)
|
861 : |
jhr |
71 |
| SOME e => let
|
862 : |
jhr |
228 |
val (e', ty') = checkExpr (env, cxt, e)
|
863 : |
jhr |
71 |
in
|
864 : |
jhr |
1971 |
case coerceType (ty, ty', e')
|
865 : |
|
|
of SOME e' => AST.D_Input(x', desc, SOME e')
|
866 : |
|
|
| NONE => err(cxt, [
|
867 : |
|
|
S "definition of ", V x', S " has wrong type\n",
|
868 : |
|
|
S " expected: ", TY ty, S "\n",
|
869 : |
|
|
S " but found: ", TY ty'
|
870 : |
|
|
])
|
871 : |
|
|
(* end case *)
|
872 : |
jhr |
71 |
end
|
873 : |
|
|
(* end case *))
|
874 : |
|
|
in
|
875 : |
jhr |
2050 |
(* check that input variables have valid types *)
|
876 : |
|
|
if not(TU.isValueType ty orelse TU.isImageType ty)
|
877 : |
|
|
then err(cxt, [S "input variable ", V x', S " has invalid type ", TY ty])
|
878 : |
jhr |
228 |
else ();
|
879 : |
jhr |
1116 |
checkForRedef (env, cxt, x);
|
880 : |
|
|
(dcl, insertGlobal(env, cxt, x, x'))
|
881 : |
jhr |
71 |
end
|
882 : |
jhr |
72 |
| PT.D_Var vd => let
|
883 : |
jhr |
228 |
val (x, x', e') = checkVarDecl (env, cxt, Var.GlobalVar, vd)
|
884 : |
jhr |
72 |
in
|
885 : |
jhr |
1116 |
checkForRedef (env, cxt, x);
|
886 : |
|
|
(AST.D_Var(AST.VD_Decl(x', e')), insertGlobal(env, cxt, x, x'))
|
887 : |
jhr |
72 |
end
|
888 : |
jhr |
2134 |
| PT.D_Func(ty, f, params, body) => let
|
889 : |
jhr |
2133 |
val ty' = checkTy(cxt, ty)
|
890 : |
|
|
val (params', env') = checkParams (env, cxt, params)
|
891 : |
|
|
val body' = (case body
|
892 : |
|
|
of PT.FB_Expr e => let
|
893 : |
|
|
val (e', ty) = checkExpr (env', cxt, e)
|
894 : |
|
|
in
|
895 : |
|
|
case coerceType(ty', ty, e')
|
896 : |
|
|
of SOME e' => AST.S_Return e'
|
897 : |
|
|
| NONE => err(cxt, [
|
898 : |
|
|
S "type of function body does not match return type\n",
|
899 : |
|
|
S " expected: ", TY ty', S "\n",
|
900 : |
|
|
S " but found: ", TY ty
|
901 : |
|
|
])
|
902 : |
|
|
(* end case *)
|
903 : |
|
|
end
|
904 : |
jhr |
2141 |
(* FIXME: we need to check that there is a return on all control-flow paths *)
|
905 : |
jhr |
2133 |
| PT.FB_Stmt s => #1(checkStmt(functionScope (env', ty'), cxt, s))
|
906 : |
|
|
(* end case *))
|
907 : |
|
|
val fnTy = Ty.T_Fun(List.map Var.monoTypeOf params', ty')
|
908 : |
|
|
val f' = Var.new (f, AST.FunVar, fnTy)
|
909 : |
|
|
in
|
910 : |
jhr |
2141 |
(* QUESTION: should we check for redefinition of the f? *)
|
911 : |
jhr |
2134 |
(AST.D_Func(f', params', body'), insertFunc(env, cxt, f, f'))
|
912 : |
jhr |
2133 |
end
|
913 : |
jhr |
511 |
| PT.D_Strand arg => (checkStrand(strandScope env, cxt, arg), env)
|
914 : |
jhr |
89 |
| PT.D_InitialArray(create, iterators) => let
|
915 : |
jhr |
228 |
val env = initScope env
|
916 : |
jhr |
89 |
val (iterators, env') = checkIters (env, cxt, iterators)
|
917 : |
|
|
val create = checkCreate (env', cxt, create)
|
918 : |
|
|
in
|
919 : |
|
|
(AST.D_InitialArray(create, iterators), env)
|
920 : |
|
|
end
|
921 : |
|
|
| PT.D_InitialCollection(create, iterators) => let
|
922 : |
jhr |
228 |
val env = initScope env
|
923 : |
jhr |
89 |
val (iterators, env') = checkIters (env, cxt, iterators)
|
924 : |
|
|
val create = checkCreate (env', cxt, create)
|
925 : |
|
|
in
|
926 : |
|
|
(AST.D_InitialCollection(create, iterators), env)
|
927 : |
|
|
end
|
928 : |
jhr |
70 |
(* end case *))
|
929 : |
|
|
|
930 : |
jhr |
1301 |
(* reorder the declarations so that the input variables come first *)
|
931 : |
|
|
fun reorderDecls dcls = let
|
932 : |
|
|
fun isInput (AST.D_Input _) = true
|
933 : |
|
|
| isInput _ = false
|
934 : |
|
|
val (inputs, others) = List.partition isInput dcls
|
935 : |
|
|
in
|
936 : |
|
|
inputs @ others
|
937 : |
|
|
end
|
938 : |
|
|
|
939 : |
jhr |
86 |
fun check errStrm (PT.Program{span, tree}) = let
|
940 : |
|
|
val cxt = (errStrm, span)
|
941 : |
jhr |
1301 |
fun chk (env, [], dcls') = AST.Program(reorderDecls(List.rev dcls'))
|
942 : |
jhr |
81 |
| chk (env, dcl::dcls, dcls') = let
|
943 : |
jhr |
86 |
val (dcl', env) = checkDecl (env, cxt, dcl)
|
944 : |
jhr |
81 |
in
|
945 : |
|
|
chk (env, dcls, dcl'::dcls')
|
946 : |
|
|
end
|
947 : |
|
|
in
|
948 : |
jhr |
1116 |
chk ({scope=GlobalScope, bindings=AtomMap.empty, env=Basis.env}, tree, [])
|
949 : |
jhr |
81 |
end
|
950 : |
jhr |
2149 |
handle TypeError => AST.Program[]
|
951 : |
jhr |
70 |
|
952 : |
jhr |
69 |
end
|