From 5d5430e17c072f48dec347c391fcd83983bf9614 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 5 Feb 2016 15:27:39 +0100
Subject: [PATCH] Move Old to xlang
---
src/main/scala/leon/purescala/ExprOps.scala | 2 +-
src/main/scala/leon/purescala/Expressions.scala | 4 ----
src/main/scala/leon/purescala/PrettyPrinter.scala | 7 ++-----
src/main/scala/leon/xlang/Expressions.scala | 8 ++++++++
4 files changed, 11 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 73fcb4849..1cee46865 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -341,7 +341,7 @@ object ExprOps {
/** Returns the set of free variables in an expression */
def variablesOf(expr: Expr): Set[Identifier] = {
- import leon.xlang.Expressions.LetVar
+ import leon.xlang.Expressions._
fold[Set[Identifier]] {
case (e, subs) =>
val subvs = subs.flatten.toSet
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 513720ff4..76a75fdf2 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -76,10 +76,6 @@ object Expressions {
val getType = tpe
}
- case class Old(id: Identifier) extends Expr with Terminal {
- val getType = id.getType
- }
-
/** Precondition of an [[Expressions.Expr]]. Corresponds to the Leon keyword *require*
*
* @param pred The precondition formula inside ``require(...)``
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 039bef507..44d454a9c 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -81,15 +81,12 @@ class PrettyPrinter(opts: PrinterOptions,
}
p"$name"
- case Old(id) =>
- p"old($id)"
-
case Variable(id) =>
p"$id"
case Let(b,d,e) =>
- p"""|val $b = $d
- |$e"""
+ p"""|val $b = $d
+ |$e"""
case LetDef(a::q,body) =>
p"""|$a
diff --git a/src/main/scala/leon/xlang/Expressions.scala b/src/main/scala/leon/xlang/Expressions.scala
index d627e0d28..98214ee64 100644
--- a/src/main/scala/leon/xlang/Expressions.scala
+++ b/src/main/scala/leon/xlang/Expressions.scala
@@ -15,6 +15,14 @@ object Expressions {
trait XLangExpr extends Expr
+ case class Old(id: Identifier) extends XLangExpr with Terminal with PrettyPrintable {
+ val getType = id.getType
+
+ def printWith(implicit pctx: PrinterContext): Unit = {
+ p"old($id)"
+ }
+ }
+
case class Block(exprs: Seq[Expr], last: Expr) extends XLangExpr with Extractable with PrettyPrintable {
def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
Some((exprs :+ last, exprs => Block(exprs.init, exprs.last)))
--
GitLab