Mercurial > urweb

comparison src/elaborate.sml @ 1311:5337adf33a4a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Smarter handling of unification variables for 'kindof' on projections
author Adam Chlipala <adam@chlipala.net>
date Tue, 19 Oct 2010 10:13:24 -0400
parents 3a845f2ce9e9
children df7bfb30dcc3
comparison
equal deleted inserted replaced
1310:f0909fb3848f 1311:5337adf33a4a
581 581
582 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc) 582 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
583 | L'.CProj (c, n) => 583 | L'.CProj (c, n) =>
584 (case hnormKind (kindof env c) of 584 (case hnormKind (kindof env c) of
585 (L'.KTuple ks, _) => List.nth (ks, n - 1) 585 (L'.KTuple ks, _) => List.nth (ks, n - 1)
586 | (L'.KUnif (_, _, r), _) =>
587 let
588 val ku = kunif loc
589 val k = (L'.KTupleUnif (loc, [(n, ku)], ref NONE), loc)
590 in
591 r := SOME k;
592 k
593 end
594 | (L'.KTupleUnif (_, nks, r), _) =>
595 (case ListUtil.search (fn (n', k) => if n' = n then SOME k else NONE) nks of
596 SOME k => k
597 | NONE =>
598 let
599 val ku = kunif loc
600 val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), ref NONE), loc)
601 in
602 r := SOME k;
603 k
604 end)
586 | k => raise CUnify' (CKindof (k, c, "tuple"))) 605 | k => raise CUnify' (CKindof (k, c, "tuple")))
587 606
588 | L'.CError => kerror 607 | L'.CError => kerror
589 | L'.CUnif (_, _, k, _, _) => k 608 | L'.CUnif (_, _, k, _, _) => k
590 609