term.util

Visibility

Public
All

Type Members

type E = Equation

Shorthand for an Equation.
Shorthand for an Equation.

Definition Classes
package
type ERC = (ES, TRS, TRS)

A tripel consisting of an equational system, a term rewrite system, and an additional constraining term rewrite system.
A tripel consisting of an equational system, a term rewrite system, and an additional constraining term rewrite system.
These tripels are used for completion runs which use external termination tools.

Definition Classes
package
type ES = List[E]

An equational system (ES) is a list of equations between terms.
An equational system (ES) is a list of equations between terms.

Definition Classes
package
case class Equation (l: Term, r: Term) extends Product with Serializable

Represents an equation between two terms.
type Overlap = (Rule, Pos, Rule)

An overlap is a tripel consisting of a term rewrite rule, a position, and another term rewrite rule.
An overlap is a tripel consisting of a term rewrite rule, a position, and another term rewrite rule.
The position shows where the left-hand side of the second rule overlaps with the left-hand side of the first rule.

Definition Classes
package
type R = Rule

Shorthand for a Rule.
Shorthand for a Rule.

Definition Classes
package
case class Rule (l: Term, r: Term) extends Product with Serializable

Represents a term rewrite rule.
type TRS = List[R]

A term rewrite system (TRS) is a list of term rewrite rules.
A term rewrite system (TRS) is a list of term rewrite rules.

Definition Classes
package

Value Members

object E extends Serializable

Factory for Equation instances.
object Equation extends Serializable

Factory for Equation instances.
object MathSymbol extends AnyRef

This object provides meaningfull names for some usefull mathematical unicode symbols.
object R extends Serializable

Factory for Rule instances.
def combine [T] (is: List[Int], xs1: List[T], ys2: List[T]): List[T]

Definition Classes
package
def cps (trs1: TRS, trs2: TRS): ES

Returns a list of critical pairs between left-hand sides of rules in trs1 and left-hand sides of rules in trs2.
Returns a list of critical pairs between left-hand sides of rules in trs1 and left-hand sides of rules in trs2.

Definition Classes
package
def cps (trs: TRS): ES

Returns a list of critical pairs between left-hand sides of rules in trs.
Returns a list of critical pairs between left-hand sides of rules in trs.

Definition Classes
package
def crit_pair (ol: ()): E

Returns the critical pair generated by the overlap ol.
Returns the critical pair generated by the overlap ol.

Definition Classes
package
def end [T] (l: List[T], r: T): List[T]

Returns a list consisting of list l with element r appended at the end.
Returns a list consisting of list l with element r appended at the end.
T
the type of the list's elements

Definition Classes
package
def filterNot [T] (l: List[T], n: Int): List[T]

Returns the list l with the n-th element removed.
Returns the list l with the n-th element removed.
T
the type of the list's elements

Definition Classes
package
def longest (ls: List[Term]): Int

Definition Classes
package
def ms : Boolean

Returns true if termlib is running on a Microsoft Windows and false otherwise.
Returns true if termlib is running on a Microsoft Windows and false otherwise.

Definition Classes
package
def overlaps (trs1: TRS, trs2: TRS): List[()]

Returns a list of all overlaps between left-hand sides of rules from trs1 and left-hand sides of rules from trs2.
Returns a list of all overlaps between left-hand sides of rules from trs1 and left-hand sides of rules from trs2.

Definition Classes
package
def overlaps (trs: TRS): List[()]

Returns a list of all overlaps between left-hand sides of rules from the term rewrite system trs.
Returns a list of all overlaps between left-hand sides of rules from the term rewrite system trs.

Definition Classes
package
def partition [T] (is: List[Int], ls: List[T]): (List[T], List[T])

Returns a pair of two lists where the first entry is the list consisting of elements from ls with indices in is and the second entry is the rest of ls.
Returns a pair of two lists where the first entry is the list consisting of elements from ls with indices in is and the second entry is the rest of ls.

Definition Classes
package
def saneVars (excl: Set[String], vs: Set[String]): Subst

Definition Classes
package
def vars (ies: IES): List[V]

Definition Classes
package
def vars (es: ES): List[V]

Returns a list of all variables used in the equational system es.
Returns a list of all variables used in the equational system es.

Definition Classes
package

util

package util

Overview

Type Members

type E = Equation

type ERC = (ES, TRS, TRS)

type ES = List[E]

case class Equation (l: Term, r: Term) extends Product with Serializable

type Overlap = (Rule, Pos, Rule)

type R = Rule

case class Rule (l: Term, r: Term) extends Product with Serializable

type TRS = List[R]

Value Members

object E extends Serializable

object Equation extends Serializable

object MathSymbol extends AnyRef

object R extends Serializable

def combine [T] (is: List[Int], xs1: List[T], ys2: List[T]): List[T]

def cps (trs1: TRS, trs2: TRS): ES

def cps (trs: TRS): ES

def crit_pair (ol: ()): E

def end [T] (l: List[T], r: T): List[T]

def filterNot [T] (l: List[T], n: Int): List[T]

def longest (ls: List[Term]): Int

def ms : Boolean

def overlaps (trs1: TRS, trs2: TRS): List[()]

def overlaps (trs: TRS): List[()]

def partition [T] (is: List[Int], ls: List[T]): (List[T], List[T])

def saneVars (excl: Set[String], vs: Set[String]): Subst

def vars (ies: IES): List[V]

def vars (es: ES): List[V]