Equations
- Lean.Elab.Eqns.instInhabitedEqnInfoCore = { default := { declName := default, levelParams := default, type := default, value := default } }
Equations
- Lean.Elab.Eqns.expandRHS? mvarId = do let target ← Lean.Meta.getMVarType' mvarId let discr ← pure (Lean.Expr.eq? target) match discr with | some (x, lhs, rhs) => let _do_jp := fun y => do let a ← Lean.Meta.mkEq lhs (Lean.Elab.Eqns.expand rhs) let a ← Lean.Meta.replaceTargetDefEq mvarId a pure (some a); if (Lean.Expr.isLet rhs || Lean.Expr.isMData rhs) = true then do let y ← pure PUnit.unit _do_jp y else pure none | x => pure none
Equations
- Lean.Elab.Eqns.funext? mvarId = do let target ← Lean.Meta.getMVarType' mvarId let discr ← pure (Lean.Expr.eq? target) match discr with | some (x, lhs, rhs) => let _do_jp := fun y => Lean.commitWhenSome? do let a ← Lean.Meta.mkConstWithFreshMVarLevels `funext let discr ← Lean.Meta.apply mvarId a match discr with | [mvarId] => do let discr ← Lean.Meta.intro1 mvarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => pure (some mvarId) | x => pure none; if Lean.Expr.isLambda rhs = true then do let y ← pure PUnit.unit _do_jp y else pure none | x => pure none
Equations
- Lean.Elab.Eqns.simpMatch? mvarId = do let mvarId' ← Lean.Meta.Split.simpMatchTarget mvarId if (mvarId != mvarId') = true then pure (some mvarId') else pure none
Equations
- Lean.Elab.Eqns.simpIf? mvarId = do let mvarId' ← Lean.Meta.simpIfTarget mvarId true if (mvarId != mvarId') = true then pure (some mvarId') else pure none
Equations
- Lean.Elab.Eqns.simpEqnType eqnType = (fun collect => do let a ← Lean.Meta.instantiateMVars eqnType Lean.Meta.forallTelescopeReducing a fun ys type => let proofVars := collect type; let cls := `Meta.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => do let type ← Lean.Meta.Match.unfoldNamedPattern type let eliminated : Lean.FVarIdSet := ∅ let r ← let col := Array.reverse ys; forIn col { fst := eliminated, snd := type } fun y r => let eliminated := r.fst; let type := r.snd; let cls := `Meta.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Lean.FVarIdSet → Lean.Expr → Unit → Lean.MetaM (ForInStep (MProd Lean.FVarIdSet Lean.Expr)) := fun eliminated type y_1 => if Std.RBTree.contains proofVars (Lean.Expr.fvarId! y) = true then do let a ← Lean.Meta.inferType y let discr ← Lean.Meta.matchEq? a match discr with | some (x, Lean.Expr.fvar fvarId x_1, rhs) => let eliminated := Std.RBTree.insert eliminated fvarId; let type := Lean.Expr.replaceFVarId type fvarId rhs; do pure PUnit.unit pure (ForInStep.yield { fst := eliminated, snd := type }) | x => do Lean.throwError (Lean.toMessageData "unexpected hypothesis in altenative" ++ Lean.toMessageData (Lean.indentExpr eqnType) ++ Lean.toMessageData "") pure (ForInStep.yield { fst := eliminated, snd := type }) else if Std.RBTree.contains eliminated (Lean.Expr.fvarId! y) = true then do let a ← Lean.Meta.dependsOn type (Lean.Expr.fvarId! y) if a = true then do let r ← Lean.Meta.mkForallFVars #[y] type false true let type : Lean.Expr := r pure PUnit.unit pure (ForInStep.yield { fst := eliminated, snd := type }) else do pure PUnit.unit pure (ForInStep.yield { fst := eliminated, snd := type }) else do let a ← Lean.Meta.inferType y let a ← Lean.Meta.matchEq? a let _do_jp : Lean.Expr → PUnit → Lean.MetaM (ForInStep (MProd Lean.FVarIdSet Lean.Expr)) := fun type y_2 => do let r ← Lean.Meta.mkForallFVars #[y] type false true let type : Lean.Expr := r pure PUnit.unit pure (ForInStep.yield { fst := eliminated, snd := type }) match a with | some (x, lhs, rhs) => do let a ← Lean.Meta.isDefEq lhs rhs if a = true then do let a ← Lean.Meta.dependsOn type (Lean.Expr.fvarId! y) if (!a) = true then pure (ForInStep.yield { fst := eliminated, snd := type }) else do let a ← Lean.Elab.Eqns.lhsDependsOn type (Lean.Expr.fvarId! y) if (!a) = true then do let a ← Lean.Meta.mkEqRefl lhs let type : Lean.Expr := Lean.Expr.replaceFVar type y a pure (ForInStep.yield { fst := eliminated, snd := type }) else do let y ← pure PUnit.unit _do_jp type y else do let y ← pure PUnit.unit _do_jp type y | x => do let y ← pure PUnit.unit _do_jp type y if a = true then do let a ← Lean.Meta.inferType y let y ← Lean.addTrace cls (Lean.toMessageData ">> simpEqnType: " ++ Lean.toMessageData a ++ Lean.toMessageData ", " ++ Lean.toMessageData type ++ Lean.toMessageData "") _do_jp eliminated type y else do let y ← pure PUnit.unit _do_jp eliminated type y let x : MProd Lean.FVarIdSet Lean.Expr := r match x with | { fst := eliminated, snd := type } => pure type if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "simpEqnType: " ++ Lean.toMessageData type ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y) Lean.Elab.Eqns.simpEqnType.collect
Equations
- Lean.Elab.Eqns.simpEqnType.collect e = let go := fun e ω => do let ref ← ST.mkRef ∅ Lean.Expr.forEach e fun e => if (Lean.Expr.isAppOfArity e `namedPattern 4 && Lean.Expr.isFVar (Lean.Expr.appArg! e)) = true then ST.Prim.Ref.modify ref fun a => Std.RBTree.insert a (Lean.Expr.fvarId! (Lean.Expr.appArg! e)) else pure PUnit.unit ST.Prim.Ref.get ref; runST (go e)
Equations
- Lean.Elab.Eqns.mkEqnTypes declNames mvarId = (fun go => do let discr ← StateRefT'.run (ReaderT.run (go mvarId) { declNames := declNames }) #[] let x : Unit × Array Lean.Expr := discr match x with | (x, eqnTypes) => pure eqnTypes) Lean.Elab.Eqns.mkEqnTypes.go
Equations
- Lean.Elab.Eqns.instInhabitedEqnsExtState = { default := { map := default } }
Equations
- Lean.Elab.Eqns.mkBaseNameFor env declName = Lean.mkBaseNameFor env declName `_eq_1 `_eqns
Equations
- Lean.Elab.Eqns.tryURefl mvarId = Lean.withOptions (fun a => Lean.Option.set a Lean.Meta.smartUnfolding false) do let r ← tryCatch (do Lean.Meta.applyRefl mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "refl failed") pure true) fun x => pure false pure r
Equations
- Lean.Elab.Eqns.deltaLHS mvarId = Lean.Meta.withMVarContext mvarId do let target ← Lean.Meta.getMVarType' mvarId let discr ← pure (Lean.Expr.eq? target) match discr with | some (x, lhs, rhs) => do let discr ← liftM (Lean.Meta.delta? lhs fun x => true) match discr with | some lhs => do let a ← Lean.Meta.mkEq lhs rhs Lean.Meta.replaceTargetDefEq mvarId a | x => Lean.Meta.throwTacticEx `deltaLHS mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "failed to delta reduce lhs") Lean.Syntax.missing | x => Lean.Meta.throwTacticEx `deltaLHS mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "equality expected") Lean.Syntax.missing
Equations
- Lean.Elab.Eqns.deltaRHS? mvarId declName = Lean.Meta.withMVarContext mvarId do let target ← Lean.Meta.getMVarType' mvarId let discr ← pure (Lean.Expr.eq? target) match discr with | some (x, lhs, rhs) => do let discr ← liftM (Lean.Meta.delta? (Lean.Expr.consumeMData rhs) fun a => a == declName) match discr with | some rhs => do let a ← Lean.Meta.mkEq lhs rhs Lean.Internal.coeM (Lean.Meta.replaceTargetDefEq mvarId a) | x => pure none | x => Lean.Meta.throwTacticEx `deltaRHS mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "equality expected") Lean.Syntax.missing
Equations
- Lean.Elab.Eqns.whnfReducibleLHS? mvarId = Lean.Meta.withMVarContext mvarId do let target ← Lean.Meta.getMVarType' mvarId let discr ← pure (Lean.Expr.eq? target) match discr with | some (x, lhs, rhs) => do let lhs' ← Lean.Elab.Eqns.whnfAux lhs if (lhs' != lhs) = true then do let a ← Lean.Meta.mkEq lhs' rhs let a ← Lean.Meta.replaceTargetDefEq mvarId a pure (some a) else pure none | x => Lean.Meta.throwTacticEx `whnfReducibleLHS mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "equality expected") Lean.Syntax.missing
Equations
- Lean.Elab.Eqns.instInhabitedUnfoldEqnExtState = { default := { map := default } }
Equations
- Lean.Elab.Eqns.mkUnfoldProof declName mvarId = do let discr ← Lean.Meta.getEqnsFor? declName match discr with | some eqs => let tryEqns := fun mvarId => Array.anyM (fun eq => Lean.commitWhen do let r ← tryCatch (do let a ← Lean.Meta.mkConstWithFreshMVarLevels eq let subgoals ← Lean.Meta.apply mvarId a let y ← List.allM Lean.Meta.assumptionCore subgoals pure (DoResultPR.pure y PUnit.unit)) fun x => pure (DoResultPR.return false PUnit.unit) match r with | DoResultPR.pure a u => let x := u; pure a | DoResultPR.return b u => let x := u; pure b) eqs 0 (Array.size eqs); (fun go => go mvarId) (Lean.Elab.Eqns.mkUnfoldProof.go declName tryEqns) | x => Lean.throwError (Lean.toMessageData "failed to generate equations for '" ++ Lean.toMessageData declName ++ Lean.toMessageData "'")
partial def
Lean.Elab.Eqns.mkUnfoldProof.go
(declName : Lean.Name)
(tryEqns : Lean.MVarId → Lean.MetaM Bool)
(mvarId : Lean.MVarId)
:
Equations
- Lean.Elab.Eqns.mkUnfoldEq declName info = Lean.Meta.withLCtx { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } ∅ do let env ← Lean.getEnv Lean.withOptions (fun a => Lean.Option.set a Lean.Meta.tactic.hygienic false) (let baseName := Lean.mkBaseNameFor env declName `_unfold `_unfold; Lean.Meta.lambdaTelescope info.value fun xs body => let us := List.map Lean.mkLevelParam info.levelParams; do let type ← Lean.Meta.mkEq (Lean.mkAppN (Lean.mkConst declName us) xs) body let goal ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar type Lean.Name.anonymous Lean.Elab.Eqns.mkUnfoldProof declName (Lean.Expr.mvarId! goal) let type ← Lean.Meta.mkForallFVars xs type false true let a ← Lean.Meta.instantiateMVars goal let value ← Lean.Meta.mkLambdaFVars xs a false true let name : Lean.Name := baseName ++ `_unfold Lean.addDecl (Lean.Declaration.thmDecl { toConstantVal := { name := name, levelParams := info.levelParams, type := type }, value := value }) pure name)
def
Lean.Elab.Eqns.getUnfoldFor?
(declName : Lean.Name)
(getInfo? : Unit → Option Lean.Elab.Eqns.EqnInfoCore)
:
Equations
- Lean.Elab.Eqns.getUnfoldFor? declName getInfo? = do let env ← Lean.getEnv match Std.PersistentHashMap.find? (Lean.EnvExtension.getState Lean.Elab.Eqns.unfoldEqnExt env).map declName with | some eq => pure (some eq) | x => match getInfo? () with | some info => do let eq ← Lean.Elab.Eqns.mkUnfoldEq declName info Lean.modifyEnv fun env => Lean.EnvExtension.modifyState Lean.Elab.Eqns.unfoldEqnExt env fun s => { map := Std.PersistentHashMap.insert s.map declName eq } pure (some eq) | x => pure none