Equations
- Lean.Elab.Tactic.elabSimpConfigCore optConfig = if Lean.Syntax.isNone optConfig = true then pure { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 2, contextual := false, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := true, iota := true, proj := true, decide := true } else Lean.withoutModifyingState (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 } } ∅ (Lean.Elab.Term.withSynthesize do let c ← Lean.Elab.Term.elabTermEnsuringType (Lean.Syntax.getOp (Lean.Syntax.getOp optConfig 0) 3) (some (Lean.mkConst `Lean.Meta.Simp.Config)) true true none let a ← liftM (Lean.Meta.instantiateMVars c) Lean.Elab.Tactic.eval✝ a))
Equations
- Lean.Elab.Tactic.elabSimpConfigCtxCore optConfig = if Lean.Syntax.isNone optConfig = true then pure { toConfig := { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 2, contextual := true, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := true, iota := true, proj := true, decide := true } } else Lean.withoutModifyingState (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 } } ∅ (Lean.Elab.Term.withSynthesize do let c ← Lean.Elab.Term.elabTermEnsuringType (Lean.Syntax.getOp (Lean.Syntax.getOp optConfig 0) 3) (some (Lean.mkConst `Lean.Meta.Simp.ConfigCtx)) true true none let a ← liftM (Lean.Meta.instantiateMVars c) Lean.Elab.Tactic.eval✝ a))
Equations
- Lean.Elab.Tactic.tacticToDischarge tacticCode = do let tacticCode ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticTry_ #[Lean.Syntax.atom info "try", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.paren #[Lean.Syntax.atom info "(", tacticCode, Lean.Syntax.atom info ")"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]) let a ← getThe Lean.Elab.Term.State let ref ← liftM (IO.mkRef a) let ctx ← readThe Lean.Elab.Term.Context let disch : Lean.Meta.Simp.Discharge := fun e => do let mvar ← liftM (Lean.Meta.mkFreshExprSyntheticOpaqueMVar e `simp.discharger) let s ← ST.Ref.get ref let runTac? : Lean.Elab.TermElabM (Option Lean.Expr) := do let r ← tryCatch (do let y ← Lean.Elab.withoutModifyingStateWithInfoAndMessages do Lean.Elab.Term.withSynthesize (Lean.Elab.Term.runTactic (Lean.Expr.mvarId! mvar) tacticCode) let result ← liftM (Lean.Meta.instantiateMVars mvar) if Lean.Expr.hasExprMVar result = true then pure none else pure (some result) pure (DoResultPR.pure y PUnit.unit)) fun x => pure (DoResultPR.return none PUnit.unit) match r with | DoResultPR.pure a u => let x := u; pure a | DoResultPR.return b u => let x := u; pure b let discr ← liftM (Lean.Elab.Term.TermElabM.run runTac? ctx s) let x : Option Lean.Expr × Lean.Elab.Term.State := discr match x with | (result?, s) => do ST.Ref.set ref s pure result? pure (ref, disch)
def
Lean.Elab.Tactic.Simp.DischargeWrapper.with
{α : Type}
(w : Lean.Elab.Tactic.Simp.DischargeWrapper)
(x : Option Lean.Meta.Simp.Discharge → Lean.Elab.Tactic.TacticM α)
:
Equations
- Lean.Elab.Tactic.Simp.DischargeWrapper.with w x = match w with | Lean.Elab.Tactic.Simp.DischargeWrapper.default => x none | Lean.Elab.Tactic.Simp.DischargeWrapper.custom ref d => do let a ← getThe Lean.Elab.Term.State ST.Ref.set ref a tryFinally (x (some d)) do let a ← ST.Ref.get ref set a
Equations
- Lean.Elab.Tactic.elabSimpConfig optConfig ctx = if ctx = true then do let a ← Lean.Elab.Tactic.elabSimpConfigCtxCore optConfig pure a.toConfig else Lean.Elab.Tactic.elabSimpConfigCore optConfig
- ctx : Lean.Meta.Simp.Context
- starArg : Bool
- ctx : Lean.Meta.Simp.Context
- dischargeWrapper : Lean.Elab.Tactic.Simp.DischargeWrapper
- fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId
def
Lean.Elab.Tactic.mkSimpContext
(stx : Lean.Syntax)
(eraseLocal : Bool)
(ctx : optParam Bool false)
(ignoreStarArg : optParam Bool false)
:
Equations
- Lean.Elab.Tactic.mkSimpContext stx eraseLocal ctx ignoreStarArg = let _do_jp := fun y => do let dischargeWrapper ← Lean.Elab.Tactic.mkDischargeWrapper (Lean.Syntax.getOp stx 2) let simpOnly : Bool := !Lean.Syntax.isNone (Lean.Syntax.getOp stx 3) let _do_jp : Lean.Meta.SimpLemmas → Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.MkSimpContextResult := fun simpLemmas => do let congrLemmas ← liftM Lean.Meta.getCongrLemmas let a ← liftM (Lean.Elab.Tactic.elabSimpConfig (Lean.Syntax.getOp stx 1) ctx) let r ← Lean.Elab.Tactic.elabSimpArgs (Lean.Syntax.getOp stx 4) { config := a, simpLemmas := simpLemmas, congrLemmas := congrLemmas, parent? := none, dischargeDepth := 0 } eraseLocal if (!r.starArg || ignoreStarArg) = true then pure { ctx := r.ctx, dischargeWrapper := dischargeWrapper, fvarIdToLemmaId := ∅ } else let ctx := r.ctx; let erased := ctx.simpLemmas.erased; do let hs ← liftM Lean.Elab.Tactic.getPropHyps let ctx : Lean.Meta.Simp.Context := ctx let fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId := ∅ let r ← forIn hs { fst := fvarIdToLemmaId, snd := ctx } fun h r => let fvarIdToLemmaId := r.fst; let ctx := r.snd; do let localDecl ← liftM (Lean.Meta.getLocalDecl h) if Std.PersistentHashSet.contains erased (Lean.LocalDecl.userName localDecl) = true then do pure PUnit.unit pure (ForInStep.yield { fst := fvarIdToLemmaId, snd := ctx }) else let fvarId := Lean.LocalDecl.fvarId localDecl; let proof := Lean.LocalDecl.toExpr localDecl; do let id ← liftM (Lean.mkFreshUserName `h) let fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId := Std.RBMap.insert fvarIdToLemmaId fvarId id let simpLemmas ← liftM (Lean.Meta.SimpLemmas.add ctx.simpLemmas #[] proof false true 1000 (some id)) let ctx : Lean.Meta.Simp.Context := { config := ctx.config, simpLemmas := simpLemmas, congrLemmas := ctx.congrLemmas, parent? := ctx.parent?, dischargeDepth := ctx.dischargeDepth } pure PUnit.unit pure (ForInStep.yield { fst := fvarIdToLemmaId, snd := ctx }) let x : MProd Lean.Meta.FVarIdToLemmaId Lean.Meta.Simp.Context := r match x with | { fst := fvarIdToLemmaId, snd := ctx } => pure { ctx := ctx, dischargeWrapper := dischargeWrapper, fvarIdToLemmaId := fvarIdToLemmaId } if simpOnly = true then do let y ← liftM (Lean.Meta.SimpLemmas.addConst { pre := Lean.Meta.DiscrTree.empty, post := Lean.Meta.DiscrTree.empty, lemmaNames := ∅, toUnfold := ∅, erased := ∅, toUnfoldThms := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } `eq_self true false 1000) _do_jp y else do let y ← liftM Lean.Meta.getSimpLemmas _do_jp y; if (ctx && !Lean.Syntax.isNone (Lean.Syntax.getOp stx 2)) = true then do let y ← Lean.throwError (Lean.toMessageData "'simp_all' tactic does not support 'discharger' option") _do_jp y else do let y ← pure PUnit.unit _do_jp y
def
Lean.Elab.Tactic.simpLocation
(ctx : Lean.Meta.Simp.Context)
(discharge? : optParam (Option Lean.Meta.Simp.Discharge) none)
(fvarIdToLemmaId : optParam Lean.Meta.FVarIdToLemmaId ∅)
(loc : Lean.Elab.Tactic.Location)
:
Equations
- Lean.Elab.Tactic.simpLocation ctx discharge? fvarIdToLemmaId loc = (fun go => match loc with | Lean.Elab.Tactic.Location.targets hyps simplifyTarget => Lean.Elab.Tactic.withMainContext do let fvarIds ← Lean.Elab.Tactic.getFVarIds hyps go fvarIds simplifyTarget fvarIdToLemmaId | Lean.Elab.Tactic.Location.wildcard => Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.getMainGoal let a ← liftM (Lean.Meta.getNondepPropHyps a) go a true fvarIdToLemmaId) (Lean.Elab.Tactic.simpLocation.go ctx discharge?)
def
Lean.Elab.Tactic.simpLocation.go
(ctx : Lean.Meta.Simp.Context)
(discharge? : optParam (Option Lean.Meta.Simp.Discharge) none)
(fvarIdsToSimp : Array Lean.FVarId)
(simplifyTarget : Bool)
(fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId)
:
Equations
- Lean.Elab.Tactic.simpLocation.go ctx discharge? fvarIdsToSimp simplifyTarget fvarIdToLemmaId = do let mvarId ← Lean.Elab.Tactic.getMainGoal let result? ← liftM (Lean.Meta.simpGoal mvarId ctx discharge? simplifyTarget fvarIdsToSimp fvarIdToLemmaId) match result? with | none => Lean.Elab.Tactic.replaceMainGoal [] | some (x, mvarId) => Lean.Elab.Tactic.replaceMainGoal [mvarId]
Equations
- Lean.Elab.Tactic.evalSimp stx = do let discr ← Lean.Elab.Tactic.withMainContext (Lean.Elab.Tactic.mkSimpContext stx false false false) let x : Lean.Elab.Tactic.MkSimpContextResult := discr match x with | { ctx := ctx, dischargeWrapper := dischargeWrapper, fvarIdToLemmaId := fvarIdToLemmaId } => Lean.Elab.Tactic.Simp.DischargeWrapper.with dischargeWrapper fun discharge? => Lean.Elab.Tactic.simpLocation ctx discharge? fvarIdToLemmaId (Lean.Elab.Tactic.expandOptLocation (Lean.Syntax.getOp stx 5))
Equations
- Lean.Elab.Tactic.evalSimpAll stx = do let discr ← Lean.Elab.Tactic.mkSimpContext stx true true true let x : Lean.Elab.Tactic.MkSimpContextResult := discr match x with | { ctx := ctx, dischargeWrapper := x, fvarIdToLemmaId := x_1 } => do let a ← Lean.Elab.Tactic.getMainGoal let a ← liftM (Lean.Meta.simpAll a ctx) match a with | none => Lean.Elab.Tactic.replaceMainGoal [] | some mvarId => Lean.Elab.Tactic.replaceMainGoal [mvarId]