Comments

src/main/scala/inox/Program.scala

@@ -4,6 +4,18 @@ package inox
 
 import ast._
 
+/** Contains all definitions required to construct a complete Inox program.
+  *
+  * The elements of this class are typed dependently on the type of ''trees'',
+  * which is an object containing classes for expressions, types and definitions
+  * used by this program.
+  *
+  * ''symbols'' contains the actual definitions (classes and functions) of the program.
+  *
+  * ''ctx'' provides configuration options.
+  *
+  * ''printerOpts'' provides options for tree printers.
+  */
 trait Program {
   val trees: Trees
   implicit val symbols: trees.Symbols

src/main/scala/inox/ast/Constructors.scala

@@ -264,7 +264,7 @@ trait Constructors {
     case _ => Times(lhs, rhs)
   }
 
-  /** $encodingof expr.asInstanceOf[tpe], returns `expr` it it already is of type `tpe`.  */
+  /** $encodingof expr.asInstanceOf[tpe], returns `expr` if it already is of type `tpe`.  */
   def asInstOf(expr: Expr, tpe: ClassType) = {
     if (symbols.isSubtypeOf(expr.getType, tpe)) {
       expr

src/main/scala/inox/package.scala

@@ -2,41 +2,17 @@
 
 /** Core package of the Inox solving interface
   *
-  * ==Structure==
-  * 
-  * Leon is organized similarly to a compiler with a concept of [[leon.Pipeline]]
-  * and [[leon.LeonPhase]]. The main phases of Leon are implemented in subpackages, with
-  * an overview of the role of each of them below.
-  * 
-  * The definition of the Pure Scala AST is in [[leon.purescala]]. Most of the other packages
-  * are articulated around the definitions of these ASTs. The [[leon.xlang]] provides extensions
-  * to the Pure Scala AST, but most of the other packages will ignore these extensions and
-  * assume a Pure Scala only AST.
-  * 
-  *   - [[leon.codegen]] provides bytecode generator for Leon programs. Enable the conversion of a [[leon.purescala.Definitions.Program]] to JVM bytecode.
-  * 
-  *   - [[leon.datagen]] provides a generator of expressions (trees), based on vanuatoo.
-  * 
-  *   - [[leon.evaluators]] implements different evaluators for Leon programs in Pure Scala. 
-  * 
-  *   - [[leon.frontends]] provides the different front-ends to Leon. Currently it only implements a scalac integration, but it could potentially support other language.
-  * 
-  *   - [[leon.purescala]] defines the core AST for Pure Scala. Also provides useful tree manipulation methods.
-  * 
-  *   - [[leon.repair]] implements the Repair module of Leon.
-  * 
-  *   - [[leon.solvers]] provides an interface and implementations to solvers for Pure Scala expressions. The solvers are typically wrappers around SMT solvers, with some additional algorithms to handle recursive function invocations.
-  * 
-  *   - [[leon.synthesis]] implements the Synthesis module of Leon.
-  * 
-  *   - [[leon.termination]] implements the termination checker of Leon.
-  * 
-  *   - [[leon.utils]]
-  * 
-  *   - [[leon.verification]] implements the verification module of Leon.
-  * 
-  *   - [[leon.xlang]] provides extensions to Pure Scala. In particular, it introduces some expressions to represent imperative programs. Also provides the code to map such programs to Pure Scala equivalent ones.
+  * == Structure ==
   *
+  * The package is organized in the following subpackages:
+  *
+  * [[inox.ast]]: Provides definitions for expressions, types and definitions,
+  *   as well as operations on them
+  * [[inox.datagen]]: Generators/enumerators for Inox expressions
+  * [[inox.evaluators]]: Evaluators of Inox expressions
+  * [[inox.solvers]]: Interfaces to SMT-solvers
+  * [[inox.transformers]]: Tree transformations for Inox expressions
+  * [[inox.utils]]: Utility methods
   */
 package object inox {
   implicit class BooleanToOption(cond: Boolean) {