Mercurial > urweb

comparison src/elaborate.sml @ 81:60d97de1bbe8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Factor some operations into ElabOps
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 09:29:49 -0400
parents 321cb9805c8e
children b4f2a258e52c
comparison
equal deleted inserted replaced
80:321cb9805c8e 81:60d97de1bbe8
414 [("Con", p_con env c)] 414 [("Con", p_con env c)]
415 | CRecordFailure => 415 | CRecordFailure =>
416 eprefaces "Can't unify record constructors" [] 416 eprefaces "Can't unify record constructors" []
417 417
418 exception SynUnif = E.SynUnif 418 exception SynUnif = E.SynUnif
419 val liftConInCon = E.liftConInCon 419
420 420 open ElabOps
421 val subConInCon =
422 U.Con.mapB {kind = fn k => k,
423 con = fn (xn, rep) => fn c =>
424 case c of
425 L'.CRel xn' =>
426 (case Int.compare (xn', xn) of
427 EQUAL => #1 rep
428 | GREATER => L'.CRel (xn' - 1)
429 | LESS => c)
430 (*| L'.CUnif _ => raise SynUnif*)
431 | _ => c,
432 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
433 | (ctx, _) => ctx}
434
435 fun subStrInSgn (m1, m2) =
436 U.Sgn.map {kind = fn k => k,
437 con = fn c as L'.CModProj (m1', ms, x) =>
438 if m1 = m1' then
439 L'.CModProj (m2, ms, x)
440 else
441 c
442 | c => c,
443 sgn_item = fn sgi => sgi,
444 sgn = fn sgn => sgn}
445 421
446 type record_summary = { 422 type record_summary = {
447 fields : (L'.con * L'.con) list, 423 fields : (L'.con * L'.con) list,
448 unifs : (L'.con * L'.con option ref) list, 424 unifs : (L'.con * L'.con option ref) list,
449 others : L'.con list 425 others : L'.con list
629 pairOffUnifs (rest1, rest2)) 605 pairOffUnifs (rest1, rest2))
630 in 606 in
631 pairOffUnifs (unifs1, unifs2) 607 pairOffUnifs (unifs1, unifs2)
632 end 608 end
633 609
634 and hnormCon env (cAll as (c, loc)) =
635 case c of
636 L'.CUnif (_, _, _, ref (SOME c)) => hnormCon env c
637
638 | L'.CNamed xn =>
639 (case E.lookupCNamed env xn of
640 (_, _, SOME c') => hnormCon env c'
641 | _ => cAll)
642
643 | L'.CModProj (n, ms, x) =>
644 let
645 val (_, sgn) = E.lookupStrNamed env n
646 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
647 case E.projectStr env {sgn = sgn, str = str, field = m} of
648 NONE => raise Fail "hnormCon: Unknown substructure"
649 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
650 ((L'.StrVar n, loc), sgn) ms
651 in
652 case E.projectCon env {sgn = sgn, str = str, field = x} of
653 NONE => raise Fail "kindof: Unknown con in structure"
654 | SOME (_, NONE) => cAll
655 | SOME (_, SOME c) => hnormCon env c
656 end
657
658 | L'.CApp (c1, c2) =>
659 (case #1 (hnormCon env c1) of
660 L'.CAbs (x, k, cb) =>
661 let
662 val sc = (hnormCon env (subConInCon (0, c2) cb))
663 handle SynUnif => cAll
664 (*val env' = E.pushCRel env x k*)
665 in
666 (*eprefaces "Subst" [("x", Print.PD.string x),
667 ("cb", p_con env' cb),
668 ("c2", p_con env c2),
669 ("sc", p_con env sc)];*)
670 sc
671 end
672 | L'.CApp (c', i) =>
673 (case #1 (hnormCon env c') of
674 L'.CApp (c', f) =>
675 (case #1 (hnormCon env c') of
676 L'.CFold ks =>
677 (case #1 (hnormCon env c2) of
678 L'.CRecord (_, []) => hnormCon env i
679 | L'.CRecord (k, (x, c) :: rest) =>
680 hnormCon env
681 (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
682 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
683 (L'.CRecord (k, rest), loc)), loc)), loc)
684 | L'.CConcat ((L'.CRecord (k, (x, c) :: rest), _), rest') =>
685 let
686 val rest'' = (L'.CConcat ((L'.CRecord (k, rest), loc), rest'), loc)
687
688 (*val ccc = (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
689 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
690 rest''), loc)), loc)*)
691 in
692 (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
693 hnormCon env
694 (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
695 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
696 rest''), loc)), loc)
697 end
698 | _ => cAll)
699 | _ => cAll)
700 | _ => cAll)
701 | _ => cAll)
702
703 | L'.CConcat (c1, c2) =>
704 (case (hnormCon env c1, hnormCon env c2) of
705 ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) =>
706 (L'.CRecord (k, xcs1 @ xcs2), loc)
707 | ((L'.CRecord (_, []), _), c2') => c2'
708 | ((L'.CConcat (c11, c12), loc), c2') =>
709 hnormCon env (L'.CConcat (c11, (L'.CConcat (c12, c2'), loc)), loc)
710 | _ => cAll)
711
712 | _ => cAll
713 610
714 and unifyCons' env c1 c2 = 611 and unifyCons' env c1 c2 =
715 unifyCons'' env (hnormCon env c1) (hnormCon env c2) 612 unifyCons'' env (hnormCon env c1) (hnormCon env c2)
716 613
717 and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) = 614 and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =