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
33 fun resetUnif () = unifCount
:= 0
40 str (chr (ord #
"A" + c
))
42 "UNIF" ^
Int.toString (c
- 26)
45 TUnif (name
, ref NONE
)
49 exception UnequalDomains
51 fun eqRecord
f (r1
, r2
) =
52 (SM
.appi (fn (k
, v1
) =>
53 case SM
.find (r2
, k
) of
54 NONE
=> raise UnequalDomains
59 raise UnequalDomains
) r1
;
60 SM
.appi (fn (k
, v2
) =>
61 case SM
.find (r1
, k
) of
62 NONE
=> raise UnequalDomains
67 raise UnequalDomains
) r2
;
69 handle UnequalDomains
=> false
71 fun eqPred ((p1
, _
), (p2
, _
)) =
73 (CRoot
, CRoot
) => true
74 |
(CConst s1
, CConst s2
) => s1
= s2
75 |
(CPrefix p1
, CPrefix p2
) => eqPred (p1
, p2
)
76 |
(CNot p1
, CNot p2
) => eqPred (p1
, p2
)
77 |
(CAnd (p1
, q1
), CAnd (p2
, q2
)) =>
78 eqPred (p1
, p2
) andalso eqPred (q1
, q2
)
82 fun eqTy (t1All
as (t1
, _
), t2All
as (t2
, _
)) =
84 (TBase s1
, TBase s2
) => s1
= s2
85 |
(TList t1
, TList t2
) => eqTy (t1
, t2
)
86 |
(TArrow (d1
, r1
), TArrow (d2
, r2
)) =>
87 eqTy (d1
, d2
) andalso eqTy (r1
, r2
)
89 |
(TAction (p1
, d1
, r1
), TAction (p2
, d2
, r2
)) =>
90 eqPred (p1
, p2
) andalso eqRecord
eqTy (d1
, d2
)
91 andalso eqRecord
eqTy (r1
, r2
)
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
114 fun preface (s
, d
) = printd (PD
.hovBox (PD
.PPS
.Rel
0,
115 [PD
.string s
, PD
.space
1, d
]))
117 fun describe_unification_error t ue
=
119 UnifyPred (p1
, p2
) =>
120 (print
"Reason: Incompatible predicates.\n";
121 preface ("Have:", p_pred p1
);
122 preface ("Need:", p_pred p2
))
123 |
UnifyTyp (t1
, t2
) =>
127 (print
"Reason: Incompatible types.\n";
128 preface ("Have:", p_typ t1
);
129 preface ("Need:", p_typ t2
))
130 |
UnifyOccurs (name
, t
') =>
134 (print
"Reason: Occurs check failed for ";
139 fun describe_type_error loc te
=
141 WrongType (place
, e
, t1
, t2
, ueo
) =>
142 (ErrorMsg
.error (SOME loc
) (place ^
" has wrong type.");
143 preface (" Expression:", p_exp e
);
144 preface ("Actual type:", p_typ t1
);
145 preface ("Needed type:", p_typ t2
);
146 Option
.app (describe_unification_error t1
) ueo
)
147 |
WrongForm (place
, form
, e
, t
, ueo
) =>
148 (ErrorMsg
.error (SOME loc
) (place ^
" has a non-" ^ form ^
" type.");
149 preface ("Expression:", p_exp e
);
150 preface (" Type:", p_typ t
);
151 Option
.app (describe_unification_error t
) ueo
)
152 | UnboundVariable name
=>
153 ErrorMsg
.error (SOME loc
) ("Unbound variable " ^ name ^
".\n")
155 fun unifyPred (p1All
as (p1
, _
), p2All
as (p2
, _
)) =
158 |
(CConst s1
, CConst s2
) =>
162 raise (Unify (UnifyPred (p1All
, p2All
)))
163 |
(CPrefix p1
, CPrefix p2
) => unifyPred (p1
, p2
)
164 |
(CNot p1
, CNot p2
) => unifyPred (p1
, p2
)
165 |
(CAnd (p1
, q1
), CAnd (p2
, q2
)) =>
169 | _
=> raise (Unify (UnifyPred (p1All
, p2All
)))
171 fun unifyRecord
f (r1
, r2
) =
172 (SM
.appi (fn (k
, v1
) =>
173 case SM
.find (r2
, k
) of
174 NONE
=> raise UnequalDomains
175 | SOME v2
=> f (v1
, v2
)) r1
;
176 SM
.appi (fn (k
, v2
) =>
177 case SM
.find (r1
, k
) of
178 NONE
=> raise UnequalDomains
179 | SOME v1
=> f (v1
, v2
)) r2
)
181 fun occurs
u (t
, _
) =
184 | TList t
=> occurs u t
185 |
TArrow (d
, r
) => occurs u d
orelse occurs u r
186 |
TAction (_
, d
, r
) =>
187 List.exists (occurs u
) (SM
.listItems d
)
188 orelse List.exists (occurs u
) (SM
.listItems r
)
190 |
TUnif (_
, ref (SOME t
)) => occurs u t
191 |
TUnif (_
, u
') => u
= u
'
193 fun unify (t1All
as (t1
, _
), t2All
as (t2
, _
)) =
195 (TBase s1
, TBase s2
) =>
199 raise Unify (UnifyTyp (t1All
, t2All
))
200 |
(TList t1
, TList t2
) => unify (t1
, t2
)
201 |
(TArrow (d1
, r1
), TArrow (d2
, r2
)) =>
205 |
(TAction (p1
, d1
, r1
), TAction (p2
, d2
, r2
)) =>
206 ((unifyPred (p1
, p2
);
207 unifyRecord
unify (d1
, d2
);
208 unifyRecord
unify (r1
, r2
))
209 handle UnequalDomains
=> raise Unify (UnifyTyp (t1All
, t2All
)))
211 |
(TUnif (_
, ref (SOME t1
)), _
) => unify (t1
, t2All
)
212 |
(_
, TUnif (_
, ref (SOME t2
))) => unify (t1All
, t2
)
214 |
(TUnif (_
, r1
), TUnif (_
, r2
)) =>
220 |
(TUnif (name
, r
), _
) =>
221 if occurs r t2All
then
222 raise (Unify (UnifyOccurs (name
, t2All
)))
226 |
(_
, TUnif (name
, r
)) =>
227 if occurs r t1All
then
228 raise (Unify (UnifyOccurs (name
, t1All
)))
235 | _
=> raise Unify (UnifyTyp (t1All
, t2All
))
242 fun checkExp
G (eAll
as (e
, loc
)) =
244 val dte
= describe_type_error loc
247 EInt _
=> (TBase
"int", loc
)
248 | EString _
=> (TBase
"string", loc
)
251 val t
= (newUnif (), loc
)
253 foldl (fn (e
', ret
) =>
255 val t
' = checkExp G e
'
259 (TList (TError
, loc
), loc
)
263 (dte (WrongType ("List element",
269 end) (TList t
, loc
) es
276 NONE
=> (newUnif (), loc
)
279 val G
' = SM
.insert (G
, x
, t
)
280 val t
' = checkExp G
' e
282 (TArrow (t
, t
'), loc
)
285 (case SM
.find (G
, x
) of
286 NONE
=> (dte (UnboundVariable x
);
289 |
EApp (func
, arg
) =>
291 val dom
= (newUnif (), loc
)
292 val ran
= (newUnif (), loc
)
294 val tf
= checkExp G func
295 val ta
= checkExp G arg
297 (unify (tf
, (TArrow (dom
, ran
), loc
));
300 dte (WrongType ("Function argument",
307 (dte (WrongForm ("Function to be applied",
315 | _
=> raise Fail
"Not ready for that expression yet!"
320 fun ununif (tAll
as (t
, loc
)) =
323 | TList t
=> (TList (ununif t
), loc
)
324 |
TArrow (d
, r
) => (TArrow (ununif d
, ununif r
), loc
)
325 |
TAction (p
, d
, r
) => (TAction (p
, SM
.map ununif d
, SM
.map ununif r
), loc
)
326 |
TUnif (_
, ref (SOME t
)) => ununif t
329 |
TUnif (_
, ref NONE
) => raise Ununif
331 fun hasError (t
, _
) =
334 | TList t
=> hasError t
335 |
TArrow (d
, r
) => hasError d
orelse hasError r
336 |
TAction (p
, d
, r
) => List.exists
hasError (SM
.listItems d
)
337 orelse List.exists
hasError (SM
.listItems r
)
339 |
TUnif (_
, ref (SOME t
)) => hasError t
340 |
TUnif (_
, ref NONE
) => false
343 fun checkUnit
G (eAll
as (_
, loc
)) =
346 val t
= checkExp G eAll
353 (ErrorMsg
.error (SOME loc
) "Unification variables remain in type:";