case class CheckingUnit(component: Option[CPath], context: Context, unknowns: Context, judgement: WFJudgement) extends MMTTask with Product with Serializable
A checking unit encapsulates the proof obligations produced by a StructureChecker and passed on to an ObjectChecker.
Typically, each checking unit checks a single term that is part of a WFJudgement, i.e., the other parts of the judgement are assumed to be valid.
- component
the term component that is validated, e.g., namespace?theory?symbol?type
- context
the constant context
- unknowns
the unknown context
- judgement
the typing judgement to check A checking unit involves three contexts, which must be separated because they correspond to a quantifier alternation. The constant context is the (universally quantified) global context that does not change during checking. It includes in particular the theory relative to which a unit is formed. The unknown context is the (existentially quantified) context of unknowns that are to be solved during checking. The variable context is the context that arises from traversing binders during checking. It changes during checking and is therefore stored within the judgement.
- Source
- CheckingUnit.scala
- Alphabetic
- By Inheritance
- CheckingUnit
- Serializable
- Serializable
- Product
- Equals
- MMTTask
- Killable
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
-
new
CheckingUnit(component: Option[CPath], context: Context, unknowns: Context, judgement: WFJudgement)
- component
the term component that is validated, e.g., namespace?theory?symbol?type
- context
the constant context
- unknowns
the unknown context
- judgement
the typing judgement to check A checking unit involves three contexts, which must be separated because they correspond to a quantifier alternation. The constant context is the (universally quantified) global context that does not change during checking. It includes in particular the theory relative to which a unit is formed. The unknown context is the (existentially quantified) context of unknowns that are to be solved during checking. The variable context is the context that arises from traversing binders during checking. It changes during checking and is therefore stored within the judgement.
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
addListener(l: MMTTaskProgressListener): Unit
- Definition Classes
- MMTTask
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
- val component: Option[CPath]
- val context: Context
-
def
diesWith(implicit that: Killable): CheckingUnit.this.type
gives a killable object the same kill button as one that is already around
gives a killable object the same kill button as one that is already around
For example, when processing a task, generates a subtask, this should be called on the subtask to ensure killing the overall task also kills the subtask.
- Definition Classes
- Killable
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
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
getReports: List[MMTTaskProgress]
get all reports in reverse chronological order
get all reports in reverse chronological order
- Definition Classes
- MMTTask
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
isKilled: Boolean
processing should be aborted gracefully if true
processing should be aborted gracefully if true
- Definition Classes
- Killable
- val judgement: WFJudgement
-
def
kill: Unit
signals aborting of processing
signals aborting of processing
- Definition Classes
- Killable
-
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
present(implicit cont: (Obj) ⇒ String): String
a toString method that may call a continuation on its objects
-
def
removeListener(l: MMTTaskProgressListener): Unit
- Definition Classes
- MMTTask
-
def
reportProgress(a: MMTTaskProgress): Unit
adds a report and forwards it to all listeners
adds a report and forwards it to all listeners
- Definition Classes
- MMTTask
-
def
setTimeout[A](millisec: Int)(f: () ⇒ Unit): CheckingUnit.this.type
presses the kill button after the specified number of milli seconds
presses the kill button after the specified number of milli seconds
- Definition Classes
- Killable
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
- val unknowns: Context
-
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()