Lean.Meta.SynthInstance

Equations

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

source

constant 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 x = match x with | Lean.Meta.SynthInstance.Waiter.consumerNode x => 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)

Equations

Lean.Meta.SynthInstance.getInstances type = do let localInstances ← Lean.Meta.getLocalInstances Lean.Meta.forallTelescopeReducing type fun x type => do let className? ← Lean.Meta.isClass? type match className? with | none => Lean.throwError (Lean.toMessageData "type class instance expected" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") | some className => do let globalInstances ← liftM Lean.Meta.getGlobalInstancesIndex let result ← Lean.Meta.DiscrTree.getUnify globalInstances type let result : Array Lean.Meta.InstanceEntry := Array.insertionSort result fun e₁ e₂ => decide (e₁.priority < e₂.priority) let erasedInstances ← liftM Lean.Meta.getErasedInstances let result ← Array.filterMapM (fun e => match e.val with | Lean.Expr.const constName us x => if Std.PersistentHashSet.contains erasedInstances constName = true then pure none else do let a ← List.mapM (fun x => Lean.Meta.mkFreshLevelMVar) us pure (some (Lean.Expr.updateConst! e.val a)) | x => panicWithPosWithDecl "Lean.Meta.SynthInstance" "Lean.Meta.SynthInstance.getInstances" 204 15 "global instance is not a constant") result 0 (Array.size result) let cls : Lean.Name := `Meta.synthInstance.globalInstances let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Array Lean.Expr) := fun y => let result := Array.foldl (fun result linst => if (linst.className == className) = true then Array.push result linst.fvar else result) result localInstances 0 (Array.size localInstances); pure result if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData type ++ Lean.toMessageData ", " ++ Lean.toMessageData result ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

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

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

Equations

Lean.Meta.SynthInstance.mkGeneratorNode? key mvar = do let mvarType ← Lean.Meta.inferType mvar let mvarType ← Lean.Meta.instantiateMVars mvarType let instances ← Lean.Meta.SynthInstance.getInstances mvarType if Array.isEmpty instances = true then pure none else do let mctx ← Lean.getMCtx pure (some { mvar := mvar, key := key, mctx := mctx, instances := instances, currInstanceIdx := Array.size instances })

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

Equations

Lean.Meta.SynthInstance.newSubgoal mctx key mvar waiter = Lean.Meta.withMCtx mctx (let cls := `Meta.synthInstance.newSubgoal; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SynthInstance.SynthM Unit := fun y => do let a ← liftM (Lean.Meta.SynthInstance.mkGeneratorNode? key mvar) match a with | none => pure () | some node => let entry := { waiters := #[waiter], answers := #[] }; modify fun s => { result? := s.result?, generatorStack := Array.push s.generatorStack node, resumeStack := s.resumeStack, tableEntries := Std.HashMap.insert s.tableEntries key entry } if a = true then do let y ← Lean.addTrace cls (Lean.MessageData.ofExpr key) _do_jp y else do let y ← pure PUnit.unit _do_jp y)

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

Lean.Meta.SynthInstance.getEntry key = do let a ← Lean.Meta.SynthInstance.findEntry? key match a with | none => panicWithPosWithDecl "Lean.Meta.SynthInstance" "Lean.Meta.SynthInstance.getEntry" 245 18 "invalid key at synthInstance" | some entry => pure entry

source

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

Lean.Meta.SynthInstance.SynthM Lean.Expr

Equations

Lean.Meta.SynthInstance.mkTableKeyFor mctx mvar = Lean.Meta.withMCtx mctx do let mvarType ← liftM (Lean.Meta.inferType mvar) let mvarType ← liftM (Lean.Meta.instantiateMVars mvarType) pure (Lean.Meta.SynthInstance.mkTableKey mctx mvarType)

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

Equations

Lean.Meta.SynthInstance.getSubgoals lctx localInsts xs inst = do let instType ← Lean.Meta.inferType inst let result ← Lean.Meta.SynthInstance.getSubgoalsAux lctx localInsts xs #[] 0 [] inst instType match Lean.Expr.getAppFn inst with | Lean.Expr.const constName x x_1 => do let env ← Lean.getEnv if Lean.Meta.SynthInstance.hasInferTCGoalsRLAttribute env constName = true then pure result else pure { subgoals := List.reverse result.subgoals, instVal := result.instVal, instTypeBody := result.instTypeBody } | x => pure result

source

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

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

Equations

Lean.Meta.SynthInstance.tryResolveCore mvar inst = do let mvar ← Lean.Meta.instantiateMVars mvar let a ← Lean.Meta.hasAssignableMVar mvar let _do_jp : PUnit → Lean.MetaM (Option (Lean.MetavarContext × List Lean.Expr)) := fun y => do let mvarType ← Lean.Meta.inferType mvar let lctx ← Lean.getLCtx let localInsts ← Lean.Meta.getLocalInstances Lean.Meta.forallTelescopeReducing mvarType fun xs mvarTypeBody => do let discr ← Lean.Meta.SynthInstance.getSubgoals lctx localInsts xs inst let x : Lean.Meta.SynthInstance.SubgoalsResult := discr match x with | { subgoals := subgoals, instVal := instVal, instTypeBody := instTypeBody } => let cls := `Meta.synthInstance.tryResolve; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option (Lean.MetavarContext × List Lean.Expr)) := fun y => do let a ← Lean.Meta.isDefEq mvarTypeBody instTypeBody if a = true then do let instVal ← Lean.Meta.mkLambdaFVars xs instVal false true let a ← Lean.Meta.isDefEq mvar instVal if a = true then let cls := `Meta.synthInstance.tryResolve; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option (Lean.MetavarContext × List Lean.Expr)) := fun y => do let a ← Lean.getMCtx pure (some (a, subgoals)) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "success") _do_jp y else do let y ← pure PUnit.unit _do_jp y else let cls := `Meta.synthInstance.tryResolve; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option (Lean.MetavarContext × List Lean.Expr)) := fun y => pure none if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "failure assigning") _do_jp y else do let y ← pure PUnit.unit _do_jp y else let cls := `Meta.synthInstance.tryResolve; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option (Lean.MetavarContext × List Lean.Expr)) := fun y => pure none if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "failure") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData mvarTypeBody ++ Lean.toMessageData " =?= " ++ Lean.toMessageData instTypeBody ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if (!a) = true then do let a ← Lean.getMCtx pure (some (a, [])) else do let y ← pure PUnit.unit _do_jp y

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

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)

Equations

Lean.Meta.SynthInstance.tryAnswer mctx mvar answer = Lean.Meta.withMCtx mctx do let discr ← liftM (Lean.Meta.openAbstractMVarsResult answer.result) let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (x, x_1, val) => do let a ← liftM (Lean.Meta.isDefEq mvar val) if a = true then do let a ← Lean.getMCtx pure (some a) else pure none

source

def Lean.Meta.SynthInstance.wakeUp (answer : Lean.Meta.SynthInstance.Answer) :

Lean.Meta.SynthInstance.Waiter → Lean.Meta.SynthInstance.SynthM Unit

Equations

Lean.Meta.SynthInstance.wakeUp answer x = match x with | Lean.Meta.SynthInstance.Waiter.root => if (answer.result.numMVars == 0) = true then modify fun s => { result? := some answer.result, generatorStack := s.generatorStack, resumeStack := s.resumeStack, tableEntries := s.tableEntries } else do let discr ← liftM (Lean.Meta.openAbstractMVarsResult answer.result) let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (x, x_1, answerExpr) => let cls := `Meta.synthInstance; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SynthInstance.SynthM Unit := fun y => pure () if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "skip answer containing metavariables " ++ Lean.toMessageData answerExpr ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y | Lean.Meta.SynthInstance.Waiter.consumerNode cNode => modify fun s => { result? := s.result?, generatorStack := s.generatorStack, resumeStack := Array.push s.resumeStack (cNode, answer), tableEntries := s.tableEntries }

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

