package util
- Alphabetic
- Public
- Protected
Type Members
- case class ConditionalNormalizer(rewriteRules: Set[ConditionalReductionRule]) extends Product with Serializable
- 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.
- class ExpressionParseHelper extends AnyRef
Extension class that provides string interpolation functions for various expression types.
- 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
- object ConditionalReductionRule extends Serializable
- object ExpressionParseHelper
- object LambdaPosition extends Serializable
- object boundVariables
Returns the set of all bound variables occurring in the given argument.
- object constants
- object expressionDepth
- object expressionSize
- object freeVariables
Returns the set of free variables in the given argument.
- object isConstructorForm
- object isGround
- 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.
- 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.
- 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.
- object replacementContext
Creates capture avoiding replacement contexts.
- object subTerms
Returns the set of all subterms of the given lambda term.
- object syntacticMGU
- object syntacticMatching
- 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.
- object typeVariables
- object variables
Returns the set of all variables occurring in the given argument (including bound variables).
This is the API documentation for GAPT.
The main package is gapt.