max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add Macro.State.Extra

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-23 16:11:12 -07:00
parent 1151ef9af0
commit 0838b95105
2 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Prelude.lean
View file

@ -2042,8 +2042,15 @@ inductive Exception where
| error : Syntax → String → Exception
| unsupportedSyntax : Exception
constant State.ExtraPointed : PointedType.{0}
def State.Extra : Type := State.ExtraPointed.type
instance : Inhabited State.Extra where
default := State.ExtraPointed.val
structure State where
macroScope : MacroScope
extra : State.Extra
deriving Inhabited
end Macro

3
src/Lean/Elab/Util.lean
View file

@ -161,7 +161,8 @@ private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syn
currMacroScope := ← MonadMacroAdapter.getCurrMacroScope,
mainModule := env.mainModule,
currRecDepth := ← MonadRecDepth.getRecDepth,
maxRecDepth := ← MonadRecDepth.getMaxRecDepth } { macroScope := (← MonadMacroAdapter.getNextMacroScope) } with
maxRecDepth := ← MonadRecDepth.getMaxRecDepth }
{ macroScope := (← MonadMacroAdapter.getNextMacroScope), extra := arbitrary } with
| EStateM.Result.error Macro.Exception.unsupportedSyntax _ => throwUnsupportedSyntax
| EStateM.Result.error (Macro.Exception.error ref msg) _ => throwErrorAt ref msg
| EStateM.Result.ok a s => MonadMacroAdapter.setNextMacroScope s.macroScope; pure a