package checking
The algorithm for checking MMT content. See api for an overview of the algorithms.
The main interfaces are - Checker: the main interface for checkers (combining a structure and an object checker) - StructureChecker: checking structural elements - ObjectChecker: checking objects
The main implementations are - MMTStructureChecker for structural elements - RuleBasedChecker for objects
The latter creates a Solver for each judgment, which perform type reconstruction.
Structure checking is not extensible except through DerivedElements. Object checking is extensible through Rules.
- Source
- package.scala
- Alphabetic
- By Inheritance
- checking
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
- class AbbreviationRuleGenerator extends ChangeListener
-
trait
ApplicableUnder extends SingleTermBasedCheckingRule
used to change the 'applicable' method when the head symbol of the rule occurs under some HOAS apply operators
- class BranchInfo extends AnyRef
-
class
Branchpoint extends AnyRef
experimental backtracking support in Solver
-
abstract
class
Checker extends StructureChecker with ObjectChecker with LeveledExtension
the designated super class for all checkers
-
trait
CheckingCallback extends AnyRef
passed to Rules to permit callbacks to the Solver
- class CheckingEnvironment extends AnyRef
-
case class
CheckingResult(solved: Boolean, solution: Option[Context], term: Term) extends Product with Serializable
A checking result encapsulates all information returned by an ObjectChecker.
A checking result encapsulates all information returned by an ObjectChecker.
See CheckingUnit.
- solved
true if term was checked successfully
- solution
the substitution for the unknown context (possibly partial)
- term
the checked version of the term (possibly approximate if check failed)
-
trait
CheckingRule extends SyntaxDrivenRule
super class of all rules primarily used by the Solver
-
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.
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.
-
case class
Comment(text: () ⇒ String) extends HistoryEntry with Product with Serializable
a HistoryEntry that consists of a string, meant as a log or error message
-
abstract
class
ComputationRule extends SingleTermBasedCheckingRule
A ComputationRule simplifies an expression operating at the toplevel of the term.
A ComputationRule simplifies an expression operating at the toplevel of the term. But it may recursively simplify the components if that makes the rule applicable. The rule must preserve equality and well-typedness of the simplified term. If necessary, additional checks must be performed.
-
class
CongruenceRule extends TermHeadBasedEqualityRule
Congruence as a TermBasedEqualityRule for two terms with the same head
-
class
Continue[A] extends AnyRef
continuation used by some rules
-
class
DelarativeVarianceRule extends VarianceRule
VarianceRule for OMA(op, args) defined by giving a variance annotation for each arg
-
abstract
class
DelayedConstraint extends AnyRef
A wrapper around a Judgement to maintain meta-information while a constraint is delayed
-
class
DelayedInference extends DelayedConstraint
A wrapper around a continuation function to be delayed until a certain type inference succeeds
-
class
DelayedJudgement extends DelayedConstraint
A wrapper around a Judgement to maintain meta-information while a constraint is delayed
-
sealed
trait
DryRunResult extends AnyRef
returned by Solver.dryRun as the result of a side-effect-free check
- abstract class EliminationRule extends InferenceRule
-
case class
Expectation(tp: Option[Term], df: Option[Term]) extends Product with Serializable
auxiliary class for the MMTStructureChecker to store expectations about a constant
-
case class
ExtendedCheckingEnvironment(ce: CheckingEnvironment, objectChecker: ObjectChecker, rules: RuleSet, current: Path, timeout: Int = 0) extends Product with Serializable
variant of CheckingEnvironment that carries around more structure
-
abstract
class
ExtensionalityRule extends TypeBasedEqualityRule
For extensionality rules, it makes sense to make applicableToTerm true only for terms that can be reduced after applying the elimination form, i.e., for terms that are not stable or an introduction form.
- abstract class FormationRule extends InferenceRule
-
abstract
class
ForwardSolutionRule extends SingleTermBasedCheckingRule
A ForwardSolutionRule solves for an unknown by inspecting its declarations (as opposed to its use) It can solve a variable directly (e.g., if it has unit type) or apply a variable transformation (e.g., X --> (X1,X2) if X has product type).
- class History extends AnyRef
-
trait
HistoryEntry extends AnyRef
wrapper for classes that can occur in the History
-
case class
IndentedHistoryEntry(e: HistoryEntry, level: Int) extends HistoryEntry with Product with Serializable
The History is a branch in the tree of decisions, messages, and judgements that occurred during type-checking
The History is a branch in the tree of decisions, messages, and judgements that occurred during type-checking
The most import History's are those ending in an error message. See Solver.getErrors
-
abstract
class
InferenceAndTypingRule extends InferenceRule
A variant of InferenceRule that may additionally use the expected type.
A variant of InferenceRule that may additionally use the expected type. Thus it can be used both for type inference and for type checking.
-
abstract
class
InferenceRule extends SingleTermBasedCheckingRule with MaytriggerBacktrack
An InferenceRule infers the type of an expression It may recursively infer the types of components.
-
abstract
class
InhabitableRule extends UnaryTermRule
checks an Inhabitable judgement
-
abstract
class
Interpreter extends Importer
parses and returns a checked result
- abstract class IntroductionRule extends InferenceRule
-
class
MMTStructureChecker extends Checker
A StructureChecker traverses structural elements and checks them, calling the object checker as needed.
A StructureChecker traverses structural elements and checks them, calling the object checker as needed.
After checking an element, it is immediately elaborated.
Deriving classes may override unitCont and reCont to customize the behavior.
-
trait
MaytriggerBacktrack extends AnyRef
rules can throw this exception after being called if they are not applicable because actual back-tracking is not implemented yet, they may only do so if they have not recursed into any state-changing judgments yet
- case class MightFail(history: History) extends Throwable with ThrowableDryRunResult with Product with Serializable
-
trait
ObjectChecker extends Extension
checks objects
checks objects
see also Checker
-
class
OneStepInterpreter extends Interpreter
an interpreter created from a trusted parser
-
trait
RelationHandler extends AnyRef
type of continuation functions passed to an ObjectChecker to report dependencies
-
class
RuleBasedChecker extends ObjectChecker
the primary object level checker of MMT
the primary object level checker of MMT
It checks CheckingUnits by invoking Solvers and updates the checked objects with the solutions. It manages errors and dependencies.
- trait SingleTermBasedCheckingRule extends CheckingRule
-
abstract
class
SolutionRule extends CheckingRule
A SolutionRule tries to isolate an unknown that occurs in a judgement.
A SolutionRule tries to isolate an unknown that occurs in a judgement.
It may be partial by, e.g., by inverting the toplevel operation of a Term without completely isolating an unknown occurring in it.
-
class
Solver extends CheckingCallback with SolverAlgorithms with Logger
A Solver is used to solve a system of constraints about Term's given as judgments.
A Solver is used to solve a system of constraints about Term's given as judgments.
The judgments may contain unknown variables (also called meta-variables or logic variables); variables may represent any MMT term, i.e., object language terms, types, etc.; the solution is a Substitution that provides a closed Term for every unknown variable. (Higher-order abstract syntax should be used to represent unknown terms with free variables as closed function terms.)
The Solver decomposes the judgments individually by applying typing rules, collecting (partial) solutions along the way and possibly delaying unsolvable judgments. If the unknown variables are untyped and rules require a certain type, the Solver adds the type.
Unsolvable constraints are delayed and reactivated if later solving of unknowns provides further information.
-
trait
SolverAlgorithms extends AnyRef
the essential subalgorithms of a bidirectional type-checking, factored out from the Solver class, which holds all bureaucracy
-
case class
SolverError(level: Level.Level, history: History, msgO: Option[((Obj) ⇒ String) ⇒ String] = None) extends Product with Serializable
error/warning produced by Solver
-
class
Stability extends BooleanTermProperty
used by Solver to mark a term as head-normal: no simplification rule can change the head symbol
-
trait
StructureChecker extends FormatBasedExtension
checks structural elements
checks structural elements
see also Checker
INVARIANTS: apply(se) must be equivalent to - for ContainerElement's: applyElementBegin(se) + se.getPrimitiveDeclarations.foreach(apply) + applyElementEnd(se) - for other elements: apply(se) must be equivalent to applyElementBegin(se)
That way all calls to the StructureParserContinuations together check the entire element.
-
abstract
class
SubtypingRule extends CheckingRule
A SubtypingRule handles Subtyping judgements
- case class Success[A](result: A) extends DryRunResult with Product with Serializable
-
abstract
class
SupertypeRule extends SingleTermBasedCheckingRule
A SupertypeRule represnts a type as a subtype of a bigger one
-
abstract
class
TermBasedEqualityRule extends CheckingRule
A TermBasedEqualityRule checks the equality of two terms without considering types
-
abstract
class
TermHeadBasedEqualityRule extends TermBasedEqualityRule
A TermBasedEqualityRule checks the equality of two terms with certain heads
- sealed trait ThrowableDryRunResult extends Throwable with DryRunResult
-
class
TwoStepInterpreter extends Interpreter
a combination of a Parser and a Checker
-
abstract
class
TypeBasedEqualityRule extends SingleTermBasedCheckingRule with ApplicableUnder
A TypeBasedEqualityRule checks the equality of two terms based on the head of their type
-
abstract
class
TypeBasedSolutionRule extends TypeBasedEqualityRule
A TypeBasedSolutionRule solves an unknown based on its type, by constructing a term of that type.
A TypeBasedSolutionRule solves an unknown based on its type, by constructing a term of that type. This is legal if all terms of that type are equal.
-
case class
TypeBound(bound: Term, upper: Boolean) extends Product with Serializable
stores a type bound for an unknown as used in the Solver
-
abstract
class
TypeCoercionRule extends CheckingRule with ApplicableUnder
a type coercion rule lifts a non-type A to the type lift(A) if A occurs where a type is expected
-
abstract
class
TypeSolutionRule extends SolutionRule
A TypeSolutionRule tries to solve for the type of an unknown in the term of a typing judgment.
-
abstract
class
TypingRule extends SingleTermBasedCheckingRule
An TypingRule checks a term against a type.
An TypingRule checks a term against a type. It may recursively call other checks.
-
abstract
class
UnaryTermRule extends SingleTermBasedCheckingRule
A UnaryTermRule checks a UnaryTermJudgement
-
abstract
class
UniverseRule extends UnaryTermRule
checks a Universe judgement
-
abstract
class
ValueSolutionRule extends SolutionRule
A ValueSolutionRule tries to solve for the value an unknown in an equality judgment.
A ValueSolutionRule tries to solve for the value an unknown in an equality judgment.
f(t1) = t2 ---> t1 = g(t2), where t1 contains a target variable that we try to isolate
-
sealed abstract
class
Variance extends AnyRef
variances annotations, used by DelarativeVarianceRule
-
abstract
class
VarianceRule extends SubtypingRule
applies to op(args1) <: op(args2)
-
abstract
class
TheoryExpRule extends InferenceRule
- Annotations
- @MMT_TODO( message = "must be reimplemented cleanly" )
- Deprecated
must be reimplemented cleanly
Value Members
- object CheckingUnit extends Serializable
- object Continue
- object Contravariant extends Variance with Product with Serializable
- object Covariant extends Variance with Product with Serializable
-
object
Disambiguation extends ComputationRule
oneOf(OMI(i),a_0,...a_n) ---> a_i
-
object
ForwardSolutionRule
auxiliary object for the class ForwardSolutionRule
-
object
Hole
apply/unapply methods for missing terms of known type
- object HoleTerm extends InferenceRule
- object Ignorevariant extends Variance with Product with Serializable
-
object
InferAmbiguous extends InferenceAndTypingRule
solves unknown X in oneOf(X,a_0,...a_n) as i iff a_i is the only alternative whose type can be inferred
-
object
InferredType extends TermProperty[(Branchpoint, Term)]
used by Solver to store inferred types with terms
- object Invariant extends Variance with Product with Serializable
-
object
NoHistory extends History
a history that ignores all messages
-
object
NullChecker
trivial checkers that do nothing
- object RelationHandler
-
object
Solver
auxiliary methods and high-level type reconstruction API
- object Stability
- object TypingRule
-
object
UncheckedElement extends BooleanClientProperty[StructuralElement]
if set, the element appears to be in scope but has not been checked yet
- object WouldFail extends Throwable with ThrowableDryRunResult with Product with Serializable