From 70fb50c21527ccf1ea1e2f22c32d2b5d12f8c796 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 10 May 2016 17:11:15 +0200
Subject: [PATCH] Make this message more explicit
---
src/main/scala/leon/purescala/Constructors.scala | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 02ac92f8f..16b7932d6 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -71,8 +71,11 @@ object Constructors {
Let(x, value, body)
case xs =>
require(
- value.getType.isInstanceOf[TupleType],
- s"The definition value in LetTuple must be of some tuple type; yet we got [${value.getType}]. In expr: \n$value"
+ value.getType match {
+ case TupleType(args) => args.size == xs.size
+ case _ => false
+ },
+ s"In letTuple: '$value' is being assigned as a tuple of arity ${xs.size}; yet its type is '${value.getType}' (body is '$body')"
)
Extractors.LetPattern(TuplePattern(None,binders map { b => WildcardPattern(Some(b)) }), value, body)
--
GitLab