Mercurial > urweb

comparison src/elaborate.sml @ 11:e97c6d335869

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simple elaboration working
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 15:20:46 -0400
parents dde5c52e5e5e
children d89477f07c1e
comparison
equal deleted inserted replaced
10:dde5c52e5e5e 11:e97c6d335869
334 | CExplicitness (c1, c2) => 334 | CExplicitness (c1, c2) =>
335 eprefaces "Differing constructor function explicitness" 335 eprefaces "Differing constructor function explicitness"
336 [("Con 1", p_con env c1), 336 [("Con 1", p_con env c1),
337 ("Con 2", p_con env c2)] 337 ("Con 2", p_con env c2)]
338 338
339 fun unifyCons' env (c1All as (c1, _)) (c2All as (c2, _)) = 339 fun hnormCon env (cAll as (c, _)) =
340 case c of
341 L'.CUnif (_, _, ref (SOME c)) => hnormCon env c
342
343 | L'.CNamed xn =>
344 (case E.lookupCNamed env xn of
345 (_, _, SOME c') => hnormCon env c'
346 | _ => cAll)
347
348 | _ => cAll
349
350 fun unifyCons' env c1 c2 =
351 unifyCons'' env (hnormCon env c1) (hnormCon env c2)
352
353 and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
340 let 354 let
341 fun err f = raise CUnify' (f (c1All, c2All)) 355 fun err f = raise CUnify' (f (c1All, c2All))
342 in 356 in
343 case (c1, c2) of 357 case (c1, c2) of
344 (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 358 (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
422 | KUnify args => raise CUnify (c1, c2, CKind args) 436 | KUnify args => raise CUnify (c1, c2, CKind args)
423 437
424 datatype exp_error = 438 datatype exp_error =
425 UnboundExp of ErrorMsg.span * string 439 UnboundExp of ErrorMsg.span * string
426 | Unify of L'.exp * L'.con * L'.con * cunify_error 440 | Unify of L'.exp * L'.con * L'.con * cunify_error
441 | Unif of string * L'.con
442 | WrongForm of string * L'.exp * L'.con
427 443
428 fun expError env err = 444 fun expError env err =
429 case err of 445 case err of
430 UnboundExp (loc, s) => 446 UnboundExp (loc, s) =>
431 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) 447 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
433 (ErrorMsg.errorAt (#2 e) "Unification failure"; 449 (ErrorMsg.errorAt (#2 e) "Unification failure";
434 eprefaces' [("Expression", p_exp env e), 450 eprefaces' [("Expression", p_exp env e),
435 ("Have con", p_con env c1), 451 ("Have con", p_con env c1),
436 ("Need con", p_con env c2)]; 452 ("Need con", p_con env c2)];
437 cunifyError env uerr) 453 cunifyError env uerr)
454 | Unif (action, c) =>
455 (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action);
456 eprefaces' [("Con", p_con env c)])
457 | WrongForm (variety, e, t) =>
458 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
459 eprefaces' [("Expression", p_exp env e),
460 ("Type", p_con env t)])
438 461
439 fun checkCon env e c1 c2 = 462 fun checkCon env e c1 c2 =
440 unifyCons env c1 c2 463 unifyCons env c1 c2
441 handle CUnify (c1, c2, err) => 464 handle CUnify (c1, c2, err) =>
442 expError env (Unify (e, c1, c2, err)) 465 expError env (Unify (e, c1, c2, err))
443 466
467 exception SynUnif
468
469 val liftConInCon =
470 U.Con.mapB {kind = fn k => k,
471 con = fn bound => fn c =>
472 case c of
473 L'.CRel xn =>
474 if xn < bound then
475 c
476 else
477 L'.CRel (xn + 1)
478 | L'.CUnif _ => raise SynUnif
479 | _ => c,
480 bind = fn (bound, U.Con.Rel _) => bound + 1
481 | (bound, _) => bound}
482
483 val subConInCon =
484 U.Con.mapB {kind = fn k => k,
485 con = fn (xn, rep) => fn c =>
486 case c of
487 L'.CRel xn' =>
488 if xn = xn' then
489 #1 rep
490 else
491 c
492 | L'.CUnif _ => raise SynUnif
493 | _ => c,
494 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
495 | (ctx, _) => ctx}
496
444 fun elabExp env (e, loc) = 497 fun elabExp env (e, loc) =
445 case e of 498 case e of
446 L.EAnnot (e, t) => 499 L.EAnnot (e, t) =>
447 let 500 let
448 val (e', et) = elabExp env e 501 val (e', et) = elabExp env e
491 | L.ECApp (e, c) => 544 | L.ECApp (e, c) =>
492 let 545 let
493 val (e', et) = elabExp env e 546 val (e', et) = elabExp env e
494 val (c', ck) = elabCon env c 547 val (c', ck) = elabCon env c
495 in 548 in
496 raise Fail "ECApp" 549 case #1 (hnormCon env et) of
497 end 550 L'.CError => (eerror, cerror)
498 | L.ECAbs _ => raise Fail "ECAbs" 551 | L'.TCFun (_, _, k, eb) =>
552 let
553 val () = checkKind env c' ck k
554 val eb' = subConInCon (0, c') eb
555 handle SynUnif => (expError env (Unif ("substitution", eb));
556 cerror)
557 in
558 ((L'.ECApp (e', c'), loc), eb')
559 end
560
561 | L'.CUnif _ =>
562 (expError env (Unif ("application", et));
563 (eerror, cerror))
564
565 | _ =>
566 (expError env (WrongForm ("constructor function", e', et));
567 (eerror, cerror))
568 end
569 | L.ECAbs (expl, x, k, e) =>
570 let
571 val expl' = elabExplicitness expl
572 val k' = elabKind k
573 val (e', et) = elabExp (E.pushCRel env x k') e
574 in
575 ((L'.ECAbs (expl', x, k', e'), loc),
576 (L'.TCFun (expl', x, k', et), loc))
577 end
499 578
500 datatype decl_error = 579 datatype decl_error =
501 KunifsRemainKind of ErrorMsg.span * L'.kind 580 KunifsRemainKind of ErrorMsg.span * L'.kind
502 | KunifsRemainCon of ErrorMsg.span * L'.con 581 | KunifsRemainCon of ErrorMsg.span * L'.con
503 | KunifsRemainExp of ErrorMsg.span * L'.exp 582 | KunifsRemainExp of ErrorMsg.span * L'.exp
530 val k' = case ko of 609 val k' = case ko of
531 NONE => kunif () 610 NONE => kunif ()
532 | SOME k => elabKind k 611 | SOME k => elabKind k
533 612
534 val (c', ck) = elabCon env c 613 val (c', ck) = elabCon env c
535 val (env', n) = E.pushCNamed env x k' 614 val (env', n) = E.pushCNamed env x k' (SOME c')
536 in 615 in
537 checkKind env c' ck k'; 616 checkKind env c' ck k';
538 617
539 if kunifsInKind k' then 618 if kunifsInKind k' then
540 declError env (KunifsRemainKind (loc, k')) 619 declError env (KunifsRemainKind (loc, k'))