Dependency ordering
[hcoop/domtool2.git] / src / tycheck.sml
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.
17 *)
18
19 (* Domtool configuration language type checking *)
20
21 structure Tycheck :> TYCHECK = struct
22
23 open Ast Print Env
24
25 structure SM = StringMap
26
27 local
28 val unifCount = ref 0
29 in
30 fun resetUnif () = unifCount := 0
31
32 fun 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
44 end
45
46 exception UnequalDomains
47
48 fun 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
68 fun 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
79 fun 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
90 | (TNested (p1, q1), TNested (p2, q2)) =>
91 eqPred (p1, p2) andalso eqTy (q1, q2)
92
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
102 datatype unification_error =
103 UnifyPred of pred * pred
104 | UnifyTyp of typ * typ
105 | UnifyOccurs of string * typ
106
107 exception Unify of unification_error
108
109 datatype 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
113 | WrongPred of string * pred * pred
114
115 fun describe_unification_error t ue =
116 case ue of
117 UnifyPred (p1, p2) =>
118 (print "Reason: Incompatible contexts.\n";
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
137 fun 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")
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))
156
157 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
158 case (p1, p2) of
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
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)
170 | (_, CPrefix p2) => predImplies (p1All, p2)
171
172 | (CNot p1, CNot p2) => predImplies (p2, p1)
173
174 | _ => false
175
176 fun 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'
191 else if predImplies (p1', p2') then
192 p1'
193 else
194 (CAnd (p1', p2'), loc)
195 end
196
197 fun subPred (p1, p2) =
198 if predImplies (p1, p2) then
199 ()
200 else
201 raise (Unify (UnifyPred (p1, p2)))
202
203 fun 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
208
209 fun 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)
217 | TNested (_, t) => occurs u t
218 | TError => false
219 | TUnif (_, ref (SOME t)) => occurs u t
220 | TUnif (_, u') => u = u'
221
222 fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
223 case (t1, t2) of
224 (TBase s1, TBase s2) =>
225 if s1 = s2 then
226 ()
227 else
228 raise Unify (UnifyTyp (t1All, t2All))
229 | (TList t1, TList t2) => subTyp (t1, t2)
230 | (TArrow (d1, r1), TArrow (d2, r2)) =>
231 (subTyp (d2, d1);
232 subTyp (r1, r2))
233
234 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
235 ((subPred (p2, p1);
236 subRecord subTyp (d2, d1);
237 subRecord subTyp (r1, r2);
238 subRecord subTyp (r2, r1))
239 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
240
241 | (TNested (d1, r1), TNested (d2, r2)) =>
242 (subPred (d2, d1);
243 subTyp (r1, r2))
244
245 | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
246 | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
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
271 fun isError t =
272 case t of
273 (TError, _) => true
274 | _ => false
275
276 fun whnorm (tAll as (t, loc)) =
277 case t of
278 TUnif (_, ref (SOME tAll)) => whnorm tAll
279 | _ => tAll
280
281 fun 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
291 fun hasTyp (e, t1, t2) =
292 if (case baseCondition t2 of
293 NONE => false
294 | SOME rule => rule e) then
295 ()
296 else
297 subTyp (t1, t2)
298
299 fun 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
315 fun 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)
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))
333 | TError => raise Fail "TError in parser-generated type"
334 | TUnif _ => raise Fail "TUnif in parser-generated type"
335 end
336
337 fun checkExp G (eAll as (e, loc)) =
338 let
339 val dte = describe_type_error loc
340 in
341 case e of
342 EInt _ => (TBase "int", loc)
343 | EString _ => (TBase "string", loc)
344 | EList es =>
345 let
346 val t = (newUnif (), loc)
347 in
348 foldl (fn (e', ret) =>
349 let
350 val t' = checkExp G e'
351 in
352 (hasTyp (eAll, t', t);
353 if isError t' then
354 (TList (TError, loc), loc)
355 else
356 ret)
357 handle Unify ue =>
358 (dte (WrongType ("List element",
359 e',
360 t',
361 t,
362 SOME ue));
363 (TError, loc))
364 end) (TList t, loc) es
365 end
366
367 | ELam (x, to, e) =>
368 let
369 val t =
370 case to of
371 NONE => (newUnif (), loc)
372 | SOME t => checkTyp G t
373
374 val G' = bindVal G (x, t, NONE)
375 val t' = checkExp G' e
376 in
377 (TArrow (t, t'), loc)
378 end
379 | EVar x =>
380 (case lookupVal G x of
381 NONE => (dte (UnboundVariable x);
382 (TError, loc))
383 | SOME t => t)
384 | EApp (func, arg) =>
385 let
386 val dom = (newUnif (), loc)
387 val ran = (newUnif (), loc)
388
389 val tf = checkExp G func
390 val ta = checkExp G arg
391 in
392 (hasTyp (func, tf, (TArrow (dom, ran), loc));
393 hasTyp (arg, ta, dom)
394 handle Unify ue =>
395 dte (WrongType ("Function argument",
396 arg,
397 ta,
398 dom,
399 SOME ue));
400 ran)
401 handle Unify ue =>
402 (dte (WrongForm ("Function to be applied",
403 "function",
404 func,
405 tf,
406 SOME ue));
407 (TError, loc))
408 end
409
410 | ESet (evar, e) =>
411 let
412 val t = checkExp G e
413 in
414 (TAction ((CPrefix (CRoot, loc), loc),
415 SM.empty,
416 SM.insert (SM.empty, evar, t)),
417 loc)
418 end
419 | EGet (x, evar, rest) =>
420 let
421 val xt = (newUnif (), loc)
422 val G' = bindVal G (x, xt, NONE)
423
424 val rt = whnorm (checkExp G' rest)
425 in
426 case rt of
427 (TAction (p, d, r), _) =>
428 (case SM.find (d, evar) of
429 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
430 | SOME xt' =>
431 (subTyp (xt', xt)
432 handle Unify ue =>
433 dte (WrongType ("Retrieved environment variable",
434 (EVar x, loc),
435 xt',
436 xt,
437 SOME ue));
438 rt))
439 | (TError, _) => rt
440 | _ => (dte (WrongForm ("Body of environment variable read",
441 "action",
442 rest,
443 rt,
444 NONE));
445 (TError, loc))
446 end
447
448 | ESeq [] => raise Fail "Empty ESeq"
449 | ESeq [e1] => checkExp G e1
450 | ESeq (e1 :: rest) =>
451 let
452 val e2 = (ESeq rest, loc)
453
454 val t1 = whnorm (checkExp G e1)
455 val t2 = whnorm (checkExp G e2)
456 in
457 case t1 of
458 (TAction (p1, d1, r1), _) =>
459 (case t2 of
460 (TAction (p2, d2, r2), _) =>
461 let
462 val p' = predSimpl (CAnd (p1, p2), loc)
463
464 val d' = SM.foldli (fn (name, t, d') =>
465 case SM.find (r1, name) of
466 NONE =>
467 (case SM.find (d', name) of
468 NONE => SM.insert (d', name, t)
469 | SOME t' =>
470 (subTyp (t, t')
471 handle Unify ue =>
472 dte (WrongType ("Shared environment variable",
473 (EVar name, loc),
474 t,
475 t',
476 SOME ue));
477 d'))
478 | SOME t' =>
479 (subTyp (t, t')
480 handle Unify ue =>
481 dte (WrongType ("Shared environment variable",
482 (EVar name, loc),
483 t,
484 t',
485 SOME ue));
486 d'))
487 d1 d2
488
489 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
490 r1 r2
491 in
492 (TAction (p', d', r'), loc)
493 end
494 | (TError, _) => t2
495 | _ => (dte (WrongForm ("Action to be sequenced",
496 "action",
497 e2,
498 t2,
499 NONE));
500 (TError, loc)))
501 | (TError, _) => t1
502 | _ => (dte (WrongForm ("Action to be sequenced",
503 "action",
504 e1,
505 t1,
506 NONE));
507 (TError, loc))
508 end
509
510 | ELocal (e1, e2) =>
511 let
512 val t1 = whnorm (checkExp G e1)
513 val t2 = whnorm (checkExp G e2)
514 in
515 case t1 of
516 (TAction (p1, d1, r1), _) =>
517 (case t2 of
518 (TAction (p2, d2, r2), _) =>
519 let
520 val p' = predSimpl (CAnd (p1, p2), loc)
521
522 val d' = SM.foldli (fn (name, t, d') =>
523 case SM.find (r1, name) of
524 NONE =>
525 (case SM.find (d', name) of
526 NONE => SM.insert (d', name, t)
527 | SOME t' =>
528 (subTyp (t, t')
529 handle Unify ue =>
530 dte (WrongType ("Shared environment variable",
531 (EVar name, loc),
532 t,
533 t',
534 SOME ue));
535 d'))
536 | SOME t' =>
537 (subTyp (t, t')
538 handle Unify ue =>
539 dte (WrongType ("Shared environment variable",
540 (EVar name, loc),
541 t,
542 t',
543 SOME ue));
544 d'))
545 d1 d2
546 in
547 (TAction (p', d', r2), loc)
548 end
549 | (TError, _) => t2
550 | _ => (dte (WrongForm ("Action to be sequenced",
551 "action",
552 e2,
553 t2,
554 NONE));
555 (TError, loc)))
556 | (TError, _) => t1
557 | _ => (dte (WrongForm ("Action to be sequenced",
558 "action",
559 e1,
560 t1,
561 NONE));
562 (TError, loc))
563 end
564
565
566 | EWith (e1, e2) =>
567 let
568 val t1 = whnorm (checkExp G e1)
569 val t2 = whnorm (checkExp G e2)
570 in
571 case t1 of
572 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
573 (case t2 of
574 (TAction (p, d, r), _) =>
575 if predImplies (pd, p) then
576 let
577 val combineRecs =
578 SM.unionWithi (fn (name, t1, t2) =>
579 (subTyp (t1, t2)
580 handle Unify ue =>
581 dte (WrongType ("Environment variable",
582 (EVar name, loc),
583 t1,
584 t2,
585 SOME ue));
586 t2))
587 in
588 (TAction (pr, combineRecs (d, d1),
589 combineRecs (r, r1)), loc)
590 end
591 else
592 (dte (WrongPred ("nested action",
593 pd,
594 p));
595 (TError, loc))
596 | (TError, _) => t2
597 | _ =>
598 (dte (WrongForm ("Body of nested action",
599 "action",
600 e2,
601 t2,
602 NONE));
603 (TError, loc)))
604 | (TError, _) => t1
605 | _ =>
606 (dte (WrongForm ("Container of nested action",
607 "action",
608 e1,
609 t1,
610 NONE));
611 (TError, loc))
612 end
613
614 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
615 SM.empty, SM.empty), loc)
616 end
617
618 exception Ununif
619
620 fun ununif (tAll as (t, loc)) =
621 case t of
622 TBase _ => tAll
623 | TList t => (TList (ununif t), loc)
624 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
625 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
626 | TUnif (_, ref (SOME t)) => ununif t
627 | TNested _ => tAll
628 | TError => tAll
629
630 | TUnif (_, ref NONE) => raise Ununif
631
632 fun hasError (t, _) =
633 case t of
634 TBase _ => false
635 | TList t => hasError t
636 | TArrow (d, r) => hasError d orelse hasError r
637 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
638 orelse List.exists hasError (SM.listItems r)
639 | TNested _ => false
640 | TError => false
641 | TUnif (_, ref (SOME t)) => hasError t
642 | TUnif (_, ref NONE) => false
643
644
645 fun checkUnit G (eAll as (_, loc)) =
646 let
647 val _ = resetUnif ()
648 val t = checkExp G eAll
649 in
650 if hasError t then
651 t
652 else
653 ununif t
654 handle Ununif =>
655 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
656 printd (p_typ t);
657 t)
658 end
659
660 fun checkDecl G (d, _, loc) =
661 case d of
662 DExternType name => bindType G name
663 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
664 | DVal (name, to, e) =>
665 let
666 val to =
667 case to of
668 NONE => (newUnif (), loc)
669 | SOME to => checkTyp G to
670
671 val t = checkExp G e
672 in
673 hasTyp (e, t, to)
674 handle Unify ue =>
675 describe_type_error loc
676 (WrongType ("Bound value",
677 e,
678 t,
679 to,
680 SOME ue));
681 bindVal G (name, to, SOME e)
682 end
683 | DContext name => bindContext G name
684
685 fun checkFile G tInit (_, ds, eo) =
686 let
687 val G' = foldl (fn (d, G) => checkDecl G d) G ds
688 in
689 case eo of
690 NONE => ()
691 | SOME (e as (_, loc)) =>
692 let
693 val t = checkExp G' e
694 in
695 hasTyp (e, t, tInit)
696 handle Unify ue =>
697 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
698 preface ("Actual:", p_typ t);
699 preface ("Needed:", p_typ tInit))
700 end;
701 G'
702 end
703
704 end