summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2015-12-31 13:02:56 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2015-12-31 13:02:56 -0500
commitdd92f19fcee5c66e0f63eaf49b746604ddd57210 (patch)
treee6cd0190fb5ded89a057b7a8ddcc7ccc11439a32
parent3d24185389cef552d4b442d16d0c5ed1d8ccaf87 (diff)
A simple eta rule for constructor-level tuples
-rw-r--r--src/elaborate.sml26
1 files changed, 26 insertions, 0 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 3b7c48ea..2dfbf5b2 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -285,6 +285,7 @@
fun hnormKind (kAll as (k, _)) =
case k of
L'.KUnif (_, _, ref (L'.KKnown k)) => hnormKind k
+ | L'.KTupleUnif (_, _, ref (L'.KKnown k)) => hnormKind k
| _ => kAll
open ElabOps
@@ -1344,6 +1345,31 @@
| (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible)
| (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible)
+ | (L'.CTuple cs, L'.CRel x) =>
+ (case hnormKind (kindof env c2All) of
+ (L'.KTuple ks, _) =>
+ if length cs <> length ks then
+ err CIncompatible
+ else
+ let
+ fun rightProjs (cs, n) =
+ case cs of
+ c :: cs' =>
+ (case hnormCon env c of
+ (L'.CProj ((L'.CRel x', _), n'), _) =>
+ x' = x andalso n' = n andalso rightProjs (cs', n+1)
+ | _ => false)
+ | [] => true
+ in
+ if rightProjs (cs, 1) then
+ ()
+ else
+ err CIncompatible
+ end
+ | _ => err CIncompatible)
+ | (L'.CRel x, L'.CTuple cs) =>
+ unifyCons'' env loc c2All c1All
+
| (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
(unifyKinds env dom1 dom2;
unifyKinds env ran1 ran2)