HCoop / hcoop / domtool2.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Mailman and Bind fixes
[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
AC		 428
429 | ESet (evar, e) =>
430 let
431 val t = checkExp G e
432 in
433 (TAction ((CPrefix (CRoot, loc), loc),
434 SM.empty,
435 SM.insert (SM.empty, evar, t)),
436 loc)
437 end
438 | EGet (x, evar, rest) =>
439 let
440 val xt = (newUnif (), loc)
492c1cff 441 val G' = bindVal G (x, xt, NONE)
db427c67
AC		 442
443 val rt = whnorm (checkExp G' rest)
444 in
445 case rt of
446 (TAction (p, d, r), _) =>
447 (case SM.find (d, evar) of
448 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
449 | SOME xt' =>
234b917a 450 (subTyp (xt', xt)
db427c67
AC		 451 handle Unify ue =>
452 dte (WrongType ("Retrieved environment variable",
453 (EVar x, loc),
454 xt',
455 xt,
456 SOME ue));
457 rt))
234b917a 458 | (TError, _) => rt
db427c67
AC		 459 | _ => (dte (WrongForm ("Body of environment variable read",
460 "action",
461 rest,
462 rt,
463 NONE));
464 (TError, loc))
465 end
466
467 | ESeq [] => raise Fail "Empty ESeq"
468 | ESeq [e1] => checkExp G e1
469 | ESeq (e1 :: rest) =>
470 let
471 val e2 = (ESeq rest, loc)
472
473 val t1 = whnorm (checkExp G e1)
474 val t2 = whnorm (checkExp G e2)
475 in
476 case t1 of
477 (TAction (p1, d1, r1), _) =>
478 (case t2 of
479 (TAction (p2, d2, r2), _) =>
480 let
481 val p' = predSimpl (CAnd (p1, p2), loc)
482
483 val d' = SM.foldli (fn (name, t, d') =>
484 case SM.find (r1, name) of
485 NONE =>
486 (case SM.find (d', name) of
487 NONE => SM.insert (d', name, t)
488 | SOME t' =>
8a7c40fa
AC		 489 ((case envVarSetFrom name e1 of
490 NONE => subTyp (t, t')
491 | SOME e => hasTyp (e, t, t'))
db427c67
AC		 492 handle Unify ue =>
493 dte (WrongType ("Shared environment variable",
494 (EVar name, loc),
db427c67 495 t',
8a7c40fa 496 t,
db427c67
AC		 497 SOME ue));
498 d'))
499 | SOME t' =>
8a7c40fa
AC		 500 ((case envVarSetFrom name e1 of
501 NONE => subTyp (t, t')
502 | SOME e => hasTyp (e, t, t'))
db427c67
AC		 503 handle Unify ue =>
504 dte (WrongType ("Shared environment variable",
505 (EVar name, loc),
db427c67 506 t',
8a7c40fa 507 t,
db427c67
AC		 508 SOME ue));
509 d'))
510 d1 d2
511
512 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
513 r1 r2
514 in
515 (TAction (p', d', r'), loc)
516 end
234b917a 517 | (TError, _) => t2
db427c67
AC		 518 | _ => (dte (WrongForm ("Action to be sequenced",
519 "action",
520 e2,
521 t2,
522 NONE));
523 (TError, loc)))
234b917a 524 | (TError, _) => t1
db427c67
AC		 525 | _ => (dte (WrongForm ("Action to be sequenced",
526 "action",
527 e1,
528 t1,
529 NONE));
530 (TError, loc))
531 end
532
1a4e5a6c 533 | ELocal (e1, e2) =>
db427c67 534 let
1a4e5a6c
AC		 535 val t1 = whnorm (checkExp G e1)
536 val t2 = whnorm (checkExp G e2)
db427c67 537 in
1a4e5a6c
AC		 538 case t1 of
539 (TAction (p1, d1, r1), _) =>
540 (case t2 of
541 (TAction (p2, d2, r2), _) =>
542 let
543 val p' = predSimpl (CAnd (p1, p2), loc)
544
545 val d' = SM.foldli (fn (name, t, d') =>
546 case SM.find (r1, name) of
547 NONE =>
548 (case SM.find (d', name) of
549 NONE => SM.insert (d', name, t)
550 | SOME t' =>
8a7c40fa
AC		 551 ((case envVarSetFrom name e1 of
552 NONE => subTyp (t', t)
553 | SOME e => hasTyp (e, t', t))
1a4e5a6c
AC		 554 handle Unify ue =>
555 dte (WrongType ("Shared environment variable",
556 (EVar name, loc),
1a4e5a6c 557 t',
8a7c40fa 558 t,
1a4e5a6c
AC		 559 SOME ue));
560 d'))
561 | SOME t' =>
8a7c40fa
AC		 562 ((case envVarSetFrom name e1 of
563 NONE => subTyp (t', t)
564 | SOME e => hasTyp (e, t', t))
1a4e5a6c
AC		 565 handle Unify ue =>
566 dte (WrongType ("Shared environment variable",
567 (EVar name, loc),
1a4e5a6c 568 t',
8a7c40fa 569 t,
1a4e5a6c
AC		 570 SOME ue));
571 d'))
572 d1 d2
573 in
574 (TAction (p', d', r2), loc)
575 end
576 | (TError, _) => t2
577 | _ => (dte (WrongForm ("Action to be sequenced",
578 "action",
579 e2,
580 t2,
581 NONE));
582 (TError, loc)))
583 | (TError, _) => t1
584 | _ => (dte (WrongForm ("Action to be sequenced",
db427c67 585 "action",
1a4e5a6c
AC		 586 e1,
587 t1,
db427c67
AC		 588 NONE));
589 (TError, loc))
590 end
234b917a 591
1a4e5a6c 592
234b917a
AC		 593 | EWith (e1, e2) =>
594 let
595 val t1 = whnorm (checkExp G e1)
596 val t2 = whnorm (checkExp G e2)
597 in
598 case t1 of
1a4e5a6c 599 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a
AC		 600 (case t2 of
601 (TAction (p, d, r), _) =>
602 if predImplies (pd, p) then
1a4e5a6c
AC		 603 let
604 val combineRecs =
605 SM.unionWithi (fn (name, t1, t2) =>
606 (subTyp (t1, t2)
607 handle Unify ue =>
608 dte (WrongType ("Environment variable",
609 (EVar name, loc),
610 t1,
611 t2,
612 SOME ue));
613 t2))
614 in
615 (TAction (pr, combineRecs (d, d1),
616 combineRecs (r, r1)), loc)
617 end
234b917a
AC		 618 else
619 (dte (WrongPred ("nested action",
620 pd,
621 p));
622 (TError, loc))
623 | (TError, _) => t2
624 | _ =>
625 (dte (WrongForm ("Body of nested action",
626 "action",
627 e2,
628 t2,
629 NONE));
630 (TError, loc)))
631 | (TError, _) => t1
632 | _ =>
633 (dte (WrongForm ("Container of nested action",
634 "action",
635 e1,
636 t1,
637 NONE));
638 (TError, loc))
639 end
640
641 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
642 SM.empty, SM.empty), loc)
27d9de59
AC		 643 end
644
645exception Ununif
646
647fun ununif (tAll as (t, loc)) =
648 case t of
649 TBase _ => tAll
650 | TList t => (TList (ununif t), loc)
651 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
652 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
653 | TUnif (_, ref (SOME t)) => ununif t
234b917a 654 | TNested _ => tAll
27d9de59
AC		 655 | TError => tAll
656
657 | TUnif (_, ref NONE) => raise Ununif
658
659fun hasError (t, _) =
660 case t of
661 TBase _ => false
662 | TList t => hasError t
663 | TArrow (d, r) => hasError d orelse hasError r
664 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
665 orelse List.exists hasError (SM.listItems r)
234b917a 666 | TNested _ => false
27d9de59
AC		 667 | TError => false
668 | TUnif (_, ref (SOME t)) => hasError t
669 | TUnif (_, ref NONE) => false
670
671
672fun checkUnit G (eAll as (_, loc)) =
673 let
674 val _ = resetUnif ()
675 val t = checkExp G eAll
676 in
677 if hasError t then
678 t
679 else
680 ununif t
681 handle Ununif =>
682 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
683 printd (p_typ t);
684 t)
685 end
686
234b917a
AC		 687fun checkDecl G (d, _, loc) =
688 case d of
689 DExternType name => bindType G name
492c1cff
AC		 690 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
691 | DVal (name, to, e) =>
692 let
693 val to =
694 case to of
695 NONE => (newUnif (), loc)
696 | SOME to => checkTyp G to
697
698 val t = checkExp G e
699 in
6be996d4 700 hasTyp (e, t, to)
492c1cff
AC		 701 handle Unify ue =>
702 describe_type_error loc
703 (WrongType ("Bound value",
704 e,
705 t,
706 to,
707 SOME ue));
708 bindVal G (name, to, SOME e)
709 end
095de39e 710 | DContext name => bindContext G name
234b917a 711
095de39e 712fun checkFile G tInit (_, ds, eo) =
234b917a
AC		 713 let
714 val G' = foldl (fn (d, G) => checkDecl G d) G ds
715 in
716 case eo of
717 NONE => ()
718 | SOME (e as (_, loc)) =>
719 let
720 val t = checkExp G' e
721 in
6be996d4 722 hasTyp (e, t, tInit)
234b917a
AC		 723 handle Unify ue =>
724 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
725 preface ("Actual:", p_typ t);
726 preface ("Needed:", p_typ tInit))
727 end;
728 G'
729 end
730
27d9de59 731end
Unnamed repository; edit this file to name it for gitweb.