package libraries
Library maintains the structural elements that have been loaded into memory. That includes the theory diagram and all documents.
ImplicitGraph maintains the commutative sub-diagram of implicit morphisms.
- Source
- package.scala
- Alphabetic
- By Inheritance
- libraries
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
case class
AlreadyDefined[E](from: Term, to: Term, old: E, nw: E) extends Throwable with Product with Serializable
thrown if the uniqueness condition of UniqueGraph is violated
-
case class
Completion(parent: MPath, completion: LocalName) extends Product with Serializable
a possible completion
a possible completion
- parent
theory from which the resolved symbol is imported
- completion
name of the completed symbol
-
trait
FailingNotFoundHandler extends AnyRef
to be mixed into LookupWithNotFoundHandler for failing on NotFound
-
class
ImplicitGraph extends AnyRef
maintains a diagram o morphisms; used in particular by Library for the diagram of implicit morphisms
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
- case class IncludeOption(from: MPath, to: MPath, name: LocalName) extends Product with Serializable
-
class
LabeledHashRelation[N, E] extends AnyRef
maintains a binary relation on N where pairs in the relation are labeled with values from E hashes in both directions are used to make all lookups fast
-
class
Library extends Lookup with Logger
A Library is the in-memory representation of an MMT diagram, including the implicit-diagram, and all root documents.
A Library is the in-memory representation of an MMT diagram, including the implicit-diagram, and all root documents.
It implements the lookup and change of MMT URIs via get/add/update/delete/reorder methods.
Invariant: This class guarantees structural well-formedness in the sense that libraries conform to the MMT grammar and all declarations have canonical URIs. The well-formedness of the objects in the declarations is not guaranteed.
The Controller own a library and uses it to load elements into memory dynamically. Therefore, access should always be through the corresponding methods of the controller. Elements are unloaded dynamically if MMT runs out of memory.
-
abstract
class
Lookup extends AnyRef
A read-only abstraction of a library.
A read-only abstraction of a library. A Library is a Lookup with write methods
-
abstract
class
LookupWithNotFoundHandler extends Lookup
delegates all lookup methods to another Lookup and handles the NotFound exception
-
class
ModuleHashMap extends AnyRef
auxiliary class of Library to optimize storage
auxiliary class of Library to optimize storage
This uses scala.ref.SoftReferences so that modules are automatically unloaded when memory is needed.
-
class
ThinGeneratedCategory extends AnyRef
maintains a thin diagram of theories This is the category generated by some edges that is guaranteed to be thin (i.e., at most one morphism between any two objects) i.e., all paths between two nodes must be equal.
maintains a thin diagram of theories This is the category generated by some edges that is guaranteed to be thin (i.e., at most one morphism between any two objects) i.e., all paths between two nodes must be equal. UniqueGraph is used to maintain the generated category, see its description for the treatment of equality. The generated category is precomputed so that retrieval of morphisms takes constant and insertion up to quadratic time.
-
class
UniqueGraph extends LabeledHashRelation[Term, Term]
A diagram of theories and morphisms with at most one edge between any two nodes.
A diagram of theories and morphisms with at most one edge between any two nodes. Morph.simplify is used to normalize paths, and equality of paths is checked by comparing normal forms; this criterion is sound and efficient but not complete.
Value Members
-
object
InactiveElement extends BooleanClientProperty[StructuralElement]
if set, the element is deactivated
-
object
Names
Auxiliary methods for name lookup