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
- Alphabetic
- By Inheritance
- SolverAlgorithms
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
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
-
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
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
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
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
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
-
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.
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
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
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.
-
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()
-
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()
-
def
simplify(t: Obj)(implicit stack: Stack, history: History): ThisType
special case simplify: no expansion, full recursion
- def solveSubtyping(j: Subtyping)(implicit history: History): Boolean
- def solveTyping(j: Typing)(implicit history: History): Boolean
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
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()