Skip to content
Snippets Groups Projects
Commit 1b3e61b0 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Move Option to lang.Option, add Map.get/getOrElse/+

parent 3ef201af
Branches
Tags
No related merge requests found
Showing
with 93 additions and 7 deletions
...@@ -297,6 +297,10 @@ Map ...@@ -297,6 +297,10 @@ Map
m isDefinedAt index m isDefinedAt index
m contains index m contains index
m.updated(index, value) m.updated(index, value)
m + (index -> value)
m + (value, index)
m.get(index)
m.getOrElse(index, value2)
Function Function
......
...@@ -12,10 +12,21 @@ object Map { ...@@ -12,10 +12,21 @@ object Map {
} }
@ignore @ignore
case class Map[A, B](val theMap: scala.collection.immutable.Map[A,B]) { case class Map[A, B] (theMap: scala.collection.immutable.Map[A,B]) {
def apply(k: A): B = theMap.apply(k) def apply(k: A): B = theMap.apply(k)
def ++(b: Map[A, B]): Map[A,B] = new Map (theMap ++ b.theMap) def ++(b: Map[A, B]): Map[A,B] = new Map (theMap ++ b.theMap)
def updated(k: A, v: B): Map[A,B] = new Map(theMap.updated(k, v)) def updated(k: A, v: B): Map[A,B] = new Map(theMap.updated(k, v))
def contains(a: A): Boolean = theMap.contains(a) def contains(a: A): Boolean = theMap.contains(a)
def isDefinedAt(a: A): Boolean = contains(a) def isDefinedAt(a: A): Boolean = contains(a)
def +(kv: (A, B)): Map[A,B] = updated(kv._1, kv._2)
def +(k: A, v: B): Map[A,B] = updated(k, v)
def getOrElse(k: A, default: B): B = get(k).getOrElse(default)
def get(k: A): Option[B] = if (contains(k)) {
Some[B](apply(k))
} else {
None[B]()
}
} }
/* Copyright 2009-2015 EPFL, Lausanne */ /* Copyright 2009-2015 EPFL, Lausanne */
package leon.collection package leon.lang
import leon.annotation._ import leon.annotation._
......
...@@ -520,6 +520,7 @@ trait CodeExtraction extends ASTExtractors { ...@@ -520,6 +520,7 @@ trait CodeExtraction extends ASTExtractors {
parent.foreach(_.classDef.registerChildren(ccd)) parent.foreach(_.classDef.registerChildren(ccd))
classesToClasses += sym -> ccd classesToClasses += sym -> ccd
val fields = args.map { case (symbol, t) => val fields = args.map { case (symbol, t) =>
...@@ -1704,6 +1705,19 @@ trait CodeExtraction extends ASTExtractors { ...@@ -1704,6 +1705,19 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, MapType(_, vt)), "apply", List(a2)) => case (IsTyped(a1, MapType(_, vt)), "apply", List(a2)) =>
MapGet(a1, a2) MapGet(a1, a2)
case (IsTyped(a1, MapType(_, vt)), "get", List(a2)) =>
val someClass = CaseClassType(libraryCaseClass(sym.pos, "leon.lang.Some"), Seq(vt))
val noneClass = CaseClassType(libraryCaseClass(sym.pos, "leon.lang.None"), Seq(vt))
IfExpr(MapIsDefinedAt(a1, a2).setPos(current.pos),
CaseClass(someClass, Seq(MapGet(a1, a2).setPos(current.pos))).setPos(current.pos),
CaseClass(noneClass, Seq()).setPos(current.pos))
case (IsTyped(a1, MapType(_, vt)), "getOrElse", List(a2, a3)) =>
IfExpr(MapIsDefinedAt(a1, a2).setPos(current.pos),
MapGet(a1, a2).setPos(current.pos),
a3)
case (IsTyped(a1, mt: MapType), "isDefinedAt", List(a2)) => case (IsTyped(a1, mt: MapType), "isDefinedAt", List(a2)) =>
MapIsDefinedAt(a1, a2) MapIsDefinedAt(a1, a2)
...@@ -1713,6 +1727,17 @@ trait CodeExtraction extends ASTExtractors { ...@@ -1713,6 +1727,17 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, mt: MapType), "updated", List(k, v)) => case (IsTyped(a1, mt: MapType), "updated", List(k, v)) =>
MapUnion(a1, FiniteMap(Seq((k, v)), mt.from, mt.to)) MapUnion(a1, FiniteMap(Seq((k, v)), mt.from, mt.to))
case (IsTyped(a1, mt: MapType), "+", List(k, v)) =>
MapUnion(a1, FiniteMap(Seq((k, v)), mt.from, mt.to))
case (IsTyped(a1, mt: MapType), "+", List(IsTyped(kv, TupleType(List(_, _))))) =>
kv match {
case Tuple(List(k, v)) =>
MapUnion(a1, FiniteMap(Seq((k, v)), mt.from, mt.to))
case kv =>
MapUnion(a1, FiniteMap(Seq((TupleSelect(kv, 1), TupleSelect(kv, 2))), mt.from, mt.to))
}
case (IsTyped(a1, mt1: MapType), "++", List(IsTyped(a2, mt2: MapType))) if mt1 == mt2 => case (IsTyped(a1, mt1: MapType), "++", List(IsTyped(a2, mt2: MapType))) if mt1 == mt2 =>
MapUnion(a1, a2) MapUnion(a1, a2)
......
...@@ -225,7 +225,12 @@ abstract class SMTLIBSolver(val context: LeonContext, ...@@ -225,7 +225,12 @@ abstract class SMTLIBSolver(val context: LeonContext,
case MapType(from, to) => case MapType(from, to) =>
// We expect a RawArrayValue with keys in from and values in Option[to], // We expect a RawArrayValue with keys in from and values in Option[to],
// with default value == None // with default value == None
require(from == r.keyTpe && r.default == OptionManager.mkLeonNone(to)) if (r.default != OptionManager.mkLeonNone(to)) {
reporter.warning("Co-finite maps are not supported. (Default was "+r.default+")")
throw new IllegalArgumentException
}
require(r.keyTpe == from, s"Type error in solver model, expected $from, found ${r.keyTpe}")
val elems = r.elems.flatMap { val elems = r.elems.flatMap {
case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x) case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x)
case (k, _) => None case (k, _) => None
......
...@@ -156,6 +156,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve ...@@ -156,6 +156,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
case DefineFun(SMTFunDef(a, Seq(SortedVar(arg, akind)), rkind, body)) => case DefineFun(SMTFunDef(a, Seq(SortedVar(arg, akind)), rkind, body)) =>
val (argTpe, retTpe) = tpe match { val (argTpe, retTpe) = tpe match {
case SetType(base) => (base, BooleanType) case SetType(base) => (base, BooleanType)
case MapType(from, to) => (from, OptionManager.leonOptionType(to))
case ArrayType(base) => (Int32Type, base) case ArrayType(base) => (Int32Type, base)
case FunctionType(args, ret) => (tupleTypeWrap(args), ret) case FunctionType(args, ret) => (tupleTypeWrap(args), ret)
case RawArrayType(from, to) => (from, to) case RawArrayType(from, to) => (from, to)
......
...@@ -11,9 +11,9 @@ case class Library(pgm: Program) { ...@@ -11,9 +11,9 @@ case class Library(pgm: Program) {
lazy val Cons = lookup("leon.collection.Cons") collect { case ccd : CaseClassDef => ccd } lazy val Cons = lookup("leon.collection.Cons") collect { case ccd : CaseClassDef => ccd }
lazy val Nil = lookup("leon.collection.Nil") collect { case ccd : CaseClassDef => ccd } lazy val Nil = lookup("leon.collection.Nil") collect { case ccd : CaseClassDef => ccd }
lazy val Option = lookup("leon.collection.Option") collect { case acd : AbstractClassDef => acd } lazy val Option = lookup("leon.lang.Option") collect { case acd : AbstractClassDef => acd }
lazy val Some = lookup("leon.collection.Some") collect { case ccd : CaseClassDef => ccd } lazy val Some = lookup("leon.lang.Some") collect { case ccd : CaseClassDef => ccd }
lazy val None = lookup("leon.collection.None") collect { case ccd : CaseClassDef => ccd } lazy val None = lookup("leon.lang.None") collect { case ccd : CaseClassDef => ccd }
lazy val String = lookup("leon.lang.string.String") collect { case ccd : CaseClassDef => ccd } lazy val String = lookup("leon.lang.string.String") collect { case ccd : CaseClassDef => ccd }
......
...@@ -3,7 +3,6 @@ package leon.blup ...@@ -3,7 +3,6 @@ package leon.blup
import leon._ import leon._
import leon.lang._ import leon.lang._
import leon.annotation._ import leon.annotation._
import leon.collection.{Option,None,Some}
//import leon.proof._ //import leon.proof._
// FIXME: the following should go into the leon.proof package object. // FIXME: the following should go into the leon.proof package object.
......
import leon.lang._
object MapGetOrElse2 {
def test1(a: Map[BigInt, BigInt]) = {
require(!(a contains 0))
a.get(0)
} ensuring {
_ == None[BigInt]()
}
def test2(a: Map[BigInt, BigInt]) = {
require(!(a contains 0))
a.getOrElse(0, 0)
} ensuring {
_ == 0
}
}
import leon.lang._
object MapGetPlus {
def test1(a: Map[BigInt, BigInt]) = {
require(!(a contains 0))
val b = a + (0, 1)
val c = a + (BigInt(0) -> BigInt(1))
b(0) == c(0)
}.holds
def test2(a: Map[BigInt, BigInt]) = {
require(!(a contains 0))
val t = (BigInt(0) -> BigInt(1))
val b = a + (0, 1)
val c = a + t
b(0) == c(0)
}.holds
}
import leon._ import leon._
import leon.lang._
import leon.collection._ import leon.collection._
object Parser { object Parser {
......
import leon._ import leon._
import leon.lang._
import leon.collection._ import leon.collection._
object Parser { object Parser {
......
import leon._ import leon._
import leon.lang._
import leon.collection._ import leon.collection._
object Parser { object Parser {
......
import leon._ import leon._
import leon.lang._
import leon.collection._ import leon.collection._
object Parser { object Parser {
......
import leon._ import leon._
import leon.lang._
import leon.collection._ import leon.collection._
object Parser { object Parser {
......
import leon._ import leon._
import leon.lang._
import leon.collection._ import leon.collection._
object Parser { object Parser {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment