12efce3dfe91086e0a72c423ae3e9ba950d2144c
[hcoop/domtool2.git] / src / tycheck.sml
1 (* HCoop Domtool (http://hcoop.sourceforge.net/)
2 * Copyright (c) 2006-2007, 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
51 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
52 case (p1, p2) of
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
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)
64 | (_, CPrefix p2) => predImplies (p1All, p2)
65
66 | (CNot p1, CNot p2) => predImplies (p2, p1)
67 | (CRoot, CNot (CConst _, _)) => true
68 | (CConst s1, CNot (CConst s2, _)) => s1 <> s2
69
70 | _ => false
71
72 fun 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'
87 else if predImplies (p1', p2') then
88 p1'
89 else
90 (CAnd (p1', p2'), loc)
91 end
92
93 fun subPred (p1, p2) =
94 if predImplies (p1, p2) then
95 ()
96 else
97 raise (Unify (UnifyPred (p1, p2)))
98
99 fun subRecord f (r1, r2) =
100 SM.appi (fn (k, v2) =>
101 case SM.find (r1, k) of
102 NONE => raise Describe.UnequalDomains
103 | SOME v1 => f (v1, v2)) r2
104
105 fun 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)
113 | TNested (_, t) => occurs u t
114 | TError => false
115 | TUnif (_, ref (SOME t)) => occurs u t
116 | TUnif (_, u') => u = u'
117
118 fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
119 case (t1, t2) of
120 (TBase s1, TBase s2) =>
121 if s1 = s2 then
122 ()
123 else
124 raise Unify (UnifyTyp (t1All, t2All))
125 | (TList t1, TList t2) => subTyp (t1, t2)
126 | (TArrow (d1, r1), TArrow (d2, r2)) =>
127 (subTyp (d2, d1);
128 subTyp (r1, r2))
129
130 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
131 ((subPred (p2, p1);
132 subRecord subTyp (d2, d1);
133 subRecord subTyp (r1, r2);
134 subRecord subTyp (r2, r1))
135 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
136
137 | (TNested (d1, r1), TNested (d2, r2)) =>
138 (subPred (d2, d1);
139 subTyp (r1, r2))
140
141 | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
142 | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
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
167 fun isError t =
168 case t of
169 (TError, _) => true
170 | _ => false
171
172 fun whnorm (tAll as (t, loc)) =
173 case t of
174 TUnif (_, ref (SOME tAll)) => whnorm tAll
175 | _ => tAll
176
177 fun 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
187 fun 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
198 fun hasTyp (e, t1, t2) =
199 if (case baseCondition t2 of
200 NONE => false
201 | SOME rule => rule (simplifyKindOf e)) then
202 ()
203 else
204 subTyp (t1, t2)
205
206 fun 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
222 fun 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)
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))
240 | TError => raise Fail "TError in parser-generated type"
241 | TUnif _ => raise Fail "TUnif in parser-generated type"
242 end
243
244 fun envVarSetFrom v (e, _) =
245 case e of
246 ESet (v', e) =>
247 if v = v' then
248 SOME e
249 else
250 NONE
251 | EGet (_, _, _, e) => envVarSetFrom v e
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
261 val ununify = Describe.ununify
262
263 fun checkExp G (eAll as (e, loc)) =
264 let
265 val dte = Describe.describe_type_error loc
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
278 (hasTyp (eAll, t', t);
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)
298 | SOME t => checkTyp G t
299
300 val G' = bindVal G (x, t, NONE)
301 val t' = checkExp G' e
302 in
303 (TArrow (t, t'), loc)
304 end
305 | EVar x =>
306 (case lookupVal G x of
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
318 (hasTyp (func, tf, (TArrow (dom, ran), loc));
319 hasTyp (arg, ta, dom)
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
335
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)
341 val t' = whnorm (checkExp G' e)
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
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
362 | EGet (x, topt, evar, rest) =>
363 let
364 val xt = (newUnif (), loc)
365 val G' = bindVal G (x, xt, NONE)
366
367 val rt = whnorm (checkExp G' rest)
368 in
369 case topt of
370 NONE => ()
371 | SOME t => subTyp (xt, checkTyp G t);
372
373 case ununify rt of
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' =>
378 (subTyp (xt', xt)
379 handle Unify ue =>
380 dte (WrongType ("Retrieved environment variable",
381 (EVar x, loc),
382 xt',
383 xt,
384 SOME ue));
385 rt))
386 | (TError, _) => rt
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' =>
417 ((case envVarSetFrom name e1 of
418 NONE => subTyp (t, t')
419 | SOME e => hasTyp (e, t, t'))
420 handle Unify ue =>
421 dte (WrongType ("Shared environment variable",
422 (EVar name, loc),
423 t',
424 t,
425 SOME ue));
426 d'))
427 | SOME t' =>
428 ((case envVarSetFrom name e1 of
429 NONE => subTyp (t, t')
430 | SOME e => hasTyp (e, t, t'))
431 handle Unify ue =>
432 dte (WrongType ("Shared environment variable",
433 (EVar name, loc),
434 t',
435 t,
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
445 | (TError, _) => t2
446 | _ => (dte (WrongForm ("First action to be sequenced",
447 "action",
448 e2,
449 t2,
450 NONE));
451 (TError, loc)))
452 | (TError, _) => t1
453 | _ => (dte (WrongForm ("Second action to be sequenced",
454 "action",
455 e1,
456 t1,
457 NONE));
458 (TError, loc))
459 end
460
461 | ELocal (e1, e2) =>
462 let
463 val t1 = whnorm (checkExp G e1)
464 val t2 = whnorm (checkExp G e2)
465 in
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' =>
479 ((case envVarSetFrom name e1 of
480 NONE => subTyp (t', t)
481 | SOME e => hasTyp (e, t', t))
482 handle Unify ue =>
483 dte (WrongType ("Shared environment variable",
484 (EVar name, loc),
485 t',
486 t,
487 SOME ue));
488 d'))
489 | SOME t' =>
490 ((case envVarSetFrom name e1 of
491 NONE => subTyp (t', t)
492 | SOME e => hasTyp (e, t', t))
493 handle Unify ue =>
494 dte (WrongType ("Shared environment variable",
495 (EVar name, loc),
496 t',
497 t,
498 SOME ue));
499 d'))
500 d1 d2
501 in
502 (TAction (p', d', r2), loc)
503 end
504 | (TError, _) => t2
505 | _ => (dte (WrongForm ("Body of local settings",
506 "action",
507 e2,
508 t2,
509 NONE));
510 (TError, loc)))
511 | (TError, _) => t1
512 | _ => (dte (WrongForm ("Local settings",
513 "action",
514 e1,
515 t1,
516 NONE));
517 (TError, loc))
518 end
519
520
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
527 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
528 (case t2 of
529 (TAction (p, d, r), _) =>
530 if predImplies (pd, p) then
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
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)
571
572 | EIf (e1, e2, e3) =>
573 let
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 =>
581 dte (WrongType ("\"if\" test",
582 e1,
583 t1,
584 bool,
585 SOME ue));
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)))
596 end
597 end
598
599 exception Ununif
600
601 fun 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
608 | TNested _ => tAll
609 | TError => tAll
610
611 | TUnif (_, ref NONE) => raise Ununif
612
613 fun 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)
620 | TNested _ => false
621 | TError => false
622 | TUnif (_, ref (SOME t)) => hasError t
623 | TUnif (_, ref NONE) => false
624
625
626 fun 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:";
637 output (p_typ t);
638 t)
639 end
640
641 fun checkDecl G (d, _, loc) =
642 case d of
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)
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
664 hasTyp (e, t, to)
665 handle Unify ue =>
666 Describe.describe_type_error loc
667 (WrongType ("Bound value",
668 e,
669 t,
670 to,
671 SOME ue));
672 bindVal G (name, to, SOME e)
673 end
674 | DContext name => bindContext G name
675
676 fun 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
726 fun checkFile G tInit (_, ds, eo) =
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
736 hasTyp (e, t, tInit)
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."
742 end;
743 G'
744 end
745
746 end