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