Start of Apache
[hcoop/domtool2.git] / src / tycheck.sml
CommitLineData
27d9de59
AC
1(* HCoop Domtool (http://hcoop.sourceforge.net/)
2 * Copyright (c) 2006, Adam Chlipala
3 *
4 * This program is free software; you can redistribute it and/or
5 * modify it under the terms of the GNU General Public License
6 * as published by the Free Software Foundation; either version 2
7 * of the License, or (at your option) any later version.
8 *
9 * This program is distributed in the hope that it will be useful,
10 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 * GNU General Public License for more details.
13 *
14 * You should have received a copy of the GNU General Public License
15 * along with this program; if not, write to the Free Software
16 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
dac62e84 17 *)
27d9de59
AC
18
19(* Domtool configuration language type checking *)
20
21structure Tycheck :> TYCHECK = struct
22
492c1cff 23open Ast Print Env
27d9de59
AC
24
25structure SM = StringMap
26
27d9de59
AC
27local
28 val unifCount = ref 0
29in
30fun resetUnif () = unifCount := 0
31
32fun newUnif () =
33 let
34 val c = !unifCount
35 val name =
36 if c < 26 then
37 str (chr (ord #"A" + c))
38 else
39 "UNIF" ^ Int.toString (c - 26)
40 in
41 unifCount := c + 1;
42 TUnif (name, ref NONE)
43 end
44end
45
46exception UnequalDomains
47
48fun eqRecord f (r1, r2) =
49 (SM.appi (fn (k, v1) =>
50 case SM.find (r2, k) of
51 NONE => raise UnequalDomains
52 | SOME v2 =>
53 if f (v1, v2) then
54 ()
55 else
56 raise UnequalDomains) r1;
57 SM.appi (fn (k, v2) =>
58 case SM.find (r1, k) of
59 NONE => raise UnequalDomains
60 | SOME v1 =>
61 if f (v1, v2) then
62 ()
63 else
64 raise UnequalDomains) r2;
65 true)
66 handle UnequalDomains => false
67
68fun eqPred ((p1, _), (p2, _)) =
69 case (p1, p2) of
70 (CRoot, CRoot) => true
71 | (CConst s1, CConst s2) => s1 = s2
72 | (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
73 | (CNot p1, CNot p2) => eqPred (p1, p2)
74 | (CAnd (p1, q1), CAnd (p2, q2)) =>
75 eqPred (p1, p2) andalso eqPred (q1, q2)
76
77 | _ => false
78
79fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
80 case (t1, t2) of
81 (TBase s1, TBase s2) => s1 = s2
82 | (TList t1, TList t2) => eqTy (t1, t2)
83 | (TArrow (d1, r1), TArrow (d2, r2)) =>
84 eqTy (d1, d2) andalso eqTy (r1, r2)
85
86 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
87 eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
88 andalso eqRecord eqTy (r1, r2)
89
234b917a 90 | (TNested (p1, q1), TNested (p2, q2)) =>
1a4e5a6c 91 eqPred (p1, p2) andalso eqTy (q1, q2)
234b917a 92
27d9de59
AC
93 | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
94 | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
95
96 | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
97
98 | (TError, TError) => true
99
100 | _ => false
101
102datatype unification_error =
103 UnifyPred of pred * pred
104 | UnifyTyp of typ * typ
105 | UnifyOccurs of string * typ
106
107exception Unify of unification_error
108
109datatype type_error =
110 WrongType of string * exp * typ * typ * unification_error option
111 | WrongForm of string * string * exp * typ * unification_error option
112 | UnboundVariable of string
234b917a 113 | WrongPred of string * pred * pred
27d9de59 114
27d9de59
AC
115fun describe_unification_error t ue =
116 case ue of
117 UnifyPred (p1, p2) =>
234b917a 118 (print "Reason: Incompatible contexts.\n";
27d9de59
AC
119 preface ("Have:", p_pred p1);
120 preface ("Need:", p_pred p2))
121 | UnifyTyp (t1, t2) =>
122 if eqTy (t, t1) then
123 ()
124 else
125 (print "Reason: Incompatible types.\n";
126 preface ("Have:", p_typ t1);
127 preface ("Need:", p_typ t2))
128 | UnifyOccurs (name, t') =>
129 if eqTy (t, t') then
130 ()
131 else
132 (print "Reason: Occurs check failed for ";
133 print name;
134 print " in:\n";
135 printd (p_typ t))
136
137fun describe_type_error loc te =
138 case te of
139 WrongType (place, e, t1, t2, ueo) =>
140 (ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
141 preface (" Expression:", p_exp e);
142 preface ("Actual type:", p_typ t1);
143 preface ("Needed type:", p_typ t2);
144 Option.app (describe_unification_error t1) ueo)
145 | WrongForm (place, form, e, t, ueo) =>
146 (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
147 preface ("Expression:", p_exp e);
148 preface (" Type:", p_typ t);
149 Option.app (describe_unification_error t) ueo)
150 | UnboundVariable name =>
151 ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
234b917a
AC
152 | WrongPred (place, p1, p2) =>
153 (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
154 preface ("Have:", p_pred p1);
155 preface ("Need:", p_pred p2))
27d9de59 156
db427c67 157fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
27d9de59 158 case (p1, p2) of
1a4e5a6c
AC
159 (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
160 | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
161
162 | (_, CPrefix (CRoot, _)) => true
db427c67
AC
163 | (CNot (CPrefix (CRoot, _), _), _) => true
164
165 | (CRoot, CRoot) => true
166
167 | (CConst s1, CConst s2) => s1 = s2
168
169 | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
234b917a 170 | (_, CPrefix p2) => predImplies (p1All, p2)
db427c67
AC
171
172 | (CNot p1, CNot p2) => predImplies (p2, p1)
27d9de59 173
db427c67
AC
174 | _ => false
175
176fun predSimpl (pAll as (p, loc)) =
177 case p of
178 CRoot => pAll
179 | CConst _ => pAll
180 | CPrefix p => (CPrefix (predSimpl p), loc)
181 | CNot p => (CNot (predSimpl p), loc)
182 | CAnd (p1, p2) =>
183 let
184 val p1' = predSimpl p1
185 val p2' = predSimpl p2
186 in
187 case p1' of
188 (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
189 | _ => if predImplies (p2', p1') then
190 p2'
1a4e5a6c
AC
191 else if predImplies (p1', p2') then
192 p1'
db427c67
AC
193 else
194 (CAnd (p1', p2'), loc)
195 end
196
234b917a 197fun subPred (p1, p2) =
db427c67
AC
198 if predImplies (p1, p2) then
199 ()
200 else
201 raise (Unify (UnifyPred (p1, p2)))
27d9de59 202
234b917a
AC
203fun subRecord f (r1, r2) =
204 SM.appi (fn (k, v2) =>
205 case SM.find (r1, k) of
206 NONE => raise UnequalDomains
207 | SOME v1 => f (v1, v2)) r2
27d9de59
AC
208
209fun occurs u (t, _) =
210 case t of
211 TBase _ => false
212 | TList t => occurs u t
213 | TArrow (d, r) => occurs u d orelse occurs u r
214 | TAction (_, d, r) =>
215 List.exists (occurs u) (SM.listItems d)
216 orelse List.exists (occurs u) (SM.listItems r)
1a4e5a6c 217 | TNested (_, t) => occurs u t
27d9de59
AC
218 | TError => false
219 | TUnif (_, ref (SOME t)) => occurs u t
220 | TUnif (_, u') => u = u'
221
234b917a 222fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
27d9de59
AC
223 case (t1, t2) of
224 (TBase s1, TBase s2) =>
225 if s1 = s2 then
226 ()
227 else
228 raise Unify (UnifyTyp (t1All, t2All))
234b917a 229 | (TList t1, TList t2) => subTyp (t1, t2)
27d9de59 230 | (TArrow (d1, r1), TArrow (d2, r2)) =>
234b917a
AC
231 (subTyp (d2, d1);
232 subTyp (r1, r2))
27d9de59
AC
233
234 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
234b917a
AC
235 ((subPred (p2, p1);
236 subRecord subTyp (d2, d1);
237 subRecord subTyp (r1, r2);
238 subRecord subTyp (r2, r1))
27d9de59
AC
239 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
240
234b917a
AC
241 | (TNested (d1, r1), TNested (d2, r2)) =>
242 (subPred (d2, d1);
1a4e5a6c 243 subTyp (r1, r2))
234b917a
AC
244
245 | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
246 | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
27d9de59
AC
247
248 | (TUnif (_, r1), TUnif (_, r2)) =>
249 if r1 = r2 then
250 ()
251 else
252 r1 := SOME t2All
253
254 | (TUnif (name, r), _) =>
255 if occurs r t2All then
256 raise (Unify (UnifyOccurs (name, t2All)))
257 else
258 r := SOME t2All
259
260 | (_, TUnif (name, r)) =>
261 if occurs r t1All then
262 raise (Unify (UnifyOccurs (name, t1All)))
263 else
264 r := SOME t1All
265
266 | (TError, _) => ()
267 | (_, TError) => ()
268
269 | _ => raise Unify (UnifyTyp (t1All, t2All))
270
271fun isError t =
272 case t of
273 (TError, _) => true
274 | _ => false
275
db427c67
AC
276fun whnorm (tAll as (t, loc)) =
277 case t of
278 TUnif (_, ref (SOME tAll)) => whnorm tAll
279 | _ => tAll
280
629a34f6
AC
281fun baseCondition t =
282 case whnorm t of
283 (TBase name, _) => typeRule name
284 | (TList t, _) =>
285 (case baseCondition t of
286 NONE => NONE
287 | SOME f => SOME (fn (EList ls, _) => List.all f ls
288 | _ => false))
289 | _ => NONE
290
6be996d4 291fun hasTyp (e, t1, t2) =
629a34f6
AC
292 if (case baseCondition t2 of
293 NONE => false
294 | SOME rule => rule e) then
295 ()
296 else
297 subTyp (t1, t2)
6be996d4 298
095de39e
AC
299fun checkPred G (p, loc) =
300 let
301 val err = ErrorMsg.error (SOME loc)
302 in
303 case p of
304 CRoot => ()
305 | CConst s =>
306 if lookupContext G s then
307 ()
308 else
309 err ("Unbound context " ^ s)
310 | CPrefix p => checkPred G p
311 | CNot p => checkPred G p
312 | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
313 end
314
234b917a
AC
315fun checkTyp G (tAll as (t, loc)) =
316 let
317 val err = ErrorMsg.error (SOME loc)
318 in
319 case t of
320 TBase name =>
321 if lookupType G name then
322 tAll
323 else
324 (err ("Unbound type name " ^ name);
325 (TError, loc))
326 | TList t => (TList (checkTyp G t), loc)
327 | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
095de39e
AC
328 | TAction (p, d, r) => (checkPred G p;
329 (TAction (p, SM.map (checkTyp G) d,
330 SM.map (checkTyp G) r), loc))
331 | TNested (p, t) => (checkPred G p;
332 (TNested (p, checkTyp G t), loc))
234b917a
AC
333 | TError => raise Fail "TError in parser-generated type"
334 | TUnif _ => raise Fail "TUnif in parser-generated type"
335 end
336
8a7c40fa
AC
337fun envVarSetFrom v (e, _) =
338 case e of
339 ESet (v', e) =>
340 if v = v' then
341 SOME e
342 else
343 NONE
344 | EGet (_, _, e) => envVarSetFrom v e
345 | ESeq es => foldr (fn (e, found) =>
346 case found of
347 SOME _ => found
348 | NONE => envVarSetFrom v e)
349 NONE es
350 | ELocal (_, e) => envVarSetFrom v e
351
352 | _ => NONE
353
27d9de59
AC
354fun checkExp G (eAll as (e, loc)) =
355 let
356 val dte = describe_type_error loc
357 in
358 case e of
359 EInt _ => (TBase "int", loc)
360 | EString _ => (TBase "string", loc)
361 | EList es =>
362 let
363 val t = (newUnif (), loc)
364 in
365 foldl (fn (e', ret) =>
366 let
367 val t' = checkExp G e'
368 in
6be996d4 369 (hasTyp (eAll, t', t);
27d9de59
AC
370 if isError t' then
371 (TList (TError, loc), loc)
372 else
373 ret)
374 handle Unify ue =>
375 (dte (WrongType ("List element",
376 e',
377 t',
378 t,
379 SOME ue));
380 (TError, loc))
381 end) (TList t, loc) es
382 end
383
384 | ELam (x, to, e) =>
385 let
386 val t =
387 case to of
388 NONE => (newUnif (), loc)
234b917a 389 | SOME t => checkTyp G t
27d9de59 390
492c1cff 391 val G' = bindVal G (x, t, NONE)
27d9de59
AC
392 val t' = checkExp G' e
393 in
394 (TArrow (t, t'), loc)
395 end
396 | EVar x =>
234b917a 397 (case lookupVal G x of
27d9de59
AC
398 NONE => (dte (UnboundVariable x);
399 (TError, loc))
400 | SOME t => t)
401 | EApp (func, arg) =>
402 let
403 val dom = (newUnif (), loc)
404 val ran = (newUnif (), loc)
405
406 val tf = checkExp G func
407 val ta = checkExp G arg
408 in
6be996d4
AC
409 (hasTyp (func, tf, (TArrow (dom, ran), loc));
410 hasTyp (arg, ta, dom)
27d9de59
AC
411 handle Unify ue =>
412 dte (WrongType ("Function argument",
413 arg,
414 ta,
415 dom,
416 SOME ue));
417 ran)
418 handle Unify ue =>
419 (dte (WrongForm ("Function to be applied",
420 "function",
421 func,
422 tf,
423 SOME ue));
424 (TError, loc))
425 end
db427c67
AC
426
427 | ESet (evar, e) =>
428 let
429 val t = checkExp G e
430 in
431 (TAction ((CPrefix (CRoot, loc), loc),
432 SM.empty,
433 SM.insert (SM.empty, evar, t)),
434 loc)
435 end
436 | EGet (x, evar, rest) =>
437 let
438 val xt = (newUnif (), loc)
492c1cff 439 val G' = bindVal G (x, xt, NONE)
db427c67
AC
440
441 val rt = whnorm (checkExp G' rest)
442 in
443 case rt of
444 (TAction (p, d, r), _) =>
445 (case SM.find (d, evar) of
446 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
447 | SOME xt' =>
234b917a 448 (subTyp (xt', xt)
db427c67
AC
449 handle Unify ue =>
450 dte (WrongType ("Retrieved environment variable",
451 (EVar x, loc),
452 xt',
453 xt,
454 SOME ue));
455 rt))
234b917a 456 | (TError, _) => rt
db427c67
AC
457 | _ => (dte (WrongForm ("Body of environment variable read",
458 "action",
459 rest,
460 rt,
461 NONE));
462 (TError, loc))
463 end
464
465 | ESeq [] => raise Fail "Empty ESeq"
466 | ESeq [e1] => checkExp G e1
467 | ESeq (e1 :: rest) =>
468 let
469 val e2 = (ESeq rest, loc)
470
471 val t1 = whnorm (checkExp G e1)
472 val t2 = whnorm (checkExp G e2)
473 in
474 case t1 of
475 (TAction (p1, d1, r1), _) =>
476 (case t2 of
477 (TAction (p2, d2, r2), _) =>
478 let
479 val p' = predSimpl (CAnd (p1, p2), loc)
480
481 val d' = SM.foldli (fn (name, t, d') =>
482 case SM.find (r1, name) of
483 NONE =>
484 (case SM.find (d', name) of
485 NONE => SM.insert (d', name, t)
486 | SOME t' =>
8a7c40fa
AC
487 ((case envVarSetFrom name e1 of
488 NONE => subTyp (t, t')
489 | SOME e => hasTyp (e, t, t'))
db427c67
AC
490 handle Unify ue =>
491 dte (WrongType ("Shared environment variable",
492 (EVar name, loc),
db427c67 493 t',
8a7c40fa 494 t,
db427c67
AC
495 SOME ue));
496 d'))
497 | SOME t' =>
8a7c40fa
AC
498 ((case envVarSetFrom name e1 of
499 NONE => subTyp (t, t')
500 | SOME e => hasTyp (e, t, t'))
db427c67
AC
501 handle Unify ue =>
502 dte (WrongType ("Shared environment variable",
503 (EVar name, loc),
db427c67 504 t',
8a7c40fa 505 t,
db427c67
AC
506 SOME ue));
507 d'))
508 d1 d2
509
510 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
511 r1 r2
512 in
513 (TAction (p', d', r'), loc)
514 end
234b917a 515 | (TError, _) => t2
db427c67
AC
516 | _ => (dte (WrongForm ("Action to be sequenced",
517 "action",
518 e2,
519 t2,
520 NONE));
521 (TError, loc)))
234b917a 522 | (TError, _) => t1
db427c67
AC
523 | _ => (dte (WrongForm ("Action to be sequenced",
524 "action",
525 e1,
526 t1,
527 NONE));
528 (TError, loc))
529 end
530
1a4e5a6c 531 | ELocal (e1, e2) =>
db427c67 532 let
1a4e5a6c
AC
533 val t1 = whnorm (checkExp G e1)
534 val t2 = whnorm (checkExp G e2)
db427c67 535 in
1a4e5a6c
AC
536 case t1 of
537 (TAction (p1, d1, r1), _) =>
538 (case t2 of
539 (TAction (p2, d2, r2), _) =>
540 let
541 val p' = predSimpl (CAnd (p1, p2), loc)
542
543 val d' = SM.foldli (fn (name, t, d') =>
544 case SM.find (r1, name) of
545 NONE =>
546 (case SM.find (d', name) of
547 NONE => SM.insert (d', name, t)
548 | SOME t' =>
8a7c40fa
AC
549 ((case envVarSetFrom name e1 of
550 NONE => subTyp (t', t)
551 | SOME e => hasTyp (e, t', t))
1a4e5a6c
AC
552 handle Unify ue =>
553 dte (WrongType ("Shared environment variable",
554 (EVar name, loc),
1a4e5a6c 555 t',
8a7c40fa 556 t,
1a4e5a6c
AC
557 SOME ue));
558 d'))
559 | SOME t' =>
8a7c40fa
AC
560 ((case envVarSetFrom name e1 of
561 NONE => subTyp (t', t)
562 | SOME e => hasTyp (e, t', t))
1a4e5a6c
AC
563 handle Unify ue =>
564 dte (WrongType ("Shared environment variable",
565 (EVar name, loc),
1a4e5a6c 566 t',
8a7c40fa 567 t,
1a4e5a6c
AC
568 SOME ue));
569 d'))
570 d1 d2
571 in
572 (TAction (p', d', r2), loc)
573 end
574 | (TError, _) => t2
575 | _ => (dte (WrongForm ("Action to be sequenced",
576 "action",
577 e2,
578 t2,
579 NONE));
580 (TError, loc)))
581 | (TError, _) => t1
582 | _ => (dte (WrongForm ("Action to be sequenced",
db427c67 583 "action",
1a4e5a6c
AC
584 e1,
585 t1,
db427c67
AC
586 NONE));
587 (TError, loc))
588 end
234b917a 589
1a4e5a6c 590
234b917a
AC
591 | EWith (e1, e2) =>
592 let
593 val t1 = whnorm (checkExp G e1)
594 val t2 = whnorm (checkExp G e2)
595 in
596 case t1 of
1a4e5a6c 597 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a
AC
598 (case t2 of
599 (TAction (p, d, r), _) =>
600 if predImplies (pd, p) then
1a4e5a6c
AC
601 let
602 val combineRecs =
603 SM.unionWithi (fn (name, t1, t2) =>
604 (subTyp (t1, t2)
605 handle Unify ue =>
606 dte (WrongType ("Environment variable",
607 (EVar name, loc),
608 t1,
609 t2,
610 SOME ue));
611 t2))
612 in
613 (TAction (pr, combineRecs (d, d1),
614 combineRecs (r, r1)), loc)
615 end
234b917a
AC
616 else
617 (dte (WrongPred ("nested action",
618 pd,
619 p));
620 (TError, loc))
621 | (TError, _) => t2
622 | _ =>
623 (dte (WrongForm ("Body of nested action",
624 "action",
625 e2,
626 t2,
627 NONE));
628 (TError, loc)))
629 | (TError, _) => t1
630 | _ =>
631 (dte (WrongForm ("Container of nested action",
632 "action",
633 e1,
634 t1,
635 NONE));
636 (TError, loc))
637 end
638
639 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
640 SM.empty, SM.empty), loc)
27d9de59
AC
641 end
642
643exception Ununif
644
645fun ununif (tAll as (t, loc)) =
646 case t of
647 TBase _ => tAll
648 | TList t => (TList (ununif t), loc)
649 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
650 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
651 | TUnif (_, ref (SOME t)) => ununif t
234b917a 652 | TNested _ => tAll
27d9de59
AC
653 | TError => tAll
654
655 | TUnif (_, ref NONE) => raise Ununif
656
657fun hasError (t, _) =
658 case t of
659 TBase _ => false
660 | TList t => hasError t
661 | TArrow (d, r) => hasError d orelse hasError r
662 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
663 orelse List.exists hasError (SM.listItems r)
234b917a 664 | TNested _ => false
27d9de59
AC
665 | TError => false
666 | TUnif (_, ref (SOME t)) => hasError t
667 | TUnif (_, ref NONE) => false
668
669
670fun checkUnit G (eAll as (_, loc)) =
671 let
672 val _ = resetUnif ()
673 val t = checkExp G eAll
674 in
675 if hasError t then
676 t
677 else
678 ununif t
679 handle Ununif =>
680 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
681 printd (p_typ t);
682 t)
683 end
684
234b917a
AC
685fun checkDecl G (d, _, loc) =
686 case d of
687 DExternType name => bindType G name
492c1cff
AC
688 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
689 | DVal (name, to, e) =>
690 let
691 val to =
692 case to of
693 NONE => (newUnif (), loc)
694 | SOME to => checkTyp G to
695
696 val t = checkExp G e
697 in
6be996d4 698 hasTyp (e, t, to)
492c1cff
AC
699 handle Unify ue =>
700 describe_type_error loc
701 (WrongType ("Bound value",
702 e,
703 t,
704 to,
705 SOME ue));
706 bindVal G (name, to, SOME e)
707 end
095de39e 708 | DContext name => bindContext G name
234b917a 709
095de39e 710fun checkFile G tInit (_, ds, eo) =
234b917a
AC
711 let
712 val G' = foldl (fn (d, G) => checkDecl G d) G ds
713 in
714 case eo of
715 NONE => ()
716 | SOME (e as (_, loc)) =>
717 let
718 val t = checkExp G' e
719 in
6be996d4 720 hasTyp (e, t, tInit)
234b917a
AC
721 handle Unify ue =>
722 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
723 preface ("Actual:", p_typ t);
724 preface ("Needed:", p_typ tInit))
725 end;
726 G'
727 end
728
27d9de59 729end