diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index b64d6cb05d58ad1dd0420d27f21cfd0b3955b2bd..a83e819b8565c93a5e8432a20a37410445b9cdef 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -28,6 +28,10 @@ trait CodeExtraction extends Extractors {
private lazy val someClassSym = definitions.getClass("scala.Some")
private lazy val function1TraitSym = definitions.getClass("scala.Function1")
+ private lazy val arraySym = definitions.getClass("scala.Array")
+
+ def isArrayClassSym(sym: Symbol): Boolean = sym == arraySym
+
def isTuple2(sym : Symbol) : Boolean = sym == tuple2Sym
def isTuple3(sym : Symbol) : Boolean = sym == tuple3Sym
def isTuple4(sym : Symbol) : Boolean = sym == tuple4Sym
@@ -784,12 +788,29 @@ trait CodeExtraction extends Extractors {
}
}
}
+ case ArrayType(bt) => {
+ assert(rargs.size == 1)
+ ArraySelect(rlhs, rargs.head).setType(bt)
+ }
case _ => {
if (!silent) unit.error(tree.pos, "apply on unexpected type")
throw ImpureCodeEncounteredException(tree)
}
}
}
+ // for now update only happens with array. later it might have to be distinguish in function of the lhs
+ case ExUpdate(lhs, index, newValue) => {
+ val lhsRec = rec(lhs)
+ val indexRec = rec(index)
+ val newValueRec = rec(newValue)
+ ArrayUpdate(lhsRec, indexRec, newValueRec).setType(newValueRec.getType)
+ }
+ case ExArrayFill(baseType, length, defaultValue) => {
+ val underlying = scalaType2PureScala(unit, silent)(baseType.tpe)
+ val lengthRec = rec(length)
+ val defaultValueRec = rec(defaultValue)
+ ArrayFill(lengthRec, defaultValueRec).setType(underlying)
+ }
case ExIfThenElse(t1,t2,t3) => {
val r1 = rec(t1)
val r2 = rec(t2)
@@ -906,6 +927,7 @@ trait CodeExtraction extends Extractors {
case TypeRef(_, sym, List(t1,t2,t3,t4)) if isTuple4(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4)))
case TypeRef(_, sym, List(t1,t2,t3,t4,t5)) if isTuple5(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4),rec(t5)))
case TypeRef(_, sym, ftt :: ttt :: Nil) if isFunction1TraitSym(sym) => FunctionType(List(rec(ftt)), rec(ttt))
+ case TypeRef(_, sym, btt :: Nil) if isArrayClassSym(sym) => ArrayType(rec(btt))
case TypeRef(_, sym, Nil) if classesToClasses.keySet.contains(sym) => classDefToClassType(classesToClasses(sym))
case _ => {
if(!silent) {
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 04cece3d96670c4723fc09e13f0deaf2bf62dd09..020cc2537fefc0c5755dc7d3f294ff0fcfa22704 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -646,6 +646,14 @@ trait Extractors {
case _ => None
}
}
+ object ExUpdate {
+ def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
+ case Apply(
+ Select(lhs, update),
+ index :: newValue :: Nil) if(update.toString == "update") => Some((lhs, index, newValue))
+ case _ => None
+ }
+ }
object ExMapIsDefinedAt {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
@@ -653,5 +661,27 @@ trait Extractors {
case _ => None
}
}
+
+ object ExArrayFill {
+ def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
+ case Apply(
+ Apply(
+ Apply(
+ TypeApply(
+ Select(Select(Ident(scala), arrayObject), fillMethod),
+ baseType :: Nil
+ ),
+ length :: Nil
+ ),
+ defaultValue :: Nil
+ ),
+ manifest
+ ) if(scala.toString == "scala" &&
+ arrayObject.toString == "Array" &&
+ fillMethod.toString == "fill") => Some((baseType, length, defaultValue))
+ case _ => None
+ }
+ }
+
}
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index d1a39f7172fafb612c2201b2c4322615a0aabdef..7b36360152413f7159bea06eb424e52036dc33f5 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -249,6 +249,26 @@ object PrettyPrinter {
nsb = ppNary(nsb, Seq(k), "(", ",", ")", lvl)
nsb
}
+ case ArrayFill(size, v) => {
+ sb.append("Array.fill(")
+ pp(size, sb, lvl)
+ sb.append(")(")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
+ case ArraySelect(ar, i) => {
+ pp(ar, sb, lvl)
+ sb.append("(")
+ pp(i, sb, lvl)
+ sb.append(")")
+ }
+ case ArrayUpdate(ar, i, v) => {
+ pp(ar, sb, lvl)
+ sb.append("(")
+ pp(i, sb, lvl)
+ sb.append(") = ")
+ pp(v, sb, lvl)
+ }
case Distinct(exprs) => {
var nsb = sb
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 638db0c2024152c46b9f735263b11e9ce01b5ca2..b160e495e28fc126ab1b22434236113d72d961a7 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -379,6 +379,11 @@ object Trees {
val fixedType = BooleanType
}
+ /* Array operations */
+ case class ArrayFill(length: Expr, defaultValue: Expr) extends Expr
+ case class ArraySelect(array: Expr, index: Expr) extends Expr
+ case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr
+
/* List operations */
case class NilList(baseType: TypeTree) extends Expr with Terminal
case class Cons(head: Expr, tail: Expr) extends Expr
@@ -446,6 +451,8 @@ object Trees {
case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
+ case ArrayFill(t1, t2) => Some((t1, t2, ArrayFill))
+ case ArraySelect(t1, t2) => Some((t1, t2, ArraySelect))
case Concat(t1,t2) => Some((t1,t2,Concat))
case ListAt(t1,t2) => Some((t1,t2,ListAt))
case wh@While(t1, t2) => Some((t1,t2, (t1, t2) => While(t1, t2).setInvariant(wh.invariant).setPosInfo(wh)))
@@ -463,6 +470,7 @@ object Trees {
case FiniteSet(args) => Some((args, FiniteSet))
case FiniteMap(args) => Some((args, (as : Seq[Expr]) => FiniteMap(as.asInstanceOf[Seq[SingletonMap]])))
case FiniteMultiset(args) => Some((args, FiniteMultiset))
+ case ArrayUpdate(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdate(as(0), as(1), as(2))))
case Distinct(args) => Some((args, Distinct))
case Block(args, rest) => Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
case Tuple(args) => Some((args, Tuple))
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 31947bf28177682e1376f0fd013944ef9dc37c05..7983e48b0565afb844ed91b18f79c001c6439600 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -148,6 +148,7 @@ object TypeTrees {
case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
case class OptionType(base: TypeTree) extends TypeTree
case class FunctionType(from: List[TypeTree], to: TypeTree) extends TypeTree
+ case class ArrayType(base: TypeTree) extends TypeTree
sealed abstract class ClassType extends TypeTree {
val classDef: ClassTypeDef