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