Equations

Lean.Meta.SynthInstance.addAnswer cNode = do let a ← read if cNode.size ≥ a.maxResultSize then do Lean.traceM `Meta.synthInstance.discarded (Lean.Meta.withMCtx cNode.mctx do let a ← read let a_1 ← liftM (Lean.Meta.inferType cNode.mvar) pure (Lean.toMessageData "size: " ++ Lean.toMessageData cNode.size ++ Lean.toMessageData " ≥ " ++ Lean.toMessageData a.maxResultSize ++ Lean.toMessageData ", " ++ Lean.toMessageData a_1 ++ Lean.toMessageData "")) pure () else do let answer ← liftM (Lean.Meta.SynthInstance.mkAnswer cNode) let key : Lean.Expr := cNode.key let entry ← Lean.Meta.SynthInstance.getEntry key if Lean.Meta.SynthInstance.isNewAnswer entry.answers answer = true then let newEntry := { waiters := entry.waiters, answers := Array.push entry.answers answer }; do modify fun s => { result? := s.result?, generatorStack := s.generatorStack, resumeStack := s.resumeStack, tableEntries := Std.HashMap.insert s.tableEntries key newEntry } Array.forM (Lean.Meta.SynthInstance.wakeUp answer) entry.waiters 0 (Array.size entry.waiters) else pure PUnit.unit

source

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

Lean.Meta.SynthInstance.SynthM Unit

Equations

Lean.Meta.SynthInstance.consume cNode = match cNode.subgoals with | [] => Lean.Meta.SynthInstance.addAnswer cNode | mvar :: x => let waiter := Lean.Meta.SynthInstance.Waiter.consumerNode cNode; do let key ← Lean.Meta.SynthInstance.mkTableKeyFor cNode.mctx mvar let entry? ← Lean.Meta.SynthInstance.findEntry? key match entry? with | none => do let a ← liftM (Lean.Meta.SynthInstance.removeUnusedArguments? cNode.mctx mvar) match a with | none => Lean.Meta.SynthInstance.newSubgoal cNode.mctx key mvar waiter | some (mvarType', transformer) => do let key' ← pure (Lean.Meta.SynthInstance.mkTableKey cNode.mctx mvarType') let a ← Lean.Meta.SynthInstance.findEntry? key' match a with | none => do let discr ← Lean.Meta.withMCtx cNode.mctx do let mvar' ← liftM (Lean.Meta.mkFreshExprMVar (some mvarType') Lean.MetavarKind.natural Lean.Name.anonymous) let a ← Lean.getMCtx pure (a, mvar') let x : Lean.MetavarContext × Lean.Expr := discr match x with | (mctx', mvar') => Lean.Meta.SynthInstance.newSubgoal mctx' key' mvar' (Lean.Meta.SynthInstance.Waiter.consumerNode { mvar := cNode.mvar, key := cNode.key, mctx := mctx', subgoals := mvar' :: cNode.subgoals, size := cNode.size }) | some entry' => do let answers' ← Array.mapM (fun a => Lean.Meta.withMCtx cNode.mctx do let a_1 ← liftM (Lean.Meta.instantiateMVars a.result.expr) let trAnswr : Lean.Expr := Lean.Expr.betaRev transformer #[a_1] let trAnswrType ← liftM (Lean.Meta.inferType trAnswr) pure { result := let src := a.result; { paramNames := src.paramNames, numMVars := src.numMVars, expr := trAnswr }, resultType := trAnswrType, size := a.size }) entry'.answers modify fun s => { result? := s.result?, generatorStack := s.generatorStack, resumeStack := Array.foldl (fun s answer => Array.push s (cNode, answer)) s.resumeStack answers' 0 (Array.size answers'), tableEntries := Std.HashMap.insert s.tableEntries key' { waiters := Array.push entry'.waiters waiter, answers := entry'.answers } } | some entry => modify fun s => { result? := s.result?, generatorStack := s.generatorStack, resumeStack := Array.foldl (fun s answer => Array.push s (cNode, answer)) s.resumeStack entry.answers 0 (Array.size entry.answers), tableEntries := Std.HashMap.insert s.tableEntries key { waiters := Array.push entry.waiters waiter, answers := entry.answers } }

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

Lean.Meta.SynthInstance.modifyTop f = modify fun s => { result? := s.result?, generatorStack := Array.modify s.generatorStack (Array.size s.generatorStack - 1) f, resumeStack := s.resumeStack, tableEntries := s.tableEntries }

source

def Lean.Meta.SynthInstance.generate :

Lean.Meta.SynthInstance.SynthM Unit

Equations

Lean.Meta.SynthInstance.generate = do let gNode ← Lean.Meta.SynthInstance.getTop if (gNode.currInstanceIdx == 0) = true then modify fun s => { result? := s.result?, generatorStack := Array.pop s.generatorStack, resumeStack := s.resumeStack, tableEntries := s.tableEntries } else let key := gNode.key; let idx := gNode.currInstanceIdx - 1; let inst := Array.get! gNode.instances idx; let mctx := gNode.mctx; let mvar := gNode.mvar; let cls := `Meta.synthInstance.generate; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SynthInstance.SynthM Unit := fun y => do Lean.Meta.SynthInstance.modifyTop fun gNode => { mvar := gNode.mvar, key := gNode.key, mctx := gNode.mctx, instances := gNode.instances, currInstanceIdx := idx } let a ← Lean.Meta.SynthInstance.tryResolve mctx mvar inst match a with | none => pure () | some (mctx, subgoals) => Lean.Meta.SynthInstance.consume { mvar := mvar, key := key, mctx := mctx, subgoals := subgoals, size := 0 } if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "instance " ++ Lean.toMessageData inst ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Meta.SynthInstance.getNextToResume :

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

