From 8e20b6001ae3e9ba9d1a379454f3358f8d42449d Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 17 Mar 2025 09:55:43 -0400 Subject: [PATCH] feat: `run_macro` & `run_cmd_macro` --- src/Init/Notation.lean | 15 +++++ src/Lean/Elab/BuiltinEvalCommand.lean | 88 +++++++++++++++++---------- src/Lean/Elab/Command.lean | 3 + tests/lean/run/run_macro.lean | 17 ++++++ 4 files changed, 91 insertions(+), 32 deletions(-) create mode 100644 tests/lean/run/run_macro.lean diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 1d3d27702e79..81fc2c9366ae 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -619,6 +619,21 @@ This is the same as `#eval show MetaM Unit from do discard doSeq`. -/ syntax (name := runMeta) "run_meta " doSeq : command +/-- +The `run_macro doSeq` command executes code in `MacroM Unit`. +This is the same as `#eval show MacroM Unit from do discard doSeq`. +-/ +syntax (name := runMacro) "run_macro " doSeq : command + +/-- +The `run_cmd_macro doSeq` command executes code in `MacroM Command`. +The produced command is then immediately elaborated. + +This effectively the same as `run_cmd elabCommand (← do doSeq)`, +but this works without any imports. +-/ +syntax (name := runCmdMacro) "run_cmd_macro " doSeq : command + set_option linter.missingDocs false in syntax guardMsgsFilterSeverity := &"info" <|> &"warning" <|> &"error" <|> &"all" diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean index adefdfc186d4..cb306e477aa3 100644 --- a/src/Lean/Elab/BuiltinEvalCommand.lean +++ b/src/Lean/Elab/BuiltinEvalCommand.lean @@ -37,7 +37,7 @@ builtin_initialize /-- Elaborates the term, ensuring the result has no expression metavariables. If there would be unsolved-for metavariables, tries hinting that the resulting type -is a monadic value with the `CommandElabM`, `TermElabM`, or `IO` monads. +is a monadic value with the `CommandElabM`, `TermElabM`, `MarcoM`, or `IO` monads. Throws errors if the term is a proof or a type, but lifts props to `Bool` using `mkDecide`. -/ private def elabTermForEval (term : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do @@ -63,7 +63,7 @@ where catch ex => let exS ← saveState -- Try hinting that `ty` is a monad application. - for m in #[``CommandElabM, ``TermElabM, ``IO] do + for m in #[``CommandElabM, ``TermElabM, ``MacroM, ``IO] do s.restore true try if ← isDefEq ty (← mkFreshMonadApp m) then @@ -159,8 +159,34 @@ private structure EvalAction where If `some`, the expression is what type to use for the type ascription when `pp.type` is true. -/ printVal : Option Expr -unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) : CommandElabM Unit := withRef tk do +def elabEvalCoreAux (tk term : Syntax) (expectedType? : Option Expr) + (mkAct : Name → Expr → TermElabM EvalAction) : CommandElabM Unit := withRef tk do let declName := `_eval + let (output, exOrRes) ← IO.FS.withIsolatedStreams do + try + -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure + -- we don't pollute the environment with auxiliary declarations. + let act : EvalAction ← liftTermElabM do Term.withDeclName declName do withoutModifyingEnv do + let e ← elabTermForEval term expectedType? + -- If there is an elaboration error, don't evaluate! + if e.hasSyntheticSorry then throwAbortTerm + mkAct declName e + let res ← act.eval + return Sum.inr (res, act.printVal) + catch ex => + return Sum.inl ex + if !output.isEmpty then logInfoAt tk output + match exOrRes with + | .inl ex => logException ex + | .inr (_, none) => pure () + | .inr (res, some type) => + if eval.type.get (← getOptions) then + logInfo m!"{res} : {type}" + else + logInfo res + +unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) : CommandElabM Unit := do + elabEvalCoreAux tk term expectedType? fun declName e => do -- `t` is either `MessageData` or `Format`, and `mkT` is for synthesizing an expression that yields a `t`. -- The `toMessageData` function adapts `t` to `MessageData`. let mkAct {t : Type} [Inhabited t] (toMessageData : t → MessageData) (mkT : Expr → MetaM Expr) (e : Expr) : TermElabM EvalAction := do @@ -185,8 +211,8 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? : if let some act ← mkMAct? ``CommandElabM CommandElabM e -- Fallbacks in case we are in the Lean package but don't have `CommandElabM` yet <||> mkMAct? ``TermElabM TermElabM e <||> mkMAct? ``MetaM MetaM e <||> mkMAct? ``CoreM CoreM e - -- Fallback in case nothing is imported - <||> mkMAct? ``IO IO e then + -- Fallbacks in case nothing is imported + <||> mkMAct? ``MacroM MacroM e <||> mkMAct? ``IO IO e then return act else -- Otherwise, assume this is a pure value. @@ -208,33 +234,12 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? : -- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below. let r ← toMessageData <$> evalConst t declName return { eval := pure r, printVal := some (← inferType e) } - let (output, exOrRes) ← IO.FS.withIsolatedStreams do - try - -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure - -- we don't pollute the environment with auxiliary declarations. - let act : EvalAction ← liftTermElabM do Term.withDeclName declName do withoutModifyingEnv do - let e ← elabTermForEval term expectedType? - -- If there is an elaboration error, don't evaluate! - if e.hasSyntheticSorry then throwAbortTerm - -- We want `#eval` to work even in the core library, so if `ofFormat` isn't available, - -- we fall back on a `Format`-based approach. - if (← getEnv).contains ``Lean.MessageData.ofFormat then - mkAct id (mkMessageData ·) e - else - mkAct Lean.MessageData.ofFormat (mkFormat ·) e - let res ← act.eval - return Sum.inr (res, act.printVal) - catch ex => - return Sum.inl ex - if !output.isEmpty then logInfoAt tk output - match exOrRes with - | .inl ex => logException ex - | .inr (_, none) => pure () - | .inr (res, some type) => - if eval.type.get (← getOptions) then - logInfo m!"{res} : {type}" - else - logInfo res + -- We want `#eval` to work even in the core library, so if `ofFormat` isn't available, + -- we fall back on a `Format`-based approach. + if (← getEnv).contains ``Lean.MessageData.ofFormat then + mkAct id (mkMessageData ·) e + else + mkAct Lean.MessageData.ofFormat (mkFormat ·) e @[implemented_by elabEvalCoreUnsafe] opaque elabEvalCore (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) : CommandElabM Unit @@ -274,4 +279,23 @@ def elabRunMeta : CommandElab := fun stx => elabEvalCore false tk (← `(discard do $elems)) (mkApp (mkConst ``MetaM) (mkConst ``Unit)) | _ => throwUnsupportedSyntax +@[builtin_command_elab runMacro] +def elabRunMacro : CommandElab := fun stx => + match stx with + | `(run_macro%$tk $elems:doSeq) => do + elabEvalCore false tk (← `(discard do $elems)) (mkApp (mkConst ``MacroM) (mkConst ``Unit)) + | _ => throwUnsupportedSyntax + +@[builtin_command_elab runCmdMacro] +def elabRunCmdMacro : CommandElab + | `(run_cmd_macro%$tk $elems:doSeq) => do + let mkAct declName e : TermElabM EvalAction := do + addAndCompileExprForEval declName e + -- Safety: `e` has the (expected) type `MacroM Command`, + -- which we are assuming is defined appropriately in the environment. + let mf : MacroM Command ← unsafe evalConst (MacroM Command) declName + return { eval := do elabCommand =<< MonadEvalT.monadEval mf; pure "", printVal := none } + elabEvalCoreAux tk (← `(do $elems)) (mkApp (mkConst ``MacroM) (mkConst ``Command)) mkAct + | _ => throwUnsupportedSyntax + end Lean.Elab.Command diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index aeb0b820e30c..0312eb942593 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -436,6 +436,9 @@ instance : MonadRecDepth CommandElabM where getRecDepth := return (← read).currRecDepth getMaxRecDepth := return (← get).maxRecDepth +instance : MonadEval MacroM CommandElabM where + monadEval := liftMacroM + builtin_initialize registerTraceClass `Elab.command open Language in diff --git a/tests/lean/run/run_macro.lean b/tests/lean/run/run_macro.lean new file mode 100644 index 000000000000..e5035d3e8c9f --- /dev/null +++ b/tests/lean/run/run_macro.lean @@ -0,0 +1,17 @@ +namespace Test + +open Lean + +/-- info: `Test -/ +#guard_msgs in +#eval Macro.getCurrNamespace + +/-- error: thrown -/ +#guard_msgs in +run_macro Macro.throwError (α := Unit) "thrown" + +run_cmd_macro (TSyntax.mk <| mkNullNode ·) <$> #[`foo, `bar].mapM fun name => + `(def $(mkIdent name) := $(quote name.toString)) + +/-- info: "foobar" -/ +#guard_msgs in #eval foo ++ bar