Fix file paths for recursive rmdom
[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 val externFlag = ref false
28 fun allowExterns () = externFlag := true
29 fun disallowExterns () = externFlag := false
30
31 local
32 val unifCount = ref 0
33 in
34 fun resetUnif () = unifCount := 0
35
36 fun 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
48 end
49
50 exception UnequalDomains
51
52 fun 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
72 fun 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
83 fun 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
94 | (TNested (p1, q1), TNested (p2, q2)) =>
95 eqPred (p1, p2) andalso eqTy (q1, q2)
96
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
106 datatype unification_error =
107 UnifyPred of pred * pred
108 | UnifyTyp of typ * typ
109 | UnifyOccurs of string * typ
110
111 exception Unify of unification_error
112
113 datatype 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
117 | WrongPred of string * pred * pred
118
119 fun describe_unification_error t ue =
120 case ue of
121 UnifyPred (p1, p2) =>
122 (print "Reason: Incompatible contexts.\n";
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
141 fun 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")
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))
160
161 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
162 case (p1, p2) of
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
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)
174 | (_, CPrefix p2) => predImplies (p1All, p2)
175
176 | (CNot p1, CNot p2) => predImplies (p2, p1)
177 | (CRoot, CNot (CConst _, _)) => true
178 | (CConst s1, CNot (CConst s2, _)) => s1 <> s2
179
180 | _ => false
181
182 fun 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'
197 else if predImplies (p1', p2') then
198 p1'
199 else
200 (CAnd (p1', p2'), loc)
201 end
202
203 fun subPred (p1, p2) =
204 if predImplies (p1, p2) then
205 ()
206 else
207 raise (Unify (UnifyPred (p1, p2)))
208
209 fun 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
214
215 fun 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)
223 | TNested (_, t) => occurs u t
224 | TError => false
225 | TUnif (_, ref (SOME t)) => occurs u t
226 | TUnif (_, u') => u = u'
227
228 fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
229 case (t1, t2) of
230 (TBase s1, TBase s2) =>
231 if s1 = s2 then
232 ()
233 else
234 raise Unify (UnifyTyp (t1All, t2All))
235 | (TList t1, TList t2) => subTyp (t1, t2)
236 | (TArrow (d1, r1), TArrow (d2, r2)) =>
237 (subTyp (d2, d1);
238 subTyp (r1, r2))
239
240 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
241 ((subPred (p2, p1);
242 subRecord subTyp (d2, d1);
243 subRecord subTyp (r1, r2);
244 subRecord subTyp (r2, r1))
245 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
246
247 | (TNested (d1, r1), TNested (d2, r2)) =>
248 (subPred (d2, d1);
249 subTyp (r1, r2))
250
251 | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
252 | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
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
277 fun isError t =
278 case t of
279 (TError, _) => true
280 | _ => false
281
282 fun whnorm (tAll as (t, loc)) =
283 case t of
284 TUnif (_, ref (SOME tAll)) => whnorm tAll
285 | _ => tAll
286
287 fun 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
297 fun hasTyp (e, t1, t2) =
298 if (case baseCondition t2 of
299 NONE => false
300 | SOME rule => rule e) then
301 ()
302 else
303 subTyp (t1, t2)
304
305 fun 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
321 fun 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)
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))
339 | TError => raise Fail "TError in parser-generated type"
340 | TUnif _ => raise Fail "TUnif in parser-generated type"
341 end
342
343 fun 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
360 fun 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
375 (hasTyp (eAll, t', t);
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)
395 | SOME t => checkTyp G t
396
397 val G' = bindVal G (x, t, NONE)
398 val t' = checkExp G' e
399 in
400 (TArrow (t, t'), loc)
401 end
402 | EVar x =>
403 (case lookupVal G x of
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
415 (hasTyp (func, tf, (TArrow (dom, ran), loc));
416 hasTyp (arg, ta, dom)
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
432
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)
438 val t' = whnorm (checkExp G' e)
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
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)
462 val G' = bindVal G (x, xt, NONE)
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' =>
471 (subTyp (xt', xt)
472 handle Unify ue =>
473 dte (WrongType ("Retrieved environment variable",
474 (EVar x, loc),
475 xt',
476 xt,
477 SOME ue));
478 rt))
479 | (TError, _) => rt
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' =>
510 ((case envVarSetFrom name e1 of
511 NONE => subTyp (t, t')
512 | SOME e => hasTyp (e, t, t'))
513 handle Unify ue =>
514 dte (WrongType ("Shared environment variable",
515 (EVar name, loc),
516 t',
517 t,
518 SOME ue));
519 d'))
520 | SOME t' =>
521 ((case envVarSetFrom name e1 of
522 NONE => subTyp (t, t')
523 | SOME e => hasTyp (e, t, t'))
524 handle Unify ue =>
525 dte (WrongType ("Shared environment variable",
526 (EVar name, loc),
527 t',
528 t,
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
538 | (TError, _) => t2
539 | _ => (dte (WrongForm ("Action to be sequenced",
540 "action",
541 e2,
542 t2,
543 NONE));
544 (TError, loc)))
545 | (TError, _) => t1
546 | _ => (dte (WrongForm ("Action to be sequenced",
547 "action",
548 e1,
549 t1,
550 NONE));
551 (TError, loc))
552 end
553
554 | ELocal (e1, e2) =>
555 let
556 val t1 = whnorm (checkExp G e1)
557 val t2 = whnorm (checkExp G e2)
558 in
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' =>
572 ((case envVarSetFrom name e1 of
573 NONE => subTyp (t', t)
574 | SOME e => hasTyp (e, t', t))
575 handle Unify ue =>
576 dte (WrongType ("Shared environment variable",
577 (EVar name, loc),
578 t',
579 t,
580 SOME ue));
581 d'))
582 | SOME t' =>
583 ((case envVarSetFrom name e1 of
584 NONE => subTyp (t', t)
585 | SOME e => hasTyp (e, t', t))
586 handle Unify ue =>
587 dte (WrongType ("Shared environment variable",
588 (EVar name, loc),
589 t',
590 t,
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",
606 "action",
607 e1,
608 t1,
609 NONE));
610 (TError, loc))
611 end
612
613
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
620 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
621 (case t2 of
622 (TAction (p, d, r), _) =>
623 if predImplies (pd, p) then
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
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)
664 end
665
666 exception Ununif
667
668 fun 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
675 | TNested _ => tAll
676 | TError => tAll
677
678 | TUnif (_, ref NONE) => raise Ununif
679
680 fun 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)
687 | TNested _ => false
688 | TError => false
689 | TUnif (_, ref (SOME t)) => hasError t
690 | TUnif (_, ref NONE) => false
691
692
693 fun 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
708 fun checkDecl G (d, _, loc) =
709 case d of
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)
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
731 hasTyp (e, t, to)
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
741 | DContext name => bindContext G name
742
743 fun checkFile G tInit (_, ds, eo) =
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
753 hasTyp (e, t, tInit)
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
762 end