abstract class Lookup extends AnyRef
A read-only abstraction of a library. A Library is a Lookup with write methods
- Self Type
- Lookup
- Source
- Lookup.scala
- Alphabetic
- By Inheritance
- Lookup
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new Lookup()
Abstract Value Members
-
abstract
def
forDeclarationsInScope(mod: Term)(f: (MPath, Term, Declaration) ⇒ Unit): Unit
apply a function to all declarations that are visible (based on what is currently loaded) to a theory
apply a function to all declarations that are visible (based on what is currently loaded) to a theory
- mod
the theory
- f
applied to (theory t declaring d, morphism mod->t that makes d visible, d)
-
abstract
def
get(home: Term, name: LocalName, error: (String) ⇒ Nothing): Declaration
lookup a declaration in a (possibly complex) module
lookup a declaration in a (possibly complex) module
- home
the module in which to look up
- name
the name look up; must start with ComplexStep unless it is local to home
- error
the continuation to call on the error message
- returns
the declaration
-
abstract
def
get(path: Path): StructuralElement
lookup a path
- abstract def getImplicit(from: Term, to: Term): Option[Term]
-
abstract
def
preImage(p: GlobalName): Option[GlobalName]
if p is imported by a structure, returns the preimage of the symbol under the outermost structure
- abstract def visible(to: Term): Iterable[MPath]
Concrete 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 apply(path: ContentPath): StructuralElement
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
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] )
-
def
getAs[E <: ContentElement](cls: Class[E], home: Term, name: LocalName, error: (String) ⇒ Nothing): E
like get but with restricted return type
-
def
getAs[E <: StructuralElement](cls: Class[E], path: Path): E
like get but with restricted return type example: getAs(classOf[Constant], path): Constant
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- def getComponent(path: CPath): ComponentContainer
- def getConstant(path: GlobalName, msg: (Path) ⇒ String = defmsg): Constant
-
def
getDomain(a: Declaration): (AbstractTheory, Option[Link])
gets the domain in which a Declaration was declared
gets the domain in which a Declaration was declared
This can be used to retrieve the source of an assignment declared in a DeclaredLink. It is also the official way to test whether a Constant is an assignment.
- a
the Constant declaration/assignment
- returns
if assignment: the source theory and the containing link; if declaration: the containing theory
- def getImplicit(from: MPath, to: MPath): Option[Term]
- def getLink(path: ContentPath, msg: (Path) ⇒ String = defmsg): Link
-
def
getModule(path: MPath): Module
important special case
-
def
getO(home: Term, name: LocalName): Option[Declaration]
like get but returns optional
-
def
getO(path: Path): Option[StructuralElement]
like get, but returns option
-
def
getParent(d: Declaration): ModuleOrLink
returns the container element that contains a declarations
- def getStructure(path: GlobalName, msg: (Path) ⇒ String = defmsg): Structure
- def getSymbol(path: GlobalName, msg: (Path) ⇒ String = defmsg): Declaration
- def getTheory(path: MPath, msg: (Path) ⇒ String = defmsg): Theory
- def getView(path: MPath, msg: (Path) ⇒ String = defmsg): View
- def hasImplicit(from: Term, to: Term): Boolean
-
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()
-
def
quasiAliasFor(c: GlobalName): List[GlobalName]
all constants for which c is a quasi-alias (recursively) a quasi-alias is defined by a definition c = OMS(d)
-
def
resolveName(parents: List[MPath], name: LocalName): List[GlobalName]
resolves a name in a list of theories using any included theory, possibly inserting include steps
-
def
resolveRealizedName(parent: ModuleOrLink, name: LocalName): List[GlobalName]
resolves a name in a module using any included or realized theories
-
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()
-
object
ApplyMorphs extends Traverser[Term]
A Traverser that recursively eliminates all explicit morphism applications.
A Traverser that recursively eliminates all explicit morphism applications. apply(t,m) can be used to apply a morphism to a term.
-
object
ExpandDefinitions extends Traverser[(ContentPath) ⇒ Boolean]
A Traverser that recursively expands definitions of Constants.
A Traverser that recursively expands definitions of Constants. It carries along a test function that is used to determine when a constant should be expanded.