From b4e9ba15007f45da668667ee7627fbc6e85930aa Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 17 Jun 2021 11:25:34 +0200 Subject: [PATCH] perf: specialize more monad instances --- src/Lean/Elab/Command.lean | 4 ++++ src/Lean/Elab/Tactic/Basic.lean | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index caa4be5609..6a67225a10 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -55,6 +55,10 @@ abbrev CommandElabM := CommandElabCoreM Exception abbrev CommandElab := Syntax → CommandElabM Unit abbrev Linter := Syntax → CommandElabM Unit +-- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the +-- whole monad stack at every use site. May eventually be covered by `deriving`. +instance : Monad CommandElabM := { inferInstanceAs (Monad CommandElabM) with } + def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := { env := env messages := messages diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 9abb0d8632..29d88dc984 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -49,6 +49,10 @@ structure SavedState where abbrev TacticM := ReaderT Context $ StateRefT State TermElabM abbrev Tactic := Syntax → TacticM Unit +-- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the +-- whole monad stack at every use site. May eventually be covered by `deriving`. +instance : Monad TacticM := { inferInstanceAs (Monad TacticM) with } + def getGoals : TacticM (List MVarId) := return (← get).goals