From 634a3749de4e4f6e5f040568448a458d6d359a33 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 4 Nov 2016 17:44:16 +0100
Subject: [PATCH] Small fixes in Definitions and Collector

---
 src/main/scala/inox/ast/Definitions.scala        | 12 ++++++------
 src/main/scala/inox/ast/Expressions.scala        |  3 +--
 src/main/scala/inox/ast/ProgramEncoder.scala     | 14 ++++++++++++++
 src/main/scala/inox/transformers/Collector.scala |  6 +++++-
 4 files changed, 26 insertions(+), 9 deletions(-)

diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 637dbc8e6..659a94fc8 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -25,8 +25,8 @@ trait Definitions { self: Trees =>
   case class FunctionLookupException(id: Identifier) extends LookupException(id, "function")
   case class ADTLookupException(id: Identifier) extends LookupException(id, "adt")
 
-  case class NotWellFormedException(id: Identifier, s: Symbols)
-    extends Exception(s"$id not well formed in $s")
+  case class NotWellFormedException(d: Definition)
+    extends Exception(s"Not well formed definition $d")
 
   /** Common super-type for [[ValDef]] and [[Expressions.Variable]].
     *
@@ -219,7 +219,7 @@ trait Definitions { self: Trees =>
     def constructors(implicit s: Symbols): Seq[ADTConstructor] = cons
       .map(id => s.getADT(id) match {
         case cons: ADTConstructor => cons
-        case _ => throw NotWellFormedException(id, s)
+        case sort => throw NotWellFormedException(sort)
       })
 
     def isInductive(implicit s: Symbols): Boolean = {
@@ -325,12 +325,12 @@ trait Definitions { self: Trees =>
 
     def toConstructor = this match {
       case tcons: TypedADTConstructor => tcons
-      case _ => throw NotWellFormedException(definition.id, symbols)
+      case _ => throw NotWellFormedException(definition)
     }
 
     def toSort = this match {
       case tsort: TypedADTSort => tsort
-      case _ => throw NotWellFormedException(definition.id, symbols)
+      case _ => throw NotWellFormedException(definition)
     }
   }
 
@@ -355,7 +355,7 @@ trait Definitions { self: Trees =>
 
     lazy val sort: Option[TypedADTSort] = definition.sort.map(id => symbols.getADT(id) match {
       case sort: ADTSort => TypedADTSort(sort, tps)
-      case _ => throw NotWellFormedException(id, symbols)
+      case cons => throw NotWellFormedException(cons)
     })
   }
 
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index bf4ebabd6..55c8aad2a 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -121,8 +121,7 @@ trait Expressions { self: Trees =>
   /** $encodingof  `function(...)` (function invocation) */
   case class FunctionInvocation(id: Identifier, tps: Seq[Type], args: Seq[Expr]) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type = s.lookupFunction(id, tps) match {
-      case Some(tfd) =>
-        require(args.size == tfd.params.size)
+      case Some(tfd) if args.size == tfd.params.size =>
         checkParamTypes(args.map(_.getType), tfd.params.map(_.tpe), tfd.returnType)
       case _ => Untyped
     }
diff --git a/src/main/scala/inox/ast/ProgramEncoder.scala b/src/main/scala/inox/ast/ProgramEncoder.scala
index 0d60a6ed6..ec40e5f9e 100644
--- a/src/main/scala/inox/ast/ProgramEncoder.scala
+++ b/src/main/scala/inox/ast/ProgramEncoder.scala
@@ -83,5 +83,19 @@ object ProgramEncoder {
     protected object encoder extends p.trees.IdentityTreeTransformer
     protected object decoder extends p.trees.IdentityTreeTransformer
   }
+
+  def apply(p: Program)(tr: SymbolTransformer { val s: p.trees.type; val t: p.trees.type }): ProgramEncoder {
+    val sourceProgram: p.type
+    val t: p.trees.type
+  } = new ProgramEncoder {
+    val sourceProgram: p.type = p
+    val t: p.trees.type = p.trees
+
+    override protected def encodedProgram: Program { val trees: p.trees.type } = p.transform(tr)
+
+    protected object encoder extends p.trees.IdentityTreeTransformer
+    protected object decoder extends p.trees.IdentityTreeTransformer
+  }
+
 }
 
diff --git a/src/main/scala/inox/transformers/Collector.scala b/src/main/scala/inox/transformers/Collector.scala
index 191e3c73a..aef262a8a 100644
--- a/src/main/scala/inox/transformers/Collector.scala
+++ b/src/main/scala/inox/transformers/Collector.scala
@@ -13,11 +13,15 @@ trait Collector extends Transformer {
 
   import trees._
 
+  protected def accumulate(e: Expr, env: Env): Unit = {
+    results ++= step(e, env)
+  }
+
   /** Does one step of collection for the current [[Expr]] and [[Env]] */
   protected def step(e: Expr, env: Env): List[Result]
 
   abstract override protected def rec(e: Expr, current: Env): Expr = {
-    results ++= step(e, current)
+    accumulate(e, current)
     super.rec(e, current)
   }
 
-- 
GitLab