From 12384b459259b6a799187a119444dd2f31cd35b9 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 4 Apr 2016 14:07:02 +0200
Subject: [PATCH] Cleanup/document, mainly grammars

---
 src/main/scala/leon/grammars/Aspect.scala     |  6 ++----
 src/main/scala/leon/grammars/Closures.scala   |  2 --
 src/main/scala/leon/grammars/Empty.scala      |  2 --
 .../leon/grammars/ExpressionGrammar.scala     | 12 +++++-------
 src/main/scala/leon/grammars/Grammars.scala   |  1 -
 src/main/scala/leon/grammars/Label.scala      |  2 --
 .../scala/leon/grammars/NonTerminal.scala     | 19 -------------------
 .../grammars/SimpleExpressionGrammar.scala    | 17 +++++++++--------
 .../grammars/aspects/ExtraTerminals.scala     |  4 ++--
 ...antAspect.scala => PersistentAspect.scala} |  8 +++-----
 .../leon/grammars/aspects/SimilarTo.scala     | 10 +++++-----
 .../scala/leon/grammars/aspects/Sized.scala   |  3 +--
 .../scala/leon/grammars/aspects/Tagged.scala  |  7 ++-----
 src/main/scala/leon/purescala/Types.scala     |  4 +---
 .../scala/leon/synthesis/graph/Graph.scala    |  2 --
 15 files changed, 30 insertions(+), 69 deletions(-)
 delete mode 100644 src/main/scala/leon/grammars/NonTerminal.scala
 rename src/main/scala/leon/grammars/aspects/{PersistantAspect.scala => PersistentAspect.scala} (70%)

diff --git a/src/main/scala/leon/grammars/Aspect.scala b/src/main/scala/leon/grammars/Aspect.scala
index a7761faab..69ed03380 100644
--- a/src/main/scala/leon/grammars/Aspect.scala
+++ b/src/main/scala/leon/grammars/Aspect.scala
@@ -25,10 +25,8 @@ import Tags._
  */
 
 
