ac69a6d4483f6f626c9c145038e5116fc6944600
[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 checkTyp G (tAll as (t, loc)) =
300 let
301 val err = ErrorMsg.error (SOME loc)
302 in
303 case t of
304 TBase name =>
305 if lookupType G name then
306 tAll
307 else
308 (err ("Unbound type name " ^ name);
309 (TError, loc))
310 | TList t => (TList (checkTyp G t), loc)
311 | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
312 | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
313 SM.map (checkTyp G) r), loc)
314 | TNested (p, t) => (TNested (p, checkTyp G t), loc)
315 | TError => raise Fail "TError in parser-generated type"
316 | TUnif _ => raise Fail "TUnif in parser-generated type"
317 end
318
319 fun checkExp G (eAll as (e, loc)) =
320 let
321 val dte = describe_type_error loc
322 in
323 case e of
324 EInt _ => (TBase "int", loc)
325 | EString _ => (TBase "string", loc)
326 | EList es =>
327 let
328 val t = (newUnif (), loc)
329 in
330 foldl (fn (e', ret) =>
331 let
332 val t' = checkExp G e'
333 in
334 (hasTyp (eAll, t', t);
335 if isError t' then
336 (TList (TError, loc), loc)
337 else
338 ret)
339 handle Unify ue =>
340 (dte (WrongType ("List element",
341 e',
342 t',
343 t,
344 SOME ue));
345 (TError, loc))
346 end) (TList t, loc) es
347 end
348
349 | ELam (x, to, e) =>
350 let
351 val t =
352 case to of
353 NONE => (newUnif (), loc)
354 | SOME t => checkTyp G t
355
356 val G' = bindVal G (x, t, NONE)
357 val t' = checkExp G' e
358 in
359 (TArrow (t, t'), loc)
360 end
361 | EVar x =>
362 (case lookupVal G x of
363 NONE => (dte (UnboundVariable x);
364 (TError, loc))
365 | SOME t => t)
366 | EApp (func, arg) =>
367 let
368 val dom = (newUnif (), loc)
369 val ran = (newUnif (), loc)
370
371 val tf = checkExp G func
372 val ta = checkExp G arg
373 in
374 (hasTyp (func, tf, (TArrow (dom, ran), loc));
375 hasTyp (arg, ta, dom)
376 handle Unify ue =>
377 dte (WrongType ("Function argument",
378 arg,
379 ta,
380 dom,
381 SOME ue));
382 ran)
383 handle Unify ue =>
384 (dte (WrongForm ("Function to be applied",
385 "function",
386 func,
387 tf,
388 SOME ue));
389 (TError, loc))
390 end
391
392 | ESet (evar, e) =>
393 let
394 val t = checkExp G e
395 in
396 (TAction ((CPrefix (CRoot, loc), loc),
397 SM.empty,
398 SM.insert (SM.empty, evar, t)),
399 loc)
400 end
401 | EGet (x, evar, rest) =>
402 let
403 val xt = (newUnif (), loc)
404 val G' = bindVal G (x, xt, NONE)
405
406 val rt = whnorm (checkExp G' rest)
407 in
408 case rt of
409 (TAction (p, d, r), _) =>
410 (case SM.find (d, evar) of
411 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
412 | SOME xt' =>
413 (subTyp (xt', xt)
414 handle Unify ue =>
415 dte (WrongType ("Retrieved environment variable",
416 (EVar x, loc),
417 xt',
418 xt,
419 SOME ue));
420 rt))
421 | (TError, _) => rt
422 | _ => (dte (WrongForm ("Body of environment variable read",
423 "action",
424 rest,
425 rt,
426 NONE));
427 (TError, loc))
428 end
429
430 | ESeq [] => raise Fail "Empty ESeq"
431 | ESeq [e1] => checkExp G e1
432 | ESeq (e1 :: rest) =>
433 let
434 val e2 = (ESeq rest, loc)
435
436 val t1 = whnorm (checkExp G e1)
437 val t2 = whnorm (checkExp G e2)
438 in
439 case t1 of
440 (TAction (p1, d1, r1), _) =>
441 (case t2 of
442 (TAction (p2, d2, r2), _) =>
443 let
444 val p' = predSimpl (CAnd (p1, p2), loc)
445
446 val d' = SM.foldli (fn (name, t, d') =>
447 case SM.find (r1, name) of
448 NONE =>
449 (case SM.find (d', name) of
450 NONE => SM.insert (d', name, t)
451 | SOME t' =>
452 (subTyp (t, t')
453 handle Unify ue =>
454 dte (WrongType ("Shared environment variable",
455 (EVar name, loc),
456 t,
457 t',
458 SOME ue));
459 d'))
460 | SOME t' =>
461 (subTyp (t, t')
462 handle Unify ue =>
463 dte (WrongType ("Shared environment variable",
464 (EVar name, loc),
465 t,
466 t',
467 SOME ue));
468 d'))
469 d1 d2
470
471 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
472 r1 r2
473 in
474 (TAction (p', d', r'), loc)
475 end
476 | (TError, _) => t2
477 | _ => (dte (WrongForm ("Action to be sequenced",
478 "action",
479 e2,
480 t2,
481 NONE));
482 (TError, loc)))
483 | (TError, _) => t1
484 | _ => (dte (WrongForm ("Action to be sequenced",
485 "action",
486 e1,
487 t1,
488 NONE));
489 (TError, loc))
490 end
491
492 | ELocal (e1, e2) =>
493 let
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' =>
510 (subTyp (t, t')
511 handle Unify ue =>
512 dte (WrongType ("Shared environment variable",
513 (EVar name, loc),
514 t,
515 t',
516 SOME ue));
517 d'))
518 | SOME t' =>
519 (subTyp (t, t')
520 handle Unify ue =>
521 dte (WrongType ("Shared environment variable",
522 (EVar name, loc),
523 t,
524 t',
525 SOME ue));
526 d'))
527 d1 d2
528 in
529 (TAction (p', d', r2), loc)
530 end
531 | (TError, _) => t2
532 | _ => (dte (WrongForm ("Action to be sequenced",
533 "action",
534 e2,
535 t2,
536 NONE));
537 (TError, loc)))
538 | (TError, _) => t1
539 | _ => (dte (WrongForm ("Action to be sequenced",
540 "action",
541 e1,
542 t1,
543 NONE));
544 (TError, loc))
545 end
546
547
548 | EWith (e1, e2) =>
549 let
550 val t1 = whnorm (checkExp G e1)
551 val t2 = whnorm (checkExp G e2)
552 in
553 case t1 of
554 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
555 (case t2 of
556 (TAction (p, d, r), _) =>
557 if predImplies (pd, p) then
558 let
559 val combineRecs =
560 SM.unionWithi (fn (name, t1, t2) =>
561 (subTyp (t1, t2)
562 handle Unify ue =>
563 dte (WrongType ("Environment variable",
564 (EVar name, loc),
565 t1,
566 t2,
567 SOME ue));
568 t2))
569 in
570 (TAction (pr, combineRecs (d, d1),
571 combineRecs (r, r1)), loc)
572 end
573 else
574 (dte (WrongPred ("nested action",
575 pd,
576 p));
577 (TError, loc))
578 | (TError, _) => t2
579 | _ =>
580 (dte (WrongForm ("Body of nested action",
581 "action",
582 e2,
583 t2,
584 NONE));
585 (TError, loc)))
586 | (TError, _) => t1
587 | _ =>
588 (dte (WrongForm ("Container of nested action",
589 "action",
590 e1,
591 t1,
592 NONE));
593 (TError, loc))
594 end
595
596 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
597 SM.empty, SM.empty), loc)
598 end
599
600 exception Ununif
601
602 fun ununif (tAll as (t, loc)) =
603 case t of
604 TBase _ => tAll
605 | TList t => (TList (ununif t), loc)
606 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
607 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
608 | TUnif (_, ref (SOME t)) => ununif t
609 | TNested _ => tAll
610 | TError => tAll
611
612 | TUnif (_, ref NONE) => raise Ununif
613
614 fun hasError (t, _) =
615 case t of
616 TBase _ => false
617 | TList t => hasError t
618 | TArrow (d, r) => hasError d orelse hasError r
619 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
620 orelse List.exists hasError (SM.listItems r)
621 | TNested _ => false
622 | TError => false
623 | TUnif (_, ref (SOME t)) => hasError t
624 | TUnif (_, ref NONE) => false
625
626
627 fun checkUnit G (eAll as (_, loc)) =
628 let
629 val _ = resetUnif ()
630 val t = checkExp G eAll
631 in
632 if hasError t then
633 t
634 else
635 ununif t
636 handle Ununif =>
637 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
638 printd (p_typ t);
639 t)
640 end
641
642 fun checkDecl G (d, _, loc) =
643 case d of
644 DExternType name => bindType G name
645 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
646 | DVal (name, to, e) =>
647 let
648 val to =
649 case to of
650 NONE => (newUnif (), loc)
651 | SOME to => checkTyp G to
652
653 val t = checkExp G e
654 in
655 hasTyp (e, t, to)
656 handle Unify ue =>
657 describe_type_error loc
658 (WrongType ("Bound value",
659 e,
660 t,
661 to,
662 SOME ue));
663 bindVal G (name, to, SOME e)
664 end
665
666 fun checkFile G tInit (ds, eo) =
667 let
668 val G' = foldl (fn (d, G) => checkDecl G d) G ds
669 in
670 case eo of
671 NONE => ()
672 | SOME (e as (_, loc)) =>
673 let
674 val t = checkExp G' e
675 in
676 hasTyp (e, t, tInit)
677 handle Unify ue =>
678 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
679 preface ("Actual:", p_typ t);
680 preface ("Needed:", p_typ tInit))
681 end;
682 G'
683 end
684
685 end