diff --git a/build.sbt b/build.sbt
index 12e774b4a9bfbe67628ddbfad2bcdf712659c675..4de988e5dc18eb4aa5c9dbf6a9c8e7f6178f1ef9 100644
--- a/build.sbt
+++ b/build.sbt
@@ -10,6 +10,8 @@ scalacOptions += "-deprecation"
scalacOptions += "-unchecked"
+javacOptions += "-Xlint:unchecked"
+
libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.2"
libraryDependencies += "org.scalatest" %% "scalatest" % "1.8" % "test"
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
new file mode 100644
index 0000000000000000000000000000000000000000..24f37cb2b90755fe5a81d0dd593a8cfe9c8a0adf
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
@@ -0,0 +1,13 @@
+package leon.codegen.runtime;
+
+public class LeonCodeGenRuntimeException extends Exception {
+ private final String msg;
+
+ public LeonCodeGenRuntimeException(String msg) {
+ this.msg = msg;
+ }
+
+ public String getMessage() {
+ return this.msg;
+ }
+}
diff --git a/src/main/java/leon/codegen/runtime/Map.java b/src/main/java/leon/codegen/runtime/Map.java
new file mode 100644
index 0000000000000000000000000000000000000000..b82ba05c9090677d713d0af74b9b8e937ae66c78
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/Map.java
@@ -0,0 +1,50 @@
+package leon.codegen.runtime;
+
+import java.util.Arrays;
+import java.util.TreeMap;
+
+/** If someone wants to make it an efficient implementation of immutable
+ * sets, go ahead. */
+public final class Map {
+ private final TreeMap<Object,Object> _underlying;
+
+ protected final TreeMap<Object,Object> underlying() {
+ return _underlying;
+ }
+
+ public Map() {
+ _underlying = new TreeMap<Object,Object>();
+ }
+
+ // For Maps, it's simpler to build them by starting with empty and putting
+ // the elements in.
+ public void add(Object key, Object value) {
+ _underlying.put(key, value);
+ }
+
+ private Map(TreeMap<Object,Object> u) {
+ _underlying = u;
+ }
+
+ public boolean isDefinedAt(Object element) {
+ return underlying().containsKey(element);
+ }
+
+ public Object get(Object k) throws LeonCodeGenRuntimeException {
+ Object result = underlying().get(k);
+ if(result == null) {
+ throw new LeonCodeGenRuntimeException("Get of undefined key.");
+ }
+ return result;
+ }
+
+ public int size() {
+ return underlying().size();
+ }
+
+ public Map union(Map s) {
+ TreeMap<Object,Object> n = new TreeMap<Object,Object>(underlying());
+ n.putAll(s.underlying());
+ return new Map(n);
+ }
+}
diff --git a/src/main/java/leon/codegen/runtime/Set.java b/src/main/java/leon/codegen/runtime/Set.java
new file mode 100644
index 0000000000000000000000000000000000000000..df70fd057836ec84a85fc8f0be5750089c46257a
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/Set.java
@@ -0,0 +1,77 @@
+package leon.codegen.runtime;
+
+import java.util.Arrays;
+import java.util.Iterator;
+import java.util.TreeSet;
+
+/** If someone wants to make it an efficient implementation of immutable
+ * sets, go ahead. */
+public final class Set {
+ private final TreeSet<Object> _underlying;
+
+ protected final TreeSet<Object> underlying() {
+ return _underlying;
+ }
+
+ public Set() {
+ _underlying = new TreeSet<Object>();
+ }
+
+ public Set(Object[] elements) {
+ _underlying = new TreeSet<Object>(Arrays.asList(elements));
+ }
+
+ // Uses mutation!
+ public void add(Object e) {
+ _underlying.add(e);
+ }
+
+ public Iterator<Object> getElements() {
+ return _underlying.iterator();
+ }
+
+ private Set(TreeSet<Object> u) {
+ _underlying = u;
+ }
+
+ public boolean contains(Object element) {
+ return _underlying.contains(element);
+ }
+
+ public boolean subsetOf(Set s) {
+ for(Object o : _underlying) {
+ if(!s.underlying().contains(o)) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ public int size() {
+ return _underlying.size();
+ }
+
+ public Set union(Set s) {
+ TreeSet<Object> n = new TreeSet<Object>(underlying());
+ n.addAll(s.underlying());
+ return new Set(n);
+ }
+
+ public Set intersect(Set s) {
+ TreeSet<Object> n = new TreeSet<Object>();
+ for(Object o : _underlying) {
+ if(s.underlying().contains(o)) {
+ n.add(o);
+ }
+ }
+ return new Set(n);
+ }
+
+ public Set minus(Set s) {
+ TreeSet<Object> n = new TreeSet<Object>(_underlying);
+ for(Object o : s.underlying()) {
+ n.remove(o);
+ }
+ return new Set(n);
+ }
+}
diff --git a/src/main/java/leon/codegen/runtime/Tuple.java b/src/main/java/leon/codegen/runtime/Tuple.java
index c8f46923bdd47184264cf8ac73ce5a6b757de4fd..e010870ad1c17cceea99bce2725f6565eb5f7a53 100644
--- a/src/main/java/leon/codegen/runtime/Tuple.java
+++ b/src/main/java/leon/codegen/runtime/Tuple.java
@@ -3,25 +3,35 @@ package leon.codegen.runtime;
import java.util.Arrays;
public final class Tuple {
- private int arity;
- private Object[] elements;
+ private final Object[] elements;
// You may think that using varargs here would show less of the internals,
// however the bytecode is exactly the same, so let's reflect the reality
// instead.
- public Tuple(int arity, Object[] elements) {
- this.arity = arity;
+ public Tuple(Object[] elements) {
this.elements = Arrays.copyOf(elements, elements.length);
}
public final Object get(int index) {
- if(index < 0 || index >= arity) {
+ if(index < 0 || index >= this.elements.length) {
throw new IllegalArgumentException("Invalid tuple index : " + index);
}
return this.elements[index];
}
public final int getArity() {
- return this.arity;
+ return this.elements.length;
+ }
+
+ @Override
+ public boolean equals(Object that) {
+ if(that == this) return true;
+ if(!(that instanceof Tuple)) return false;
+ Tuple other = (Tuple)that;
+ if(other.getArity() != this.getArity()) return false;
+ for(int i = 0; i < this.getArity(); i++) {
+ if(other.get(i) != this.get(i)) return false;
+ }
+ return true;
}
}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index b585b5b1c36573d939be3b499379d59be3c19f94..7ed53e440042d9e0507391e86bd131ce0112c335 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -17,7 +17,8 @@ object CodeGeneration {
private val BoxedIntClass = "java/lang/Integer"
private val BoxedBoolClass = "java/lang/Boolean"
- private val TupleClass = "leon/codegen/runtime/Tuple"
+ private val TupleClass = "leon/codegen/runtime/Tuple"
+ private val SetClass = "leon/codegen/runtime/Set"
private val CaseClassClass = "leon/codegen/runtime/CaseClass"
def defToJVMName(p : Program, d : Definition) : String = "Leon$CodeGen$" + d.id.uniqueName
@@ -30,9 +31,12 @@ object CodeGeneration {
case c : ClassType =>
env.classDefToClass(c.classDef).map(n => "L" + n + ";").getOrElse("Unsupported class " + c.id)
- case t : TupleType =>
+ case _ : TupleType =>
"L" + TupleClass + ";"
+ case _ : SetType =>
+ "L" + SetClass + ";"
+
case _ => throw CompilationException("Unsupported type : " + tpe)
}
@@ -49,7 +53,7 @@ object CodeGeneration {
case Int32Type | BooleanType =>
ch << IRETURN
- case _ : ClassType | _ : TupleType =>
+ case _ : ClassType | _ : TupleType | _ : SetType =>
ch << ARETURN
case other =>
@@ -132,7 +136,7 @@ object CodeGeneration {
case Tuple(es) =>
ch << New(TupleClass) << DUP
- ch << Ldc(es.size) << DUP
+ ch << Ldc(es.size)
ch << NewArray("java/lang/Object")
for((e,i) <- es.zipWithIndex) {
ch << DUP
@@ -140,7 +144,7 @@ object CodeGeneration {
mkBoxedExpr(e, ch)
ch << AASTORE
}
- ch << InvokeSpecial(TupleClass, constructorName, "(I[Ljava/lang/Object;)V")
+ ch << InvokeSpecial(TupleClass, constructorName, "([Ljava/lang/Object;)V")
case TupleSelect(t, i) =>
val TupleType(bs) = t.getType
@@ -149,6 +153,46 @@ object CodeGeneration {
ch << InvokeVirtual(TupleClass, "get", "(I)Ljava/lang/Object;")
mkUnbox(bs(i - 1), ch)
+ case EmptySet(_) =>
+ ch << DefaultNew(SetClass)
+
+ case FiniteSet(es) =>
+ ch << DefaultNew(SetClass)
+ for(e <- es) {
+ ch << DUP
+ mkBoxedExpr(e, ch)
+ ch << InvokeVirtual(SetClass, "add", "(Ljava/lang/Object;)V")
+ }
+
+ case ElementOfSet(e, s) =>
+ mkExpr(s, ch)
+ mkBoxedExpr(e, ch)
+ ch << InvokeVirtual(SetClass, "contains", "(Ljava/lang/Object;)Z")
+
+ case SetCardinality(s) =>
+ mkExpr(s, ch)
+ ch << InvokeVirtual(SetClass, "size", "()I")
+
+ case SubsetOf(s1, s2) =>
+ mkExpr(s1, ch)
+ mkExpr(s2, ch)
+ ch << InvokeVirtual(SetClass, "subsetOf", "(L%s;)Z".format(SetClass))
+
+ case SetIntersection(s1, s2) =>
+ mkExpr(s1, ch)
+ mkExpr(s2, ch)
+ ch << InvokeVirtual(SetClass, "intersect", "(L%s;)L%s;".format(SetClass,SetClass))
+
+ case SetUnion(s1, s2) =>
+ mkExpr(s1, ch)
+ mkExpr(s2, ch)
+ ch << InvokeVirtual(SetClass, "union", "(L%s;)L%s;".format(SetClass,SetClass))
+
+ case SetDifference(s1, s2) =>
+ mkExpr(s1, ch)
+ mkExpr(s2, ch)
+ ch << InvokeVirtual(SetClass, "minus", "(L%s;)L%s;".format(SetClass,SetClass))
+
case IfExpr(c, t, e) =>
val tl = ch.getFreshLabel("then")
val el = ch.getFreshLabel("else")
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 6f5d2aff477af4e27369bb790f3d58084b3802f6..844152a3d07325efc40b9e86d23c8bdd728e6977 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -429,6 +429,8 @@ object Trees {
/* Set expressions */
case class EmptySet(baseType: TypeTree) extends Expr with Terminal
case class FiniteSet(elements: Seq[Expr]) extends Expr
+ // TODO : Figure out what evaluation order is, for this.
+ // Perhaps then rewrite as "contains".
case class ElementOfSet(element: Expr, set: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
diff --git a/src/test/resources/regression/codegen/Prog004.scala b/src/test/resources/regression/codegen/Prog004.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cf5ece1a1a0e9d85ace9fbefdf4f70c43ffe7a15
--- /dev/null
+++ b/src/test/resources/regression/codegen/Prog004.scala
@@ -0,0 +1,17 @@
+object Prog004 {
+ def set1() : Set[Int] = {
+ Set(6, 7)
+ }
+
+ def set2() : Set[Int] = {
+ set1() ++ Set(4)
+ }
+
+ def set3() : Set[Int] = {
+ set2() ** set1()
+ }
+
+ def set4() : Set[Int] = {
+ set2() -- set1()
+ }
+}