From 1721a8652e7b6eaf916daa92b26448ef1f0a0eb4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 13 Dec 2012 13:59:30 +0100
Subject: [PATCH] remove usage of FunctionType and AnonymousFunction
---
src/main/scala/leon/Evaluator.scala | 12 -------
src/main/scala/leon/FunctionTemplate.scala | 4 ---
.../scala/leon/plugin/CodeExtraction.scala | 11 -------
.../scala/leon/purescala/Extractors.scala | 1 -
.../scala/leon/purescala/PrettyPrinter.scala | 29 ----------------
.../scala/leon/purescala/ScalaPrinter.scala | 25 --------------
src/main/scala/leon/purescala/TreeOps.scala | 3 --
src/main/scala/leon/purescala/Trees.scala | 4 ---
src/main/scala/leon/purescala/TypeTrees.scala | 11 -------
.../scala/leon/solvers/RandomSolver.scala | 1 -
.../leon/solvers/z3/AbstractZ3Solver.scala | 33 -------------------
11 files changed, 134 deletions(-)
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 27ecd4a6a..5792b973c 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -319,18 +319,6 @@ object Evaluator {
case (FiniteMap(ss), e) => BooleanLiteral(ss.exists(_.from == e))
case (l, r) => throw TypeErrorEx(TypeError(l, m.getType))
}
- case AnonymousFunctionInvocation(i,as) => {
- val fun = ctx(i)
- fun match {
- case AnonymousFunction(es, ev) => {
- es.find(_._1 == as) match {
- case Some(res) => res._2
- case None => ev
- }
- }
- case _ => scala.sys.error("function id has non-function interpretation")
- }
- }
case Distinct(args) => {
val newArgs = args.map(rec(ctx, _))
BooleanLiteral(newArgs.distinct.size == newArgs.size)
diff --git a/src/main/scala/leon/FunctionTemplate.scala b/src/main/scala/leon/FunctionTemplate.scala
index c7dac3029..3f3494524 100644
--- a/src/main/scala/leon/FunctionTemplate.scala
+++ b/src/main/scala/leon/FunctionTemplate.scala
@@ -161,10 +161,6 @@ object FunctionTemplate {
case b @ BinaryOperator(a1, a2, r) => r(rec(pathVar, pathPol, a1), rec(pathVar, pathPol, a2)).setType(b.getType)
case u @ UnaryOperator(a, r) => r(rec(pathVar, pathPol, a)).setType(u.getType)
case t : Terminal => t
- case a : AnonymousFunction => {
- Settings.reporter.warning("AnonymousFunction literal showed up in the construction of a FunctionTemplate.")
- a
- }
}
}
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 0c42d24f7..8807b8761 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -901,16 +901,6 @@ trait CodeExtraction extends Extractors {
case MapType(_,tt) =>
assert(rargs.size == 1)
MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
- case FunctionType(fts, tt) => {
- rlhs match {
- case Variable(id) =>
- AnonymousFunctionInvocation(id, rargs).setType(tt)
- case _ => {
- if (!silent) unit.error(tree.pos, "apply on non-variable or non-map expression")
- throw ImpureCodeEncounteredException(tree)
- }
- }
- }
case ArrayType(bt) => {
assert(rargs.size == 1)
ArraySelect(rlhs, rargs.head).setType(bt).setPosInfo(app.pos.line, app.pos.column)
@@ -1065,7 +1055,6 @@ trait CodeExtraction extends Extractors {
case TypeRef(_, sym, List(t1,t2,t3)) if isTuple3(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3)))
case TypeRef(_, sym, List(t1,t2,t3,t4)) if isTuple4(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4)))
case TypeRef(_, sym, List(t1,t2,t3,t4,t5)) if isTuple5(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4),rec(t5)))
- case TypeRef(_, sym, ftt :: ttt :: Nil) if isFunction1TraitSym(sym) => FunctionType(List(rec(ftt)), rec(ttt))
case TypeRef(_, sym, btt :: Nil) if isArrayClassSym(sym) => ArrayType(rec(btt))
case TypeRef(_, sym, Nil) if classesToClasses.keySet.contains(sym) => classDefToClassType(classesToClasses(sym))
case _ => {
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index ce64bbadb..b5a349bb1 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -84,7 +84,6 @@ object Extractors {
object NAryOperator {
def unapply(expr: Expr) : Option[(Seq[Expr],(Seq[Expr])=>Expr)] = expr match {
case fi @ FunctionInvocation(fd, args) => Some((args, (as => FunctionInvocation(fd, as).setPosInfo(fi))))
- case AnonymousFunctionInvocation(id, args) => Some((args, (as => AnonymousFunctionInvocation(id, as))))
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, And.apply))
case Or(args) => Some((args, Or.apply))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 27d1b6e74..7ab1b3c2f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -143,26 +143,6 @@ object PrettyPrinter {
nsb = ppNary(nsb, args, "(", ", ", ")", lvl)
nsb
}
- case AnonymousFunction(es, ev) => {
- var nsb = sb
- nsb.append("{")
- es.foreach {
- case (as, res) =>
- nsb = ppNary(nsb, as, "", " ", "", lvl)
- nsb.append(" -> ")
- nsb = pp(res, nsb, lvl)
- nsb.append(", ")
- }
- nsb.append("else -> ")
- nsb = pp(ev, nsb, lvl)
- nsb.append("}")
- }
- case AnonymousFunctionInvocation(id, args) => {
- var nsb = sb
- nsb.append(id)
- nsb = ppNary(nsb, args, "(", ", ", ")", lvl)
- nsb
- }
case Plus(l,r) => ppBinary(sb, l, r, " + ", lvl)
case Minus(l,r) => ppBinary(sb, l, r, " - ", lvl)
case Times(l,r) => ppBinary(sb, l, r, " * ", lvl)
@@ -388,15 +368,6 @@ object PrettyPrinter {
case MapType(ft,tt) => pp(tt, pp(ft, sb.append("Map["), lvl).append(","), lvl).append("]")
case MultisetType(bt) => pp(bt, sb.append("Multiset["), lvl).append("]")
case OptionType(bt) => pp(bt, sb.append("Option["), lvl).append("]")
- case FunctionType(fts, tt) => {
- var nsb = sb
- if (fts.size > 1)
- nsb = ppNaryType(nsb, fts, "(", ", ", ")", lvl)
- else if (fts.size == 1)
- nsb = pp(fts.head, nsb, lvl)
- nsb.append(" => ")
- pp(tt, nsb, lvl)
- }
case TupleType(tpes) => ppNaryType(sb, tpes, "(", ", ", ")", lvl)
case c: ClassType => sb.append(c.classDef.id)
case _ => sb.append("Type?")
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index d2059302c..b1cec54c5 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -137,23 +137,6 @@ object ScalaPrinter {
sb.append(fd.id)
ppNary(sb, args, "(", ", ", ")", lvl)
}
- case AnonymousFunction(es, ev) => {
- sb.append("{")
- es.foreach {
- case (as, res) =>
- ppNary(sb, as, "", " ", "", lvl)
- sb.append(" -> ")
- pp(res, sb, lvl)
- sb.append(", ")
- }
- sb.append("else -> ")
- pp(ev, sb, lvl)
- sb.append("}")
- }
- case AnonymousFunctionInvocation(id, args) => {
- sb.append(id)
- ppNary(sb, args, "(", ", ", ")", lvl)
- }
case Plus(l,r) => ppBinary(sb, l, r, " + ", lvl)
case Minus(l,r) => ppBinary(sb, l, r, " - ", lvl)
case Times(l,r) => ppBinary(sb, l, r, " * ", lvl)
@@ -388,14 +371,6 @@ object ScalaPrinter {
sb.append("Option[")
pp(bt, sb, lvl)
sb.append("]")
- case FunctionType(fts, tt) => {
- if (fts.size > 1)
- ppNaryType(sb, fts, "(", ", ", ")", lvl)
- else if (fts.size == 1)
- pp(fts.head, sb, lvl)
- sb.append(" => ")
- pp(tt, sb, lvl)
- }
case TupleType(tpes) => ppNaryType(sb, tpes, "(", ", ", ")", lvl)
case c: ClassType => sb.append(c.classDef.id)
case _ => sb.append("Type?")
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index a38c557ae..10a74488f 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -331,7 +331,6 @@ object TreeOps {
case u @ UnaryOperator(a,_) => compute(u, rec(a))
case i @ IfExpr(a1,a2,a3) => compute(i, combine(combine(rec(a1), rec(a2)), rec(a3)))
case m @ MatchExpr(scrut, cses) => compute(m, (scrut +: cses.flatMap(_.expressions)).map(rec(_)).reduceLeft(combine))
- case a @ AnonymousFunction(es, ev) => compute(a, (es.flatMap(e => e._1 ++ Seq(e._2)) ++ Seq(ev)).map(rec(_)).reduceLeft(combine))
case c @ Choose(args, body) => compute(c, rec(body))
case t: Terminal => compute(t, convert(t))
case unhandled => scala.sys.error("Non-terminal case should be handled in treeCatamorphism: " + unhandled)
@@ -362,7 +361,6 @@ object TreeOps {
def compute(t: Expr, s: Set[Identifier]) = t match {
case Let(i,_,_) => s -- Set(i)
case MatchExpr(_, cses) => s -- (cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b))
- case AnonymousFunctionInvocation(i,_) => s ++ Set[Identifier](i)
case _ => s
}
treeCatamorphism(convert, combine, compute, expr)
@@ -826,7 +824,6 @@ object TreeOps {
CaseClass(ccd, fields.map(f => simplestValue(f.getType)))
case SetType(baseType) => EmptySet(baseType).setType(tpe)
case MapType(fromType, toType) => EmptyMap(fromType, toType).setType(tpe)
- case FunctionType(fromTypes, toType) => AnonymousFunction(Seq.empty, simplestValue(toType)).setType(tpe)
case _ => throw new Exception("I can't choose simplest value for type " + tpe)
}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index d69931e75..e8516fc9a 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -457,10 +457,6 @@ object Trees {
case class Concat(list1: Expr, list2: Expr) extends Expr
case class ListAt(list: Expr, index: Expr) extends Expr
- /* Function operations */
- case class AnonymousFunction(entries: Seq[(Seq[Expr],Expr)], elseValue: Expr) extends Expr
- case class AnonymousFunctionInvocation(id: Identifier, args: Seq[Expr]) extends Expr
-
/* Constraint programming */
case class Distinct(exprs: Seq[Expr]) extends Expr with FixedType {
val fixedType = BooleanType
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 7f3f20c29..3e834e0b0 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -146,16 +146,6 @@ object TypeTrees {
case InfiniteSize => InfiniteSize
case FiniteSize(n) => FiniteSize(n+1)
}
- case FunctionType(fts, tt) => {
- val fromSizes = fts map domainSize
- val toSize = domainSize(tt)
- if (fromSizes.exists(_ == InfiniteSize) || toSize == InfiniteSize)
- InfiniteSize
- else {
- val n = toSize.asInstanceOf[FiniteSize].size
- FiniteSize(scala.math.pow(n, fromSizes.foldLeft(1)((acc, s) => acc * s.asInstanceOf[FiniteSize].size)).toInt)
- }
- }
case c: ClassType => InfiniteSize
}
@@ -198,7 +188,6 @@ object TypeTrees {
case class MultisetType(base: TypeTree) extends TypeTree
case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
case class OptionType(base: TypeTree) extends TypeTree
- case class FunctionType(from: List[TypeTree], to: TypeTree) extends TypeTree
case class ArrayType(base: TypeTree) extends TypeTree
sealed abstract class ClassType extends TypeTree {
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index f7c8ee3e9..da6731a73 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -76,7 +76,6 @@ class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extend
case TupleType(bases) => sys.error("I don't know what to do")
case MapType(from, to) => sys.error("I don't know what to do")
case OptionType(base) => sys.error("I don't know what to do")
- case f: FunctionType => sys.error("I don't know what to do")
case _ => sys.error("Unexpected type: " + t)
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 759b9d749..7628c6acb 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -315,19 +315,6 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
arrayTupleSort
}
}
- case ft @ FunctionType(fts, tt) => funSorts.get(ft) match {
- case Some(s) => s
- case None => {
- val fss = fts map typeToSort
- val ts = typeToSort(tt)
- val (tupleSort, consFuncDecl, projFuncDecls) = z3.mkTupleSort(fts.map(_.toString).mkString("(",", ", ")"), fss: _*)
- val funSort = z3.mkArraySort(tupleSort, ts)
- funSorts += (ft -> funSort)
- funDomainConstructors += (ft -> consFuncDecl)
- funDomainSelectors += (ft -> projFuncDecls)
- funSort
- }
- }
case tt @ TupleType(tpes) => tupleSorts.get(tt) match {
case Some(s) => s
case None => {
@@ -544,16 +531,6 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
val res = getLength(ar)
res
}
- case AnonymousFunctionInvocation(id, args) => id.getType match {
- case ft @ FunctionType(fts, tt) => {
- val consFD = funDomainConstructors(ft)
- val rid = rec(Variable(id))
- val rargs = args map rec
- z3.mkSelect(rid, consFD(rargs: _*))
- }
- case errorType => scala.sys.error("Unexpected type for function: " + (ex, errorType))
- }
-
case Distinct(exs) => z3.mkDistinct(exs.map(rec(_)): _*)
case _ => {
@@ -583,16 +560,6 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
}
(if (singletons.isEmpty) EmptyMap(kt, vt) else FiniteMap(singletons.toSeq)).setType(expType.get)
}
- case funType @ Some(FunctionType(fts, tt)) =>
- model.getArrayValue(t) match {
- case None => throw new CantTranslateException(t)
- case Some((es, ev)) =>
- val entries: Seq[(Seq[Expr], Expr)] = es.toSeq.map(e => (e, z3.getASTKind(e._1))).collect {
- case ((key, value), Z3AppAST(cons, args)) if cons == funDomainConstructors(funType.get) => ((args zip fts) map (p => rec(p._1, Some(p._2))), rec(value, Some(tt)))
- }
- val elseValue = rec(ev, Some(tt))
- AnonymousFunction(entries, elseValue).setType(expType.get)
- }
case Some(SetType(dt)) =>
model.getSetValue(t) match {
case None => throw new CantTranslateException(t)
--
GitLab