From 37bcf2bd2d5e391f8203f213e50b6d3dfccabe24 Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <colder@php.net> Date: Fri, 21 Mar 2014 17:03:10 +0100 Subject: [PATCH] Fix positions of holes and resulting chooses --- src/main/scala/leon/frontends/scalac/CodeExtraction.scala | 2 +- src/main/scala/leon/synthesis/ConvertHoles.scala | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index 250b96211..720aef319 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -898,7 +898,7 @@ trait CodeExtraction extends ASTExtractors { case chs @ ExHole(tpe) => val cTpe = extractType(tpe) - Hole().setType(cTpe) + Hole().setType(cTpe).setPos(chs.pos) case chs @ ExChooseExpression(args, tpe, body, select) => val cTpe = extractType(tpe) diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala index 686c5e4b1..57cc7bf59 100644 --- a/src/main/scala/leon/synthesis/ConvertHoles.scala +++ b/src/main/scala/leon/synthesis/ConvertHoles.scala @@ -51,17 +51,17 @@ object ConvertHoles extends LeonPhase[Program, Program] { holes = holes.reverse if (holes.nonEmpty) { - val res = FreshIdentifier("b", true).setType(body.getType) + val res = FreshIdentifier("b", true).copiedFrom(body) val (pid, pbody) = fd.postcondition.get val c = Choose(holes, Let(res, body, replaceFromIDs(Map(pid -> res.toVariable), pbody))) if (holes.size > 1) { val newHoles = holes.map(_.freshen) - fd.body = Some(LetTuple(newHoles, c, replaceFromIDs((holes zip newHoles.map(_.toVariable)).toMap, body))) + fd.body = Some(LetTuple(newHoles, c.setPos(body), replaceFromIDs((holes zip newHoles.map(_.toVariable)).toMap, body)).setPos(body)) } else { fd.body = Some(preMap { - case h @ Hole() => Some(c) + case h @ Hole() => Some(c.setPos(h)) case _ => None }(fd.body.get)) } -- GitLab