From cfe12844050921bac41ac1ba6f7babca900c2990 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 4 Dec 2015 17:54:08 +0100
Subject: [PATCH] Extract ConstantType's
---
.../scala/leon/frontends/scalac/CodeExtraction.scala | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 4bca0e767..43d977fb3 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1092,11 +1092,11 @@ trait CodeExtraction extends ASTExtractors {
}
val restTree = rest match {
- case Some(rst) => {
+ case Some(rst) =>
val nctx = dctx.withNewVar(vs -> (() => Variable(newID)))
extractTree(rst)(nctx)
- }
- case None => UnitLiteral()
+ case None =>
+ UnitLiteral()
}
rest = None
@@ -1765,6 +1765,9 @@ trait CodeExtraction extends ASTExtractors {
case tpe if tpe == NothingClass.tpe =>
Untyped
+ case ct: ConstantType =>
+ extractType(ct.value.tpe)
+
case TypeRef(_, sym, _) if isBigIntSym(sym) =>
IntegerType
--
GitLab