Packages

t

info.kwarc.mmt.api.checking

SolverAlgorithms

trait SolverAlgorithms extends AnyRef

the essential subalgorithms of a bidirectional type-checking, factored out from the Solver class, which holds all bureaucracy

Self Type
Solver
Source
SolverAlgorithms.scala
Linear Supertypes
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SolverAlgorithms
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. 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

  6. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  7. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  8. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  9. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  10. 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

  11. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. 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

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

  15. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  16. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  19. 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.

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

    Annotations
    @tailrec()
  21. 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

    Annotations
    @tailrec()
  22. def simplify(t: Obj)(implicit stack: Stack, history: History): ThisType

    special case simplify: no expansion, full recursion

  23. def solveSubtyping(j: Subtyping)(implicit history: History): Boolean
  24. def solveTyping(j: Typing)(implicit history: History): Boolean
  25. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  26. def toString(): String
    Definition Classes
    AnyRef → Any
  27. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  28. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  29. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from AnyRef

Inherited from Any

Ungrouped