source
opaque Lean.Meta.synthInstance.maxHeartbeats :
Lean.Option Nat
source
opaque Lean.Meta.synthInstance.maxSize :
Lean.Option Nat
source
opaque Lean.Meta.backward.synthInstance.canonInstances :
Lean.Option Bool
source
def Lean.Meta.SynthInstance.getMaxHeartbeats (opts : Options) :
Nat
Equations

- Lean.Meta.SynthInstance.getMaxHeartbeats opts = Lean.Option.get opts Lean.Meta.synthInstance.maxHeartbeats * 1000

Instances For

source
structure Lean.Meta.SynthInstance.Instance :
Type

- val : Expr
- synthOrder : Array Nat

Instances For

source
def Lean.Meta.SynthInstance.instInhabitedInstance.default :
Instance
Equations

- Lean.Meta.SynthInstance.instInhabitedInstance.default = { val := default, synthOrder := default }

Instances For

source
instance Lean.Meta.SynthInstance.instInhabitedInstance :
Inhabited Instance
Equations

- Lean.Meta.SynthInstance.instInhabitedInstance = { default := Lean.Meta.SynthInstance.instInhabitedInstance.default }

source
structure Lean.Meta.SynthInstance.GeneratorNode :
Type

- mvar : Expr
- key : Expr
- mctx : MetavarContext
- instances : Array Instance
- currInstanceIdx : Nat
- typeHasMVars : Bool

  `typeHasMVars := true` if type of `mvar` contains metavariables. We store this information to implement an optimization that relies on the fact that instances are "morally canonical." That is, we need to find at most one answer for this generator node if the type does not have metavariables.

Instances For

source
def Lean.Meta.SynthInstance.instInhabitedGeneratorNode.default :
GeneratorNode
Equations

- Lean.Meta.SynthInstance.instInhabitedGeneratorNode.default = { mvar := default, key := default, mctx := default, instances := default, currInstanceIdx := default, typeHasMVars := default }

Instances For

source
instance Lean.Meta.SynthInstance.instInhabitedGeneratorNode :
Inhabited GeneratorNode
Equations

- Lean.Meta.SynthInstance.instInhabitedGeneratorNode = { default := Lean.Meta.SynthInstance.instInhabitedGeneratorNode.default }

source
structure Lean.Meta.SynthInstance.ConsumerNode :
Type

- mvar : Expr
- key : Expr
- mctx : MetavarContext
- subgoals : List Expr
- size : Nat

Instances For

source
def Lean.Meta.SynthInstance.instInhabitedConsumerNode.default :
ConsumerNode
Equations

- Lean.Meta.SynthInstance.instInhabitedConsumerNode.default = { mvar := default, key := default, mctx := default, subgoals := default, size := default }

Instances For

source
instance Lean.Meta.SynthInstance.instInhabitedConsumerNode :
Inhabited ConsumerNode
Equations

- Lean.Meta.SynthInstance.instInhabitedConsumerNode = { default := Lean.Meta.SynthInstance.instInhabitedConsumerNode.default }

source
inductive Lean.Meta.SynthInstance.Waiter :
Type

- consumerNode : ConsumerNode → Waiter
- root : Waiter

Instances For

source
def Lean.Meta.SynthInstance.Waiter.isRoot :
Waiter → Bool
Equations

- (Lean.Meta.SynthInstance.Waiter.consumerNode a).isRoot = false
- Lean.Meta.SynthInstance.Waiter.root.isRoot = true

Instances For

In tabled resolution, we creating a mapping from goals (e.g., `Coe Nat ?x`) to answers and waiters. Waiters are consumer nodes that are waiting for answers for a particular node.

We implement this mapping using a `HashMap` where the keys are normalized expressions. That is, we replace assignable metavariables with auxiliary free variables of the form `_tc.<idx>`. We do not declare these free variables in any local context, and we should view them as "normalized names" for metavariables. For example, the term `f ?m ?m ?n` is normalized as `f _tc.0 _tc.0 _tc.1`.

This approach is structural, and we may visit the same goal more than once if the different occurrences are just definitionally equal, but not structurally equal.

Remark: a metavariable is assignable only if its depth is equal to the metavar context depth.

source
structure Lean.Meta.SynthInstance.MkTableKey.State :
Type

- nextIdx : Nat
- lmap : Std.HashMap LMVarId Level
- emap : Std.HashMap MVarId Expr
- mctx : MetavarContext

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.SynthInstance.MkTableKey.M (α : Type) :
Type
Equations

- Lean.Meta.SynthInstance.MkTableKey.M = StateM Lean.Meta.SynthInstance.MkTableKey.State

