From c4c715fe44fccd9837fc41a8c520aa9e4ff496fd Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 10 Jul 2015 19:01:15 +0200
Subject: [PATCH] real numbers trees and frontend
---
library/lang/Real.scala | 17 ++++++++++++
.../leon/frontends/scalac/ASTExtractors.scala | 14 ++++++++++
.../frontends/scalac/CodeExtraction.scala | 21 +++++++++++++++
.../scala/leon/purescala/Expressions.scala | 26 +++++++++++++++++++
src/main/scala/leon/purescala/Types.scala | 1 +
5 files changed, 79 insertions(+)
create mode 100644 library/lang/Real.scala
diff --git a/library/lang/Real.scala b/library/lang/Real.scala
new file mode 100644
index 000000000..3e94b27c0
--- /dev/null
+++ b/library/lang/Real.scala
@@ -0,0 +1,17 @@
+package leon.lang
+import leon.annotation._
+
+@ignore
+class Real {
+
+ def +(a: Real): Real = ???
+ def -(a: Real): Real = ???
+ def *(a: Real): Real = ???
+ def /(a: Real): Real = ???
+
+ def unary_- : Real = ???
+}
+
+object Real {
+ def apply(n: BigInt, d: BigInt): Real = ???
+}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 402a7d7cf..348680e6e 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -40,6 +40,7 @@ trait ASTExtractors {
protected lazy val scalaSetSym = classFromName("scala.collection.immutable.Set")
protected lazy val setSym = classFromName("leon.lang.Set")
protected lazy val mapSym = classFromName("leon.lang.Map")
+ protected lazy val realSym = classFromName("leon.lang.Real")
protected lazy val optionClassSym = classFromName("scala.Option")
protected lazy val arraySym = classFromName("scala.Array")
protected lazy val someClassSym = classFromName("scala.Some")
@@ -72,6 +73,10 @@ trait ASTExtractors {
getResolvedTypeSym(sym) == setSym
}
+ def isRealSym(sym: Symbol) : Boolean = {
+ getResolvedTypeSym(sym) == realSym
+ }
+
def isScalaSetSym(sym: Symbol) : Boolean = {
getResolvedTypeSym(sym) == scalaSetSym
}
@@ -242,6 +247,15 @@ trait ASTExtractors {
}
}
+ object ExRealLiteral {
+ def unapply(tree: Tree): Option[(Tree, Tree)] = tree match {
+ case Apply(ExSelected("leon", "lang", "Real", "apply"), n :: d :: Nil) =>
+ Some((n, d))
+ case _ =>
+ None
+ }
+ }
+
object ExIntToBigInt {
def unapply(tree: Tree): Option[Tree] = tree match {
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 1e995aaf6..d7cab0c0a 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1213,6 +1213,9 @@ trait CodeExtraction extends ASTExtractors {
}
}
+ case ExRealLiteral(n: Literal, d: Literal) =>
+ RealLiteral((BigInt(n.value.stringValue), BigInt(d.value.stringValue)))
+
case ExInt32Literal(v) =>
IntLiteral(v)
@@ -1505,6 +1508,24 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, IntegerType), "<=", List(IsTyped(a2, IntegerType))) =>
LessEquals(a1, a2)
+ //Real methods
+ case (IsTyped(a1, RealType), "+", List(IsTyped(a2, RealType))) =>
+ RealPlus(a1, a2)
+ case (IsTyped(a1, RealType), "-", List(IsTyped(a2, RealType))) =>
+ RealMinus(a1, a2)
+ case (IsTyped(a1, RealType), "*", List(IsTyped(a2, RealType))) =>
+ RealTimes(a1, a2)
+ case (IsTyped(a1, RealType), "/", List(IsTyped(a2, RealType))) =>
+ RealDivision(a1, a2)
+ case (IsTyped(a1, RealType), ">", List(IsTyped(a2, RealType))) =>
+ GreaterThan(a1, a2)
+ case (IsTyped(a1, RealType), ">=", List(IsTyped(a2, RealType))) =>
+ GreaterEquals(a1, a2)
+ case (IsTyped(a1, RealType), "<", List(IsTyped(a2, RealType))) =>
+ LessThan(a1, a2)
+ case (IsTyped(a1, RealType), "<=", List(IsTyped(a2, RealType))) =>
+ LessEquals(a1, a2)
+
// Int methods
case (IsTyped(a1, Int32Type), "+", List(IsTyped(a2, Int32Type))) =>
BVPlus(a1, a2)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index c25f9be43..12900e3ec 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -274,6 +274,9 @@ object Expressions {
case class InfiniteIntegerLiteral(value: BigInt) extends Literal[BigInt] {
val getType = IntegerType
}
+ case class RealLiteral(value: (BigInt, BigInt)) extends Literal[(BigInt, BigInt)] {
+ val getType = RealType
+ }
case class BooleanLiteral(value: Boolean) extends Literal[Boolean] {
val getType = BooleanType
@@ -482,6 +485,29 @@ object Expressions {
}
+ /* Integer arithmetic */
+ case class RealPlus(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == RealType && rhs.getType == RealType)
+ val getType = RealType
+ }
+ case class RealMinus(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == RealType && rhs.getType == RealType)
+ val getType = RealType
+ }
+ case class RealUMinus(expr: Expr) extends Expr {
+ require(expr.getType == RealType)
+ val getType = RealType
+ }
+ case class RealTimes(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == RealType && rhs.getType == RealType)
+ val getType = RealType
+ }
+ case class RealDivision(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == RealType && rhs.getType == RealType)
+ val getType = RealType
+ }
+
+
/* Tuple operations */
// If you are not sure about the requirement you should use
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 6bb1f921d..3754b8534 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -47,6 +47,7 @@ object Types {
case object UnitType extends TypeTree
case object CharType extends TypeTree
case object IntegerType extends TypeTree
+ case object RealType extends TypeTree
case class BitVectorType(size: Int) extends TypeTree
case object Int32Type extends TypeTree
--
GitLab