Mercurial > urweb

changeset 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 f0909fb3848f
children 726f0caeea3f
files src/elab.sml src/elaborate.sml
diffstat 2 files changed, 20 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Sun Oct 17 13:26:11 2010 -0400
+++ b/src/elab.sml	Tue Oct 19 10:13:24 2010 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
--- a/src/elaborate.sml	Sun Oct 17 13:26:11 2010 -0400
+++ b/src/elaborate.sml	Tue Oct 19 10:13:24 2010 -0400
@@ -583,6 +583,25 @@
        | L'.CProj (c, n) =>
          (case hnormKind (kindof env c) of
               (L'.KTuple ks, _) => List.nth (ks, n - 1)
+            | (L'.KUnif (_, _, r), _) =>
+              let
+                  val ku = kunif loc
+                  val k = (L'.KTupleUnif (loc, [(n, ku)], ref NONE), loc)
+              in
+                  r := SOME k;
+                  k
+              end
+            | (L'.KTupleUnif (_, nks, r), _) =>
+              (case ListUtil.search (fn (n', k) => if n' = n then SOME k else NONE) nks of
+                   SOME k => k
+                 | NONE =>
+                   let
+                       val ku = kunif loc
+                       val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), ref NONE), loc)
+                   in
+                       r := SOME k;
+                       k
+                   end)
             | k => raise CUnify' (CKindof (k, c, "tuple")))
 
        | L'.CError => kerror