class ImplicitGraph extends AnyRef
maintains a diagram o morphisms; used in particular by Library for the diagram of implicit morphisms
the diagram does not have to be commutative
the generated category is cached so that lookups do not require traversals of the diagram
every edge maintains its dependencies and paths can be invalidated by calling delete invalidation is efficient: invalid paths are marked as invalid and removed only whenever they are encountered if an invalid path becomes valid again later, a new path instance is created for it JVM garbage collection collects the invalid paths whenever they have been removed from everywhere
- Source
- ImplicitGraph.scala
- Alphabetic
- By Inheritance
- ImplicitGraph
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new ImplicitGraph()
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
add(from: MPath, to: MPath, mor: Option[Term]): Unit
adds an implicit morphism
adds an implicit morphism
- from
domain
- to
codomain
- mor
the morphism; absent if identity (i.e., plain include)
-
def
apply(from: Term, to: Term): Option[Term]
retrieves the implicit morphism between two theory expressions (if any)
retrieves the implicit morphism between two theory expressions (if any)
- from
domain
- to
codomain
- returns
the implicit morphism if one exists
-
def
apply(from: MPath, to: MPath): Option[Term]
the most common lookup method: retrieves the implicit morphism between two theories (first if multiple), similar to get(from,to).headOption
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clear: Unit
clears all data
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
def
delete(d: MPath): Unit
deletes all implicit morphisms that depend on an element, must be called when that element is deleted
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getTo(to: MPath, refl: Boolean): Iterator[(MPath, Term)]
retrieves all implicit morphisms into a theory
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()