Instances For

source
@[always_inline]
instance Lean.Meta.SynthInstance.MkTableKey.instMonadMCtxM :
MonadMCtx M
Equations

- One or more equations did not get rendered due to their size.

source
partial def Lean.Meta.SynthInstance.MkTableKey.normLevel (u : Level) :
M Level
source
partial def Lean.Meta.SynthInstance.MkTableKey.normExpr (e : Expr) :
M Expr
source
def Lean.Meta.SynthInstance.mkTableKey {m : Type → Type} [Monad m] [MonadMCtx m] (e : Expr) :
m Expr

Remark: `mkTableKey` assumes `e` does not contain assigned metavariables.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Lean.Meta.SynthInstance.Answer :
Type

- result : AbstractMVarsResult
- resultType : Expr
- size : Nat

Instances For

source
instance Lean.Meta.SynthInstance.instInhabitedAnswer :
Inhabited Answer
Equations

- Lean.Meta.SynthInstance.instInhabitedAnswer = { default := Lean.Meta.SynthInstance.instInhabitedAnswer.default }

source
def Lean.Meta.SynthInstance.instInhabitedAnswer.default :
Answer
Equations

- Lean.Meta.SynthInstance.instInhabitedAnswer.default = { result := default, resultType := default, size := default }

Instances For

source
structure Lean.Meta.SynthInstance.TableEntry :
Type

- waiters : Array Waiter
- answers : Array Answer

Instances For

source
structure Lean.Meta.SynthInstance.Context :
Type

- maxResultSize : Nat
- maxHeartbeats : Nat

Instances For

source
structure Lean.Meta.SynthInstance.State :
Type

Remark: the SynthInstance.State is not really an extension of `Meta.State`. The field `postponed` is not needed, and the field `mctx` is misleading since `synthInstance` methods operate over different `MetavarContext`s simultaneously. That being said, we still use `extends` because it makes it simpler to move from `M` to `MetaM`.

- result? : Option AbstractMVarsResult
- generatorStack : Array GeneratorNode
- resumeStack : Array (ConsumerNode × Answer)
- tableEntries : Std.HashMap Expr TableEntry

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.SynthInstance.SynthM (α : Type) :
Type
Equations

- Lean.Meta.SynthInstance.SynthM = ReaderT Lean.Meta.SynthInstance.Context (StateRefT' IO.RealWorld Lean.Meta.SynthInstance.State Lean.MetaM)

Instances For

source
def Lean.Meta.SynthInstance.checkSystem :
SynthM Unit
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.Meta.SynthInstance.instInhabitedSynthM {α : Type} :
Inhabited (SynthM α)
Equations

- Lean.Meta.SynthInstance.instInhabitedSynthM = { default := fun (x : Lean.Meta.SynthInstance.Context) (x_1 : ST.Ref IO.RealWorld Lean.Meta.SynthInstance.State) => default }

source
def Lean.Meta.SynthInstance.getInstances (type : Expr) :
MetaM (Array Instance)

Return globals and locals instances that may unify with `type`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.mkGeneratorNode? (key mvar : Expr) :
MetaM (Option GeneratorNode)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.newSubgoal (mctx : MetavarContext) (key mvar : Expr) (waiter : Waiter) :
SynthM Unit

Create a new generator node for `mvar` and add `waiter` as its waiter. `key` must be `mkTableKey mctx mvarType`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.findEntry? (key : Expr) :
SynthM (Option TableEntry)
Equations

- Lean.Meta.SynthInstance.findEntry? key = do let __do_lift ← get pure __do_lift.tableEntries[key]?

Instances For

source
def Lean.Meta.SynthInstance.getEntry (key : Expr) :
SynthM TableEntry
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.mkTableKeyFor (mctx : MetavarContext) (mvar : Expr) :
SynthM Expr

Create a `key` for the goal associated with the given metavariable. That is, we create a key for the type of the metavariable.

We must instantiate assigned metavariables before we invoke `mkTableKey`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Lean.Meta.SynthInstance.SubgoalsResult :
Type

See `getSubgoals` and `getSubgoalsAux`

We use the parameter `j` to reduce the number of `instantiate*` invocations. It is the same approach we use at `forallTelescope` and `lambdaTelescope`. Given `getSubgoalsAux args j subgoals instVal type`, we have that `type.instantiateRevRange j args.size args` does not have loose bound variables.

- subgoals : List Expr
- instVal : Expr
- instTypeBody : Expr

Instances For

source
def Lean.Meta.SynthInstance.getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr) (inst : Instance) :
MetaM SubgoalsResult

