Value Members

1.  final def !=(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

2.  final def ##(): Int

   Definition Classes

   AnyRef → Any

3.  final def ==(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

4.  def Subst(subs: List[SubstRepl]): Subst

   Create a (generalized) substitution from the given representation subs.

   Create a (generalized) substitution from the given representation subs. Faster since compose preserves distinctness.

   Attributes

   protected

   Definition Classes

   FreshUnificationMatch → Matcher

5.  def SubstRepl(what: Expression, repl: Expression): SubstRepl

   Create a (generalized) substitution pair.

   Create a (generalized) substitution pair.

   Attributes

   protected

   Definition Classes

   Matcher

   See also

   SubstitutionPair

6.  def apply(e1: Sequent, e2: Sequent): Subst

   apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

   apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

   Definition Classes

   BaseMatcher → Matcher

   Exceptions thrown

   UnificationException if input cannot be matched against the pattern shape.

7.  def apply(e1: DifferentialProgram, e2: DifferentialProgram): Subst

   apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

   apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

   Definition Classes

   BaseMatcher → Matcher

   Exceptions thrown

   UnificationException if input cannot be matched against the pattern shape.

8.  def apply(e1: Program, e2: Program): Subst

   apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

   apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

   Definition Classes

   BaseMatcher → Matcher

   Exceptions thrown

   UnificationException if input cannot be matched against the pattern shape.

9.  def apply(e1: Formula, e2: Formula): Subst

   apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

   apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

   Definition Classes

   BaseMatcher → Matcher

   Exceptions thrown

   UnificationException if input cannot be matched against the pattern shape.

10.  def apply(e1: Term, e2: Term): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes

    BaseMatcher → Matcher

    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

11.  def apply(e1: Expression, e2: Expression): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes

    BaseMatcher → Matcher → Function2

12.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

13.  def clone(): AnyRef

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )

14.  def coloredDotsTerm(s: Sort, color: Int = 0): Term

    DotTerms of different "colors" for components of a Tuple, uncolored DotTerm for non-Tuples

    DotTerms of different "colors" for components of a Tuple, uncolored DotTerm for non-Tuples

    Definition Classes

    SchematicUnificationMatch

    Example:

    1. coloredDotsTerm(Real) = • coloredDotsTerm(Real*Real) = (•_0, •_1) coloredDotsTerm(Real*Real*Real) = (•_0, •_1, •_2)

15.  def compose(after: List[SubstRepl], before: List[SubstRepl]): List[SubstRepl]

    Quickly compose patterns coming from fresh shapes by just concatenating them.

    Quickly compose patterns coming from fresh shapes by just concatenating them. If indeed the shape used fresh names that did not occur in the input, this fast composition is fine.

    returns

    a substitution that has the same effect as applying substitution after after applying substitution before.

    Attributes

    protected

    Definition Classes

    FreshUnificationMatch → SchematicUnificationMatch

16.  def curried: (Expression) ⇒ (Expression) ⇒ RenUSubst

    Definition Classes

    Function2

    Annotations

    @unspecialized()

17.  def distinctIfNeedBe(repl: List[SubstRepl]): List[SubstRepl]

    Make repl distinct fast by directly returning it since this algorithm preserves distinctness in compose.

    Make repl distinct fast by directly returning it since this algorithm preserves distinctness in compose.

    returns

    repl.distinct

    Attributes

    protected

    Definition Classes

    FreshUnificationMatch → SchematicComposedUnificationMatch

18.  final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

19.  def equals(arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

20.  def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

21.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

22.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

23.  val id: List[SubstRepl]

    Identity substitution {} that does not change anything.

    Identity substitution {} that does not change anything.

    Attributes

    protected

    Definition Classes

    Matcher

24.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

25.  def join(s: List[(Expression, Expression)], t: List[(Expression, Expression)]): List[(Expression, Expression)]

    Union of renaming substitution representations: join(s, t) gives the representation of s performed together with t, if compatible.

    Union of renaming substitution representations: join(s, t) gives the representation of s performed together with t, if compatible.

    s \cup t = {p(.)~>F | (p(.)~>F) \in s}  ++  {(p(.)~>F) | (p(.)~>F) \in t}
    if s and t are compatible, so do not map the same p(.) or f(.) or a to different replacements

    returns

    a substitution that has the same effect as applying both substitutions s and t simultaneously. Similar to returning s++t but skipping duplicates and checking compatibility in passing.

    Definition Classes

    RestrictedBiDiUnificationMatch → BaseMatcher

26.  lazy val logger: Logger

    Attributes

    protected

    Definition Classes

    LazyLogging → LoggerHolder

27.  final val loggerName: String

    Attributes

    protected

    Definition Classes

    LoggerHolder

28.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

29.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

30.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

31.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

32.  def toString(): String

    Definition Classes

    Function2 → AnyRef → Any

33.  def tupled: ((Expression, Expression)) ⇒ RenUSubst

    Definition Classes

    Function2

    Annotations

    @unspecialized()

34.  def unifiable(shape: Sequent, input: Sequent): Option[Subst]

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    Definition Classes

    BaseMatcher → Matcher

35.  def unifiable(shape: Expression, input: Expression): Option[Subst]

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    Definition Classes

    BaseMatcher → Matcher

36.  def unifier(e1: Expression, e2: Expression, us: List[SubstRepl]): Subst

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Attributes

    protected

    Definition Classes

    FreshUnificationMatch → BaseMatcher

37.  def unifier(e1: Sequent, e2: Sequent, us: List[SubstRepl]): Subst

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Attributes

    protected

    Definition Classes

    BaseMatcher

38.  def unifier(shape: Expression, input: Expression): List[SubstRepl]

    Construct the base unifier that forces shape and input to unify unless equal already

    Construct the base unifier that forces shape and input to unify unless equal already

    returns

    {shape~>input} unless shape=input in which case it's {}.

    Attributes

    protected

    Definition Classes

    BaseMatcher

39.  def unifies2(s1: Program, s2: Program, t1: Program, t2: Program): List[SubstRepl]

    Attributes

    protected

    Definition Classes

    SchematicComposedUnificationMatch → SchematicUnificationMatch

40.  def unifies2(s1: Formula, s2: Formula, t1: Formula, t2: Formula): List[SubstRepl]

    Attributes

    protected

    Definition Classes

    SchematicComposedUnificationMatch → SchematicUnificationMatch

41.  def unifies2(s1: Term, s2: Term, t1: Term, t2: Term): List[SubstRepl]

    Attributes

    protected

    Definition Classes

    SchematicComposedUnificationMatch → SchematicUnificationMatch

42.  def unifies2(s1: Expression, s2: Expression, t1: Expression, t2: Expression): List[SubstRepl]

    unifies2(s1,s2, t1,t2) unifies the two expressions of shape (s2,s2) against the two inputs (t1,t2) by single-sided matching.

    unifies2(s1,s2, t1,t2) unifies the two expressions of shape (s2,s2) against the two inputs (t1,t2) by single-sided matching.

    s1 = t1 | u1     u1(s2) = t2 | u2
    ----------------------------------
    (s1,s2) = (t1,t2)  | u2 after u1

    Implemented by unifying from left to right, but will fall back to converse direction if exception.

    Attributes

    protected

    Definition Classes

    SchematicComposedUnificationMatch → SchematicUnificationMatch

43.  def unifiesODE2(s1: DifferentialProgram, s2: DifferentialProgram, t1: DifferentialProgram, t2: DifferentialProgram): List[SubstRepl]

    Attributes

    protected

    Definition Classes

    SchematicComposedUnificationMatch → SchematicUnificationMatch

44.  def unify(e1: Program, e2: Program): List[SubstRepl]

    A simple recursive unification algorithm for single-sided matching.

    A simple recursive unification algorithm for single-sided matching. unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes

    protected

    Definition Classes

    RestrictedBiDiUnificationMatch → SchematicUnificationMatch → BaseMatcher

45.  def unify(e1: Formula, e2: Formula): List[SubstRepl]

    A simple recursive unification algorithm for single-sided matching.

    A simple recursive unification algorithm for single-sided matching. unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes

    protected

    Definition Classes

    RestrictedBiDiUnificationMatch → SchematicUnificationMatch → BaseMatcher

46.  def unify(e1: Term, e2: Term): List[SubstRepl]

    A simple recursive unification algorithm for single-sided matching.

    A simple recursive unification algorithm for single-sided matching. unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes

    protected

    Definition Classes

    RestrictedBiDiUnificationMatch → SchematicUnificationMatch → BaseMatcher

47.  def unify(s1: Sequent, s2: Sequent): List[SubstRepl]

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes

    protected

    Definition Classes

    SchematicComposedUnificationMatch → BaseMatcher

    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

48.  def unify(shape: Expression, input: Expression): List[SubstRepl]

    Attributes

    protected

    Definition Classes

    BaseMatcher

49.  def unifyApplicationOf(F: (Function, Term) ⇒ Expression, f: Function, t: Term, e2: Expression): List[SubstRepl]

    Unify f(t) with e2 where F is the operator (FuncOf or PredOf) that forms the ApplicationOf f(t).

    Unify f(t) with e2 where F is the operator (FuncOf or PredOf) that forms the ApplicationOf f(t).

    1) unify the argument t with a DotTerm abstraction • (t may be a tuple, then • is a tuple: coloredDotsTerm) ua = unify(•, t) 2) unifier = substitute with the inverse of the argument unifier e2 f(•) ~> ua^-1(e2)

    Attributes

    protected

    Definition Classes

    RestrictedBiDiUnificationMatch → SchematicUnificationMatch

    Example:

    1. given t = (a, b), e2 = a2*b 1) unify((•_0, •_1), (a, b)) yields ua = •_0 ~> a, •_1 ~> b 2) the inverse is ua-1 = a ~> •_0, b ~> •_1, therefore ua-1(e2) = •_02*•_1, resulting in f(•_0, •_1) ~> (•_0^2*•_1) the inverse substitution is applied top-down, i.e., larger abstractions get precedence when components of t overlap: t = (x, y, x + y) and e2 = x + y yields f(•_0, •_1, •_2) ~> •_2; not f(•_0, •_1, •_2) ~> •_0 + •_1

