HCoop / hcoop / domtool2.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Reduction
[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.
17*)
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
27d9de59
AC		 27local
28 val unifCount = ref 0
29in
30fun resetUnif () = unifCount := 0
31
32fun 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
44end
45
46exception UnequalDomains
47
48fun 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
68fun 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
79fun 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
234b917a 90 | (TNested (p1, q1), TNested (p2, q2)) =>
1a4e5a6c 91 eqPred (p1, p2) andalso eqTy (q1, q2)
234b917a 92
27d9de59
AC		 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
102datatype unification_error =
103 UnifyPred of pred * pred
104 | UnifyTyp of typ * typ
105 | UnifyOccurs of string * typ
106
107exception Unify of unification_error
108
109datatype 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
234b917a 113 | WrongPred of string * pred * pred
27d9de59
AC		 114
115fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
116 [PD.string s, PD.space 1, d]))
117
118fun describe_unification_error t ue =
119 case ue of
120 UnifyPred (p1, p2) =>
234b917a 121 (print "Reason: Incompatible contexts.\n";
27d9de59
AC		 122 preface ("Have:", p_pred p1);
123 preface ("Need:", p_pred p2))
124 | UnifyTyp (t1, t2) =>
125 if eqTy (t, t1) then
126 ()
127 else
128 (print "Reason: Incompatible types.\n";
129 preface ("Have:", p_typ t1);
130 preface ("Need:", p_typ t2))
131 | UnifyOccurs (name, t') =>
132 if eqTy (t, t') then
133 ()
134 else
135 (print "Reason: Occurs check failed for ";
136 print name;
137 print " in:\n";
138 printd (p_typ t))
139
140fun describe_type_error loc te =
141 case te of
142 WrongType (place, e, t1, t2, ueo) =>
143 (ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
144 preface (" Expression:", p_exp e);
145 preface ("Actual type:", p_typ t1);
146 preface ("Needed type:", p_typ t2);
147 Option.app (describe_unification_error t1) ueo)
148 | WrongForm (place, form, e, t, ueo) =>
149 (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
150 preface ("Expression:", p_exp e);
151 preface (" Type:", p_typ t);
152 Option.app (describe_unification_error t) ueo)
153 | UnboundVariable name =>
154 ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
234b917a
AC		 155 | WrongPred (place, p1, p2) =>
156 (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
157 preface ("Have:", p_pred p1);
158 preface ("Need:", p_pred p2))
27d9de59 159
db427c67 160fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
27d9de59 161 case (p1, p2) of
1a4e5a6c
AC		 162 (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
163 | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
164
165 | (_, CPrefix (CRoot, _)) => true
db427c67
AC		 166 | (CNot (CPrefix (CRoot, _), _), _) => true
167
168 | (CRoot, CRoot) => true
169
170 | (CConst s1, CConst s2) => s1 = s2
171
172 | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
234b917a 173 | (_, CPrefix p2) => predImplies (p1All, p2)
db427c67
AC		 174
175 | (CNot p1, CNot p2) => predImplies (p2, p1)
27d9de59 176
db427c67
AC		 177 | _ => false
178
179fun predSimpl (pAll as (p, loc)) =
180 case p of
181 CRoot => pAll
182 | CConst _ => pAll
183 | CPrefix p => (CPrefix (predSimpl p), loc)
184 | CNot p => (CNot (predSimpl p), loc)
185 | CAnd (p1, p2) =>
186 let
187 val p1' = predSimpl p1
188 val p2' = predSimpl p2
189 in
190 case p1' of
191 (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
192 | _ => if predImplies (p2', p1') then
193 p2'
1a4e5a6c
AC		 194 else if predImplies (p1', p2') then
195 p1'
db427c67
AC		 196 else
197 (CAnd (p1', p2'), loc)
198 end
199
234b917a 200fun subPred (p1, p2) =
db427c67
AC		 201 if predImplies (p1, p2) then
202 ()
203 else
204 raise (Unify (UnifyPred (p1, p2)))
27d9de59 205
234b917a
AC		 206fun subRecord f (r1, r2) =
207 SM.appi (fn (k, v2) =>
208 case SM.find (r1, k) of
209 NONE => raise UnequalDomains
210 | SOME v1 => f (v1, v2)) r2
27d9de59
AC		 211
212fun occurs u (t, _) =
213 case t of
214 TBase _ => false
215 | TList t => occurs u t
216 | TArrow (d, r) => occurs u d orelse occurs u r
217 | TAction (_, d, r) =>
218 List.exists (occurs u) (SM.listItems d)
219 orelse List.exists (occurs u) (SM.listItems r)
1a4e5a6c 220 | TNested (_, t) => occurs u t
27d9de59
AC		 221 | TError => false
222 | TUnif (_, ref (SOME t)) => occurs u t
223 | TUnif (_, u') => u = u'
224
234b917a 225fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
27d9de59
AC		 226 case (t1, t2) of
227 (TBase s1, TBase s2) =>
228 if s1 = s2 then
229 ()
230 else
231 raise Unify (UnifyTyp (t1All, t2All))
234b917a 232 | (TList t1, TList t2) => subTyp (t1, t2)
27d9de59 233 | (TArrow (d1, r1), TArrow (d2, r2)) =>
234b917a
AC		 234 (subTyp (d2, d1);
235 subTyp (r1, r2))
27d9de59
AC		 236
237 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
234b917a
AC		 238 ((subPred (p2, p1);
239 subRecord subTyp (d2, d1);
240 subRecord subTyp (r1, r2);
241 subRecord subTyp (r2, r1))
27d9de59
AC		 242 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
243
234b917a
AC		 244 | (TNested (d1, r1), TNested (d2, r2)) =>
245 (subPred (d2, d1);
1a4e5a6c 246 subTyp (r1, r2))
234b917a
AC		 247
248 | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
249 | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
27d9de59
AC		 250
251 | (TUnif (_, r1), TUnif (_, r2)) =>
252 if r1 = r2 then
253 ()
254 else
255 r1 := SOME t2All
256
257 | (TUnif (name, r), _) =>
258 if occurs r t2All then
259 raise (Unify (UnifyOccurs (name, t2All)))
260 else
261 r := SOME t2All
262
263 | (_, TUnif (name, r)) =>
264 if occurs r t1All then
265 raise (Unify (UnifyOccurs (name, t1All)))
266 else
267 r := SOME t1All
268
269 | (TError, _) => ()
270 | (_, TError) => ()
271
272 | _ => raise Unify (UnifyTyp (t1All, t2All))
273
274fun isError t =
275 case t of
276 (TError, _) => true
277 | _ => false
278
db427c67
AC		 279fun whnorm (tAll as (t, loc)) =
280 case t of
281 TUnif (_, ref (SOME tAll)) => whnorm tAll
282 | _ => tAll
283
234b917a
AC		 284fun checkTyp G (tAll as (t, loc)) =
285 let
286 val err = ErrorMsg.error (SOME loc)
287 in
288 case t of
289 TBase name =>
290 if lookupType G name then
291 tAll
292 else
293 (err ("Unbound type name " ^ name);
294 (TError, loc))
295 | TList t => (TList (checkTyp G t), loc)
296 | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
297 | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
298 SM.map (checkTyp G) r), loc)
1a4e5a6c 299 | TNested (p, t) => (TNested (p, checkTyp G t), loc)
234b917a
AC		 300 | TError => raise Fail "TError in parser-generated type"
301 | TUnif _ => raise Fail "TUnif in parser-generated type"
302 end
303
27d9de59
AC		 304fun checkExp G (eAll as (e, loc)) =
305 let
306 val dte = describe_type_error loc
307 in
308 case e of
309 EInt _ => (TBase "int", loc)
310 | EString _ => (TBase "string", loc)
311 | EList es =>
312 let
313 val t = (newUnif (), loc)
314 in
315 foldl (fn (e', ret) =>
316 let
317 val t' = checkExp G e'
318 in
234b917a 319 (subTyp (t', t);
27d9de59
AC		 320 if isError t' then
321 (TList (TError, loc), loc)
322 else
323 ret)
324 handle Unify ue =>
325 (dte (WrongType ("List element",
326 e',
327 t',
328 t,
329 SOME ue));
330 (TError, loc))
331 end) (TList t, loc) es
332 end
333
334 | ELam (x, to, e) =>
335 let
336 val t =
337 case to of
338 NONE => (newUnif (), loc)
234b917a 339 | SOME t => checkTyp G t
27d9de59 340
492c1cff 341 val G' = bindVal G (x, t, NONE)
27d9de59
AC		 342 val t' = checkExp G' e
343 in
344 (TArrow (t, t'), loc)
345 end
346 | EVar x =>
234b917a 347 (case lookupVal G x of
27d9de59
AC		 348 NONE => (dte (UnboundVariable x);
349 (TError, loc))
350 | SOME t => t)
351 | EApp (func, arg) =>
352 let
353 val dom = (newUnif (), loc)
354 val ran = (newUnif (), loc)
355
356 val tf = checkExp G func
357 val ta = checkExp G arg
358 in
234b917a
AC		 359 (subTyp (tf, (TArrow (dom, ran), loc));
360 subTyp (ta, dom)
27d9de59
AC		 361 handle Unify ue =>
362 dte (WrongType ("Function argument",
363 arg,
364 ta,
365 dom,
366 SOME ue));
367 ran)
368 handle Unify ue =>
369 (dte (WrongForm ("Function to be applied",
370 "function",
371 func,
372 tf,
373 SOME ue));
374 (TError, loc))
375 end
db427c67
AC		 376
377 | ESet (evar, e) =>
378 let
379 val t = checkExp G e
380 in
381 (TAction ((CPrefix (CRoot, loc), loc),
382 SM.empty,
383 SM.insert (SM.empty, evar, t)),
384 loc)
385 end
386 | EGet (x, evar, rest) =>
387 let
388 val xt = (newUnif (), loc)
492c1cff 389 val G' = bindVal G (x, xt, NONE)
db427c67
AC		 390
391 val rt = whnorm (checkExp G' rest)
392 in
393 case rt of
394 (TAction (p, d, r), _) =>
395 (case SM.find (d, evar) of
396 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
397 | SOME xt' =>
234b917a 398 (subTyp (xt', xt)
db427c67
AC		 399 handle Unify ue =>
400 dte (WrongType ("Retrieved environment variable",
401 (EVar x, loc),
402 xt',
403 xt,
404 SOME ue));
405 rt))
234b917a 406 | (TError, _) => rt
db427c67
AC		 407 | _ => (dte (WrongForm ("Body of environment variable read",
408 "action",
409 rest,
410 rt,
411 NONE));
412 (TError, loc))
413 end
414
415 | ESeq [] => raise Fail "Empty ESeq"
416 | ESeq [e1] => checkExp G e1
417 | ESeq (e1 :: rest) =>
418 let
419 val e2 = (ESeq rest, loc)
420
421 val t1 = whnorm (checkExp G e1)
422 val t2 = whnorm (checkExp G e2)
423 in
424 case t1 of
425 (TAction (p1, d1, r1), _) =>
426 (case t2 of
427 (TAction (p2, d2, r2), _) =>
428 let
429 val p' = predSimpl (CAnd (p1, p2), loc)
430
431 val d' = SM.foldli (fn (name, t, d') =>
432 case SM.find (r1, name) of
433 NONE =>
434 (case SM.find (d', name) of
435 NONE => SM.insert (d', name, t)
436 | SOME t' =>
234b917a 437 (subTyp (t, t')
db427c67
AC		 438 handle Unify ue =>
439 dte (WrongType ("Shared environment variable",
440 (EVar name, loc),
441 t,
442 t',
443 SOME ue));
444 d'))
445 | SOME t' =>
234b917a 446 (subTyp (t, t')
db427c67
AC		 447 handle Unify ue =>
448 dte (WrongType ("Shared environment variable",
449 (EVar name, loc),
450 t,
451 t',
452 SOME ue));
453 d'))
454 d1 d2
455
456 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
457 r1 r2
458 in
459 (TAction (p', d', r'), loc)
460 end
234b917a 461 | (TError, _) => t2
db427c67
AC		 462 | _ => (dte (WrongForm ("Action to be sequenced",
463 "action",
464 e2,
465 t2,
466 NONE));
467 (TError, loc)))
234b917a 468 | (TError, _) => t1
db427c67
AC		 469 | _ => (dte (WrongForm ("Action to be sequenced",
470 "action",
471 e1,
472 t1,
473 NONE));
474 (TError, loc))
475 end
476
1a4e5a6c 477 | ELocal (e1, e2) =>
db427c67 478 let
1a4e5a6c
AC		 479 val t1 = whnorm (checkExp G e1)
480 val t2 = whnorm (checkExp G e2)
db427c67 481 in
1a4e5a6c
AC		 482 case t1 of
483 (TAction (p1, d1, r1), _) =>
484 (case t2 of
485 (TAction (p2, d2, r2), _) =>
486 let
487 val p' = predSimpl (CAnd (p1, p2), loc)
488
489 val d' = SM.foldli (fn (name, t, d') =>
490 case SM.find (r1, name) of
491 NONE =>
492 (case SM.find (d', name) of
493 NONE => SM.insert (d', name, t)
494 | SOME t' =>
495 (subTyp (t, t')
496 handle Unify ue =>
497 dte (WrongType ("Shared environment variable",
498 (EVar name, loc),
499 t,
500 t',
501 SOME ue));
502 d'))
503 | SOME t' =>
504 (subTyp (t, t')
505 handle Unify ue =>
506 dte (WrongType ("Shared environment variable",
507 (EVar name, loc),
508 t,
509 t',
510 SOME ue));
511 d'))
512 d1 d2
513 in
514 (TAction (p', d', r2), loc)
515 end
516 | (TError, _) => t2
517 | _ => (dte (WrongForm ("Action to be sequenced",
518 "action",
519 e2,
520 t2,
521 NONE));
522 (TError, loc)))
523 | (TError, _) => t1
524 | _ => (dte (WrongForm ("Action to be sequenced",
db427c67 525 "action",
1a4e5a6c
AC		 526 e1,
527 t1,
db427c67
AC		 528 NONE));
529 (TError, loc))
530 end
234b917a 531
1a4e5a6c 532
234b917a
AC		 533 | EWith (e1, e2) =>
534 let
535 val t1 = whnorm (checkExp G e1)
536 val t2 = whnorm (checkExp G e2)
537 in
538 case t1 of
1a4e5a6c 539 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a
AC		 540 (case t2 of
541 (TAction (p, d, r), _) =>
542 if predImplies (pd, p) then
1a4e5a6c
AC		 543 let
544 val combineRecs =
545 SM.unionWithi (fn (name, t1, t2) =>
546 (subTyp (t1, t2)
547 handle Unify ue =>
548 dte (WrongType ("Environment variable",
549 (EVar name, loc),
550 t1,
551 t2,
552 SOME ue));
553 t2))
554 in
555 (TAction (pr, combineRecs (d, d1),
556 combineRecs (r, r1)), loc)
557 end
234b917a
AC		 558 else
559 (dte (WrongPred ("nested action",
560 pd,
561 p));
562 (TError, loc))
563 | (TError, _) => t2
564 | _ =>
565 (dte (WrongForm ("Body of nested action",
566 "action",
567 e2,
568 t2,
569 NONE));
570 (TError, loc)))
571 | (TError, _) => t1
572 | _ =>
573 (dte (WrongForm ("Container of nested action",
574 "action",
575 e1,
576 t1,
577 NONE));
578 (TError, loc))
579 end
580
581 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
582 SM.empty, SM.empty), loc)
27d9de59
AC		 583 end
584
585exception Ununif
586
587fun ununif (tAll as (t, loc)) =
588 case t of
589 TBase _ => tAll
590 | TList t => (TList (ununif t), loc)
591 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
592 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
593 | TUnif (_, ref (SOME t)) => ununif t
234b917a 594 | TNested _ => tAll
27d9de59
AC		 595 | TError => tAll
596
597 | TUnif (_, ref NONE) => raise Ununif
598
599fun hasError (t, _) =
600 case t of
601 TBase _ => false
602 | TList t => hasError t
603 | TArrow (d, r) => hasError d orelse hasError r
604 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
605 orelse List.exists hasError (SM.listItems r)
234b917a 606 | TNested _ => false
27d9de59
AC		 607 | TError => false
608 | TUnif (_, ref (SOME t)) => hasError t
609 | TUnif (_, ref NONE) => false
610
611
612fun checkUnit G (eAll as (_, loc)) =
613 let
614 val _ = resetUnif ()
615 val t = checkExp G eAll
616 in
617 if hasError t then
618 t
619 else
620 ununif t
621 handle Ununif =>
622 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
623 printd (p_typ t);
624 t)
625 end
626
234b917a
AC		 627fun checkDecl G (d, _, loc) =
628 case d of
629 DExternType name => bindType G name
492c1cff
AC		 630 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
631 | DVal (name, to, e) =>
632 let
633 val to =
634 case to of
635 NONE => (newUnif (), loc)
636 | SOME to => checkTyp G to
637
638 val t = checkExp G e
639 in
640 subTyp (t, to)
641 handle Unify ue =>
642 describe_type_error loc
643 (WrongType ("Bound value",
644 e,
645 t,
646 to,
647 SOME ue));
648 bindVal G (name, to, SOME e)
649 end
234b917a
AC		 650
651fun checkFile G tInit (ds, eo) =
652 let
653 val G' = foldl (fn (d, G) => checkDecl G d) G ds
654 in
655 case eo of
656 NONE => ()
657 | SOME (e as (_, loc)) =>
658 let
659 val t = checkExp G' e
660 in
661 subTyp (t, tInit)
662 handle Unify ue =>
663 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
664 preface ("Actual:", p_typ t);
665 preface ("Needed:", p_typ tInit))
666 end;
667 G'
668 end
669
27d9de59 670end
Unnamed repository; edit this file to name it for gitweb.