-abstract class Aspect {
-  type Production = ProductionRule[Label, Expr]
-
-  def asString(implicit ctx: LeonContext): String
+abstract class Aspect extends Printable {
+  final type Production = ProductionRule[Label, Expr]
 
   def applyTo(l: Label, ps: Seq[Production])(implicit ctx: LeonContext): Seq[Production]
 }
diff --git a/src/main/scala/leon/grammars/Closures.scala b/src/main/scala/leon/grammars/Closures.scala
index 101534302..1d1d8c9cc 100644
--- a/src/main/scala/leon/grammars/Closures.scala
+++ b/src/main/scala/leon/grammars/Closures.scala
@@ -4,11 +4,9 @@ package leon
 package grammars
 
 import purescala.Types._
-import purescala.TypeOps._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.Common._
-import purescala.Constructors._
 
 case object Closures extends ExpressionGrammar {
   def computeProductions(lab: Label)(implicit ctx: LeonContext): Seq[ProductionRule[Label, Expr]] = lab.getType match {
diff --git a/src/main/scala/leon/grammars/Empty.scala b/src/main/scala/leon/grammars/Empty.scala
index 79f391820..639c0f956 100644
--- a/src/main/scala/leon/grammars/Empty.scala
+++ b/src/main/scala/leon/grammars/Empty.scala
@@ -3,8 +3,6 @@
 package leon
 package grammars
 
-import purescala.Types.Typed
-
 /** The empty expression grammar */
 case class Empty() extends ExpressionGrammar {
   def computeProductions(l: Label)(implicit ctx: LeonContext) = Nil
diff --git a/src/main/scala/leon/grammars/ExpressionGrammar.scala b/src/main/scala/leon/grammars/ExpressionGrammar.scala
index 8c5e304e5..186729fce 100644
--- a/src/main/scala/leon/grammars/ExpressionGrammar.scala
+++ b/src/main/scala/leon/grammars/ExpressionGrammar.scala
@@ -4,21 +4,19 @@ package leon
 package grammars
 
 import purescala.Expressions._
-import purescala.Types._
 import purescala.Common._
 
 import scala.collection.mutable.{HashMap => MutableMap}
 
-/** Represents a context-free grammar of expressions
-  */
+/** Represents a context-free grammar of expressions */
 abstract class ExpressionGrammar {
 
   private[this] val cache = new MutableMap[Label, Seq[ProductionRule[Label, Expr]]]()
 
   /** The list of production rules for this grammar for a given nonterminal.
-    * This is the cached version of [[getProductions]] which clients should use.
     *
     * @param lab The nonterminal for which production rules will be generated
+    * @note This is the cached version of [[computeProductions]]. Clients should use this method.
     */
   def getProductions(lab: Label)(implicit ctx: LeonContext) = {
     cache.getOrElse(lab, {
@@ -28,19 +26,20 @@ abstract class ExpressionGrammar {
     })
   }
 
-  /** The list of production rules for this grammar for a given nonterminal
+  /** The list of production rules for this grammar for a given nonterminal.
     *
     * @param lab The nonterminal for which production rules will be generated
+    * @note Clients should use the cached version, [[getProductions]] instead
     */
   def computeProductions(lab: Label)(implicit ctx: LeonContext): Seq[ProductionRule[Label, Expr]]
 
-
   def applyAspects(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: LeonContext) = {
     lab.aspects.foldLeft(ps) {
       case (ps, a) => a.applyTo(lab, ps)
     }
   }
 
+  /** Union of grammars */
   final def ||(that: ExpressionGrammar): ExpressionGrammar = {
     Union(Seq(this, that))
   }
@@ -66,7 +65,6 @@ abstract class ExpressionGrammar {
       }
     }
 
-
     for ((lab, gs) <- cache.toSeq.sortWith(sorter)) {
       val lhs = f"${Console.BOLD}${lab.asString}%50s${Console.RESET} ::= "
 
diff --git a/src/main/scala/leon/grammars/Grammars.scala b/src/main/scala/leon/grammars/Grammars.scala
index 7ed0760f4..2f60d59a4 100644
--- a/src/main/scala/leon/grammars/Grammars.scala
+++ b/src/main/scala/leon/grammars/Grammars.scala
@@ -7,7 +7,6 @@ import synthesis.Witnesses.Hint
 import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Types._
-import purescala.TypeOps._
 import purescala.Extractors.TopLevelAnds
 import purescala.ExprOps.formulaSize
 
diff --git a/src/main/scala/leon/grammars/Label.scala b/src/main/scala/leon/grammars/Label.scala
index dc3e98ea9..efb36387d 100644
--- a/src/main/scala/leon/grammars/Label.scala
+++ b/src/main/scala/leon/grammars/Label.scala
@@ -4,8 +4,6 @@ package leon
 package grammars
 
 import purescala.Types._
-import purescala.Expressions._
-import purescala.Constructors._
 
 case class Label(tpe: TypeTree, aspects: List[Aspect] = Nil) extends Typed {
   val getType = tpe
diff --git a/src/main/scala/leon/grammars/NonTerminal.scala b/src/main/scala/leon/grammars/NonTerminal.scala
deleted file mode 100644
index c57283f26..000000000
--- a/src/main/scala/leon/grammars/NonTerminal.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package grammars
-
-import purescala.Types._
-
-/** A basic non-terminal symbol of a grammar.
-  *
-  * @param t The type of which expressions will be generated
-  * @param l A label that characterizes this [[NonTerminal]]
-  * @param depth The optional depth within the syntax tree where this [[NonTerminal]] is.
-  * @tparam L The type of label for this NonTerminal.
-  */
-case class NonTerminal[L](t: TypeTree, l: L, depth: Option[Int] = None) extends Typed {
-  val getType = t
-
-  override def asString(implicit ctx: LeonContext) = t.asString+"#"+l+depth.map(d => "@"+d).getOrElse("")
-}
diff --git a/src/main/scala/leon/grammars/SimpleExpressionGrammar.scala b/src/main/scala/leon/grammars/SimpleExpressionGrammar.scala
index f12849521..41b293f81 100644
--- a/src/main/scala/leon/grammars/SimpleExpressionGrammar.scala
+++ b/src/main/scala/leon/grammars/SimpleExpressionGrammar.scala
@@ -3,9 +3,12 @@
 package leon
 package grammars
 
-import purescala.Expressions._
-import purescala.Types._
+import purescala.Expressions.Expr
+import purescala.Types.TypeTree
 
+/** An [[ExpressionGrammar]] whose productions for a given [[Label]]
+  * depend only on the underlying [[TypeTree]] of the label
+  */
 abstract class SimpleExpressionGrammar extends ExpressionGrammar {
 
   type Prod = ProductionRule[TypeTree, Expr]
@@ -28,15 +31,13 @@ abstract class SimpleExpressionGrammar extends ExpressionGrammar {
     }
   }
 
-  /** The list of production rules for this grammar for a given nonterminal
-    *
-    * @param lab The nonterminal for which production rules will be generated
-    */
-  def computeProductions(lab: Label)(implicit ctx: LeonContext): Seq[ProductionRule[Label, Expr]] = {
+  // Finalize this to depend only on the type of the label
+  final def computeProductions(lab: Label)(implicit ctx: LeonContext): Seq[ProductionRule[Label, Expr]] = {
     computeProductions(lab.getType).map { p =>
       ProductionRule(p.subTrees.map(Label(_)), p.builder, p.tag, p.cost)
     }
   }
 
-  def computeProductions(tpe: TypeTree)(implicit ctx: LeonContext): Seq[ProductionRule[TypeTree, Expr]]
+  /** Version of [[ExpressionGrammar.computeProductions]] which depends only a [[TypeTree]] */
+  def computeProductions(tpe: TypeTree)(implicit ctx: LeonContext): Seq[Prod]
 }
diff --git a/src/main/scala/leon/grammars/aspects/ExtraTerminals.scala b/src/main/scala/leon/grammars/aspects/ExtraTerminals.scala
index f2d0f46d0..213ea7445 100644
--- a/src/main/scala/leon/grammars/aspects/ExtraTerminals.scala
+++ b/src/main/scala/leon/grammars/aspects/ExtraTerminals.scala
@@ -12,13 +12,13 @@ import purescala.TypeOps.isSubtypeOf
  * Informs sub-productions that there are extra terminals available (used by
  * grammars.ExtraTerminals).
  */
-case class ExtraTerminals(s: Set[Expr]) extends PersistantAspect {
+case class ExtraTerminals(s: Set[Expr]) extends PersistentAspect {
   def asString(implicit ctx: LeonContext) = {
     s.toList.map(_.asString).mkString("{", ",", "}")
   }
 
 
-  override def applyTo(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: LeonContext) = {
+  override def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: LeonContext) = {
     super.applyTo(lab, ps) ++ {
       s.filter(e => isSubtypeOf(e.getType, lab.getType)).map { e =>
         ProductionRule[Label, Expr](Nil, { (es: Seq[Expr]) => e }, Tags.Top, formulaSize(e))
diff --git a/src/main/scala/leon/grammars/aspects/PersistantAspect.scala b/src/main/scala/leon/grammars/aspects/PersistentAspect.scala
similarity index 70%
rename from src/main/scala/leon/grammars/aspects/PersistantAspect.scala
rename to src/main/scala/leon/grammars/aspects/PersistentAspect.scala
index 4d8670bd4..05f17f736 100644
--- a/src/main/scala/leon/grammars/aspects/PersistantAspect.scala
+++ b/src/main/scala/leon/grammars/aspects/PersistentAspect.scala
@@ -4,10 +4,8 @@ package leon
 package grammars
 package aspects
 
-import purescala.Expressions.Expr
-
 /**
- * Persistant aspects allow label information to be propagated down:
+ * Persistent aspects allow label information to be propagated down:
  * Int{e} means (Int with a terminal 'e'). And thus, the Closure grammar
  * is able to have, as production:
  *   Int=>Int  :=  (e: Int) => Int{e}
@@ -19,8 +17,8 @@ import purescala.Expressions.Expr
  * like:
  *   e + 1
  */
-abstract class PersistantAspect extends Aspect {
-  def applyTo(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: LeonContext) = {
+abstract class PersistentAspect extends Aspect {
+  def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: LeonContext) = {
     ps.map { p =>
       p.copy(subTrees = p.subTrees.map(lab => lab.withAspect(this)))
     }
diff --git a/src/main/scala/leon/grammars/aspects/SimilarTo.scala b/src/main/scala/leon/grammars/aspects/SimilarTo.scala
index 4685f9a3c..cd27a0583 100644
--- a/src/main/scala/leon/grammars/aspects/SimilarTo.scala
+++ b/src/main/scala/leon/grammars/aspects/SimilarTo.scala
@@ -11,9 +11,9 @@ import purescala.Constructors._
 import purescala.Extractors._
 import utils.SeqUtils._
 
-/**
- * Attach sizes to labels and transmit them down accordingly
- */
+/** Generates expressions similar to a given expression
+  * @param e The expression for which similar ones will be generated
+  */
 case class SimilarTo(e: Expr) extends Aspect {
   type Prods = Seq[ProductionRule[Label, Expr]]
 
@@ -28,7 +28,7 @@ case class SimilarTo(e: Expr) extends Aspect {
    *                f(a, ~b~)
    *                f(b, a)   // if non-commut
    */
-  def applyTo(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: LeonContext) = {
+  def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: LeonContext) = {
     def isCommutative(e: Expr) = e match {
       case _: Plus | _: Times => true
       case _ => false
@@ -63,7 +63,7 @@ case class SimilarTo(e: Expr) extends Aspect {
       }
 
       val subs: Prods = e match {
-        case Operator(as, b) if as.size > 0 =>
+        case Operator(as, b) if as.nonEmpty =>
           for ((a, i) <- as.zipWithIndex) yield {
             ProductionRule[Label, Expr](
               List(Label(a.getType).withAspect(SimilarTo(a))),
diff --git a/src/main/scala/leon/grammars/aspects/Sized.scala b/src/main/scala/leon/grammars/aspects/Sized.scala
index 664852578..e2ed3c0e8 100644
--- a/src/main/scala/leon/grammars/aspects/Sized.scala
+++ b/src/main/scala/leon/grammars/aspects/Sized.scala
@@ -4,7 +4,6 @@ package leon
 package grammars
 package aspects
 
-import purescala.Expressions.Expr
 import utils.SeqUtils._
 
 /**
@@ -13,7 +12,7 @@ import utils.SeqUtils._
 case class Sized(size: Int) extends Aspect {
   def asString(implicit ctx: LeonContext) = "|"+size+"|"
 
-  def applyTo(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: LeonContext) = {
+  def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: LeonContext) = {
     val optimizeCommut = true
 
     ps.flatMap { p =>
diff --git a/src/main/scala/leon/grammars/aspects/Tagged.scala b/src/main/scala/leon/grammars/aspects/Tagged.scala
index be097ac12..c6838ab2f 100644
--- a/src/main/scala/leon/grammars/aspects/Tagged.scala
+++ b/src/main/scala/leon/grammars/aspects/Tagged.scala
@@ -4,8 +4,6 @@ package leon
 package grammars
 package aspects
 
-import purescala.Expressions.Expr
-import utils.SeqUtils._
 import Tags._
 
 case class Tagged(tag: Tag, pos: Int, isConst: Option[Boolean]) extends Aspect {
@@ -18,10 +16,9 @@ case class Tagged(tag: Tag, pos: Int, isConst: Option[Boolean]) extends Aspect {
   /** [[isConst]] is printed as follows: ↓ for constants only, ↑ for nonconstants only,
     * ○ for anything allowed.
     */
-  override def asString(implicit ctx: LeonContext): String = s"$tag@$pos$cString"
+  def asString(implicit ctx: LeonContext): String = s"#$tag$cString@$pos"
 
-
-  override def applyTo(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: LeonContext) = {
+  def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: LeonContext) = {
 
     // Tags to avoid depending on parent aspect
     val excludedTags: Set[Tag] = (tag, pos) match {
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 75693c375..0b02ca9e3 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -3,8 +3,6 @@
 package leon
 package purescala
 
-import scala.language.implicitConversions
-
 import Common._
 import Expressions._
 import Definitions._
@@ -146,7 +144,7 @@ object Types {
       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)))
-      /* n-ary operators */
+      /* nullary types */
       case t => Some(Nil, _ => t)
     }
   }
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index af52ea5b9..59ae2ae37 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -29,8 +29,6 @@ sealed class Graph(problem: Problem) {
 
 sealed abstract class Node(val parent: Option[Node]) extends Printable {
 
-  def asString(implicit ctx: LeonContext): String
-
   var descendants: List[Node] = Nil
   // indicates whether this particular node has already been expanded
   var isExpanded: Boolean = false
-- 
GitLab