50.  def unifyODE(e1: DifferentialProgram, e2: DifferentialProgram): List[SubstRepl]

    A simple recursive unification algorithm for single-sided matching.

    A simple recursive unification algorithm for single-sided matching. unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes

    protected

    Definition Classes

    SchematicUnificationMatch → BaseMatcher

51.  def unifyVar(x1: Variable, e2: Expression): List[SubstRepl]

    unifyVar(x1,e2) gives a unifier making x1 equal to e2 unless it already is.

    unifyVar(x1,e2) gives a unifier making x1 equal to e2 unless it already is.

    returns

    unifyVar(x1,x2)={x1~>x2} if x2 is a variable other than x1. unifyVar(x1,x1)={}

    Attributes

    protected

    Definition Classes

    RestrictedBiDiUnificationMatch → SchematicUnificationMatch

    Exceptions thrown

    UnificationException if e2 is not a variable

52.  def unifyVar(xp1: DifferentialSymbol, e2: Expression): List[SubstRepl]

    unifyVar(x1',e2) gives a unifier making x1' equal to e2 unless it already is.

    unifyVar(x1',e2) gives a unifier making x1' equal to e2 unless it already is.

    returns

    unifyVar(x1',x2')={x1~>x2} if x2' is a differential variable other than x1' unifyVar(x1',x1')={}

    Attributes

    protected

    Definition Classes

    SchematicUnificationMatch

    Exceptions thrown

    UnificationException if e2 is not a differential variable

53.  def ununifiable(shape: Sequent, input: Sequent): Nothing

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Attributes

    protected

    Definition Classes

    BaseMatcher

    Exceptions thrown

    UnificationException always.

54.  def ununifiable(shape: Expression, input: Expression): Nothing

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Attributes

    protected

    Definition Classes

    BaseMatcher

    Exceptions thrown

    UnificationException always.

55.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

56.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

57.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )