diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 3ca73c672705dcfe6c19e5275ad7a70287ccda2a..5b6147c055672096f1e68a8718b6ba07013bf6d9 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -15,12 +15,16 @@ import Types._
*
* The constructors implement some logic to simplify the tree and
* potentially use a different expression node if one is more suited.
- */
+ * @define encodingof Encoding of
+ * */
object Constructors {
- // If isTuple, the whole expression is returned. This is to avoid a situation
- // like tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> x, which is not expected.
- // Instead, tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> Tuple(x,y).
+ /** If `isTuple`, the whole expression is returned. This is to avoid a situation like
+ * `tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> x`, which is not expected.
+ * Instead,
+ * `tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> Tuple(x,y)`.
+ * @see [[purescala.Expressions.TupleSelect]]
+ */
def tupleSelect(t: Expr, index: Int, isTuple: Boolean): Expr = t match {
case Tuple(es) if isTuple => es(index-1)
case _ if t.getType.isInstanceOf[TupleType] && isTuple =>
@@ -30,14 +34,24 @@ object Constructors {
sys.error(s"Calling tupleSelect on non-tuple $t")
}
+ /** Simplifies the construct `TupleSelect(expr, index, originalSize > 1)`
+ * @param originalSize The arity of the tuple. If less or equal to 1, the whole expression is returned.
+ * @see [[purescala.Expressions.TupleSelect]]
+ */
def tupleSelect(t: Expr, index: Int, originalSize: Int): Expr = tupleSelect(t, index, originalSize > 1)
+ /** $encodingof ``val id = e; bd`, and returns `bd` if the identifier is not bound in `bd`.
+ * @see [[purescala.Expressions.Let]]
+ */
def let(id: Identifier, e: Expr, bd: Expr) = {
if (variablesOf(bd) contains id)
Let(id, e, bd)
else bd
}
+ /** $encodingof ``val (id1, id2, ...) = e; bd`, and returns `bd` if the identifiers are not bound in `bd`.
+ * @see [[purescala.Expressions.Let]]
+ */
def letTuple(binders: Seq[Identifier], value: Expr, body: Expr) = binders match {
case Nil =>
body
@@ -52,25 +66,40 @@ object Constructors {
Extractors.LetPattern(TuplePattern(None,binders map { b => WildcardPattern(Some(b)) }), value, body)
}
+ /** Wraps the sequence of expressions as a tuple. If the sequence contains a single expression, it is returned instead.
+ * @see [[purescala.Expressions.Tuple]]
+ */
def tupleWrap(es: Seq[Expr]): Expr = es match {
case Seq() => UnitLiteral()
case Seq(elem) => elem
case more => Tuple(more)
}
+ /** Wraps the sequence of patterns as a tuple. If the sequence contains a single pattern, it is returned instead.
+ * If the sequence is empty, [[purescala.Expressions.LiteralPattern `LiteralPattern`]]`(None, `[[purescala.Expressions.UnitLiteral `UnitLiteral`]]`())` is returned.
+ * @see [[purescala.Expressions.TuplePattern]]
+ * @see [[purescala.Expressions.LiteralPattern]]
+ */
def tuplePatternWrap(ps: Seq[Pattern]) = ps match {
case Seq() => LiteralPattern(None, UnitLiteral())
case Seq(elem) => elem
case more => TuplePattern(None, more)
}
+ /** Wraps the sequence of types as a tuple. If the sequence contains a single type, it is returned instead.
+ * If the sequence is empty, the [[purescala.Types.UnitType UnitType]] is returned.
+ * @see [[purescala.Types.TupleType]]
+ */
def tupleTypeWrap(tps : Seq[TypeTree]) = tps match {
case Seq() => UnitType
case Seq(elem) => elem
case more => TupleType(more)
}
- /** Will instantiate the type parameters of the function according to argument types */
+ /** Instantiates the type parameters of the function according to argument types
+ * @return A [[purescala.Expressions.FunctionInvocation FunctionInvocation]] if it type checks, else throws an error.
+ * @see [[purescala.Expressions.FunctionInvocation]]
+ */
def functionInvocation(fd : FunDef, args : Seq[Expr]) = {
require(fd.params.length == args.length, "Invoking function with incorrect number of arguments")
@@ -83,9 +112,11 @@ object Constructors {
FunctionInvocation(fd.typed(fd.tparams map { tpd => tmap.getOrElse(tpd.tp, tpd.tp) }), args)
case None => sys.error(s"$actualType cannot be a subtype of $formalType!")
}
-
}
+ /** Simplifies the provided case class selector.
+ * @see [[purescala.Expressions.CaseClassSelector]]
+ */
def caseClassSelector(classType: CaseClassType, caseClass: Expr, selector: Identifier): Expr = {
caseClass match {
case CaseClass(ct, fields) if ct.classDef == classType.classDef =>
@@ -95,6 +126,10 @@ object Constructors {
}
}
+ /** $encoding of `case ... if ... => ... ` but simplified if possible, based on types of the encompassing [[purescala.Expressions.CaseClassPattern MatchExpr]].
+ * @see [[purescala.Expressions.CaseClassPattern MatchExpr]]
+ * @see [[purescala.Expressions.CaseClassPattern CaseClassPattern]]
+ */
private def filterCases(scrutType : TypeTree, resType: Option[TypeTree], cases: Seq[MatchCase]): Seq[MatchCase] = {
val casesFiltered = scrutType match {
case c: CaseClassType =>
@@ -118,6 +153,9 @@ object Constructors {
}
}
+ /** $encodingof the I/O example specification, simplified to '''true''' if the cases are trivially true.
+ * @see [[purescala.Expressions.Passes Passes]]
+ */
def passes(in : Expr, out : Expr, cases : Seq[MatchCase]): Expr = {
val resultingCases = filterCases(in.getType, Some(out.getType), cases)
if (resultingCases.nonEmpty) {
@@ -126,7 +164,9 @@ object Constructors {
BooleanLiteral(true)
}
}
-
+ /** $encodingof `... match { ... }` but simplified if possible. Throws an error if no case can match the scrutined expression.
+ * @see [[purescala.Expressions.MatchExpr MatchExpr]]
+ */
def matchExpr(scrutinee : Expr, cases : Seq[MatchCase]) : Expr ={
val filtered = filterCases(scrutinee.getType, None, cases)
if (filtered.nonEmpty)
@@ -137,9 +177,10 @@ object Constructors {
"No case matches the scrutinee"
)
}
-
-
-
+
+ /** $encodingof `&&`-expressions with arbitrary number of operands, and simplified.
+ * @see [[purescala.Expressions.And And]]
+ */
def and(exprs: Expr*): Expr = {
val flat = exprs.flatMap {
case And(es) => es
@@ -159,8 +200,14 @@ object Constructors {
}
}
+ /** $encodingof `&&`-expressions with arbitrary number of operands as a sequence, and simplified.
+ * @see [[purescala.Expressions.And And]]
+ */
def andJoin(es: Seq[Expr]) = and(es :_*)
+ /** $encodingof `||`-expressions with arbitrary number of operands, and simplified.
+ * @see [[purescala.Expressions.Or Or]]
+ */
def or(exprs: Expr*): Expr = {
val flat = exprs.flatMap {
case Or(es) => es
@@ -180,14 +227,23 @@ object Constructors {
}
}
+ /** $encodingof `||`-expressions with arbitrary number of operands as a sequence, and simplified.
+ * @see [[purescala.Expressions.Or Or]]
+ */
def orJoin(es: Seq[Expr]) = or(es :_*)
+ /** $encodingof simplified `!`-expressions .
+ * @see [[purescala.Expressions.Not Not]]
+ */
def not(e: Expr): Expr = e match {
case Not(e) => e
case BooleanLiteral(v) => BooleanLiteral(!v)
case _ => Not(e)
}
+ /** $encodingof simplified `... ==> ...` (implication)
+ * @see [[purescala.Expressions.Implies Implies]]
+ */
def implies(lhs: Expr, rhs: Expr): Expr = (lhs, rhs) match {
case (BooleanLiteral(false), _) => BooleanLiteral(true)
case (_, BooleanLiteral(true)) => BooleanLiteral(true)
@@ -197,32 +253,42 @@ object Constructors {
case _ => Implies(lhs, rhs)
}
+ /** $encodingof Simplified `Array(...)` (array length defined at compile-time)
+ * @see [[purescala.Expressions.NonemptyArray NonemptyArray]]
+ */
def finiteArray(els: Seq[Expr]): Expr = {
require(els.nonEmpty)
finiteArray(els, None, Untyped) // Untyped is not correct, but will not be used anyway
}
-
+ /** $encodingof Simplified `Array[...](...)` (array length and default element defined at run-time) with type information
+ * @see [[purescala.Constructors#finiteArray(els:Map* finiteArray]]
+ */
def finiteArray(els: Seq[Expr], defaultLength: Option[(Expr, Expr)], tpe: TypeTree): Expr = {
finiteArray(els.zipWithIndex.map{ _.swap }.toMap, defaultLength, tpe)
}
-
+ /** $encodingof Simplified `Array[...](...)` (array length and default element defined at run-time) with type information
+ * @see [[purescala.Expressions.EmptyArray EmptyArray]]
+ */
def finiteArray(els: Map[Int, Expr], defaultLength: Option[(Expr, Expr)], tpe: TypeTree): Expr = {
if (els.isEmpty && defaultLength.isEmpty) EmptyArray(tpe)
else NonemptyArray(els, defaultLength)
}
-
+ /** $encodingof simplified `Array(...)` (array length and default element defined at run-time).
+ * @see [[purescala.Expressions.NonemptyArray NonemptyArray]]
+ */
def nonemptyArray(els: Seq[Expr], defaultLength: Option[(Expr, Expr)]): Expr = {
NonemptyArray(els.zipWithIndex.map{ _.swap }.toMap, defaultLength)
}
- /*
- * Take a mapping from keys to values and a default expression and return a lambda of the form
- * (x1, ..., xn) =>
- * if ( key1 == (x1, ..., xn) ) value1
- * else if ( key2 == (x1, ..., xn) ) value2
- * ...
- * else default
- */
+ /** Takes a mapping from keys to values and a default expression and return a lambda of the form
+ * {{{
+ * (x1, ..., xn) =>
+ * if ( key1 == (x1, ..., xn) ) value1
+ * else if ( key2 == (x1, ..., xn) ) value2
+ * ...
+ * else default
+ * }}}
+ */
def finiteLambda(default: Expr, els: Seq[(Expr, Expr)], inputTypes: Seq[TypeTree]): Lambda = {
val args = inputTypes map { tpe => ValDef(FreshIdentifier("x", tpe, true)) }
val argsExpr = tupleWrap(args map { _.toVariable })
@@ -231,7 +297,9 @@ object Constructors {
}
Lambda(args, body)
}
-
+ /** $encodingof simplified `... == ...` (equality).
+ * @see [[purescala.Expressions.Equals Equals]]
+ */
def equality(a: Expr, b: Expr) = {
if (a == b && isDeterministic(a)) {
BooleanLiteral(true)
@@ -240,6 +308,10 @@ object Constructors {
}
}
+ /** $encodingof simplified `fn(realArgs)` (function application).
+ * @see [[purescala.Expressions.Lambda Lambda]]
+ * @see [[purescala.Expressions.Application Application]]
+ */
def application(fn: Expr, realArgs: Seq[Expr]) = fn match {
case Lambda(formalArgs, body) =>
assert(realArgs.size == formalArgs.size, "Invoking lambda with incorrect number of arguments")
@@ -262,6 +334,11 @@ object Constructors {
Application(fn, realArgs)
}
+ /** $encodingof simplified `... + ...` (plus).
+ * @see [[purescala.Expressions.Plus Plus]]
+ * @see [[purescala.Expressions.BVPlus BVPlus]]
+ * @see [[purescala.Expressions.RealPlus RealPlus]]
+ */
def plus(lhs: Expr, rhs: Expr): Expr = (lhs, rhs) match {
case (InfiniteIntegerLiteral(bi), _) if bi == 0 => rhs
case (_, InfiniteIntegerLiteral(bi)) if bi == 0 => lhs
@@ -274,6 +351,11 @@ object Constructors {
case (IsTyped(_, RealType), IsTyped(_, RealType)) => RealPlus(lhs, rhs)
}
+ /** $encodingof simplified `... - ...` (minus).
+ * @see [[purescala.Expressions.Minus Minus]]
+ * @see [[purescala.Expressions.BVMinus BVMinus]]
+ * @see [[purescala.Expressions.RealMinus RealMinus]]
+ */
def minus(lhs: Expr, rhs: Expr): Expr = (lhs, rhs) match {
case (_, InfiniteIntegerLiteral(bi)) if bi == 0 => lhs
case (_, IntLiteral(0)) => lhs
@@ -284,6 +366,11 @@ object Constructors {
case (IsTyped(_, RealType), IsTyped(_, RealType)) => RealMinus(lhs, rhs)
}
+ /** $encodingof simplified `... * ...` (times).
+ * @see [[purescala.Expressions.Times Times]]
+ * @see [[purescala.Expressions.BVTimes BVTimes]]
+ * @see [[purescala.Expressions.RealTimes RealTimes]]
+ */
def times(lhs: Expr, rhs: Expr): Expr = (lhs, rhs) match {
case (InfiniteIntegerLiteral(bi), _) if bi == 1 => rhs
case (_, InfiniteIntegerLiteral(bi)) if bi == 1 => lhs
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 684dfce59eb97c476284faeffb22e398e6e9b973..918fa363c0e64c32916922ae012e09940441bb15 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -42,16 +42,15 @@ object ExprOps {
*/
- /**
- * Do a right tree fold
+ /** Does a right tree fold
*
* A right tree fold applies the input function to the subnodes first (from left
* to right), and combine the results along with the current node value.
*
* @param f a function that takes the current node and the seq
* of results form the subtrees.
- * @param e the Expr on which to apply the fold.
- * @return The expression after applying ``f`` on all subtrees.
+ * @param e The Expr on which to apply the fold.
+ * @return The expression after applying `f` on all subtrees.
* @note the computation is lazy, hence you should rely on side-effects of `f`
*/
def foldRight[T](f: (Expr, Seq[T]) => T)(e: Expr): T = {
@@ -63,9 +62,9 @@ object ExprOps {
f(e, es.view.map(rec))
}
- /** pre-traversal of the tree.
+ /** Pre-traversal of the tree.
*
- * invokes the input function on every node *before* visiting
+ * Invokes the input function on every node '''before''' visiting
* children. Traverse children from left to right subtrees.
*
* e.g.
@@ -87,9 +86,9 @@ object ExprOps {
es.foreach(rec)
}
- /** post-traversal of the tree.
+ /** Post-traversal of the tree.
*
- * Invokes the input function on every node *after* visiting
+ * Invokes the input function on every node '''after''' visiting
* children.
*
* e.g.
@@ -111,10 +110,10 @@ object ExprOps {
f(e)
}
- /** pre-transformation of the tree.
+ /** Pre-transformation of the tree.
*
- * takes a partial function of replacements and substitute
- * *before* recursing down the trees.
+ * Takes a partial function of replacements and substitute
+ * '''before''' recursing down the trees.
*
* Supports two modes :
*
@@ -162,10 +161,10 @@ object ExprOps {
}
}
- /** post-transformation of the tree.
+ /** Post-transformation of the tree.
*
- * takes a partial function of replacements.
- * Substitutes *after* recursing down the trees.
+ * Takes a partial function of replacements.
+ * Substitutes '''after''' recursing down the trees.
*
* Supports two modes :
*
@@ -189,7 +188,7 @@ object ExprOps {
* Add(a, f)
* }}}
*
- * @note The mode with applyRec true can diverge if f is not well formed
+ * @note The mode with applyRec true can diverge if f is not well formed (i.e. not convergent)
*/
def postMap(f: Expr => Option[Expr], applyRec : Boolean = false)(e: Expr): Expr = {
val rec = postMap(f, applyRec) _
@@ -262,11 +261,12 @@ object ExprOps {
* Convenient methods using the Core API.
*/
- /** check if the predicate holds in some sub-expression */
+ /** Checks if the predicate holds in some sub-expression */
def exists(matcher: Expr => Boolean)(e: Expr): Boolean = {
foldRight[Boolean]({ (e, subs) => matcher(e) || subs.contains(true) } )(e)
}
+ /** Collects a set of objects from all sub-expressions */
def collect[T](matcher: Expr => Set[T])(e: Expr): Set[T] = {
foldRight[Set[T]]({ (e, subs) => matcher(e) ++ subs.flatten } )(e)
}
@@ -275,19 +275,22 @@ object ExprOps {
foldRight[Seq[T]]({ (e, subs) => matcher(e) ++ subs.flatten } )(e)
}
+ /** Returns a set of all sub-expressions matching the predicate */
def filter(matcher: Expr => Boolean)(e: Expr): Set[Expr] = {
collect[Expr] { e => if (matcher(e)) Set(e) else Set() }(e)
}
- /** Count how many times the predicate holds in sub-expressions */
+ /** Counts how many times the predicate holds in sub-expressions */
def count(matcher: Expr => Int)(e: Expr): Int = {
foldRight[Int]({ (e, subs) => matcher(e) + subs.sum } )(e)
}
+ /** Replaces bottom-up sub-expressions by looking up for them in a map */
def replace(substs: Map[Expr,Expr], expr: Expr) : Expr = {
postMap(substs.lift)(expr)
}
+ /** Replaces bottom-up sub-expressions by looking up for them in the provided order */
def replaceSeq(substs: Seq[(Expr, Expr)], expr: Expr): Expr = {
var res = expr
for (s <- substs) {
@@ -296,7 +299,7 @@ object ExprOps {
res
}
-
+ /** Replaces bottom-up sub-identifiers by looking up for them in a map */
def replaceFromIDs(substs: Map[Identifier, Expr], expr: Expr) : Expr = {
postMap({
case Variable(i) => substs.get(i)
@@ -304,6 +307,7 @@ object ExprOps {
})(expr)
}
+ /** Returns the set of identifiers in an expression */
def variablesOf(expr: Expr): Set[Identifier] = {
foldRight[Set[Identifier]]{
case (e, subs) =>
@@ -321,6 +325,7 @@ object ExprOps {
}(expr)
}
+ /** Returns true if the expression contains a function call */
def containsFunctionCalls(expr: Expr): Boolean = {
exists{
case _: FunctionInvocation => true
@@ -328,7 +333,7 @@ object ExprOps {
}(expr)
}
- /** Returns all Function calls found in an expression */
+ /** Returns all Function calls found in the expression */
def functionCallsOf(expr: Expr): Set[FunctionInvocation] = {
collect[FunctionInvocation] {
case f: FunctionInvocation => Set(f)
@@ -344,6 +349,7 @@ object ExprOps {
}(e)
}
+ /** Computes the negation of a boolean formula in Negation Normal Form. */
def negate(expr: Expr) : Expr = {
require(expr.getType == BooleanType)
(expr match {
@@ -362,8 +368,9 @@ object ExprOps {
}).setPos(expr)
}
- // rewrites pattern-matching expressions to use fresh variables for the binders
- // ATTENTION: Unused, and untested
+ /** ATTENTION: Unused, and untested
+ * rewrites pattern-matching expressions to use fresh variables for the binders
+ */
def freshenLocals(expr: Expr) : Expr = {
def rewritePattern(p: Pattern, sm: Map[Identifier,Identifier]) : Pattern = p match {
case InstanceOfPattern(ob, ctd) => InstanceOfPattern(ob map sm, ctd)
@@ -403,10 +410,12 @@ object ExprOps {
}(expr)
}
+ /** Computes the depth of the expression's tree */
def depth(e: Expr): Int = {
foldRight[Int]{ (e, sub) => 1 + (0 +: sub).max }(e)
}
+ /** Applies the function to the I/O constraint and simplifies the resulting constraint */
def applyAsMatches(p : Passes, f : Expr => Expr) = {
f(p.asConstraint) match {
case Equals(newOut, MatchExpr(newIn, newCases)) => {
@@ -420,6 +429,7 @@ object ExprOps {
}
}
+ /** Normalizes the expression expr */
def normalizeExpression(expr: Expr) : Expr = {
def rec(e: Expr): Option[Expr] = e match {
case TupleSelect(Let(id, v, b), ts) =>
@@ -453,10 +463,16 @@ object ExprOps {
fixpoint(postMap(rec))(expr)
}
+ /** Returns '''true''' if the formula is Ground,
+ * which means that it does not contain any variable ([[purescala.ExprOps#variablesOf]] e is empty)
+ * and [[purescala.ExprOps#isDeterministic isDeterministic]]
+ */
def isGround(e: Expr): Boolean = {
variablesOf(e).isEmpty && isDeterministic(e)
}
+ /** Returns a function which can simplify all ground expressions which appear in a program context.
+ */
def evalGround(ctx: LeonContext, program: Program): Expr => Expr = {
import evaluators._
@@ -721,6 +737,23 @@ object ExprOps {
recBinder(in, pattern).filter{ case (a, b) => a != b }
}
+ /** Recursively transforms a pattern on a boolean formula expressing the conditions for the input expression, possibly including name binders
+ *
+ * For example, the following pattern on the input `i`
+ * {{{
+ * case m @ MyCaseClass(t: B, (_, 7)) =>
+ * }}}
+ * will yield the following condition before simplification (to give some flavour)
+ *
+ * {{{and(IsInstanceOf(MyCaseClass, i), and(Equals(m, i), InstanceOfClass(B, i.t), equals(i.k.arity, 2), equals(i.k._2, 7))) }}}
+ *
+ * Pretty-printed, this would be:
+ * {{{
+ * i.instanceOf[MyCaseClass] && m == i && i.t.instanceOf[B] && i.k.instanceOf[Tuple2] && i.k._2 == 7
+ * }}}
+ *
+ * @see [[purescala.Expressions.Pattern]]
+ */
def conditionForPattern(in: Expr, pattern: Pattern, includeBinders: Boolean = false): Expr = {
def bind(ob: Option[Identifier], to: Expr): Expr = {
if (!includeBinders) {
@@ -770,6 +803,7 @@ object ExprOps {
rec(in, pattern)
}
+ /** Converts the pattern applied to an input to a map between identifiers and expressions */
def mapForPattern(in: Expr, pattern: Pattern) : Map[Identifier,Expr] = {
def bindIn(id: Option[Identifier]): Map[Identifier,Expr] = id match {
case None => Map()
@@ -802,8 +836,7 @@ object ExprOps {
}
/** Rewrites all pattern-matching expressions into if-then-else expressions
- *
- * Introduce additional error conditions. Does not introduce additional variables.
+ * Introduces additional error conditions. Does not introduce additional variables.
*/
def matchToIfThenElse(expr: Expr): Expr = {
@@ -842,6 +875,13 @@ object ExprOps {
preMap(rewritePM)(expr)
}
+ /** For each case in the [[purescala.Expressions.MatchExpr MatchExpr]], concatenates the path condition with the newly induced conditions.
+ *
+ * Each case holds the conditions on other previous cases as negative.
+ *
+ * @see [[purescala.ExprOps#conditionForPattern conditionForPattern]]
+ * @see [[purescala.ExprOps#mapForPattern mapForPattern]]
+ */
def matchExprCaseConditions(m: MatchExpr, pathCond: List[Expr]) : Seq[List[Expr]] = {
val MatchExpr(scrut, cases) = m
var pcSoFar = pathCond
@@ -860,7 +900,7 @@ object ExprOps {
}
}
- // Condition to pass this match case, expressed w.r.t scrut only
+ /** Condition to pass this match case, expressed w.r.t scrut only */
def matchCaseCondition(scrut: Expr, c: MatchCase): Expr = {
val patternC = conditionForPattern(scrut, c.pattern, includeBinders = false)
@@ -876,12 +916,16 @@ object ExprOps {
}
}
+ /** Returns the path conditions for each of the case passes.
+ *
+ * Each case holds the conditions on other previous cases as negative.
+ */
def passesPathConditions(p : Passes, pathCond: List[Expr]) : Seq[List[Expr]] = {
matchExprCaseConditions(MatchExpr(p.in, p.cases), pathCond)
}
- /*
- * Returns a pattern and a guard, if needed
+ /**
+ * Returns a pattern from an expression, and a guard if any.
*/
def expressionToPattern(e : Expr) : (Pattern, Expr) = {
var guard : Expr = BooleanLiteral(true)
@@ -898,10 +942,9 @@ object ExprOps {
(rec(e), guard)
}
-
/**
* Takes a pattern and returns an expression that corresponds to it.
- * Also returns a sequence of (Identifier -> Expr) pairs which
+ * Also returns a sequence of `Identifier -> Expr` pairs which
* represent the bindings for intermediate binders (from outermost to innermost)
*/
def patternToExpression(p: Pattern, expectedType: TypeTree): (Expr, Seq[(Identifier, Expr)]) = {
@@ -1009,9 +1052,9 @@ object ExprOps {
case _ => throw new Exception("I can't choose simplest value for type " + tpe)
}
- /** hoists all IfExpr at top level.
+ /** Hoists all IfExpr at top level.
*
- * Guarentees that all IfExpr will be at the top level and as soon as you
+ * Guarantees that all IfExpr will be at the top level and as soon as you
* encounter a non-IfExpr, then no more IfExpr can be found in the
* sub-expressions
*
@@ -1183,10 +1226,12 @@ object ExprOps {
es.map(formulaSize).sum+1
}
+ /** Return a list of all [[purescala.Expressions.Choose Choose]] construct inside the expression */
def collectChooses(e: Expr): List[Choose] = {
new ChooseCollectorWithPaths().traverse(e).map(_._1).toList
}
+ /** Returns true if the expression is deterministic / does not contain any [[purescala.Expressions.Choose Choose]] or [[purescala.Expressions.Hole Hole]]*/
def isDeterministic(e: Expr): Boolean = {
preTraversal{
case Choose(_) => return false
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 7dfb82ff1f3c4ea144636706e391560bc554ed16..a11e542297b0fe6a4745966f41cc755755c966cd 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -1,7 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-package leon
-package purescala
+package leon.purescala
import Common._
import Types._
@@ -276,6 +275,7 @@ object Expressions {
case class InstanceOfPattern(binder: Option[Identifier], ct: ClassType) extends Pattern { // c: Class
val subPatterns = Seq()
}
+ /** Pattern encoding `case binder @ _ => ` with optional identifier `binder` */
case class WildcardPattern(binder: Option[Identifier]) extends Pattern { // c @ _
val subPatterns = Seq()
}
@@ -328,10 +328,14 @@ object Expressions {
)
}
- /** Symbolic IO examples as a match/case
+ /** Symbolic I/O examples as a match/case.
+ * $encodingof `out == in match { cases }`
*
* If you are not sure about the requirement you should use
* [[purescala.Constructors#passes purescala's constructor passes]]
+ *
+ * @param in
+ * @param out
*/
case class Passes(in: Expr, out : Expr, cases : Seq[MatchCase]) extends Expr {
require(cases.nonEmpty)
@@ -341,6 +345,7 @@ object Expressions {
case Some(_) => BooleanType
}
+ /** Transforms the set of I/O examples to a constraint equality. */
def asConstraint = {
val defaultCase = SimpleCase(WildcardPattern(None), out)
Equals(out, MatchExpr(in, cases :+ defaultCase))
@@ -352,25 +357,27 @@ object Expressions {
sealed abstract class Literal[+T] extends Expr with Terminal {
val value: T
}
-
+ /** $encodingof a char literal */
case class CharLiteral(value: Char) extends Literal[Char] {
val getType = CharType
}
-
+ /** $encodingof an integer literal */
case class IntLiteral(value: Int) extends Literal[Int] {
val getType = Int32Type
}
+ /** $encodingof a big integer literal */
case class InfiniteIntegerLiteral(value: BigInt) extends Literal[BigInt] {
val getType = IntegerType
}
+ /** $encodingof a real literal */
case class RealLiteral(value: BigDecimal) extends Literal[BigDecimal] {
val getType = RealType
}
-
+ /** $encodingof a boolean literal '''true''' or '''false''' */
case class BooleanLiteral(value: Boolean) extends Literal[Boolean] {
val getType = BooleanType
}
-
+ /** $encodingof a unit literal `()` */
case class UnitLiteral() extends Literal[Unit] {
val getType = UnitType
val value = ()
@@ -378,8 +385,8 @@ object Expressions {
/** Generic values. Represent values of the generic type `tp` */
- // TODO: Is it valid that GenericValue(tp, 0) != GenericValue(tp, 1)?
case class GenericValue(tp: TypeParameter, id: Int) extends Expr with Terminal {
+ // TODO: Is it valid that GenericValue(tp, 0) != GenericValue(tp, 1)?
val getType = tp
}
@@ -463,7 +470,11 @@ object Expressions {
def apply(a: Expr, b: Expr): Expr = Or(Seq(a, b))
}
- /** Locical Implication */
+ /** $encodingof `... ==> ...` (logical implication)
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#implies purescala's constructor implies]]
+ */
case class Implies(lhs: Expr, rhs: Expr) extends Expr {
val getType = {
if(lhs.getType == BooleanType && rhs.getType == BooleanType) BooleanType
@@ -660,6 +671,8 @@ object Expressions {
*
* If you are not sure about the requirement you should use
* [[purescala.Constructors#tupleWrap purescala's constructor tupleWrap]]
+ *
+ * @param exprs The expressions in the tuple
*/
case class Tuple (exprs: Seq[Expr]) extends Expr {
require(exprs.size >= 2)
@@ -771,7 +784,10 @@ object Expressions {
val getType = Int32Type
}
- /** $encodingof `array.nonempty` */
+ /** $encodingof Array(...) with predetermined elements
+ * @param elems The map from the position to the elements.
+ * @param defaultLength An optional pair where the first element is the default value and the second is the size of the array.
+ */
case class NonemptyArray(elems: Map[Int, Expr], defaultLength: Option[(Expr, Expr)]) extends Expr {
private val elements = elems.values.toList ++ defaultLength.map{_._1}
val getType = ArrayType(optionToType(leastUpperBound(elements map { _.getType}))).unveilUntyped