Mercurial > urweb

comparison src/elaborate.sml @ 67:9f89f0b00b84

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating cfold
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 09:48:54 -0400
parents 1ec5703c09c4
children 6431b315a1e3
comparison
equal deleted inserted replaced
66:1ec5703c09c4 67:9f89f0b00b84
113 113
114 datatype con_error = 114 datatype con_error =
115 UnboundCon of ErrorMsg.span * string 115 UnboundCon of ErrorMsg.span * string
116 | UnboundStrInCon of ErrorMsg.span * string 116 | UnboundStrInCon 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 | DuplicateField of ErrorMsg.span * string
118 119
119 fun conError env err = 120 fun conError env err =
120 case err of 121 case err of
121 UnboundCon (loc, s) => 122 UnboundCon (loc, s) =>
122 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) 123 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
126 (ErrorMsg.errorAt (#2 c) "Wrong kind"; 127 (ErrorMsg.errorAt (#2 c) "Wrong kind";
127 eprefaces' [("Constructor", p_con env c), 128 eprefaces' [("Constructor", p_con env c),
128 ("Have kind", p_kind k1), 129 ("Have kind", p_kind k1),
129 ("Need kind", p_kind k2)]; 130 ("Need kind", p_kind k2)];
130 kunifyError kerr) 131 kunifyError kerr)
132 | DuplicateField (loc, s) =>
133 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
131 134
132 fun checkKind env c k1 k2 = 135 fun checkKind env c k1 k2 =
133 unifyKinds k1 k2 136 unifyKinds k1 k2
134 handle KUnify (k1, k2, err) => 137 handle KUnify (k1, k2, err) =>
135 conError env (WrongKind (c, k1, k2, err)) 138 conError env (WrongKind (c, k1, k2, err))
195 L.KType => (L'.KType, loc) 198 L.KType => (L'.KType, loc)
196 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) 199 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
197 | L.KName => (L'.KName, loc) 200 | L.KName => (L'.KName, loc)
198 | L.KRecord k => (L'.KRecord (elabKind k), loc) 201 | L.KRecord k => (L'.KRecord (elabKind k), loc)
199 | L.KWild => kunif () 202 | L.KWild => kunif ()
203
204 fun foldKind (dom, ran, loc)=
205 (L'.KArrow ((L'.KArrow ((L'.KName, loc),
206 (L'.KArrow (dom,
207 (L'.KArrow (ran, ran), loc)), loc)), loc),
208 (L'.KArrow (ran,
209 (L'.KArrow ((L'.KRecord dom, loc),
210 ran), loc)), loc)), loc)
200 211
201 fun elabCon env (c, loc) = 212 fun elabCon env (c, loc) =
202 case c of 213 case c of
203 L.CAnnot (c, k) => 214 L.CAnnot (c, k) =>
204 let 215 let
276 in 287 in
277 checkKind env c1' k1 (L'.KArrow (dom, ran), loc); 288 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
278 checkKind env c2' k2 dom; 289 checkKind env c2' k2 dom;
279 ((L'.CApp (c1', c2'), loc), ran) 290 ((L'.CApp (c1', c2'), loc), ran)
280 end 291 end
281 | L.CAbs (x, k, t) => 292 | L.CAbs (x, ko, t) =>
282 let 293 let
283 val k' = elabKind k 294 val k' = case ko of
295 NONE => kunif ()
296 | SOME k => elabKind k
284 val env' = E.pushCRel env x k' 297 val env' = E.pushCRel env x k'
285 val (t', tk) = elabCon env' t 298 val (t', tk) = elabCon env' t
286 in 299 in
287 ((L'.CAbs (x, k', t'), loc), 300 ((L'.CAbs (x, k', t'), loc),
288 (L'.KArrow (k', tk), loc)) 301 (L'.KArrow (k', tk), loc))
302 in 315 in
303 checkKind env x' xk kname; 316 checkKind env x' xk kname;
304 checkKind env c' ck k; 317 checkKind env c' ck k;
305 (x', c') 318 (x', c')
306 end) xcs 319 end) xcs
307 in 320
308 ((L'.CRecord (k, xcs'), loc), (L'.KRecord k, loc)) 321 val rc = (L'.CRecord (k, xcs'), loc)
322 (* Add duplicate field checking later. *)
323 in
324 (rc, (L'.KRecord k, loc))
309 end 325 end
310 | L.CConcat (c1, c2) => 326 | L.CConcat (c1, c2) =>
311 let 327 let
312 val (c1', k1) = elabCon env c1 328 val (c1', k1) = elabCon env c1
313 val (c2', k2) = elabCon env c2 329 val (c2', k2) = elabCon env c2
315 val k = (L'.KRecord ku, loc) 331 val k = (L'.KRecord ku, loc)
316 in 332 in
317 checkKind env c1' k1 k; 333 checkKind env c1' k1 k;
318 checkKind env c2' k2 k; 334 checkKind env c2' k2 k;
319 ((L'.CConcat (c1', c2'), loc), k) 335 ((L'.CConcat (c1', c2'), loc), k)
336 end
337 | L.CFold =>
338 let
339 val dom = kunif ()
340 val ran = kunif ()
341 in
342 ((L'.CFold (dom, ran), loc),
343 foldKind (dom, ran, loc))
320 end 344 end
321 345
322 | L.CWild k => 346 | L.CWild k =>
323 let 347 let
324 val k' = elabKind k 348 val k' = elabKind k
471 495
472 | L'.CName _ => kname 496 | L'.CName _ => kname
473 497
474 | L'.CRecord (k, _) => (L'.KRecord k, loc) 498 | L'.CRecord (k, _) => (L'.KRecord k, loc)
475 | L'.CConcat (c, _) => kindof env c 499 | L'.CConcat (c, _) => kindof env c
500 | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
476 501
477 | L'.CError => kerror 502 | L'.CError => kerror
478 | L'.CUnif (k, _, _) => k 503 | L'.CUnif (k, _, _) => k
479 504
480 fun unifyRecordCons env (c1, c2) = 505 fun unifyRecordCons env (c1, c2) =
622 | SOME (_, NONE) => cAll 647 | SOME (_, NONE) => cAll
623 | SOME (_, SOME c) => hnormCon env c 648 | SOME (_, SOME c) => hnormCon env c
624 end 649 end
625 650
626 | L'.CApp (c1, c2) => 651 | L'.CApp (c1, c2) =>
627 (case hnormCon env c1 of 652 (case #1 (hnormCon env c1) of
628 (L'.CAbs (_, _, cb), _) => 653 L'.CAbs (_, _, cb) =>
629 ((hnormCon env (subConInCon (0, c2) cb)) 654 ((hnormCon env (subConInCon (0, c2) cb))
630 handle SynUnif => cAll) 655 handle SynUnif => cAll)
656 | L'.CApp (c', i) =>
657 (case #1 (hnormCon env c') of
658 L'.CApp (c', f) =>
659 (case #1 (hnormCon env c') of
660 L'.CFold ks =>
661 (case #1 (hnormCon env c2) of
662 L'.CRecord (_, []) => hnormCon env i
663 | L'.CRecord (k, (x, c) :: rest) =>
664 hnormCon env
665 (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
666 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
667 (L'.CRecord (k, rest), loc)), loc)), loc)
668 | _ => cAll)
669 | _ => cAll)
670 | _ => cAll)
631 | _ => cAll) 671 | _ => cAll)
632 672
633 | L'.CConcat (c1, c2) => 673 | L'.CConcat (c1, c2) =>
634 (case (hnormCon env c1, hnormCon env c2) of 674 (case (hnormCon env c1, hnormCon env c2) of
635 ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) => 675 ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) =>