diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 0be34a227e952eb5876440a21c388a78ba4b23aa..7a0a76427b085588831add1d3e7a18f44817b3ea 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1647,6 +1647,16 @@ object ExprOps {
* =================
*/
+ /** Replaces the precondition of an existing [[Expressions.Expr]] with a new one.
+ *
+ * If no precondition is provided, removes any existing precondition.
+ * Else, wraps the expression with a [[Expressions.Require]] clause referring to the new precondition.
+ *
+ * @param expr The current expression
+ * @param pred An optional precondition. Setting it to None removes any precondition.
+ * @see [[Expressions.Ensuring]]
+ * @see [[Expressions.Require]]
+ */
def withPrecondition(expr: Expr, pred: Option[Expr]): Expr = (pred, expr) match {
case (Some(newPre), Require(pre, b)) => Require(newPre, b)
case (Some(newPre), Ensuring(Require(pre, b), p)) => Ensuring(Require(newPre, b), p)
@@ -1657,6 +1667,16 @@ object ExprOps {
case (None, b) => b
}
+ /** Replaces the postcondition of an existing [[Expressions.Expr]] with a new one.
+ *
+ * If no postcondition is provided, removes any existing postcondition.
+ * Else, wraps the expression with a [[Expressions.Ensuring]] clause referring to the new postcondition.
+ *
+ * @param expr The current expression
+ * @param pred An optional postcondition. Setting it to None removes any postcondition.
+ * @see [[Expressions.Ensuring]]
+ * @see [[Expressions.Require]]
+ */
def withPostcondition(expr: Expr, oie: Option[Expr]) = (oie, expr) match {
case (Some(npost), Ensuring(b, post)) => Ensuring(b, npost)
case (Some(npost), b) => Ensuring(b, npost)
@@ -1664,6 +1684,14 @@ object ExprOps {
case (None, b) => b
}
+ /** Adds a body to a specification
+ *
+ * @param expr The specification expression [[Expressions.Ensuring]] or [[Expressions.Require]]. If none of these, the argument is discarded.
+ * @param body An option of [[Expressions.Expr]] possibly containing an expression body.
+ * @return The post/pre condition with the body. If no body is provided, returns [[Expressions.NoTree]]
+ * @see [[Expressions.Ensuring]]
+ * @see [[Expressions.Require]]
+ */
def withBody(expr: Expr, body: Option[Expr]) = expr match {
case Require(pre, _) => Require(pre, body.getOrElse(NoTree(expr.getType)))
case Ensuring(Require(pre, _), post) => Ensuring(Require(pre, body.getOrElse(NoTree(expr.getType))), post)
@@ -1671,6 +1699,15 @@ object ExprOps {
case _ => body.getOrElse(NoTree(expr.getType))
}
+ /** Extracts the body without its specification
+ *
+ * [[Expressions.Expr]] trees contain its specifications as part of certain nodes.
+ * This function helps extracting only the body part of an expression
+ *
+ * @return An option type with the resulting expression if not [[Expressions.NoTree]]
+ * @see [[Expressions.Ensuring]]
+ * @see [[Expressions.Require]]
+ */
def withoutSpec(expr: Expr) = expr match {
case Require(pre, b) => Option(b).filterNot(_.isInstanceOf[NoTree])
case Ensuring(Require(pre, b), post) => Option(b).filterNot(_.isInstanceOf[NoTree])
@@ -1678,17 +1715,20 @@ object ExprOps {
case b => Option(b).filterNot(_.isInstanceOf[NoTree])
}
+ /** Returns the precondition of an expression wrapped in Option */
def preconditionOf(expr: Expr) = expr match {
case Require(pre, _) => Some(pre)
case Ensuring(Require(pre, _), _) => Some(pre)
case b => None
}
+ /** Returns the postcondition of an expression wrapped in Option */
def postconditionOf(expr: Expr) = expr match {
case Ensuring(_, post) => Some(post)
case _ => None
}
+ /** Returns a tuple of precondition, the raw body and the postcondition of an expression */
def breakDownSpecs(e : Expr) = (preconditionOf(e), withoutSpec(e), postconditionOf(e))
def preTraversalWithParent(f: (Expr, Option[Tree]) => Unit, initParent: Option[Tree] = None)(e: Expr): Unit = {
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index c23aa1f6e0ee183e85df3f88448c727dc7df98f4..5a0626bd0c99f249b412076f87240ecfc05af7f8 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -26,6 +26,10 @@ import ExprOps.replaceFromIDs
* 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.
+ *
+ * @define encodingof Encoding of
+ * @define note_bitvector (32-bit vector)
+ * @define note_real (Real)
*/
object Expressions {
@@ -53,7 +57,7 @@ object Expressions {
}
- /* Stands for an undefined Expr, similar to ??? or null */
+ /** Stands for an undefined Expr, similar to ??? or null */
case class NoTree(tpe: TypeTree) extends Expr with Terminal {
val getType = tpe
}
@@ -61,14 +65,18 @@ object Expressions {
/* Specifications */
- /* This describes computational errors (unmatched case, taking min of an
- * empty set, division by zero, etc.). It should always be typed according to
- * the expected type. */
+ /** This describes computational errors (unmatched case, taking min of an
+ * empty set, division by zero, etc.). It should always be typed according to
+ * the expected type. */
case class Error(tpe: TypeTree, description: String) extends Expr with Terminal {
val getType = tpe
}
- // Preconditions
+ /** Precondition of an [[Expressions.Expr]]. Corresponds to the Leon keyword *require*
+ *
+ * @param pred The precondition formula inside ``require(...)``
+ * @param body The body following the ``require(...)``
+ */
case class Require(pred: Expr, body: Expr) extends Expr {
val getType = {
if (pred.getType == BooleanType)
@@ -77,7 +85,10 @@ object Expressions {
}
}
- // Postconditions
+ /** Postcondition of an [[Expressions.Expr]]. Corresponds to the Leon keyword *ensuring*
+ *
+ * @param body The body of the expression. It can contain at most one [[Expressions.Require]] sub-expression.
+ * @param pred The predicate to satisfy. It should be a function whose argument's type can handle the type of the body */
case class Ensuring(body: Expr, pred: Expr) extends Expr {
val getType = pred.getType match {
case FunctionType(Seq(bodyType), BooleanType) if isSubtypeOf(body.getType, bodyType) =>
@@ -85,6 +96,7 @@ object Expressions {
case _ =>
untyped
}
+ /** Converts this ensuring clause to the body followed by an assert statement */
def toAssert: Expr = {
val res = FreshIdentifier("res", getType, true)
Let(res, body, Assert(
@@ -94,7 +106,12 @@ object Expressions {
}
}
- // Local assertions
+ /** Local assertions with customizable error message
+ *
+ * @param pred The predicate, first argument of `assert(..., ...)`
+ * @param error An optional error string to display if the assert fails. Second argument of `assert(..., ...)`
+ * @param body The expression following `assert(..., ...)`
+ */
case class Assert(pred: Expr, error: Option[String], body: Expr) extends Expr {
val getType = {
if (pred.getType == BooleanType)
@@ -104,13 +121,22 @@ object Expressions {
}
- /* Variables */
+ /** Variable
+ * @param id The identifier of this variable */
case class Variable(id: Identifier) extends Expr with Terminal {
val getType = id.getType
}
- /* Local val's and def's */
+ /** $encodingof `val ... = ...; ...`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#let purescala's constructor let]] or [[purescala.Constructors#letTuple purescala's constructor letTuple]]
+ *
+ * @param binder The identifier 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
+ */
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
val getType = {
// We can't demand anything sticter here, because some binders are
@@ -123,17 +149,27 @@ object Expressions {
}
}
+ /** $encodingof `def ... = ...; ...` (lazy evaluation)
+ *
+ * @param id The function definition.
+ * @param body The body of the expression after the function
+ */
case class LetDef(fd: FunDef, body: Expr) extends Expr {
val getType = body.getType
}
- /**
- * OO Trees
- *
- * Both MethodInvocation and This get removed by phase MethodLifting. Methods become functions,
- * This becomes first argument, and MethodInvocation becomes FunctionInvocation.
- */
+ // OO Trees
+ /** $encodingof `(...).method(args)` (method invocation)
+ *
+ * Both [[Expressions.MethodInvocation]] and [[Expressions.This]] get removed by phase [[MethodLifting]]. Methods become functions,
+ * [[Expressions.This]] becomes first argument, and [[Expressions.MethodInvocation]] becomes [[Expressions.FunctionInvocation]].
+ *
+ * @param rec The expression evaluating to an object
+ * @param cd The class definition typing `rec`
+ * @param tfd The typed function definition of the method
+ * @param args The arguments provided to the method
+ */
case class MethodInvocation(rec: Expr, cd: ClassDef, tfd: TypedFunDef, args: Seq[Expr]) extends Expr {
val getType = {
// We need ot instantiate the type based on the type of the function as well as receiver
@@ -148,12 +184,19 @@ object Expressions {
}
}
+ /** The '''this''' keyword */
case class This(ct: ClassType) extends Expr with Terminal {
val getType = ct
}
- /* HOFs */
+ /* HOFs (Higher-order Formulas) */
+
+ /** $encodingof `callee.apply(args...)`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#application purescala's constructor application]]
+ */
case class Application(callee: Expr, args: Seq[Expr]) extends Expr {
val getType = callee.getType match {
case FunctionType(from, to) =>
@@ -163,6 +206,7 @@ object Expressions {
}
}
+ /** $encodingof `(args) => body` */
case class Lambda(args: Seq[ValDef], body: Expr) extends Expr {
val getType = FunctionType(args.map(_.getType), body.getType).unveilUntyped
def paramSubst(realArgs: Seq[Expr]) = {
@@ -176,24 +220,45 @@ object Expressions {
/* Control flow */
+ /** $encodingof `function(...)` (function invocation) */
case class FunctionInvocation(tfd: TypedFunDef, args: Seq[Expr]) extends Expr {
require(tfd.params.size == args.size)
val getType = checkParamTypes(args, tfd.params, tfd.returnType)
}
+ /** $encodingof `if(...) ... else ...` */
case class IfExpr(cond: Expr, thenn: Expr, elze: Expr) extends Expr {
val getType = leastUpperBound(thenn.getType, elze.getType).getOrElse(untyped).unveilUntyped
}
+ /** $encodingof `... match { ... }`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#matchExpr purescala's constructor matchExpr]]
+ *
+ * @param scrutinee Expression to the left of the '''match''' keyword
+ * @param cases A sequence of cases to match `scrutinee` against
+ */
case class MatchExpr(scrutinee: Expr, cases: Seq[MatchCase]) extends Expr {
require(cases.nonEmpty)
val getType = leastUpperBound(cases.map(_.rhs.getType)).getOrElse(untyped).unveilUntyped
}
+ /** $encodingof `case ... [if ...] => ... `
+ *
+ * @param pattern The pattern just to the right of the '''case''' keyword
+ * @param optGuard An optional if-condition just to the left of the `=>`
+ * @param rhs The expression to the right of `=>`
+ * @see [[Expressions.MatchExpr]]
+ */
case class MatchCase(pattern : Pattern, optGuard : Option[Expr], rhs: Expr) extends Tree {
def expressions: Seq[Expr] = optGuard.toList :+ rhs
}
+ /** $encodingof a pattern after a '''case''' keyword.
+ *
+ * @see [[Expressions.MatchCase]]
+ */
sealed abstract class Pattern extends Tree {
val subPatterns: Seq[Pattern]
val binder: Option[Identifier]
@@ -207,20 +272,25 @@ object Expressions {
}}.copiedFrom(this)
}
+ /** Pattern encoding `case a: ct` making sure an identifier is of the given type */
case class InstanceOfPattern(binder: Option[Identifier], ct: ClassType) extends Pattern { // c: Class
val subPatterns = Seq()
}
case class WildcardPattern(binder: Option[Identifier]) extends Pattern { // c @ _
val subPatterns = Seq()
}
+ /** Pattern encoding `case CaseClass(...) =>` */
case class CaseClassPattern(binder: Option[Identifier], ct: CaseClassType, subPatterns: Seq[Pattern]) extends Pattern
+ /** Pattern encoding tuple pattern `case (...) =>` */
case class TuplePattern(binder: Option[Identifier], subPatterns: Seq[Pattern]) extends Pattern
+ /** Pattern encoding like `case 0 => ...` or `case "Foo" => ...` */
case class LiteralPattern[+T](binder: Option[Identifier], lit : Literal[T]) extends Pattern {
val subPatterns = Seq()
}
+ /** Any pattern having an `unapply` function */
case class UnapplyPattern(binder: Option[Identifier], unapplyFun: TypedFunDef, subPatterns: Seq[Pattern]) extends Pattern {
// Hacky, but ok
lazy val optionType = unapplyFun.returnType.asInstanceOf[AbstractClassType]
@@ -258,7 +328,11 @@ object Expressions {
)
}
- /* Symbolic IO examples */
+ /** Symbolic IO examples as a match/case
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#passes purescala's constructor passes]]
+ */
case class Passes(in: Expr, out : Expr, cases : Seq[MatchCase]) extends Expr {
require(cases.nonEmpty)
@@ -274,7 +348,7 @@ object Expressions {
}
- /* Literals */
+ /** Literals */
sealed abstract class Literal[+T] extends Expr with Terminal {
val value: T
}
@@ -310,15 +384,24 @@ object Expressions {
}
- /* Case classes */
+ /** $encodingof `case class ...(...)`
+ * @param ct The case class name and inherited attributes
+ * @param args The arguments of the case class
+ */
case class CaseClass(ct: CaseClassType, args: Seq[Expr]) extends Expr {
val getType = checkParamTypes(args, ct.fieldsTypes, ct)
}
+ /** $encodingof `.isInstanceOf[...]` */
case class IsInstanceOf(classType: ClassType, expr: Expr) extends Expr {
val getType = BooleanType
}
+ /** $encodingof `value.selector` where value is a case class
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#caseClassSelector purescala's constructor caseClassSelector]]
+ */
case class CaseClassSelector(classType: CaseClassType, caseClass: Expr, selector: Identifier) extends Expr {
val selectorIndex = classType.classDef.selectorID2Index(selector)
val getType = {
@@ -334,7 +417,11 @@ object Expressions {
}
- /* Equality */
+ /** $encodingof `... == ...`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#equality purescala's constructor equality]]
+ */
case class Equals(lhs: Expr, rhs: Expr) extends Expr {
val getType = {
if (typesCompatible(lhs.getType, rhs.getType)) BooleanType
@@ -346,6 +433,11 @@ object Expressions {
/* Propositional logic */
+ /** $encodingof `... && ...`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#and purescala's constructor and]] or [[purescala.Constructors#andJoin purescala's constructor andJoin]]
+ */
case class And(exprs: Seq[Expr]) extends Expr {
require(exprs.size >= 2)
val getType = {
@@ -358,6 +450,11 @@ object Expressions {
def apply(a: Expr, b: Expr): Expr = And(Seq(a, b))
}
+ /** $encodingof `... || ...`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#or purescala's constructor or]] or [[purescala.Constructors#orJoin purescala's constructor orJoin]]
+ */
case class Or(exprs: Seq[Expr]) extends Expr {
require(exprs.size >= 2)
val getType = {
@@ -370,6 +467,11 @@ object Expressions {
def apply(a: Expr, b: Expr): Expr = Or(Seq(a, b))
}
+ /** 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
@@ -377,6 +479,11 @@ object Expressions {
}
}
+ /** $encodingof `!...`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#not purescala's constructor not]]
+ */
case class Not(expr: Expr) extends Expr {
val getType = {
if (expr.getType == BooleanType) BooleanType
@@ -386,137 +493,184 @@ object Expressions {
/* Integer arithmetic */
+ /** $encodingof `... + ...`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#plus purescala's constructor plus]]
+ */
case class Plus(lhs: Expr, rhs: Expr) extends Expr {
val getType = {
if (lhs.getType == IntegerType && rhs.getType == IntegerType) IntegerType
else untyped
}
}
+ /** $encodingof `... - ...`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#matchExpr purescala's constructor matchExpr]]
+ */
case class Minus(lhs: Expr, rhs: Expr) extends Expr {
val getType = {
if (lhs.getType == IntegerType && rhs.getType == IntegerType) IntegerType
else untyped
}
}
+ /** $encodingof `- ...`*/
case class UMinus(expr: Expr) extends Expr {
val getType = {
if (expr.getType == IntegerType) IntegerType
else untyped
}
}
+ /** $encodingof `... * ...`
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#times purescala's constructor times]]
+ */
case class Times(lhs: Expr, rhs: Expr) extends Expr {
val getType = {
if (lhs.getType == IntegerType && rhs.getType == IntegerType) IntegerType
else untyped
}
}
- /*
- * Division and Remainder follows Java/Scala semantics. Division corresponds
- * to / operator on BigInt and Remainder corresponds to %. Note that in
- * Java/Scala % is called remainder and the "mod" operator (Modulo in Leon) is also
- * defined on BigInteger and differs from Remainder. The "mod" operator
- * returns an always positive remainder, while Remainder could return
- * a negative remainder. The following must hold:
- *
- * Division(x, y) * y + Remainder(x, y) == x
- */
+ /** $encodingof `... / ...`
+ *
+ * Division and Remainder follows Java/Scala semantics. Division corresponds
+ * to / operator on BigInt and Remainder corresponds to %. Note that in
+ * Java/Scala % is called remainder and the "mod" operator (Modulo in Leon) is also
+ * defined on BigInteger and differs from Remainder. The "mod" operator
+ * returns an always positive remainder, while Remainder could return
+ * a negative remainder. The following must hold:
+ *
+ * Division(x, y) * y + Remainder(x, y) == x
+ */
case class Division(lhs: Expr, rhs: Expr) extends Expr {
val getType = {
if (lhs.getType == IntegerType && rhs.getType == IntegerType) IntegerType
else untyped
}
}
+ /** $encodingof `... % ...` (can return negative numbers)
+ *
+ * @see [[Expressions.Division]]
+ */
case class Remainder(lhs: Expr, rhs: Expr) extends Expr {
val getType = {
if (lhs.getType == IntegerType && rhs.getType == IntegerType) IntegerType
else untyped
}
}
+ /** $encodingof `... mod ...` (cannot return negative numbers)
+ *
+ * @see [[Expressions.Division]]
+ */
case class Modulo(lhs: Expr, rhs: Expr) extends Expr {
val getType = {
if (lhs.getType == IntegerType && rhs.getType == IntegerType) IntegerType
else untyped
}
}
+ /** $encodingof `... < ...`*/
case class LessThan(lhs: Expr, rhs: Expr) extends Expr {
val getType = BooleanType
}
+ /** $encodingof `... > ...`*/
case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr {
val getType = BooleanType
}
+ /** $encodingof `... <= ...`*/
case class LessEquals(lhs: Expr, rhs: Expr) extends Expr {
val getType = BooleanType
}
+ /** $encodingof `... >= ...`*/
case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr {
val getType = BooleanType
}
/* Bit-vector arithmetic */
+ /** $encodingof `... + ...` $note_bitvector*/
case class BVPlus(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == Int32Type && rhs.getType == Int32Type)
val getType = Int32Type
}
+ /** $encodingof `... - ...` $note_bitvector*/
case class BVMinus(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == Int32Type && rhs.getType == Int32Type)
val getType = Int32Type
}
+ /** $encodingof `- ...` $note_bitvector*/
case class BVUMinus(expr: Expr) extends Expr {
require(expr.getType == Int32Type)
val getType = Int32Type
}
+ /** $encodingof `... * ...` $note_bitvector*/
case class BVTimes(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == Int32Type && rhs.getType == Int32Type)
val getType = Int32Type
}
+ /** $encodingof `... / ...` $note_bitvector*/
case class BVDivision(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == Int32Type && rhs.getType == Int32Type)
val getType = Int32Type
}
+ /** $encodingof `... % ...` $note_bitvector*/
case class BVRemainder(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == Int32Type && rhs.getType == Int32Type)
val getType = Int32Type
}
+ /** $encodingof `! ...` $note_bitvector*/
case class BVNot(expr: Expr) extends Expr {
val getType = Int32Type
}
+ /** $encodingof `... & ...` $note_bitvector*/
case class BVAnd(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
+ /** $encodingof `... | ...` $note_bitvector*/
case class BVOr(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
+ /** $encodingof `... ^ ...` $note_bitvector*/
case class BVXOr(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
+ /** $encodingof `... << ...` $note_bitvector*/
case class BVShiftLeft(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
+ /** $encodingof `... >>> ...` $note_bitvector (logical shift)*/
case class BVAShiftRight(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
+ /** $encodingof `... >> ...` $note_bitvector (arighmetic shift, sign-preserving)*/
case class BVLShiftRight(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
- /* Integer arithmetic */
+ /* Real arithmetic */
+ /** $encodingof `... + ...` $note_real */
case class RealPlus(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == RealType && rhs.getType == RealType)
val getType = RealType
}
+ /** $encodingof `... - ...` $note_real */
case class RealMinus(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == RealType && rhs.getType == RealType)
val getType = RealType
}
+ /** $encodingof `- ...` $note_real */
case class RealUMinus(expr: Expr) extends Expr {
require(expr.getType == RealType)
val getType = RealType
}
+ /** $encodingof `... * ...` $note_real */
case class RealTimes(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == RealType && rhs.getType == RealType)
val getType = RealType
}
+ /** $encodingof `... / ...` $note_real */
case class RealDivision(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == RealType && rhs.getType == RealType)
val getType = RealType
@@ -525,18 +679,22 @@ object Expressions {
/* Tuple operations */
- // If you are not sure about the requirement you should use
- // the tupleWrap in purescala.Constructors
+ /** $encodingof `(..., ....)` (tuple)
+ *
+ * If you are not sure about the requirement you should use
+ * [[purescala.Constructors#tupleWrap purescala's constructor tupleWrap]]
+ */
case class Tuple (exprs: Seq[Expr]) extends Expr {
require(exprs.size >= 2)
val getType = TupleType(exprs.map(_.getType)).unveilUntyped
}
- /*
- * 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 tupleSelect in pureScala.Constructors
- */
+ /** $encodingof `(tuple)._i`
+ *
+ * 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 [[purescala.Constructors$.tupleSelect(t:leon\.purescala\.Expressions\.Expr,index:Int,isTuple:Boolean):leon\.purescala\.Expressions\.Expr* purescala's constructor tupleSelect]]
+ */
case class TupleSelect(tuple: Expr, index: Int) extends Expr {
require(index >= 1)
@@ -552,24 +710,31 @@ object Expressions {
/* Set operations */
+ /** $encodingof `Set(elements)` */
case class FiniteSet(elements: Set[Expr], base: TypeTree) extends Expr {
val getType = SetType(base).unveilUntyped
}
+ /** $encodingof `set.contains(elements)` or `set(elements)` */
case class ElementOfSet(element: Expr, set: Expr) extends Expr {
val getType = BooleanType
}
+ /** $encodingof `set.length` */
case class SetCardinality(set: Expr) extends Expr {
val getType = Int32Type
}
+ /** $encodingof `set.subsetOf(set2)` */
case class SubsetOf(set1: Expr, set2: Expr) extends Expr {
val getType = BooleanType
}
+ /** $encodingof `set.intersect(set2)` */
case class SetIntersection(set1: Expr, set2: Expr) extends Expr {
val getType = leastUpperBound(Seq(set1, set2).map(_.getType)).getOrElse(untyped).unveilUntyped
}
+ /** $encodingof `set ++ set2` */
case class SetUnion(set1: Expr, set2: Expr) extends Expr {
val getType = leastUpperBound(Seq(set1, set2).map(_.getType)).getOrElse(untyped).unveilUntyped
}
+ /** $encodingof `set -- set2` */
case class SetDifference(set1: Expr, set2: Expr) extends Expr {
val getType = leastUpperBound(Seq(set1, set2).map(_.getType)).getOrElse(untyped).unveilUntyped
}
@@ -577,9 +742,11 @@ object Expressions {
// TODO: Add checks for these expressions too
/* Map operations */
+ /** $encodingof `Map(key -> value, key2 -> value2 ...)` */
case class FiniteMap(singletons: Seq[(Expr, Expr)], keyType: TypeTree, valueType: TypeTree) extends Expr {
val getType = MapType(keyType, valueType).unveilUntyped
}
+ /** $encodingof `map.get(key)` */
case class MapGet(map: Expr, key: Expr) extends Expr {
val getType = map.getType match {
case MapType(from, to) if isSubtypeOf(key.getType, from) =>
@@ -587,18 +754,22 @@ object Expressions {
case _ => untyped
}
}
+ /** $encodingof `map ++ map2` */
case class MapUnion(map1: Expr, map2: Expr) extends Expr {
val getType = leastUpperBound(Seq(map1, map2).map(_.getType)).getOrElse(untyped).unveilUntyped
}
+ /** $encodingof `map -- map2` */
case class MapDifference(map: Expr, keys: Expr) extends Expr {
val getType = map.getType
}
+ /** $encodingof `map.isDefinedAt(key)` */
case class MapIsDefinedAt(map: Expr, key: Expr) extends Expr {
val getType = BooleanType
}
/* Array operations */
+ /** $encodingof `array(key)` */
case class ArraySelect(array: Expr, index: Expr) extends Expr {
val getType = array.getType match {
case ArrayType(base) =>
@@ -608,6 +779,7 @@ object Expressions {
}
}
+ /** $encodingof `array.updated(key, index)` */
case class ArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr {
val getType = array.getType match {
case ArrayType(base) =>
@@ -617,22 +789,25 @@ object Expressions {
}
}
+ /** $encodingof `array.length` */
case class ArrayLength(array: Expr) extends Expr {
val getType = Int32Type
}
+ /** $encodingof `array.nonempty` */
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
}
+ /** $encodingof `Array()` with a given type */
case class EmptyArray(tpe: TypeTree) extends Expr with Terminal {
val getType = ArrayType(tpe).unveilUntyped
}
/* Special trees for synthesis */
-
+ /** $encodingof `choose(pred)` where pred should be a [[Types.FunctionType]] */
case class Choose(pred: Expr) extends Expr {
val getType = pred.getType match {
case FunctionType(from, BooleanType) if from.nonEmpty => // @mk why nonEmpty?
@@ -653,6 +828,7 @@ object Expressions {
}
}
+ /** $encodingof `???[tpe]` */
case class Hole(tpe: TypeTree, alts: Seq[Expr]) extends Expr with Extractable {
val getType = tpe