Mercurial > urweb
comparison src/elaborate.sml @ 1311:5337adf33a4a
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 |