From 4785b17ce96c51fa08c00a3224a0bd30ef5ed744 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 13 Dec 2012 15:23:54 +0100
Subject: [PATCH] remove Options trees
---
src/main/scala/leon/plugin/CodeExtraction.scala | 6 ------
src/main/scala/leon/purescala/PrettyPrinter.scala | 11 -----------
src/main/scala/leon/purescala/ScalaPrinter.scala | 12 ------------
src/main/scala/leon/purescala/Trees.scala | 6 ------
src/main/scala/leon/purescala/TypeTrees.scala | 5 -----
src/main/scala/leon/solvers/RandomSolver.scala | 1 -
6 files changed, 41 deletions(-)
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 8807b8761..c7cc6a103 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -709,11 +709,6 @@ trait CodeExtraction extends Extractors {
val IntLiteral(ri) = rec(i)
Waypoint(ri, rec(tree)).setType(pstpe)
}
- case ExSomeConstruction(tpe, arg) => {
- // println("Got Some !" + tpe + ":" + arg)
- val underlying = scalaType2PureScala(unit, silent)(tpe)
- OptionSome(rec(arg)).setType(OptionType(underlying))
- }
case ExCaseClassConstruction(tpt, args) => {
val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
if(!cctype.isInstanceOf[CaseClassType]) {
@@ -1049,7 +1044,6 @@ trait CodeExtraction extends Extractors {
case tpe if tpe == NothingClass.tpe => BottomType
case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) => SetType(rec(btt))
case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) => MultisetType(rec(btt))
- case TypeRef(_, sym, btt :: Nil) if isOptionClassSym(sym) => OptionType(rec(btt))
case TypeRef(_, sym, List(ftt,ttt)) if isMapTraitSym(sym) => MapType(rec(ftt),rec(ttt))
case TypeRef(_, sym, List(t1,t2)) if isTuple2(sym) => TupleType(Seq(rec(t1),rec(t2)))
case TypeRef(_, sym, List(t1,t2,t3)) if isTuple3(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3)))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 7ab1b3c2f..0f023bfb9 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -114,16 +114,6 @@ object PrettyPrinter {
nsb
}
- case OptionSome(a) => {
- var nsb = sb
- nsb.append("Some(")
- nsb = pp(a, nsb, lvl)
- nsb.append(")")
- nsb
- }
-
- case OptionNone(_) => sb.append("None")
-
case CaseClass(cd, args) => {
var nsb = sb
nsb.append(cd.id)
@@ -367,7 +357,6 @@ object PrettyPrinter {
case SetType(bt) => pp(bt, sb.append("Set["), lvl).append("]")
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 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 b1cec54c5..aad213668 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -114,14 +114,6 @@ object ScalaPrinter {
sb.append("._" + i)
}
- case OptionSome(a) => {
- sb.append("Some(")
- pp(a, sb, lvl)
- sb.append(")")
- }
-
- case OptionNone(_) => sb.append("None")
-
case CaseClass(cd, args) => {
sb.append(cd.id)
ppNary(sb, args, "(", ", ", ")", lvl)
@@ -367,10 +359,6 @@ object ScalaPrinter {
sb.append("Multiset[")
pp(bt, sb, lvl)
sb.append("]")
- case OptionType(bt) =>
- sb.append("Option[")
- pp(bt, sb, lvl)
- sb.append("]")
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/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index e8516fc9a..741b3fcaa 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -383,12 +383,6 @@ object Trees {
val fixedType = BooleanType
}
- /* Option expressions */
- case class OptionSome(value: Expr) extends Expr
- case class OptionNone(baseType: TypeTree) extends Expr with Terminal with FixedType {
- val fixedType = OptionType(baseType)
- }
-
/* Set expressions */
case class EmptySet(baseType: TypeTree) extends Expr with Terminal
case class FiniteSet(elements: Seq[Expr]) extends Expr
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 3e834e0b0..6dd49f749 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -142,10 +142,6 @@ object TypeTrees {
case (_,InfiniteSize) => InfiniteSize
case (FiniteSize(n),FiniteSize(m)) => FiniteSize(scala.math.pow(m+1, n).toInt)
}
- case OptionType(base) => domainSize(base) match {
- case InfiniteSize => InfiniteSize
- case FiniteSize(n) => FiniteSize(n+1)
- }
case c: ClassType => InfiniteSize
}
@@ -187,7 +183,6 @@ object TypeTrees {
case class SetType(base: TypeTree) extends TypeTree
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 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 da6731a73..330bd00fc 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -75,7 +75,6 @@ class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extend
case ListType(base) => sys.error("I don't know what to do")
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 _ => sys.error("Unexpected type: " + t)
}
--
GitLab