From 6a7e5e6f5c76a110ed376803e56babad4f959695 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 8 Jul 2014 20:26:53 +0200
Subject: [PATCH] Various code extraction corrections
---
src/main/scala/leon/frontends/scalac/ASTExtractors.scala | 2 +-
src/main/scala/leon/frontends/scalac/CodeExtraction.scala | 4 ++++
src/main/scala/leon/frontends/scalac/ExtractionPhase.scala | 2 +-
3 files changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index e444d225d..ea488c76e 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -166,7 +166,7 @@ trait ASTExtractors {
* objects of case classes (or any synthetic class). */
def unapply(cd: ClassDef): Option[(String,Template)] = cd match {
case ClassDef(_, name, tparams, impl) if ((cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) && tparams.isEmpty && !cd.symbol.isSynthetic) => {
- Some((name.toString, impl))
+ Some((if (name.toString == "package") cd.symbol.owner.name.toString else name.toString, impl))
}
case _ => None
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 51338cb30..e34b95c9b 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -229,6 +229,7 @@ trait CodeExtraction extends ASTExtractors {
// Phase 6, we create modules and extract bodies
templates.map{ case (name, templ) => extractObjectDef(name, templ) }
+
} catch {
case icee: ImpureCodeEncounteredException =>
icee.emit()
@@ -1264,6 +1265,9 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, mt: MapType), "updated", List(k, v)) =>
MapUnion(a1, FiniteMap(Seq((k, v))).setType(mt)).setType(mt)
+ case (IsTyped(a1, mt1: MapType), "++", List(IsTyped(a2, mt2: MapType))) if mt1 == mt2 =>
+ MapUnion(a1, a2).setType(mt1)
+
case (_, name, _) =>
outOfSubsetError(tr, "Unknown call to "+name)
}
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 06658e31d..6200332b8 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -60,7 +60,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
run.compile(command.files)
- val pgm = Program(FreshIdentifier("<program>"), compiler.leonExtraction.modules)
+ val pgm = Program(FreshIdentifier("__program"), compiler.leonExtraction.modules)
ctx.reporter.debug(pgm.asString(ctx))
pgm
} else {
--
GitLab