- keys : Array Lean.Meta.DiscrTree.Key
- val : Lean.Name
Equations
- Lean.Meta.instInhabitedUnificationHintEntry = { default := { keys := default, val := default } }
Equations
- Lean.Meta.instInhabitedUnificationHints = { default := { discrTree := default } }
Equations
- Lean.Meta.instToFormatUnificationHints = { format := fun h => Lean.format h.discrTree }
def
Lean.Meta.UnificationHints.add
(hints : Lean.Meta.UnificationHints)
(e : Lean.Meta.UnificationHintEntry)
:
Equations
- Lean.Meta.UnificationHints.add hints e = { discrTree := Lean.Meta.DiscrTree.insertCore hints.discrTree e.keys e.val }
- pattern : Lean.Meta.UnificationConstraint
- constraints : List Lean.Meta.UnificationConstraint
Equations
- Lean.Meta.addUnificationHint declName kind = Lean.Meta.withNewMCtxDepth do let info ← Lean.getConstInfo declName match Lean.ConstantInfo.value? info with | none => Lean.throwError (Lean.toMessageData "invalid unification hint, it must be a definition") | some val => do let discr ← Lean.Meta.lambdaMetaTelescope val none let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (x, x_1, body) => match Lean.Meta.decodeUnificationHint body with | Except.error msg => Lean.throwError msg | Except.ok hint => do let keys ← Lean.Meta.DiscrTree.mkPath hint.pattern.lhs Lean.Meta.validateHint declName hint Lean.ScopedEnvExtension.add Lean.Meta.unificationHintExtension { keys := keys, val := declName } kind let cls : Lean.Name := `Meta.debug let a ← Lean.isTracingEnabledFor cls if a = true then do let a ← Lean.getEnv Lean.addTrace cls (Lean.toMessageData "addUnificationHint: " ++ Lean.toMessageData (Lean.ScopedEnvExtension.getState Lean.Meta.unificationHintExtension a) ++ Lean.toMessageData "") else pure PUnit.unit
Equations
- Lean.Meta.tryUnificationHints t s = (fun isDefEqPattern tryCandidate => let cls := `Meta.isDefEq.hint; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Bool := fun y => do let a ← read let _do_jp : PUnit → Lean.MetaM Bool := fun y => let _do_jp := fun y => do let a ← Lean.getEnv let hints : Lean.Meta.UnificationHints := Lean.ScopedEnvExtension.getState Lean.Meta.unificationHintExtension a let candidates ← Lean.Meta.DiscrTree.getMatch hints.discrTree t let r ← forIn candidates { fst := none, snd := PUnit.unit } fun candidate r => let r := r.snd; do let a ← tryCandidate candidate if a = true then pure (ForInStep.done { fst := some true, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM Bool := fun y => pure false match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a; if Lean.Expr.isMVar t = true then pure false else do let y ← pure PUnit.unit _do_jp y if a.config.unificationHints = true then do let y ← pure PUnit.unit _do_jp y else pure false if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData t ++ Lean.toMessageData " =?= " ++ Lean.toMessageData s ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y) Lean.Meta.tryUnificationHints.isDefEqPattern (Lean.Meta.tryUnificationHints.tryCandidate t s)
Equations
def
Lean.Meta.tryUnificationHints.tryCandidate
(t : Lean.Expr)
(s : Lean.Expr)
(candidate : Lean.Name)
:
Equations
- Lean.Meta.tryUnificationHints.tryCandidate t s candidate = Lean.traceCtx `Meta.isDefEq.hint (Lean.Meta.checkpointDefEq (let cls := `Meta.isDefEq.hint; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Bool := fun y => do let cinfo ← Lean.getConstInfo candidate let us ← List.mapM (fun x => Lean.Meta.mkFreshLevelMVar) (Lean.ConstantInfo.levelParams cinfo) let val : Lean.Expr := Lean.ConstantInfo.instantiateValueLevelParams cinfo us let discr ← Lean.Meta.lambdaMetaTelescope val none let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (xs, bis, body) => do let hint? ← Lean.Meta.withConfig (fun cfg => { foApprox := cfg.foApprox, ctxApprox := cfg.ctxApprox, quasiPatternApprox := cfg.quasiPatternApprox, constApprox := cfg.constApprox, isDefEqStuckEx := cfg.isDefEqStuckEx, transparency := cfg.transparency, zetaNonDep := cfg.zetaNonDep, trackZeta := cfg.trackZeta, unificationHints := false, proofIrrelevance := cfg.proofIrrelevance, assignSyntheticOpaque := cfg.assignSyntheticOpaque, ignoreLevelMVarDepth := cfg.ignoreLevelMVarDepth, offsetCnstrs := cfg.offsetCnstrs, etaStruct := cfg.etaStruct }) (match Lean.Meta.decodeUnificationHint body with | Except.error x => pure none | Except.ok hint => do let a ← Lean.Meta.tryUnificationHints.isDefEqPattern hint.pattern.lhs t <&&> Lean.Meta.tryUnificationHints.isDefEqPattern hint.pattern.rhs s if a = true then pure (some hint) else pure none) match hint? with | none => pure false | some hint => let cls := `Meta.isDefEq.hint; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Bool := fun y => do let r ← let col := hint.constraints; forIn col { fst := none, snd := PUnit.unit } fun c r => let r := r.snd; do let a ← Lean.Meta.isExprDefEqAux c.lhs c.rhs if a = true then do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) else pure (ForInStep.done { fst := some false, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM Bool := fun y => let s := toStream bis; do let r ← forIn xs { fst := none, snd := s } fun x r => let r := r.snd; let s := r; match Stream.next? s with | none => pure (ForInStep.done { fst := none, snd := s }) | some (bi, s') => let s := s'; if (bi == Lean.BinderInfo.instImplicit) = true then do let a ← Lean.Meta.inferType x let a ← Lean.Meta.trySynthInstance a none match a with | Lean.LOption.some val => do let a ← Lean.Meta.isDefEq x val if a = true then do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := s }) else pure (ForInStep.done { fst := some false, snd := s }) | x => pure (ForInStep.done { fst := some false, snd := s }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := s }) let x : Subarray Lean.BinderInfo := r.snd let s : Subarray Lean.BinderInfo := x let _do_jp : PUnit → Lean.MetaM Bool := fun y => pure true match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData candidate ++ Lean.toMessageData " succeeded, applying constraints") _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 "trying hint " ++ Lean.toMessageData candidate ++ Lean.toMessageData " at " ++ Lean.toMessageData t ++ Lean.toMessageData " =?= " ++ Lean.toMessageData s ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y) true)