class Solver extends CheckingCallback with SolverAlgorithms with Logger
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.
- Source
- Solver.scala
- Alphabetic
- By Inheritance
- Solver
- Logger
- SolverAlgorithms
- CheckingCallback
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
-
new
Solver(controller: Controller, checkingUnit: CheckingUnit, rules: RuleSet)
- controller
an MMT controller that is used to look up Rule's and Constant's. No changes are made to the controller.
Type Members
-
class
SubstituteUnknowns extends StatelessTraverser
substitutes some unknowns with solutions pre: solutions are of the form Free(xs,s) where xs.length is the number of arguments of the unknown getSolution returns such a substitution
substitutes some unknowns with solutions pre: solutions are of the form Free(xs,s) where xs.length is the number of arguments of the unknown getSolution returns such a substitution
- Attributes
- protected
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
addUnknowns(newVars: Context, before: Option[LocalName]): Boolean
- newVars
new unknowns; creating new unknowns during checking permits variable transformations
- before
the variable before which to insert the new ones, otherwise insert at end
-
def
apply(j: Judgement): Boolean
applies this Solver to one Judgement This method can be called multiple times to solve a system of constraints.
applies this Solver to one Judgement This method can be called multiple times to solve a system of constraints.
- j
the Judgement
- returns
if false, j is disproved; if true, j holds relative to all delayed judgements Note that this may return true even if j can be disproved, namely if the delayed judgements are disproved later. If this returns false, an error must have been registered.
-
def
applyMain: Boolean
main entry method: runs the solver on the judgment in the checking unit
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
check(j: Judgement)(implicit history: History): Boolean
general entry point for checking a judgement
general entry point for checking a judgement
This is the method that should be used to recurse into a hypothesis. It handles logging and error reporting and delegates to specific methods based on the judgement.
The apply method is similar but additionally simplifies the judgment.
- j
the judgement
- returns
like apply
- Definition Classes
- SolverAlgorithms
-
def
checkSucceeded: Boolean
true if all judgments solved so far succeeded (all variables solved, no delayed constraints, no errors)
- val checkingUnit: CheckingUnit
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
- val constantContext: Context
- val controller: Controller
-
def
defineByConstraint(x: LocalName, tp: Term)(constraint: (Term) ⇒ Boolean): Boolean
define x:tp as the unique value that satisfies the constraint
define x:tp as the unique value that satisfies the constraint
this is implemented by adding a fresh unknown, and running the constraint this can be used to compute a value in logic programming style, where the computation is given by a functional predicate
-
def
delay(j: Judgement)(implicit history: History): Boolean
delays a constraint for future processing
delays a constraint for future processing
- j
the Judgement to be delayed
- returns
true (i.e., delayed Judgment's always return success)
- Attributes
- protected
-
def
dryRun[A](allowDelay: Boolean, commitOnSuccess: (A) ⇒ Boolean)(a: ⇒ A): DryRunResult
tries to evaluate an expression without any generating new constraints
tries to evaluate an expression without any generating new constraints
- commitOnSuccess
do not roll back state changes if successful
- a
the expression
- Definition Classes
- Solver → CheckingCallback
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
error(message: ⇒ String)(implicit history: History): Boolean
registers an error, returns false
registers an error, returns false
- Definition Classes
- Solver → CheckingCallback
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
def
findUniqueInhabitant(tp: Term, covered: Boolean = false)(implicit stack: Stack, history: History): Option[Term]
tries to find a unique term of a given type by applying TypeBaseSolutionRules
tries to find a unique term of a given type by applying TypeBaseSolutionRules
- tp
the type
- stack
its Context
- returns
the found term, if search succeeded pre: context and tp are covered post: if result, typing judgment is covered
- Definition Classes
- SolverAlgorithms
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getConstraints: List[DelayedConstraint]
- returns
the current list of unresolved constraints
-
def
getDef(p: GlobalName)(implicit h: History): Option[Term]
retrieves the definiens of a constant and registers the dependency
retrieves the definiens of a constant and registers the dependency
returns nothing if the type could not be reconstructed
-
def
getDependencies: List[CPath]
- returns
the current list of dependencies
-
def
getErrors: List[SolverError]
- returns
the current list of errors and their history
- def getModule(p: MPath): Option[Module]
-
def
getPartialSolution: Context
- returns
the current partial solution to the constraint problem This solution may contain unsolved variables, and there may be unresolved constraints.
-
def
getSolution: Option[Substitution]
the solution to the constraint problem
the solution to the constraint problem
- returns
None if there are unresolved constraints or unsolved variables; Some(solution) otherwise
-
def
getSolvedVariables: List[LocalName]
- returns
the the unsolved variables
-
def
getType(p: GlobalName)(implicit h: History): Option[Term]
retrieves the type type of a constant and registers the dependency
retrieves the type type of a constant and registers the dependency
returns nothing if the type could not be reconstructed
-
def
getUnsolvedVariables: Context
- returns
the context containing only the unsolved variables
-
def
getVar(name: LocalName)(implicit stack: Stack): VarDecl
looks up a variable in the appropriate context
looks up a variable in the appropriate context
- returns
the variable declaration for name
-
def
hasUnresolvedConstraints: Boolean
true if unresolved constraints are left
-
def
hasUnsolvedVariables: Boolean
true if unsolved variables are left
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
inferType(tm: Term, covered: Boolean = false)(implicit stack: Stack, history: History): Option[Term]
infers the type of a term by applying InferenceRule's
infers the type of a term by applying InferenceRule's
- tm
the term
- stack
its Context
- returns
the inferred type, if inference succeeded This method should not be called by users (instead, use object Solver.check). It is only public because it serves as a callback for Rule's. pre: context is covered post: if result, typing judgment is covered
- Definition Classes
- SolverAlgorithms
-
def
inferTypeAndThen(tm: Term)(stack: Stack, history: History)(cont: (Term) ⇒ Boolean): Boolean
performs a type inference and calls a continuation function on the inferred type
performs a type inference and calls a continuation function on the inferred type
If type inference is not successful, this is delayed.
- Definition Classes
- SolverAlgorithms
- val initUnknowns: Context
-
def
isDistinctVarList(xs: List[Term])(implicit stack: Stack): Option[Context]
- Attributes
- protected
-
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
logAndHistoryGroup[A](body: ⇒ A)(implicit history: History): A
- Attributes
- protected
-
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
-
val
logPrefix: String
the component URI if provided, solver otherwise
-
def
logState(prefix: String = logPrefix): Unit
logs a string representation of the current state
logs a string representation of the current state
- prefix
the log prefix to use (the normal one by default) (occasionally it's useful to use a different prefix, e.g., "error" or when the normal prefix is not logged but the result should be)
-
def
logTemp(s: ⇒ String): Unit
temporary logging - always logged
temporary logging - always logged
- Attributes
- protected
- Definition Classes
- Logger
-
def
lookup: LookupWithNotFoundHandler
lookup
lookup
- Definition Classes
- Solver → CheckingCallback
-
def
moveToRight(name: LocalName): Unit
moves declarations in solution to the right so that 'name' occurs as far to the right as allowed by dependencies
moves declarations in solution to the right so that 'name' occurs as far to the right as allowed by dependencies
- Attributes
- protected
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
notAllowedInSolution(m: LocalName, tm: Term)(implicit stack: Stack, history: History): List[LocalName]
- m
an unknown variable
- returns
if m is an unknown, the list of free variables of tm that preclude solving type/definition of m as tm namely the bound variables and the unknowns declared after m
- Attributes
- protected
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
outerContext: Context
the context that is not part of judgements
the context that is not part of judgements
- Definition Classes
- Solver → CheckingCallback
-
implicit
val
presentObj: (Obj) ⇒ String
used for rendering objects, should be used by rules if they want to log
-
def
prove(conc: Term, allowUnknowns: Boolean = true)(implicit stack: Stack, history: History): Option[Term]
tries to prove a goal by finding a term of type conc If conc contains unknowns, this is unlikely to succeed unless an appropriate assumption is in the context.
tries to prove a goal by finding a term of type conc If conc contains unknowns, this is unlikely to succeed unless an appropriate assumption is in the context.
- Definition Classes
- SolverAlgorithms
-
val
report: Report
for Logger
- val rules: RuleSet
-
final
def
safeSimplifyUntil[A](tm1: Term, tm2: Term)(simple: (Term, Term) ⇒ Option[A])(implicit stack: Stack, history: History): (Term, Term, Option[A])
like the other method but simplifies two terms in parallel
like the other method but simplifies two terms in parallel
- Definition Classes
- SolverAlgorithms
- Annotations
- @tailrec()
-
final
def
safeSimplifyUntil[A](tm: Term)(simple: (Term) ⇒ Option[A])(implicit stack: Stack, history: History): (Term, Option[A])
applies ComputationRules expands definitions until a condition is satisfied; A typical case is transformation into weak head normal form.
applies ComputationRules expands definitions until a condition is satisfied; A typical case is transformation into weak head normal form.
- tm
the term to simplify (It may be simple already.)
- simple
a term is considered simple if this function returns a non-None result
- stack
the context of tm
- returns
(tmS, Some(a)) if tmS is simple and simple(tm)=tmS; (tmS, None) if tmS is not simple but no further simplification rules are applicable
- Definition Classes
- SolverAlgorithms
- Annotations
- @tailrec()
-
def
simplify(t: Obj)(implicit stack: Stack, history: History): ThisType
special case simplify: no expansion, full recursion
special case simplify: no expansion, full recursion
- Definition Classes
- SolverAlgorithms
-
def
solve(name: LocalName, value: Term)(implicit history: History): Boolean
registers the solution for an unknown variable
registers the solution for an unknown variable
If a solution exists already, their equality is checked.
- name
the solved variable
- value
the solution; must not contain object variables, but may contain meta-variables that are declared before the solved variable
- returns
true unless the solution differs from an existing one precondition: value is well-typed if the overall check succeeds
-
def
solveBound(name: LocalName, value: Term, below: Boolean)(implicit history: History): Boolean
solves a type bound for an unknown
solves a type bound for an unknown
- below
if true, name <: value, else name :> value
- Attributes
- protected
-
def
solveSubtyping(j: Subtyping)(implicit history: History): Boolean
- Definition Classes
- SolverAlgorithms
-
def
solveType(name: LocalName, value: Term)(implicit history: History): Boolean
registers the solved type for a variable
registers the solved type for a variable
If a type exists already, their equality is checked.
- name
the variable
- value
the type; must not contain object variables, but may contain meta-variables that are declared before the solved variable
- returns
true unless the type differs from an existing one precondition: value is well-typed if the the overall check succeeds
- Attributes
- protected
-
def
solveTyping(j: Typing)(implicit history: History): Boolean
- Definition Classes
- SolverAlgorithms
-
val
stability: Stability
for marking objects as stable, created fresh for every run because stability depends on the context and we do not want to have to remove the marker
-
def
subOrSuper(sub: Boolean)(stack: Stack, t1: Term, t2: Term): Subtyping
- Attributes
- protected
-
def
substituteSolution(o: Obj): ThisType
replaces all solved unknowns with their solution
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
def
tryToCheckWithoutDelay(js: Judgement*): Option[Boolean]
tries to check some judgments without delaying constraints
tries to check some judgments without delaying constraints
if this returns None, the check is inconclusive at this point, and no state changes were applied if this returns Some(true), all judgments have been derived and all state changes are applied if this returns Some(false), no state changes are applied and the caller still has to generate an error message, possibly by calling check(j)
- Definition Classes
- CheckingCallback
-
def
tryToCheckWithoutEffect(js: Judgement*): Option[Boolean]
tries to derive a set of judgments without any side effect (no solving of variables, no delay)
-
def
typeCheckSolution(vd: VarDecl)(implicit history: History): Boolean
if the type and the definiens of an unknown are solved independently, this type-checks them
if the type and the definiens of an unknown are solved independently, this type-checks them
- Attributes
- protected
-
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
warning(message: ⇒ String)(implicit history: History): Boolean
registers a warning, returns false
-
object
Unknown
an unknown meta-variable see also Solver.makeUnknown
-
object
state
to have better control over state changes, all stateful variables are encapsulated a second time
to have better control over state changes, all stateful variables are encapsulated a second time
- Attributes
- protected