1 (* HCoop Domtool (http://hcoop.sourceforge.net/)
2 * Copyright (c) 2006, Adam Chlipala
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.
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.
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.
19 (* Domtool configuration language type checking *)
21 structure Tycheck :> TYCHECK = struct
25 structure SM = StringMap
30 fun resetUnif () = unifCount := 0
37 str (chr (ord #"A" + c))
39 "UNIF" ^ Int.toString (c - 26)
42 TUnif (name, ref NONE)
46 exception UnequalDomains
48 fun eqRecord f (r1, r2) =
49 (SM.appi (fn (k, v1) =>
50 case SM.find (r2, k) of
51 NONE => raise UnequalDomains
56 raise UnequalDomains) r1;
57 SM.appi (fn (k, v2) =>
58 case SM.find (r1, k) of
59 NONE => raise UnequalDomains
64 raise UnequalDomains) r2;
66 handle UnequalDomains => false
68 fun eqPred ((p1, _), (p2, _)) =
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)
79 fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
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)
86 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
87 eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
88 andalso eqRecord eqTy (r1, r2)
90 | (TNested (p1, q1), TNested (p2, q2)) =>
91 eqPred (p1, p2) andalso eqTy (q1, q2)
93 | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
94 | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
96 | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
98 | (TError, TError) => true
102 datatype unification_error =
103 UnifyPred of pred * pred
104 | UnifyTyp of typ * typ
105 | UnifyOccurs of string * typ
107 exception Unify of unification_error
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
115 fun describe_unification_error t ue =
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) =>
125 (print "Reason: Incompatible types.\n";
126 preface ("Have:", p_typ t1);
127 preface ("Need:", p_typ t2))
128 | UnifyOccurs (name, t') =>
132 (print "Reason: Occurs check failed for ";
137 fun describe_type_error loc te =
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))
157 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
159 (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
160 | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
162 | (_, CPrefix (CRoot, _)) => true
163 | (CNot (CPrefix (CRoot, _), _), _) => true
165 | (CRoot, CRoot) => true
167 | (CConst s1, CConst s2) => s1 = s2
169 | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
170 | (_, CPrefix p2) => predImplies (p1All, p2)
172 | (CNot p1, CNot p2) => predImplies (p2, p1)
176 fun predSimpl (pAll as (p, loc)) =
180 | CPrefix p => (CPrefix (predSimpl p), loc)
181 | CNot p => (CNot (predSimpl p), loc)
184 val p1' = predSimpl p1
185 val p2' = predSimpl p2
188 (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
189 | _ => if predImplies (p2', p1') then
191 else if predImplies (p1', p2') then
194 (CAnd (p1', p2'), loc)
197 fun subPred (p1, p2) =
198 if predImplies (p1, p2) then
201 raise (Unify (UnifyPred (p1, p2)))
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
209 fun occurs u (t, _) =
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
219 | TUnif (_, ref (SOME t)) => occurs u t
220 | TUnif (_, u') => u = u'
222 fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
224 (TBase s1, TBase s2) =>
228 raise Unify (UnifyTyp (t1All, t2All))
229 | (TList t1, TList t2) => subTyp (t1, t2)
230 | (TArrow (d1, r1), TArrow (d2, r2)) =>
234 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
236 subRecord subTyp (d2, d1);
237 subRecord subTyp (r1, r2);
238 subRecord subTyp (r2, r1))
239 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
241 | (TNested (d1, r1), TNested (d2, r2)) =>
245 | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
246 | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
248 | (TUnif (_, r1), TUnif (_, r2)) =>
254 | (TUnif (name, r), _) =>
255 if occurs r t2All then
256 raise (Unify (UnifyOccurs (name, t2All)))
260 | (_, TUnif (name, r)) =>
261 if occurs r t1All then
262 raise (Unify (UnifyOccurs (name, t1All)))
269 | _ => raise Unify (UnifyTyp (t1All, t2All))
276 fun whnorm (tAll as (t, loc)) =
278 TUnif (_, ref (SOME tAll)) => whnorm tAll
281 fun baseCondition t =
283 (TBase name, _) => typeRule name
285 (case baseCondition t of
287 | SOME f => SOME (fn (EList ls, _) => List.all f ls
291 fun hasTyp (e, t1, t2) =
292 if (case baseCondition t2 of
294 | SOME rule => rule e) then
299 fun checkPred G (p, loc) =
301 val err = ErrorMsg.error (SOME loc)
306 if lookupContext G s then
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)
315 fun checkTyp G (tAll as (t, loc)) =
317 val err = ErrorMsg.error (SOME loc)
321 if lookupType G name then
324 (err ("Unbound type name " ^ name);
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"
337 fun envVarSetFrom v (e, _) =
344 | EGet (_, _, e) => envVarSetFrom v e
345 | ESeq es => foldr (fn (e, found) =>
348 | NONE => envVarSetFrom v e)
350 | ELocal (_, e) => envVarSetFrom v e
354 fun checkExp G (eAll as (e, loc)) =
356 val dte = describe_type_error loc
359 EInt _ => (TBase "int", loc)
360 | EString _ => (TBase "string", loc)
363 val t = (newUnif (), loc)
365 foldl (fn (e', ret) =>
367 val t' = checkExp G e'
369 (hasTyp (eAll, t', t);
371 (TList (TError, loc), loc)
375 (dte (WrongType ("List element",
381 end) (TList t, loc) es
388 NONE => (newUnif (), loc)
389 | SOME t => checkTyp G t
391 val G' = bindVal G (x, t, NONE)
392 val t' = checkExp G' e
394 (TArrow (t, t'), loc)
397 (case lookupVal G x of
398 NONE => (dte (UnboundVariable x);
401 | EApp (func, arg) =>
403 val dom = (newUnif (), loc)
404 val ran = (newUnif (), loc)
406 val tf = checkExp G func
407 val ta = checkExp G arg
409 (hasTyp (func, tf, (TArrow (dom, ran), loc));
410 hasTyp (arg, ta, dom)
412 dte (WrongType ("Function argument",
419 (dte (WrongForm ("Function to be applied",
431 (TAction ((CPrefix (CRoot, loc), loc),
433 SM.insert (SM.empty, evar, t)),
436 | EGet (x, evar, rest) =>
438 val xt = (newUnif (), loc)
439 val G' = bindVal G (x, xt, NONE)
441 val rt = whnorm (checkExp G' rest)
444 (TAction (p, d, r), _) =>
445 (case SM.find (d, evar) of
446 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
450 dte (WrongType ("Retrieved environment variable",
457 | _ => (dte (WrongForm ("Body of environment variable read",
465 | ESeq [] => raise Fail "Empty ESeq"
466 | ESeq [e1] => checkExp G e1
467 | ESeq (e1 :: rest) =>
469 val e2 = (ESeq rest, loc)
471 val t1 = whnorm (checkExp G e1)
472 val t2 = whnorm (checkExp G e2)
475 (TAction (p1, d1, r1), _) =>
477 (TAction (p2, d2, r2), _) =>
479 val p' = predSimpl (CAnd (p1, p2), loc)
481 val d' = SM.foldli (fn (name, t, d') =>
482 case SM.find (r1, name) of
484 (case SM.find (d', name) of
485 NONE => SM.insert (d', name, t)
487 ((case envVarSetFrom name e1 of
488 NONE => subTyp (t, t')
489 | SOME e => hasTyp (e, t, t'))
491 dte (WrongType ("Shared environment variable",
498 ((case envVarSetFrom name e1 of
499 NONE => subTyp (t, t')
500 | SOME e => hasTyp (e, t, t'))
502 dte (WrongType ("Shared environment variable",
510 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
513 (TAction (p', d', r'), loc)
516 | _ => (dte (WrongForm ("Action to be sequenced",
523 | _ => (dte (WrongForm ("Action to be sequenced",
533 val t1 = whnorm (checkExp G e1)
534 val t2 = whnorm (checkExp G e2)
537 (TAction (p1, d1, r1), _) =>
539 (TAction (p2, d2, r2), _) =>
541 val p' = predSimpl (CAnd (p1, p2), loc)
543 val d' = SM.foldli (fn (name, t, d') =>
544 case SM.find (r1, name) of
546 (case SM.find (d', name) of
547 NONE => SM.insert (d', name, t)
549 ((case envVarSetFrom name e1 of
550 NONE => subTyp (t', t)
551 | SOME e => hasTyp (e, t', t))
553 dte (WrongType ("Shared environment variable",
560 ((case envVarSetFrom name e1 of
561 NONE => subTyp (t', t)
562 | SOME e => hasTyp (e, t', t))
564 dte (WrongType ("Shared environment variable",
572 (TAction (p', d', r2), loc)
575 | _ => (dte (WrongForm ("Action to be sequenced",
582 | _ => (dte (WrongForm ("Action to be sequenced",
593 val t1 = whnorm (checkExp G e1)
594 val t2 = whnorm (checkExp G e2)
597 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
599 (TAction (p, d, r), _) =>
600 if predImplies (pd, p) then
603 SM.unionWithi (fn (name, t1, t2) =>
606 dte (WrongType ("Environment variable",
613 (TAction (pr, combineRecs (d, d1),
614 combineRecs (r, r1)), loc)
617 (dte (WrongPred ("nested action",
623 (dte (WrongForm ("Body of nested action",
631 (dte (WrongForm ("Container of nested action",
639 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
640 SM.empty, SM.empty), loc)
645 fun ununif (tAll as (t, loc)) =
648 | TList t => (TList (ununif t), loc)
649 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
650 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
651 | TUnif (_, ref (SOME t)) => ununif t
655 | TUnif (_, ref NONE) => raise Ununif
657 fun hasError (t, _) =
660 | TList t => hasError t
661 | TArrow (d, r) => hasError d orelse hasError r
662 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
663 orelse List.exists hasError (SM.listItems r)
666 | TUnif (_, ref (SOME t)) => hasError t
667 | TUnif (_, ref NONE) => false
670 fun checkUnit G (eAll as (_, loc)) =
673 val t = checkExp G eAll
680 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
685 fun checkDecl G (d, _, loc) =
687 DExternType name => bindType G name
688 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
689 | DVal (name, to, e) =>
693 NONE => (newUnif (), loc)
694 | SOME to => checkTyp G to
700 describe_type_error loc
701 (WrongType ("Bound value",
706 bindVal G (name, to, SOME e)
708 | DContext name => bindContext G name
710 fun checkFile G tInit (_, ds, eo) =
712 val G' = foldl (fn (d, G) => checkDecl G d) G ds
716 | SOME (e as (_, loc)) =>
718 val t = checkExp G' e
722 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
723 preface ("Actual:", p_typ t);
724 preface ("Needed:", p_typ tInit))