Packages

object Unify

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Unify
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. case class UnifyApplnException(func: Term, arg: Term, freeVars: Vector[Term], error: Throwable) extends Exception with Product with Serializable

Value Members

  1. def appln(func: Term, arg: Term, freeVars: Vector[Term] = Vector()): Option[Term]
  2. def dependsOn(term: Term): (Vector[Term]) => Boolean
  3. def extraVars(v: Vector[Term], m: Map[Term, Term]): Vector[Term]
  4. def mergeAll[U, V](xs: Option[Map[U, V]]*): Option[Map[U, V]]
  5. def mergeMaps[U, V](x: Map[U, V], y: Map[U, V]): Option[Map[U, V]]
  6. def mergeOptMaps[U, V](x: Option[Map[U, V]], y: Option[Map[U, V]]): Option[Map[U, V]]
  7. def multisub[U <: Term with Subs[U]](x: U, m: Map[Term, Term]): U
  8. def purgeInv(r1: Term, inv1: Set[(Term, Term)], r2: Term, inv2: Set[(Term, Term)], freeVars: (Term) => Boolean): Set[(Term, Term)]
  9. def purgeVector(r2: Term, inv2: Set[(Term, Term)], invVector: Vector[(Term, Set[(Term, Term)])], freeVars: (Term) => Boolean): (Term, Set[(Term, Term)])
  10. def purgedInvVector(invVector: Vector[(Term, Set[(Term, Term)])], accum: Vector[(Term, Set[(Term, Term)])] = Vector(), freeVars: (Term) => Boolean = HoTT.isVar): Vector[(Term, Set[(Term, Term)])]
    Annotations
    @tailrec()
  11. def purgedPairs(fxs: Set[(Term, Term)]): Set[(Term, Term)]
  12. def purgedPairsList(fxs: List[(Term, Term)], accum: List[(Term, Term)] = List()): List[(Term, Term)]
    Annotations
    @tailrec()
  13. def subsApply(func: Term, arg: Term, unifMap: Map[Term, Term], freeVars: Vector[Term]): Option[Term]
  14. def targetCodomain(func: Term, codomain: Term, freeVars: Vector[Term] = Vector()): Option[Term]

    Given a function and a target type, optionally returns a function with eventual codomain the given type; this is done by attempting to unify, filling in parameters where they are determined and returing lambdas if all parameters work.

  15. def targetCodomainStrict(func: Term, codomain: Term, freeVars: Vector[Term] = Vector()): Option[Term]

    Given a function and a target type, optionally returns a function with eventual codomain the given type; this is done by attempting to unify, filling in parameters where they are determined and returing lambdas if all parameters work.

  16. def unifApply(func: Term, arg: Term, freeVars: Vector[Term]): Option[Term]
  17. def unify(lhs: Term, rhs: Term, freevars: (Term) => Boolean): Option[Map[Term, Term]]
  18. def unifyAll(freeVars: (Term) => Boolean)(xys: (Term, Term)*): Option[Map[Term, Term]]
  19. def unifyVector(xys: Vector[(Term, Term)], freeVars: (Term) => Boolean): Option[Map[Term, Term]]