diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 301d9fa3a9d354b089bd4259533fadc5a3d026bd..0eb453a067a0318026839e9af4f4bd1ff569ffcf 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -23,9 +23,14 @@ package ast
*
*/
trait ExprOps extends GenTreeOps {
+ protected val trees: Trees
+ val sourceTrees: trees.type = trees
+ val targetTrees: trees.type = trees
+
import trees._
- type SubTree = Expr
+ type Source = Expr
+ type Target = Expr
val Deconstructor = Operator
@@ -105,7 +110,7 @@ trait ExprOps extends GenTreeOps {
f(e, initParent)
- val Deconstructor(es, _) = e
+ val Operator(es, _) = e
es foreach rec
}
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index c95132d7ebe87cac7c46128c02e2e80950eb4296..d2af32ea89cbebdbb99a9b4c093d398f815a477c 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -3,12 +3,234 @@
package inox
package ast
+
+trait TreeDeconstructor {
+ protected val s: Trees
+ protected val t: Trees
+
+ def deconstruct(expr: s.Expr): (Seq[s.Expr], Seq[s.Type], (Seq[t.Expr], Seq[t.Type]) => t.Expr) = expr match {
+ /* Unary operators */
+ case s.Not(e) =>
+ (Seq(e), Seq(), (es, tps) => t.Not(es.head))
+ case s.BVNot(e) =>
+ (Seq(e), Seq(), (es, tps) => t.BVNot(es.head))
+ case s.UMinus(e) =>
+ (Seq(e), Seq(), (es, tps) => t.UMinus(es.head))
+ case s.StringLength(e) =>
+ (Seq(e), Seq(), (es, tps) => t.StringLength(es.head))
+ case s.SetCardinality(e) =>
+ (Seq(e), Seq(), (es, tps) => t.SetCardinality(es.head))
+ case s.CaseClassSelector(e, sel) =>
+ (Seq(e), Seq(), (es, tps) => t.CaseClassSelector(es.head, sel))
+ case s.IsInstanceOf(e, ct) =>
+ (Seq(e), Seq(ct), (es, tps) => t.IsInstanceOf(es.head, tps.head.asInstanceOf[t.ClassType]))
+ case s.AsInstanceOf(e, ct) =>
+ (Seq(e), Seq(ct), (es, tps) => t.AsInstanceOf(es.head, tps.head.asInstanceOf[t.ClassType]))
+ case s.TupleSelect(e, i) =>
+ (Seq(e), Seq(), (es, tps) => t.TupleSelect(es.head, i))
+ case s.Lambda(args, body) =>
+ (
+ Seq(body), args.map(_.tpe),
+ (es, tps) => t.Lambda(args.zip(tps).map(p => t.ValDef(p._1.id, p._2)), es.head)
+ )
+ case s.Forall(args, body) =>
+ (
+ Seq(body), args.map(_.tpe),
+ (es, tps) => t.Forall(args.zip(tps).map(p => t.ValDef(p._1.id, p._2)), es.head)
+ )
+ case s.Choose(res, pred) =>
+ (Seq(pred), Seq(res.tpe), (es, tps) => t.Choose(t.ValDef(res.id, tps.head), es.head))
+
+ /* Binary operators */
+ case s.Equals(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.Equals(es(0), es(1)))
+ case s.Implies(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.Implies(es(0), es(1)))
+ case s.Plus(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.Plus(es(0), es(1)))
+ case s.Minus(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.Minus(es(0), es(1)))
+ case s.Times(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.Times(es(0), es(1)))
+ case s.Division(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.Division(es(0), es(1)))
+ case s.Remainder(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.Remainder(es(0), es(1)))
+ case s.Modulo(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.Modulo(es(0), es(1)))
+ case s.LessThan(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.LessThan(es(0), es(1)))
+ case s.GreaterThan(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.GreaterThan(es(0), es(1)))
+ case s.LessEquals(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.LessEquals(es(0), es(1)))
+ case s.GreaterEquals(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.GreaterEquals(es(0), es(1)))
+ case s.BVOr(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.BVOr(es(0), es(1)))
+ case s.BVAnd(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.BVAnd(es(0), es(1)))
+ case s.BVXOr(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.BVXOr(es(0), es(1)))
+ case s.BVShiftLeft(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.BVShiftLeft(es(0), es(1)))
+ case s.BVAShiftRight(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.BVAShiftRight(es(0), es(1)))
+ case s.BVLShiftRight(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.BVLShiftRight(es(0), es(1)))
+ case s.StringConcat(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.StringConcat(es(0), es(1)))
+ case s.SetAdd(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.SetAdd(es(0), es(1)))
+ case s.ElementOfSet(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.ElementOfSet(es(0), es(1)))
+ case s.SubsetOf(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.SubsetOf(es(0), es(1)))
+ case s.SetIntersection(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.SetIntersection(es(0), es(1)))
+ case s.SetUnion(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.SetUnion(es(0), es(1)))
+ case s.SetDifference(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.SetDifference(es(0), es(1)))
+ case s.BagAdd(e1, e2) =>
+ (Seq(e1, e2), Seq(), (es, tps) => t.BagAdd(es(0), es(1)))
+ case s.MultiplicityInBag(e1, e2) =>
+ (Seq(e1, e2), Seq(), (es, tps) => t.MultiplicityInBag(es(0), es(1)))
+ case s.BagIntersection(e1, e2) =>
+ (Seq(e1, e2), Seq(), (es, tps) => t.BagIntersection(es(0), es(1)))
+ case s.BagUnion(e1, e2) =>
+ (Seq(e1, e2), Seq(), (es, tps) => t.BagUnion(es(0), es(1)))
+ case s.BagDifference(e1, e2) =>
+ (Seq(e1, e2), Seq(), (es, tps) => t.BagDifference(es(0), es(1)))
+ case s.MapUpdated(map, k, v) =>
+ (Seq(map, k, v), Seq(), (es, tps) => t.MapUpdated(es(0), es(1), es(2)))
+ case s.MapApply(t1, t2) =>
+ (Seq(t1, t2), Seq(), (es, tps) => t.MapApply(es(0), es(1)))
+ case s.Let(binder, e, body) =>
+ (Seq(e, body), Seq(binder.tpe), (es, tps) => t.Let(t.ValDef(binder.id, tps.head), es(0), es(1)))
+
+ /* Other operators */
+ case s.FunctionInvocation(id, tps, args) =>
+ (args, tps, (es, tps) => t.FunctionInvocation(id, tps, es))
+ case s.Application(caller, args) => (caller +: args, Seq(), (es, tps) => t.Application(es.head, es.tail))
+ case s.CaseClass(ct, args) => (args, Seq(ct), (es, tps) => t.CaseClass(tps.head.asInstanceOf[t.ClassType], es))
+ case s.And(args) => (args, Seq(), (es, _) => t.And(es))
+ case s.Or(args) => (args, Seq(), (es, _) => t.Or(es))
+ case s.SubString(t1, a, b) => (t1 :: a :: b :: Nil, Seq(), (es, _) => t.SubString(es(0), es(1), es(2)))
+ case s.FiniteSet(els, base) =>
+ (els, Seq(base), (els, tps) => t.FiniteSet(els, tps.head))
+ case s.FiniteBag(els, base) =>
+ val subArgs = els.flatMap { case (k, v) => Seq(k, v) }
+ val builder = (as: Seq[t.Expr], tps: Seq[t.Type]) => {
+ def rec(kvs: Seq[t.Expr]): Seq[(t.Expr, t.Expr)] = kvs match {
+ case Seq(k, v, t @ _*) =>
+ Seq(k -> v) ++ rec(t)
+ case Seq() => Seq()
+ case _ => sys.error("odd number of key/value expressions")
+ }
+ t.FiniteBag(rec(as), tps.head)
+ }
+ (subArgs, Seq(base), builder)
+ case s.FiniteMap(elems, default, kT) =>
+ val subArgs = elems.flatMap { case (k, v) => Seq(k, v) }
+ val builder = (as: Seq[t.Expr], kT: Seq[t.Type]) => {
+ def rec(kvs: Seq[t.Expr]): (Seq[(t.Expr, t.Expr)], t.Expr) = kvs match {
+ case Seq(k, v, t @ _*) =>
+ val (kvs, default) = rec(t)
+ (Seq(k -> v) ++ kvs, default)
+ case Seq(default) => (Seq(), default)
+ }
+ val (pairs, default) = rec(as)
+ t.FiniteMap(pairs, default, kT.head)
+ }
+ (subArgs, Seq(kT), builder)
+ case s.Tuple(args) => (args, Seq(), (es, _) => t.Tuple(es))
+ case s.IfExpr(cond, thenn, elze) => (
+ Seq(cond, thenn, elze), Seq(),
+ (es, _) => t.IfExpr(es(0), es(1), es(2))
+ )
+
+ case s.Variable(id, tp) =>
+ (Seq(), Seq(tp), (_, tps) => t.Variable(id, tps.head))
+
+ case s.GenericValue(tp, id) =>
+ (Seq(), Seq(tp), (_, tps) => t.GenericValue(tps.head.asInstanceOf[t.TypeParameter], id))
+
+ case s.CharLiteral(ch) =>
+ (Seq(), Seq(), (_, _) => t.CharLiteral(ch))
+
+ case s.BVLiteral(bits, size) =>
+ (Seq(), Seq(), (_, _) => t.BVLiteral(bits, size))
+
+ case s.IntegerLiteral(i) =>
+ (Seq(), Seq(), (_, _) => t.IntegerLiteral(i))
+
+ case s.FractionLiteral(n, d) =>
+ (Seq(), Seq(), (_, _) => t.FractionLiteral(n, d))
+
+ case s.BooleanLiteral(b) =>
+ (Seq(), Seq(), (_, _) => t.BooleanLiteral(b))
+
+ case s.StringLiteral(st) =>
+ (Seq(), Seq(), (_, _) => t.StringLiteral(st))
+
+ case s.UnitLiteral() =>
+ (Seq(), Seq(), (_, _) => t.UnitLiteral())
+
+ /* Expr's not handled here should implement this trait */
+ // case e: Extractable =>
+ // e.extract
+
+ }
+
+ def deconstruct(tp: s.Type): (Seq[s.Type], Seq[t.Type] => t.Type) = tp match {
+ case s.ClassType(ccd, ts) => (ts, ts => t.ClassType(ccd, ts))
+ case s.TupleType(ts) => (ts, t.TupleType)
+ case s.SetType(tp) => (Seq(tp), ts => t.SetType(ts.head))
+ case s.BagType(tp) => (Seq(tp), ts => t.BagType(ts.head))
+ case s.MapType(from,to) => (Seq(from, to), ts => t.MapType(ts(0), ts(1)))
+ case s.FunctionType(fts, tt) => (tt +: fts, ts => t.FunctionType(ts.tail.toList, ts.head))
+
+ case s.TypeParameter(id) => (Seq(), _ => t.TypeParameter(id))
+ case s.BVType(size) => (Seq(), _ => t.BVType(size))
+
+ case s.Untyped => (Seq(), _ => t.Untyped)
+ case s.BooleanType => (Seq(), _ => t.BooleanType)
+ case s.UnitType => (Seq(), _ => t.UnitType)
+ case s.CharType => (Seq(), _ => t.CharType)
+ case s.IntegerType => (Seq(), _ => t.IntegerType)
+ case s.RealType => (Seq(), _ => t.RealType)
+ case s.StringType => (Seq(), _ => t.StringType)
+ }
+
+ def translate(e: s.Expr): t.Expr = {
+ val (es, tps, builder) = deconstruct(e)
+ builder(es map translate, tps map translate)
+ }
+
+ def translate(tp: s.Type): t.Type = {
+ val (tps, builder) = deconstruct(tp)
+ builder(tps map translate)
+ }
+
+}
+
+trait ExprDeconstructor extends TreeExtractor with TreeDeconstructor {
+ type Source = s.Expr
+ type Target = t.Expr
+
+ def unapply(e: Source): Option[(Seq[Source], (Seq[Target]) => Target)] = {
+ val (es, tps, builder) = deconstruct(e)
+ Some(es, ess => builder(ess, tps map translate))
+ }
+}
+
trait Extractors { self: Trees =>
/** Operator Extractor to extract any Expression in a consistent way.
*
* You can match on any Leon Expr, and then get both a Seq[Expr] of
- * subterms and a builder fonction that takes a Seq of subterms (of same
+ * subterms and a builder function that takes a Seq of subterms (of same
* length) and rebuild the original node.
*
* Those extractors do not perform any syntactic simplifications. They
@@ -18,163 +240,12 @@ trait Extractors { self: Trees =>
* 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 {
- val trees: Extractors.this.type = Extractors.this
- type SubTree = trees.Expr
-
- def unapply(expr: Expr): Option[(Seq[Expr], (Seq[Expr]) => Expr)] = expr match {
- /* Unary operators */
- case Not(t) =>
- Some((Seq(t), (es: Seq[Expr]) => Not(es.head)))
- case BVNot(t) =>
- Some((Seq(t), (es: Seq[Expr]) => BVNot(es.head)))
- case UMinus(t) =>
- Some((Seq(t), (es: Seq[Expr]) => UMinus(es.head)))
- case StringLength(t) =>
- Some((Seq(t), (es: Seq[Expr]) => StringLength(es.head)))
- case SetCardinality(t) =>
- Some((Seq(t), (es: Seq[Expr]) => SetCardinality(es.head)))
- case CaseClassSelector(e, sel) =>
- Some((Seq(e), (es: Seq[Expr]) => CaseClassSelector(es.head, sel)))
- case IsInstanceOf(e, ct) =>
- Some((Seq(e), (es: Seq[Expr]) => IsInstanceOf(es.head, ct)))
- case AsInstanceOf(e, ct) =>
- Some((Seq(e), (es: Seq[Expr]) => AsInstanceOf(es.head, ct)))
- case TupleSelect(t, i) =>
- Some((Seq(t), (es: Seq[Expr]) => TupleSelect(es.head, i)))
- case Lambda(args, body) =>
- Some((Seq(body), (es: Seq[Expr]) => Lambda(args, es.head)))
- case Forall(args, body) =>
- Some((Seq(body), (es: Seq[Expr]) => Forall(args, es.head)))
- case Choose(res, pred) =>
- Some((Seq(pred), (es: Seq[Expr]) => Choose(res, es.head)))
-
- /* Binary operators */
- case Equals(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => Equals(es(0), es(1)))
- case Implies(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => Implies(es(0), es(1)))
- case Plus(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => Plus(es(0), es(1)))
- case Minus(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => Minus(es(0), es(1)))
- case Times(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => Times(es(0), es(1)))
- case Division(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => Division(es(0), es(1)))
- case Remainder(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => Remainder(es(0), es(1)))
- case Modulo(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => Modulo(es(0), es(1)))
- case LessThan(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => LessThan(es(0), es(1)))
- case GreaterThan(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => GreaterThan(es(0), es(1)))
- case LessEquals(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => LessEquals(es(0), es(1)))
- case GreaterEquals(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => GreaterEquals(es(0), es(1)))
- case BVOr(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => BVOr(es(0), es(1)))
- case BVAnd(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => BVAnd(es(0), es(1)))
- case BVXOr(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => BVXOr(es(0), es(1)))
- case BVShiftLeft(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => BVShiftLeft(es(0), es(1)))
- case BVAShiftRight(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => BVAShiftRight(es(0), es(1)))
- case BVLShiftRight(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => BVLShiftRight(es(0), es(1)))
- case StringConcat(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => StringConcat(es(0), es(1)))
- case SetAdd(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => SetAdd(es(0), es(1)))
- case ElementOfSet(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => ElementOfSet(es(0), es(1)))
- case SubsetOf(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => SubsetOf(es(0), es(1)))
- case SetIntersection(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => SetIntersection(es(0), es(1)))
- case SetUnion(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => SetUnion(es(0), es(1)))
- case SetDifference(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => SetDifference(es(0), es(1)))
- case BagAdd(e1, e2) =>
- Some(Seq(e1, e2), (es: Seq[Expr]) => BagAdd(es(0), es(1)))
- case MultiplicityInBag(e1, e2) =>
- Some(Seq(e1, e2), (es: Seq[Expr]) => MultiplicityInBag(es(0), es(1)))
- case BagIntersection(e1, e2) =>
- Some(Seq(e1, e2), (es: Seq[Expr]) => BagIntersection(es(0), es(1)))
- case BagUnion(e1, e2) =>
- Some(Seq(e1, e2), (es: Seq[Expr]) => BagUnion(es(0), es(1)))
- case BagDifference(e1, e2) =>
- Some(Seq(e1, e2), (es: Seq[Expr]) => BagDifference(es(0), es(1)))
- case MapUpdated(map, k, v) =>
- Some(Seq(map, k, v), (es: Seq[Expr]) => MapUpdated(es(0), es(1), es(2)))
- case MapApply(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => MapApply(es(0), es(1)))
- case Let(binder, e, body) =>
- Some(Seq(e, body), (es: Seq[Expr]) => Let(binder, es(0), es(1)))
-
- /* Other operators */
- case fi @ FunctionInvocation(fd, tps, args) => Some((args, FunctionInvocation(fd, tps, _)))
- case fa @ Application(caller, args) => Some(caller +: args, as => Application(as.head, as.tail))
- case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
- case And(args) => Some((args, es => And(es)))
- case Or(args) => Some((args, es => Or(es)))
- case SubString(t1, a, b) => Some((t1::a::b::Nil, es => SubString(es(0), es(1), es(2))))
- case FiniteSet(els, base) =>
- Some((els, els => FiniteSet(els, base)))
- case FiniteBag(els, base) =>
- val subArgs = els.flatMap { case (k, v) => Seq(k, v) }
- val builder = (as: Seq[Expr]) => {
- def rec(kvs: Seq[Expr]): Seq[(Expr, Expr)] = kvs match {
- case Seq(k, v, t @ _*) =>
- Seq(k -> v) ++ rec(t)
- case Seq() => Seq()
- case _ => sys.error("odd number of key/value expressions")
- }
- FiniteBag(rec(as), base)
- }
- Some((subArgs, builder))
- case FiniteMap(args, f, t) => {
- val subArgs = args.flatMap { case (k, v) => Seq(k, v) }
- val builder = (as: Seq[Expr]) => {
- def rec(kvs: Seq[Expr]): Seq[(Expr, Expr)] = kvs match {
- case Seq(k, v, t @ _*) =>
- Seq(k -> v) ++ rec(t)
- case Seq() => Seq()
- case _ => sys.error("odd number of key/value expressions")
- }
- FiniteMap(rec(as), f, t)
- }
- Some((subArgs, builder))
- }
- case Tuple(args) => Some((args, es => Tuple(es)))
- case IfExpr(cond, thenn, elze) => Some((
- Seq(cond, thenn, elze),
- { case Seq(c, t, e) => IfExpr(c, t, e) }
- ))
- /* Terminals */
- case t: Terminal => Some(Seq[Expr](), (_:Seq[Expr]) => t)
-
- /* Expr's not handled here should implement this trait */
- case e: Extractable =>
- e.extract
-
- case _ =>
- None
- }
+ object Operator extends ExprDeconstructor {
+ val s: self.type = self
+ val t: self.type = self
}
- // Extractors for types are available at Types.NAryType
-
- trait Extractable {
- def extract: Option[(Seq[Expr], Seq[Expr] => Expr)]
- }
-
object TopLevelOrs { // expr1 OR (expr2 OR (expr3 OR ..)) => List(expr1, expr2, expr3)
def unapply(e: Expr): Option[Seq[Expr]] = e match {
case Let(i, e, TopLevelOrs(bs)) => Some(bs map (Let(i,e,_)))
diff --git a/src/main/scala/inox/ast/GenTreeOps.scala b/src/main/scala/inox/ast/GenTreeOps.scala
index 273d2180d2ab2160231a41e9c0feac7a720ab1fe..1b8af7c4a5dc1e4b0f1af9a9f2f63a67d1759842 100644
--- a/src/main/scala/inox/ast/GenTreeOps.scala
+++ b/src/main/scala/inox/ast/GenTreeOps.scala
@@ -5,33 +5,37 @@ package ast
import utils._
-/** 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.
+/** A type that pattern matches agains a type of [[Tree]] and extracts it Sources,
+ * and a builder that reconstructs a tree of the same type from Sources.
*
- * @tparam SubTree The type of the tree
+ * @tparam Source The type of the tree
*/
trait TreeExtractor {
- val trees: Trees
- import trees._
+ protected val s: Trees
+ protected val t: Trees
- type SubTree <: Tree
- def unapply(e: SubTree): Option[(Seq[SubTree], (Seq[SubTree]) => SubTree)]
+ type Source <: s.Tree
+ type Target <: t.Tree
+ def unapply(e: Source): Option[(Seq[Source], (Seq[Target]) => Target)]
}
/** Generic tree traversals based on a deconstructor of a specific tree type
*
- * @tparam SubTree The type of the tree
+ * @tparam Source The type of the tree
*/
-trait GenTreeOps {
- protected val trees: Trees
- import trees._
+trait GenTreeOps { self =>
+ protected val sourceTrees: Trees
+ protected val targetTrees: Trees
- type SubTree <: Tree
+ type Source <: sourceTrees.Tree
+ type Target <: targetTrees.Tree
- /** An extractor for [[SubTree]]*/
+ /** An extractor for [[Source]]*/
val Deconstructor: TreeExtractor {
- val trees: GenTreeOps.this.trees.type
- type SubTree = GenTreeOps.this.SubTree
+ val s: self.sourceTrees.type
+ val t: self.targetTrees.type
+ type Source = self.Source
+ type Target = self.Target
}
/* ========
@@ -48,12 +52,12 @@ trait GenTreeOps {
* to right), and combine the results along with the current node value.
*
* @param f a function that takes the current node and the seq
- * of results form the subtrees.
+ * of results form the Sources.
* @param e The value on which to apply the fold.
- * @return The expression after applying `f` on all subtrees.
+ * @return The expression after applying `f` on all Sources.
* @note the computation is lazy, hence you should not rely on side-effects of `f`
*/
- def fold[T](f: (SubTree, Seq[T]) => T)(e: SubTree): T = {
+ def fold[T](f: (Source, Seq[T]) => T)(e: Source): T = {
val rec = fold(f) _
val Deconstructor(es, _) = e
@@ -66,7 +70,7 @@ trait GenTreeOps {
/** Pre-traversal of the tree.
*
* Invokes the input function on every node '''before''' visiting
- * children. Traverse children from left to right subtrees.
+ * children. Traverse children from left to right Sources.
*
* e.g.
* {{{
@@ -80,7 +84,7 @@ trait GenTreeOps {
* @param f a function to apply on each node of the expression
* @param e the expression to traverse
*/
- def preTraversal(f: SubTree => Unit)(e: SubTree): Unit = {
+ def preTraversal(f: Source => Unit)(e: Source): Unit = {
val rec = preTraversal(f) _
val Deconstructor(es, _) = e
f(e)
@@ -104,7 +108,7 @@ trait GenTreeOps {
* @param f a function to apply on each node of the expression
* @param e the expression to traverse
*/
- def postTraversal(f: SubTree => Unit)(e: SubTree): Unit = {
+ def postTraversal(f: Source => Unit)(e: Source): Unit = {
val rec = postTraversal(f) _
val Deconstructor(es, _) = e
es.foreach(rec)
@@ -142,8 +146,8 @@ trait GenTreeOps {
*
* @note The mode with applyRec true can diverge if f is not well formed
*/
- def preMap(f: SubTree => Option[SubTree], applyRec : Boolean = false)(e: SubTree): SubTree = {
- def g(t: SubTree, u: Unit): (Option[SubTree], Unit) = (f(t), ())
+ def preMap(f: Source => Option[Source], applyRec : Boolean = false)(e: Source): Target = {
+ def g(t: Source, u: Unit): (Option[Source], Unit) = (f(t), ())
preMapWithContext[Unit](g, applyRec)(e, ())
}
@@ -151,7 +155,7 @@ trait GenTreeOps {
/** Post-transformation of the tree.
*
* Takes a partial function of replacements.
- * Substitutes '''after''' recursing down the trees.
+ * Substitutes '''after''' recurring down the trees.
*
* Supports two modes :
*
@@ -177,77 +181,27 @@ trait GenTreeOps {
*
* @note The mode with applyRec true can diverge if f is not well formed (i.e. not convergent)
*/
- def postMap(f: SubTree => Option[SubTree], applyRec : Boolean = false)(e: SubTree): SubTree = {
+ def postMap(f: Target => Option[Target], applyRec : Boolean = false)(e: Source): Target = {
val rec = postMap(f, applyRec) _
val Deconstructor(es, builder) = e
val newEs = es.map(rec)
- val newV = {
- if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
+ val newV: Target = {
+ if ((newEs zip es).exists { case (bef, aft) => aft ne bef } || (sourceTrees ne targetTrees)) {
builder(newEs).copiedFrom(e)
} else {
- e
+ e.asInstanceOf[Target]
}
}
if (applyRec) {
// Apply f as long as it returns Some()
- fixpoint { e : SubTree => f(e) getOrElse e } (newV)
+ fixpoint { e : Target => f(e) getOrElse e } (newV)
} else {
f(newV) getOrElse newV
}
}
- /** Post-transformation of the tree using flattening methods.
- *
- * Takes a partial function of replacements.
- * Substitutes '''after''' recursing down the trees.
- *
- * Supports two modes :
- *
- * - If applyRec is false (default), will only substitute once on each level.
- * e.g.
- * {{{
- * Add(a, Minus(b, c)) with replacements: Minus(b,c) -> z, Minus(e,c) -> d, b -> e
- * }}}
- * will yield:
- * {{{
- * Add(a, Minus(e, c))
- * }}}
- *
- * - If applyRec is true, it will substitute multiple times on each level:
- * e.g.
- * {{{
- * Add(a, Minus(b, c)) with replacements: Minus(e,c) -> d, b -> e, d -> f
- * }}}
- * will yield:
- * {{{
- * Add(a, f)
- * }}}
- *
- * @note The mode with applyRec true can diverge if f is not well formed (i.e. not convergent)
- */
- def postFlatmap(f: SubTree => Option[Seq[SubTree]], applyRec: Boolean = false)(e: SubTree): Seq[SubTree] = {
- val rec = postFlatmap(f, applyRec) _
-
- val Deconstructor(es, builder) = e
- val newEss = es.map(rec)
- val newVs: Seq[SubTree] = SeqUtils.cartesianProduct(newEss).map { newEs =>
- if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
- builder(newEs).copiedFrom(e)
- } else {
- e
- }
- }
-
- if (applyRec) {
- // Apply f as long as it returns Some()
- fixpoint { (e : Seq[SubTree]) => e.flatMap(newV => f(newV) getOrElse Seq(newV)) } (newVs)
- } else {
- newVs.flatMap((newV: SubTree) => f(newV) getOrElse Seq(newV))
- }
- }
-
/** Applies functions and combines results in a generic way
*
* Start with an initial value, and apply functions to nodes before
@@ -265,11 +219,11 @@ trait GenTreeOps {
* @see [[simplePreTransform]]
* @see [[simplePostTransform]]
*/
- def genericTransform[C](pre: (SubTree, C) => (SubTree, C),
- post: (SubTree, C) => (SubTree, C),
- combiner: (SubTree, Seq[C]) => C)(init: C)(expr: SubTree) = {
+ def genericTransform[C](pre: (Source, C) => (Source, C),
+ post: (Target, C) => (Target, C),
+ combiner: (Target, Seq[C]) => C)(init: C)(expr: Source) = {
- def rec(eIn: SubTree, cIn: C): (SubTree, C) = {
+ def rec(eIn: Source, cIn: C): (Target, C) = {
val (expr, ctx) = pre(eIn, cIn)
val Deconstructor(es, builder) = expr
@@ -286,27 +240,27 @@ trait GenTreeOps {
rec(expr, init)
}
- def noCombiner(e: SubTree, subCs: Seq[Unit]) = ()
- def noTransformer[C](e: SubTree, c: C) = (e, c)
+ def noCombiner(e: Target, subCs: Seq[Unit]) = ()
+ def noTransformer[C](e: Source, c: C) = (e, c)
/** A [[genericTransform]] with the trivial combiner that returns () */
- def simpleTransform(pre: SubTree => SubTree, post: SubTree => SubTree)(tree: SubTree) = {
- val newPre = (e: SubTree, c: Unit) => (pre(e), ())
- val newPost = (e: SubTree, c: Unit) => (post(e), ())
+ def simpleTransform(pre: Source => Source, post: Target => Target)(tree: Source) = {
+ val newPre = (e: Source, c: Unit) => (pre(e), ())
+ val newPost = (e: Target, c: Unit) => (post(e), ())
genericTransform[Unit](newPre, newPost, noCombiner)(())(tree)._1
}
/** A [[simpleTransform]] without a post-transformation */
- def simplePreTransform(pre: SubTree => SubTree)(tree: SubTree) = {
- val newPre = (e: SubTree, c: Unit) => (pre(e), ())
+ def simplePreTransform(pre: Source => Source)(tree: Source) = {
+ val newPre = (e: Source, c: Unit) => (pre(e), ())
genericTransform[Unit](newPre, (_, _), noCombiner)(())(tree)._1
}
/** A [[simpleTransform]] without a pre-transformation */
- def simplePostTransform(post: SubTree => SubTree)(tree: SubTree) = {
- val newPost = (e: SubTree, c: Unit) => (post(e), ())
+ def simplePostTransform(post: Target => Target)(tree: Source) = {
+ val newPost = (e: Target, c: Unit) => (post(e), ())
genericTransform[Unit]((e,c) => (e, None), newPost, noCombiner)(())(tree)._1
}
@@ -321,15 +275,15 @@ trait GenTreeOps {
* the recursion in its children. The context is "lost" when going back up,
* so changes made by one node will not be see by its siblings.
*/
- def preMapWithContext[C](f: (SubTree, C) => (Option[SubTree], C), applyRec: Boolean = false)
- (e: SubTree, c: C): SubTree = {
+ def preMapWithContext[C](f: (Source, C) => (Option[Source], C), applyRec: Boolean = false)
+ (e: Source, c: C): Target = {
- def rec(expr: SubTree, context: C): SubTree = {
+ def rec(expr: Source, context: C): Target = {
val (newV, newCtx) = {
if(applyRec) {
var ctx = context
- val finalV = fixpoint{ e: SubTree => {
+ val finalV = fixpoint{ e: Source => {
val res = f(e, ctx)
ctx = res._2
res._1.getOrElse(e)
@@ -344,10 +298,10 @@ trait GenTreeOps {
val Deconstructor(es, builder) = newV
val newEs = es.map(e => rec(e, newCtx))
- if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
+ if ((newEs zip es).exists { case (bef, aft) => aft ne bef } || (sourceTrees ne targetTrees)) {
builder(newEs).copiedFrom(newV)
} else {
- newV
+ newV.asInstanceOf[Target]
}
}
@@ -355,10 +309,10 @@ trait GenTreeOps {
rec(e, c)
}
- def preFoldWithContext[C](f: (SubTree, C) => C, combiner: (SubTree, C, Seq[C]) => C)
- (e: SubTree, c: C): C = {
+ def preFoldWithContext[C](f: (Source, C) => C, combiner: (Source, C, Seq[C]) => C)
+ (e: Source, c: C): C = {
- def rec(eIn: SubTree, cIn: C): C = {
+ def rec(eIn: Source, cIn: C): C = {
val ctx = f(eIn, cIn)
val Deconstructor(es, _) = eIn
val cs = es.map{ rec(_, ctx) }
@@ -377,57 +331,48 @@ trait GenTreeOps {
*/
/** Checks if the predicate holds in some sub-expression */
- def exists(matcher: SubTree => Boolean)(e: SubTree): Boolean = {
+ def exists(matcher: Source => Boolean)(e: Source): Boolean = {
fold[Boolean]({ (e, subs) => matcher(e) || subs.contains(true) } )(e)
}
/** Collects a set of objects from all sub-expressions */
- def collect[T](matcher: SubTree => Set[T])(e: SubTree): Set[T] = {
+ def collect[T](matcher: Source => Set[T])(e: Source): Set[T] = {
fold[Set[T]]({ (e, subs) => matcher(e) ++ subs.flatten } )(e)
}
- def collectPreorder[T](matcher: SubTree => Seq[T])(e: SubTree): Seq[T] = {
+ def collectPreorder[T](matcher: Source => Seq[T])(e: Source): Seq[T] = {
fold[Seq[T]]({ (e, subs) => matcher(e) ++ subs.flatten } )(e)
}
/** Returns a set of all sub-expressions matching the predicate */
- def filter(matcher: SubTree => Boolean)(e: SubTree): Set[SubTree] = {
- collect[SubTree] { e => Set(e) filter matcher }(e)
+ def filter(matcher: Source => Boolean)(e: Source): Set[Source] = {
+ collect[Source] { e => Set(e) filter matcher }(e)
}
/** Counts how many times the predicate holds in sub-expressions */
- def count(matcher: SubTree => Int)(e: SubTree): Int = {
+ def count(matcher: Source => Int)(e: Source): Int = {
fold[Int]({ (e, subs) => matcher(e) + subs.sum } )(e)
}
/** Replaces bottom-up sub-expressions by looking up for them in a map */
- def replace(substs: Map[SubTree,SubTree], expr: SubTree) : SubTree = {
+ def replace(substs: Map[Target, Target], expr: Source): Target = {
postMap(substs.lift)(expr)
}
- /** Replaces bottom-up sub-expressions by looking up for them in the provided order */
- def replaceSeq(substs: Seq[(SubTree, SubTree)], expr: SubTree): SubTree = {
- var res = expr
- for (s <- substs) {
- res = replace(Map(s), res)
- }
- res
- }
-
/** Computes the size of a tree */
- def formulaSize(t: SubTree): Int = {
+ def formulaSize(t: Source): Int = {
val Deconstructor(ts, _) = t
ts.map(formulaSize).sum + 1
}
/** Computes the depth of the tree */
- def depth(e: SubTree): Int = {
+ def depth(e: Source): Int = {
fold[Int]{ (_, sub) => 1 + (0 +: sub).max }(e)
}
/** Given a tree `toSearch` present in `treeToLookInto`, if `treeToLookInto` has the same shape as `treeToExtract`,
* returns the matching expression in `treeToExtract``.*/
- def lookup[T](checker: SubTree => Boolean, toExtract: SubTree => T)(treeToLookInto: SubTree, treeToExtract: SubTree): Option[T] = {
+ def lookup[T](checker: Source => Boolean, toExtract: Source => T)(treeToLookInto: Source, treeToExtract: Source): Option[T] = {
if(checker(treeToLookInto)) return Some(toExtract(treeToExtract))
val Deconstructor(childrenToLookInto, _) = treeToLookInto
@@ -443,7 +388,7 @@ trait GenTreeOps {
}
object Same {
- def unapply(tt: (SubTree, SubTree)): Option[(SubTree, SubTree)] = {
+ def unapply(tt: (Source, Source)): Option[(Source, Source)] = {
if (tt._1.getClass == tt._2.getClass) {
Some(tt)
} else {
diff --git a/src/main/scala/inox/ast/Identifier.scala b/src/main/scala/inox/ast/Identifier.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f9f847b80082d85ad00ceea1d395b43f93c01ccb
--- /dev/null
+++ b/src/main/scala/inox/ast/Identifier.scala
@@ -0,0 +1,70 @@
+package inox.ast
+
+import inox.utils.UniqueCounter
+
+/** Represents a unique symbol in Inox.
+ *
+ * The name is stored in the decoded (source code) form rather than encoded (JVM) form.
+ * The type may be left blank (Untyped) for Identifiers that are not variables.
+ */
+class Identifier (
+ val name: String,
+ val globalId: Int,
+ private val id: Int,
+ private val alwaysShowUniqueID: Boolean = false
+) extends Ordered[Identifier] {
+
+ override def equals(other: Any): Boolean = other match {
+ case null => false
+ case i: Identifier => i.globalId == this.globalId
+ case _ => false
+ }
+
+ override def hashCode: Int = globalId
+
+ override def toString: String = {
+ if (alwaysShowUniqueID) uniqueName else name
+ }
+
+ def uniqueNameDelimited(delim: String) = s"$name$delim$id"
+
+ def uniqueName: String = uniqueNameDelimited("$")
+
+ def freshen: Identifier = FreshIdentifier(name, alwaysShowUniqueID)
+
+ override def compare(that: Identifier): Int = {
+ val ord = implicitly[Ordering[(String, Int, Int)]]
+ ord.compare(
+ (this.name, this.id, this.globalId),
+ (that.name, that.id, that.globalId)
+ )
+ }
+}
+
+object FreshIdentifier {
+
+ private val uniqueCounter = new UniqueCounter[String]()
+
+ // Replace $opcode inside a string with the symbolic operator name
+ private def decode(s: String) =
+ scala.reflect.NameTransformer.decode(s)
+
+ /** Builds a fresh identifier
+ *
+ * @param name The name of the identifier
+ * @param alwaysShowUniqueID If the unique ID should always be shown
+ */
+ def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = {
+ val decoded = decode(name)
+ new Identifier(decoded, uniqueCounter.nextGlobal, uniqueCounter.next(decoded), alwaysShowUniqueID)
+ }
+
+ /** Builds a fresh identifier, whose ID is always shown
+ *
+ * @param name The name of the identifier
+ * @param forceId The forced ID of the identifier
+ * @param alwaysShowUniqueID If the unique ID should always be shown
+ */
+ def forceId(name: String, forceId: Int, alwaysShowUniqueID: Boolean = false): Identifier =
+ new Identifier(decode(name), uniqueCounter.nextGlobal, forceId, alwaysShowUniqueID)
+}
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index 7c30e972d82ff599835657bc0261d3bfc8ba88c3..aaec515fa045ab52cb2b6c1a7ea3a5f8a44246ed 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -11,24 +11,25 @@ object optPrintPositions extends InoxFlagOptionDef("printPositions", "Attach pos
object optPrintUniqueIds extends InoxFlagOptionDef("printIds", "Always print unique ids", false)
object optPrintTypes extends InoxFlagOptionDef("printPositions", "Attach types to trees when printing", false)
-trait Printers { self: Trees =>
+trait Printers {
+ self: Trees =>
case class PrinterContext(
- current: Tree,
- parents: List[Tree],
- lvl: Int,
- printer: PrettyPrinter) {
+ current: Tree,
+ parents: List[Tree],
+ lvl: Int,
+ printer: PrettyPrinter) {
def parent = parents.headOption
}
case class PrinterOptions(
- baseIndent: Int = 0,
- printPositions: Boolean = false,
- printUniqueIds: Boolean = false,
- printTypes: Boolean = false,
- symbols: Option[Symbols] = None
- ) {
+ baseIndent: Int = 0,
+ printPositions: Boolean = false,
+ printUniqueIds: Boolean = false,
+ printTypes: Boolean = false,
+ symbols: Option[Symbols] = None
+ ) {
require(
!printTypes || symbols.isDefined,
"Can't print types without an available symbol table"
@@ -41,10 +42,11 @@ trait Printers { self: Trees =>
baseIndent = 0,
printPositions = ctx.options.findOptionOrDefault(optPrintPositions),
printUniqueIds = ctx.options.findOptionOrDefault(optPrintUniqueIds),
- printTypes = ctx.options.findOptionOrDefault(optPrintTypes),
- symbols = None
+ printTypes = ctx.options.findOptionOrDefault(optPrintTypes),
+ symbols = None
)
}
+
def fromSymbols(s: Symbols, ctx: InoxContext): PrinterOptions = {
fromContext(ctx).copy(symbols = Some(s))
}
@@ -56,7 +58,7 @@ trait Printers { self: Trees =>
/** 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,
+ class PrettyPrinter(val opts: PrinterOptions,
osym: Option[Symbols],
val sb: StringBuffer = new StringBuffer) {
@@ -71,7 +73,7 @@ trait Printers { self: Trees =>
body
}
}
-
+
private val dbquote = "\""
def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
@@ -92,21 +94,13 @@ trait Printers { self: Trees =>
}
}
tree match {
- case id: Identifier =>
- val name = if (opts.printUniqueIds) {
- id.uniqueName
- } else {
- id.toString
- }
- p"$name"
-
case Variable(id, _) =>
p"$id"
-
+
case Let(vd, expr, SubString(v2: Variable, start, StringLength(v3: Variable))) if vd.toVariable == v2 && v2 == v3 =>
p"$expr.substring($start)"
- case Let(b,d,e) =>
+ case Let(b, d, e) =>
p"""|val $b = $d
|$e"""
@@ -116,42 +110,54 @@ trait Printers { self: Trees =>
case Choose(res, pred) =>
p"choose(($res) => $pred)"
- case e @ CaseClass(cct, args) =>
+ case e@CaseClass(cct, args) =>
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 UMinus(expr) => p"-$expr"
- case Equals(l,r) => optP { p"$l == $r" }
+ 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 UMinus(expr) => p"-$expr"
+ case Equals(l, r) => optP {
+ p"$l == $r"
+ }
- case StringConcat(lhs, rhs) => optP { p"$lhs + $rhs" }
+ case StringConcat(lhs, rhs) => optP {
+ p"$lhs + $rhs"
+ }
case SubString(expr, start, end) => p"$expr.substring($start, $end)"
- case StringLength(expr) => p"$expr.length"
+ case StringLength(expr) => p"$expr.length"
- case IntLiteral(v) => p"$v"
+ case IntLiteral(v) => p"$v"
case BVLiteral(bits, size) => p"x${(size to 1 by -1).map(i => if (bits(i)) "1" else "0")}"
case IntegerLiteral(v) => p"$v"
case FractionLiteral(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) {
+ 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 AsInstanceOf(e, ct) => p"""$e.asInstanceOf[$ct]"""
+ case Tuple(exprs) => p"($exprs)"
+ case TupleSelect(t, i) => p"$t._$i"
+ case AsInstanceOf(e, ct) => p"""$e.asInstanceOf[$ct]"""
case IsInstanceOf(e, cct) => p"$e.isInstanceOf[$cct]"
- case CaseClassSelector(e, id) => p"$e.$id"
+ case CaseClassSelector(e, id) => p"$e.$id"
case FunctionInvocation(id, tps, args) =>
p"$id${nary(tps, ", ", "[", "]")}"
@@ -166,55 +172,91 @@ trait Printers { self: Trees =>
p"$id"
case Lambda(args, body) =>
- optP { p"($args) => $body" }
-
- 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 BVNot(e) => optP { p"~$e" }
- case BVXOr(l,r) => optP { p"$l ^ $r" }
- case BVOr(l,r) => optP { p"$l | $r" }
- case BVAnd(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 fs @ FiniteSet(rs, _) => p"{${rs.distinct}}"
- case fs @ FiniteBag(rs, _) => p"{${rs.toMap.toSeq}}"
- case fm @ FiniteMap(rs, _, _) => p"{${rs.toMap.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 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)"
+ optP {
+ p"($args) => $body"
+ }
+
+ 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 BVNot(e) => optP {
+ p"~$e"
+ }
+ case BVXOr(l, r) => optP {
+ p"$l ^ $r"
+ }
+ case BVOr(l, r) => optP {
+ p"$l | $r"
+ }
+ case BVAnd(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 fs@FiniteSet(rs, _) => p"{${rs.distinct}}"
+ case fs@FiniteBag(rs, _) => p"{${rs.toMap.toSeq}}"
+ case fm@FiniteMap(rs, _, _) => p"{${rs.toMap.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 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 Not(expr) => p"\u00AC$expr"
- case vd @ ValDef(id, tpe) =>
+ case vd@ValDef(id, tpe) =>
p"$id : $tpe"
- case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
+ case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
case TypeParameterDef(tp) => p"$tp"
- case TypeParameter(id) => p"$id"
+ case TypeParameter(id) => p"$id"
- case IfExpr(c, t, ie : IfExpr) =>
+ case IfExpr(c, t, ie: IfExpr) =>
optP {
p"""|if ($c) {
| $t
@@ -231,18 +273,18 @@ trait Printers { self: Trees =>
}
// 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 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 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 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 =>
p"${c.id}${nary(c.tps, ", ", "[", "]")}"
@@ -251,7 +293,7 @@ trait Printers { self: Trees =>
case acd: AbstractClassDef =>
p"abstract class ${acd.id}${nary(acd.tparams, ", ", "[", "]")}"
- case ccd : CaseClassDef =>
+ case ccd: CaseClassDef =>
p"case class ${ccd.id}"
p"${nary(ccd.tparams, ", ", "[", "]")}"
p"(${ccd.fields})"
@@ -285,7 +327,7 @@ trait Printers { self: Trees =>
}
if (opts.printTypes) {
tree match {
- case t: Expr=>
+ case t: Expr =>
p" : ${t.getType(opts.symbols.get)} ⟩"
case _ =>
@@ -342,9 +384,9 @@ trait Printers { self: Trees =>
case (_: And | _: BVAnd | _: SetIntersection) => 3
// 4: < >
case (
- _: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan |
+ _: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan |
_: BVAShiftRight | _: BVLShiftRight | _: BVShiftLeft
- ) => 4
+ ) => 4
// 5: = !
case (_: Equals | _: Not | _: Implies) => 5
// 6: :
@@ -360,7 +402,7 @@ trait Printers { self: Trees =>
case (pa: PrettyPrintable, _) => pa.printRequiresParentheses(within)
case (_, None) => false
case (_, Some(
- _: Definition | _: Let | _: IfExpr | _: CaseClass | _: Lambda | _: Choose | _: Tuple
+ _: Definition | _: Let | _: IfExpr | _: CaseClass | _: Lambda | _: Choose | _: Tuple
)) => false
case (ex: StringConcat, Some(_: StringConcat)) => false
case (_, Some(_: FunctionInvocation)) => false
@@ -378,41 +420,41 @@ trait Printers { self: Trees =>
def p(args: Any*)(implicit ctx: PrinterContext): Unit = {
val printer = ctx.printer
- val sb = printer.sb
+ val sb = printer.sb
- val strings = sc.parts.iterator
+ val strings = sc.parts.iterator
val expressions = args.iterator
var extraInd = 0
var firstElem = true
- while(strings.hasNext) {
+ while (strings.hasNext) {
val currval = strings.next
- val s = if(currval != " || ") {
+ 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) == ' ') {
+ if (start >= 0 || firstElem) {
+ var i = start + 1
+ while (i < s.length && s(i) == ' ') {
i += 1
}
- extraInd = (i-start-1)/2
+ extraInd = (i - start - 1) / 2
}
firstElem = false
// Make sure new lines are also indented
- sb.append(s.replaceAll("\n", "\n"+(" "*ctx.lvl)))
+ 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)
+ if (e == "||")
+ println("Seen Expression: " + e)
e match {
case (t1, t2) =>
@@ -431,6 +473,14 @@ trait Printers { self: Trees =>
val nctx2 = nctx.copy(parents = parents, current = t)
printer.pp(t)(nctx2)
+ case id: Identifier =>
+ val name = if (ctx.printer.opts.printUniqueIds) {
+ id.uniqueName
+ } else {
+ id.toString
+ }
+ p"$name"
+
case p: PrintWrapper =>
p.print(nctx)
@@ -443,8 +493,8 @@ trait Printers { self: Trees =>
}
def nary(ls: Seq[Any], sep: String = ", ", init: String = "", closing: String = ""): PrintWrapper = {
- val (i, c) = if(ls.isEmpty) ("", "") else (init, closing)
- val strs = i +: List.fill(ls.size-1)(sep) :+ c
+ 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: _*)
@@ -465,20 +515,10 @@ trait Printers { self: Trees =>
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, osym: Option[Symbols]) extends PrettyPrinter(opts, osym) {
- override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
- tree match {
- case id: Identifier =>
- p"${id.name}"
+ def printRequiresParentheses(within: Option[Tree]): Boolean = false
- case _ =>
- super.pp(tree)
- }
- }
+ def isSimpleExpr: Boolean = false
}
abstract class PrettyPrinterFactory {
@@ -506,7 +546,4 @@ trait Printers { self: Trees =>
def create(opts: PrinterOptions, osym: Option[Symbols]) = new PrettyPrinter(opts, osym)
}
- object EquivalencePrettyPrinter extends PrettyPrinterFactory {
- def create(opts: PrinterOptions, osym: Option[Symbols]) = new EquivalencePrettyPrinter(opts, osym)
- }
}
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 2c101cfce8fe18e092aec0fb53b8e5fb3702d77e..da2698aa6a7fdf602b6cf14d80b5f013e4e54185 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -190,7 +190,7 @@ trait SymbolOps { self: TypeOps =>
case v: Variable if s.isDefinedAt(v) => rec(s(v), s)
case l @ Let(i,e,b) => rec(b, s + (i.toVariable -> rec(e, s)))
case i @ IfExpr(t1,t2,t3) => IfExpr(rec(t1, s),rec(t2, s),rec(t3, s)).copiedFrom(i)
- case n @ Deconstructor(args, recons) =>
+ case n @ Operator(args, recons) =>
var change = false
val rargs = args.map(a => {
val ra = rec(a, s)
@@ -422,7 +422,7 @@ trait SymbolOps { self: TypeOps =>
rec(lhs, path) ++
rec(rhs, path withCond lhs)
- case Operator(es, _) =>
+ case Deconstructor(es, _) =>
es.flatMap(rec(_, path))
case _ => sys.error("Expression " + expr + "["+expr.getClass+"] is not extractable")
diff --git a/src/main/scala/inox/ast/Trees.scala b/src/main/scala/inox/ast/Trees.scala
index 83297cc39a3dfc92c76b17517fe40714cb3d9f0c..2d1aba675eb1e6d588dbfe0edfa21bb765dce3b2 100644
--- a/src/main/scala/inox/ast/Trees.scala
+++ b/src/main/scala/inox/ast/Trees.scala
@@ -16,11 +16,14 @@ trait Trees
with Printers
with TreeOps {
+ type Identifier = ast.Identifier
+ val FreshIdentifier = ast.FreshIdentifier
+
class Unsupported(t: Tree, msg: String)(implicit ctx: InoxContext)
extends Exception(s"${t.asString(PrinterOptions.fromContext(ctx))}@${t.getPos} $msg")
abstract class Tree extends utils.Positioned with Serializable {
- def copiedFrom(o: Tree): this.type = {
+ def copiedFrom(o: Trees#Tree): this.type = {
setPos(o)
this
}
@@ -40,73 +43,6 @@ trait Trees
protected val trees: Trees.this.type = Trees.this
} with DSL
- /** Represents a unique symbol in Inox.
- *
- * The name is stored in the decoded (source code) form rather than encoded (JVM) form.
- * The type may be left blank (Untyped) for Identifiers that are not variables.
- */
- class Identifier private[Trees](
- val name: String,
- val globalId: Int,
- private[Trees] val id: Int,
- private val alwaysShowUniqueID: Boolean = false
- ) extends Tree with Ordered[Identifier] {
-
- override def equals(other: Any): Boolean = other match {
- case null => false
- case i: Identifier => i.globalId == this.globalId
- case _ => false
- }
-
- override def hashCode: Int = globalId
-
- override def toString: String = {
- if (alwaysShowUniqueID) uniqueName else name
- }
-
- def uniqueNameDelimited(delim: String) = s"$name$delim$id"
-
- def uniqueName: String = uniqueNameDelimited("$")
-
- def freshen: Identifier = FreshIdentifier(name, alwaysShowUniqueID).copiedFrom(this)
-
- override def compare(that: Identifier): Int = {
- val ord = implicitly[Ordering[(String, Int, Int)]]
- ord.compare(
- (this.name, this.id, this.globalId),
- (that.name, that.id, that.globalId)
- )
- }
- }
-
- object FreshIdentifier {
-
- private val uniqueCounter = new UniqueCounter[String]()
-
- // Replace $opcode inside a string with the symbolic operator name
- private def decode(s: String) =
- scala.reflect.NameTransformer.decode(s)
-
- /** Builds a fresh identifier
- *
- * @param name The name of the identifier
- * @param alwaysShowUniqueID If the unique ID should always be shown
- */
- def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = {
- val decoded = decode(name)
- new Identifier(decoded, uniqueCounter.nextGlobal, uniqueCounter.next(decoded), alwaysShowUniqueID)
- }
-
- /** Builds a fresh identifier, whose ID is always shown
- *
- * @param name The name of the identifier
- * @param forceId The forced ID of the identifier
- * @param alwaysShowUniqueID If the unique ID should always be shown
- */
- def forceId(name: String, forceId: Int, alwaysShowUniqueID: Boolean = false): Identifier =
- new Identifier(decode(name), uniqueCounter.nextGlobal, forceId, alwaysShowUniqueID)
- }
-
def aliased(id1: Identifier, id2: Identifier) = {
id1.toString == id2.toString
}
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index b7019771e53b5968698faed7d8ec0afebba3c704..79e0c4fdc9780df0db79e885255e4e14e30db2fa 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -8,12 +8,13 @@ trait TypeOps {
import trees._
protected implicit val symbols: Symbols
- object typeOps extends GenTreeOps {
- val trees: TypeOps.this.trees.type = TypeOps.this.trees
- import trees._
-
- type SubTree = Type
- val Deconstructor = NAryType
+ object typeOps extends {
+ protected val sourceTrees: trees.type = trees
+ protected val targetTrees: trees.type = trees
+ } with GenTreeOps {
+ type Source = trees.Type
+ type Target = trees.Type
+ lazy val Deconstructor = NAryType
}
class TypeErrorException(msg: String) extends Exception(msg)
diff --git a/src/main/scala/inox/ast/Types.scala b/src/main/scala/inox/ast/Types.scala
index e7ae6f8cd7b39213362de7949b289a46cf1544ab..1de21b0c064010bb268152ad1d6c473dad1ed130 100644
--- a/src/main/scala/inox/ast/Types.scala
+++ b/src/main/scala/inox/ast/Types.scala
@@ -51,9 +51,8 @@ trait Types { self: Trees =>
override def toString = "Int32Type"
}
- class TypeParameter private (name: String) extends Type {
- val id = FreshIdentifier(name)
- def freshen = new TypeParameter(name)
+ case class TypeParameter(id: Identifier) extends Type {
+ def freshen = new TypeParameter(id.freshen)
override def equals(that: Any) = that match {
case TypeParameter(id) => this.id == id
@@ -64,8 +63,7 @@ trait Types { self: Trees =>
}
object TypeParameter {
- def unapply(tp: TypeParameter): Option[Identifier] = Some(tp.id)
- def fresh(name: String) = new TypeParameter(name)
+ def fresh(name: String) = new TypeParameter(FreshIdentifier(name))
}
/*
@@ -87,21 +85,11 @@ trait Types { self: Trees =>
def tcd(implicit s: Symbols): TypedClassDef = s.getClass(id, tps)
}
- object NAryType extends TreeExtractor {
- val trees: Types.this.type = Types.this
-
- 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))
- case SetType(t) => Some((Seq(t), ts => SetType(ts.head)))
- case BagType(t) => Some((Seq(t), ts => BagType(ts.head)))
- case MapType(from,to) => Some((Seq(from, to), t => MapType(t(0), t(1))))
- case FunctionType(fts, tt) => Some((tt +: fts, ts => FunctionType(ts.tail.toList, ts.head)))
- /* nullary types */
- case t => Some(Nil, _ => t)
- }
+ val NAryType: TreeExtractor {
+ val s: self.type
+ val t: self.type
+ type Source = self.Type
+ type Target = self.Type
}
object FirstOrderFunctionType {
@@ -112,3 +100,12 @@ trait Types { self: Trees =>
}
}
}
+
+trait TypeDeconstructor extends TreeExtractor with TreeDeconstructor {
+ type Source = s.Type
+ type Target = t.Type
+
+ def unapply(tp: s.Type): Option[(Seq[s.Type], Seq[t.Type] => t.Type)] = {
+ Some(deconstruct(tp))
+ }
+}
diff --git a/src/main/scala/inox/grammars/FunctionCallsGrammars.scala b/src/main/scala/inox/grammars/FunctionCallsGrammars.scala
index b798e360a0b4c98780beaf19eeec9d2e6c8994e9..c82da4bd2fae57568b5754b8b3dc2a5eab07c14b 100644
--- a/src/main/scala/inox/grammars/FunctionCallsGrammars.scala
+++ b/src/main/scala/inox/grammars/FunctionCallsGrammars.scala
@@ -15,7 +15,7 @@ trait FunctionCallsGrammars extends utils.Helpers { self: GrammarsUniverse =>
* @param types The candidate real type parameters for [[currentFunction]]
* @param exclude An additional set of functions for which no calls will be generated
*/
- case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[Type], exclude: Set[FunDef]) extends SimpleExpressionGrammar {
+ case class FunctionCalls(currentFunction: FunDef, types: Seq[Type], exclude: Set[FunDef]) extends SimpleExpressionGrammar {
def computeProductions(t: Type): Seq[Prod] = {
def getCandidates(fd: FunDef): Seq[TypedFunDef] = {
@@ -74,7 +74,7 @@ trait FunctionCallsGrammars extends utils.Helpers { self: GrammarsUniverse =>
val filter = (tfd:TypedFunDef) => /* TODO: Reimplement this somehow tfd.fd.isSynthetic || tfd.fd.isInner || */ (exclude contains tfd.fd)
- val funcs = functionsAvailable(prog).toSeq.sortBy(_.id).flatMap(getCandidates).filterNot(filter)
+ val funcs = functionsAvailable.toSeq.sortBy(_.id).flatMap(getCandidates).filterNot(filter)
funcs.map{ tfd =>
nonTerminal(tfd.params.map(_.getType), FunctionInvocation(tfd.id, tfd.tps, _))//, tagOf(tfd.fd, isSafe = false))
diff --git a/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala b/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala
index f5ed9bd5c905a9c646af112ce6153108a71c6267..b7041cabf47020abbf3779217c575fdc7fa81ac6 100644
--- a/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala
@@ -10,8 +10,10 @@ trait SimilarToAspects { self: GrammarsUniverse =>
import program._
import trees.{Minus => EMinus, Plus => EPlus, Times => ETimes, _}
import symbols._
+ import exprOps._
/** Generates expressions similar to a [[Seq]] of given expressions
+ *
* @param es The expressions for which similar ones will be generated
*/
case class SimilarTo(es: Seq[Expr]) extends Aspect {
@@ -36,7 +38,7 @@ trait SimilarToAspects { self: GrammarsUniverse =>
val similarProds: Prods = es.filter(e => isSubtypeOf(e.getType, lab.getType)).flatMap { e =>
val swaps: Prods = e match {
- case Operator(as, b) if as.nonEmpty && !isCommutative(e) =>
+ case Deconstructor(as, b) if as.nonEmpty && !isCommutative(e) =>
val ast = as.zipWithIndex.groupBy(_._1.getType).mapValues(_.map(_._2).toList)
val perms = ast.values.map { is =>
diff --git a/src/main/scala/inox/grammars/utils/Helpers.scala b/src/main/scala/inox/grammars/utils/Helpers.scala
index 24a689970e7ebbd9e2200bfb3ace4d82044ead1c..8e7d37cf8702b14d60d76e6c03c625569fefe0a3 100644
--- a/src/main/scala/inox/grammars/utils/Helpers.scala
+++ b/src/main/scala/inox/grammars/utils/Helpers.scala
@@ -103,5 +103,5 @@ trait Helpers { self: GrammarsUniverse =>
* - all functions in main units
* - all functions imported, or methods of classes imported
*/
- def functionsAvailable(p: Program): Set[p.trees.FunDef] = p.symbols.functions.values.toSet
+ def functionsAvailable: Set[FunDef] = program.symbols.functions.values.toSet
}
diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala
index 43b0f7db53cf0a76cfa216c13aa234b8d7699e88..3fec7b2283dfc86888119eda3032d04bc0489aa9 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -1,5 +1,7 @@
/* Copyright 2009-2016 EPFL, Lausanne */
+import inox.ast.TypeDeconstructor
+
/** Core package of the Inox solving interface
*
* == Structure ==
@@ -43,6 +45,11 @@ package object inox {
object trees extends ast.Trees {
+ object NAryType extends {
+ protected val s: trees.type = trees
+ protected val t: trees.type = trees
+ } with TypeDeconstructor
+
class Symbols(
val functions: Map[Identifier, FunDef],
val classes: Map[Identifier, ClassDef]
@@ -71,5 +78,6 @@ package object inox {
this.classes ++ classes.map(cd => cd.id -> cd)
)
}
+
}
}
diff --git a/src/main/scala/inox/solvers/ADTManagers.scala b/src/main/scala/inox/solvers/ADTManagers.scala
index 51e1bdadf701824d4f8215f5640fd6c05a3a33be..2dd2e707877f516836fe692fe52068eb5dcd093c 100644
--- a/src/main/scala/inox/solvers/ADTManagers.scala
+++ b/src/main/scala/inox/solvers/ADTManagers.scala
@@ -13,13 +13,13 @@ trait ADTManagers {
case class DataType(sym: Identifier, cases: Seq[Constructor]) extends Printable {
def asString(implicit opts: PrinterOptions) = {
- "Datatype: " + sym.asString(opts) + "\n" + cases.map(c => " - " + c.asString(opts)).mkString("\n")
+ "Datatype: " + sym.toString + "\n" + cases.map(c => " - " + c.asString(opts)).mkString("\n")
}
}
case class Constructor(sym: Identifier, tpe: Type, fields: Seq[(Identifier, Type)]) extends Printable {
def asString(implicit opts: PrinterOptions) = {
- sym.asString(opts) + " [" + tpe.asString(opts) + "] " + fields.map(f => f._1.asString(opts) + ": " + f._2.asString(opts)).mkString("(", ", ", ")")
+ sym.toString + " [" + tpe.asString(opts) + "] " + fields.map(f => f._1.toString + ": " + f._2.toString).mkString("(", ", ", ")")
}
}
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index ac419f0978da1033aafdc71314a55dc11bc0404f..34d317c6244f85e25deea4394d5ff7fb78dff5d0 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -45,7 +45,7 @@ trait AbstractSolver extends Interruptible {
object SolverUnsupportedError {
def msg(t: Tree, reason: Option[String]) = {
- s"(of ${t.getClass}) is unsupported by solver ${name}" + reason.map(":\n " + _ ).getOrElse("")
+ s"(of ${t.getClass}) is unsupported by solver $name" + reason.map(":\n " + _ ).getOrElse("")
}
}
@@ -84,7 +84,6 @@ trait AbstractSolver extends Interruptible {
}
trait Solver extends AbstractSolver {
- import program._
import program.trees._
type Trees = Expr
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index c8c0f3713246fb7ee38d9e29d7d4788d573890ad..7ee370361e30105c345d3cd7410c758a5dec8b65 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -28,6 +28,7 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
import program._
import trees._
import symbols._
+
def targetName: String
implicit val debugSection: DebugSection
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index 9d7f34597c3d9ae8edc51bdc8bf66597d741256f..d31f11fc97ed0e879afb85a025d31943af454a05 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -65,12 +65,12 @@ trait DatatypeTemplates { self: Templates =>
res
}
- private case class FreshFunction(expr: Expr) extends Expr with Extractable {
+ private case class FreshFunction(expr: Expr) extends Expr { //with Extractable {
def getType(implicit s: Symbols) = BooleanType
val extract = Some(Seq(expr), (exprs: Seq[Expr]) => FreshFunction(exprs.head))
}
- private case class InductiveType(tcd: TypedAbstractClassDef, expr: Expr) extends Expr with Extractable {
+ private case class InductiveType(tcd: TypedAbstractClassDef, expr: Expr) extends Expr { //with Extractable {
def getType(implicit s: Symbols) = BooleanType
val extract = Some(Seq(expr), (exprs: Seq[Expr]) => InductiveType(tcd, exprs.head))
}