From ffaae455670db62698adc234c28fabc8490803e7 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 10 Aug 2016 10:23:01 +0200
Subject: [PATCH] Documentation
---
src/main/scala/inox/ast/Definitions.scala | 79 ++++++++++++++---------
src/main/scala/inox/ast/Expressions.scala | 36 ++++-------
2 files changed, 63 insertions(+), 52 deletions(-)
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 4559bc702..69f9b2269 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -5,8 +5,10 @@ package ast
import scala.collection.mutable.{Map => MutableMap}
+/** Provides types that describe Inox definitions. */
trait Definitions { self: Trees =>
+ /** The base trait for Inox definitions */
sealed trait Definition extends Tree {
val id: Identifier
@@ -82,7 +84,7 @@ trait Definitions { self: Trees =>
type Symbols >: Null <: AbstractSymbols
- /** A wrapper for a program. For now a program is simply a single object. */
+ /** Provides the class and function definitions of a program and lookups on them */
trait AbstractSymbols
extends Printable
with TypeOps
@@ -158,12 +160,14 @@ trait Definitions { self: Trees =>
// Compiler annotations given in the source code as @annot
case class Annotation(annot: String, args: Seq[Option[Any]]) extends FunctionFlag with ClassFlag
- // Class has ADT invariant method
+ /** Denotes that this class is refined by invariant ''id'' */
case class HasADTInvariant(id: Identifier) extends ClassFlag
// Is inlined
case object IsInlined extends FunctionFlag
- /** Represents a class definition (either an abstract- or a case-class) */
+ /** Represents a class definition (either an abstract- or a case-class).
+ * In functional terms, abstract classes are ADTs and case classes are ADT constructors.
+ */
sealed trait ClassDef extends Definition {
val id: Identifier
val tparams: Seq[TypeParameterDef]
@@ -172,7 +176,10 @@ trait Definitions { self: Trees =>
def annotations: Set[String] = extAnnotations.keySet
def extAnnotations: Map[String, Seq[Option[Any]]] = flags.collect { case Annotation(s, args) => s -> args }.toMap
+ /** The root of the class hierarchy */
def root(implicit s: Symbols): ClassDef
+
+ /** An invariant that refines this [[ClassDef]] */
def invariant(implicit s: Symbols): Option[FunDef] = {
val rt = root
if (rt ne this) rt.invariant
@@ -189,7 +196,7 @@ trait Definitions { self: Trees =>
def typed(implicit s: Symbols): TypedClassDef
}
- /** Abstract classes. */
+ /** Abstract classes / ADTs */
class AbstractClassDef(val id: Identifier,
val tparams: Seq[TypeParameterDef],
val children: Seq[Identifier],
@@ -232,7 +239,14 @@ trait Definitions { self: Trees =>
}
}
- /** Case classes/ case objects. */
+ /** Case classes/ ADT constructors. For single-case classes these may coincide
+ *
+ * @param id
+ * @param tparams
+ * @param parent
+ * @param fields
+ * @param flags
+ */
class CaseClassDef(val id: Identifier,
val tparams: Seq[TypeParameterDef],
val parent: Option[Identifier],
@@ -240,7 +254,7 @@ trait Definitions { self: Trees =>
val flags: Set[ClassFlag]) extends ClassDef {
val isAbstract = false
-
+ /** Returns the index of the field with the specified id */
def selectorID2Index(id: Identifier) : Int = {
val index = fields.indexWhere(_.id == id)
@@ -261,13 +275,14 @@ trait Definitions { self: Trees =>
}
}
+ /** Represents a [[ClassDef]] whose type parameters have been instantiated to ''tps'' */
sealed abstract class TypedClassDef extends Tree {
val cd: ClassDef
val tps: Seq[Type]
implicit val symbols: Symbols
val id: Identifier = cd.id
-
+ /** The root of the class hierarchy */
lazy val root: TypedClassDef = cd.root.typed(tps)
lazy val invariant: Option[TypedFunDef] = cd.invariant.map(_.typed(tps))
lazy val hasInvariant: Boolean = invariant.isDefined
@@ -285,10 +300,12 @@ trait Definitions { self: Trees =>
}
}
+ /** Represents an [[AbstractClassDef]] whose type parameters have been instantiated to ''tps'' */
case class TypedAbstractClassDef(cd: AbstractClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
def descendants: Seq[TypedCaseClassDef] = cd.descendants.map(_.typed(tps))
}
+ /** Represents a [[CaseClassDef]] whose type parameters have been instantiated to ''tps'' */
case class TypedCaseClassDef(cd: CaseClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
lazy val fields: Seq[ValDef] = {
val tmap = (cd.typeArgs zip tps).toMap
@@ -305,18 +322,11 @@ trait Definitions { self: Trees =>
}
- /** Function/method definition.
- *
- * This class represents methods or fields of objects or classes. By "fields" we mean
- * fields defined in the body of a class/object, not the constructor arguments of a case class
- * (those are accessible through [[leon.purescala.Definitions.ClassDef.fields]]).
+ /** Function definition
*
- * When it comes to verification, all are treated the same (as functions).
- * They are only differentiated when it comes to code generation/ pretty printing.
- * By default, the FunDef represents a function/method as opposed to a field,
- * unless otherwise specified by its flags.
- *
- * Bear in mind that [[id]] will not be consistently typed.
+ * @param id The identifier which will refer to this function.
+ * @param body The optional body of this function. Empty body functions are treated as uninterpreted
+ * @param flags Flags that annotate this function with attributes.
*/
class FunDef(
val id: Identifier,
@@ -327,20 +337,20 @@ trait Definitions { self: Trees =>
val flags: Set[FunctionFlag]
) extends Definition {
- def hasBody = body.isDefined
+ def hasBody = body.isDefined
def annotations: Set[String] = extAnnotations.keySet
def extAnnotations: Map[String, Seq[Option[Any]]] = flags.collect {
case Annotation(s, args) => s -> args
}.toMap
- /* Wrapping in TypedFunDef */
-
+ /** Wraps this [[FunDef]] in a in [[TypedFunDef]] with the specified type parameters */
def typed(tps: Seq[Type])(implicit s: Symbols): TypedFunDef = {
assert(tps.size == tparams.size)
TypedFunDef(this, tps)
}
+ /** Wraps this [[FunDef]] in a in [[TypedFunDef]] with its own type parameters */
def typed(implicit s: Symbols): TypedFunDef = typed(tparams.map(_.tp))
/* Auxiliary methods */
@@ -349,12 +359,14 @@ trait Definitions { self: Trees =>
def typeArgs = tparams map (_.tp)
+ /** Applies this function on some arguments; type parameters are inferred. */
def applied(args: Seq[Expr])(implicit s: Symbols): FunctionInvocation = s.functionInvocation(this, args)
+ /** Applies this function on its formal parameters */
def applied = FunctionInvocation(id, typeArgs, params map (_.toVariable))
}
- // Wrapper for typing function according to valuations for type parameters
+ /** Represents a [[FunDef]] whose type parameters have been instantiated with the specified types */
case class TypedFunDef(fd: FunDef, tps: Seq[Type])(implicit symbols: Symbols) extends Tree {
val id = fd.id
@@ -370,13 +382,15 @@ trait Definitions { self: Trees =>
(fd.typeArgs zip tps).toMap.filter(tt => tt._1 != tt._2)
}
- def translated(t: Type): Type = symbols.instantiateType(t, typesMap)
+ /** A [[Type]] instantiated with this [[TypedFunDef]]'s type instantiation */
+ def instantiate(t: Type): Type = symbols.instantiateType(t, typesMap)
- def translated(e: Expr): Expr = symbols.instantiateType(e, typesMap)
+ /** A [[Expr]] instantiated with this [[TypedFunDef]]'s type instantiation */
+ def instantiate(e: Expr): Expr = symbols.instantiateType(e, typesMap)
/** A mapping from this [[TypedFunDef]]'s formal parameters to real arguments
*
- * @param realArgs The arguments to which the formal argumentas are mapped
+ * @param realArgs The arguments to which the formal arguments are mapped
*/
def paramSubst(realArgs: Seq[Expr]) = {
require(realArgs.size == params.size)
@@ -392,26 +406,31 @@ trait Definitions { self: Trees =>
exprOps.replaceFromSymbols(paramSubst(realArgs), e)
}
+ /** Apply this [[inox.ast.Definitions.TypedFunDef]] on specified arguments */
def applied(realArgs: Seq[Expr]): FunctionInvocation = {
FunctionInvocation(id, tps, realArgs)
}
+ /** Apply this [[inox.ast.Definitions.TypedFunDef]] on its formal parameters */
def applied: FunctionInvocation = applied(params map { _.toVariable })
- /** Params will contain ValDefs instantiated with the correct types */
+ /** The paremeters of the respective [[FunDef]] instantiated with the real type parameters */
lazy val params: Seq[ValDef] = {
if (typesMap.isEmpty) {
fd.params
} else {
- fd.params.map(vd => vd.copy(tpe = translated(vd.getType)))
+ fd.params.map(vd => vd.copy(tpe = instantiate(vd.getType)))
}
}
+ /** The function type corresponding to this [[TypedFunDef]]'s arguments and return type */
lazy val functionType = FunctionType(params.map(_.getType).toList, returnType)
- lazy val returnType: Type = translated(fd.returnType)
+ /** The return type of the respective [[FunDef]] instantiated with the real type parameters */
+ lazy val returnType: Type = instantiate(fd.returnType)
- lazy val body = fd.body map translated
- def hasBody = body.isDefined
+ /** The body of the respective [[FunDef]] instantiated with the real type parameters */
+ lazy val body = fd.body map instantiate
+ def hasBody = body.isDefined
}
}
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 2828e2cfe..24da96276 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -7,19 +7,11 @@ import scala.collection.BitSet
/** Expression definitions for Pure Scala.
*
- * If you are looking for things such as function or class definitions,
- * please have a look in [[purescala.Definitions]].
+ * Every expression in Inox inherits from [[Expressions.Expr]].
+ * Expressions can be manipulated with functions in [[Constructors]] and [[ExprOps]].
*
- * Every expression in Leon inherits from [[Expr]]. The AST definitions are simple
- * case classes, with no behaviour. In particular, they do not perform smart
- * rewriting. What you build is what you get. For example,
- * {{{
- * And(BooleanLiteral(true), Variable(id, BooleanType)) != Variable(id, BooleanType)
- * }}}
- * because the ``And`` constructor will simply build a tree without checking for
- * optimization opportunities. Unless you need exact control on the structure
- * of the trees, you should use constructors in [[purescala.Constructors]], that
- * simplify the trees they produce.
+ * If you are looking for things such as function or class definitions,
+ * please have a look in [[inox.ast.Definitions]].
*
* @define encodingof Encoding of
* @define noteBitvector (32-bit vector)
@@ -76,7 +68,7 @@ trait Expressions { self: Trees =>
* @param vd The ValDef used in body, defined just after '''val'''
* @param value The value assigned to the identifier, after the '''=''' sign
* @param body The expression following the ``val ... = ... ;`` construct
- * @see [[purescala.Constructors#let purescala's constructor let]]
+ * @see [[Constructors#let purescala's constructor let]]
*/
case class Let(vd: ValDef, value: Expr, body: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type = {
@@ -247,7 +239,7 @@ trait Expressions { self: Trees =>
/** $encodingof `value.selector` where value is of a case class type
*
* If you are not sure about the requirement you should use
- * [[purescala.Constructors#caseClassSelector purescala's constructor caseClassSelector]]
+ * [[Constructors#caseClassSelector purescala's constructor caseClassSelector]]
*/
case class CaseClassSelector(caseClass: Expr, selector: Identifier) extends Expr with CachingTyped {
@@ -287,8 +279,8 @@ trait Expressions { self: Trees =>
/** $encodingof `... && ...`
*
* [[exprs]] must contain at least two elements; if you are not sure about this,
- * you should use [[purescala.Constructors#and purescala's constructor and]]
- * or [[purescala.Constructors#andJoin purescala's constructor andJoin]]
+ * you should use [[Constructors#and purescala's constructor and]]
+ * or [[Constructors#andJoin purescala's constructor andJoin]]
*/
case class And(exprs: Seq[Expr]) extends Expr with CachingTyped {
require(exprs.size >= 2)
@@ -305,8 +297,8 @@ trait Expressions { self: Trees =>
/** $encodingof `... || ...`
*
* [[exprs]] must contain at least two elements; if you are not sure about this,
- * you should use [[purescala.Constructors#or purescala's constructor or]] or
- * [[purescala.Constructors#orJoin purescala's constructor orJoin]]
+ * you should use [[Constructors#or purescala's constructor or]] or
+ * [[Constructors#orJoin purescala's constructor orJoin]]
*/
case class Or(exprs: Seq[Expr]) extends Expr with CachingTyped {
require(exprs.size >= 2)
@@ -325,7 +317,7 @@ trait Expressions { self: Trees =>
* This is not a standard Scala operator, but it results from an implicit
* conversion in the Leon library.
*
- * @see [[leon.purescala.Constructors.implies]]
+ * @see [[Constructors.implies]]
*/
case class Implies(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type = {
@@ -336,7 +328,7 @@ trait Expressions { self: Trees =>
/** $encodingof `!...`
*
- * @see [[leon.purescala.Constructors.not]]
+ * @see [[Constructors.not]]
*/
case class Not(expr: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type = {
@@ -525,7 +517,7 @@ trait Expressions { self: Trees =>
*
* [[exprs]] should always contain at least 2 elements.
* If you are not sure about this requirement, you should use
- * [[leon.purescala.Constructors.tupleWrap purescala's constructor tupleWrap]]
+ * [[Constructors.tupleWrap purescala's constructor tupleWrap]]
*
* @param exprs The expressions in the tuple
*/
@@ -538,7 +530,7 @@ trait Expressions { self: Trees =>
*
* Index is 1-based, first element of tuple is 1.
* If you are not sure that [[tuple]] is indeed of a TupleType,
- * you should use [[leon.purescala.Constructors.tupleSelect(t:leon\.purescala\.Expressions\.Expr,index:Int,isTuple:Boolean):leon\.purescala\.Expressions\.Expr* purescala's constructor tupleSelect]]
+ * you should use [[Constructors.tupleSelect purescala's constructor tupleSelect]]
*/
case class TupleSelect(tuple: Expr, index: Int) extends Expr with CachingTyped {
require(index >= 1)
--
GitLab