Lean.Meta.SynthInstance

Equations

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

source

opaque Lean.Meta.SynthInstance.inferTCGoalsRLAttr:

Lean.TagAttribute

source

def Lean.Meta.SynthInstance.hasInferTCGoalsRLAttribute (env : Lean.Environment) (constName : Lean.Name) :

Bool

Equations

Lean.Meta.SynthInstance.hasInferTCGoalsRLAttribute env constName = Lean.TagAttribute.hasTag Lean.Meta.SynthInstance.inferTCGoalsRLAttr env constName

source

structure Lean.Meta.SynthInstance.GeneratorNode:

Type

mvar : Lean.Expr
key : Lean.Expr
mctx : Lean.MetavarContext
instances : Array Lean.Expr
currInstanceIdx : Nat

source

instance Lean.Meta.SynthInstance.instInhabitedGeneratorNode:

Inhabited Lean.Meta.SynthInstance.GeneratorNode

Equations

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

source

structure Lean.Meta.SynthInstance.ConsumerNode:

Type

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

source

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 } }

source

inductive Lean.Meta.SynthInstance.Waiter:

Type

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

source

def Lean.Meta.SynthInstance.Waiter.isRoot:

Lean.Meta.SynthInstance.Waiter → Bool

Equations

Lean.Meta.SynthInstance.Waiter.isRoot _fun_discr = match _fun_discr with | Lean.Meta.SynthInstance.Waiter.consumerNode a => false | Lean.Meta.SynthInstance.Waiter.root => true

source

structure Lean.Meta.SynthInstance.MkTableKey.State:

Type

nextIdx : Nat
lmap : Std.HashMap Lean.MVarId Lean.Level
emap : Std.HashMap Lean.MVarId Lean.Expr

source

@[inline]

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

Type

Equations

Lean.Meta.SynthInstance.MkTableKey.M = ReaderT Lean.MetavarContext (StateM Lean.Meta.SynthInstance.MkTableKey.State)

source

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

Lean.Meta.SynthInstance.MkTableKey.M Lean.Level

source

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

Lean.Meta.SynthInstance.MkTableKey.M Lean.Expr

source

def Lean.Meta.SynthInstance.mkTableKey (mctx : Lean.MetavarContext) (e : Lean.Expr) :

Lean.Expr

Equations

Lean.Meta.SynthInstance.mkTableKey mctx e = StateT.run' (Lean.Meta.SynthInstance.MkTableKey.normExpr e mctx) { nextIdx := 0, lmap := ∅, emap := ∅ }

source

structure Lean.Meta.SynthInstance.Answer:

Type

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

source

instance Lean.Meta.SynthInstance.instInhabitedAnswer:

Inhabited Lean.Meta.SynthInstance.Answer

Equations

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

source

structure Lean.Meta.SynthInstance.TableEntry:

Type

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

source

structure Lean.Meta.SynthInstance.Context:

Type

maxResultSize : Nat
maxHeartbeats : Nat

source

structure Lean.Meta.SynthInstance.State:

Type

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

source

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

source

def Lean.Meta.SynthInstance.checkMaxHeartbeats:

Lean.Meta.SynthInstance.SynthM Unit

Equations

Lean.Meta.SynthInstance.checkMaxHeartbeats = do let a ← read liftM (Lean.Core.checkMaxHeartbeatsCore "typeclass" `synthInstance.maxHeartbeats a.maxHeartbeats)

source

@[inline]

def Lean.Meta.SynthInstance.mapMetaM (f : {α : Type} → Lean.MetaM α → Lean.MetaM α) {α : Type} :

Lean.Meta.SynthInstance.SynthM α → Lean.Meta.SynthInstance.SynthM α

Equations

Lean.Meta.SynthInstance.mapMetaM f = monadMap f

source

instance Lean.Meta.SynthInstance.instInhabitedSynthM {α : Type} :

Inhabited (Lean.Meta.SynthInstance.SynthM α)

Equations

Lean.Meta.SynthInstance.instInhabitedSynthM = { default := fun x x => default }

source

def Lean.Meta.SynthInstance.getInstances (type : Lean.Expr) :

Lean.MetaM (Array Lean.Expr)

Return globals and locals instances that may unify with type

Equations

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

source

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

Lean.MetaM (Option Lean.Meta.SynthInstance.GeneratorNode)

Equations

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

source

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

source

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

Lean.Meta.SynthInstance.SynthM (Option Lean.Meta.SynthInstance.TableEntry)

Equations

Lean.Meta.SynthInstance.findEntry? key = do let a ← get pure (Std.HashMap.find? a.tableEntries key)

source

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

Lean.Meta.SynthInstance.SynthM Lean.Meta.SynthInstance.TableEntry

Equations

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

source

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.

Equations

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

source

structure Lean.Meta.SynthInstance.SubgoalsResult:

Type

subgoals : List Lean.Expr
instVal : Lean.Expr
instTypeBody : Lean.Expr

source

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

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)

Equations

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

source

def Lean.Meta.SynthInstance.tryResolveCore (mvar : Lean.Expr) (inst : Lean.Expr) :

Lean.MetaM (Option (Lean.MetavarContext × List Lean.Expr))

Equations

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

source

def Lean.Meta.SynthInstance.tryResolve (mctx : Lean.MetavarContext) (mvar : Lean.Expr) (inst : Lean.Expr) :

Lean.Meta.SynthInstance.SynthM (Option (Lean.MetavarContext × List Lean.Expr))

Try to synthesize metavariable mvar using the instance inst. Remark: mctx contains mvar. 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

Lean.Meta.SynthInstance.tryResolve mctx mvar inst = Lean.traceCtx `Meta.synthInstance.tryResolve (Lean.Meta.withMCtx mctx (liftM (Lean.Meta.SynthInstance.tryResolveCore mvar inst)))

source

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.

source

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.

Equations

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

source

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

Bool

Equations

Lean.Meta.SynthInstance.isNewAnswer oldAnswers answer = Array.all oldAnswers (fun oldAnswer => oldAnswer.resultType != answer.resultType) 0 (Array.size oldAnswers)

source

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.

source

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.

source

def Lean.Meta.SynthInstance.getTop:

Lean.Meta.SynthInstance.SynthM Lean.Meta.SynthInstance.GeneratorNode

Equations

Lean.Meta.SynthInstance.getTop = do let a ← get pure (Array.back a.generatorStack)

source

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

source

def Lean.Meta.SynthInstance.generate:

Lean.Meta.SynthInstance.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.

source

def Lean.Meta.SynthInstance.getNextToResume:

Lean.Meta.SynthInstance.SynthM (Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer)

Equations

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

source

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.

Equations

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

source

def Lean.Meta.SynthInstance.step:

Lean.Meta.SynthInstance.SynthM Bool

Equations

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

source

def Lean.Meta.SynthInstance.getResult:

Lean.Meta.SynthInstance.SynthM (Option Lean.Meta.AbstractMVarsResult)

Equations

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

source

partial def Lean.Meta.SynthInstance.synth:

Lean.Meta.SynthInstance.SynthM (Option Lean.Meta.AbstractMVarsResult)

source

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

Lean.MetaM (Option Lean.Meta.AbstractMVarsResult)

Equations

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

source

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

Lean.MetaM (Option Lean.Expr)

Equations

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

source

def Lean.Meta.trySynthInstance (type : Lean.Expr) (maxResultSize? : optParam (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.

source

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

Lean.MetaM Lean.Expr

Equations

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