`getSubgoals lctx localInsts xs inst` creates the subgoals for the instance `inst`. The subgoals are in the context of the free variables `xs`, and `(lctx, localInsts)` is the local context and instances before we added the free variables to it.

This extra complication is required because 1- We want all metavariables created by `synthInstance` to share the same local context. 2- We want to ensure that applications such as `mvar xs` are higher order patterns.

The method `getGoals` create a new metavariable for each parameter of `inst`. For example, suppose the type of `inst` is `forall (x_1 : A_1) ... (x_n : A_n), B x_1 ... x_n`. Then, we create the metavariables `?m_i : forall xs, A_i`, and return the subset of these metavariables that are instance implicit arguments, and the expressions:

- `inst (?m_1 xs) ... (?m_n xs)` (aka `instVal`)
- `B (?m_1 xs) ... (?m_n xs)`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.tryResolve (mvar : Expr) (inst : Instance) :
MetaM (Option (MetavarContext × List Expr))

Try to synthesize metavariable `mvar` using the instance `inst`. Remark: `mctx` is set using `withMCtx`. If it succeeds, the result is a new updated metavariable context and a new list of subgoals. A subgoal is created for each instance implicit parameter of `inst`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.tryAnswer (mctx : MetavarContext) (mvar : Expr) (answer : Answer) :
SynthM (Option MetavarContext)

Assign a precomputed answer to `mvar`. If it succeeds, the result is a new updated metavariable context and a new list of subgoals.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.wakeUp (answer : Answer) :
Waiter → SynthM Unit

Move waiters that are waiting for the given answer to the resume stack.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.isNewAnswer (oldAnswers : Array Answer) (answer : Answer) :
Bool
Equations

- Lean.Meta.SynthInstance.isNewAnswer oldAnswers answer = oldAnswers.all fun (oldAnswer : Lean.Meta.SynthInstance.Answer) => oldAnswer.resultType != answer.resultType

Instances For

source
def Lean.Meta.SynthInstance.addAnswer (cNode : ConsumerNode) :
SynthM Unit

Create a new answer after `cNode` resolved all subgoals. That is, `cNode.subgoals == []`. And then, store it in the tabled entries map, and wakeup waiters.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.consume (cNode : ConsumerNode) :
SynthM Unit

Process the next subgoal in the given consumer node.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.getTop :
SynthM GeneratorNode
Equations

- Lean.Meta.SynthInstance.getTop = do let __do_lift ← get pure __do_lift.generatorStack.back!

Instances For

source
@[inline]
def Lean.Meta.SynthInstance.modifyTop (f : GeneratorNode → GeneratorNode) :
SynthM Unit
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.generate :
SynthM Unit

Try the next instance in the node on the top of the generator stack.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.getNextToResume :
SynthM (ConsumerNode × Answer)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.resume :
SynthM Unit

Given `(cNode, answer)` on the top of the resume stack, continue execution by using `answer` to solve the next subgoal.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.step :
SynthM Bool
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.SynthInstance.getResult :
SynthM (Option AbstractMVarsResult)
Equations

- Lean.Meta.SynthInstance.getResult = do let __do_lift ← get pure __do_lift.result?

Instances For

source
partial def Lean.Meta.SynthInstance.synth :
SynthM (Option AbstractMVarsResult)
source
def Lean.Meta.SynthInstance.main (type : Expr) (maxResultSize : Nat) :
MetaM (Option AbstractMVarsResult)
Equations

- One or more equations did not get rendered due to their size.

Instances For

Type class parameters can be annotated with `outParam` annotations.

Given `C a_1 ... a_n`, we replace `a_i` with a fresh metavariable `?m_i` IF `a_i` is an `outParam`. The result is type correct because we reject type class declarations IF it contains a regular parameter X that depends on an `out` parameter Y.

Then, we execute type class resolution as usual. If it succeeds, and metavariables ?m_i have been assigned, we try to unify the original type `C a_1 ... a_n` with the normalized one.

Remark: when `maxResultSize? == none`, the configuration option `synthInstance.maxResultSize` is used. Remark: we use a different option for controlling the maximum result size for coercions.

source
def Lean.Meta.synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) :
MetaM (Option Expr)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) :
MetaM (Option Expr)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.trySynthInstance (type : Expr) (maxResultSize? : Option Nat := none) :
MetaM (LOption Expr)

Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if instance cannot be synthesized right now because `type` contains metavariables.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.throwFailedToSynthesize (type : Expr) :
MetaM Expr
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.synthInstance (type : Expr) (maxResultSize? : Option Nat := none) :
MetaM Expr
Equations

- One or more equations did not get rendered due to their size.

Instances For