Mercurial > urweb

comparison src/elaborate.sml @ 5:258261a53842

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating files
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 16:02:47 -0500
parents 5c3cc348e9e6
children 38bf996e1c2e
comparison
equal deleted inserted replaced
4:5c3cc348e9e6 5:258261a53842
114 114
115 datatype con_error = 115 datatype con_error =
116 UnboundCon of ErrorMsg.span * string 116 UnboundCon of ErrorMsg.span * string
117 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error 117 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
118 118
119 fun conError err = 119 fun conError env err =
120 case err of 120 case err of
121 UnboundCon (loc, s) => 121 UnboundCon (loc, s) =>
122 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) 122 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
123 | WrongKind (c, k1, k2, kerr) => 123 | WrongKind (c, k1, k2, kerr) =>
124 (ErrorMsg.errorAt (#2 c) "Wrong kind"; 124 (ErrorMsg.errorAt (#2 c) "Wrong kind";
125 eprefaces' [("Have", p_kind k1), 125 eprefaces' [("Constructor", p_con env c),
126 ("Need", p_kind k2)]; 126 ("Have kind", p_kind k1),
127 ("Need kind", p_kind k2)];
127 kunifyError kerr) 128 kunifyError kerr)
128 129
129 fun checkKind c k1 k2 = 130 fun checkKind env c k1 k2 =
130 unifyKinds k1 k2 131 unifyKinds k1 k2
131 handle KUnify (k1, k2, err) => 132 handle KUnify (k1, k2, err) =>
132 conError (WrongKind (c, k1, k2, err)) 133 conError env (WrongKind (c, k1, k2, err))
133 134
134 val dummy = ErrorMsg.dummySpan 135 val dummy = ErrorMsg.dummySpan
135 136
136 val ktype = (L'.KType, dummy) 137 val ktype = (L'.KType, dummy)
137 val kname = (L'.KName, dummy) 138 val kname = (L'.KName, dummy)
164 L.CAnnot (c, k) => 165 L.CAnnot (c, k) =>
165 let 166 let
166 val k' = elabKind k 167 val k' = elabKind k
167 val (c', ck) = elabCon env c 168 val (c', ck) = elabCon env c
168 in 169 in
169 checkKind c' ck k'; 170 checkKind env c' ck k';
170 (c', k') 171 (c', k')
171 end 172 end
172 173
173 | L.TFun (t1, t2) => 174 | L.TFun (t1, t2) =>
174 let 175 let
175 val (t1', k1) = elabCon env t1 176 val (t1', k1) = elabCon env t1
176 val (t2', k2) = elabCon env t2 177 val (t2', k2) = elabCon env t2
177 in 178 in
178 checkKind t1' k1 ktype; 179 checkKind env t1' k1 ktype;
179 checkKind t2' k2 ktype; 180 checkKind env t2' k2 ktype;
180 ((L'.TFun (t1', t2'), loc), ktype) 181 ((L'.TFun (t1', t2'), loc), ktype)
181 end 182 end
182 | L.TCFun (e, x, k, t) => 183 | L.TCFun (e, x, k, t) =>
183 let 184 let
184 val e' = elabExplicitness e 185 val e' = elabExplicitness e
185 val k' = elabKind k 186 val k' = elabKind k
186 val env' = E.pushCRel env x k' 187 val env' = E.pushCRel env x k'
187 val (t', tk) = elabCon env' t 188 val (t', tk) = elabCon env' t
188 in 189 in
189 checkKind t' tk ktype; 190 checkKind env t' tk ktype;
190 ((L'.TCFun (e', x, k', t'), loc), ktype) 191 ((L'.TCFun (e', x, k', t'), loc), ktype)
191 end 192 end
192 | L.TRecord c => 193 | L.TRecord c =>
193 let 194 let
194 val (c', ck) = elabCon env c 195 val (c', ck) = elabCon env c
195 val k = (L'.KRecord ktype, loc) 196 val k = (L'.KRecord ktype, loc)
196 in 197 in
197 checkKind c' ck k; 198 checkKind env c' ck k;
198 ((L'.TRecord c', loc), ktype) 199 ((L'.TRecord c', loc), ktype)
199 end 200 end
200 201
201 | L.CVar s => 202 | L.CVar s =>
202 (case E.lookupC env s of 203 (case E.lookupC env s of
203 E.CNotBound => 204 E.CNotBound =>
204 (conError (UnboundCon (loc, s)); 205 (conError env (UnboundCon (loc, s));
205 (cerror, kerror)) 206 (cerror, kerror))
206 | E.CRel (n, k) => 207 | E.CRel (n, k) =>
207 ((L'.CRel n, loc), k) 208 ((L'.CRel n, loc), k)
208 | E.CNamed (n, k) => 209 | E.CNamed (n, k) =>
209 ((L'.CNamed n, loc), k)) 210 ((L'.CNamed n, loc), k))
212 val (c1', k1) = elabCon env c1 213 val (c1', k1) = elabCon env c1
213 val (c2', k2) = elabCon env c2 214 val (c2', k2) = elabCon env c2
214 val dom = kunif () 215 val dom = kunif ()
215 val ran = kunif () 216 val ran = kunif ()
216 in 217 in
217 checkKind c1' k1 (L'.KArrow (dom, ran), loc); 218 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
218 checkKind c2' k2 dom; 219 checkKind env c2' k2 dom;
219 ((L'.CApp (c1', c2'), loc), ran) 220 ((L'.CApp (c1', c2'), loc), ran)
220 end 221 end
221 | L.CAbs (e, x, k, t) => 222 | L.CAbs (e, x, k, t) =>
222 let 223 let
223 val e' = elabExplicitness e 224 val e' = elabExplicitness e
239 val xcs' = map (fn (x, c) => 240 val xcs' = map (fn (x, c) =>
240 let 241 let
241 val (x', xk) = elabCon env x 242 val (x', xk) = elabCon env x
242 val (c', ck) = elabCon env c 243 val (c', ck) = elabCon env c
243 in 244 in
244 checkKind x' xk kname; 245 checkKind env x' xk kname;
245 checkKind c' ck k; 246 checkKind env c' ck k;
246 (x', c') 247 (x', c')
247 end) xcs 248 end) xcs
248 in 249 in
249 ((L'.CRecord (k, xcs'), loc), k) 250 ((L'.CRecord (k, xcs'), loc), (L'.KRecord k, loc))
250 end 251 end
251 | L.CConcat (c1, c2) => 252 | L.CConcat (c1, c2) =>
252 let 253 let
253 val (c1', k1) = elabCon env c1 254 val (c1', k1) = elabCon env c1
254 val (c2', k2) = elabCon env c2 255 val (c2', k2) = elabCon env c2
255 val ku = kunif () 256 val ku = kunif ()
256 val k = (L'.KRecord ku, loc) 257 val k = (L'.KRecord ku, loc)
257 in 258 in
258 checkKind c1' k1 k; 259 checkKind env c1' k1 k;
259 checkKind c2' k2 k; 260 checkKind env c2' k2 k;
260 ((L'.CConcat (c1', c2'), loc), k) 261 ((L'.CConcat (c1', c2'), loc), k)
261 end 262 end
262 263
263 fun elabDecl env (d, loc) = 264 fun elabDecl env (d, loc) =
264 case d of 265 (resetKunif ();
265 L.DCon (x, ko, c) => 266 case d of
266 let 267 L.DCon (x, ko, c) =>
267 val k' = case ko of 268 let
268 NONE => kunif () 269 val k' = case ko of
269 | SOME k => elabKind k 270 NONE => kunif ()
270 271 | SOME k => elabKind k
271 val (c', ck) = elabCon env c 272
272 in 273 val (c', ck) = elabCon env c
273 checkKind c' ck k'; 274 val (env', n) = E.pushCNamed env x k'
274 (E.pushCNamed env x k', 275 in
275 L'.DCon (x, k', c')) 276 checkKind env c' ck k';
276 end 277 (env',
277 278 (L'.DCon (x, n, k', c'), loc))
278 fun elabFile _ = raise Fail "" 279 end)
280
281 fun elabFile env ds =
282 ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds
279 283
280 end 284 end