HCoop / hcoop / domtool2.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Now builds with MLton
[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)
2882ee37
AC		 173 | (CRoot, CNot (CConst _, _)) => true
174 | (CConst s1, CNot (CConst s2, _)) => s1 <> s2
27d9de59 175
db427c67
AC		 176 | _ => false
177
178fun predSimpl (pAll as (p, loc)) =
179 case p of
180 CRoot => pAll
181 | CConst _ => pAll
182 | CPrefix p => (CPrefix (predSimpl p), loc)
183 | CNot p => (CNot (predSimpl p), loc)
184 | CAnd (p1, p2) =>
185 let
186 val p1' = predSimpl p1
187 val p2' = predSimpl p2
188 in
189 case p1' of
190 (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
191 | _ => if predImplies (p2', p1') then
192 p2'
1a4e5a6c
AC		 193 else if predImplies (p1', p2') then
194 p1'
db427c67
AC		 195 else
196 (CAnd (p1', p2'), loc)
197 end
198
234b917a 199fun subPred (p1, p2) =
db427c67
AC		 200 if predImplies (p1, p2) then
201 ()
202 else
203 raise (Unify (UnifyPred (p1, p2)))
27d9de59 204
234b917a
AC		 205fun subRecord f (r1, r2) =
206 SM.appi (fn (k, v2) =>
207 case SM.find (r1, k) of
208 NONE => raise UnequalDomains
209 | SOME v1 => f (v1, v2)) r2
27d9de59
AC		 210
211fun occurs u (t, _) =
212 case t of
213 TBase _ => false
214 | TList t => occurs u t
215 | TArrow (d, r) => occurs u d orelse occurs u r
216 | TAction (_, d, r) =>
217 List.exists (occurs u) (SM.listItems d)
218 orelse List.exists (occurs u) (SM.listItems r)
1a4e5a6c 219 | TNested (_, t) => occurs u t
27d9de59
AC		 220 | TError => false
221 | TUnif (_, ref (SOME t)) => occurs u t
222 | TUnif (_, u') => u = u'
223
234b917a 224fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
27d9de59
AC		 225 case (t1, t2) of
226 (TBase s1, TBase s2) =>
227 if s1 = s2 then
228 ()
229 else
230 raise Unify (UnifyTyp (t1All, t2All))
234b917a 231 | (TList t1, TList t2) => subTyp (t1, t2)
27d9de59 232 | (TArrow (d1, r1), TArrow (d2, r2)) =>
234b917a
AC		 233 (subTyp (d2, d1);
234 subTyp (r1, r2))
27d9de59
AC		 235
236 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
234b917a
AC		 237 ((subPred (p2, p1);
238 subRecord subTyp (d2, d1);
239 subRecord subTyp (r1, r2);
240 subRecord subTyp (r2, r1))
27d9de59
AC		 241 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
242
234b917a
AC		 243 | (TNested (d1, r1), TNested (d2, r2)) =>
244 (subPred (d2, d1);
1a4e5a6c 245 subTyp (r1, r2))
234b917a
AC		 246
247 | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
248 | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
27d9de59
AC		 249
250 | (TUnif (_, r1), TUnif (_, r2)) =>
251 if r1 = r2 then
252 ()
253 else
254 r1 := SOME t2All
255
256 | (TUnif (name, r), _) =>
257 if occurs r t2All then
258 raise (Unify (UnifyOccurs (name, t2All)))
259 else
260 r := SOME t2All
261
262 | (_, TUnif (name, r)) =>
263 if occurs r t1All then
264 raise (Unify (UnifyOccurs (name, t1All)))
265 else
266 r := SOME t1All
267
268 | (TError, _) => ()
269 | (_, TError) => ()
270
271 | _ => raise Unify (UnifyTyp (t1All, t2All))
272
273fun isError t =
274 case t of
275 (TError, _) => true
276 | _ => false
277
db427c67
AC		 278fun whnorm (tAll as (t, loc)) =
279 case t of
280 TUnif (_, ref (SOME tAll)) => whnorm tAll
281 | _ => tAll
282
629a34f6
AC		 283fun baseCondition t =
284 case whnorm t of
285 (TBase name, _) => typeRule name
286 | (TList t, _) =>
287 (case baseCondition t of
288 NONE => NONE
289 | SOME f => SOME (fn (EList ls, _) => List.all f ls
290 | _ => false))
291 | _ => NONE
292
6be996d4 293fun hasTyp (e, t1, t2) =
629a34f6
AC		 294 if (case baseCondition t2 of
295 NONE => false
296 | SOME rule => rule e) then
297 ()
298 else
299 subTyp (t1, t2)
6be996d4 300
095de39e
AC		 301fun checkPred G (p, loc) =
302 let
303 val err = ErrorMsg.error (SOME loc)
304 in
305 case p of
306 CRoot => ()
307 | CConst s =>
308 if lookupContext G s then
309 ()
310 else
311 err ("Unbound context " ^ s)
312 | CPrefix p => checkPred G p
313 | CNot p => checkPred G p
314 | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
315 end
316
234b917a
AC		 317fun checkTyp G (tAll as (t, loc)) =
318 let
319 val err = ErrorMsg.error (SOME loc)
320 in
321 case t of
322 TBase name =>
323 if lookupType G name then
324 tAll
325 else
326 (err ("Unbound type name " ^ name);
327 (TError, loc))
328 | TList t => (TList (checkTyp G t), loc)
329 | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
095de39e
AC		 330 | TAction (p, d, r) => (checkPred G p;
331 (TAction (p, SM.map (checkTyp G) d,
332 SM.map (checkTyp G) r), loc))
333 | TNested (p, t) => (checkPred G p;
334 (TNested (p, checkTyp G t), loc))
234b917a
AC		 335 | TError => raise Fail "TError in parser-generated type"
336 | TUnif _ => raise Fail "TUnif in parser-generated type"
337 end
338
8a7c40fa
AC		 339fun envVarSetFrom v (e, _) =
340 case e of
341 ESet (v', e) =>
342 if v = v' then
343 SOME e
344 else
345 NONE
346 | EGet (_, _, e) => envVarSetFrom v e
347 | ESeq es => foldr (fn (e, found) =>
348 case found of
349 SOME _ => found
350 | NONE => envVarSetFrom v e)
351 NONE es
352 | ELocal (_, e) => envVarSetFrom v e
353
354 | _ => NONE
355
27d9de59
AC		 356fun checkExp G (eAll as (e, loc)) =
357 let
358 val dte = describe_type_error loc
359 in
360 case e of
361 EInt _ => (TBase "int", loc)
362 | EString _ => (TBase "string", loc)
363 | EList es =>
364 let
365 val t = (newUnif (), loc)
366 in
367 foldl (fn (e', ret) =>
368 let
369 val t' = checkExp G e'
370 in
6be996d4 371 (hasTyp (eAll, t', t);
27d9de59
AC		 372 if isError t' then
373 (TList (TError, loc), loc)
374 else
375 ret)
376 handle Unify ue =>
377 (dte (WrongType ("List element",
378 e',
379 t',
380 t,
381 SOME ue));
382 (TError, loc))
383 end) (TList t, loc) es
384 end
385
386 | ELam (x, to, e) =>
387 let
388 val t =
389 case to of
390 NONE => (newUnif (), loc)
234b917a 391 | SOME t => checkTyp G t
27d9de59 392
492c1cff 393 val G' = bindVal G (x, t, NONE)
27d9de59
AC		 394 val t' = checkExp G' e
395 in
396 (TArrow (t, t'), loc)
397 end
398 | EVar x =>
234b917a 399 (case lookupVal G x of
27d9de59
AC		 400 NONE => (dte (UnboundVariable x);
401 (TError, loc))
402 | SOME t => t)
403 | EApp (func, arg) =>
404 let
405 val dom = (newUnif (), loc)
406 val ran = (newUnif (), loc)
407
408 val tf = checkExp G func
409 val ta = checkExp G arg
410 in
6be996d4
AC		 411 (hasTyp (func, tf, (TArrow (dom, ran), loc));
412 hasTyp (arg, ta, dom)
27d9de59
AC		 413 handle Unify ue =>
414 dte (WrongType ("Function argument",
415 arg,
416 ta,
417 dom,
418 SOME ue));
419 ran)
420 handle Unify ue =>
421 (dte (WrongForm ("Function to be applied",
422 "function",
423 func,
424 tf,
425 SOME ue));
426 (TError, loc))
427 end
db427c67 428
6bb366c5
AC		 429 | EALam (x, p, e) =>
430 let
431 val p' = checkPred G p
432
433 val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
434 val t' = checkExp G' e
435 in
436 case t' of
437 (TAction _, _) => (TNested (p, t'), loc)
438 | _ => (dte (WrongForm ("Body of nested configuration 'fn'",
439 "action",
440 e,
441 t',
442 NONE));
443 (TError, loc))
444 end
445
db427c67
AC		 446 | ESet (evar, e) =>
447 let
448 val t = checkExp G e
449 in
450 (TAction ((CPrefix (CRoot, loc), loc),
451 SM.empty,
452 SM.insert (SM.empty, evar, t)),
453 loc)
454 end
455 | EGet (x, evar, rest) =>
456 let
457 val xt = (newUnif (), loc)
492c1cff 458 val G' = bindVal G (x, xt, NONE)
db427c67
AC		 459
460 val rt = whnorm (checkExp G' rest)
461 in
462 case rt of
463 (TAction (p, d, r), _) =>
464 (case SM.find (d, evar) of
465 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
466 | SOME xt' =>
234b917a 467 (subTyp (xt', xt)
db427c67
AC		 468 handle Unify ue =>
469 dte (WrongType ("Retrieved environment variable",
470 (EVar x, loc),
471 xt',
472 xt,
473 SOME ue));
474 rt))
234b917a 475 | (TError, _) => rt
db427c67
AC		 476 | _ => (dte (WrongForm ("Body of environment variable read",
477 "action",
478 rest,
479 rt,
480 NONE));
481 (TError, loc))
482 end
483
484 | ESeq [] => raise Fail "Empty ESeq"
485 | ESeq [e1] => checkExp G e1
486 | ESeq (e1 :: rest) =>
487 let
488 val e2 = (ESeq rest, loc)
489
490 val t1 = whnorm (checkExp G e1)
491 val t2 = whnorm (checkExp G e2)
492 in
493 case t1 of
494 (TAction (p1, d1, r1), _) =>
495 (case t2 of
496 (TAction (p2, d2, r2), _) =>
497 let
498 val p' = predSimpl (CAnd (p1, p2), loc)
499
500 val d' = SM.foldli (fn (name, t, d') =>
501 case SM.find (r1, name) of
502 NONE =>
503 (case SM.find (d', name) of
504 NONE => SM.insert (d', name, t)
505 | SOME t' =>
8a7c40fa
AC		 506 ((case envVarSetFrom name e1 of
507 NONE => subTyp (t, t')
508 | SOME e => hasTyp (e, t, t'))
db427c67
AC		 509 handle Unify ue =>
510 dte (WrongType ("Shared environment variable",
511 (EVar name, loc),
db427c67 512 t',
8a7c40fa 513 t,
db427c67
AC		 514 SOME ue));
515 d'))
516 | SOME t' =>
8a7c40fa
AC		 517 ((case envVarSetFrom name e1 of
518 NONE => subTyp (t, t')
519 | SOME e => hasTyp (e, t, t'))
db427c67
AC		 520 handle Unify ue =>
521 dte (WrongType ("Shared environment variable",
522 (EVar name, loc),
db427c67 523 t',
8a7c40fa 524 t,
db427c67
AC		 525 SOME ue));
526 d'))
527 d1 d2
528
529 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
530 r1 r2
531 in
532 (TAction (p', d', r'), loc)
533 end
234b917a 534 | (TError, _) => t2
db427c67
AC		 535 | _ => (dte (WrongForm ("Action to be sequenced",
536 "action",
537 e2,
538 t2,
539 NONE));
540 (TError, loc)))
234b917a 541 | (TError, _) => t1
db427c67
AC		 542 | _ => (dte (WrongForm ("Action to be sequenced",
543 "action",
544 e1,
545 t1,
546 NONE));
547 (TError, loc))
548 end
549
1a4e5a6c 550 | ELocal (e1, e2) =>
db427c67 551 let
1a4e5a6c
AC		 552 val t1 = whnorm (checkExp G e1)
553 val t2 = whnorm (checkExp G e2)
db427c67 554 in
1a4e5a6c
AC		 555 case t1 of
556 (TAction (p1, d1, r1), _) =>
557 (case t2 of
558 (TAction (p2, d2, r2), _) =>
559 let
560 val p' = predSimpl (CAnd (p1, p2), loc)
561
562 val d' = SM.foldli (fn (name, t, d') =>
563 case SM.find (r1, name) of
564 NONE =>
565 (case SM.find (d', name) of
566 NONE => SM.insert (d', name, t)
567 | SOME t' =>
8a7c40fa
AC		 568 ((case envVarSetFrom name e1 of
569 NONE => subTyp (t', t)
570 | SOME e => hasTyp (e, t', t))
1a4e5a6c
AC		 571 handle Unify ue =>
572 dte (WrongType ("Shared environment variable",
573 (EVar name, loc),
1a4e5a6c 574 t',
8a7c40fa 575 t,
1a4e5a6c
AC		 576 SOME ue));
577 d'))
578 | SOME t' =>
8a7c40fa
AC		 579 ((case envVarSetFrom name e1 of
580 NONE => subTyp (t', t)
581 | SOME e => hasTyp (e, t', t))
1a4e5a6c
AC		 582 handle Unify ue =>
583 dte (WrongType ("Shared environment variable",
584 (EVar name, loc),
1a4e5a6c 585 t',
8a7c40fa 586 t,
1a4e5a6c
AC		 587 SOME ue));
588 d'))
589 d1 d2
590 in
591 (TAction (p', d', r2), loc)
592 end
593 | (TError, _) => t2
594 | _ => (dte (WrongForm ("Action to be sequenced",
595 "action",
596 e2,
597 t2,
598 NONE));
599 (TError, loc)))
600 | (TError, _) => t1
601 | _ => (dte (WrongForm ("Action to be sequenced",
db427c67 602 "action",
1a4e5a6c
AC		 603 e1,
604 t1,
db427c67
AC		 605 NONE));
606 (TError, loc))
607 end
234b917a 608
1a4e5a6c 609
234b917a
AC		 610 | EWith (e1, e2) =>
611 let
612 val t1 = whnorm (checkExp G e1)
613 val t2 = whnorm (checkExp G e2)
614 in
615 case t1 of
1a4e5a6c 616 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a
AC		 617 (case t2 of
618 (TAction (p, d, r), _) =>
619 if predImplies (pd, p) then
1a4e5a6c
AC		 620 let
621 val combineRecs =
622 SM.unionWithi (fn (name, t1, t2) =>
623 (subTyp (t1, t2)
624 handle Unify ue =>
625 dte (WrongType ("Environment variable",
626 (EVar name, loc),
627 t1,
628 t2,
629 SOME ue));
630 t2))
631 in
632 (TAction (pr, combineRecs (d, d1),
633 combineRecs (r, r1)), loc)
634 end
234b917a
AC		 635 else
636 (dte (WrongPred ("nested action",
637 pd,
638 p));
639 (TError, loc))
640 | (TError, _) => t2
641 | _ =>
642 (dte (WrongForm ("Body of nested action",
643 "action",
644 e2,
645 t2,
646 NONE));
647 (TError, loc)))
648 | (TError, _) => t1
649 | _ =>
650 (dte (WrongForm ("Container of nested action",
651 "action",
652 e1,
653 t1,
654 NONE));
655 (TError, loc))
656 end
657
658 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
659 SM.empty, SM.empty), loc)
27d9de59
AC		 660 end
661
662exception Ununif
663
664fun ununif (tAll as (t, loc)) =
665 case t of
666 TBase _ => tAll
667 | TList t => (TList (ununif t), loc)
668 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
669 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
670 | TUnif (_, ref (SOME t)) => ununif t
234b917a 671 | TNested _ => tAll
27d9de59
AC		 672 | TError => tAll
673
674 | TUnif (_, ref NONE) => raise Ununif
675
676fun hasError (t, _) =
677 case t of
678 TBase _ => false
679 | TList t => hasError t
680 | TArrow (d, r) => hasError d orelse hasError r
681 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
682 orelse List.exists hasError (SM.listItems r)
234b917a 683 | TNested _ => false
27d9de59
AC		 684 | TError => false
685 | TUnif (_, ref (SOME t)) => hasError t
686 | TUnif (_, ref NONE) => false
687
688
689fun checkUnit G (eAll as (_, loc)) =
690 let
691 val _ = resetUnif ()
692 val t = checkExp G eAll
693 in
694 if hasError t then
695 t
696 else
697 ununif t
698 handle Ununif =>
699 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
700 printd (p_typ t);
701 t)
702 end
703
234b917a
AC		 704fun checkDecl G (d, _, loc) =
705 case d of
706 DExternType name => bindType G name
492c1cff
AC		 707 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
708 | DVal (name, to, e) =>
709 let
710 val to =
711 case to of
712 NONE => (newUnif (), loc)
713 | SOME to => checkTyp G to
714
715 val t = checkExp G e
716 in
6be996d4 717 hasTyp (e, t, to)
492c1cff
AC		 718 handle Unify ue =>
719 describe_type_error loc
720 (WrongType ("Bound value",
721 e,
722 t,
723 to,
724 SOME ue));
725 bindVal G (name, to, SOME e)
726 end
095de39e 727 | DContext name => bindContext G name
234b917a 728
095de39e 729fun checkFile G tInit (_, ds, eo) =
234b917a
AC		 730 let
731 val G' = foldl (fn (d, G) => checkDecl G d) G ds
732 in
733 case eo of
734 NONE => ()
735 | SOME (e as (_, loc)) =>
736 let
737 val t = checkExp G' e
738 in
6be996d4 739 hasTyp (e, t, tInit)
234b917a
AC		 740 handle Unify ue =>
741 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
742 preface ("Actual:", p_typ t);
743 preface ("Needed:", p_typ tInit))
744 end;
745 G'
746 end
747
27d9de59 748end
Unnamed repository; edit this file to name it for gitweb.