From 282f172c2f669311648d3621fa17c5d3b17ca9ac Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 13 Jul 2016 10:24:17 +0200
Subject: [PATCH] Added datagen, continued working on trees
---
.../scala/inox/datagen/DataGenerator.scala | 26 +
.../scala/inox/datagen/GrammarDataGen.scala | 94 ++
.../scala/inox/datagen/NaiveDataGen.scala | 104 +++
.../scala/inox/datagen/SolverDataGen.scala | 83 ++
.../scala/inox/datagen/VanuatooDataGen.scala | 409 +++++++++
.../inox/evaluators/AbstractEvaluator.scala | 357 --------
.../evaluators/AbstractOnlyEvaluator.scala | 275 ------
.../inox/evaluators/AngelicEvaluator.scala | 46 -
.../inox/evaluators/CodeGenEvaluator.scala | 78 --
.../scala/inox/evaluators/DualEvaluator.scala | 138 ---
.../inox/evaluators/EvaluationPhase.scala | 55 --
.../inox/evaluators/ScalacEvaluator.scala | 459 ----------
.../inox/evaluators/StreamEvaluator.scala | 718 ---------------
.../inox/evaluators/TracingEvaluator.scala | 118 ---
.../inox/evaluators/TrackingEvaluator.scala | 124 ---
.../scala/inox/solvers/EvaluatingSolver.scala | 20 -
src/main/scala/inox/solvers/RawArray.scala | 81 --
.../inox/solvers/string/StringSolver.scala | 18 +-
.../unrolling}/Quantification.scala | 0
src/main/scala/inox/trees/CallGraph.scala | 4 +-
src/main/scala/inox/trees/Constructors.scala | 17 +-
.../inox/trees/DefinitionTransformer.scala | 218 -----
src/main/scala/inox/trees/Definitions.scala | 20 +-
.../scala/inox/trees/DependencyFinder.scala | 103 ---
src/main/scala/inox/trees/ExprOps.scala | 14 +-
src/main/scala/inox/trees/Extractors.scala | 14 +-
src/main/scala/inox/trees/GenTreeOps.scala | 24 +-
src/main/scala/inox/trees/Path.scala | 231 -----
src/main/scala/inox/trees/Paths.scala | 232 +++++
src/main/scala/inox/trees/PrettyPrinter.scala | 756 ----------------
.../scala/inox/trees/PrinterHelpers.scala | 98 --
src/main/scala/inox/trees/Printers.scala | 835 ++++++++++++++++++
src/main/scala/inox/trees/Transformer.scala | 10 -
.../scala/inox/trees/TransformerWithPC.scala | 101 ---
.../scala/inox/trees/TreeTransformer.scala | 242 -----
src/main/scala/inox/trees/Trees.scala | 22 +-
src/main/scala/inox/trees/TypeOps.scala | 15 +-
src/main/scala/inox/trees/Types.scala | 16 +-
src/main/scala/inox/trees/package.scala | 4 +-
39 files changed, 1857 insertions(+), 4322 deletions(-)
create mode 100644 src/main/scala/inox/datagen/DataGenerator.scala
create mode 100644 src/main/scala/inox/datagen/GrammarDataGen.scala
create mode 100644 src/main/scala/inox/datagen/NaiveDataGen.scala
create mode 100644 src/main/scala/inox/datagen/SolverDataGen.scala
create mode 100644 src/main/scala/inox/datagen/VanuatooDataGen.scala
delete mode 100644 src/main/scala/inox/evaluators/AbstractEvaluator.scala
delete mode 100644 src/main/scala/inox/evaluators/AbstractOnlyEvaluator.scala
delete mode 100644 src/main/scala/inox/evaluators/AngelicEvaluator.scala
delete mode 100644 src/main/scala/inox/evaluators/CodeGenEvaluator.scala
delete mode 100644 src/main/scala/inox/evaluators/DualEvaluator.scala
delete mode 100644 src/main/scala/inox/evaluators/EvaluationPhase.scala
delete mode 100644 src/main/scala/inox/evaluators/ScalacEvaluator.scala
delete mode 100644 src/main/scala/inox/evaluators/StreamEvaluator.scala
delete mode 100644 src/main/scala/inox/evaluators/TracingEvaluator.scala
delete mode 100644 src/main/scala/inox/evaluators/TrackingEvaluator.scala
delete mode 100644 src/main/scala/inox/solvers/EvaluatingSolver.scala
delete mode 100644 src/main/scala/inox/solvers/RawArray.scala
rename src/main/scala/inox/{trees => solvers/unrolling}/Quantification.scala (100%)
delete mode 100644 src/main/scala/inox/trees/DefinitionTransformer.scala
delete mode 100644 src/main/scala/inox/trees/DependencyFinder.scala
delete mode 100644 src/main/scala/inox/trees/Path.scala
create mode 100644 src/main/scala/inox/trees/Paths.scala
delete mode 100644 src/main/scala/inox/trees/PrettyPrinter.scala
delete mode 100644 src/main/scala/inox/trees/PrinterHelpers.scala
create mode 100644 src/main/scala/inox/trees/Printers.scala
delete mode 100644 src/main/scala/inox/trees/Transformer.scala
delete mode 100644 src/main/scala/inox/trees/TransformerWithPC.scala
delete mode 100644 src/main/scala/inox/trees/TreeTransformer.scala
diff --git a/src/main/scala/inox/datagen/DataGenerator.scala b/src/main/scala/inox/datagen/DataGenerator.scala
new file mode 100644
index 000000000..ea6aac313
--- /dev/null
+++ b/src/main/scala/inox/datagen/DataGenerator.scala
@@ -0,0 +1,26 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package datagen
+
+import purescala.Expressions._
+import purescala.Common._
+import utils._
+
+import java.util.concurrent.atomic.AtomicBoolean
+
+trait DataGenerator extends Interruptible {
+ implicit val debugSection = DebugSectionDataGen
+
+ def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]]
+
+ protected val interrupted: AtomicBoolean = new AtomicBoolean(false)
+
+ def interrupt(): Unit = {
+ interrupted.set(true)
+ }
+
+ def recoverInterrupt(): Unit = {
+ interrupted.set(false)
+ }
+}
diff --git a/src/main/scala/inox/datagen/GrammarDataGen.scala b/src/main/scala/inox/datagen/GrammarDataGen.scala
new file mode 100644
index 000000000..ffe7b8b47
--- /dev/null
+++ b/src/main/scala/inox/datagen/GrammarDataGen.scala
@@ -0,0 +1,94 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package datagen
+
+import purescala.Expressions._
+import purescala.Types._
+import purescala.Common._
+import purescala.Constructors._
+import purescala.Extractors._
+import purescala.ExprOps._
+import evaluators._
+import bonsai.enumerators._
+
+import grammars._
+import utils.UniqueCounter
+import utils.SeqUtils.cartesianProduct
+
+/** Utility functions to generate values of a given type.
+ * In fact, it could be used to generate *terms* of a given type,
+ * e.g. by passing trees representing variables for the "bounds". */
+class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar = ValueGrammar) extends DataGenerator {
+ implicit val ctx = evaluator.context
+
+ // Assume e contains generic values with index 0.
+ // Return a series of expressions with all normalized combinations of generic values.
+ private def expandGenerics(e: Expr): Seq[Expr] = {
+ val c = new UniqueCounter[TypeParameter]
+ val withUniqueCounters: Expr = postMap {
+ case GenericValue(t, _) =>
+ Some(GenericValue(t, c.next(t)))
+ case _ => None
+ }(e)
+
+ val indices = c.current
+
+ val (tps, substInt) = (for {
+ tp <- indices.keySet.toSeq
+ } yield tp -> (for {
+ from <- 0 to indices(tp)
+ to <- 0 to from
+ } yield (from, to))).unzip
+
+ val combos = cartesianProduct(substInt)
+
+ val substitutions = combos map { subst =>
+ tps.zip(subst).map { case (tp, (from, to)) =>
+ (GenericValue(tp, from): Expr) -> (GenericValue(tp, to): Expr)
+ }.toMap
+ }
+
+ substitutions map (replace(_, withUniqueCounters))
+
+ }
+
+ def generate(tpe: TypeTree): Iterator[Expr] = {
+ val enum = new MemoizedEnumerator[Label, Expr, ProductionRule[Label, Expr]](grammar.getProductions)
+ enum.iterator(Label(tpe)).flatMap(expandGenerics).takeWhile(_ => !interrupted.get)
+ }
+
+ def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = {
+
+ def filterCond(vs: Seq[Expr]): Boolean = satisfying match {
+ case BooleanLiteral(true) =>
+ true
+ case e =>
+ // in -> e should be enough. We shouldn't find any subexpressions of in.
+ evaluator.eval(e, (ins zip vs).toMap) match {
+ case EvaluationResults.Successful(BooleanLiteral(true)) => true
+ case _ => false
+ }
+ }
+
+ if (ins.isEmpty) {
+ Iterator(Seq[Expr]()).filter(filterCond)
+ } else {
+ val values = generate(tupleTypeWrap(ins.map{ _.getType }))
+
+ val detupled = values.map {
+ v => unwrapTuple(v, ins.size)
+ }
+
+ detupled.take(maxEnumerated)
+ .filter(filterCond)
+ .take(maxValid)
+ .takeWhile(_ => !interrupted.get)
+ }
+ }
+
+ def generateMapping(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int) = {
+ generateFor(ins, satisfying, maxValid, maxEnumerated) map (ins zip _)
+ }
+
+}
diff --git a/src/main/scala/inox/datagen/NaiveDataGen.scala b/src/main/scala/inox/datagen/NaiveDataGen.scala
new file mode 100644
index 000000000..e40359e68
--- /dev/null
+++ b/src/main/scala/inox/datagen/NaiveDataGen.scala
@@ -0,0 +1,104 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package datagen
+
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.Definitions._
+import purescala.Quantification._
+import utils.StreamUtils._
+
+import evaluators._
+
+import scala.collection.mutable.{Map=>MutableMap}
+
+/** Utility functions to generate values of a given type.
+ * In fact, it could be used to generate *terms* of a given type,
+ * e.g. by passing trees representing variables for the "bounds". */
+@deprecated("Stream-based datagen is deprecated, use GrammarDataGen with ValueGrammar instead", "3.0")
+class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds : Option[Map[TypeTree,Seq[Expr]]] = None) extends DataGenerator {
+
+ val bounds = _bounds.getOrElse(Map())
+
+ private def tpStream(tp: TypeParameter, i: Int = 1): Stream[Expr] = Stream.cons(GenericValue(tp, i), tpStream(tp, i+1))
+
+ private val streamCache : MutableMap[TypeTree,Stream[Expr]] = MutableMap.empty
+ def generate(tpe : TypeTree) : Stream[Expr] = {
+ try {
+ streamCache.getOrElse(tpe, {
+ val s = generate0(tpe)
+ streamCache(tpe) = s
+ s
+ })
+ } catch {
+ case so: StackOverflowError =>
+ Stream.empty
+ }
+ }
+
+ private def generate0(tpe: TypeTree): Stream[Expr] = bounds.get(tpe).map(_.toStream).getOrElse {
+ tpe match {
+ case BooleanType =>
+ BooleanLiteral(true) #:: BooleanLiteral(false) #:: Stream.empty
+
+ case Int32Type =>
+ IntLiteral(0) #:: IntLiteral(1) #:: IntLiteral(2) #:: IntLiteral(-1) #:: Stream.empty
+
+ case tp: TypeParameter =>
+ tpStream(tp)
+
+ case TupleType(bses) =>
+ cartesianProduct(bses.map(generate)).map(Tuple)
+
+ case act : AbstractClassType =>
+ // We prioritize base cases among the children.
+ // Otherwise we run the risk of infinite recursion when
+ // generating lists.
+ val ccChildren = act.knownCCDescendants
+
+ val (leafs,conss) = ccChildren.partition(_.fields.isEmpty)
+
+ // FIXME: Will not work for mutually recursive types
+ val sortedConss = conss sortBy { _.fields.count{ _.getType.isInstanceOf[ClassType]}}
+
+ // The stream for leafs...
+ val leafsStream = leafs.toStream.flatMap(generate)
+
+ // ...to which we append the streams for constructors.
+ leafsStream.append(interleave(sortedConss.map(generate)))
+
+ case cct : CaseClassType =>
+ if(cct.fields.isEmpty) {
+ Stream.cons(CaseClass(cct, Nil), Stream.empty)
+ } else {
+ val fieldTypes = cct.fieldsTypes
+ cartesianProduct(fieldTypes.map(generate)).map(CaseClass(cct, _))
+ }
+
+ case _ => Stream.empty
+ }
+ }
+
+ def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid : Int, maxEnumerated : Int) : Iterator[Seq[Expr]] = {
+ val filtering = if (satisfying == BooleanLiteral(true)) {
+ { (e: Seq[Expr]) => true }
+ } else {
+ evaluator.compile(satisfying, ins).map { evalFun =>
+ val sat = EvaluationResults.Successful(BooleanLiteral(true))
+
+ { (e: Seq[Expr]) => evalFun(new solvers.Model((ins zip e).toMap)) == sat }
+ } getOrElse {
+ { (e: Seq[Expr]) => false }
+ }
+ }
+
+ cartesianProduct(ins.map(id => generate(id.getType)))
+ .take(maxEnumerated)
+ .takeWhile(s => !interrupted.get)
+ .filter{filtering}
+ .take(maxValid)
+ .iterator
+ }
+}
diff --git a/src/main/scala/inox/datagen/SolverDataGen.scala b/src/main/scala/inox/datagen/SolverDataGen.scala
new file mode 100644
index 000000000..37dcfba06
--- /dev/null
+++ b/src/main/scala/inox/datagen/SolverDataGen.scala
@@ -0,0 +1,83 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package datagen
+
+import purescala.Expressions._
+import purescala.Types._
+import purescala.Definitions._
+import purescala.Common._
+import purescala.Constructors._
+import solvers._
+import utils._
+
+class SolverDataGen(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) extends DataGenerator {
+ implicit val ctx0 = ctx
+
+ def generate(tpe: TypeTree): FreeableIterator[Expr] = {
+ generateFor(Seq(FreshIdentifier("tmp", tpe)), BooleanLiteral(true), 20, 20).map(_.head).takeWhile(_ => !interrupted.get)
+ }
+
+ def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): FreeableIterator[Seq[Expr]] = {
+ if (ins.isEmpty) {
+ FreeableIterator.empty
+ } else {
+
+ var fds = Map[ClassDef, FunDef]()
+
+ def sizeFor(of: Expr): Expr = of.getType match {
+ case AbstractClassType(acd, tps) =>
+ val fd = fds.getOrElse(acd, {
+ val actDef = AbstractClassType(acd, acd.tparams.map(_.tp))
+
+ val e = FreshIdentifier("e", actDef)
+
+ val fd: FunDef = new FunDef(FreshIdentifier("sizeOf", Untyped), acd.tparams, Seq(ValDef(e)), IntegerType)
+
+ fds += acd -> fd
+
+
+ fd.body = Some(MatchExpr(e.toVariable,
+ actDef.knownCCDescendants.map { cct =>
+ val fields = cct.fieldsTypes.map ( t => FreshIdentifier("field", t))
+
+ val rhs = fields.foldLeft(InfiniteIntegerLiteral(1): Expr) { (i, f) =>
+ plus(i, sizeFor(f.toVariable))
+ }
+
+ MatchCase(CaseClassPattern(None, cct, fields.map(f => WildcardPattern(Some(f)))), None, rhs)
+ }
+ ))
+
+ fd
+ })
+
+ FunctionInvocation(fd.typed(tps), Seq(of))
+
+ case tt @ TupleType(tps) =>
+ val exprs = for ((t,i) <- tps.zipWithIndex) yield {
+ sizeFor(tupleSelect(of, i+1, tps.size))
+ }
+
+ exprs.foldLeft(InfiniteIntegerLiteral(1): Expr)(plus)
+
+ case _ =>
+ InfiniteIntegerLiteral(1)
+ }
+
+ val sizeOf = sizeFor(tupleWrap(ins.map(_.toVariable)))
+
+ // We need to synthesize a size function for ins' types.
+ val pgm1 = Program(pgm.units :+ UnitDef(FreshIdentifier("new"), List(
+ ModuleDef(FreshIdentifier("new"), fds.values.toSeq, false)
+ )))
+
+ val modelEnum = new ModelEnumerator(ctx, pgm1, sf)
+
+ val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
+
+ enum.take(maxValid).map(model => ins.map(model)).takeWhile(_ => !interrupted.get)
+ }
+ }
+
+}
diff --git a/src/main/scala/inox/datagen/VanuatooDataGen.scala b/src/main/scala/inox/datagen/VanuatooDataGen.scala
new file mode 100644
index 000000000..ccba55af9
--- /dev/null
+++ b/src/main/scala/inox/datagen/VanuatooDataGen.scala
@@ -0,0 +1,409 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package datagen
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.ExprOps._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.Extractors._
+import purescala.Constructors._
+
+import codegen.CompilationUnit
+import codegen.CodeGenParams
+import codegen.runtime.StdMonitor
+import vanuatoo.{Pattern => VPattern, _}
+
+import evaluators._
+
+class VanuatooDataGen(ctx: LeonContext, p: Program, bank: EvaluationBank = new EvaluationBank) extends DataGenerator {
+ val unit = new CompilationUnit(ctx, p, bank, CodeGenParams.default.copy(doInstrument = true))
+
+ val ints = (for (i <- Set(0, 1, 2, 3)) yield {
+ i -> Constructor[Expr, TypeTree](List(), Int32Type, s => IntLiteral(i), ""+i)
+ }).toMap
+
+ val bigInts = (for (i <- Set(0, 1, 2, 3)) yield {
+ i -> Constructor[Expr, TypeTree](List(), IntegerType, s => InfiniteIntegerLiteral(i), ""+i)
+ }).toMap
+
+ val booleans = (for (b <- Set(true, false)) yield {
+ b -> Constructor[Expr, TypeTree](List(), BooleanType, s => BooleanLiteral(b), ""+b)
+ }).toMap
+
+ val chars = (for (c <- Set('a', 'b', 'c', 'd')) yield {
+ c -> Constructor[Expr, TypeTree](List(), CharType, s => CharLiteral(c), ""+c)
+ }).toMap
+
+ val rationals = (for (n <- Set(0, 1, 2, 3); d <- Set(1,2,3,4)) yield {
+ (n, d) -> Constructor[Expr, TypeTree](List(), RealType, s => FractionalLiteral(n, d), "" + n + "/" + d)
+ }).toMap
+
+ val strings = (for (b <- Set("", "a", "foo", "bar")) yield {
+ b -> Constructor[Expr, TypeTree](List(), StringType, s => StringLiteral(b), b)
+ }).toMap
+
+
+ def intConstructor(i: Int) = ints(i)
+
+ def bigIntConstructor(i: Int) = bigInts(i)
+
+ def boolConstructor(b: Boolean) = booleans(b)
+
+ def charConstructor(c: Char) = chars(c)
+
+ def rationalConstructor(n: Int, d: Int) = rationals(n -> d)
+
+ def stringConstructor(s: String) = strings(s)
+
+ lazy val stubValues = ints.values ++ bigInts.values ++ booleans.values ++ chars.values ++ rationals.values ++ strings.values
+
+ def cPattern(c: Constructor[Expr, TypeTree], args: Seq[VPattern[Expr, TypeTree]]) = {
+ ConstructorPattern[Expr, TypeTree](c, args)
+ }
+
+ private var constructors = Map[TypeTree, List[Constructor[Expr, TypeTree]]]()
+
+ private def getConstructorFor(t: CaseClassType, act: AbstractClassType): Constructor[Expr, TypeTree] = {
+ // We "up-cast" the returnType of the specific caseclass generator to match its superclass
+ getConstructors(t).head.copy(retType = act)
+ }
+
+ private def getConstructors(t: TypeTree): List[Constructor[Expr, TypeTree]] = t match {
+ case UnitType =>
+ constructors.getOrElse(t, {
+ val cs = List(Constructor[Expr, TypeTree](List(), t, s => UnitLiteral(), "()"))
+ constructors += t -> cs
+ cs
+ })
+
+ case at @ ArrayType(sub) =>
+ constructors.getOrElse(at, {
+ val cs = for (size <- List(0, 1, 2, 5)) yield {
+ Constructor[Expr, TypeTree](
+ (1 to size).map(i => sub).toList,
+ at,
+ s => finiteArray(s, None, sub),
+ at.asString(ctx)+"@"+size
+ )
+ }
+ constructors += at -> cs
+ cs
+ })
+
+ case st @ SetType(sub) =>
+ constructors.getOrElse(st, {
+ val cs = for (size <- List(0, 1, 2, 5)) yield {
+ Constructor[Expr, TypeTree](
+ (1 to size).map(i => sub).toList,
+ st,
+ s => FiniteSet(s.toSet, sub),
+ st.asString(ctx)+"@"+size
+ )
+ }
+ constructors += st -> cs
+ cs
+ })
+
+ case bt @ BagType(sub) =>
+ constructors.getOrElse(bt, {
+ val cs = for (size <- List(0, 1, 2, 5)) yield {
+ val subs = (1 to size).flatMap(i => List(sub, IntegerType)).toList
+ Constructor[Expr, TypeTree](subs, bt, s => FiniteBag(s.grouped(2).map {
+ case Seq(k, i @ InfiniteIntegerLiteral(v)) =>
+ k -> (if (v > 0) i else InfiniteIntegerLiteral(-v + 1))
+ }.toMap, sub), bt.asString(ctx)+"@"+size)
+ }
+ constructors += bt -> cs
+ cs
+ })
+
+ case tt @ TupleType(parts) =>
+ constructors.getOrElse(tt, {
+ val cs = List(Constructor[Expr, TypeTree](parts, tt, s => tupleWrap(s), tt.asString(ctx)))
+ constructors += tt -> cs
+ cs
+ })
+
+ case mt @ MapType(from, to) =>
+ constructors.getOrElse(mt, {
+ val cs = for (size <- List(0, 1, 2, 5)) yield {
+ val subs = (1 to size).flatMap(i => List(from, to)).toList
+ Constructor[Expr, TypeTree](subs, mt, s => FiniteMap(s.grouped(2).map(t => (t(0), t(1))).toMap, from, to), mt.asString(ctx)+"@"+size)
+ }
+ constructors += mt -> cs
+ cs
+ })
+
+ case ft @ FunctionType(from, to) =>
+ constructors.getOrElse(ft, {
+ val cs = for (size <- List(1, 2, 3, 5)) yield {
+ val subs = (1 to size).flatMap(_ => from :+ to).toList
+ Constructor[Expr, TypeTree](subs, ft, { s =>
+ val grouped = s.grouped(from.size + 1).toSeq
+ val mapping = grouped.init.map { case args :+ res => (args -> res) }
+ FiniteLambda(mapping, grouped.last.last, ft)
+ }, ft.asString(ctx) + "@" + size)
+ }
+ constructors += ft -> cs
+ cs
+ })
+
+ case tp: TypeParameter =>
+ constructors.getOrElse(tp, {
+ val cs = for (i <- List(1, 2)) yield {
+ Constructor[Expr, TypeTree](List(), tp, s => GenericValue(tp, i), tp.id+"#"+i)
+ }
+ constructors += tp -> cs
+ cs
+ })
+
+ case act: AbstractClassType =>
+ constructors.getOrElse(act, {
+ val cs = act.knownCCDescendants.map {
+ cct => getConstructorFor(cct, act)
+ }.toList
+
+ constructors += act -> cs
+
+ cs
+ })
+
+ case cct: CaseClassType =>
+ constructors.getOrElse(cct, {
+ val c = List(Constructor[Expr, TypeTree](cct.fieldsTypes, cct, s => CaseClass(cct, s), cct.id.name))
+ constructors += cct -> c
+ c
+ })
+
+ case _ =>
+ ctx.reporter.error("Unknown type to generate constructor for: "+t)
+ Nil
+ }
+
+ // Returns the pattern and whether it is fully precise
+ private def valueToPattern(v: AnyRef, expType: TypeTree): (VPattern[Expr, TypeTree], Boolean) = (v, expType) match {
+ case (i: Integer, Int32Type) =>
+ (cPattern(intConstructor(i), List()), true)
+
+ case (i: Integer, IntegerType) =>
+ (cPattern(bigIntConstructor(i), List()), true)
+
+ case (b: java.lang.Boolean, BooleanType) =>
+ (cPattern(boolConstructor(b), List()), true)
+
+ case (c: java.lang.Character, CharType) =>
+ (cPattern(charConstructor(c), List()), true)
+
+ case (b: java.lang.String, StringType) =>
+ (cPattern(stringConstructor(b), List()), true)
+
+ case (cc: codegen.runtime.CaseClass, ct: ClassType) =>
+ val r = cc.__getRead()
+
+ unit.jvmClassToLeonClass(cc.getClass.getName) match {
+ case Some(ccd: CaseClassDef) =>
+ val cct = CaseClassType(ccd, ct.tps)
+ val c = ct match {
+ case act : AbstractClassType =>
+ getConstructorFor(cct, act)
+ case cct : CaseClassType =>
+ getConstructors(cct).head
+ }
+
+ val fields = cc.productElements()
+
+ val elems = for (i <- 0 until fields.length) yield {
+ if (((r >> i) & 1) == 1) {
+ // has been read
+ valueToPattern(fields(i), cct.fieldsTypes(i))
+ } else {
+ (AnyPattern[Expr, TypeTree](), false)
+ }
+ }
+
+ (ConstructorPattern(c, elems.map(_._1)), elems.forall(_._2))
+
+ case _ =>
+ ctx.reporter.error("Could not retrieve type for :"+cc.getClass.getName)
+ (AnyPattern[Expr, TypeTree](), false)
+ }
+
+ case (t: codegen.runtime.Tuple, tpe) =>
+ val r = t.__getRead()
+
+ val parts = unwrapTupleType(tpe, t.getArity)
+
+ val c = getConstructors(tpe).head
+
+ val elems = for (i <- 0 until t.getArity) yield {
+ if (((r >> i) & 1) == 1) {
+ // has been read
+ valueToPattern(t.get(i), parts(i))
+ } else {
+ (AnyPattern[Expr, TypeTree](), false)
+ }
+ }
+
+ (ConstructorPattern(c, elems.map(_._1)), elems.forall(_._2))
+
+ case (gv: GenericValue, t: TypeParameter) =>
+ (cPattern(getConstructors(t)(gv.id-1), List()), true)
+
+ case (v, t) =>
+ ctx.reporter.debug("Unsupported value, can't paternify : "+v+" ("+v.getClass+") : "+t)
+ (AnyPattern[Expr, TypeTree](), false)
+ }
+
+ type InstrumentedResult = (EvaluationResults.Result[Expr], Option[vanuatoo.Pattern[Expr, TypeTree]])
+
+ def compile(expression: Expr, argorder: Seq[Identifier]) : Option[Expr=>InstrumentedResult] = {
+ import leon.codegen.runtime.LeonCodeGenRuntimeException
+ import leon.codegen.runtime.LeonCodeGenEvaluationException
+
+ try {
+ val ttype = tupleTypeWrap(argorder.map(_.getType))
+ val tid = FreshIdentifier("tup", ttype)
+
+ val map = argorder.zipWithIndex.map{ case (id, i) => id -> tupleSelect(Variable(tid), i + 1, argorder.size) }.toMap
+
+ val newExpr = replaceFromIDs(map, expression)
+
+ val ce = unit.compileExpression(newExpr, Seq(tid))(ctx)
+
+ Some((args : Expr) => {
+ try {
+ val monitor = new StdMonitor(unit, unit.params.maxFunctionInvocations, Map())
+
+ val jvmArgs = ce.argsToJVM(Seq(args), monitor)
+
+ val result = ce.evalFromJVM(jvmArgs, monitor)
+
+ // jvmArgs is getting updated by evaluating
+ val pattern = valueToPattern(jvmArgs.head, ttype)
+
+ (EvaluationResults.Successful(result), if (!pattern._2) Some(pattern._1) else None)
+ } catch {
+ case e : StackOverflowError =>
+ (EvaluationResults.RuntimeError(e.getMessage), None)
+
+ case e : ClassCastException =>
+ (EvaluationResults.RuntimeError(e.getMessage), None)
+
+ case e : ArithmeticException =>
+ (EvaluationResults.RuntimeError(e.getMessage), None)
+
+ case e : ArrayIndexOutOfBoundsException =>
+ (EvaluationResults.RuntimeError(e.getMessage), None)
+
+ case e : LeonCodeGenRuntimeException =>
+ (EvaluationResults.RuntimeError(e.getMessage), None)
+
+ case e : LeonCodeGenEvaluationException =>
+ (EvaluationResults.EvaluatorError(e.getMessage), None)
+ }
+ })
+ } catch {
+ case t: Throwable =>
+ ctx.reporter.warning("Error while compiling expression: "+t.getMessage); t.printStackTrace()
+ None
+ }
+ }
+
+ def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = {
+ // Split conjunctions
+ val TopLevelAnds(ands) = satisfying
+
+ val runners = ands.flatMap(a => compile(a, ins) match {
+ case Some(runner) => Some(runner)
+ case None =>
+ ctx.reporter.error("Could not compile predicate " + a)
+ None
+ })
+
+ val gen = new StubGenerator[Expr, TypeTree](stubValues.toSeq,
+ Some(getConstructors _),
+ treatEmptyStubsAsChildless = true)
+
+ /**
+ * Gather at most <n> isomoprhic models before skipping them
+ * - Too little means skipping many excluding patterns
+ * - Too large means repetitive (and not useful models) before reaching maxEnumerated
+ */
+
+ val maxIsomorphicModels = maxValid+1
+
+ val it = gen.enumerate(tupleTypeWrap(ins.map(_.getType)))
+
+ new Iterator[Seq[Expr]] {
+ var total = 0
+ var found = 0
+
+ var theNext: Option[Seq[Expr]] = None
+
+ def hasNext = {
+ if (total == 0) {
+ theNext = computeNext()
+ }
+
+ theNext.isDefined
+ }
+
+ def next() = {
+ val res = theNext.get
+ theNext = computeNext()
+ res
+ }
+
+
+ def computeNext(): Option[Seq[Expr]] = {
+ //return None
+ while (total < maxEnumerated && found < maxValid && it.hasNext && !interrupted.get) {
+ val model = it.next()
+ it.hasNext // FIXME: required for some reason by StubGenerator or will return false during loop check
+
+ if (model eq null) {
+ total = maxEnumerated
+ } else {
+ total += 1
+
+ var failed = false
+
+ for (r <- runners) r(model) match {
+ case (EvaluationResults.Successful(BooleanLiteral(true)), _) =>
+
+ case (_, Some(pattern)) =>
+ failed = true
+ it.exclude(pattern)
+
+ case (_, None) =>
+ failed = true;
+ }
+
+ if (!failed) {
+ //println("Got model:")
+ //for ((i, v) <- (ins zip model.exprs)) {
+ // println(" - "+i+" -> "+v)
+ //}
+
+ found += 1
+
+ if (found % maxIsomorphicModels == 0) {
+ it.skipIsomorphic()
+ }
+
+ return Some(unwrapTuple(model, ins.size))
+ }
+
+ //if (total % 1000 == 0) {
+ // println("... "+total+" ...")
+ //}
+ }
+ }
+ None
+ }
+ }
+ }
+}
diff --git a/src/main/scala/inox/evaluators/AbstractEvaluator.scala b/src/main/scala/inox/evaluators/AbstractEvaluator.scala
deleted file mode 100644
index 142628aff..000000000
--- a/src/main/scala/inox/evaluators/AbstractEvaluator.scala
+++ /dev/null
@@ -1,357 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import purescala.Extractors.Operator
-import purescala.Constructors._
-import purescala.Expressions._
-import purescala.Types._
-import purescala.Common.Identifier
-import purescala.Definitions.{TypedFunDef, Program}
-import purescala.DefOps
-import purescala.TypeOps
-import purescala.ExprOps
-import purescala.Expressions.Expr
-import leon.utils.DebugSectionSynthesis
-
-case class AbstractRecContext(mappings: Map[Identifier, Expr], mappingsAbstract: Map[Identifier, Expr]) extends RecContext[AbstractRecContext] {
- def newVars(news: Map[Identifier, Expr], newsAbstract: Map[Identifier, Expr]): AbstractRecContext = copy(news, newsAbstract)
- def newVars(news: Map[Identifier, Expr]): AbstractRecContext = copy(news, news)
-
- def withNewVar(id: Identifier, v: (Expr, Expr)): AbstractRecContext = {
- newVars(mappings + (id -> v._1), mappingsAbstract + (id -> v._2))
- }
-
- def withNewVars2(news: Map[Identifier, (Expr, Expr)]): AbstractRecContext = {
- newVars(mappings ++ news.mapValues(_._1), mappingsAbstract ++ news.mapValues(_._2))
- }
-
- override def withNewVar(id: Identifier, v: Expr): AbstractRecContext = {
- newVars(mappings + (id -> v), mappingsAbstract + (id -> v))
- }
-
- override def withNewVars(news: Map[Identifier, Expr]): AbstractRecContext = {
- newVars(mappings ++ news, mappingsAbstract ++ news)
- }
-}
-
-
-trait HasAbstractRecContext extends ContextualEvaluator {
- type RC = AbstractRecContext
- def initRC(mappings: Map[Identifier, Expr]) = AbstractRecContext(mappings, mappings)
-}
-
-/** The evaluation returns a pair (e, t),
- * where e is the expression evaluated as much as possible, and t is the way the expression has been evaluated.
- * Caution: If and Match statement require the condition to be non-abstract. */
-class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext with HasAbstractRecContext {
- lazy val scalaEv = new ScalacEvaluator(underlying, ctx, prog)
-
- /** Evaluates resuts which can be evaluated directly
- * For example, concatenation of two string literals */
- val underlying = new DefaultEvaluator(ctx, prog)
- underlying.setEvaluationFailOnChoose(true)
- override type Value = (Expr, Expr)
-
- override val description: String = "Evaluates string programs but keeps the formula which generated the value"
- override val name: String = "Abstract evaluator"
-
- /** True if CaseClassSelector(...CaseClass(...)) have to be simplified. */
- var evaluateCaseClassSelector = true
- /** True if Application(Lambda(), ...) have to be simplified. */
- var evaluateApplications = true
-
- // Used to make the final mkString for maps, sets, and bags. First column is the key to sort the expression on, second are the values and third are the trees.
- protected def mkString(elements: List[(String, Expr, Expr)], infix: (Expr, Expr)): (Expr, Expr) = {
- val (infix_value, infix_tree) = infix
- val (sorting_key, elements_value, elements_tree) = elements.sortBy(f => f._1).unzip3
-
- val fst = infix_value match {
- case StringLiteral(v) if elements_value.forall(_.isInstanceOf[StringLiteral]) =>
- StringLiteral(elements_value.map(_.asInstanceOf[StringLiteral].value).mkString(v))
- case infix_value =>
- elements_value match {
- case Nil => StringLiteral("")
- case a::q => q.foldLeft(a: Expr){ case (a, s) => StringConcat(StringConcat(a, infix_value), s) }
- }
- }
-
- val snd = elements_tree match {
- case Nil => StringLiteral("")
- case a::q => q.foldLeft(a){ case (a, s) => StringConcat(StringConcat(a, infix_tree), s) }
- }
- (fst, snd)
- }
-
- protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): (Expr, Expr) = {
- implicit def aToC: AbstractEvaluator.this.underlying.RC = DefaultRecContext(rctx.mappings.filter{ case (k, v) => ExprOps.isValue(v) })
- expr match {
- case Variable(id) =>
- (rctx.mappings.get(id), rctx.mappingsAbstract.get(id)) match {
- case (Some(v), Some(va)) =>
- (v, va)
- case _ =>
- (expr, expr)
- }
-
- case e if ExprOps.isValue(e) =>
- (e, e)
-
- case IfExpr(cond, thenn, elze) =>
- val first = underlying.e(cond)
- first match {
- case BooleanLiteral(true) =>
- ctx.reporter.ifDebug(printer => printer(thenn))(DebugSectionSynthesis)
- e(thenn)
- case BooleanLiteral(false) => e(elze)
- case _ => throw EvalError(typeErrorMsg(first, BooleanType))
- }
-
- case MatchExpr(scrut, cases) =>
- val (escrut, tscrut) = e(scrut)
- cases.toStream.map(c => matchesCaseAbstract(escrut, tscrut, c)).find(_.nonEmpty) match {
- case Some(Some((c, mappings))) => e(c.rhs)(rctx.withNewVars2(mappings), gctx)
- case _ => throw RuntimeError("MatchError(Abstract evaluation): "+escrut.asString+" did not match any of the cases :\n" + cases.mkString("\n"))
- }
-
- case FunctionInvocation(TypedFunDef(fd, Seq(ta, tb)), Seq(mp, inkv, betweenkv, fk, fv)) if fd == program.library.mapMkString.get =>
- val (inkv_str, inkv_tree) = e(inkv)
- val infix = e(betweenkv)
- val (mp_map, mp_tree) = e(mp) match {
- case (FiniteMap(theMap, keyType, valueType), t) => (theMap, t)
- case (e, f) =>
- println("First argument is not a finite map: " + e)
- throw EvalError(typeErrorMsg(mp, MapType(ta, tb)))
- }
-
- val res1 = mp_map.toList.map{ case (k, v) =>
- val (kvalue, ktree) = e(application(fk, Seq(k)))
- val (vvalue, vtree) = e(application(fv, Seq(v)))
- val abs_value = StringConcat(StringConcat(ktree, inkv_tree), vtree)
- kvalue match {
- case StringLiteral(k) =>
- if(ExprOps.isValue(vvalue) && ExprOps.isValue(inkv_str)) {
- underlying.e(StringConcat(StringConcat(kvalue, inkv_str), vvalue)) match {
- case sl@StringLiteral(s) => (s, sl, abs_value)
- case e => throw RuntimeError("Not a string literal: " + e)
- }
- } else {
- (k, StringConcat(StringConcat(kvalue, inkv_str), vvalue), abs_value)
- }
- case _ =>
- throw RuntimeError("cannot infer the order on which to print the map " + mp_map)
- }
- }
-
- mkString(res1, infix)
-
- case FunctionInvocation(TypedFunDef(fd, Seq(ta)), Seq(mp, inf, f)) if fd == program.library.setMkString.get =>
- val infix = e(inf)
- val (mp_set, mp_tree) = e(mp) match { case (FiniteSet(elems, valueType), t) => (elems, t) case _ => throw EvalError(typeErrorMsg(mp, SetType(ta))) }
-
- val res = mp_set.toList.map{ case v =>
- e(application(f, Seq(v))) match { case (sl@StringLiteral(s), t) => (s, sl, t)
- case _ => throw EvalError(typeErrorMsg(v, StringType)) } }
-
- mkString(res, infix)
-
- case FunctionInvocation(TypedFunDef(fd, Seq(ta)), Seq(mp, inf, f)) if fd == program.library.bagMkString.get =>
- val infix = e(inf)
- val (mp_bag, mp_tree) = e(mp) match { case (FiniteBag(elems, valueType), t) => (elems, t) case _ => throw EvalError(typeErrorMsg(mp, SetType(ta))) }
-
- val res = mp_bag.toList.flatMap{ case (k, v) =>
- val fk = (e(application(f, Seq(k))) match { case (sl@StringLiteral(s), t) => (s, sl, t) case _ => throw EvalError(typeErrorMsg(k, StringType)) })
- val times = (e(v)) match { case (InfiniteIntegerLiteral(i), t) => i case _ => throw EvalError(typeErrorMsg(k, IntegerType)) }
- List.fill(times.toString.toInt)(fk)
- }
-
- mkString(res, infix)
-
- case FunctionInvocation(tfd, args) =>
- if (gctx.stepsLeft < 0) {
- throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
- }
- gctx.stepsLeft -= 1
- val evArgs = args map e
- val evArgsValues = evArgs.map(_._1)
- val evArgsOrigin = evArgs.map(_._2)
-
- // build a mapping for the function...
- val frame = rctx.withNewVars2((tfd.paramIds zip evArgs).toMap)
-
- val callResult = if ((evArgsValues forall ExprOps.isValue) && tfd.fd.annotations("extern") && ctx.classDir.isDefined) {
- (scalaEv.call(tfd, evArgsValues), functionInvocation(tfd.fd, evArgsOrigin))
- } else {
- if((!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) || tfd.body.exists(b => ExprOps.exists(e => e.isInstanceOf[Choose])(b))) {
- (functionInvocation(tfd.fd, evArgsValues), functionInvocation(tfd.fd, evArgsOrigin))
- } else {
- val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
- try {
- e(body)(frame, gctx)
- } catch {
- case e: RuntimeError =>
- (functionInvocation(tfd.fd, evArgsValues), functionInvocation(tfd.fd, evArgsOrigin))
- }
- }
- }
- callResult
-
- case Let(i, ex, b) =>
- val (first, second) = e(ex)
- e(b)(rctx.withNewVar(i, (first, second)), gctx)
-
- case Application(caller, args) =>
- val (ecaller, tcaller) = e(caller)
- val nargs = args map e
- val (eargs, targs) = nargs.unzip
- ecaller match {
- case l @ Lambda(params, body) if evaluateApplications =>
- val mapping = (params map (_.id) zip nargs).toMap
- e(body)(rctx.withNewVars2(mapping), gctx)
- case _ =>
- val abs_value = Application(tcaller, targs)
- if (ExprOps.isValue(ecaller) && (eargs forall ExprOps.isValue)) {
- (underlying.e(Application(ecaller, eargs)), abs_value)
- } else {
- (Application(ecaller, eargs), abs_value)
- }
- }
-
- case l @ Lambda(_, _) =>
- import ExprOps._
- val mapping = variablesOf(l).map(id => id -> e(Variable(id))).toMap
- (
- replaceFromIDs(mapping.mapValues(_._1), l).asInstanceOf[Lambda],
- replaceFromIDs(mapping.mapValues(_._2), l).asInstanceOf[Lambda])
-
- case Operator(es, builder) =>
- val (ees, ts) = es.map(e).unzip
- if(ees forall ExprOps.isValue) {
- val conc_value = underlying.e(builder(ees))
- val abs_value = builder(ts)
- val final_abs_value = if( evaluateCaseClassSelector) {
- abs_value match {
- case CaseClassSelector(cct, CaseClass(ct, args), id) =>
- args(ct.classDef.selectorID2Index(id))
- case CaseClassSelector(cct, AsInstanceOf(CaseClass(ct, args), ccct), id) =>
- args(ct.classDef.selectorID2Index(id))
- case TupleSelect(Tuple(args), i) =>
- args(i-1)
- case e => e
- }
- } else abs_value
-
- (conc_value, final_abs_value)
- } else {
- val abs_value = builder(ees)
- val final_abs_value = if( evaluateCaseClassSelector) {
- abs_value match {
- case CaseClassSelector(cct, CaseClass(ct, args), id) =>
- args(ct.classDef.selectorID2Index(id))
- case CaseClassSelector(cct, AsInstanceOf(CaseClass(ct, args), ccct), id) =>
- args(ct.classDef.selectorID2Index(id))
- case TupleSelect(Tuple(args), i) =>
- args(i-1)
- case e => e
- }
- } else abs_value
-
- (final_abs_value, builder(ts))
- }
- }
- }
-
- def matchesCaseAbstract(scrut: Expr, abstractScrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Option[(MatchCase, Map[Identifier, (Expr, Expr)])] = {
- import purescala.TypeOps.isSubtypeOf
- import purescala.Extractors._
-
- def matchesPattern(pat: Pattern, expr: Expr, exprFromScrut: Expr): Option[Map[Identifier, (Expr, Expr)]] = (pat, expr) match {
- case (InstanceOfPattern(ob, pct), e) =>
- if (isSubtypeOf(e.getType, pct)) {
- Some(obind(ob, e, /*AsInstanceOf(*/exprFromScrut/*, pct)*/))
- } else {
- None
- }
- case (WildcardPattern(ob), e) =>
- Some(obind(ob, e, exprFromScrut))
-
- case (CaseClassPattern(ob, pct, subs), CaseClass(ct, args)) =>
- if (pct == ct) {
- val res = (subs zip args zip ct.classDef.fieldsIds).map{
- case ((s, a), id) =>
- exprFromScrut match {
- case CaseClass(ct, args) if evaluateCaseClassSelector =>
- matchesPattern(s, a, args(ct.classDef.selectorID2Index(id)))
- case AsInstanceOf(CaseClass(ct, args), _) if evaluateCaseClassSelector =>
- matchesPattern(s, a, args(ct.classDef.selectorID2Index(id)))
- case _ =>
- matchesPattern(s, a, CaseClassSelector(ct, exprFromScrut, id))
- }
- }
- if (res.forall(_.isDefined)) {
- Some(obind(ob, expr, exprFromScrut) ++ res.flatten.flatten)
- } else {
- None
- }
- } else {
- None
- }
- case (up @ UnapplyPattern(ob, _, subs), scrut) =>
- e(functionInvocation(up.unapplyFun.fd, Seq(scrut))) match {
- case (CaseClass(CaseClassType(cd, _), Seq()), eBuilt) if cd == program.library.None.get =>
- None
- case (CaseClass(CaseClassType(cd, _), Seq(arg)), eBuilt) if cd == program.library.Some.get =>
- val res = (subs zip unwrapTuple(arg, subs.size)).zipWithIndex map {
- case ((s, a), i) => matchesPattern(s, a, tupleSelect(eBuilt, i + 1, subs.size))
- }
- if (res.forall(_.isDefined)) {
- Some(obind(ob, expr, eBuilt) ++ res.flatten.flatten)
- } else {
- None
- }
- case other =>
- throw EvalError(typeErrorMsg(other._1, up.unapplyFun.returnType))
- }
- case (TuplePattern(ob, subs), Tuple(args)) =>
- if (subs.size == args.size) {
- val res = (subs zip args).zipWithIndex.map{
- case ((s, a), i) =>
- exprFromScrut match {
- case Tuple(args) if evaluateCaseClassSelector=>
- matchesPattern(s, a, args(i))
- case _ =>
- matchesPattern(s, a, TupleSelect(exprFromScrut, i+1))
- }
- }
- if (res.forall(_.isDefined)) {
- Some(obind(ob, expr, exprFromScrut) ++ res.flatten.flatten)
- } else {
- None
- }
- } else {
- None
- }
- case (LiteralPattern(ob, l1) , l2 : Literal[_]) if l1 == l2 =>
- Some(obind(ob, l1, exprFromScrut))
- case _ => None
- }
-
- def obind(ob: Option[Identifier], e: Expr, eBuilder: Expr): Map[Identifier, (Expr, Expr)] = {
- Map[Identifier, (Expr, Expr)]() ++ ob.map(id => id -> ((e, eBuilder)))
- }
-
- caze match {
- case SimpleCase(p, rhs) =>
- matchesPattern(p, scrut, abstractScrut).map(r =>
- (caze, r)
- )
-
- case GuardedCase(p, g, rhs) =>
- for {
- r <- matchesPattern(p, scrut, abstractScrut)
- if e(g)(rctx.withNewVars2(r), gctx)._1 == BooleanLiteral(true)
- } yield (caze, r)
- }
- }
-}
diff --git a/src/main/scala/inox/evaluators/AbstractOnlyEvaluator.scala b/src/main/scala/inox/evaluators/AbstractOnlyEvaluator.scala
deleted file mode 100644
index 589213264..000000000
--- a/src/main/scala/inox/evaluators/AbstractOnlyEvaluator.scala
+++ /dev/null
@@ -1,275 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import purescala.Extractors.Operator
-import purescala.Constructors._
-import purescala.Expressions._
-import purescala.Types._
-import purescala.Common.Identifier
-import purescala.Definitions.{TypedFunDef, Program}
-import purescala.DefOps
-import purescala.TypeOps
-import purescala.ExprOps
-import purescala.Expressions.Expr
-import leon.utils.DebugSectionSynthesis
-
-case class AbstractOnlyRecContext(concMapping: DefaultRecContext, mappingsAbstractOnly: Map[Identifier, Expr]) extends RecContext[AbstractOnlyRecContext] {
- def newVars(news: Map[Identifier, Expr], newsAbstractOnly: Map[Identifier, Expr]): AbstractOnlyRecContext = copy(concMapping.newVars(news), newsAbstractOnly)
- def newVars(news: Map[Identifier, Expr]): AbstractOnlyRecContext = copy(concMapping.newVars(news), news)
- def mappings = concMapping.mappings
-
- def withNewVar(id: Identifier, v: Expr, vAbs: Expr): AbstractOnlyRecContext = {
- newVars(mappings + (id -> v), mappingsAbstractOnly + (id -> vAbs))
- }
-
- /*def withNewVars2(news: Map[Identifier, (Expr, Expr)]): AbstractOnlyRecContext = {
- newVars(mappings ++ news.mapValues(_._1), mappingsAbstractOnly ++ news.mapValues(_._2))
- }*/
-
- def withNewVars3(news: Map[Identifier, Expr], newsAbstract: Map[Identifier, Expr]): AbstractOnlyRecContext = {
- newVars(concMapping.mappings ++ news, mappingsAbstractOnly ++ newsAbstract)
- }
-
- override def withNewVar(id: Identifier, v: Expr): AbstractOnlyRecContext = {
- newVars(mappings + (id -> v), mappingsAbstractOnly + (id -> v))
- }
-
- override def withNewVars(news: Map[Identifier, Expr]): AbstractOnlyRecContext = {
- newVars(mappings ++ news, mappingsAbstractOnly ++ news)
- }
-}
-
-
-trait HasAbstractOnlyRecContext extends ContextualEvaluator {
- type RC = AbstractOnlyRecContext
- def initRC(mappings: Map[Identifier, Expr]) = AbstractOnlyRecContext(DefaultRecContext(mappings), mappings)
-}
-
-/** The evaluation returns only the abstract value compared to the other implementation of [[leon.evaluators.AbstractEvaluator AbstractEvaluator]]
- * It also supposes that everything can be computed else (i.e. not possible to add non-bound variables)
- * @returns the way the expression has been evaluated. */
-class AbstractOnlyEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 150000) extends ContextualEvaluator(ctx, prog, maxSteps) with HasDefaultGlobalContext with HasAbstractOnlyRecContext {
- /** Evaluates resuts which can be evaluated directly
- * For example, concatenation of two string literals */
- val underlying = new RecursiveEvaluator(ctx, prog, new EvaluationBank, maxSteps)
- with HasDefaultGlobalContext
- with HasDefaultRecContext
- underlying.setEvaluationFailOnChoose(true)
- override type Value = Expr
-
- override val description: String = "Evaluates string programs but keeps the formula which generated the value"
- override val name: String = "AbstractOnly evaluator"
-
- /** True if CaseClassSelector(...CaseClass(...)) have to be simplified. */
- var evaluateCaseClassSelector = true
- /** True if Application(Lambda(), ...) have to be simplified. */
- var evaluateApplications = true
-
- implicit def aToC(implicit rctx: RC): AbstractOnlyEvaluator.this.underlying.RC = rctx.concMapping
-
- protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = {
- expr match {
- case Variable(id) =>
- rctx.mappingsAbstractOnly.get(id) match {
- case Some(va) =>
- (va)
- case _ =>
- expr
- }
-
- case e : Literal[_] =>
- e
-
- case IfExpr(cond, thenn, elze) =>
- val first = underlying.e(cond)
- first match {
- case BooleanLiteral(true) =>
- ctx.reporter.ifDebug(printer => printer(thenn))(DebugSectionSynthesis)
- e(thenn)
- case BooleanLiteral(false) => e(elze)
- case _ => throw EvalError(typeErrorMsg(first, BooleanType))
- }
-
- case MatchExpr(scrut, cases) =>
- val escrut = underlying.e(scrut)
- val tscrut = e(scrut)
- cases.toStream.map(c => matchesCaseAbstractOnly(escrut, tscrut, c)).find(_.nonEmpty) match {
- case Some(Some((c, mappings))) => e(c.rhs)(rctx.withNewVars3(mappings.map(v => v._1 -> underlying.e(v._2)).toMap, mappings.toMap), gctx)
- case _ => throw RuntimeError("MatchError(AbstractOnly evaluation): "+escrut.asString+" did not match any of the cases :\n" + cases.mkString("\n"))
- }
-
- case FunctionInvocation(tfd, args) =>
- if (gctx.stepsLeft < 0) {
- throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
- }
- gctx.stepsLeft -= 1
-
- val evArgsValues = args map (underlying.e)
- val evArgsOrigin = args map e
-
- // build a mapping for the function...
- //val frame = rctx.withNewVars2((tfd.paramIds zip evArgs).toMap)
-
- val callResult = if (tfd.fd.annotations("extern") && ctx.classDir.isDefined) {
- functionInvocation(tfd.fd, evArgsOrigin)
- } else {
- if((!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) || tfd.body.exists(b => ExprOps.exists(e => e.isInstanceOf[Choose])(b))) {
- functionInvocation(tfd.fd, evArgsOrigin)
- } else {
- val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
- try {
- val frame = rctx.withNewVars3((tfd.paramIds zip evArgsValues).toMap, (tfd.paramIds zip evArgsOrigin).toMap)
- e(body)(frame, gctx)
- } catch {
- case e: Throwable =>
- //println("Error during execution of " + expr + ": " + e + ", " + e.getMessage)
- //println(e.getStackTrace.map(_.toString).mkString("\n"))
- functionInvocation(tfd.fd, evArgsOrigin)
- }
- }
- }
- callResult
-
- case Let(i, ex, b) =>
- val first = underlying.e(ex)
- val second = e(ex)
- e(b)(rctx.withNewVar(i, first, second), gctx)
-
- case Application(caller, args) =>
- val ecaller = underlying.e(caller)
- val tcaller = e(caller)
- val targs = args map e
- val eargs = args map underlying.e
- ecaller match {
- case l @ Lambda(params, body) if evaluateApplications =>
- val mapping = (params map (_.id) zip eargs).toMap
- val mappingAbs = (params map (_.id) zip targs).toMap
- e(body)(rctx.withNewVars3(mapping, mappingAbs), gctx)
- case _ =>
- Application(tcaller, targs)
- }
-
- case l @ Lambda(_, _) =>
- import ExprOps._
- val mapping = variablesOf(l).map(id => id -> e(Variable(id))).toMap
- replaceFromIDs(mapping, l).asInstanceOf[Lambda]
-
- case Operator(es, builder) =>
- val ees = es.map(underlying.e)
- val ts = es.map(e)
- val conc_value = underlying.e(builder(ees))
- val abs_value = builder(ts)
- val final_abs_value = if( evaluateCaseClassSelector) {
- abs_value match {
- case CaseClassSelector(cct, CaseClass(ct, args), id) =>
- args(ct.classDef.selectorID2Index(id))
- case CaseClassSelector(cct, AsInstanceOf(CaseClass(ct, args), ccct), id) =>
- args(ct.classDef.selectorID2Index(id))
- case TupleSelect(Tuple(args), i) =>
- args(i-1)
- case Assert(a, error, body) => body
- case MapApply(FiniteMap(theMap, keyType, valueType), thekey) if theMap contains thekey =>
- theMap(thekey)
- case e => e
- }
- } else abs_value
-
- final_abs_value
- }
- }
-
- def matchesCaseAbstractOnly(scrut: Expr, abstractScrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Option[(MatchCase, Iterable[(Identifier, Expr)])] = {
- import purescala.TypeOps.isSubtypeOf
- import purescala.Extractors._
-
- def matchesPattern(pat: Pattern, expr: Expr, exprFromScrut: Expr): Option[Iterable[(Identifier, Expr)]] = (pat, expr) match {
- case (InstanceOfPattern(ob, pct), _) =>
- if (isSubtypeOf(exprFromScrut.getType, pct)) {
- Some(obind(ob, exprFromScrut/*AsInstanceOf(exprFromScrut, pct)*/)) // is AsInstanceOf needed?
- } else {
- None
- }
- case (WildcardPattern(ob), _) =>
- Some(obind(ob, exprFromScrut))
-
- case (CaseClassPattern(ob, pct, subs), CaseClass(ct, args)) =>
- if (pct == ct) {
- val res = (subs zip args zip ct.classDef.fieldsIds).map{
- case ((s, a), id) =>
- exprFromScrut match {
- case CaseClass(ct, args) if evaluateCaseClassSelector =>
- matchesPattern(s, a, args(ct.classDef.selectorID2Index(id)))
- case AsInstanceOf(CaseClass(ct, args), _) if evaluateCaseClassSelector =>
- matchesPattern(s, a, args(ct.classDef.selectorID2Index(id)))
- case _ =>
- matchesPattern(s, a, CaseClassSelector(ct, exprFromScrut, id))
- }
- }
- if (res.forall(_.isDefined)) {
- Some(obind(ob, exprFromScrut) ++ res.flatten.flatten)
- } else {
- None
- }
- } else {
- None
- }
- case (up @ UnapplyPattern(ob, _, subs), scrut) =>
- underlying.e(functionInvocation(up.unapplyFun.fd, Seq(scrut))) match {
- case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.None.get =>
- None
- case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Some.get =>
- val res = (subs zip unwrapTuple(arg, subs.size)).zipWithIndex map {
- case ((s, a), i) => matchesPattern(s, a, tupleSelect(arg, i + 1, subs.size))
- }
- if (res.forall(_.isDefined)) {
- Some(obind(ob, scrut) ++ res.flatten.flatten)
- } else {
- None
- }
- case other =>
- throw EvalError(typeErrorMsg(other, up.unapplyFun.returnType))
- }
- case (TuplePattern(ob, subs), Tuple(args)) =>
- if (subs.size == args.size) {
- val res = (subs zip args).zipWithIndex.map{
- case ((s, a), i) =>
- exprFromScrut match {
- case Tuple(args) if evaluateCaseClassSelector=>
- matchesPattern(s, a, args(i))
- case _ =>
- matchesPattern(s, a, TupleSelect(exprFromScrut, i+1))
- }
- }
- if (res.forall(_.isDefined)) {
- Some(obind(ob, exprFromScrut) ++ res.flatten.flatten)
- } else {
- None
- }
- } else {
- None
- }
- case (LiteralPattern(ob, l1) , l2 : Literal[_]) if l1 == l2 =>
- Some(obind(ob, exprFromScrut))
- case _ => None
- }
-
- def obind(ob: Option[Identifier], eBuilder: Expr): Iterable[(Identifier, Expr)] = {
- ob.map(id => id -> (eBuilder)).toList
- }
-
- caze match {
- case SimpleCase(p, rhs) =>
- matchesPattern(p, scrut, abstractScrut).map(r =>
- (caze, r)
- )
-
- case GuardedCase(p, g, rhs) =>
- for {
- r <- matchesPattern(p, scrut, abstractScrut)
- if underlying.e(g)(rctx.concMapping.withNewVars(r.map(kv => kv._1 -> underlying.e(kv._2)).toMap), gctx) == BooleanLiteral(true)
- } yield (caze, r)
- }
- }
-}
diff --git a/src/main/scala/inox/evaluators/AngelicEvaluator.scala b/src/main/scala/inox/evaluators/AngelicEvaluator.scala
deleted file mode 100644
index 26db1865b..000000000
--- a/src/main/scala/inox/evaluators/AngelicEvaluator.scala
+++ /dev/null
@@ -1,46 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import leon.solvers.Model
-import purescala.Expressions.Expr
-import EvaluationResults._
-
-class AngelicEvaluator(underlying: NDEvaluator)
- extends Evaluator(underlying.context, underlying.program)
- with DeterministicEvaluator {
-
- val description: String = "angelic evaluator"
- val name: String = "Interpreter that returns the first solution of a non-deterministic program"
-
- val bank = new EvaluationBank
-
- def eval(expr: Expr, model: Model): EvaluationResult = underlying.eval(expr, model) match {
- case Successful(Stream(h, _*)) =>
- Successful(h)
- case Successful(Stream()) =>
- RuntimeError("Underlying ND-evaluator returned no solution")
- case other@(RuntimeError(_) | EvaluatorError(_)) =>
- other.asInstanceOf[Result[Nothing]]
- }
-}
-
-class DemonicEvaluator(underlying: NDEvaluator)
- extends Evaluator(underlying.context, underlying.program)
- with DeterministicEvaluator {
-
- val description: String = "demonic evaluator"
- val name: String = "Interpreter that demands an underlying non-deterministic program has unique solution"
-
- val bank = new EvaluationBank
-
- def eval(expr: Expr, model: Model): EvaluationResult = underlying.eval(expr, model) match {
- case Successful(Stream(h)) =>
- Successful(h)
- case Successful(_) =>
- RuntimeError("Underlying ND-evaluator did not return unique solution!")
- case other@(RuntimeError(_) | EvaluatorError(_)) =>
- other.asInstanceOf[Result[Nothing]]
- }
-}
diff --git a/src/main/scala/inox/evaluators/CodeGenEvaluator.scala b/src/main/scala/inox/evaluators/CodeGenEvaluator.scala
deleted file mode 100644
index 74df09bad..000000000
--- a/src/main/scala/inox/evaluators/CodeGenEvaluator.scala
+++ /dev/null
@@ -1,78 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-
-import codegen.CompilationUnit
-import codegen.CompiledExpression
-import codegen.CodeGenParams
-
-import leon.codegen.runtime.LeonCodeGenRuntimeException
-import leon.codegen.runtime.LeonCodeGenEvaluationException
-
-class CodeGenEvaluator(ctx: LeonContext, val unit: CompilationUnit) extends Evaluator(ctx, unit.program) with DeterministicEvaluator {
-
- val name = "codegen-eval"
- val description = "Evaluator for PureScala expressions based on compilation to JVM"
-
- val bank = unit.bank
-
- /** Another constructor to make it look more like other `Evaluator`s. */
- def this(ctx: LeonContext, prog: Program, bank: EvaluationBank = new EvaluationBank, params: CodeGenParams = CodeGenParams.default) {
- this(ctx, new CompilationUnit(ctx, prog, bank, params))
- }
-
- private def compileExpr(expression: Expr, args: Seq[Identifier]): Option[CompiledExpression] = {
- ctx.timers.evaluators.codegen.compilation.start()
- try {
- Some(unit.compileExpression(expression, args)(ctx))
- } catch {
- case t: Throwable =>
- ctx.reporter.warning(expression.getPos, "Error while compiling expression: "+t.getMessage)
- None
- } finally {
- ctx.timers.evaluators.codegen.compilation.stop()
- }
- }
-
- def eval(expression: Expr, model: solvers.Model) : EvaluationResult = {
- compile(expression, model.toSeq.map(_._1)).map { e =>
- ctx.timers.evaluators.codegen.runtime.start()
- val res = e(model)
- ctx.timers.evaluators.codegen.runtime.stop()
- res
- }.getOrElse(EvaluationResults.EvaluatorError("Couldn't compile expression."))
- }
-
- override def compile(expression: Expr, args: Seq[Identifier]) : Option[solvers.Model=>EvaluationResult] = {
- compileExpr(expression, args).map(ce => (model: solvers.Model) => {
- if (args.exists(arg => !model.isDefinedAt(arg))) {
- EvaluationResults.EvaluatorError("Model undefined for free arguments")
- } else try {
- EvaluationResults.Successful(ce.eval(model))
- } catch {
- case e : ArithmeticException =>
- EvaluationResults.RuntimeError(e.getMessage)
-
- case e : ArrayIndexOutOfBoundsException =>
- EvaluationResults.RuntimeError(e.getMessage)
-
- case e : LeonCodeGenRuntimeException =>
- EvaluationResults.RuntimeError(e.getMessage)
-
- case e : LeonCodeGenEvaluationException =>
- EvaluationResults.EvaluatorError(e.getMessage)
-
- case e : java.lang.ExceptionInInitializerError =>
- EvaluationResults.RuntimeError(e.getException.getMessage)
-
- case so : java.lang.StackOverflowError =>
- EvaluationResults.RuntimeError("Stack overflow")
- }
- })
- }
- }
diff --git a/src/main/scala/inox/evaluators/DualEvaluator.scala b/src/main/scala/inox/evaluators/DualEvaluator.scala
deleted file mode 100644
index a99f4d477..000000000
--- a/src/main/scala/inox/evaluators/DualEvaluator.scala
+++ /dev/null
@@ -1,138 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Definitions._
-import purescala.Types._
-
-import codegen._
-import codegen.runtime.{StdMonitor, Monitor}
-
-class DualEvaluator(
- ctx: LeonContext,
- prog: Program,
- bank: EvaluationBank = new EvaluationBank,
- params: CodeGenParams = CodeGenParams.default
-) extends RecursiveEvaluator(ctx, prog, params.maxFunctionInvocations)
- with HasDefaultGlobalContext {
-
- type RC = DualRecContext
- def initRC(mappings: Map[Identifier, Expr]): RC = DualRecContext(mappings)
- implicit val debugSection = utils.DebugSectionEvaluation
-
- val unit = new CompilationUnit(ctx, prog, bank, params)
-
- var monitor: Monitor = new StdMonitor(unit, params.maxFunctionInvocations, Map())
-
- val isCompiled = prog.definedFunctions.toSet
-
- case class DualRecContext(mappings: Map[Identifier, Expr], needJVMRef: Boolean = false) extends RecContext[DualRecContext] {
- def newVars(news: Map[Identifier, Expr]) = copy(news)
- }
-
- case class RawObject(o: AnyRef, tpe: TypeTree) extends Expr {
- val getType = tpe
- }
-
- def call(tfd: TypedFunDef, args: Seq[AnyRef]): Expr = {
-
- val (className, methodName, _) = unit.leonFunDefToJVMInfo(tfd.fd).get
-
- val allArgs = Seq(monitor) ++
- (if (tfd.fd.tparams.nonEmpty) Seq(tfd.tps.map(unit.registerType(_)).toArray) else Seq()) ++
- args
-
- ctx.reporter.debug(s"Calling $className.$methodName(${args.mkString(",")})")
-
- try {
- val cl = unit.loader.loadClass(className)
-
- val meth = cl.getMethods.find(_.getName == methodName).get
-
- val res = if (allArgs.isEmpty) {
- meth.invoke(null)
- } else {
- meth.invoke(null, allArgs : _*)
- }
-
- RawObject(res, tfd.returnType)
- } catch {
- case e: java.lang.reflect.InvocationTargetException =>
- throw new RuntimeError(e.getCause.getMessage)
-
- case t: Throwable =>
- t.printStackTrace()
- throw new EvalError(t.getMessage)
- }
- }
-
- def retrieveField(fd : FunDef): Expr = {
-
- val (className, fieldName, _) = unit.leonFunDefToJVMInfo(fd).get
-
- ctx.reporter.debug(s"Retrieving $className.$fieldName")
-
- try {
- val cl = unit.loader.loadClass(className)
-
- val field = cl.getFields.find(_.getName == fieldName).get
-
- val res = field.get(null)
-
- RawObject(res, fd.returnType)
- } catch {
- case e: java.lang.reflect.InvocationTargetException =>
- throw new RuntimeError(e.getCause.getMessage)
-
- case t: Throwable =>
- t.printStackTrace()
- throw new EvalError(t.getMessage)
- }
- }
-
-
-
- override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
- case FunctionInvocation(tfd, args) =>
- if (isCompiled(tfd.fd)) {
- if (!tfd.fd.canBeStrictField) {
- val rargs = args.map(
- e(_)(rctx.copy(needJVMRef = true), gctx) match {
- case RawObject(obj, _) => obj
- case _ => throw new EvalError("Failed to get JVM ref when requested")
- }
- )
-
- jvmBarrier(call(tfd, rargs), rctx.needJVMRef)
- } else {
- jvmBarrier(retrieveField(tfd.fd), rctx.needJVMRef)
- }
- } else {
- jvmBarrier(super.e(expr)(rctx.copy(needJVMRef = false), gctx), rctx.needJVMRef)
- }
- case _ =>
- jvmBarrier(super.e(expr)(rctx.copy(needJVMRef = false), gctx), rctx.needJVMRef)
- }
-
- def jvmBarrier(e: Expr, returnJVMRef: Boolean): Expr = {
- e match {
- case RawObject(obj, _) if returnJVMRef =>
- e
- case RawObject(obj, _) if !returnJVMRef =>
- unit.jvmToValue(obj, e.getType)
- case e if returnJVMRef =>
- RawObject(unit.valueToJVM(e)(monitor), e.getType)
- case e if !returnJVMRef =>
- e
- }
- }
-
- override def eval(ex: Expr, model: solvers.Model) = {
- monitor = unit.getMonitor(model, params.maxFunctionInvocations)
- super.eval(ex, model)
- }
-
-}
diff --git a/src/main/scala/inox/evaluators/EvaluationPhase.scala b/src/main/scala/inox/evaluators/EvaluationPhase.scala
deleted file mode 100644
index a06d1b39a..000000000
--- a/src/main/scala/inox/evaluators/EvaluationPhase.scala
+++ /dev/null
@@ -1,55 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import leon.Main.MainComponent
-import purescala.Definitions._
-import purescala.DefOps._
-import purescala.Expressions._
-
-object EvaluationPhase extends UnitPhase[Program] {
- val name = "Evaluation"
- val description = "Evaluating ground functions"
-
- implicit val debugSection = utils.DebugSectionEvaluation
-
- def apply(ctx: LeonContext, program: Program): Unit = {
- val evalFuns: Option[Seq[String]] = ctx.findOption(GlobalOptions.optFunctions)
-
- val evaluator = ctx.findOptionOrDefault(MainComponent.optEval)
-
- val reporter = ctx.reporter
-
- val fdFilter = {
- import OptionsHelpers._
-
- filterInclusive(evalFuns.map(fdMatcher(program)), None)
- }
-
- val toEvaluate = funDefsFromMain(program).toList.filter(_.params.size == 0).filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
-
- if (toEvaluate.isEmpty) reporter.warning("No ground functions found with the given names")
-
- val eval = if (evaluator == "codegen") {
- new CodeGenEvaluator(ctx, program)
- } else if (evaluator == "default" || evaluator == "") {
- new DefaultEvaluator(ctx, program)
- } else {
- reporter.fatalError(s"Unknown evaluator '$evaluator'. Available: default, codegen")
- }
-
- for (fd <- toEvaluate) {
- reporter.info(s" - Evaluating ${fd.id}")
- val call = FunctionInvocation(fd.typed, Seq())
- eval.eval(call) match {
- case EvaluationResults.Successful(ex) =>
- reporter.info(s" => $ex")
- case EvaluationResults.RuntimeError(msg) =>
- reporter.warning(s" Runtime Error: $msg")
- case EvaluationResults.EvaluatorError(msg) =>
- reporter.warning(s" Evaluator Error: $msg")
- }
- }
- }
-}
diff --git a/src/main/scala/inox/evaluators/ScalacEvaluator.scala b/src/main/scala/inox/evaluators/ScalacEvaluator.scala
deleted file mode 100644
index db855fbcd..000000000
--- a/src/main/scala/inox/evaluators/ScalacEvaluator.scala
+++ /dev/null
@@ -1,459 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import leon.codegen.runtime.RuntimeResources
-
-import purescala.Definitions._
-import purescala.DefOps._
-import purescala.Expressions._
-import purescala.Types._
-
-import java.io.File
-import java.net.URLClassLoader
-import java.lang.reflect.Constructor
-
-/**
- * Call scalac-compiled functions from within Leon
- *
- * Known limitations:
- * - Multiple argument lists
- */
-class ScalacEvaluator(ev: DeterministicEvaluator, ctx: LeonContext, pgm: Program) extends LeonComponent {
- implicit val _: Program = pgm
-
- val name = "Evaluator of external functions"
- val description = "Evaluator for non-purescala functions"
-
- implicit val debugSection = utils.DebugSectionEvaluation
-
- val classPaths: List[File] = ctx.classDir.toList
-
- lazy val runtimeTok = {
- RuntimeResources.register(this)
- }
-
- private def unsupported(err: String): Nothing = {
- throw new RuntimeException(err)
- }
-
- private def encodeName(name: String): String = {
- scala.reflect.NameTransformer.encode(name)
- }
-
- private def jvmName(d: Definition): String = {
- compiledName(d).replace(".", "/")
- }
-
- private def jvmClassName(tpe: TypeTree): String = tpe match {
- case IntegerType =>
- "scala/math/BigInt"
-
- case TupleType(subs) =>
- f"scala/Tuple${subs.size}%d"
-
- case UnitType =>
- "scala/runtime/BoxedUnit"
-
- case ct: ClassType =>
- jvmName(ct.classDef)
-
- case _ =>
- ctx.reporter.internalError(s"$tpe is not a jvm class type ?!?")
- }
-
- private def compiledName(d: Definition): String = {
- // Scala encodes fullname of modules using ".". After the module, it
- // becomes an inner class, with '$'
- val path = pathFromRoot(d)
-
- val pathToModule = path.takeWhile{!_.isInstanceOf[ModuleDef]}
- val rest = path.drop(pathToModule.size)
-
- val upToModule = pathToNames(pathToModule, false).map(encodeName).mkString(".")
-
- if(rest.isEmpty) {
- upToModule
- } else {
- d match {
- case md: ModuleDef =>
- upToModule+"."+encodeName(md.id.name)+"$"
- case _ =>
- val afterModule = pathToNames(rest, false).map(encodeName).mkString("$")
- upToModule+"."+afterModule
- }
- }
- }
-
- def call(tfd: TypedFunDef, args: Seq[Expr]): Expr = {
- val fd = tfd.fd
-
- val methodName = encodeName(fd.id.name)
-
- val jvmArgs = args.map(leonToScalac)
-
- val (clazz, jvmRec, jvmCallArgs) = fd.methodOwner match {
- case Some(cd) =>
- (cd, jvmArgs.head, jvmArgs.tail)
-
- case None =>
- val md = moduleOf(fd).get
-
- val jvmModule = loadClass(compiledName(md))
- val rec = jvmModule.getField("MODULE$").get(null)
-
- (md, rec, jvmArgs)
- }
-
- val jvmClassName = compiledName(clazz)
- val jvmClass = loadClass(jvmClassName)
-
- ctx.reporter.debug(s"Calling $jvmClassName.${tfd.signature}(${args.mkString(", ")})")
-
- // Lookup method in jvmClass
-
- jvmClass.getMethods().filter(_.getName() == methodName).toList match {
- case List(meth) =>
-
- val res = if (jvmCallArgs.isEmpty) {
- meth.invoke(jvmRec)
- } else {
- meth.invoke(jvmRec, jvmCallArgs: _*)
- }
-
- scalacToLeon(res, tfd.returnType)
-
- case Nil =>
- unsupported(s"Unable to lookup method")
-
- case ms =>
- unsupported(s"Ambiguous reference to method: ${ms.size} methods found with a matching name")
-
- }
- }
-
- val localClassLoader = {
- classOf[ScalacEvaluator].getClassLoader()
- }
-
- val toInstrument = {
- val fds = (for (fd <- pgm.definedFunctions if !fd.annotations("extern")) yield {
- encodeName(fd.id.name) -> fd
- }).toMap
-
- fds.groupBy { case (n, fd) =>
- compiledName(fd.methodOwner.getOrElse(moduleOf(fd).get))
- }
- }
-
- val compiledClassLoader = {
- val classUrls = ctx.classDir.map(_.toURI.toURL)
- val cl = new URLClassLoader(classUrls.toArray, localClassLoader)
- new InterceptingClassLoader(cl)
- }
-
- def loadClass(classname: String): Class[_] = {
- compiledClassLoader.loadClass(classname)
- }
-
- def leonToScalac(e: Expr): AnyRef = e match {
- case CharLiteral(v) =>
- new java.lang.Character(v)
-
- case IntLiteral(v) =>
- new java.lang.Integer(v)
-
- case InfiniteIntegerLiteral(v) =>
- v
-
- case BooleanLiteral(v) =>
- new java.lang.Boolean(v)
-
- case Tuple(exprs) =>
- val name = f"scala.Tuple${exprs.size}%d"
-
- val cl = localClassLoader.loadClass(name)
- val constr = cl.getConstructors().head.asInstanceOf[Constructor[AnyRef]]
-
- constr.newInstance(exprs.map(leonToScalac) : _*)
-
- case UnitLiteral() =>
- Unit.box(())
-
- case FiniteSet(exprs, tpe) =>
-
- val cl = compiledClassLoader.loadClass("leon.lang.Set")
- val constr = cl.getConstructors().head.asInstanceOf[Constructor[AnyRef]]
-
- constr.newInstance(Set(exprs.toSeq.map(leonToScalac) : _*))
-
- case FiniteMap(pairs, ktpe, vtpe) =>
-
- val cl = compiledClassLoader.loadClass("leon.lang.Map")
- val constr = cl.getConstructors().head.asInstanceOf[Constructor[AnyRef]]
-
- constr.newInstance(Map(
- pairs.map { case (k, v) =>
- leonToScalac(k) -> leonToScalac(v)
- }.toSeq : _*
- ))
-
- case CaseClass(cct, fields) =>
-
- val name = compiledName(cct.classDef)
-
- val cl = loadClass(name)
- val constr = cl.getConstructors().head.asInstanceOf[Constructor[AnyRef]]
- constr.newInstance(fields.map(leonToScalac) : _*)
-
-
- case Lambda(_, _) =>
- unsupported("It is not yet possible to pass a closure to an @extern function")
-
- case t: Terminal =>
- unsupported("Unhandled conversion to scala runtime: "+t)
-
- case _ =>
- unsupported("Trying to convert non-terminal: "+e)
- }
-
- def productToElems(p: Product, tps: Seq[TypeTree]): Seq[Expr] = {
- for ((t,i) <- tps.zipWithIndex) yield {
- scalacToLeon(p.productElement(i), t)
- }
- }
-
- def scalacToLeon(o: Any, t: TypeTree): Expr = t match {
- case BooleanType =>
- BooleanLiteral(o.asInstanceOf[Boolean].booleanValue)
- case Int32Type =>
- IntLiteral(o.asInstanceOf[Integer].intValue)
- case CharType =>
- CharLiteral(o.asInstanceOf[Character].charValue)
- case IntegerType =>
- InfiniteIntegerLiteral(o.asInstanceOf[BigInt])
- case UnitType =>
- UnitLiteral()
- case TupleType(tps) =>
- Tuple(productToElems(o.asInstanceOf[Product], tps))
- case cct: CaseClassType =>
- CaseClass(cct, productToElems(o.asInstanceOf[Product], cct.fieldsTypes))
-
- case act: AbstractClassType =>
- val className = o.getClass.getName
-
- act.knownCCDescendants.find(cct => compiledName(cct.classDef) == className) match {
- case Some(cct) =>
- scalacToLeon(o, cct)
-
- case None =>
- unsupported("Expected "+act+", got: "+className)
- }
-
- case SetType(b) =>
- val cl = compiledClassLoader.loadClass("leon.lang.Set")
-
- val s = cl.getMethod("theSet").invoke(o).asInstanceOf[Set[_]]
-
- FiniteSet(s.iterator.map(scalacToLeon(_, b)).toSet, b)
-
- case MapType(ktpe, vtpe) =>
-
- val cl = compiledClassLoader.loadClass("leon.lang.Map")
-
- val s = cl.getMethod("theMap").invoke(o).asInstanceOf[Map[_, _]]
-
- FiniteMap(s.iterator.map {
- case (k, v) => scalacToLeon(k, ktpe) -> scalacToLeon(v, vtpe)
- }.toMap, ktpe, vtpe)
-
- case FunctionType(_, _) =>
- unsupported("It is not possible to pass a closure from @extern back to leon")
-
- case _ =>
- unsupported("Unhandled conversion from scala runtime: "+t)
- }
-
- def jvmCallBack(cName: String, fName: String, args: Array[AnyRef]): AnyRef = {
- toInstrument.get(cName).flatMap(_.get(fName)) match {
- case Some(fd) =>
- val leonArgs = fd.params.map(_.getType).zip(args).map {
- case (tpe, arg) => scalacToLeon(arg, tpe)
- }
-
- val fi = FunctionInvocation(fd.typed, leonArgs)
- leonToScalac(ev.eval(fi).result.getOrElse {
- unsupported("Evaluation in Leon failed!")
- })
-
- case None =>
- unsupported("Unable to locate callback function "+cName+"."+fName)
- }
- }
-
- /**
- * Black magic here we come!
- */
- import org.objectweb.asm.ClassReader
- import org.objectweb.asm.ClassWriter
- import org.objectweb.asm.ClassVisitor
- import org.objectweb.asm.MethodVisitor
- import org.objectweb.asm.Opcodes
-
- class InterceptingClassLoader(p: ClassLoader) extends ClassLoader(p) {
- import java.io._
-
- var loaded = Set[String]()
-
- override def loadClass(name: String, resolve: Boolean): Class[_] = {
- if (loaded(name)) {
- super.loadClass(name, resolve)
- } else {
- loaded += name
-
- if (!(toInstrument contains name)) {
- super.loadClass(name, resolve)
- } else {
- val bs = new ByteArrayOutputStream()
- val is = getResourceAsStream(name.replace('.', '/') + ".class")
- val buf = new Array[Byte](512)
- var len = is.read(buf)
- while (len > 0) {
- bs.write(buf, 0, len)
- len = is.read(buf)
- }
-
- // Transform bytecode
- val cr = new ClassReader(bs.toByteArray())
- val cw = new ClassWriter(cr, ClassWriter.COMPUTE_FRAMES)
- val cv = new LeonCallsClassVisitor(cw, name, toInstrument(name))
- cr.accept(cv, 0)
-
- val res = cw.toByteArray()
-
- defineClass(name, res, 0, res.length)
- }
- }
- }
- }
-
- class LeonCallsClassVisitor(cv: ClassVisitor, cName: String, fdMap: Map[String, FunDef]) extends ClassVisitor(Opcodes.ASM5, cv) {
- override def visitMethod(access: Int, fName: String, desc: String, sig: String, exceptions: Array[String]) = {
- val mv = super.visitMethod(access, fName, desc, sig, exceptions)
- if ((fdMap contains fName)) {
- new LeonCallsMethodVisitor(mv, cName, fName, fdMap(fName))
- } else {
- mv
- }
- }
- }
-
- class LeonCallsMethodVisitor(mv: MethodVisitor, cName: String, fName: String, fd: FunDef) extends MethodVisitor(Opcodes.ASM5, mv) {
-
- def box(tpe: TypeTree) = tpe match {
- case Int32Type =>
- mv.visitTypeInsn(Opcodes.NEW, "java/lang/Integer")
- mv.visitInsn(Opcodes.DUP_X1)
- mv.visitInsn(Opcodes.SWAP)
- mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Integer", "<init>", "(I)V", false)
-
- case CharType =>
- mv.visitTypeInsn(Opcodes.NEW, "java/lang/Character")
- mv.visitInsn(Opcodes.DUP_X1)
- mv.visitInsn(Opcodes.SWAP)
- mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Character", "<init>", "(C)V", false)
-
- case BooleanType =>
- mv.visitTypeInsn(Opcodes.NEW, "java/lang/Boolean")
- mv.visitInsn(Opcodes.DUP_X1)
- mv.visitInsn(Opcodes.SWAP)
- mv.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Boolean", "<init>", "(Z)V", false)
-
- case _ =>
- }
-
- def unbox(tpe: TypeTree) = tpe match {
- case Int32Type =>
- mv.visitTypeInsn(Opcodes.CHECKCAST, "java/lang/Integer")
- mv.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/lang/Integer", "intValue", "()I", false)
-
- case CharType =>
- mv.visitTypeInsn(Opcodes.CHECKCAST, "java/lang/Character")
- mv.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/lang/Character", "charValue", "()C", false)
-
- case BooleanType =>
- mv.visitTypeInsn(Opcodes.CHECKCAST, "java/lang/Boolean")
- mv.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/lang/Boolean", "booleanValue", "()Z", false)
-
- case tpe =>
- mv.visitTypeInsn(Opcodes.CHECKCAST, jvmClassName(tpe))
- }
-
- def loadOpCode(tpe: TypeTree) = tpe match {
- case CharType => Opcodes.ILOAD
- case Int32Type => Opcodes.ILOAD
- case BooleanType => Opcodes.ILOAD
- case _ => Opcodes.ALOAD
- }
-
- def returnOpCode(tpe: TypeTree) = tpe match {
- case CharType => Opcodes.IRETURN
- case Int32Type => Opcodes.IRETURN
- case BooleanType => Opcodes.IRETURN
- case UnitType => Opcodes.RETURN
- case _ => Opcodes.ARETURN
- }
-
-
- override def visitCode() {
- mv.visitLdcInsn(runtimeTok.id)
- mv.visitLdcInsn(cName)
- mv.visitLdcInsn(fName)
-
- // If we are visiting a method, we need to add the receiver in the arguments array
- val readOffset = fd.methodOwner match {
- case Some(cd) =>
- // $this is the receiver
- 0
- case _ =>
- // We skip the module object
- 1
- }
-
- // Array of arguments called
- mv.visitLdcInsn(fd.params.size)
- mv.visitTypeInsn(Opcodes.ANEWARRAY, "java/lang/Object")
-
- // Note: fd.params includes the receiver!
- // Add actual arguments, box necessary values
- for ((tpe, i) <- fd.params.map(_.getType).zipWithIndex) {
- // Array ref
- mv.visitInsn(Opcodes.DUP)
- mv.visitLdcInsn(i)
- // Arg Value
- mv.visitVarInsn(loadOpCode(tpe), i+readOffset)
- box(tpe)
- mv.visitInsn(Opcodes.AASTORE)
- }
-
-
- mv.visitMethodInsn(Opcodes.INVOKESTATIC,
- "leon/evaluators/LeonJVMCallBacks",
- "callBack",
- "(ILjava/lang/String;Ljava/lang/String;[Ljava/lang/Object;)Ljava/lang/Object;",
- false)
-
- unbox(fd.returnType)
- mv.visitInsn(returnOpCode(fd.returnType))
- mv.visitEnd()
- }
- }
-}
-
-object LeonJVMCallBacks {
- def callBack(token: Int, className: String, methodName: String, args: Array[AnyRef]): AnyRef = {
- val ev = RuntimeResources.get[ScalacEvaluator](token)
- ev.jvmCallBack(className, methodName, args)
- }
-}
diff --git a/src/main/scala/inox/evaluators/StreamEvaluator.scala b/src/main/scala/inox/evaluators/StreamEvaluator.scala
deleted file mode 100644
index 8caf0c9f4..000000000
--- a/src/main/scala/inox/evaluators/StreamEvaluator.scala
+++ /dev/null
@@ -1,718 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import purescala.Constructors._
-import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.TypeOps.{leastUpperBound, isSubtypeOf}
-import purescala.Types._
-import purescala.Common.Identifier
-import purescala.Definitions.{TypedFunDef, Program}
-import purescala.Expressions._
-import purescala.Quantification._
-
-import leon.solvers.{SolverFactory, PartialModel}
-import leon.solvers.unrolling.UnrollingProcedure
-import leon.utils.StreamUtils._
-
-import scala.concurrent.duration._
-
-class StreamEvaluator(ctx: LeonContext, prog: Program)
- extends ContextualEvaluator(ctx, prog, 50000)
- with NDEvaluator
- with HasDefaultGlobalContext
- with HasDefaultRecContext
-{
-
- val name = "ND-evaluator"
- val description = "Non-deterministic interpreter for Leon programs that returns a Stream of solutions"
-
- protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Stream[Expr] = expr match {
- case Variable(id) =>
- rctx.mappings.get(id).toStream
-
- case Application(caller, args) =>
- for {
- cl <- e(caller).distinct
- newArgs <- cartesianProduct(args map e).distinct
- res <- cl match {
- case l @ Lambda(params, body) =>
- val mapping = l.paramSubst(newArgs)
- e(body)(rctx.withNewVars(mapping), gctx).distinct
- case FiniteLambda(mapping, dflt, _) =>
- // FIXME
- Stream(mapping.collectFirst {
- case (pargs, res) if (newArgs zip pargs).forall { case (f, r) => f == r } =>
- res
- }.getOrElse(dflt))
- case _ =>
- Stream()
- }
- } yield res
-
- case Let(i,v,b) =>
- for {
- ev <- e(v).distinct
- eb <- e(b)(rctx.withNewVar(i, ev), gctx).distinct
- } yield eb
-
- case Assert(cond, oerr, body) =>
- e(IfExpr(Not(cond), Error(expr.getType, oerr.getOrElse("Assertion failed @"+expr.getPos)), body))
-
- case en@Ensuring(body, post) =>
- e(en.toAssert)
-
- case Error(tpe, desc) =>
- Stream()
-
- case IfExpr(cond, thenn, elze) =>
- e(cond).distinct.flatMap {
- case BooleanLiteral(true) => e(thenn)
- case BooleanLiteral(false) => e(elze)
- case other => Stream()
- }.distinct
-
- case FunctionInvocation(TypedFunDef(fd, Seq(tp)), Seq(set)) if fd == program.library.setToList.get =>
- val cons = program.library.Cons.get
- val nil = CaseClass(CaseClassType(program.library.Nil.get, Seq(tp)), Seq())
- def mkCons(h: Expr, t: Expr) = CaseClass(CaseClassType(cons, Seq(tp)), Seq(h,t))
- e(set).distinct.collect {
- case FiniteSet(els, _) =>
- els.foldRight(nil)(mkCons)
- }.distinct
-
- case FunctionInvocation(tfd, args) =>
- if (gctx.stepsLeft < 0) {
- return Stream()
- }
- gctx.stepsLeft -= 1
-
- for {
- evArgs <- cartesianProduct(args map e).distinct
- // build a mapping for the function...
- frame = rctx.withNewVars(tfd.paramSubst(evArgs))
- BooleanLiteral(true) <- e(tfd.precOrTrue)(frame, gctx).distinct
- body <- tfd.body.orElse(rctx.mappings.get(tfd.id)).toStream
- callResult <- e(body)(frame, gctx).distinct
- BooleanLiteral(true) <- e(application(tfd.postOrTrue, Seq(callResult)))(frame, gctx).distinct
- } yield callResult
-
- case And(args) if args.isEmpty =>
- Stream(BooleanLiteral(true))
-
- case And(args) =>
- e(args.head).distinct.flatMap {
- case BooleanLiteral(false) => Stream(BooleanLiteral(false))
- case BooleanLiteral(true) => e(andJoin(args.tail))
- case other => Stream()
- }
-
- case Or(args) if args.isEmpty =>
- Stream(BooleanLiteral(false))
-
- case Or(args) =>
- e(args.head).distinct.flatMap {
- case BooleanLiteral(true) => Stream(BooleanLiteral(true))
- case BooleanLiteral(false) => e(orJoin(args.tail))
- case other => Stream()
- }
-
- case Implies(lhs, rhs) =>
- e(Or(Not(lhs), rhs))
-
- case l @ Lambda(_, _) =>
- val mapping = variablesOf(l).map(id =>
- id -> (e(Variable(id)) match {
- case Stream(v) => v
- case _ => return Stream()
- })
- ).toMap
- Stream(replaceFromIDs(mapping, l))
-
- case fl @ FiniteLambda(mapping, dflt, tpe) =>
- // finite lambda should always be ground!
- Stream(fl)
-
- case f @ Forall(fargs, body) =>
-
- // TODO add memoization
- implicit val debugSection = utils.DebugSectionVerification
-
- ctx.reporter.debug("Executing forall!")
-
- val mapping = variablesOf(f).map(id => id -> rctx.mappings(id)).toMap
- val context = mapping.toSeq.sortBy(_._1.uniqueName).map(_._2)
-
- val tStart = System.currentTimeMillis
-
- val newCtx = ctx.copy(options = ctx.options.map {
- case LeonOption(optDef, value) if optDef == UnrollingProcedure.optFeelingLucky =>
- LeonOption(optDef)(false)
- case opt => opt
- })
-
- val solverf = SolverFactory.getFromSettings(newCtx, program).withTimeout(1.second)
- val solver = solverf.getNewSolver()
-
- try {
- val cnstr = Not(replaceFromIDs(mapping, body))
- solver.assertCnstr(cnstr)
-
- gctx.model match {
- case pm: PartialModel =>
- val quantifiers = fargs.map(_.id).toSet
- val quorums = extractQuorums(body, quantifiers)
-
- val domainCnstr = orJoin(quorums.map { quorum =>
- val quantifierDomains = quorum.flatMap { case (path, caller, args) =>
- val optMatcher = e(caller) match {
- case Stream(l: Lambda) => Some(gctx.lambdas.getOrElse(l, l))
- case Stream(ev) => Some(ev)
- case _ => None
- }
-
- optMatcher.toSeq.flatMap { matcher =>
- val domain = pm.domains.get(matcher)
- args.zipWithIndex.flatMap {
- case (Variable(id),idx) if quantifiers(id) =>
- Some(id -> domain.map(cargs => path -> cargs(idx)))
- case _ => None
- }
- }
- }
-
- val domainMap = quantifierDomains.groupBy(_._1).mapValues(_.map(_._2).flatten)
- andJoin(domainMap.toSeq.map { case (id, dom) =>
- orJoin(dom.toSeq.map { case (path, value) =>
- // @nv: Note that equality is allowed here because of first-order quantifiers.
- // See [[leon.codegen.runtime.Monitor]] for more details.
- path and Equals(Variable(id), value)
- })
- })
- })
-
- solver.assertCnstr(domainCnstr)
-
- case _ =>
- }
-
- solver.check match {
- case Some(negRes) =>
- val total = System.currentTimeMillis-tStart
- val res = BooleanLiteral(!negRes)
- ctx.reporter.debug("Verification took "+total+"ms")
- ctx.reporter.debug("Finished forall evaluation with: "+res)
- Stream(res)
- case _ =>
- Stream()
- }
- } catch {
- case e: Throwable => Stream()
- } finally {
- solverf.reclaim(solver)
- solverf.shutdown()
- }
-
- case p : Passes =>
- e(p.asConstraint)
-
- case choose: Choose =>
-
- // TODO add memoization
- implicit val debugSection = utils.DebugSectionSynthesis
-
- val p = synthesis.Problem.fromSpec(choose.pred)
-
- ctx.reporter.debug("Executing choose!")
-
- val tStart = System.currentTimeMillis
-
- val newCtx = ctx.copy(options = ctx.options.map {
- case LeonOption(optDef, value) if optDef == UnrollingProcedure.optFeelingLucky =>
- LeonOption(optDef)(false)
- case opt => opt
- })
-
- val solverf = SolverFactory.getFromSettings(newCtx, program)
- val solver = solverf.getNewSolver()
-
- try {
- val eqs = p.as.map {
- case id => Equals(Variable(id), rctx.mappings(id))
- }
-
- val cnstr = p.pc withBindings p.as.map(id => id -> rctx.mappings(id)) and p.phi
- solver.assertCnstr(cnstr)
-
- def getSolution = try {
- solver.check match {
- case Some(true) =>
- val model = solver.getModel
-
- val valModel = valuateWithModel(model) _
-
- val res = p.xs.map(valModel)
- val leonRes = tupleWrap(res)
- val total = System.currentTimeMillis - tStart
-
- ctx.reporter.debug("Synthesis took " + total + "ms")
- ctx.reporter.debug("Finished synthesis with " + leonRes.asString)
-
- Some(leonRes)
- case _ =>
- None
- }
- } catch {
- case _: Throwable => None
- }
-
- Stream.iterate(getSolution)(prev => {
- val ensureDistinct = Not(Equals(tupleWrap(p.xs.map{ _.toVariable}), prev.get))
- solver.assertCnstr(ensureDistinct)
- val sol = getSolution
- // Clean up when the stream ends
- if (sol.isEmpty) {
- solverf.reclaim(solver)
- solverf.shutdown()
- }
- sol
- }).takeWhile(_.isDefined).take(10).map(_.get)
- // This take(10) is there because we are not working well with infinite streams yet...
- } catch {
- case e: Throwable =>
- solverf.reclaim(solver)
- solverf.shutdown()
- Stream()
- }
-
- case synthesis.utils.MutableExpr(ex) =>
- e(ex)
-
- case MatchExpr(scrut, cases) =>
-
- def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Stream[(MatchCase, Map[Identifier, Expr])] = {
- import purescala.TypeOps.isSubtypeOf
-
- def matchesPattern(pat: Pattern, expr: Expr): Stream[Map[Identifier, Expr]] = (pat, expr) match {
- case (InstanceOfPattern(ob, pct), e) =>
- (if (isSubtypeOf(e.getType, pct)) {
- Some(obind(ob, e))
- } else {
- None
- }).toStream
- case (WildcardPattern(ob), e) =>
- Stream(obind(ob, e))
-
- case (CaseClassPattern(ob, pct, subs), CaseClass(ct, args)) =>
- if (pct == ct) {
- val subMaps = (subs zip args).map{ case (s, a) => matchesPattern(s, a) }
- cartesianProduct(subMaps).map( _.flatten.toMap ++ obind(ob, expr))
- } else {
- Stream()
- }
- case (UnapplyPattern(ob, unapplyFun, subs), scrut) =>
- e(functionInvocation(unapplyFun.fd, Seq(scrut))) flatMap {
- case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.None.get =>
- None
- case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Some.get =>
- val subMaps = subs zip unwrapTuple(arg, subs.size) map {
- case (s,a) => matchesPattern(s,a)
- }
- cartesianProduct(subMaps).map( _.flatten.toMap ++ obind(ob, expr))
- case other =>
- None
- }
- case (TuplePattern(ob, subs), Tuple(args)) =>
- if (subs.size == args.size) {
- val subMaps = (subs zip args).map { case (s, a) => matchesPattern(s, a) }
- cartesianProduct(subMaps).map(_.flatten.toMap ++ obind(ob, expr))
- } else Stream()
- case (LiteralPattern(ob, l1) , l2 : Literal[_]) if l1 == l2 =>
- Stream(obind(ob,l1))
- case _ => Stream()
- }
-
- def obind(ob: Option[Identifier], e: Expr): Map[Identifier, Expr] = {
- Map[Identifier, Expr]() ++ ob.map(id => id -> e)
- }
-
- caze match {
- case SimpleCase(p, rhs) =>
- matchesPattern(p, scrut).map(r =>
- (caze, r)
- )
-
- case GuardedCase(p, g, rhs) =>
- for {
- r <- matchesPattern(p, scrut)
- BooleanLiteral(true) <- e(g)(rctx.withNewVars(r), gctx)
- } yield (caze, r)
- }
- }
-
- for {
- rscrut <- e(scrut)
- cs <- cases.toStream.map(c => matchesCase(rscrut, c)).find(_.nonEmpty).toStream
- (c, mp) <- cs
- res <- e(c.rhs)(rctx.withNewVars(mp), gctx)
- } yield res
-
- case Operator(es, _) =>
- cartesianProduct(es map e) flatMap { es =>
- try {
- Some(step(expr, es))
- } catch {
- case _: RuntimeError =>
- // EvalErrors stop the computation altogether
- None
- }
- }
-
- case other =>
- context.reporter.error(other.getPos, "Error: don't know how to handle " + other.asString + " in Evaluator ("+other.getClass+").")
- Stream()
- }
-
-
- protected def step(expr: Expr, subs: Seq[Expr])(implicit rctx: RC, gctx: GC): Expr = (expr, subs) match {
- case (Tuple(_), ts) =>
- Tuple(ts)
-
- case (TupleSelect(_, i), rs) =>
- rs(i - 1)
-
- case (Assert(_, oerr, _), Seq(BooleanLiteral(cond), body)) =>
- if (cond) body
- else throw RuntimeError(oerr.getOrElse("Assertion failed @" + expr.getPos))
-
- case (Error(_, desc), _) =>
- throw RuntimeError("Error reached in evaluation: " + desc)
-
- case (FunctionInvocation(TypedFunDef(fd, Seq(tp)), _), Seq(FiniteSet(els, _))) if fd == program.library.setToList.get =>
- val cons = program.library.Cons.get
- val nil = CaseClass(CaseClassType(program.library.Nil.get, Seq(tp)), Seq())
- def mkCons(h: Expr, t: Expr) = CaseClass(CaseClassType(cons, Seq(tp)), Seq(h, t))
- els.foldRight(nil)(mkCons)
-
- case (Not(_), Seq(BooleanLiteral(arg))) =>
- BooleanLiteral(!arg)
-
- case (Implies(_, _) Seq (BooleanLiteral(b1), BooleanLiteral(b2))) =>
- BooleanLiteral(!b1 || b2)
-
- case (Equals(_, _), Seq(lv, rv)) =>
- (lv, rv) match {
- case (FiniteSet(el1, _), FiniteSet(el2, _)) => BooleanLiteral(el1 == el2)
- case (FiniteBag(el1, _), FiniteBag(el2, _)) => BooleanLiteral(el1 == el2)
- case (FiniteMap(el1, _, _), FiniteMap(el2, _, _)) => BooleanLiteral(el1.toSet == el2.toSet)
- case (FiniteLambda(m1, d1, _), FiniteLambda(m2, d2, _)) => BooleanLiteral(m1.toSet == m2.toSet && d1 == d2)
- case _ => BooleanLiteral(lv == rv)
- }
-
- case (CaseClass(cd, _), args) =>
- CaseClass(cd, args)
-
- case (AsInstanceOf(_, ct), Seq(ce)) =>
- if (isSubtypeOf(ce.getType, ct)) {
- ce
- } else {
- throw RuntimeError("Cast error: cannot cast " + ce.asString + " to " + ct.asString)
- }
-
- case (IsInstanceOf(_, ct), Seq(ce)) =>
- BooleanLiteral(isSubtypeOf(ce.getType, ct))
-
- case (CaseClassSelector(ct1, _, sel), Seq(CaseClass(ct2, args))) if ct1 == ct2 =>
- args(ct1.classDef.selectorID2Index(sel))
-
- case (Plus(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
- InfiniteIntegerLiteral(i1 + i2)
-
- case (Minus(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
- InfiniteIntegerLiteral(i1 - i2)
-
- case (Times(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
- InfiniteIntegerLiteral(i1 * i2)
-
- case (Division(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
- if (i2 != BigInt(0)) InfiniteIntegerLiteral(i1 / i2)
- else throw RuntimeError("Division by 0.")
-
- case (Remainder(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
- if (i2 != BigInt(0)) InfiniteIntegerLiteral(i1 % i2)
- else throw RuntimeError("Remainder of division by 0.")
-
- case (Modulo(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
- if (i2 < 0)
- InfiniteIntegerLiteral(i1 mod (-i2))
- else if (i2 != BigInt(0))
- InfiniteIntegerLiteral(i1 mod i2)
- else
- throw RuntimeError("Modulo of division by 0.")
-
- case (UMinus(_), Seq(InfiniteIntegerLiteral(i))) =>
- InfiniteIntegerLiteral(-i)
-
- case (RealPlus(_, _), Seq(FractionalLiteral(ln, ld), FractionalLiteral(rn, rd))) =>
- normalizeFraction(FractionalLiteral(ln * rd + rn * ld, ld * rd))
-
- case (RealMinus(_, _), Seq(FractionalLiteral(ln, ld), FractionalLiteral(rn, rd))) =>
- normalizeFraction(FractionalLiteral(ln * rd - rn * ld, ld * rd))
-
- case (RealTimes(_, _), Seq(FractionalLiteral(ln, ld), FractionalLiteral(rn, rd))) =>
- normalizeFraction(FractionalLiteral(ln * rn, ld * rd))
-
- case (RealDivision(_, _), Seq(FractionalLiteral(ln, ld), FractionalLiteral(rn, rd))) =>
- if (rn != 0) normalizeFraction(FractionalLiteral(ln * rd, ld * rn))
- else throw RuntimeError("Division by 0.")
-
- case (BVPlus(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- IntLiteral(i1 + i2)
-
- case (BVMinus(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- IntLiteral(i1 - i2)
-
- case (BVUMinus(_), Seq(IntLiteral(i))) =>
- IntLiteral(-i)
-
- case (RealUMinus(_), Seq(FractionalLiteral(n, d))) =>
- FractionalLiteral(-n, d)
-
- case (BVNot(_), Seq(IntLiteral(i))) =>
- IntLiteral(~i)
-
- case (BVTimes(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- IntLiteral(i1 * i2)
-
- case (BVDivision(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- if (i2 != 0) IntLiteral(i1 / i2)
- else throw RuntimeError("Division by 0.")
-
- case (BVRemainder(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- if (i2 != 0) IntLiteral(i1 % i2)
- else throw RuntimeError("Remainder of division by 0.")
-
- case (BVAnd(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- IntLiteral(i1 & i2)
-
- case (BVOr(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- IntLiteral(i1 | i2)
-
- case (BVXOr(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- IntLiteral(i1 ^ i2)
-
- case (BVShiftLeft(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- IntLiteral(i1 << i2)
-
- case (BVAShiftRight(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- IntLiteral(i1 >> i2)
-
- case (BVLShiftRight(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
- IntLiteral(i1 >>> i2)
-
- case (LessThan(_, _), Seq(el, er)) =>
- (el, er) match {
- case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 < i2)
- case (a@FractionalLiteral(_, _), b@FractionalLiteral(_, _)) =>
- val FractionalLiteral(n, _) = e(RealMinus(a, b)).head
- BooleanLiteral(n < 0)
- case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 < c2)
- case (le, re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
- case (GreaterThan(_, _), Seq(el, er)) =>
- (el, er) match {
- case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 > i2)
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 > i2)
- case (a@FractionalLiteral(_, _), b@FractionalLiteral(_, _)) =>
- val FractionalLiteral(n, _) = e(RealMinus(a, b)).head
- BooleanLiteral(n > 0)
- case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 > c2)
- case (le, re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
- case (LessEquals(_, _), Seq(el, er)) =>
- (el, er) match {
- case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 <= i2)
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 <= i2)
- case (a@FractionalLiteral(_, _), b@FractionalLiteral(_, _)) =>
- val FractionalLiteral(n, _) = e(RealMinus(a, b)).head
- BooleanLiteral(n <= 0)
- case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 <= c2)
- case (le, re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
- case (GreaterEquals(_, _), Seq(el, er)) =>
- (el, er) match {
- case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 >= i2)
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 >= i2)
- case (a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) =>
- val FractionalLiteral(n, _) = e(RealMinus(a, b)).head
- BooleanLiteral(n >= 0)
- case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 >= c2)
- case (le, re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
- case (IsTyped(sa @ SetAdd(_, _), tpe), Seq(
- IsTyped(FiniteSet(els1, _), SetType(tpe1)),
- IsTyped(elem, tpe2)
- )) =>
- FiniteSet(
- els1 + elem,
- leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(sa, tpe)))
- )
-
- case (IsTyped(su @ SetUnion(s1, s2), tpe), Seq(
- IsTyped(FiniteSet(els1, _), SetType(tpe1)),
- IsTyped(FiniteSet(els2, _), SetType(tpe2))
- )) =>
- FiniteSet(
- els1 ++ els2,
- leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(su, tpe)))
- )
-
- case (IsTyped(su @ SetIntersection(s1, s2), tpe), Seq(
- IsTyped(FiniteSet(els1, _), SetType(tpe1)),
- IsTyped(FiniteSet(els2, _), SetType(tpe2))
- )) =>
- FiniteSet(
- els1 & els2,
- leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(su, tpe)))
- )
-
- case (IsTyped(su @ SetDifference(s1, s2), tpe), Seq(
- IsTyped(FiniteSet(els1, _), SetType(tpe1)),
- IsTyped(FiniteSet(els2, _), SetType(tpe2))
- )) =>
- FiniteSet(
- els1 -- els2,
- leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(su, tpe)))
- )
-
- case (ElementOfSet(_, _), Seq(e, FiniteSet(els, _))) =>
- BooleanLiteral(els.contains(e))
-
- case (SubsetOf(_, _), Seq(FiniteSet(els1, _), FiniteSet(els2, _))) =>
- BooleanLiteral(els1.subsetOf(els2))
-
- case (SetCardinality(_), Seq(FiniteSet(els, _))) =>
- IntLiteral(els.size)
-
- case (FiniteSet(_, base), els) =>
- FiniteSet(els.toSet, base)
-
- case (IsTyped(ba @ BagAdd(_, _), tpe), Seq(
- IsTyped(FiniteBag(els1, _), BagType(tpe1)),
- IsTyped(e, tpe2)
- )) =>
- FiniteBag(
- els1 + (e -> (els1.getOrElse(e, InfiniteIntegerLiteral(0)) match {
- case InfiniteIntegerLiteral(i) => InfiniteIntegerLiteral(i + 1)
- case il => throw EvalError(typeErrorMsg(il, IntegerType))
- })),
- leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(ba, tpe)))
- )
-
- case (IsTyped(bu @ BagUnion(b1, b2), tpe), Seq(
- IsTyped(FiniteBag(els1, _), BagType(tpe1)),
- IsTyped(FiniteBag(els2, _), BagType(tpe2))
- )) =>
- FiniteBag(
- (els1.keys ++ els2.keys).map(k => k -> {
- ((els1.getOrElse(k, InfiniteIntegerLiteral(0)), els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 + i2)
- case (l, r) => throw EvalError(typeErrorMsg(l, IntegerType))
- })
- }).toMap,
- leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(bu, tpe)))
- )
-
- case (IsTyped(bi @ BagIntersection(s1, s2), tpe), Seq(
- IsTyped(FiniteBag(els1, _), BagType(tpe1)),
- IsTyped(FiniteBag(els2, _), BagType(tpe2))
- )) =>
- FiniteBag(
- els1.flatMap { case (k, e) =>
- val res = (e, els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => i1 min i2
- case (l, r) => throw EvalError(typeErrorMsg(l, IntegerType))
- }
- if (res <= 0) None else Some(k -> InfiniteIntegerLiteral(res))
- },
- leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(bi, tpe)))
- )
-
- case (IsTyped(bd @ BagDifference(s1, s2), tpe), Seq(
- IsTyped(FiniteBag(els1, _), BagType(tpe1)),
- IsTyped(FiniteBag(els2, _), BagType(tpe2))
- )) =>
- FiniteBag(
- els1.flatMap { case (k, e) =>
- val res = (e, els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => i1 - i2
- case (l, r) => throw EvalError(typeErrorMsg(l, IntegerType))
- }
- if (res <= 0) None else Some(k -> InfiniteIntegerLiteral(res))
- },
- leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(bd, tpe)))
- )
-
- case (MultiplicityInBag(_, _), Seq(e, FiniteBag(els, _))) =>
- els.getOrElse(e, InfiniteIntegerLiteral(0))
-
- case (fb @ FiniteBag(_, _), els) =>
- val Operator(_, builder) = fb
- builder(els)
-
- case (ArrayLength(_), Seq(FiniteArray(_, _, IntLiteral(length)))) =>
- IntLiteral(length)
-
- case (ArrayUpdated(_, _, _), Seq(
- IsTyped(FiniteArray(elems, default, length), ArrayType(tp)),
- IntLiteral(i),
- v
- )) =>
- finiteArray(elems.updated(i, v), default map {(_, length)}, tp)
-
- case (ArraySelect(_, _), Seq(fa@FiniteArray(elems, default, IntLiteral(length)), IntLiteral(index))) =>
- elems
- .get(index)
- .orElse(if (index >= 0 && index < length) default else None)
- .getOrElse(throw RuntimeError(s"Array out of bounds error during evaluation:\n array = $fa, index = $index"))
-
- case (fa @ FiniteArray(_, _, _), subs) =>
- val Operator(_, builder) = fa
- builder(subs)
-
- case (fm @ FiniteMap(_, _, _), subs) =>
- val Operator(_, builder) = fm
- builder(subs)
-
- case (g @ MapApply(_, _), Seq(FiniteMap(m, _, _), k)) =>
- m.getOrElse(k, throw RuntimeError("Key not found: " + k.asString))
-
- case (u@IsTyped(MapUnion(_, _), MapType(kT, vT)), Seq(FiniteMap(m1, _, _), FiniteMap(m2, _, _))) =>
- FiniteMap(m1 ++ m2, kT, vT)
-
- case (i@MapIsDefinedAt(_, _), Seq(FiniteMap(elems, _, _), k)) =>
- BooleanLiteral(elems.contains(k))
-
- case (gv: GenericValue, Seq()) =>
- gv
-
- case (fl: FractionalLiteral, Seq()) =>
- normalizeFraction(fl)
-
- case (l: Literal[_], Seq()) =>
- l
-
- case (other, _) =>
- context.reporter.error(other.getPos, "Error: don't know how to handle " + other.asString + " in Evaluator ("+other.getClass+").")
- throw EvalError("Unhandled case in Evaluator: " + other.asString)
-
- }
-
-}
diff --git a/src/main/scala/inox/evaluators/TracingEvaluator.scala b/src/main/scala/inox/evaluators/TracingEvaluator.scala
deleted file mode 100644
index dca816d87..000000000
--- a/src/main/scala/inox/evaluators/TracingEvaluator.scala
+++ /dev/null
@@ -1,118 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Definitions._
-import purescala.Types._
-
-class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) extends RecursiveEvaluator(ctx, prog, maxSteps) {
- type RC = TracingRecContext
- type GC = TracingGlobalContext
-
- def initRC(mappings: Map[Identifier, Expr]) = TracingRecContext(mappings, 2)
-
- def initGC(model: solvers.Model, check: Boolean) = new TracingGlobalContext(Nil, model, check)
-
- class TracingGlobalContext(var values: List[(Tree, Expr)], model: solvers.Model, check: Boolean)
- extends GlobalContext(model, this.maxSteps, check)
-
- case class TracingRecContext(mappings: Map[Identifier, Expr], tracingFrames: Int) extends RecContext[TracingRecContext] {
- def newVars(news: Map[Identifier, Expr]) = copy(mappings = news)
- }
-
- override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = {
- try {
- val (res, recordedRes) = expr match {
- case Let(i,ex,b) =>
- // We record the value of the val at the position of Let, not the value of the body.
- val first = e(ex)
- val res = e(b)(rctx.withNewVar(i, first), gctx)
- (res, first)
-
- case p: Passes =>
- val r = e(p.asConstraint)
- (r, r)
-
- case MatchExpr(scrut, cases) =>
- val rscrut = e(scrut)
-
- val r = cases.toStream.map(c => matchesCase(rscrut, c)).find(_.nonEmpty) match {
- case Some(Some((c, mappings))) =>
- gctx.values ++= (Map(c.pattern -> rscrut) ++ mappings.map { case (id, v) => id.toVariable.setPos(id) -> v })
-
- e(c.rhs)(rctx.withNewVars(mappings), gctx)
- case _ =>
- throw RuntimeError("MatchError: "+rscrut+" did not match any of the cases")
- }
-
- (r, r)
-
- case SpecializedFunctionInvocation(res) => (res, res)
-
- case fi @ FunctionInvocation(tfd, args) =>
- if (gctx.stepsLeft < 0) {
- throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
- }
- gctx.stepsLeft -= 1
-
- val evArgs = args.map(a => e(a))
-
- // build a mapping for the function...
- val frame = new TracingRecContext(tfd.paramSubst(evArgs), rctx.tracingFrames-1)
-
- if(tfd.hasPrecondition) {
- e(tfd.precondition.get)(frame, gctx) match {
- case BooleanLiteral(true) =>
- case BooleanLiteral(false) =>
- throw RuntimeError("Precondition violation for " + tfd.id.name + " reached in evaluation.: " + tfd.precondition.get)
- case other => throw RuntimeError(typeErrorMsg(other, BooleanType))
- }
- }
-
- if(!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
- throw EvalError("Tracing Evaluation of function with unknown implementation.")
- }
-
- val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
- val callResult = e(body)(frame, gctx)
-
- tfd.postcondition match {
- case Some(post) =>
-
- e(Application(post, Seq(callResult)))(frame, gctx) match {
- case BooleanLiteral(true) =>
- case BooleanLiteral(false) => throw RuntimeError("Postcondition violation for " + tfd.id.name + " reached in evaluation.")
- case other => throw EvalError(typeErrorMsg(other, BooleanType))
- }
- case None =>
- }
-
- (callResult, callResult)
- case _ =>
- val res = super.e(expr)
- (res, res)
- }
- if (rctx.tracingFrames > 0) {
- gctx.values ::= (expr -> recordedRes)
- }
-
- res
- } catch {
- case ee @ EvalError(e) =>
- if (rctx.tracingFrames > 0) {
- gctx.values ::= (expr -> Error(expr.getType, e))
- }
- throw ee;
-
- case re @ RuntimeError(e) =>
- if (rctx.tracingFrames > 0) {
- gctx.values ::= (expr -> Error(expr.getType, e))
- }
- throw re;
- }
- }
-
-}
diff --git a/src/main/scala/inox/evaluators/TrackingEvaluator.scala b/src/main/scala/inox/evaluators/TrackingEvaluator.scala
deleted file mode 100644
index 7b652742f..000000000
--- a/src/main/scala/inox/evaluators/TrackingEvaluator.scala
+++ /dev/null
@@ -1,124 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-import purescala.Types._
-
-import scala.collection.mutable.{Map => MMap}
-
-/** An [[Evaluator]] that tracks information about the runtime call tree.
- * Transitive dependencies between function calls are stored in [[fullCallGraph]].
- * Additionally, [[fiStatus]] tracks if each function invocation was successful or erroneous (led to an error).
- */
-class TrackingEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext {
- type RC = CollectingRecContext
-
- def initRC(mappings: Map[Identifier, Expr]) = CollectingRecContext(mappings, None)
-
- type FI = (FunDef, Seq[Expr])
-
- // This is a call graph to track dependencies of function invocations.
- // If fi1 calls fi2 but fails fi2's precondition, we consider it
- // fi1's fault and we don't register the dependency.
- private val callGraph : MMap[FI, Set[FI]] = MMap()
- // Register a call without any edges towards other calls
- private def registerNode(fi : FI) = if (!callGraph.contains(fi)) callGraph update (fi, Set())
- // Register an edge - also registers start and end nodes
- private def registerCall(fi : FI, lastFI : Option[FI]) = {
- lastFI foreach { lfi =>
- callGraph update (lfi, callGraph(lfi) + fi)
- }
- }
- def fullCallGraph = leon.utils.GraphOps.transitiveClosure(callGraph.toMap)
-
- // Tracks if every function invocation succeeded or failed
- private val fiStatus_ : MMap[FI, Boolean] = MMap().withDefaultValue(false)
- private def registerSuccessful(fi : FI) = fiStatus_ update (fi, true )
- private def registerFailed (fi : FI) = fiStatus_ update (fi, false)
- def fiStatus = fiStatus_.toMap.withDefaultValue(false)
-
- case class CollectingRecContext(mappings: Map[Identifier, Expr], lastFI : Option[FI]) extends RecContext[CollectingRecContext] {
- def newVars(news: Map[Identifier, Expr]) = copy(news, lastFI)
- def withLastFI(fi : FI) = copy(lastFI = Some(fi))
- }
-
- override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
- case SpecializedFunctionInvocation(res) => res
-
- case FunctionInvocation(tfd, args) =>
- if (gctx.stepsLeft < 0) {
- throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
- }
- gctx.stepsLeft -= 1
-
- val evArgs = args.map(a => e(a))
-
- // build a mapping for the function...
- val frameBlamingCaller = rctx.newVars(tfd.paramSubst(evArgs))
-
- if(tfd.hasPrecondition) {
- e(tfd.precondition.get)(frameBlamingCaller, gctx) match {
- case BooleanLiteral(true) =>
- // We consider this function invocation successful, unless the opposite is proven.
- registerSuccessful(tfd.fd, evArgs)
- // Only register a call dependency if the call we depend on does not fail precondition
- registerCall((tfd.fd, evArgs), rctx.lastFI)
- registerNode((tfd.fd, evArgs))
- case BooleanLiteral(false) =>
- // Caller's fault!
- rctx.lastFI foreach registerFailed
- throw RuntimeError("Precondition violation for " + tfd.id.name + " reached in evaluation.: " + tfd.precondition.get)
- case other =>
- // Caller's fault!
- rctx.lastFI foreach registerFailed
- throw RuntimeError(typeErrorMsg(other, BooleanType))
- }
- } else {
- registerSuccessful(tfd.fd, evArgs)
- registerNode((tfd.fd, evArgs))
- registerCall((tfd.fd, evArgs), rctx.lastFI)
- }
-
- if(!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
- throw EvalError("Tracking Evaluation of function with unknown implementation.")
- }
-
- val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
-
- val frameBlamingCallee = frameBlamingCaller.withLastFI(tfd.fd, evArgs)
-
- val callResult = e(body)(frameBlamingCallee, gctx)
-
- tfd.postcondition match {
- case Some(post) =>
- e(Application(post, Seq(callResult)))(frameBlamingCallee, gctx) match {
- case BooleanLiteral(true) =>
- case BooleanLiteral(false) =>
- // Callee's fault
- registerFailed(tfd.fd, evArgs)
- throw RuntimeError("Postcondition violation for " + tfd.id.name + " reached in evaluation.")
- case other =>
- // Callee's fault
- registerFailed(tfd.fd, evArgs)
- throw EvalError(typeErrorMsg(other, BooleanType))
- }
- case None =>
- }
-
- callResult
-
- case other =>
- try {
- super.e(other)
- } catch {
- case t : Throwable =>
- rctx.lastFI foreach registerFailed
- throw t
- }
- }
-
-}
diff --git a/src/main/scala/inox/solvers/EvaluatingSolver.scala b/src/main/scala/inox/solvers/EvaluatingSolver.scala
deleted file mode 100644
index 292ef1605..000000000
--- a/src/main/scala/inox/solvers/EvaluatingSolver.scala
+++ /dev/null
@@ -1,20 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Definitions._
-import evaluators._
-
-trait EvaluatingSolver extends Solver {
- val program: Program
-
- val useCodeGen: Boolean
-
- val evaluator: DeterministicEvaluator = if (useCodeGen) {
- new CodeGenEvaluator(context, program, sctx.bank)
- } else {
- new DefaultEvaluator(context, program, sctx.bank)
- }
-}
-
diff --git a/src/main/scala/inox/solvers/RawArray.scala b/src/main/scala/inox/solvers/RawArray.scala
deleted file mode 100644
index e651bfea4..000000000
--- a/src/main/scala/inox/solvers/RawArray.scala
+++ /dev/null
@@ -1,81 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Types._
-import purescala.Expressions._
-import purescala.Extractors._
-import purescala.TypeOps._
-import purescala.{PrettyPrintable, PrinterContext}
-import purescala.PrinterHelpers._
-
-// Corresponds to a complete map (SMT Array), not a Leon/Scala array
-// Only used within solvers or SMT for encoding purposes
-case class RawArrayType(from: TypeTree, to: TypeTree) extends TypeTree with PrettyPrintable {
- override def asString(implicit ctx: LeonContext) = {
- s"RawArrayType[${from.asString}, ${to.asString}]"
- }
-
- override def printWith(implicit pctx: PrinterContext) = {
- p"RawArrayType[$from, $to]"
- }
-}
-
-// Corresponds to a raw array value, which is coerced to a Leon expr depending on target type (set/array)
-case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr with Extractable {
-
- override def extract: Option[(Seq[Expr], (Seq[Expr]) => Expr)] = {
- val linearized: Seq[Expr] = elems.toVector.flatMap(p => Seq(p._1, p._2)) :+ default
- Some((linearized, es => {
- val freshElems = es.dropRight(1).grouped(2).map(p => p(0) -> p(1)).toMap
- RawArrayValue(keyTpe, freshElems, es.last)
- }))
- }
-
- val getType = RawArrayType(keyTpe, default.getType)
-
- override def asString(implicit ctx: LeonContext) = {
- val elemsString = elems.map { case (k, v) => k.asString+" -> "+v.asString } mkString(", ")
- s"RawArray[${keyTpe.asString}]($elemsString, default = ${default.asString})"
- }
-}
-
-case class RawArraySelect(array: Expr, index: Expr) extends Expr with Extractable with PrettyPrintable {
-
- override def extract: Option[(Seq[Expr], (Seq[Expr]) => Expr)] =
- Some((Seq(array, index), es => RawArraySelect(es(0), es(1))))
-
- val getType = array.getType match {
- case RawArrayType(from, to) if isSubtypeOf(index.getType, from) =>
- to
- case _ =>
- Untyped
- }
-
- override def asString(implicit ctx: LeonContext) = {
- s"$array($index)"
- }
-
- override def printWith(implicit pctx: PrinterContext) = {
- p"$array($index)"
- }
-
-}
-
-case class RawArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr with Extractable with PrettyPrintable {
-
- val getType = array.getType
-
- override def extract: Option[(Seq[Expr], (Seq[Expr]) => Expr)] =
- Some((Seq(array, index, newValue), es => RawArrayUpdated(es(0), es(1), es(2))))
-
- override def asString(implicit ctx: LeonContext) = {
- s"$array($index) = $newValue"
- }
-
- override def printWith(implicit pctx: PrinterContext) = {
- p"$array($index) = $newValue"
- }
-
-}
diff --git a/src/main/scala/inox/solvers/string/StringSolver.scala b/src/main/scala/inox/solvers/string/StringSolver.scala
index 5fac95318..c39dc9043 100644
--- a/src/main/scala/inox/solvers/string/StringSolver.scala
+++ b/src/main/scala/inox/solvers/string/StringSolver.scala
@@ -11,16 +11,16 @@ import scala.annotation.tailrec
*/
object StringSolver {
type Assignment = Map[Identifier, String]
-
+
type StringFormToken = Either[String, Identifier]
-
+
type StringForm = List[StringFormToken]
-
+
type Equation = (StringForm, String)
-
+
/** Sequences of equalities such as xyz"1"uv"2" = "1, 2" */
type Problem = List[Equation]
-
+
def renderStringForm(sf: StringForm): String = sf match {
case Left(const)::Nil => "\""+const+"\""
case Right(id)::Nil => id.toString
@@ -28,7 +28,7 @@ object StringSolver {
case Right(id)::q => id.toString + "+" + renderStringForm(q)
case Nil => ""
}
-
+
def renderProblem(p: Problem): String = {
def renderEquation(e: Equation): String = {
renderStringForm(e._1) + "==\""+e._2+"\""
@@ -36,14 +36,14 @@ object StringSolver {
p match {case Nil => ""
case e::q => renderEquation(e) + ", " + renderProblem(q)}
}
-
+
/** Evaluates a String form. Requires the solution to have an assignment to all identifiers. */
@tailrec def evaluate(s: Assignment, acc: StringBuffer = new StringBuffer(""))(sf: StringForm): String = sf match {
case Nil => acc.toString
case Left(constant)::q => evaluate(s, acc append constant)(q)
case Right(identifier)::q => evaluate(s, acc append s(identifier))(q)
}
-
+
/** Assigns the new values to the equations and simplify them at the same time. */
@tailrec def reduceStringForm(s: Assignment, acc: ListBuffer[StringFormToken] = ListBuffer())(sf: StringForm): StringForm = sf match {
case Nil => acc.toList
@@ -702,4 +702,4 @@ object StringSolver {
solution <- minimizeChanges(newSolutions_nonredundant, newProblem, ifVariable, initialMapping: Assignment)
} yield solution
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/inox/trees/Quantification.scala b/src/main/scala/inox/solvers/unrolling/Quantification.scala
similarity index 100%
rename from src/main/scala/inox/trees/Quantification.scala
rename to src/main/scala/inox/solvers/unrolling/Quantification.scala
diff --git a/src/main/scala/inox/trees/CallGraph.scala b/src/main/scala/inox/trees/CallGraph.scala
index 63fe2c570..0c5d1b2b0 100644
--- a/src/main/scala/inox/trees/CallGraph.scala
+++ b/src/main/scala/inox/trees/CallGraph.scala
@@ -1,7 +1,7 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
-package purescala
+package inox
+package trees
import Definitions._
import Expressions._
diff --git a/src/main/scala/inox/trees/Constructors.scala b/src/main/scala/inox/trees/Constructors.scala
index 22844a422..85ec99a73 100644
--- a/src/main/scala/inox/trees/Constructors.scala
+++ b/src/main/scala/inox/trees/Constructors.scala
@@ -1,15 +1,7 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
-package purescala
-
-import Expressions._
-import Extractors._
-import ExprOps._
-import Definitions._
-import TypeOps._
-import Common._
-import Types._
+package inox
+package trees
/** Provides constructors for [[purescala.Expressions]].
*
@@ -17,7 +9,8 @@ import Types._
* potentially use a different expression node if one is more suited.
* @define encodingof Encoding of
* */
-trait Constructors { self: Expressions =>
+trait Constructors { self: ExprOps =>
+ import trees._
/** If `isTuple`:
* `tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> x`
@@ -45,7 +38,7 @@ trait Constructors { self: Expressions =>
* @see [[purescala.Expressions.Let]]
*/
def let(id: Identifier, e: Expr, bd: Expr) = {
- if (variablesOf(bd) contains id)
+ if (exprOps.variablesOf(bd) contains id)
Let(id, e, bd)
else bd
}
diff --git a/src/main/scala/inox/trees/DefinitionTransformer.scala b/src/main/scala/inox/trees/DefinitionTransformer.scala
deleted file mode 100644
index f27a11046..000000000
--- a/src/main/scala/inox/trees/DefinitionTransformer.scala
+++ /dev/null
@@ -1,218 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import Common._
-import Definitions._
-import Expressions._
-import Types._
-
-import utils._
-import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
-
-class DefinitionTransformer(
- idMap: Bijection[Identifier, Identifier] = new Bijection[Identifier, Identifier],
- fdMap: Bijection[FunDef , FunDef ] = new Bijection[FunDef , FunDef ],
- cdMap: Bijection[ClassDef , ClassDef ] = new Bijection[ClassDef , ClassDef ]) extends TreeTransformer {
-
- private def transformId(id: Identifier, freshen: Boolean): Identifier = {
- val ntpe = transform(id.getType)
- if (ntpe == id.getType && !freshen) id else id.duplicate(tpe = ntpe)
- }
-
- def transformType(tpe: TypeTree): Option[TypeTree] = None
- final override def transform(tpe: TypeTree): TypeTree = {
- super.transform(transformType(tpe).getOrElse(tpe))
- }
-
- final override def transform(id: Identifier): Identifier = {
- val ntpe = transform(id.getType)
- idMap.getB(id) match {
- case Some(nid) if ntpe == nid.getType => nid
- case _ =>
- val nid = transformId(id, false)
- idMap += id -> nid
- nid
- }
- }
-
- def transformExpr(e: Expr)(implicit bindings: Map[Identifier, Identifier]): Option[Expr] = None
- final override def transform(e: Expr)(implicit bindings: Map[Identifier, Identifier]): Expr = {
- transformExpr(e) match {
- case Some(r) => super.transform(r)
- case None => super.transform(e)
- }
- }
-
- protected def transformFunDef(fd: FunDef): Option[FunDef] = None
- final override def transform(fd: FunDef): FunDef = {
- if ((fdMap containsB fd) || (tmpFdMap containsB fd)) fd
- else if (tmpFdMap containsA fd) tmpFdMap.toB(fd)
- else fdMap.getBorElse(fd, {
- transformDefs(fd)
- fdMap.toB(fd)
- })
- }
-
-
- /** Override this to provide specific ClassDef transform
- *
- * It is guaranteed to only be called once per ClassDef accross the whole
- * program transformation, and won't be applied recursively
- * to the transformed class.
- *
- * This design choice is to allow for a typical use case in which you
- * want to add a field to every single case classes in your program,
- * and for obvious reasons you don't want to apply this transformation
- * recursively on transformed case classes. Another typical case is
- * to duplicate the whole program, which needs duplicating each case
- * class by freshening all the fields. Without this specific contract,
- * client implementation of such functionalities would require the use
- * of a local map to track which classes are in the program before starting
- * the transformation, and which classes was already transformed.
- */
- protected def transformClassDef(cd: ClassDef): Option[ClassDef] = None
- final override def transform(cd: ClassDef): ClassDef = {
- if ((cdMap containsB cd) || (tmpCdMap containsB cd)) cd
- else if (tmpCdMap containsA cd) tmpCdMap.toB(cd)
- else
- cdMap.getBorElse(cd, {
- transformDefs(cd)
- cdMap.toB(cd)
- })
- }
-
- private val dependencies = new DependencyFinder
- private val tmpCdMap = new Bijection[ClassDef, ClassDef]
- private val tmpFdMap = new Bijection[FunDef , FunDef ]
- private val fieldsSet: MutableSet[CaseClassDef] = MutableSet.empty[CaseClassDef]
-
- private def transformDefs(base: Definition): Unit = {
- val (cds, fds) = {
- val deps = dependencies(base) + base
- val (c, f) = deps.partition(_.isInstanceOf[ClassDef])
- val cds = c.map(_.asInstanceOf[ClassDef]).filter(cd => !(cdMap containsA cd) && !(cdMap containsB cd))
- val fds = f.map(_.asInstanceOf[FunDef]).filter(fd => !(fdMap containsA fd) && !(fdMap containsB fd))
- (cds, fds)
- }
-
- val transformedCds = (for (cd <- cds if !(cdMap containsA cd) && !(cdMap containsB cd)) yield {
- val ncd = transformClassDef(cd).getOrElse(cd)
- tmpCdMap += cd -> ncd
- if (cd ne ncd) Some(cd -> ncd) else None
- }).flatten.toMap
-
- val transformedFds = (for (fd <- fds if !(fdMap containsA fd) && !(fdMap containsB fd)) yield {
- val nfd = transformFunDef(fd).getOrElse(fd)
- tmpFdMap += fd -> nfd
- if (fd ne nfd) Some(fd -> nfd) else None
- }).flatten.toMap
-
- val req: Set[Definition] = {
- val requireCache: MutableMap[Definition, Boolean] = MutableMap.empty
- def required(d: Definition): Boolean = requireCache.getOrElse(d, {
- val res = d match {
- case funDef: FunDef =>
- val (fd, checkBody) = transformedFds.get(funDef) match {
- case Some(fd) => (fd, false)
- case None => (funDef, true)
- }
-
- val newReturn = transform(fd.returnType)
- lazy val newParams = fd.params.map(vd => ValDef(transform(vd.id)))
- newReturn != fd.returnType || newParams != fd.params || (checkBody && {
- val newBody = transform(fd.fullBody)((fd.params.map(_.id) zip newParams.map(_.id)).toMap)
- newBody != fd.fullBody
- })
-
- case cd: ClassDef =>
- !(transformedCds contains cd) &&
- (cd.fieldsIds.exists(id => transform(id.getType) != id.getType) ||
- cd.invariant.exists(required))
-
- case _ => scala.sys.error("Should never happen!?")
- }
-
- requireCache += d -> res
- res
- })
-
- val filtered = (cds ++ fds) filter required
-
- // clear can only take place after all calls to required(_) have taken place
- tmpCdMap.clear()
- tmpFdMap.clear()
-
- filtered
- }
-
- val (fdsToDup: Set[FunDef], cdsToDup: Set[ClassDef]) = {
- val prevTransformed = cdMap.aSet.filter(a => a ne cdMap.toB(a)) ++ fdMap.aSet.filter(a => a ne fdMap.toB(a))
- val reqs = req ++ transformedCds.keys ++ transformedFds.keys ++ prevTransformed
-
- val cdsToDup = cds filter { cd => req(cd) ||
- (!(transformedCds contains cd) && (dependencies(cd) & reqs).nonEmpty) ||
- ((transformedCds contains cd) && ((cd.root +: cd.root.knownDescendants).toSet & req).nonEmpty) }
-
- val fdsToDup = fds filter (fd => req(fd) || {
- val deps = dependencies(fd)
- (deps exists { case cd: ClassDef => cdsToDup(cd) case _ => false }) ||
- (!(transformedFds contains fd) && (deps & reqs).nonEmpty) })
-
- (fdsToDup, cdsToDup)
- }
-
- val fdsToTransform = (transformedFds.keys filterNot fdsToDup).toSet
- val cdsToTransform = (transformedCds.keys filterNot cdsToDup).toSet
-
- val fdsToKeep = fds filterNot (fd => fdsToDup(fd) || fdsToTransform(fd))
- val cdsToKeep = cds filterNot (cd => cdsToDup(cd) || cdsToTransform(cd))
-
- fdMap ++= fdsToKeep.map(fd => fd -> fd) ++ fdsToTransform.map(fd => fd -> transformedFds(fd))
- cdMap ++= cdsToKeep.map(cd => cd -> cd) ++ cdsToTransform.map(cd => cd -> transformedCds(cd))
-
- def duplicateCd(cd: ClassDef): ClassDef = cdMap.cachedB(cd) {
- val parent = cd.parent.map(act => act.copy(classDef = duplicateCd(act.classDef).asInstanceOf[AbstractClassDef]))
- transformedCds.getOrElse(cd, cd) match {
- case acd: AbstractClassDef => acd.duplicate(id = transformId(acd.id, true), parent = parent)
- case ccd: CaseClassDef => ccd.duplicate(id = transformId(ccd.id, true), parent = parent)
- }
- }
-
- def duplicateFd(fd: FunDef): FunDef = fdMap.cachedB(fd) {
- val ffd = transformedFds.getOrElse(fd, fd)
- val newId = transformId(ffd.id, true)
- val newReturn = transform(ffd.returnType)
- val newParams = ffd.params map (vd => ValDef(transformId(vd.id, true)))
- ffd.duplicate(id = newId, params = newParams, returnType = newReturn)
- }
-
- for (cd <- cdsToDup) duplicateCd(cd)
- for (fd <- fdsToDup) duplicateFd(fd)
-
- for (cd <- cdsToDup ++ cdsToTransform) {
- val newCd = cdMap.toB(cd)
- cd.invariant.foreach(fd => newCd.setInvariant(transform(fd)))
- newCd match {
- case (newCcd: CaseClassDef) =>
- if(!fieldsSet(newCcd)) {
- //newCcd is duplicated from the original ccd, so it will always have defined fields,
- //and they will the same as the original ccd fields.
- newCcd.setFields(newCcd.fields.map(vd => ValDef(transformId(vd.id, true))))
- fieldsSet += newCcd
- }
- case _ =>
- }
- }
-
- for (fd <- fdsToDup ++ fdsToTransform) {
- val nfd = fdMap.toB(fd)
- val bindings = (fd.params zip nfd.params).map(p => p._1.id -> p._2.id).toMap ++
- nfd.params.map(vd => vd.id -> vd.id)
-
- nfd.fullBody = transform(nfd.fullBody)(bindings)
- }
- }
-}
-
diff --git a/src/main/scala/inox/trees/Definitions.scala b/src/main/scala/inox/trees/Definitions.scala
index ded2b3615..7d4c8efd6 100644
--- a/src/main/scala/inox/trees/Definitions.scala
+++ b/src/main/scala/inox/trees/Definitions.scala
@@ -3,16 +3,9 @@
package leon
package purescala
-import utils.Library
-import Common._
-import Expressions._
-import ExprOps._
-import Types._
-import TypeOps._
-
import scala.collection.mutable.{Map => MutableMap}
-object Definitions {
+trait Definitions { self: Trees =>
sealed trait Definition extends Tree {
val id: Identifier
@@ -88,10 +81,10 @@ object Definitions {
// Compiler annotations given in the source code as @annot
case class Annotation(annot: String, args: Seq[Option[Any]]) extends FunctionFlag with ClassFlag
+ // Class has ADT invariant method
+ case class HasADTInvariant(id: Identifier) extends ClassFlag
// Is inlined
case object IsInlined extends FunctionFlag
- // Is an ADT invariant method
- case object IsADTInvariant(id: Identifier) extends FunctionFlag
/** Represents a class definition (either an abstract- or a case-class) */
sealed trait ClassDef extends Definition {
@@ -105,11 +98,8 @@ object Definitions {
def hasParent = parent.isDefined
- def invariana(implicit p: Program)t: Option[FunDef] = {
- // TODO
- parent.flatMap(_.classDef.invariant).orElse(_invariant)
-
- }
+ def invariant(implicit p: Program): Option[FunDef] =
+ flags.collect { case HasADTInvariant(id) => id }.map(p.getFunction)
def annotations: Set[String] = extAnnotations.keySet
def extAnnotations: Map[String, Seq[Option[Any]]] = flags.collect { case Annotation(s, args) => s -> args }.toMap
diff --git a/src/main/scala/inox/trees/DependencyFinder.scala b/src/main/scala/inox/trees/DependencyFinder.scala
deleted file mode 100644
index 95e894f16..000000000
--- a/src/main/scala/inox/trees/DependencyFinder.scala
+++ /dev/null
@@ -1,103 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import Common._
-import Definitions._
-import Expressions._
-import Extractors._
-import Types._
-
-import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
-
-/** Accumulate dependency information for a given program */
-class DependencyFinder(p: Program) {
- private val deps: MutableMap[Identifier, Set[Identifier]] = MutableMap.empty
-
- /** Return all dependencies for a given Definition
- *
- * Use a cache internally, so two calls (from the same instance of DependencyFinder)
- * will return the same Set without re-computing. A dependency for ClassDef `d` is
- * any ClassDef references by the fields of any class in the hierarch of the `d`, as
- * well as any class invariants in the hierarchy.
- *
- * Dependencies for FunDef are any ClassDef that appear in any types (parameter list,
- * return value) as well as transitive dependencies via the body (a function invocation
- * in the body will generate a dependency to the fundef of the call).
- *
- * A def does not depend on itself by default. But if it calls itself recursively, or
- * via some transitive dependencies, then the return set will contain the input def.
- */
- def apply(d: Definition): Set[Definition] = deps.getOrElseUpdate(d, {
- new Finder(d).dependencies
- })
-
- private class Finder(private var current: Definition) extends TreeTraverser {
- val foundDeps: MutableMap[Definition, MutableSet[Definition]] = MutableMap.empty
-
- private def withCurrent[T](d: Definition)(b: => T): T = {
- if (!(foundDeps contains d)) foundDeps(d) = MutableSet.empty
- val c = current
- current = d
- val res = b
- current = c
- res
- }
-
- override def traverse(id: Identifier): Unit = traverse(id.getType)
-
- override def traverse(cd: ClassDef): Unit = if (!foundDeps(current)(cd)) {
- foundDeps(current) += cd
- if (!(deps contains cd) && !(foundDeps contains cd)) traverseClassDef(cd)
- }
-
- private def traverseClassDef(cd: ClassDef): Unit = {
- for (cd <- cd.root.knownDescendants :+ cd) {
- cd.invariant foreach (fd => withCurrent(cd)(traverse(fd)))
- withCurrent(cd)(cd.fieldsIds foreach traverse)
- cd.parent foreach { p =>
- foundDeps(p.classDef) = foundDeps.getOrElse(p.classDef, MutableSet.empty) + cd
- foundDeps(cd) = foundDeps.getOrElse(cd, MutableSet.empty) + p.classDef
- }
- }
- }
-
- override def traverse(fd: FunDef): Unit = if (!foundDeps(current)(fd)) {
- foundDeps(current) += fd
- if (!(deps contains fd) && !(foundDeps contains fd)) traverseFunDef(fd)
- }
-
- private def traverseFunDef(fd: FunDef): Unit = withCurrent(fd) {
- fd.params foreach (vd => traverse(vd.id))
- traverse(fd.returnType)
- traverse(fd.fullBody)
- }
-
- def dependencies: Set[Definition] = {
- current match {
- case fd: FunDef => traverseFunDef(fd)
- case cd: ClassDef => traverseClassDef(cd)
- case _ =>
- }
-
- for ((d, ds) <- foundDeps) {
- deps(d) = deps.getOrElse(d, Set.empty) ++ ds
- }
-
- var changed = false
- do {
- changed = false
- for ((d, ds) <- deps.toSeq) {
- val next = ds ++ ds.flatMap(d => deps.getOrElse(d, Set.empty))
- if (!(next subsetOf ds)) {
- deps(d) = next
- changed = true
- }
- }
- } while (changed)
-
- deps(current)
- }
- }
-}
diff --git a/src/main/scala/inox/trees/ExprOps.scala b/src/main/scala/inox/trees/ExprOps.scala
index e3406cbbf..50c9de76f 100644
--- a/src/main/scala/inox/trees/ExprOps.scala
+++ b/src/main/scala/inox/trees/ExprOps.scala
@@ -3,16 +3,6 @@
package leon
package purescala
-import Common._
-import Types._
-import Definitions._
-import Expressions._
-import Extractors._
-import Constructors._
-import utils._
-import solvers._
-import scala.language.implicitConversions
-
/** Provides functions to manipulate [[purescala.Expressions]].
*
* This object provides a few generic operations on Leon expressions,
@@ -32,7 +22,9 @@ import scala.language.implicitConversions
* operations on Leon expressions.
*
*/
-trait ExprOps extends GenTreeOps[Expr] with Extractors { self: Trees =>
+trait ExprOps extends GenTreeOps[Expr] with Constructors with Paths {
+ val trees: Trees
+ import trees._
val Deconstructor = Operator
diff --git a/src/main/scala/inox/trees/Extractors.scala b/src/main/scala/inox/trees/Extractors.scala
index ac3a22663..19998d88b 100644
--- a/src/main/scala/inox/trees/Extractors.scala
+++ b/src/main/scala/inox/trees/Extractors.scala
@@ -1,12 +1,7 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
-package purescala
-
-import Expressions._
-import Common._
-import Types._
-import Constructors._
+package inox
+package trees
trait Extractors { self: Expressions =>
@@ -23,7 +18,10 @@ trait Extractors { self: Expressions =>
* one need to simplify the tree, it is easy to write/call a simplification
* function that would simply apply the corresponding constructor for each node.
*/
- object Operator extends TreeExtractor[Expr] {
+ object Operator extends TreeExtractor {
+ val trees: Extractors.this.trees = Extractors.this.trees
+ type SubTree = trees.Expr
+
def unapply(expr: Expr): Option[(Seq[Expr], (Seq[Expr]) => Expr)] = expr match {
/* Unary operators */
case Not(t) =>
diff --git a/src/main/scala/inox/trees/GenTreeOps.scala b/src/main/scala/inox/trees/GenTreeOps.scala
index 286b1ae23..35cde2198 100644
--- a/src/main/scala/inox/trees/GenTreeOps.scala
+++ b/src/main/scala/inox/trees/GenTreeOps.scala
@@ -1,17 +1,18 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-package leon
-package purescala
-
-import Common._
-import utils._
+package inox
+package trees
/** A type that pattern matches agains a type of [[Tree]] and extracts it subtrees,
* and a builder that reconstructs a tree of the same type from subtrees.
*
* @tparam SubTree The type of the tree
*/
-trait TreeExtractor[SubTree <: Tree] {
+trait TreeExtractor {
+ val trees: Trees
+ import trees._
+
+ type SubTree <: Tree
def unapply(e: SubTree): Option[(Seq[SubTree], (Seq[SubTree]) => SubTree)]
}
@@ -19,10 +20,17 @@ trait TreeExtractor[SubTree <: Tree] {
*
* @tparam SubTree The type of the tree
*/
-trait GenTreeOps[SubTree <: Tree] {
+trait GenTreeOps {
+ val trees: Trees
+ import trees._
+
+ type SubTree <: Tree
/** An extractor for [[SubTree]]*/
- val Deconstructor: TreeExtractor[SubTree]
+ val Deconstructor: TreeExtractor {
+ val trees: GenTreeOps.this.trees
+ type SubTree <: GenTreeOps.this.SubTree
+ }
/* ========
* Core API
diff --git a/src/main/scala/inox/trees/Path.scala b/src/main/scala/inox/trees/Path.scala
deleted file mode 100644
index d6e85d938..000000000
--- a/src/main/scala/inox/trees/Path.scala
+++ /dev/null
@@ -1,231 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import Common._
-import Definitions._
-import Expressions._
-import Constructors._
-import ExprOps._
-import Types._
-
-object Path {
- final type Element = Either[(Identifier, Expr), Expr]
- def empty: Path = new Path(Seq.empty)
- def apply(p: Expr): Path = p match {
- case Let(i, e, b) => new Path(Seq(Left(i -> e))) merge apply(b)
- case _ => new Path(Seq(Right(p)))
- }
- def apply(path: Seq[Expr]): Path = new Path(path.map(Right(_)))
-}
-
-/** Encodes path conditions
- *
- * Paths are encoded as an (ordered) series of let-bindings and boolean
- * propositions. A path is satisfiable iff all propositions are true
- * in the context of the provided let-bindings.
- *
- * This encoding enables let-bindings over types for which equality is
- * not defined, whereas an encoding of let-bindings with equalities
- * could introduce non-sensical equations.
- */
-class Path private[purescala](
- private[purescala] val elements: Seq[Path.Element]) extends Printable {
-
- import Path.Element
-
- /** Add a binding to this [[Path]] */
- def withBinding(p: (Identifier, Expr)) = {
- def exprOf(e: Element) = e match { case Right(e) => e; case Left((_, e)) => e }
- val (before, after) = elements span (el => !variablesOf(exprOf(el)).contains(p._1))
- new Path(before ++ Seq(Left(p)) ++ after)
- }
- def withBindings(ps: Iterable[(Identifier, Expr)]) = {
- ps.foldLeft(this)( _ withBinding _ )
- }
-
- /** Add a condition to this [[Path]] */
- def withCond(e: Expr) = {
- if (e == BooleanLiteral(true)) this
- else new Path(elements :+ Right(e))
- }
- def withConds(es: Iterable[Expr]) = new Path(elements ++ es.filterNot( _ == BooleanLiteral(true)).map(Right(_)))
-
- /** Remove bound variables from this [[Path]]
- * @param ids the bound variables to remove
- */
- def --(ids: Set[Identifier]) = new Path(elements.filterNot(_.left.exists(p => ids(p._1))))
-
- /** Appends `that` path at the end of `this` */
- def merge(that: Path): Path = new Path(elements ++ that.elements)
-
- /** Appends `those` paths at the end of `this` */
- def merge(those: Traversable[Path]): Path = those.foldLeft(this)(_ merge _)
-
- /** Transforms all expressions inside the path
- *
- * Expressions in a path appear both on the right-hand side of let binders
- * and in boolean path conditions.
- */
- def map(f: Expr => Expr) = new Path(elements.map(_.left.map { case (id, e) => id -> f(e) }.right.map(f)))
-
- /** Splits the path on predicate `p`
- *
- * The path is split into
- * 1. the sub-path containing all conditions that pass `p` (and all let-bindings), and
- * 2. the sequence of conditions that didn't pass `p`.
- */
- def partition(p: Expr => Boolean): (Path, Seq[Expr]) = {
- val (passed, failed) = elements.partition {
- case Right(e) => p(e)
- case Left(_) => true
- }
-
- (new Path(passed), failed.flatMap(_.right.toOption))
- }
-
- /** Check if the path is empty
- *
- * A path is empty iff it contains no let-bindings and its path condition is trivial.
- */
- def isEmpty = elements.forall {
- case Right(BooleanLiteral(true)) => true
- case _ => false
- }
-
- /** Returns the negation of a path
- *
- * Path negation requires folding the path into a proposition and negating it.
- * However, all external let-binders can be preserved in the resulting path, thus
- * avoiding let-binding dupplication in future path foldings.
- */
- def negate: Path = {
- val (outers, rest) = elements.span(_.isLeft)
- new Path(outers :+ Right(not(fold[Expr](BooleanLiteral(true), let, Constructors.and(_, _))(rest))))
- }
-
- /** Returns a new path which depends ONLY on provided ids.
- *
- * Let-bindings obviously depend on some `id` if it corresponds to the bound
- * identifier. An expression depends on an `id` iff the identifier is
- * contained within the expression.
- *
- * This method makes little sense on its own and will typically be used from
- * within a fixpoint computation where the `ids` set is iteratively computed
- * by performing [[filterByIds]] calls on some (unchaning) base [[Path]].
- *
- * @see [[leon.purescala.FunctionClosure.close]] for an example usecase.
- */
- def filterByIds(ids: Set[Identifier]): Path = {
- def containsIds(ids: Set[Identifier])(e: Expr): Boolean = exists{
- case Variable(id) => ids.contains(id)
- case _ => false
- }(e)
-
- val newElements = elements.filter{
- case Left((id, e)) => ids.contains(id) || containsIds(ids)(e)
- case Right(e) => containsIds(ids)(e)
- }
- new Path(newElements)
- }
-
- /** Free variables within the path */
- lazy val variables: Set[Identifier] = fold[Set[Identifier]](Set.empty,
- (id, e, res) => res - id ++ variablesOf(e), (e, res) => res ++ variablesOf(e)
- )(elements)
-
- lazy val bindings: Seq[(Identifier, Expr)] = elements.collect { case Left(p) => p }
- lazy val boundIds = bindings map (_._1)
- lazy val conditions: Seq[Expr] = elements.collect { case Right(e) => e }
-
- def isBound(id: Identifier): Boolean = bindings.exists(p => p._1 == id)
-
- /** Fold the path elements
- *
- * This function takes two combiner functions, one for let bindings and one
- * for proposition expressions.
- */
- private def fold[T](base: T, combineLet: (Identifier, Expr, T) => T, combineCond: (Expr, T) => T)
- (elems: Seq[Element]): T = elems.foldRight(base) {
- case (Left((id, e)), res) => combineLet(id, e, res)
- case (Right(e), res) => combineCond(e, res)
- }
-
- /** Folds the path elements over a distributive proposition combinator [[combine]]
- *
- * Certain combiners can be distributive over let-binding folds. Namely, one
- * requires that `combine(let a = b in e1, e2)` be equivalent to
- * `let a = b in combine(e1, e2)` (where a \not\in FV(e2)). This is the case for
- * - conjunction [[and]]
- * - implication [[implies]]
- */
- private def distributiveClause(base: Expr, combine: (Expr, Expr) => Expr): Expr = {
- val (outers, rest) = elements.span(_.isLeft)
- val inner = fold[Expr](base, let, combine)(rest)
- fold[Expr](inner, let, (_,_) => scala.sys.error("Should never happen!"))(outers)
- }
-
- /** Folds the path into a conjunct with the expression `base` */
- def and(base: Expr) = distributiveClause(base, Constructors.and(_, _))
-
- /** Fold the path into an implication of `base`, namely `path ==> base` */
- def implies(base: Expr) = distributiveClause(base, Constructors.implies)
-
- /** Folds the path into a `require` wrapping the expression `body`
- *
- * The function takes additional optional parameters
- * - [[pre]] if one wishes to mix a pre-existing precondition into the final
- * [[leon.purescala.Expressions.Require]], and
- * - [[post]] for mixing a postcondition ([[leon.purescala.Expressions.Ensuring]]) in.
- */
- def specs(body: Expr, pre: Expr = BooleanLiteral(true), post: Expr = NoTree(BooleanType)) = {
- val (outers, rest) = elements.span(_.isLeft)
- val cond = fold[Expr](BooleanLiteral(true), let, Constructors.and(_, _))(rest)
-
- def wrap(e: Expr): Expr = {
- val bindings = rest.collect { case Left((id, e)) => id -> e }
- val idSubst = bindings.map(p => p._1 -> p._1.freshen).toMap
- val substMap = idSubst.mapValues(_.toVariable)
- val replace = replaceFromIDs(substMap, _: Expr)
- bindings.foldRight(replace(e)) { case ((id, e), b) => let(idSubst(id), replace(e), b) }
- }
-
- val req = Require(Constructors.and(cond, wrap(pre)), wrap(body))
- val full = post match {
- case l @ Lambda(args, body) => Ensuring(req, Lambda(args, wrap(body)).copiedFrom(l))
- case _ => req
- }
-
- fold[Expr](full, let, (_, _) => scala.sys.error("Should never happen!"))(outers)
- }
-
- /** Folds the path into the associated boolean proposition */
- lazy val toClause: Expr = and(BooleanLiteral(true))
-
- /** Like [[toClause]] but doesn't simplify final path through constructors
- * from [[leon.purescala.Constructors]] */
- lazy val fullClause: Expr = fold[Expr](BooleanLiteral(true), Let, And(_, _))(elements)
-
- /** Folds the path into a boolean proposition where let-bindings are
- * replaced by equations.
- *
- * CAUTION: Should only be used once INSIDE the solver!!
- */
- lazy val toPath: Expr = andJoin(elements.map {
- case Left((id, e)) => Equals(id.toVariable, e)
- case Right(e) => e
- })
-
- override def equals(that: Any): Boolean = that match {
- case p: Path => elements == p.elements
- case _ => false
- }
-
- override def hashCode: Int = elements.hashCode
-
- override def toString = asString(LeonContext.printNames)
- def asString(implicit ctx: LeonContext): String = fullClause.asString
- def asString(pgm: Program)(implicit ctx: LeonContext): String = fullClause.asString(pgm)
-}
-
diff --git a/src/main/scala/inox/trees/Paths.scala b/src/main/scala/inox/trees/Paths.scala
new file mode 100644
index 000000000..a5c0d7633
--- /dev/null
+++ b/src/main/scala/inox/trees/Paths.scala
@@ -0,0 +1,232 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package trees
+
+trait Paths { self: ExprOps =>
+ import trees._
+
+ object Path {
+ final type Element = Either[(Identifier, Expr), Expr]
+
+ def empty: Path = new Path(Seq.empty)
+
+ def apply(p: Expr): Path = p match {
+ case Let(i, e, b) => new Path(Seq(Left(i -> e))) merge apply(b)
+ case _ => new Path(Seq(Right(p)))
+ }
+
+ def apply(path: Seq[Expr]): Path = new Path(path.map(Right(_)))
+ }
+
+ /** Encodes path conditions
+ *
+ * Paths are encoded as an (ordered) series of let-bindings and boolean
+ * propositions. A path is satisfiable iff all propositions are true
+ * in the context of the provided let-bindings.
+ *
+ * This encoding enables let-bindings over types for which equality is
+ * not defined, whereas an encoding of let-bindings with equalities
+ * could introduce non-sensical equations.
+ */
+ class Path private[purescala](
+ private[purescala] val elements: Seq[Path.Element]) extends Printable {
+
+ import Path.Element
+
+ /** Add a binding to this [[Path]] */
+ def withBinding(p: (Identifier, Expr)) = {
+ def exprOf(e: Element) = e match { case Right(e) => e; case Left((_, e)) => e }
+ val (before, after) = elements span (el => !variablesOf(exprOf(el)).contains(p._1))
+ new Path(before ++ Seq(Left(p)) ++ after)
+ }
+
+ def withBindings(ps: Iterable[(Identifier, Expr)]) = {
+ ps.foldLeft(this)( _ withBinding _ )
+ }
+
+ /** Add a condition to this [[Path]] */
+ def withCond(e: Expr) = {
+ if (e == BooleanLiteral(true)) this
+ else new Path(elements :+ Right(e))
+ }
+
+ def withConds(es: Iterable[Expr]) = new Path(elements ++ es.filterNot( _ == BooleanLiteral(true)).map(Right(_)))
+
+ /** Remove bound variables from this [[Path]]
+ * @param ids the bound variables to remove
+ */
+ def --(ids: Set[Identifier]) = new Path(elements.filterNot(_.left.exists(p => ids(p._1))))
+
+ /** Appends `that` path at the end of `this` */
+ def merge(that: Path): Path = new Path(elements ++ that.elements)
+
+ /** Appends `those` paths at the end of `this` */
+ def merge(those: Traversable[Path]): Path = those.foldLeft(this)(_ merge _)
+
+ /** Transforms all expressions inside the path
+ *
+ * Expressions in a path appear both on the right-hand side of let binders
+ * and in boolean path conditions.
+ */
+ def map(f: Expr => Expr) = new Path(elements.map(_.left.map { case (id, e) => id -> f(e) }.right.map(f)))
+
+ /** Splits the path on predicate `p`
+ *
+ * The path is split into
+ * 1. the sub-path containing all conditions that pass `p` (and all let-bindings), and
+ * 2. the sequence of conditions that didn't pass `p`.
+ */
+ def partition(p: Expr => Boolean): (Path, Seq[Expr]) = {
+ val (passed, failed) = elements.partition {
+ case Right(e) => p(e)
+ case Left(_) => true
+ }
+
+ (new Path(passed), failed.flatMap(_.right.toOption))
+ }
+
+ /** Check if the path is empty
+ *
+ * A path is empty iff it contains no let-bindings and its path condition is trivial.
+ */
+ def isEmpty = elements.forall {
+ case Right(BooleanLiteral(true)) => true
+ case _ => false
+ }
+
+ /** Returns the negation of a path
+ *
+ * Path negation requires folding the path into a proposition and negating it.
+ * However, all external let-binders can be preserved in the resulting path, thus
+ * avoiding let-binding dupplication in future path foldings.
+ */
+ def negate: Path = {
+ val (outers, rest) = elements.span(_.isLeft)
+ new Path(outers :+ Right(not(fold[Expr](BooleanLiteral(true), let, Constructors.and(_, _))(rest))))
+ }
+
+ /** Returns a new path which depends ONLY on provided ids.
+ *
+ * Let-bindings obviously depend on some `id` if it corresponds to the bound
+ * identifier. An expression depends on an `id` iff the identifier is
+ * contained within the expression.
+ *
+ * This method makes little sense on its own and will typically be used from
+ * within a fixpoint computation where the `ids` set is iteratively computed
+ * by performing [[filterByIds]] calls on some (unchaning) base [[Path]].
+ *
+ * @see [[leon.purescala.FunctionClosure.close]] for an example usecase.
+ */
+ def filterByIds(ids: Set[Identifier]): Path = {
+ def containsIds(ids: Set[Identifier])(e: Expr): Boolean = exists{
+ case Variable(id) => ids.contains(id)
+ case _ => false
+ }(e)
+
+ val newElements = elements.filter{
+ case Left((id, e)) => ids.contains(id) || containsIds(ids)(e)
+ case Right(e) => containsIds(ids)(e)
+ }
+ new Path(newElements)
+ }
+
+ /** Free variables within the path */
+ lazy val variables: Set[Identifier] = fold[Set[Identifier]](Set.empty,
+ (id, e, res) => res - id ++ variablesOf(e), (e, res) => res ++ variablesOf(e)
+ )(elements)
+
+ lazy val bindings: Seq[(Identifier, Expr)] = elements.collect { case Left(p) => p }
+ lazy val boundIds = bindings map (_._1)
+ lazy val conditions: Seq[Expr] = elements.collect { case Right(e) => e }
+
+ def isBound(id: Identifier): Boolean = bindings.exists(p => p._1 == id)
+
+ /** Fold the path elements
+ *
+ * This function takes two combiner functions, one for let bindings and one
+ * for proposition expressions.
+ */
+ private def fold[T](base: T, combineLet: (Identifier, Expr, T) => T, combineCond: (Expr, T) => T)
+ (elems: Seq[Element]): T = elems.foldRight(base) {
+ case (Left((id, e)), res) => combineLet(id, e, res)
+ case (Right(e), res) => combineCond(e, res)
+ }
+
+ /** Folds the path elements over a distributive proposition combinator [[combine]]
+ *
+ * Certain combiners can be distributive over let-binding folds. Namely, one
+ * requires that `combine(let a = b in e1, e2)` be equivalent to
+ * `let a = b in combine(e1, e2)` (where a \not\in FV(e2)). This is the case for
+ * - conjunction [[and]]
+ * - implication [[implies]]
+ */
+ private def distributiveClause(base: Expr, combine: (Expr, Expr) => Expr): Expr = {
+ val (outers, rest) = elements.span(_.isLeft)
+ val inner = fold[Expr](base, let, combine)(rest)
+ fold[Expr](inner, let, (_,_) => scala.sys.error("Should never happen!"))(outers)
+ }
+
+ /** Folds the path into a conjunct with the expression `base` */
+ def and(base: Expr) = distributiveClause(base, Constructors.and(_, _))
+
+ /** Fold the path into an implication of `base`, namely `path ==> base` */
+ def implies(base: Expr) = distributiveClause(base, Constructors.implies)
+
+ /** Folds the path into a `require` wrapping the expression `body`
+ *
+ * The function takes additional optional parameters
+ * - [[pre]] if one wishes to mix a pre-existing precondition into the final
+ * [[leon.purescala.Expressions.Require]], and
+ * - [[post]] for mixing a postcondition ([[leon.purescala.Expressions.Ensuring]]) in.
+ */
+ def specs(body: Expr, pre: Expr = BooleanLiteral(true), post: Expr = NoTree(BooleanType)) = {
+ val (outers, rest) = elements.span(_.isLeft)
+ val cond = fold[Expr](BooleanLiteral(true), let, Constructors.and(_, _))(rest)
+
+ def wrap(e: Expr): Expr = {
+ val bindings = rest.collect { case Left((id, e)) => id -> e }
+ val idSubst = bindings.map(p => p._1 -> p._1.freshen).toMap
+ val substMap = idSubst.mapValues(_.toVariable)
+ val replace = replaceFromIDs(substMap, _: Expr)
+ bindings.foldRight(replace(e)) { case ((id, e), b) => let(idSubst(id), replace(e), b) }
+ }
+
+ val req = Require(Constructors.and(cond, wrap(pre)), wrap(body))
+ val full = post match {
+ case l @ Lambda(args, body) => Ensuring(req, Lambda(args, wrap(body)).copiedFrom(l))
+ case _ => req
+ }
+
+ fold[Expr](full, let, (_, _) => scala.sys.error("Should never happen!"))(outers)
+ }
+
+ /** Folds the path into the associated boolean proposition */
+ lazy val toClause: Expr = and(BooleanLiteral(true))
+
+ /** Like [[toClause]] but doesn't simplify final path through constructors
+ * from [[leon.purescala.Constructors]] */
+ lazy val fullClause: Expr = fold[Expr](BooleanLiteral(true), Let, And(_, _))(elements)
+
+ /** Folds the path into a boolean proposition where let-bindings are
+ * replaced by equations.
+ *
+ * CAUTION: Should only be used once INSIDE the solver!!
+ */
+ lazy val toPath: Expr = andJoin(elements.map {
+ case Left((id, e)) => Equals(id.toVariable, e)
+ case Right(e) => e
+ })
+
+ override def equals(that: Any): Boolean = that match {
+ case p: Path => elements == p.elements
+ case _ => false
+ }
+
+ override def hashCode: Int = elements.hashCode
+
+ override def toString = asString(LeonContext.printNames)
+ def asString(implicit ctx: LeonContext): String = fullClause.asString
+ def asString(pgm: Program)(implicit ctx: LeonContext): String = fullClause.asString(pgm)
+ }
+}
diff --git a/src/main/scala/inox/trees/PrettyPrinter.scala b/src/main/scala/inox/trees/PrettyPrinter.scala
deleted file mode 100644
index 1d93d9725..000000000
--- a/src/main/scala/inox/trees/PrettyPrinter.scala
+++ /dev/null
@@ -1,756 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import leon.utils._
-import Common._
-import DefOps._
-import Definitions._
-import Extractors._
-import PrinterHelpers._
-import ExprOps.{isListLiteral, simplestValue}
-import Expressions._
-import Constructors._
-import Types._
-import org.apache.commons.lang3.StringEscapeUtils
-
-case class PrinterContext(
- current: Tree,
- parents: List[Tree],
- lvl: Int,
- printer: PrettyPrinter
-) {
-
- def parent = parents.headOption
-}
-
-/** This pretty-printer uses Unicode for some operators, to make sure we
- * distinguish PureScala from "real" Scala (and also because it's cute). */
-class PrettyPrinter(opts: PrinterOptions,
- opgm: Option[Program],
- val sb: StringBuffer = new StringBuffer) {
-
- override def toString = sb.toString
-
- protected def optP(body: => Any)(implicit ctx: PrinterContext) = {
- if (requiresParentheses(ctx.current, ctx.parent)) {
- sb.append("(")
- body
- sb.append(")")
- } else {
- body
- }
- }
-
- protected def getScope(implicit ctx: PrinterContext) =
- ctx.parents.collectFirst { case (d: Definition) if !d.isInstanceOf[ValDef] => d }
-
- protected def printNameWithPath(df: Definition)(implicit ctx: PrinterContext) {
- (opgm, getScope) match {
- case (Some(pgm), Some(scope)) =>
- sb.append(fullNameFrom(df, scope, opts.printUniqueIds)(pgm))
-
- case _ =>
- p"${df.id}"
- }
- }
-
- private val dbquote = "\""
-
- def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
-
- if (requiresBraces(tree, ctx.parent) && !ctx.parent.contains(tree)) {
- p"""|{
- | $tree
- |}"""
- return
- }
-
- if (opts.printTypes) {
- tree match {
- case t: Expr =>
- p"⟨"
-
- case _ =>
- }
- }
- tree match {
- case id: Identifier =>
- val name = if (opts.printUniqueIds) {
- id.uniqueName
- } else {
- id.toString
- }
- p"$name"
-
- case Variable(id) =>
- p"$id"
-
- case Let(id, expr, SubString(Variable(id2), start, StringLength(Variable(id3)))) if id == id2 && id2 == id3 =>
- p"$expr.substring($start)"
-
- case Let(id, expr, BigSubString(Variable(id2), start, StringLength(Variable(id3)))) if id == id2 && id2 == id3 =>
- p"$expr.bigSubstring($start)"
-
- case Let(b,d,e) =>
- p"""|val $b = $d
- |$e"""
-
- case LetDef(a::q,body) =>
- p"""|$a
- |${letDef(q, body)}"""
- case LetDef(Nil,body) =>
- p"""$body"""
-
- case Require(pre, body) =>
- p"""|require($pre)
- |$body"""
-
- case Assert(const, Some(err), body) =>
- p"""|assert($const, "$err")
- |$body"""
-
- case Assert(const, None, body) =>
- p"""|assert($const)
- |$body"""
-
- case Ensuring(body, post) =>
- p"""| {
- | $body
- |} ensuring {
- | $post
- |}"""
-
- case p@Passes(in, out, tests) =>
- tests match {
- case Seq(MatchCase(_, Some(BooleanLiteral(false)), NoTree(_))) =>
- p"""|byExample($in, $out)"""
- case _ =>
- optP {
- p"""|($in, $out) passes {
- | ${nary(tests, "\n")}
- |}"""
- }
- }
-
-
- case c @ WithOracle(vars, pred) =>
- p"""|withOracle { (${typed(vars)}) =>
- | $pred
- |}"""
-
- case h @ Hole(tpe, es) =>
- if (es.isEmpty) {
- val hole = (for{scope <- getScope
- program <- opgm }
- yield simplifyPath("leon" :: "lang" :: "synthesis" :: "???" :: Nil, scope, false)(program))
- .getOrElse("leon.lang.synthesis.???")
- p"$hole[$tpe]"
- } else {
- p"?($es)"
- }
-
- case Forall(args, e) =>
- p"\u2200${typed(args.map(_.id))}. $e"
-
- case e @ CaseClass(cct, args) =>
- opgm.flatMap { pgm => isListLiteral(e)(pgm) } match {
- case Some((tpe, elems)) =>
- val chars = elems.collect{ case CharLiteral(ch) => ch }
- if (chars.length == elems.length && tpe == CharType) {
- // String literal
- val str = chars mkString ""
- val q = '"'
- p"$q$str$q"
- } else {
- val lclass = AbstractClassType(opgm.get.library.List.get, cct.tps)
-
- p"$lclass($elems)"
- }
-
- case None =>
- if (cct.classDef.isCaseObject) {
- p"$cct"
- } else {
- p"$cct($args)"
- }
- }
-
- case And(exprs) => optP { p"${nary(exprs, " && ")}" }
- case Or(exprs) => optP { p"${nary(exprs, "| || ")}" } // Ugliness award! The first | is there to shield from stripMargin()
- case Not(Equals(l, r)) => optP { p"$l \u2260 $r" }
- case Implies(l,r) => optP { p"$l ==> $r" }
- case BVNot(expr) => p"~$expr"
- case UMinus(expr) => p"-$expr"
- case BVUMinus(expr) => p"-$expr"
- case RealUMinus(expr) => p"-$expr"
- case Equals(l,r) => optP { p"$l == $r" }
-
-
- case Int32ToString(expr) => p"$expr.toString"
- case BooleanToString(expr) => p"$expr.toString"
- case IntegerToString(expr) => p"$expr.toString"
- case CharToString(expr) => p"$expr.toString"
- case RealToString(expr) => p"$expr.toString"
- case StringConcat(lhs, rhs) => optP { p"$lhs + $rhs" }
-
- case SubString(expr, start, end) => p"$expr.substring($start, $end)"
- case BigSubString(expr, start, end) => p"$expr.bigSubstring($start, $end)"
- case StringLength(expr) => p"$expr.length"
- case StringBigLength(expr) => p"$expr.bigLength"
-
- case IntLiteral(v) => p"$v"
- case InfiniteIntegerLiteral(v) => p"$v"
- case FractionalLiteral(n, d) =>
- if (d == 1) p"$n"
- else p"$n/$d"
- case CharLiteral(v) => p"$v"
- case BooleanLiteral(v) => p"$v"
- case UnitLiteral() => p"()"
- case StringLiteral(v) =>
- if(v.count(c => c == '\n') >= 1 && v.length >= 80 && v.indexOf("\"\"\"") == -1) {
- p"$dbquote$dbquote$dbquote$v$dbquote$dbquote$dbquote"
- } else {
- val escaped = StringEscapeUtils.escapeJava(v)
- p"$dbquote$escaped$dbquote"
- }
- case GenericValue(tp, id) => p"$tp#$id"
- case Tuple(exprs) => p"($exprs)"
- case TupleSelect(t, i) => p"$t._$i"
- case NoTree(tpe) => p"<empty tree>[$tpe]"
- case Choose(pred) =>
- val choose = (for{scope <- getScope
- program <- opgm }
- yield simplifyPath("leon" :: "lang" :: "synthesis" :: "choose" :: Nil, scope, false)(program))
- .getOrElse("leon.lang.synthesis.choose")
- p"$choose($pred)"
- case e @ Error(tpe, err) => p"""error[$tpe]("$err")"""
- case AsInstanceOf(e, ct) => p"""$e.asInstanceOf[$ct]"""
- case IsInstanceOf(e, cct) =>
- if (cct.classDef.isCaseObject) {
- p"($e == $cct)"
- } else {
- p"$e.isInstanceOf[$cct]"
- }
- case CaseClassSelector(_, e, id) => p"$e.$id"
- case MethodInvocation(rec, _, tfd, args) =>
- p"$rec.${tfd.id}${nary(tfd.tps, ", ", "[", "]")}"
- // No () for fields
- if (tfd.fd.isRealFunction) {
- // The non-present arguments are synthetic function invocations
- val presentArgs = args filter {
- case MethodInvocation(_, _, tfd, _) if tfd.fd.isSynthetic => false
- case FunctionInvocation(tfd, _) if tfd.fd.isSynthetic => false
- case other => true
- }
-
- val requireParens = presentArgs.nonEmpty || args.nonEmpty
- if (requireParens) {
- p"($presentArgs)"
- }
- }
-
- case BinaryMethodCall(a, op, b) =>
- optP { p"$a $op $b" }
-
- case FcallMethodInvocation(rec, fd, id, tps, args) =>
-
- p"$rec.$id${nary(tps, ", ", "[", "]")}"
-
- if (fd.isRealFunction) {
- // The non-present arguments are synthetic function invocations
- val presentArgs = args filter {
- case MethodInvocation(_, _, tfd, _) if tfd.fd.isSynthetic => false
- case FunctionInvocation(tfd, _) if tfd.fd.isSynthetic => false
- case other => true
- }
-
- val requireParens = presentArgs.nonEmpty || args.nonEmpty
- if (requireParens) {
- p"($presentArgs)"
- }
- }
-
- case FunctionInvocation(TypedFunDef(fd, tps), args) =>
- printNameWithPath(fd)
-
- p"${nary(tps, ", ", "[", "]")}"
-
- if (fd.isRealFunction) {
- // The non-present arguments are synthetic function invocations
- val presentArgs = args filter {
- case MethodInvocation(_, _, tfd, _) if tfd.fd.isSynthetic => false
- case FunctionInvocation(tfd, _) if tfd.fd.isSynthetic => false
- case other => true
- }
- val requireParens = presentArgs.nonEmpty || args.nonEmpty
- if (requireParens) {
- p"($presentArgs)"
- }
- }
-
- case Application(caller, args) =>
- p"$caller($args)"
-
- case Lambda(Seq(ValDef(id)), FunctionInvocation(TypedFunDef(fd, Seq()), Seq(Variable(idArg)))) if id == idArg =>
- printNameWithPath(fd)
-
- case Lambda(args, body) =>
- optP { p"($args) => $body" }
-
- case FiniteLambda(mapping, dflt, _) =>
- optP {
- def pm(p: (Seq[Expr], Expr)): PrinterHelpers.Printable =
- (pctx: PrinterContext) => p"${purescala.Constructors.tupleWrap(p._1)} => ${p._2}"(pctx)
-
- if (mapping.isEmpty) {
- p"{ * => ${dflt} }"
- } else {
- p"{ ${nary(mapping map pm)}, * => ${dflt} }"
- }
- }
-
- case Plus(l,r) => optP { p"$l + $r" }
- case Minus(l,r) => optP { p"$l - $r" }
- case Times(l,r) => optP { p"$l * $r" }
- case Division(l,r) => optP { p"$l / $r" }
- case Remainder(l,r) => optP { p"$l % $r" }
- case Modulo(l,r) => optP { p"$l mod $r" }
- case LessThan(l,r) => optP { p"$l < $r" }
- case GreaterThan(l,r) => optP { p"$l > $r" }
- case LessEquals(l,r) => optP { p"$l <= $r" }
- case GreaterEquals(l,r) => optP { p"$l >= $r" }
- case BVPlus(l,r) => optP { p"$l + $r" }
- case BVMinus(l,r) => optP { p"$l - $r" }
- case BVTimes(l,r) => optP { p"$l * $r" }
- case BVDivision(l,r) => optP { p"$l / $r" }
- case BVRemainder(l,r) => optP { p"$l % $r" }
- case BVAnd(l,r) => optP { p"$l & $r" }
- case BVOr(l,r) => optP { p"$l | $r" }
- case BVXOr(l,r) => optP { p"$l ^ $r" }
- case BVShiftLeft(l,r) => optP { p"$l << $r" }
- case BVAShiftRight(l,r) => optP { p"$l >> $r" }
- case BVLShiftRight(l,r) => optP { p"$l >>> $r" }
- case RealPlus(l,r) => optP { p"$l + $r" }
- case RealMinus(l,r) => optP { p"$l - $r" }
- case RealTimes(l,r) => optP { p"$l * $r" }
- case RealDivision(l,r) => optP { p"$l / $r" }
- case fs @ FiniteSet(rs, _) => p"{${rs.toSeq}}"
- case fs @ FiniteBag(rs, _) => p"{$rs}"
- case fm @ FiniteMap(rs, _, _) => p"{${rs.toSeq}}"
- case Not(ElementOfSet(e,s)) => p"$e \u2209 $s"
- case ElementOfSet(e,s) => p"$e \u2208 $s"
- case SubsetOf(l,r) => p"$l \u2286 $r"
- case Not(SubsetOf(l,r)) => p"$l \u2288 $r"
- case SetAdd(s,e) => p"$s \u222A {$e}"
- case SetUnion(l,r) => p"$l \u222A $r"
- case BagUnion(l,r) => p"$l \u222A $r"
- case MapUnion(l,r) => p"$l \u222A $r"
- case SetDifference(l,r) => p"$l \\ $r"
- case BagDifference(l,r) => p"$l \\ $r"
- case SetIntersection(l,r) => p"$l \u2229 $r"
- case BagIntersection(l,r) => p"$l \u2229 $r"
- case SetCardinality(s) => p"$s.size"
- case BagAdd(b,e) => p"$b + $e"
- case MultiplicityInBag(e, b) => p"$b($e)"
- case MapApply(m,k) => p"$m($k)"
- case MapIsDefinedAt(m,k) => p"$m.isDefinedAt($k)"
- case ArrayLength(a) => p"$a.length"
- case ArraySelect(a, i) => p"$a($i)"
- case ArrayUpdated(a, i, v) => p"$a.updated($i, $v)"
- case a@FiniteArray(es, d, s) => {
- val ArrayType(underlying) = a.getType
- val default = d.getOrElse(simplestValue(underlying))
- def ppBigArray(): Unit = {
- if(es.isEmpty) {
- p"Array($default, $default, $default, ..., $default) (of size $s)"
- } else {
- p"Array(_) (of size $s)"
- }
- }
- s match {
- case IntLiteral(length) => {
- if(es.size == length) {
- val orderedElements = es.toSeq.sortWith((e1, e2) => e1._1 < e2._1).map(el => el._2)
- p"Array($orderedElements)"
- } else if(length < 10) {
- val elems = (0 until length).map(i =>
- es.find(el => el._1 == i).map(el => el._2).getOrElse(d.get)
- )
- p"Array($elems)"
- } else {
- ppBigArray()
- }
- }
- case _ => ppBigArray()
- }
- }
-
- case Not(expr) => p"\u00AC$expr"
-
- case vd @ ValDef(id) =>
- if(vd.isVar)
- p"var "
- p"$id : ${vd.getType}"
- vd.defaultValue.foreach { fd => p" = ${fd.body.get}" }
-
- case This(_) => p"this"
- case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
- case TypeParameterDef(tp) => p"$tp"
- case TypeParameter(id) => p"$id"
-
-
- case IfExpr(c, t, ie : IfExpr) =>
- optP {
- p"""|if ($c) {
- | $t
- |} else $ie"""
- }
-
- case IfExpr(c, t, e) =>
- optP {
- p"""|if ($c) {
- | $t
- |} else {
- | $e
- |}"""
- }
-
- case LetPattern(p,s,rhs) =>
- p"""|val $p = $s
- |$rhs"""
-
- case MatchExpr(s, csc) =>
- optP {
- p"""|$s match {
- | ${nary(csc, "\n")}
- |}"""
- }
-
- // Cases
- case MatchCase(pat, optG, rhs) =>
- p"|case $pat "; optG foreach { g => p"if $g "}; p"""=>
- | $rhs"""
-
- // Patterns
- case WildcardPattern(None) => p"_"
- case WildcardPattern(Some(id)) => p"$id"
-
- case CaseClassPattern(ob, cct, subps) =>
- ob.foreach { b => p"$b @ " }
- // Print only the classDef because we don't want type parameters in patterns
- printNameWithPath(cct.classDef)
- if (!cct.classDef.isCaseObject) p"($subps)"
-
- case InstanceOfPattern(ob, cct) =>
- if (cct.classDef.isCaseObject) {
- ob.foreach { b => p"$b @ " }
- } else {
- ob.foreach { b => p"$b : " }
- }
- // It's ok to print the whole type because there are no type parameters for case objects
- p"$cct"
-
- case TuplePattern(ob, subps) =>
- ob.foreach { b => p"$b @ " }
- p"($subps)"
-
- case UnapplyPattern(ob, tfd, subps) =>
- ob.foreach { b => p"$b @ " }
-
- // @mk: I admit this is pretty ugly
- (for {
- p <- opgm
- mod <- p.modules.find( _.definedFunctions contains tfd.fd )
- } yield mod) match {
- case Some(obj) =>
- printNameWithPath(obj)
- case None =>
- p"<unknown object>"
- }
-
- p"(${nary(subps)})"
-
- case LiteralPattern(ob, lit) =>
- ob foreach { b => p"$b @ " }
- p"$lit"
-
- // Types
- case Untyped => p"<untyped>"
- case UnitType => p"Unit"
- case Int32Type => p"Int"
- case IntegerType => p"BigInt"
- case RealType => p"Real"
- case CharType => p"Char"
- case BooleanType => p"Boolean"
- case StringType => p"String"
- case ArrayType(bt) => p"Array[$bt]"
- case SetType(bt) => p"Set[$bt]"
- case BagType(bt) => p"Bag[$bt]"
- case MapType(ft,tt) => p"Map[$ft, $tt]"
- case TupleType(tpes) => p"($tpes)"
- case FunctionType(fts, tt) => p"($fts) => $tt"
- case c: ClassType =>
- printNameWithPath(c.classDef)
- p"${nary(c.tps, ", ", "[", "]")}"
-
- // Definitions
- case Program(units) =>
- p"""${nary(units filter { /*opts.printUniqueIds ||*/ _.isMainUnit }, "\n\n")}"""
-
- case UnitDef(id,pack, imports, defs,_) =>
- if (pack.nonEmpty){
- p"""|package ${pack mkString "."}
- |"""
- }
- p"""|${nary(imports,"\n")}
- |
- |${nary(defs,"\n\n")}
- |"""
-
- case Import(path, isWild) =>
- if (isWild) {
- p"import ${nary(path,".")}._"
- } else {
- p"import ${nary(path,".")}"
- }
-
- case ModuleDef(id, defs, _) =>
- p"""|object $id {
- | ${nary(defs, "\n\n")}
- |}"""
-
- case acd : AbstractClassDef =>
- p"abstract class ${acd.id}${nary(acd.tparams, ", ", "[", "]")}"
-
- acd.parent.foreach{ par =>
- p" extends ${par.id}"
- }
-
- if (acd.methods.nonEmpty) {
- p"""| {
- | ${nary(acd.methods, "\n\n")}
- |}"""
- }
-
- case ccd : CaseClassDef =>
- if (ccd.isCaseObject) {
- p"case object ${ccd.id}"
- } else {
- p"case class ${ccd.id}"
- }
-
- p"${nary(ccd.tparams, ", ", "[", "]")}"
-
- if (!ccd.isCaseObject) {
- p"(${ccd.fields})"
- }
-
- ccd.parent.foreach { par =>
- // Remember child and parents tparams are simple bijection
- p" extends ${par.id}${nary(ccd.tparams, ", ", "[", "]")}"
- }
-
- if (ccd.methods.nonEmpty) {
- p"""| {
- | ${nary(ccd.methods, "\n\n") }
- |}"""
- }
-
- case fd: FunDef =>
- for (an <- fd.annotations) {
- p"""|@$an
- |"""
- }
-
- if (fd.canBeStrictField) {
- p"val ${fd.id} : "
- } else if (fd.canBeLazyField) {
- p"lazy val ${fd.id} : "
- } else {
- p"def ${fd.id}${nary(fd.tparams, ", ", "[", "]")}(${fd.params}): "
- }
-
- p"${fd.returnType} = ${fd.fullBody}"
-
- case (tree: PrettyPrintable) => tree.printWith(ctx)
-
- case _ => sb.append("Tree? (" + tree.getClass + ")")
- }
- if (opts.printTypes) {
- tree match {
- case t: Expr=>
- p" : ${t.getType} ⟩"
-
- case _ =>
- }
- }
- if (opts.printPositions) {
- tree.getPos match {
- case op: OffsetPosition =>
- p"@($op)"
- case rp: RangePosition =>
- if (rp.lineFrom == rp.lineTo) {
- if (rp.colFrom == rp.colTo) {
- p"@(${rp.lineFrom}:${rp.colFrom})"
- } else {
- p"@(${rp.lineFrom}:${rp.colFrom}-${rp.colTo})"
- }
- } else {
- p"@(${rp.focusBegin}-${rp.focusEnd})"
- }
- case _ =>
- p"@(?)"
- }
- }
-
- }
-
- protected object FcallMethodInvocation {
- def unapply(fi: FunctionInvocation): Option[(Expr, FunDef, Identifier, Seq[TypeTree], Seq[Expr])] = {
- val FunctionInvocation(tfd, args) = fi
- tfd.fd.methodOwner.map { cd =>
- val (rec, rargs) = (args.head, args.tail)
-
- val fid = tfd.fd.id
-
- val realtps = tfd.tps.drop(cd.tparams.size)
-
- (rec, tfd.fd, fid, realtps, rargs)
- }
- }
- }
-
- protected object BinaryMethodCall {
- val makeBinary = Set("+", "-", "*", "::", "++", "--", "&&", "||", "/")
-
- def unapply(fi: FunctionInvocation): Option[(Expr, String, Expr)] = fi match {
- case FcallMethodInvocation(rec, _, id, Nil, List(a)) =>
- val name = id.name
- if (makeBinary contains name) {
- if(name == "::")
- Some((a, name, rec))
- else
- Some((rec, name, a))
- } else {
- None
- }
- case _ => None
- }
- }
-
- protected def isSimpleExpr(e: Expr): Boolean = e match {
- case _: LetDef | _: Let | LetPattern(_, _, _) | _: Assert | _: Require => false
- case p: PrettyPrintable => p.isSimpleExpr
- case _ => true
- }
-
- protected def noBracesSub(e: Expr): Seq[Expr] = e match {
- case Assert(_, _, bd) => Seq(bd)
- case Let(_, _, bd) => Seq(bd)
- case xlang.Expressions.LetVar(_, _, bd) => Seq(bd)
- case LetDef(_, bd) => Seq(bd)
- case LetPattern(_, _, bd) => Seq(bd)
- case Require(_, bd) => Seq(bd)
- case IfExpr(_, t, e) => Seq(t, e) // if-else always has braces anyway
- case Ensuring(bd, pred) => Seq(bd, pred)
- case _ => Seq()
- }
-
- protected def requiresBraces(ex: Tree, within: Option[Tree]) = (ex, within) match {
- case (e: Expr, _) if isSimpleExpr(e) => false
- case (e: Expr, Some(within: Expr)) if noBracesSub(within) contains e => false
- case (_: Expr, Some(_: MatchCase)) => false
- case (_: LetDef, Some(_: LetDef)) => false
- case (_: Expr, Some(_: xlang.Expressions.Block)) => false
- case (_: xlang.Expressions.Block, Some(_: xlang.Expressions.While)) => false
- case (_: xlang.Expressions.Block, Some(_: FunDef)) => false
- case (_: xlang.Expressions.Block, Some(_: LetDef)) => false
- case (e: Expr, Some(_)) => true
- case _ => false
- }
-
- protected def precedence(ex: Expr): Int = ex match {
- case (pa: PrettyPrintable) => pa.printPrecedence
- case (_: ElementOfSet) => 0
- case (_: Modulo) => 1
- case (_: Or | BinaryMethodCall(_, "||", _)) => 2
- case (_: And | BinaryMethodCall(_, "&&", _)) => 3
- case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan | _: Implies) => 4
- case (_: Equals | _: Not) => 5
- case (_: Plus | _: BVPlus | _: Minus | _: BVMinus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 7
- case (_: Times | _: BVTimes | _: Division | _: BVDivision | _: Remainder | _: BVRemainder | BinaryMethodCall(_, "*" | "/", _)) => 8
- case _ => 9
- }
-
- protected def requiresParentheses(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
- case (pa: PrettyPrintable, _) => pa.printRequiresParentheses(within)
- case (_, None) => false
- case (_, Some(
- _: Ensuring | _: Assert | _: Require | _: Definition | _: MatchExpr | _: MatchCase |
- _: Let | _: LetDef | _: IfExpr | _ : CaseClass | _ : Lambda | _ : Choose | _ : Tuple
- )) => false
- case (_:Pattern, _) => false
- case (ex: StringConcat, Some(_: StringConcat)) => false
- case (b1 @ BinaryMethodCall(_, _, _), Some(b2 @ BinaryMethodCall(_, _, _))) if precedence(b1) > precedence(b2) => false
- case (BinaryMethodCall(_, _, _), Some(_: FunctionInvocation)) => true
- case (_, Some(_: FunctionInvocation)) => false
- case (ie: IfExpr, _) => true
- case (me: MatchExpr, _ ) => true
- case (e1: Expr, Some(e2: Expr)) if precedence(e1) > precedence(e2) => false
- case (_, _) => true
- }
-}
-
-trait PrettyPrintable {
- self: Tree =>
-
- def printWith(implicit pctx: PrinterContext): Unit
-
- def printPrecedence: Int = 1000
- def printRequiresParentheses(within: Option[Tree]): Boolean = false
- def isSimpleExpr: Boolean = false
-}
-
-class EquivalencePrettyPrinter(opts: PrinterOptions, opgm: Option[Program]) extends PrettyPrinter(opts, opgm) {
- override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
- tree match {
- case id: Identifier =>
- p"${id.name}"
-
- case _ =>
- super.pp(tree)
- }
- }
-}
-
-abstract class PrettyPrinterFactory {
- def create(opts: PrinterOptions, opgm: Option[Program]): PrettyPrinter
-
- def apply(tree: Tree, opts: PrinterOptions = PrinterOptions(), opgm: Option[Program] = None): String = {
- val printer = create(opts, opgm)
- val ctx = PrinterContext(tree, Nil, opts.baseIndent, printer)
- printer.pp(tree)(ctx)
- printer.toString
- }
-
- def apply(tree: Tree, ctx: LeonContext): String = {
- val opts = PrinterOptions.fromContext(ctx)
- apply(tree, opts, None)
- }
-
- def apply(tree: Tree, ctx: LeonContext, pgm: Program): String = {
- val opts = PrinterOptions.fromContext(ctx)
- apply(tree, opts, Some(pgm))
- }
-
-}
-
-object PrettyPrinter extends PrettyPrinterFactory {
- def create(opts: PrinterOptions, opgm: Option[Program]) = new PrettyPrinter(opts, opgm)
-}
-
-object EquivalencePrettyPrinter extends PrettyPrinterFactory {
- def create(opts: PrinterOptions, opgm: Option[Program]) = new EquivalencePrettyPrinter(opts, opgm)
-}
diff --git a/src/main/scala/inox/trees/PrinterHelpers.scala b/src/main/scala/inox/trees/PrinterHelpers.scala
deleted file mode 100644
index 9cc470697..000000000
--- a/src/main/scala/inox/trees/PrinterHelpers.scala
+++ /dev/null
@@ -1,98 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import purescala.Common._
-import purescala.Types._
-
-object PrinterHelpers {
- implicit class Printable(val f: PrinterContext => Any) extends AnyVal {
- def print(ctx: PrinterContext) = f(ctx)
- }
-
- implicit class PrintingHelper(val sc: StringContext) extends AnyVal {
-
- def p(args: Any*)(implicit ctx: PrinterContext): Unit = {
- val printer = ctx.printer
- val sb = printer.sb
-
- val strings = sc.parts.iterator
- val expressions = args.iterator
-
- var extraInd = 0
- var firstElem = true
-
- while(strings.hasNext) {
- val currval = strings.next
- val s = if(currval != " || ") {
- currval.stripMargin
- } else currval
-
- // Compute indentation
- val start = s.lastIndexOf('\n')
- if(start >= 0 || firstElem) {
- var i = start+1
- while(i < s.length && s(i) == ' ') {
- i += 1
- }
- extraInd = (i-start-1)/2
- }
-
- firstElem = false
-
- // Make sure new lines are also indented
- sb.append(s.replaceAll("\n", "\n"+(" "*ctx.lvl)))
-
- val nctx = ctx.copy(lvl = ctx.lvl + extraInd)
-
- if (expressions.hasNext) {
- val e = expressions.next
- if(e == "||")
- println("Seen Expression: "+e)
-
- e match {
- case (t1, t2) =>
- nary(Seq(t1, t2), " -> ").print(nctx)
-
- case ts: Seq[Any] =>
- nary(ts).print(nctx)
-
- case t: Tree =>
- // Don't add same tree twice in parents
- val parents = if (nctx.parents.headOption contains nctx.current) {
- nctx.parents
- } else {
- nctx.current :: nctx.parents
- }
- val nctx2 = nctx.copy(parents = parents, current = t)
- printer.pp(t)(nctx2)
-
- case p: Printable =>
- p.print(nctx)
-
- case e =>
- sb.append(e.toString)
- }
- }
- }
- }
- }
-
- def nary(ls: Seq[Any], sep: String = ", ", init: String = "", closing: String = ""): Printable = {
- val (i, c) = if(ls.isEmpty) ("", "") else (init, closing)
- val strs = i +: List.fill(ls.size-1)(sep) :+ c
-
- implicit pctx: PrinterContext =>
- new StringContext(strs: _*).p(ls: _*)
- }
-
- def typed(t: Tree with Typed): Printable = {
- implicit pctx: PrinterContext =>
- p"$t : ${t.getType}"
- }
-
- def typed(ts: Seq[Tree with Typed]): Printable = {
- nary(ts.map(typed))
- }
-}
diff --git a/src/main/scala/inox/trees/Printers.scala b/src/main/scala/inox/trees/Printers.scala
new file mode 100644
index 000000000..460b1bdb2
--- /dev/null
+++ b/src/main/scala/inox/trees/Printers.scala
@@ -0,0 +1,835 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package trees
+
+import org.apache.commons.lang3.StringEscapeUtils
+
+trait Printers { self: Trees =>
+
+ case class PrinterContext(
+ current: Tree,
+ parents: List[Tree],
+ lvl: Int,
+ printer: PrettyPrinter) {
+
+ def parent = parents.headOption
+ }
+
+ /** This pretty-printer uses Unicode for some operators, to make sure we
+ * distinguish PureScala from "real" Scala (and also because it's cute). */
+ class PrettyPrinter(opts: PrinterOptions,
+ opgm: Option[Program],
+ val sb: StringBuffer = new StringBuffer) {
+
+ override def toString = sb.toString
+
+ protected def optP(body: => Any)(implicit ctx: PrinterContext) = {
+ if (requiresParentheses(ctx.current, ctx.parent)) {
+ sb.append("(")
+ body
+ sb.append(")")
+ } else {
+ body
+ }
+ }
+
+ protected def getScope(implicit ctx: PrinterContext) =
+ ctx.parents.collectFirst { case (d: Definition) if !d.isInstanceOf[ValDef] => d }
+
+ protected def printNameWithPath(df: Definition)(implicit ctx: PrinterContext) {
+ (opgm, getScope) match {
+ case (Some(pgm), Some(scope)) =>
+ sb.append(fullNameFrom(df, scope, opts.printUniqueIds)(pgm))
+
+ case _ =>
+ p"${df.id}"
+ }
+ }
+
+ private val dbquote = "\""
+
+ def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
+
+ if (requiresBraces(tree, ctx.parent) && !ctx.parent.contains(tree)) {
+ p"""|{
+ | $tree
+ |}"""
+ return
+ }
+
+ if (opts.printTypes) {
+ tree match {
+ case t: Expr =>
+ p"⟨"
+
+ case _ =>
+ }
+ }
+ tree match {
+ case id: Identifier =>
+ val name = if (opts.printUniqueIds) {
+ id.uniqueName
+ } else {
+ id.toString
+ }
+ p"$name"
+
+ case Variable(id) =>
+ p"$id"
+
+ case Let(id, expr, SubString(Variable(id2), start, StringLength(Variable(id3)))) if id == id2 && id2 == id3 =>
+ p"$expr.substring($start)"
+
+ case Let(id, expr, BigSubString(Variable(id2), start, StringLength(Variable(id3)))) if id == id2 && id2 == id3 =>
+ p"$expr.bigSubstring($start)"
+
+ case Let(b,d,e) =>
+ p"""|val $b = $d
+ |$e"""
+
+ case LetDef(a::q,body) =>
+ p"""|$a
+ |${letDef(q, body)}"""
+ case LetDef(Nil,body) =>
+ p"""$body"""
+
+ case Require(pre, body) =>
+ p"""|require($pre)
+ |$body"""
+
+ case Assert(const, Some(err), body) =>
+ p"""|assert($const, "$err")
+ |$body"""
+
+ case Assert(const, None, body) =>
+ p"""|assert($const)
+ |$body"""
+
+ case Ensuring(body, post) =>
+ p"""| {
+ | $body
+ |} ensuring {
+ | $post
+ |}"""
+
+ case p @ Passes(in, out, tests) =>
+ tests match {
+ case Seq(MatchCase(_, Some(BooleanLiteral(false)), NoTree(_))) =>
+ p"""|byExample($in, $out)"""
+ case _ =>
+ optP {
+ p"""|($in, $out) passes {
+ | ${nary(tests, "\n")}
+ |}"""
+ }
+ }
+
+
+ case c @ WithOracle(vars, pred) =>
+ p"""|withOracle { (${typed(vars)}) =>
+ | $pred
+ |}"""
+
+ case h @ Hole(tpe, es) =>
+ if (es.isEmpty) {
+ val hole = (for{scope <- getScope
+ program <- opgm }
+ yield simplifyPath("leon" :: "lang" :: "synthesis" :: "???" :: Nil, scope, false)(program))
+ .getOrElse("leon.lang.synthesis.???")
+ p"$hole[$tpe]"
+ } else {
+ p"?($es)"
+ }
+
+ case Forall(args, e) =>
+ p"\u2200${typed(args.map(_.id))}. $e"
+
+ case e @ CaseClass(cct, args) =>
+ opgm.flatMap { pgm => isListLiteral(e)(pgm) } match {
+ case Some((tpe, elems)) =>
+ val chars = elems.collect{ case CharLiteral(ch) => ch }
+ if (chars.length == elems.length && tpe == CharType) {
+ // String literal
+ val str = chars mkString ""
+ val q = '"'
+ p"$q$str$q"
+ } else {
+ val lclass = AbstractClassType(opgm.get.library.List.get, cct.tps)
+
+ p"$lclass($elems)"
+ }
+
+ case None =>
+ if (cct.classDef.isCaseObject) {
+ p"$cct"
+ } else {
+ p"$cct($args)"
+ }
+ }
+
+ case And(exprs) => optP { p"${nary(exprs, " && ")}" }
+ case Or(exprs) => optP { p"${nary(exprs, "| || ")}" } // Ugliness award! The first | is there to shield from stripMargin()
+ case Not(Equals(l, r)) => optP { p"$l \u2260 $r" }
+ case Implies(l,r) => optP { p"$l ==> $r" }
+ case BVNot(expr) => p"~$expr"
+ case UMinus(expr) => p"-$expr"
+ case BVUMinus(expr) => p"-$expr"
+ case RealUMinus(expr) => p"-$expr"
+ case Equals(l,r) => optP { p"$l == $r" }
+
+
+ case Int32ToString(expr) => p"$expr.toString"
+ case BooleanToString(expr) => p"$expr.toString"
+ case IntegerToString(expr) => p"$expr.toString"
+ case CharToString(expr) => p"$expr.toString"
+ case RealToString(expr) => p"$expr.toString"
+ case StringConcat(lhs, rhs) => optP { p"$lhs + $rhs" }
+
+ case SubString(expr, start, end) => p"$expr.substring($start, $end)"
+ case BigSubString(expr, start, end) => p"$expr.bigSubstring($start, $end)"
+ case StringLength(expr) => p"$expr.length"
+ case StringBigLength(expr) => p"$expr.bigLength"
+
+ case IntLiteral(v) => p"$v"
+ case InfiniteIntegerLiteral(v) => p"$v"
+ case FractionalLiteral(n, d) =>
+ if (d == 1) p"$n"
+ else p"$n/$d"
+ case CharLiteral(v) => p"$v"
+ case BooleanLiteral(v) => p"$v"
+ case UnitLiteral() => p"()"
+ case StringLiteral(v) =>
+ if(v.count(c => c == '\n') >= 1 && v.length >= 80 && v.indexOf("\"\"\"") == -1) {
+ p"$dbquote$dbquote$dbquote$v$dbquote$dbquote$dbquote"
+ } else {
+ val escaped = StringEscapeUtils.escapeJava(v)
+ p"$dbquote$escaped$dbquote"
+ }
+ case GenericValue(tp, id) => p"$tp#$id"
+ case Tuple(exprs) => p"($exprs)"
+ case TupleSelect(t, i) => p"$t._$i"
+ case NoTree(tpe) => p"<empty tree>[$tpe]"
+ case Choose(pred) =>
+ val choose = (for{scope <- getScope
+ program <- opgm }
+ yield simplifyPath("leon" :: "lang" :: "synthesis" :: "choose" :: Nil, scope, false)(program))
+ .getOrElse("leon.lang.synthesis.choose")
+ p"$choose($pred)"
+ case e @ Error(tpe, err) => p"""error[$tpe]("$err")"""
+ case AsInstanceOf(e, ct) => p"""$e.asInstanceOf[$ct]"""
+ case IsInstanceOf(e, cct) =>
+ if (cct.classDef.isCaseObject) {
+ p"($e == $cct)"
+ } else {
+ p"$e.isInstanceOf[$cct]"
+ }
+ case CaseClassSelector(_, e, id) => p"$e.$id"
+ case MethodInvocation(rec, _, tfd, args) =>
+ p"$rec.${tfd.id}${nary(tfd.tps, ", ", "[", "]")}"
+ // No () for fields
+ if (tfd.fd.isRealFunction) {
+ // The non-present arguments are synthetic function invocations
+ val presentArgs = args filter {
+ case MethodInvocation(_, _, tfd, _) if tfd.fd.isSynthetic => false
+ case FunctionInvocation(tfd, _) if tfd.fd.isSynthetic => false
+ case other => true
+ }
+
+ val requireParens = presentArgs.nonEmpty || args.nonEmpty
+ if (requireParens) {
+ p"($presentArgs)"
+ }
+ }
+
+ case BinaryMethodCall(a, op, b) =>
+ optP { p"$a $op $b" }
+
+ case FcallMethodInvocation(rec, fd, id, tps, args) =>
+
+ p"$rec.$id${nary(tps, ", ", "[", "]")}"
+
+ if (fd.isRealFunction) {
+ // The non-present arguments are synthetic function invocations
+ val presentArgs = args filter {
+ case MethodInvocation(_, _, tfd, _) if tfd.fd.isSynthetic => false
+ case FunctionInvocation(tfd, _) if tfd.fd.isSynthetic => false
+ case other => true
+ }
+
+ val requireParens = presentArgs.nonEmpty || args.nonEmpty
+ if (requireParens) {
+ p"($presentArgs)"
+ }
+ }
+
+ case FunctionInvocation(TypedFunDef(fd, tps), args) =>
+ printNameWithPath(fd)
+
+ p"${nary(tps, ", ", "[", "]")}"
+
+ if (fd.isRealFunction) {
+ // The non-present arguments are synthetic function invocations
+ val presentArgs = args filter {
+ case MethodInvocation(_, _, tfd, _) if tfd.fd.isSynthetic => false
+ case FunctionInvocation(tfd, _) if tfd.fd.isSynthetic => false
+ case other => true
+ }
+ val requireParens = presentArgs.nonEmpty || args.nonEmpty
+ if (requireParens) {
+ p"($presentArgs)"
+ }
+ }
+
+ case Application(caller, args) =>
+ p"$caller($args)"
+
+ case Lambda(Seq(ValDef(id)), FunctionInvocation(TypedFunDef(fd, Seq()), Seq(Variable(idArg)))) if id == idArg =>
+ printNameWithPath(fd)
+
+ case Lambda(args, body) =>
+ optP { p"($args) => $body" }
+
+ case FiniteLambda(mapping, dflt, _) =>
+ optP {
+ def pm(p: (Seq[Expr], Expr)): PrinterHelpers.Printable =
+ (pctx: PrinterContext) => p"${purescala.Constructors.tupleWrap(p._1)} => ${p._2}"(pctx)
+
+ if (mapping.isEmpty) {
+ p"{ * => ${dflt} }"
+ } else {
+ p"{ ${nary(mapping map pm)}, * => ${dflt} }"
+ }
+ }
+
+ case Plus(l,r) => optP { p"$l + $r" }
+ case Minus(l,r) => optP { p"$l - $r" }
+ case Times(l,r) => optP { p"$l * $r" }
+ case Division(l,r) => optP { p"$l / $r" }
+ case Remainder(l,r) => optP { p"$l % $r" }
+ case Modulo(l,r) => optP { p"$l mod $r" }
+ case LessThan(l,r) => optP { p"$l < $r" }
+ case GreaterThan(l,r) => optP { p"$l > $r" }
+ case LessEquals(l,r) => optP { p"$l <= $r" }
+ case GreaterEquals(l,r) => optP { p"$l >= $r" }
+ case BVPlus(l,r) => optP { p"$l + $r" }
+ case BVMinus(l,r) => optP { p"$l - $r" }
+ case BVTimes(l,r) => optP { p"$l * $r" }
+ case BVDivision(l,r) => optP { p"$l / $r" }
+ case BVRemainder(l,r) => optP { p"$l % $r" }
+ case BVAnd(l,r) => optP { p"$l & $r" }
+ case BVOr(l,r) => optP { p"$l | $r" }
+ case BVXOr(l,r) => optP { p"$l ^ $r" }
+ case BVShiftLeft(l,r) => optP { p"$l << $r" }
+ case BVAShiftRight(l,r) => optP { p"$l >> $r" }
+ case BVLShiftRight(l,r) => optP { p"$l >>> $r" }
+ case RealPlus(l,r) => optP { p"$l + $r" }
+ case RealMinus(l,r) => optP { p"$l - $r" }
+ case RealTimes(l,r) => optP { p"$l * $r" }
+ case RealDivision(l,r) => optP { p"$l / $r" }
+ case fs @ FiniteSet(rs, _) => p"{${rs.toSeq}}"
+ case fs @ FiniteBag(rs, _) => p"{$rs}"
+ case fm @ FiniteMap(rs, _, _) => p"{${rs.toSeq}}"
+ case Not(ElementOfSet(e,s)) => p"$e \u2209 $s"
+ case ElementOfSet(e,s) => p"$e \u2208 $s"
+ case SubsetOf(l,r) => p"$l \u2286 $r"
+ case Not(SubsetOf(l,r)) => p"$l \u2288 $r"
+ case SetAdd(s,e) => p"$s \u222A {$e}"
+ case SetUnion(l,r) => p"$l \u222A $r"
+ case BagUnion(l,r) => p"$l \u222A $r"
+ case MapUnion(l,r) => p"$l \u222A $r"
+ case SetDifference(l,r) => p"$l \\ $r"
+ case BagDifference(l,r) => p"$l \\ $r"
+ case SetIntersection(l,r) => p"$l \u2229 $r"
+ case BagIntersection(l,r) => p"$l \u2229 $r"
+ case SetCardinality(s) => p"$s.size"
+ case BagAdd(b,e) => p"$b + $e"
+ case MultiplicityInBag(e, b) => p"$b($e)"
+ case MapApply(m,k) => p"$m($k)"
+ case MapIsDefinedAt(m,k) => p"$m.isDefinedAt($k)"
+ case ArrayLength(a) => p"$a.length"
+ case ArraySelect(a, i) => p"$a($i)"
+ case ArrayUpdated(a, i, v) => p"$a.updated($i, $v)"
+ case a@FiniteArray(es, d, s) => {
+ val ArrayType(underlying) = a.getType
+ val default = d.getOrElse(simplestValue(underlying))
+ def ppBigArray(): Unit = {
+ if(es.isEmpty) {
+ p"Array($default, $default, $default, ..., $default) (of size $s)"
+ } else {
+ p"Array(_) (of size $s)"
+ }
+ }
+ s match {
+ case IntLiteral(length) => {
+ if(es.size == length) {
+ val orderedElements = es.toSeq.sortWith((e1, e2) => e1._1 < e2._1).map(el => el._2)
+ p"Array($orderedElements)"
+ } else if(length < 10) {
+ val elems = (0 until length).map(i =>
+ es.find(el => el._1 == i).map(el => el._2).getOrElse(d.get)
+ )
+ p"Array($elems)"
+ } else {
+ ppBigArray()
+ }
+ }
+ case _ => ppBigArray()
+ }
+ }
+
+ case Not(expr) => p"\u00AC$expr"
+
+ case vd @ ValDef(id) =>
+ if(vd.isVar)
+ p"var "
+ p"$id : ${vd.getType}"
+ vd.defaultValue.foreach { fd => p" = ${fd.body.get}" }
+
+ case This(_) => p"this"
+ case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
+ case TypeParameterDef(tp) => p"$tp"
+ case TypeParameter(id) => p"$id"
+
+
+ case IfExpr(c, t, ie : IfExpr) =>
+ optP {
+ p"""|if ($c) {
+ | $t
+ |} else $ie"""
+ }
+
+ case IfExpr(c, t, e) =>
+ optP {
+ p"""|if ($c) {
+ | $t
+ |} else {
+ | $e
+ |}"""
+ }
+
+ case LetPattern(p,s,rhs) =>
+ p"""|val $p = $s
+ |$rhs"""
+
+ case MatchExpr(s, csc) =>
+ optP {
+ p"""|$s match {
+ | ${nary(csc, "\n")}
+ |}"""
+ }
+
+ // Cases
+ case MatchCase(pat, optG, rhs) =>
+ p"|case $pat "; optG foreach { g => p"if $g "}; p"""=>
+ | $rhs"""
+
+ // Patterns
+ case WildcardPattern(None) => p"_"
+ case WildcardPattern(Some(id)) => p"$id"
+
+ case CaseClassPattern(ob, cct, subps) =>
+ ob.foreach { b => p"$b @ " }
+ // Print only the classDef because we don't want type parameters in patterns
+ printNameWithPath(cct.classDef)
+ if (!cct.classDef.isCaseObject) p"($subps)"
+
+ case InstanceOfPattern(ob, cct) =>
+ if (cct.classDef.isCaseObject) {
+ ob.foreach { b => p"$b @ " }
+ } else {
+ ob.foreach { b => p"$b : " }
+ }
+ // It's ok to print the whole type because there are no type parameters for case objects
+ p"$cct"
+
+ case TuplePattern(ob, subps) =>
+ ob.foreach { b => p"$b @ " }
+ p"($subps)"
+
+ case UnapplyPattern(ob, tfd, subps) =>
+ ob.foreach { b => p"$b @ " }
+
+ // @mk: I admit this is pretty ugly
+ (for {
+ p <- opgm
+ mod <- p.modules.find( _.definedFunctions contains tfd.fd )
+ } yield mod) match {
+ case Some(obj) =>
+ printNameWithPath(obj)
+ case None =>
+ p"<unknown object>"
+ }
+
+ p"(${nary(subps)})"
+
+ case LiteralPattern(ob, lit) =>
+ ob foreach { b => p"$b @ " }
+ p"$lit"
+
+ // Types
+ case Untyped => p"<untyped>"
+ case UnitType => p"Unit"
+ case Int32Type => p"Int"
+ case IntegerType => p"BigInt"
+ case RealType => p"Real"
+ case CharType => p"Char"
+ case BooleanType => p"Boolean"
+ case StringType => p"String"
+ case ArrayType(bt) => p"Array[$bt]"
+ case SetType(bt) => p"Set[$bt]"
+ case BagType(bt) => p"Bag[$bt]"
+ case MapType(ft,tt) => p"Map[$ft, $tt]"
+ case TupleType(tpes) => p"($tpes)"
+ case FunctionType(fts, tt) => p"($fts) => $tt"
+ case c: ClassType =>
+ printNameWithPath(c.classDef)
+ p"${nary(c.tps, ", ", "[", "]")}"
+
+ // Definitions
+ case Program(units) =>
+ p"""${nary(units filter { /*opts.printUniqueIds ||*/ _.isMainUnit }, "\n\n")}"""
+
+ case UnitDef(id,pack, imports, defs,_) =>
+ if (pack.nonEmpty){
+ p"""|package ${pack mkString "."}
+ |"""
+ }
+ p"""|${nary(imports,"\n")}
+ |
+ |${nary(defs,"\n\n")}
+ |"""
+
+ case Import(path, isWild) =>
+ if (isWild) {
+ p"import ${nary(path,".")}._"
+ } else {
+ p"import ${nary(path,".")}"
+ }
+
+ case ModuleDef(id, defs, _) =>
+ p"""|object $id {
+ | ${nary(defs, "\n\n")}
+ |}"""
+
+ case acd : AbstractClassDef =>
+ p"abstract class ${acd.id}${nary(acd.tparams, ", ", "[", "]")}"
+
+ acd.parent.foreach{ par =>
+ p" extends ${par.id}"
+ }
+
+ if (acd.methods.nonEmpty) {
+ p"""| {
+ | ${nary(acd.methods, "\n\n")}
+ |}"""
+ }
+
+ case ccd : CaseClassDef =>
+ if (ccd.isCaseObject) {
+ p"case object ${ccd.id}"
+ } else {
+ p"case class ${ccd.id}"
+ }
+
+ p"${nary(ccd.tparams, ", ", "[", "]")}"
+
+ if (!ccd.isCaseObject) {
+ p"(${ccd.fields})"
+ }
+
+ ccd.parent.foreach { par =>
+ // Remember child and parents tparams are simple bijection
+ p" extends ${par.id}${nary(ccd.tparams, ", ", "[", "]")}"
+ }
+
+ if (ccd.methods.nonEmpty) {
+ p"""| {
+ | ${nary(ccd.methods, "\n\n") }
+ |}"""
+ }
+
+ case fd: FunDef =>
+ for (an <- fd.annotations) {
+ p"""|@$an
+ |"""
+ }
+
+ if (fd.canBeStrictField) {
+ p"val ${fd.id} : "
+ } else if (fd.canBeLazyField) {
+ p"lazy val ${fd.id} : "
+ } else {
+ p"def ${fd.id}${nary(fd.tparams, ", ", "[", "]")}(${fd.params}): "
+ }
+
+ p"${fd.returnType} = ${fd.fullBody}"
+
+ case (tree: PrettyPrintable) => tree.printWith(ctx)
+
+ case _ => sb.append("Tree? (" + tree.getClass + ")")
+ }
+ if (opts.printTypes) {
+ tree match {
+ case t: Expr=>
+ p" : ${t.getType} ⟩"
+
+ case _ =>
+ }
+ }
+ if (opts.printPositions) {
+ tree.getPos match {
+ case op: OffsetPosition =>
+ p"@($op)"
+ case rp: RangePosition =>
+ if (rp.lineFrom == rp.lineTo) {
+ if (rp.colFrom == rp.colTo) {
+ p"@(${rp.lineFrom}:${rp.colFrom})"
+ } else {
+ p"@(${rp.lineFrom}:${rp.colFrom}-${rp.colTo})"
+ }
+ } else {
+ p"@(${rp.focusBegin}-${rp.focusEnd})"
+ }
+ case _ =>
+ p"@(?)"
+ }
+ }
+ }
+
+ protected object FcallMethodInvocation {
+ def unapply(fi: FunctionInvocation): Option[(Expr, FunDef, Identifier, Seq[TypeTree], Seq[Expr])] = {
+ val FunctionInvocation(tfd, args) = fi
+ tfd.fd.methodOwner.map { cd =>
+ val (rec, rargs) = (args.head, args.tail)
+
+ val fid = tfd.fd.id
+
+ val realtps = tfd.tps.drop(cd.tparams.size)
+
+ (rec, tfd.fd, fid, realtps, rargs)
+ }
+ }
+ }
+
+ protected object BinaryMethodCall {
+ val makeBinary = Set("+", "-", "*", "::", "++", "--", "&&", "||", "/")
+
+ def unapply(fi: FunctionInvocation): Option[(Expr, String, Expr)] = fi match {
+ case FcallMethodInvocation(rec, _, id, Nil, List(a)) =>
+ val name = id.name
+ if (makeBinary contains name) {
+ if(name == "::")
+ Some((a, name, rec))
+ else
+ Some((rec, name, a))
+ } else {
+ None
+ }
+ case _ => None
+ }
+ }
+
+ protected def isSimpleExpr(e: Expr): Boolean = e match {
+ case _: LetDef | _: Let | LetPattern(_, _, _) | _: Assert | _: Require => false
+ case p: PrettyPrintable => p.isSimpleExpr
+ case _ => true
+ }
+
+ protected def noBracesSub(e: Expr): Seq[Expr] = e match {
+ case Assert(_, _, bd) => Seq(bd)
+ case Let(_, _, bd) => Seq(bd)
+ case xlang.Expressions.LetVar(_, _, bd) => Seq(bd)
+ case LetDef(_, bd) => Seq(bd)
+ case LetPattern(_, _, bd) => Seq(bd)
+ case Require(_, bd) => Seq(bd)
+ case IfExpr(_, t, e) => Seq(t, e) // if-else always has braces anyway
+ case Ensuring(bd, pred) => Seq(bd, pred)
+ case _ => Seq()
+ }
+
+ protected def requiresBraces(ex: Tree, within: Option[Tree]) = (ex, within) match {
+ case (e: Expr, _) if isSimpleExpr(e) => false
+ case (e: Expr, Some(within: Expr)) if noBracesSub(within) contains e => false
+ case (_: Expr, Some(_: MatchCase)) => false
+ case (_: LetDef, Some(_: LetDef)) => false
+ case (_: Expr, Some(_: xlang.Expressions.Block)) => false
+ case (_: xlang.Expressions.Block, Some(_: xlang.Expressions.While)) => false
+ case (_: xlang.Expressions.Block, Some(_: FunDef)) => false
+ case (_: xlang.Expressions.Block, Some(_: LetDef)) => false
+ case (e: Expr, Some(_)) => true
+ case _ => false
+ }
+
+ protected def precedence(ex: Expr): Int = ex match {
+ case (pa: PrettyPrintable) => pa.printPrecedence
+ case (_: ElementOfSet) => 0
+ case (_: Modulo) => 1
+ case (_: Or | BinaryMethodCall(_, "||", _)) => 2
+ case (_: And | BinaryMethodCall(_, "&&", _)) => 3
+ case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan | _: Implies) => 4
+ case (_: Equals | _: Not) => 5
+ case (_: Plus | _: BVPlus | _: Minus | _: BVMinus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 7
+ case (_: Times | _: BVTimes | _: Division | _: BVDivision | _: Remainder | _: BVRemainder | BinaryMethodCall(_, "*" | "/", _)) => 8
+ case _ => 9
+ }
+
+ protected def requiresParentheses(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
+ case (pa: PrettyPrintable, _) => pa.printRequiresParentheses(within)
+ case (_, None) => false
+ case (_, Some(
+ _: Ensuring | _: Assert | _: Require | _: Definition | _: MatchExpr | _: MatchCase |
+ _: Let | _: LetDef | _: IfExpr | _ : CaseClass | _ : Lambda | _ : Choose | _ : Tuple
+ )) => false
+ case (_:Pattern, _) => false
+ case (ex: StringConcat, Some(_: StringConcat)) => false
+ case (b1 @ BinaryMethodCall(_, _, _), Some(b2 @ BinaryMethodCall(_, _, _))) if precedence(b1) > precedence(b2) => false
+ case (BinaryMethodCall(_, _, _), Some(_: FunctionInvocation)) => true
+ case (_, Some(_: FunctionInvocation)) => false
+ case (ie: IfExpr, _) => true
+ case (me: MatchExpr, _ ) => true
+ case (e1: Expr, Some(e2: Expr)) if precedence(e1) > precedence(e2) => false
+ case (_, _) => true
+ }
+ }
+
+ implicit class Printable(val f: PrinterContext => Any) extends AnyVal {
+ def print(ctx: PrinterContext) = f(ctx)
+ }
+
+ implicit class PrintingHelper(val sc: StringContext) extends AnyVal {
+
+ def p(args: Any*)(implicit ctx: PrinterContext): Unit = {
+ val printer = ctx.printer
+ val sb = printer.sb
+
+ val strings = sc.parts.iterator
+ val expressions = args.iterator
+
+ var extraInd = 0
+ var firstElem = true
+
+ while(strings.hasNext) {
+ val currval = strings.next
+ val s = if(currval != " || ") {
+ currval.stripMargin
+ } else currval
+
+ // Compute indentation
+ val start = s.lastIndexOf('\n')
+ if(start >= 0 || firstElem) {
+ var i = start+1
+ while(i < s.length && s(i) == ' ') {
+ i += 1
+ }
+ extraInd = (i-start-1)/2
+ }
+
+ firstElem = false
+
+ // Make sure new lines are also indented
+ sb.append(s.replaceAll("\n", "\n"+(" "*ctx.lvl)))
+
+ val nctx = ctx.copy(lvl = ctx.lvl + extraInd)
+
+ if (expressions.hasNext) {
+ val e = expressions.next
+ if(e == "||")
+ println("Seen Expression: "+e)
+
+ e match {
+ case (t1, t2) =>
+ nary(Seq(t1, t2), " -> ").print(nctx)
+
+ case ts: Seq[Any] =>
+ nary(ts).print(nctx)
+
+ case t: Tree =>
+ // Don't add same tree twice in parents
+ val parents = if (nctx.parents.headOption contains nctx.current) {
+ nctx.parents
+ } else {
+ nctx.current :: nctx.parents
+ }
+ val nctx2 = nctx.copy(parents = parents, current = t)
+ printer.pp(t)(nctx2)
+
+ case p: Printable =>
+ p.print(nctx)
+
+ case e =>
+ sb.append(e.toString)
+ }
+ }
+ }
+ }
+ }
+
+ def nary(ls: Seq[Any], sep: String = ", ", init: String = "", closing: String = ""): Printable = {
+ val (i, c) = if(ls.isEmpty) ("", "") else (init, closing)
+ val strs = i +: List.fill(ls.size-1)(sep) :+ c
+
+ implicit pctx: PrinterContext =>
+ new StringContext(strs: _*).p(ls: _*)
+ }
+
+ def typed(t: Tree with Typed): Printable = {
+ implicit pctx: PrinterContext =>
+ p"$t : ${t.getType}"
+ }
+
+ def typed(ts: Seq[Tree with Typed]): Printable = {
+ nary(ts.map(typed))
+ }
+
+ trait PrettyPrintable {
+ self: Tree =>
+
+ def printWith(implicit pctx: PrinterContext): Unit
+
+ def printPrecedence: Int = 1000
+ def printRequiresParentheses(within: Option[Tree]): Boolean = false
+ def isSimpleExpr: Boolean = false
+ }
+
+ class EquivalencePrettyPrinter(opts: PrinterOptions, opgm: Option[Program]) extends PrettyPrinter(opts, opgm) {
+ override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
+ tree match {
+ case id: Identifier =>
+ p"${id.name}"
+
+ case _ =>
+ super.pp(tree)
+ }
+ }
+ }
+
+ abstract class PrettyPrinterFactory {
+ def create(opts: PrinterOptions, opgm: Option[Program]): PrettyPrinter
+
+ def apply(tree: Tree, opts: PrinterOptions = PrinterOptions(), opgm: Option[Program] = None): String = {
+ val printer = create(opts, opgm)
+ val ctx = PrinterContext(tree, Nil, opts.baseIndent, printer)
+ printer.pp(tree)(ctx)
+ printer.toString
+ }
+
+ def apply(tree: Tree, ctx: LeonContext): String = {
+ val opts = PrinterOptions.fromContext(ctx)
+ apply(tree, opts, None)
+ }
+
+ def apply(tree: Tree, ctx: LeonContext, pgm: Program): String = {
+ val opts = PrinterOptions.fromContext(ctx)
+ apply(tree, opts, Some(pgm))
+ }
+ }
+
+ object PrettyPrinter extends PrettyPrinterFactory {
+ def create(opts: PrinterOptions, opgm: Option[Program]) = new PrettyPrinter(opts, opgm)
+ }
+
+ object EquivalencePrettyPrinter extends PrettyPrinterFactory {
+ def create(opts: PrinterOptions, opgm: Option[Program]) = new EquivalencePrettyPrinter(opts, opgm)
+ }
+}
diff --git a/src/main/scala/inox/trees/Transformer.scala b/src/main/scala/inox/trees/Transformer.scala
deleted file mode 100644
index c44d56a67..000000000
--- a/src/main/scala/inox/trees/Transformer.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import purescala.Expressions.Expr
-
-trait Transformer {
- def transform(e: Expr): Expr
-}
diff --git a/src/main/scala/inox/trees/TransformerWithPC.scala b/src/main/scala/inox/trees/TransformerWithPC.scala
deleted file mode 100644
index 2408757a6..000000000
--- a/src/main/scala/inox/trees/TransformerWithPC.scala
+++ /dev/null
@@ -1,101 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import Expressions._
-import Constructors._
-import Extractors._
-import ExprOps._
-
-/** Traverses expressions with path condition awareness.
- *
- * As lets cannot be encoded as Equals due to types for which equality
- * is not well-founded, path conditions reconstruct lets around the
- * final condition one wishes to verify through [[Path.getClause]].
- */
-abstract class TraverserWithPaths[T](trees: Trees) {
- import trees._
-
- protected def rec(e: Expr, path: Path): Unit = e match {
- case Let(i, v, b) =>
- val se = rec(v, path)
- val sb = rec(b, path withBinding (i -> se))
- Let(i, se, sb).copiedFrom(e)
-
- case Ensuring(req @ Require(pre, body), lam @ Lambda(Seq(arg), post)) =>
- val spre = rec(pre, path)
- val sbody = rec(body, path withCond spre)
- val spost = rec(post, path withCond spre withBinding (arg.id -> sbody))
- Ensuring(
- Require(spre, sbody).copiedFrom(req),
- Lambda(Seq(arg), spost).copiedFrom(lam)
- ).copiedFrom(e)
-
- case Ensuring(body, lam @ Lambda(Seq(arg), post)) =>
- val sbody = rec(body, path)
- val spost = rec(post, path withBinding (arg.id -> sbody))
- Ensuring(
- sbody,
- Lambda(Seq(arg), spost).copiedFrom(lam)
- ).copiedFrom(e)
-
- case Require(pre, body) =>
- val sp = rec(pre, path)
- val sb = rec(body, path withCond pre)
- Require(sp, sb).copiedFrom(e)
-
- case Assert(pred, err, body) =>
- val sp = rec(pred, path)
- val sb = rec(body, register(sp, path))
- Assert(sp, err, sb).copiedFrom(e)
-
- case MatchExpr(scrut, cases) =>
- val rs = rec(scrut, path)
- var soFar = path
-
- MatchExpr(rs, cases.map { c =>
- val patternPathPos = conditionForPattern(rs, c.pattern, includeBinders = true)
- val patternPathNeg = conditionForPattern(rs, c.pattern, includeBinders = false)
- val map = mapForPattern(rs, c.pattern)
- val guardOrTrue = c.optGuard.getOrElse(BooleanLiteral(true))
- val guardMapped = replaceFromIDs(map, guardOrTrue)
-
- val subPath = soFar merge (patternPathPos withCond guardOrTrue)
- soFar = soFar merge (patternPathNeg withCond guardMapped).negate
-
- MatchCase(c.pattern, c.optGuard, rec(c.rhs, subPath)).copiedFrom(c)
- }).copiedFrom(e)
-
- case IfExpr(cond, thenn, elze) =>
- val rc = rec(cond, path)
- IfExpr(rc, rec(thenn, path withCond rc), rec(elze, path withCond Not(rc))).copiedFrom(e)
-
- case And(es) =>
- var soFar = path
- andJoin(for(e <- es) yield {
- val se = rec(e, soFar)
- soFar = soFar withCond se
- se
- }).copiedFrom(e)
-
- case Or(es) =>
- var soFar = path
- orJoin(for(e <- es) yield {
- val se = rec(e, soFar)
- soFar = soFar withCond Not(se)
- se
- }).copiedFrom(e)
-
- case i @ Implies(lhs, rhs) =>
- val rc = rec(lhs, path)
- Implies(rc, rec(rhs, path withCond rc)).copiedFrom(i)
-
- case o @ Operator(es, builder) =>
- builder(es.map(rec(_, path))).copiedFrom(o)
-
- case _ =>
- sys.error("Expression "+e+" ["+e.getClass+"] is not extractable")
- }
-}
-
diff --git a/src/main/scala/inox/trees/TreeTransformer.scala b/src/main/scala/inox/trees/TreeTransformer.scala
deleted file mode 100644
index a1f6e2ad6..000000000
--- a/src/main/scala/inox/trees/TreeTransformer.scala
+++ /dev/null
@@ -1,242 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import Common._
-import Definitions._
-import Expressions._
-import xlang.Expressions._
-import Extractors._
-import Types._
-
-import utils._
-import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
-
-trait TreeTransformer {
- def transform(id: Identifier): Identifier = id
- def transform(cd: ClassDef): ClassDef = cd
- def transform(fd: FunDef): FunDef = fd
-
- def transform(e: Expr)(implicit bindings: Map[Identifier, Identifier]): Expr = e match {
- case Variable(id) if bindings contains id => Variable(bindings(id)).copiedFrom(e)
- case Variable(id) => Variable(transform(id)).copiedFrom(e)
- case FiniteLambda(mappings, default, tpe) =>
- FiniteLambda(mappings.map { case (ks, v) => (ks map transform, transform(v)) },
- transform(default), transform(tpe).asInstanceOf[FunctionType]).copiedFrom(e)
- case Lambda(args, body) =>
- val newArgs = args.map(vd => ValDef(transform(vd.id)))
- val newBindings = (args zip newArgs).map(p => p._1.id -> p._2.id)
- Lambda(newArgs, transform(body)(bindings ++ newBindings)).copiedFrom(e)
- case Forall(args, body) =>
- val newArgs = args.map(vd => ValDef(transform(vd.id)))
- val newBindings = (args zip newArgs).map(p => p._1.id -> p._2.id)
- Forall(newArgs, transform(body)(bindings ++ newBindings)).copiedFrom(e)
- case Let(a, expr, body) =>
- val newA = transform(a)
- Let(newA, transform(expr), transform(body)(bindings + (a -> newA))).copiedFrom(e)
- case LetVar(a, expr, body) =>
- val newA = transform(a)
- LetVar(newA, transform(expr), transform(body)(bindings + (a -> newA))).copiedFrom(e)
- case LetDef(fds, body) =>
- val rFds = fds map transform
- val rBody = transform(body)
- LetDef(rFds, rBody).copiedFrom(e)
- case CaseClass(cct, args) =>
- CaseClass(transform(cct).asInstanceOf[CaseClassType], args map transform).copiedFrom(e)
- case CaseClassSelector(cct, caseClass, selector) =>
- val newCct @ CaseClassType(ccd, _) = transform(cct)
- val newSelector = ccd.fieldsIds(cct.classDef.fieldsIds.indexOf(selector))
- CaseClassSelector(newCct, transform(caseClass), newSelector).copiedFrom(e)
- case FunctionInvocation(TypedFunDef(fd, tpes), args) =>
- FunctionInvocation(TypedFunDef(transform(fd), tpes map transform), args map transform).copiedFrom(e)
- case MethodInvocation(rec, cd, TypedFunDef(fd, tpes), args) =>
- MethodInvocation(transform(rec), transform(cd), TypedFunDef(transform(fd), tpes map transform), args map transform).copiedFrom(e)
- case This(ct) =>
- This(transform(ct).asInstanceOf[ClassType]).copiedFrom(e)
- case IsInstanceOf(expr, ct) =>
- IsInstanceOf(transform(expr), transform(ct).asInstanceOf[ClassType]).copiedFrom(e)
- case AsInstanceOf(expr, ct) =>
- AsInstanceOf(transform(expr), transform(ct).asInstanceOf[ClassType]).copiedFrom(e)
- case MatchExpr(scrutinee, cases) =>
- MatchExpr(transform(scrutinee), for (cse @ MatchCase(pattern, guard, rhs) <- cases) yield {
- val (newPattern, newBindings) = transform(pattern)
- val allBindings = bindings ++ newBindings
- MatchCase(newPattern, guard.map(g => transform(g)(allBindings)), transform(rhs)(allBindings)).copiedFrom(cse)
- }).copiedFrom(e)
- case Passes(in, out, cases) =>
- Passes(transform(in), transform(out), for (cse @ MatchCase(pattern, guard, rhs) <- cases) yield {
- val (newPattern, newBindings) = transform(pattern)
- val allBindings = bindings ++ newBindings
- MatchCase(newPattern, guard.map(g => transform(g)(allBindings)), transform(rhs)(allBindings)).copiedFrom(cse)
- }).copiedFrom(e)
- case FiniteSet(es, tpe) =>
- FiniteSet(es map transform, transform(tpe)).copiedFrom(e)
- case FiniteBag(es, tpe) =>
- FiniteBag(es map { case (k, v) => transform(k) -> v }, transform(tpe)).copiedFrom(e)
- case FiniteMap(pairs, from, to) =>
- FiniteMap(pairs map { case (k, v) => transform(k) -> transform(v) }, transform(from), transform(to)).copiedFrom(e)
- case EmptyArray(tpe) =>
- EmptyArray(transform(tpe)).copiedFrom(e)
- case Hole(tpe, alts) =>
- Hole(transform(tpe), alts map transform).copiedFrom(e)
- case NoTree(tpe) =>
- NoTree(transform(tpe)).copiedFrom(e)
- case Error(tpe, desc) =>
- Error(transform(tpe), desc).copiedFrom(e)
- case Operator(es, builder) =>
- val newEs = es map transform
- if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
- builder(newEs).copiedFrom(e)
- } else {
- e
- }
- case e => e
- }
-
- def transform(pat: Pattern): (Pattern, Map[Identifier, Identifier]) = pat match {
- case InstanceOfPattern(binder, ct) =>
- val newBinder = binder map transform
- val newPat = InstanceOfPattern(newBinder, transform(ct).asInstanceOf[ClassType]).copiedFrom(pat)
- (newPat, (binder zip newBinder).toMap)
- case WildcardPattern(binder) =>
- val newBinder = binder map transform
- val newPat = WildcardPattern(newBinder).copiedFrom(pat)
- (newPat, (binder zip newBinder).toMap)
- case CaseClassPattern(binder, ct, subs) =>
- val newBinder = binder map transform
- val (newSubs, subBinders) = (subs map transform).unzip
- val newPat = CaseClassPattern(newBinder, transform(ct).asInstanceOf[CaseClassType], newSubs).copiedFrom(pat)
- (newPat, (binder zip newBinder).toMap ++ subBinders.flatten)
- case TuplePattern(binder, subs) =>
- val newBinder = binder map transform
- val (newSubs, subBinders) = (subs map transform).unzip
- val newPat = TuplePattern(newBinder, newSubs).copiedFrom(pat)
- (newPat, (binder zip newBinder).toMap ++ subBinders.flatten)
- case UnapplyPattern(binder, TypedFunDef(fd, tpes), subs) =>
- val newBinder = binder map transform
- val (newSubs, subBinders) = (subs map transform).unzip
- val newPat = UnapplyPattern(newBinder, TypedFunDef(transform(fd), tpes map transform), newSubs).copiedFrom(pat)
- (newPat, (binder zip newBinder).toMap ++ subBinders.flatten)
- case PatternExtractor(subs, builder) =>
- val (newSubs, subBinders) = (subs map transform).unzip
- (builder(newSubs).copiedFrom(pat), subBinders.flatten.toMap)
- }
-
- def transform(tpe: TypeTree): TypeTree = tpe match {
- case cct @ CaseClassType(ccd, args) =>
- CaseClassType(transform(ccd).asInstanceOf[CaseClassDef], args map transform).copiedFrom(tpe)
- case act @ AbstractClassType(acd, args) =>
- AbstractClassType(transform(acd).asInstanceOf[AbstractClassDef], args map transform).copiedFrom(tpe)
- case NAryType(ts, builder) => builder(ts map transform).copiedFrom(tpe)
- }
-}
-
-trait TreeTraverser {
- def traverse(id: Identifier): Unit = ()
- def traverse(cd: ClassDef): Unit = ()
- def traverse(fd: FunDef): Unit = ()
-
- def traverse(e: Expr): Unit = e match {
- case Variable(id) => traverse(id)
- case FiniteLambda(mappings, default, tpe) =>
- (default +: mappings.toSeq.flatMap(p => p._2 +: p._1)) foreach traverse
- traverse(tpe)
- case Lambda(args, body) =>
- args foreach (vd => traverse(vd.id))
- traverse(body)
- case Forall(args, body) =>
- args foreach (vd => traverse(vd.id))
- traverse(body)
- case Let(a, expr, body) =>
- traverse(a)
- traverse(expr)
- traverse(body)
- case CaseClass(cct, args) =>
- traverse(cct)
- args foreach traverse
- case CaseClassSelector(cct, caseClass, selector) =>
- traverse(cct)
- traverse(caseClass)
- case FunctionInvocation(TypedFunDef(fd, tpes), args) =>
- traverse(fd)
- tpes foreach traverse
- args foreach traverse
- case MethodInvocation(rec, cd, TypedFunDef(fd, tpes), args) =>
- traverse(rec)
- traverse(cd)
- traverse(fd)
- tpes foreach traverse
- args foreach traverse
- case This(ct) =>
- traverse(ct)
- case IsInstanceOf(expr, ct) =>
- traverse(expr)
- traverse(ct)
- case AsInstanceOf(expr, ct) =>
- traverse(expr)
- traverse(ct)
- case MatchExpr(scrutinee, cases) =>
- traverse(scrutinee)
- for (cse @ MatchCase(pattern, guard, rhs) <- cases) {
- traverse(pattern)
- guard foreach traverse
- traverse(rhs)
- }
- case FiniteSet(es, tpe) =>
- es foreach traverse
- traverse(tpe)
- case FiniteBag(es, tpe) =>
- es foreach { case (k, _) => traverse(k) }
- traverse(tpe)
- case FiniteMap(pairs, from, to) =>
- pairs foreach { case (k, v) => traverse(k); traverse(v) }
- traverse(from)
- traverse(to)
- case EmptyArray(tpe) =>
- traverse(tpe)
- case Hole(tpe, alts) =>
- traverse(tpe)
- alts foreach traverse
- case NoTree(tpe) =>
- traverse(tpe)
- case Error(tpe, desc) =>
- traverse(tpe)
- case Operator(es, builder) =>
- es foreach traverse
- case e =>
- }
-
- def traverse(pat: Pattern): Unit = pat match {
- case InstanceOfPattern(binder, ct) =>
- binder foreach traverse
- traverse(ct)
- case WildcardPattern(binder) =>
- binder foreach traverse
- case CaseClassPattern(binder, ct, subs) =>
- binder foreach traverse
- traverse(ct)
- subs foreach traverse
- case TuplePattern(binder, subs) =>
- binder foreach traverse
- subs foreach traverse
- case UnapplyPattern(binder, TypedFunDef(fd, tpes), subs) =>
- binder foreach traverse
- traverse(fd)
- tpes foreach traverse
- subs foreach traverse
- case PatternExtractor(subs, builder) =>
- subs foreach traverse
- }
-
- def traverse(tpe: TypeTree): Unit = tpe match {
- case cct @ CaseClassType(ccd, args) =>
- traverse(ccd)
- args foreach traverse
- case act @ AbstractClassType(acd, args) =>
- traverse(acd)
- args foreach traverse
- case NAryType(ts, builder) =>
- ts foreach traverse
- }
-}
diff --git a/src/main/scala/inox/trees/Trees.scala b/src/main/scala/inox/trees/Trees.scala
index 39d317891..5b7874b18 100644
--- a/src/main/scala/inox/trees/Trees.scala
+++ b/src/main/scala/inox/trees/Trees.scala
@@ -1,14 +1,17 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
-package purescala
+package inox
+package trees
-import utils._
-import Expressions.Variable
-import Types._
-import Definitions.Program
+trait Trees extends Expressions with Extractors with Types with Definitions {
-trait Trees extends Expressions with ExprOps with Types with TypeOps {
+ object exprOps extends {
+ val trees: Trees.this.type = Trees.this
+ } with ExprOps with Constructors
+
+ object typeOps extends {
+ val trees: Trees.this.type = Trees.this
+ } with TypeOps
abstract class Tree extends Positioned with Serializable with Printable {
def copiedFrom(o: Tree): this.type = {
@@ -34,11 +37,8 @@ trait Trees extends Expressions with ExprOps with Types with TypeOps {
val name: String,
val globalId: Int,
private[Common] val id: Int,
- private val tpe: TypeTree,
private val alwaysShowUniqueID: Boolean = false
- ) extends Tree with Typed with Ordered[Identifier] {
-
- val getType = tpe
+ ) extends Tree with Ordered[Identifier] {
override def equals(other: Any): Boolean = other match {
case null => false
diff --git a/src/main/scala/inox/trees/TypeOps.scala b/src/main/scala/inox/trees/TypeOps.scala
index 2a9e96b2d..0fd4bf588 100644
--- a/src/main/scala/inox/trees/TypeOps.scala
+++ b/src/main/scala/inox/trees/TypeOps.scala
@@ -1,19 +1,18 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
-package purescala
+package inox
+package trees
-import Types._
-import Definitions._
-import Common._
-import Expressions._
+trait TypeOps extends GenTreeOps {
+ val trees: Trees
+ import trees._
-object TypeOps extends GenTreeOps[TypeTree] {
+ type SubTree = Type
val Deconstructor = NAryType
def typeParamsOf(expr: Expr): Set[TypeParameter] = {
- ExprOps.collect(e => typeParamsOf(e.getType))(expr)
+ exprOps.collect(e => typeParamsOf(e.getType))(expr)
}
def typeParamsOf(t: TypeTree): Set[TypeParameter] = t match {
diff --git a/src/main/scala/inox/trees/Types.scala b/src/main/scala/inox/trees/Types.scala
index 608f01ccf..fe9d6a0bb 100644
--- a/src/main/scala/inox/trees/Types.scala
+++ b/src/main/scala/inox/trees/Types.scala
@@ -1,12 +1,7 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
-package purescala
-
-import Common._
-import Expressions._
-import Definitions._
-import TypeOps._
+package inox
+package trees
trait Types { self: Trees =>
@@ -89,7 +84,12 @@ trait Types { self: Trees =>
def lookupClass(implicit p: Program): Option[ClassDef] = p.lookupClass(id, tps)
}
- object NAryType extends TreeExtractor[Type] {
+ object NAryType extends TreeExtractor {
+ val trees: Types.this.type = Types.this
+ import trees._
+
+ type SubTree = Type
+
def unapply(t: Type): Option[(Seq[Type], Seq[Type] => Type)] = t match {
case ClassType(ccd, ts) => Some((ts, ts => ClassType(ccd, ts)))
case TupleType(ts) => Some((ts, TupleType))
diff --git a/src/main/scala/inox/trees/package.scala b/src/main/scala/inox/trees/package.scala
index 669bc61a1..db1812595 100644
--- a/src/main/scala/inox/trees/package.scala
+++ b/src/main/scala/inox/trees/package.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
+package inox
/** Provides AST definitions for Leon programs.
*
@@ -19,6 +19,6 @@ package leon
* a [[leon.purescala.ScalaPrinter]] that outputs a valid Scala program from a Leon
* representation.
*/
-package object purescala {
+package object trees {
}
--
GitLab