Packages

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
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Solver
  2. Logger
  3. SolverAlgorithms
  4. CheckingCallback
  5. AnyRef
  6. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. 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

  1. 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

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. 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

  5. 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.

  6. def applyMain: Boolean

    main entry method: runs the solver on the judgment in the checking unit

  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. 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
  9. def checkSucceeded: Boolean

    true if all judgments solved so far succeeded (all variables solved, no delayed constraints, no errors)

  10. val checkingUnit: CheckingUnit
  11. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  12. val constantContext: Context
  13. val controller: Controller
  14. 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

  15. 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
  16. 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
    SolverCheckingCallback
  17. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  18. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  19. def error(message: ⇒ String)(implicit history: History): Boolean

    registers an error, returns false

    registers an error, returns false

    Definition Classes
    SolverCheckingCallback
  20. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  21. 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
  22. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  23. def getConstraints: List[DelayedConstraint]

    returns

    the current list of unresolved constraints

  24. 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

  25. def getDependencies: List[CPath]

    returns

    the current list of dependencies

  26. def getErrors: List[SolverError]

    returns

    the current list of errors and their history

  27. def getModule(p: MPath): Option[Module]
  28. def getPartialSolution: Context

    returns

    the current partial solution to the constraint problem This solution may contain unsolved variables, and there may be unresolved constraints.

  29. 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

  30. def getSolvedVariables: List[LocalName]

    returns

    the the unsolved variables

  31. 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

  32. def getUnsolvedVariables: Context

    returns

    the context containing only the unsolved variables

  33. 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

  34. def hasUnresolvedConstraints: Boolean

    true if unresolved constraints are left

  35. def hasUnsolvedVariables: Boolean

    true if unsolved variables are left

  36. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  37. 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
  38. 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
  39. val initUnknowns: Context
  40. def isDistinctVarList(xs: List[Term])(implicit stack: Stack): Option[Context]
    Attributes
    protected
  41. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  42. def log(e: Error): Unit

    logs an error - always logged

    logs an error - always logged

    Attributes
    protected
    Definition Classes
    Logger
  43. 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
  44. def logAndHistoryGroup[A](body: ⇒ A)(implicit history: History): A
    Attributes
    protected
  45. def logError(s: ⇒ String): Unit

    log as an error message

    log as an error message

    Attributes
    protected
    Definition Classes
    Logger
  46. 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
  47. val logPrefix: String

    the component URI if provided, solver otherwise

    the component URI if provided, solver otherwise

    Definition Classes
    SolverLogger
  48. 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)

  49. def logTemp(s: ⇒ String): Unit

    temporary logging - always logged

    temporary logging - always logged

    Attributes
    protected
    Definition Classes
    Logger
  50. def lookup: LookupWithNotFoundHandler

    lookup

    lookup

    Definition Classes
    SolverCheckingCallback
  51. 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
  52. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  53. 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
  54. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  55. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  56. def outerContext: Context

    the context that is not part of judgements

    the context that is not part of judgements

    Definition Classes
    SolverCheckingCallback
  57. implicit val presentObj: (Obj) ⇒ String

    used for rendering objects, should be used by rules if they want to log

  58. 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
  59. val report: Report

    for Logger

    for Logger

    Definition Classes
    SolverLogger
  60. val rules: RuleSet
  61. 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()
  62. 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()
  63. 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
  64. 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

  65. 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
  66. def solveSubtyping(j: Subtyping)(implicit history: History): Boolean
    Definition Classes
    SolverAlgorithms
  67. 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
  68. def solveTyping(j: Typing)(implicit history: History): Boolean
    Definition Classes
    SolverAlgorithms
  69. 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

  70. def subOrSuper(sub: Boolean)(stack: Stack, t1: Term, t2: Term): Subtyping
    Attributes
    protected
  71. def substituteSolution(o: Obj): ThisType

    replaces all solved unknowns with their solution

  72. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  73. def toString(): String
    Definition Classes
    AnyRef → Any
  74. 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
  75. def tryToCheckWithoutEffect(js: Judgement*): Option[Boolean]

    tries to derive a set of judgments without any side effect (no solving of variables, no delay)

  76. 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
  77. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  78. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  79. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  80. def warning(message: ⇒ String)(implicit history: History): Boolean

    registers a warning, returns false

  81. object Unknown

    an unknown meta-variable see also Solver.makeUnknown

  82. 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

Inherited from Logger

Inherited from SolverAlgorithms

Inherited from CheckingCallback

Inherited from AnyRef

Inherited from Any

Ungrouped