opaque Lean.Meta.synthInstance.maxHeartbeats : Lean.Option Nat

opaque Lean.Meta.synthInstance.maxSize : Lean.Option Nat

opaque Lean.Meta.backward.synthInstance.canonInstances : Lean.Option Bool

def Lean.Meta.SynthInstance.getMaxHeartbeats (opts : Lean.Options) : Nat

Equations

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

structure Lean.Meta.SynthInstance.Instance : Type

• val : Lean.Expr
• synthOrder : Array Nat

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

structure Lean.Meta.SynthInstance.GeneratorNode : Type

• mvar : Lean.Expr
• key : Lean.Expr
• mctx : Lean.MetavarContext
• instances : Array Lean.Meta.SynthInstance.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.

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

structure Lean.Meta.SynthInstance.ConsumerNode : Type

• mvar : Lean.Expr
• key : Lean.Expr
• mctx : Lean.MetavarContext
• subgoals : List Lean.Expr
• size : Nat

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

Equations

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

inductive Lean.Meta.SynthInstance.Waiter : Type

• consumerNode: Lean.Meta.SynthInstance.ConsumerNode → Lean.Meta.SynthInstance.Waiter
• root: Lean.Meta.SynthInstance.Waiter

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

Equations

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

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.

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

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

@[reducible, inline]

abbrev Lean.Meta.SynthInstance.MkTableKey.M (α : Type) : Type

Equations

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

@[always_inline]

instance Lean.Meta.SynthInstance.MkTableKey.instMonadMCtxM : Lean.MonadMCtx Lean.Meta.SynthInstance.MkTableKey.M

partial def Lean.Meta.SynthInstance.MkTableKey.normLevel (u : Lean.Level) : Lean.Meta.SynthInstance.MkTableKey.M Lean.Level

partial def Lean.Meta.SynthInstance.MkTableKey.normExpr (e : Lean.Expr) : Lean.Meta.SynthInstance.MkTableKey.M Lean.Expr

def Lean.Meta.SynthInstance.mkTableKey {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (e : Lean.Expr) : m Lean.Expr

Remark: mkTableKey assumes e does not contain assigned metavariables.

Equations

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

structure Lean.Meta.SynthInstance.Answer : Type

• result : Lean.Meta.AbstractMVarsResult
• resultType : Lean.Expr
• size : Nat

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

structure Lean.Meta.SynthInstance.TableEntry : Type

• waiters : Array Lean.Meta.SynthInstance.Waiter
• answers : Array Lean.Meta.SynthInstance.Answer

structure Lean.Meta.SynthInstance.Context : Type

• maxResultSize : Nat
• maxHeartbeats : Nat

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 MetavarContexts simultaneously. That being said, we still use extends because it makes it simpler to move from M to MetaM.

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

@[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)

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

Equations

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

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

Equations

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

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

Return globals and locals instances that may unify with type

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

Equations

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

def Lean.Meta.SynthInstance.newSubgoal (mctx : Lean.MetavarContext) (key mvar : Lean.Expr) (waiter : Lean.Meta.SynthInstance.Waiter) : Lean.Meta.SynthInstance.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.

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

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

def Lean.Meta.SynthInstance.mkTableKeyFor (mctx : Lean.MetavarContext) (mvar : Lean.Expr) : Lean.Meta.SynthInstance.SynthM Lean.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.

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 Lean.Expr
• instVal : Lean.Expr
• instTypeBody : Lean.Expr

def Lean.Meta.SynthInstance.getSubgoals (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances) (xs : Array Lean.Expr) (inst : Lean.Meta.SynthInstance.Instance) : Lean.MetaM Lean.Meta.SynthInstance.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)

def Lean.Meta.SynthInstance.tryResolve (mvar : Lean.Expr) (inst : Lean.Meta.SynthInstance.Instance) : Lean.MetaM (Option (Lean.MetavarContext × List Lean.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.

def Lean.Meta.SynthInstance.tryAnswer (mctx : Lean.MetavarContext) (mvar : Lean.Expr) (answer : Lean.Meta.SynthInstance.Answer) : Lean.Meta.SynthInstance.SynthM (Option Lean.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.

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

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

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

Equations

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

def Lean.Meta.SynthInstance.addAnswer (cNode : Lean.Meta.SynthInstance.ConsumerNode) : Lean.Meta.SynthInstance.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.

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

Process the next subgoal in the given consumer node.

Equations

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

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

Equations

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

@[inline]

def Lean.Meta.SynthInstance.modifyTop (f : Lean.Meta.SynthInstance.GeneratorNode → Lean.Meta.SynthInstance.GeneratorNode) : Lean.Meta.SynthInstance.SynthM Unit

Equations

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

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

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

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

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

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

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

Equations

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

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

partial def Lean.Meta.SynthInstance.synth : Lean.Meta.SynthInstance.SynthM (Option Lean.Meta.AbstractMVarsResult)

def Lean.Meta.SynthInstance.main (type : Lean.Expr) (maxResultSize : Nat) : Lean.MetaM (Option Lean.Meta.AbstractMVarsResult)

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.

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

Equations

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

def Lean.Meta.trySynthInstance (type : Lean.Expr) (maxResultSize? : Option Nat := none) : Lean.MetaM (Lean.LOption Lean.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.

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

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

Equations

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