Equations

Lean.Meta.SynthInstance.getNextToResume = do let s ← get let r : Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer := Array.back s.resumeStack modify fun s => { result? := s.result?, generatorStack := s.generatorStack, resumeStack := Array.pop s.resumeStack, tableEntries := s.tableEntries } pure r

source

def Lean.Meta.SynthInstance.resume :

Lean.Meta.SynthInstance.SynthM Unit

Equations

Lean.Meta.SynthInstance.resume = do let discr ← Lean.Meta.SynthInstance.getNextToResume let x : Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer := discr match x with | (cNode, answer) => match cNode.subgoals with | [] => panicWithPosWithDecl "Lean.Meta.SynthInstance" "Lean.Meta.SynthInstance.resume" 546 18 "resume found no remaining subgoals" | mvar :: rest => do let a ← Lean.Meta.SynthInstance.tryAnswer cNode.mctx mvar answer match a with | none => pure () | some mctx => do Lean.Meta.withMCtx mctx (Lean.traceM `Meta.synthInstance.resume do let goal ← liftM (Lean.Meta.inferType cNode.mvar) let subgoal ← liftM (Lean.Meta.inferType mvar) pure (Lean.toMessageData "size: " ++ Lean.toMessageData (cNode.size + answer.size) ++ Lean.toMessageData ", " ++ Lean.toMessageData goal ++ Lean.toMessageData " <== " ++ Lean.toMessageData subgoal ++ Lean.toMessageData "")) Lean.Meta.SynthInstance.consume { mvar := cNode.mvar, key := cNode.key, mctx := mctx, subgoals := rest, size := cNode.size + answer.size }

source

def Lean.Meta.SynthInstance.step :

Lean.Meta.SynthInstance.SynthM Bool

Equations

Lean.Meta.SynthInstance.step = do Lean.Meta.SynthInstance.checkMaxHeartbeats let s ← get if (!Array.isEmpty s.resumeStack) = true then do Lean.Meta.SynthInstance.resume pure true else if (!Array.isEmpty s.generatorStack) = true then do Lean.Meta.SynthInstance.generate pure true else pure false

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

Lean.Meta.SynthInstance.main type maxResultSize = Lean.withCurrHeartbeats (Lean.traceCtx `Meta.synthInstance (let cls := `Meta.synthInstance; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option Lean.Meta.AbstractMVarsResult) := fun y => do let mvar ← Lean.Meta.mkFreshExprMVar (some type) Lean.MetavarKind.natural Lean.Name.anonymous let mctx ← Lean.getMCtx let key : Lean.Expr := Lean.Meta.SynthInstance.mkTableKey mctx type let action : Lean.Meta.SynthInstance.SynthM (Option Lean.Meta.AbstractMVarsResult) := do Lean.Meta.SynthInstance.newSubgoal mctx key mvar Lean.Meta.SynthInstance.Waiter.root Lean.Meta.SynthInstance.synth let a ← Lean.getOptions StateRefT'.run' (ReaderT.run action { maxResultSize := maxResultSize, maxHeartbeats := Lean.Meta.SynthInstance.getMaxHeartbeats a }) { result? := none, generatorStack := #[], resumeStack := #[], tableEntries := ∅ } if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "main goal " ++ Lean.toMessageData type ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y))

source

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

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.synthInstance? type maxResultSize? = do let a ← Lean.getOptions Lean.profileitM Lean.Exception "typeclass inference" a do let opts ← Lean.getOptions let maxResultSize : Nat := Option.getD maxResultSize? (Lean.Option.get opts Lean.Meta.synthInstance.maxSize) let inputConfig ← Lean.Meta.getConfig Lean.Meta.withConfig (fun config => { foApprox := true, ctxApprox := true, quasiPatternApprox := config.quasiPatternApprox, constApprox := false, isDefEqStuckEx := true, transparency := Lean.Meta.TransparencyMode.instances, zetaNonDep := config.zetaNonDep, trackZeta := config.trackZeta, unificationHints := config.unificationHints, proofIrrelevance := config.proofIrrelevance, assignSyntheticOpaque := config.assignSyntheticOpaque, ignoreLevelMVarDepth := true, offsetCnstrs := config.offsetCnstrs, etaStruct := config.etaStruct }) do let type ← Lean.Meta.instantiateMVars type let type ← Lean.Meta.preprocess type let s ← get match Std.PersistentHashMap.find? s.cache.synthInstance type with | some result => pure result | none => do let result? ← Lean.Meta.withNewMCtxDepth do let normType ← Lean.Meta.preprocessOutParam type let cls : Lean.Name := `Meta.synthInstance let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option Lean.Meta.AbstractMVarsResult) := fun y => Lean.Meta.SynthInstance.main normType maxResultSize if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "preprocess: " ++ Lean.toMessageData type ++ Lean.toMessageData " ==> " ++ Lean.toMessageData normType ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y let resultHasUnivMVars : Bool := match result? with | some result => !Array.isEmpty result.paramNames | x => false let _do_jp : Option Lean.Expr → Lean.MetaM (Option Lean.Expr) := fun result? => if (Lean.Expr.hasMVar type || resultHasUnivMVars) = true then pure result? else do modify fun s => { mctx := s.mctx, cache := let src := s.cache; { inferType := src.inferType, funInfo := src.funInfo, synthInstance := Std.PersistentHashMap.insert s.cache.synthInstance type result?, whnfDefault := src.whnfDefault, whnfAll := src.whnfAll, defEqDefault := src.defEqDefault, defEqAll := src.defEqAll }, zetaFVarIds := s.zetaFVarIds, postponed := s.postponed } pure result? match result? with | none => do let y ← pure none _do_jp y | some result => do let discr ← Lean.Meta.openAbstractMVarsResult result let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (x, x_1, result) => let cls := `Meta.synthInstance; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option Lean.Expr) := fun y => do let resultType ← Lean.Meta.inferType result let a ← Lean.Meta.withConfig (fun x => inputConfig) (Lean.Meta.isDefEq type resultType) if a = true then do let result ← Lean.Meta.instantiateMVars result Lean.Meta.check result let y ← pure (some result) _do_jp y else let cls := `Meta.synthInstance; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option Lean.Expr) := fun y => do let y ← pure none _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "result type" ++ Lean.toMessageData (Lean.indentExpr resultType) ++ Lean.toMessageData "\nis not definitionally equal to" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "result " ++ Lean.toMessageData result ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

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

Lean.MetaM (Lean.LOption Lean.Expr)

Equations

Lean.Meta.trySynthInstance type maxResultSize? = Lean.catchInternalId Lean.Meta.isDefEqStuckExceptionId (toLOptionM (Lean.Meta.synthInstance? type maxResultSize?)) fun x => pure Lean.LOption.undef

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.synthInstance type maxResultSize? = Lean.catchInternalId Lean.Meta.isDefEqStuckExceptionId (do let result? ← Lean.Meta.synthInstance? type maxResultSize? match result? with | some result => pure result | none => Lean.throwError (Lean.toMessageData "failed to synthesize" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "")) fun x => Lean.throwError (Lean.toMessageData "failed to synthesize" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "")