class ElaborationBasedSimplifier extends Simplifier with ChangeListener
the primary class for all flattening, materialization, enriching of theories
*internal* flattening of s: change the body of s by flattening all its components and children. *external* flattening of s: change the parent of s by adding all declarations induced by s. Internal flattening includes the recursive internal and external flattening of its children.
Most declarations are subject to either internal (modules and links) or external (includes, structures, derived declarations) flattening. Only non-include structures are subject to both.
- Alphabetic
- By Inheritance
- ElaborationBasedSimplifier
- ChangeListener
- Simplifier
- LeveledExtension
- StructureSimplifier
- Extension
- Logger
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new ElaborationBasedSimplifier(oS: ObjectSimplifier)
Type Members
-
case class
LocalError(s: String) extends ExtensionError with Product with Serializable
a custom error class for this extension
a custom error class for this extension
- Definition Classes
- Extension
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(obj: Obj, su: SimplificationUnit): ThisType
- Definition Classes
- Simplifier
-
def
apply(obj: Obj, su: SimplificationUnit, rules: RuleSet): ThisType
- Definition Classes
- Simplifier
-
def
apply(se: StructuralElement): Unit
elaborates one element and relevant parts of its dependency closure
elaborates one element and relevant parts of its dependency closure
This is typically used for assumed-correct content that is not checked, e.g., content loaded directly from OMDoc For container elements that are checked incrementally, one may alternatively use applyElementBegin and applyElementEnd
- Definition Classes
- StructureSimplifier
-
def
apply(p: ContentPath): Unit
convenience abbreviation
convenience abbreviation
- Definition Classes
- StructureSimplifier
-
def
applyChecked(s: StructuralElement)(implicit env: SimplificationEnvironment): Unit
like apply but takes an extra argument to handle checking and error reporting
like apply but takes an extra argument to handle checking and error reporting
- Definition Classes
- ElaborationBasedSimplifier → StructureSimplifier
-
def
applyElementBegin(s: StructuralElement)(implicit env: SimplificationEnvironment): Unit
like apply except that for container elements applyElementBegin + apply on every child + applyElementEnd = apply
like apply except that for container elements applyElementBegin + apply on every child + applyElementEnd = apply
- Definition Classes
- ElaborationBasedSimplifier → StructureSimplifier
-
def
applyElementEnd(s: ContainerElement[_])(implicit env: SimplificationEnvironment): Unit
called in conjunction with applyElementBegin
called in conjunction with applyElementBegin
- Definition Classes
- ElaborationBasedSimplifier → StructureSimplifier
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
catchErrors[A](msg: String, recoverWith: ⇒ A)(code: ⇒ A): A
like its partner but with return value
like its partner but with return value
- Attributes
- protected
- Definition Classes
- Extension
-
def
catchErrors(msg: String)(code: ⇒ Unit): Unit
convenience method for wrapping code in error handler that throws LocalError
convenience method for wrapping code in error handler that throws LocalError
- Attributes
- protected
- Definition Classes
- Extension
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
val
controller: Controller
the controller that this extension is added to; only valid after creation of the extension, i.e., will return null if used in a non-lazy val-field
the controller that this extension is added to; only valid after creation of the extension, i.e., will return null if used in a non-lazy val-field
- Attributes
- protected
- Definition Classes
- Extension
-
lazy val
defaultPrefix: String
- Definition Classes
- Extension
-
def
destroy: Unit
extension-specific cleanup (override as needed, empty by default)
extension-specific cleanup (override as needed, empty by default)
Extensions may create persistent data structures and threads, but they must clean up after themselves in this method
- Definition Classes
- LeveledExtension → Extension
-
def
destroyWhenRemainingTasksFinished: Unit
convenience for calling waitUntilRemainingTasksFinished and then destroy
convenience for calling waitUntilRemainingTasksFinished and then destroy
- Definition Classes
- Extension
-
def
enrich(t: Theory): Theory
adds declarations induced by views to all theories
- def enrichFineGrained(t: Theory): List[Theory]
-
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
getBody(context: Context, moduleExp: Term): ElementContainer[NamedElement]
- Definition Classes
- ElaborationBasedSimplifier → StructureSimplifier
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getFromFirstArgOrEnvvar(args: List[String], name: String, default: String = ""): String
- Attributes
- protected
- Definition Classes
- Extension
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
init(controller: Controller): Unit
MMT initialization (idempotent)
MMT initialization (idempotent)
- Definition Classes
- LeveledExtension → Extension
-
def
initOther(e: Extension): Unit
any extension can initialize other extensions if those are not meant to be added to the ExtensionManager
any extension can initialize other extensions if those are not meant to be added to the ExtensionManager
- Attributes
- protected
- Definition Classes
- Extension
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
log(e: Error): Unit
logs an error - always logged
logs an error - always logged
- Attributes
- protected
- Definition Classes
- Logger
-
def
log(s: ⇒ String, subgroup: Option[String] = None): Unit
logs a message with this logger's logprefix
logs a message with this logger's logprefix
- Attributes
- protected
- Definition Classes
- Logger
-
def
logError(s: ⇒ String): Unit
log as an error message
log as an error message
- Attributes
- protected
- Definition Classes
- Logger
-
def
logGroup[A](a: ⇒ A): A
wraps around a group to create nested logging
wraps around a group to create nested logging
- Attributes
- protected
- Definition Classes
- Logger
-
def
logPrefix: String
the prefix used to identify this extension for logging, by default the class name
the prefix used to identify this extension for logging, by default the class name
- Definition Classes
- ElaborationBasedSimplifier → Extension → Logger
-
def
logTemp(s: ⇒ String): Unit
temporary logging - always logged
temporary logging - always logged
- Attributes
- protected
- Definition Classes
- Logger
-
def
makeErrorThrower(msg: String): ErrorHandler
an ErrorHandler that wraps an error in a LocalError and throws it
an ErrorHandler that wraps an error in a LocalError and throws it
- Attributes
- protected
- Definition Classes
- Extension
-
def
materialize(context: Context, exp: Term, pathOpt: Option[MPath], tcOpt: Option[TermContainer]): AbstractTheory
Elaborate a theory expression into a module
Elaborate a theory expression into a module
- exp
the theory expression
- pathOpt
the path to use if a new theory has to be created
- tcOpt
the term container hold exp
- Definition Classes
- ElaborationBasedSimplifier → StructureSimplifier
-
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()
-
val
objectLevel: ObjectSimplifier
- Definition Classes
- Simplifier → LeveledExtension
-
def
onAdd(c: StructuralElement): Unit
change management
change management
- Definition Classes
- ElaborationBasedSimplifier → ChangeListener
-
def
onArchiveClose(a: Archive): Unit
called when an archive is removed
called when an archive is removed
- Definition Classes
- ChangeListener
-
def
onArchiveOpen(a: Archive): Unit
called when a new archive is added
called when a new archive is added
- Definition Classes
- ChangeListener
-
def
onCheck(c: StructuralElement): Unit
called after checking the element
called after checking the element
- Definition Classes
- ChangeListener
-
def
onClear: Unit
called after clearing the Constant
called after clearing the Constant
- Definition Classes
- ChangeListener
-
def
onDelete(se: StructuralElement): Unit
deletes all declarations that were added by elaborating se
deletes all declarations that were added by elaborating se
- Definition Classes
- ElaborationBasedSimplifier → ChangeListener
-
def
onFileBuilt(a: Archive, target: TraversingBuildTarget, path: FilePath, res: BuildResult): Unit
called when a file was built
called when a file was built
- Definition Classes
- ChangeListener
-
def
onNavigate(p: Path): Unit
called when navigating to an element
called when navigating to an element
- Definition Classes
- ChangeListener
-
def
onUpdate(old: StructuralElement, nw: StructuralElement): Unit
re-elaborates if old element was
re-elaborates if old element was
- Definition Classes
- ElaborationBasedSimplifier → ChangeListener
- val report: Report
-
def
start(args: List[String]): Unit
extension-specific initialization (override as needed, empty by default)
extension-specific initialization (override as needed, empty by default)
- Definition Classes
- Extension
-
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()
-
def
waitUntilRemainingTasksFinished: Unit
extensions that process tasks in separate threads should override this and wait until those threads are done
extensions that process tasks in separate threads should override this and wait until those threads are done
- Definition Classes
- Extension
Deprecated Value Members
-
def
elaborateContext(outer: Context, con: Context): Context
- Definition Classes
- ElaborationBasedSimplifier → StructureSimplifier
- Annotations
- @MMT_TODO( message = "needs to be reviewed" )
- Deprecated
needs to be reviewed