From 9183f16ff05ad383d70ffa16b4944844b08e0152 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Tue, 16 Sep 2014 12:30:09 +0200
Subject: [PATCH] Tracing now includes values for binders/patterns in MatchExpr
---
src/main/scala/leon/evaluators/TracingEvaluator.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala
index 273270b46..e99cd8269 100644
--- a/src/main/scala/leon/evaluators/TracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala
@@ -17,7 +17,7 @@ class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) ex
def initGC = new TracingGlobalContext(Nil)
- class TracingGlobalContext(var values: List[(Expr, Expr)]) extends GlobalContext
+ class TracingGlobalContext(var values: List[(Tree, Expr)]) extends GlobalContext
case class TracingRecContext(mappings: Map[Identifier, Expr], tracingFrames: Int) extends RecContext {
def withVars(news: Map[Identifier, Expr]) = copy(mappings = news)
@@ -37,7 +37,7 @@ class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) ex
val r = cases.toStream.map(c => matchesCase(rscrut, c)).find(_.nonEmpty) match {
case Some(Some((c, mappings))) =>
- gctx.values ++= mappings.map { case (id, v) => id.toVariable.setPos(id) -> v }
+ gctx.values ++= (Map(c.pattern -> rscrut) ++ mappings.map { case (id, v) => id.toVariable.setPos(id) -> v })
e(c.rhs)(rctx.withNewVars(mappings), gctx)
case _ =>
--
GitLab