Packages

package util

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. Protected

Type Members

  1. case class ConditionalNormalizer(rewriteRules: Set[ConditionalReductionRule]) extends Product with Serializable
  2. case class ConditionalReductionRule(conditions: Seq[Formula], lhs: Expr, rhs: Expr) extends Product with Serializable

    A conditional rewrite rule.

    A conditional rewrite rule.

    An instance of this rule can be used to rewrite the left hand side into its right hand side only if the conditions all rewrite to ⊤.

    The free variables of the conditions together with those of the right hand side must form a subset of the free variables of the left hand side. The left hand side must not be a variable.

    conditions

    The conditions of this rewrite rule.

    lhs

    The left hand side of this rewrite rule.

    rhs

    The right hand side of this rewrite rule.

  3. class ExpressionParseHelper extends AnyRef

    Extension class that provides string interpolation functions for various expression types.

  4. case class LambdaPosition(list: List[Choice]) extends Product with Serializable

    Represents a position in a gapt.expr.Expr.

    Represents a position in a gapt.expr.Expr.

    Positions are represented by lists of Integers. The empty list denotes the expression itself. A nonempty list denotes a position in the left or right subexpression according to whether it starts with 1 or 2.

    list

    The list of integers describing the position.

Value Members

  1. object ConditionalReductionRule extends Serializable
  2. object ExpressionParseHelper
  3. object LambdaPosition extends Serializable
  4. object boundVariables

    Returns the set of all bound variables occurring in the given argument.

  5. object constants
  6. object expressionDepth
  7. object expressionSize
  8. object freeVariables

    Returns the set of free variables in the given argument.

  9. object isConstructorForm
  10. object isGround
  11. object isInVNF

    A lambda term is in variable-normal form (VNF) if different binders bind different variables, and bound variables are disjoint from the free ones.

  12. object longNormalForm

    If t = λx₁...λxₘ(y u₁ ...

    If t = λx₁...λxₘ(y u₁ ... uₚ) is a normal term of type T₁ → ... → Tₙ → U, with U atomic and m ≤ n, then its long normal form is the term

    λx₁...λxₘλxₘ₊₁...λxₙ(y u₁'... uₚ' xₘ₊₁' ... xₙ'),

    where uᵢ' is the long normal form of uᵢ and xⱼ' is the long normal form of xⱼ.

    Implemented according to Definition 2.25, Higher-Order Unification and Matching by Gilles Dowek.

  13. object rename

    get a new variable/constant (similar to the current and) different from all variables/constants in the blackList, returns this variable if this variable is not in the blackList.

  14. object replacementContext

    Creates capture avoiding replacement contexts.

  15. object subTerms

    Returns the set of all subterms of the given lambda term.

  16. object syntacticMGU
  17. object syntacticMatching
  18. object toVNF

    Transforms an expression into an alpha-equivalent expression in variable-normal form, where no two binders bind the same variable, and the bound variables are disjoint from the free ones.

  19. object typeVariables
  20. object variables

    Returns the set of all variables occurring in the given argument (including bound variables).

Ungrouped