fix: fixes #175

src/Lean/Elab/Util.lean

@@ -59,25 +59,44 @@ match macroStack with
       msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ macroFmt))
     msgData
 
-def checkSyntaxNodeKind (env : Environment) (k : Name) : ExceptT String Id Name :=
+def checkSyntaxNodeKind (k : Name) : AttrM Name := do
+env ← getEnv;
 if Parser.isValidSyntaxNodeKind env k then pure k
-else throw "failed"
+else throwError "failed"
 
-def checkSyntaxNodeKindAtNamespaces (env : Environment) (k : Name) : List Name → ExceptT String Id Name
-| []    => throw "failed"
-| n::ns => checkSyntaxNodeKind env (n ++ k) <|> checkSyntaxNodeKindAtNamespaces ns
+namespace OldFrontend -- TODO: delete
 
-def syntaxNodeKindOfAttrParam (env : Environment) (defaultParserNamespace : Name) (arg : Syntax) : ExceptT String Id SyntaxNodeKind :=
+private def checkSyntaxNodeKindAtNamespacesAux (k : Name) : List Name → AttrM Name
+| []    => throwError "failed"
+| n::ns => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux ns
+
+def checkSyntaxNodeKindAtNamespaces (k : Name) : AttrM Name := do
+env ← getEnv;
+checkSyntaxNodeKindAtNamespacesAux k (Lean.TODELETE.getNamespaces env)
+
+end OldFrontend
+
+def checkSyntaxNodeKindAtNamespacesAux (k : Name) : Name → AttrM Name
+| n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux p
+| _ => throwError "failed"
+
+def checkSyntaxNodeKindAtNamespaces (k : Name) : AttrM Name := do
+ctx ← read;
+checkSyntaxNodeKindAtNamespacesAux k ctx.currNamespace
+
+def syntaxNodeKindOfAttrParam (defaultParserNamespace : Name) (arg : Syntax) : AttrM SyntaxNodeKind :=
 match attrParamSyntaxToIdentifier arg with
 | some k =>
-  checkSyntaxNodeKind env k
+  checkSyntaxNodeKind k
   <|>
-  checkSyntaxNodeKindAtNamespaces env k (Lean.TODELETE.getNamespaces env) -- TODO: fix for the new frontend. We do not store the current namespaces and OpenDecls in the environment
+  checkSyntaxNodeKindAtNamespaces k
   <|>
-  checkSyntaxNodeKind env (defaultParserNamespace ++ k)
+  OldFrontend.checkSyntaxNodeKindAtNamespaces k -- TODO: delete the following old frontend support code
   <|>
-  throw ("invalid syntax node kind '" ++ toString k ++ "'")
-| none   => throw ("syntax node kind is missing")
+  checkSyntaxNodeKind (defaultParserNamespace ++ k)
+  <|>
+  throwError ("invalid syntax node kind '" ++ toString k ++ "'")
+| none   => throwError ("syntax node kind is missing")
 
 private unsafe def evalSyntaxConstantUnsafe (env : Environment) (constName : Name) : ExceptT String Id Syntax :=
 env.evalConstCheck Syntax `Lean.Syntax constName
@@ -94,7 +113,7 @@ KeyedDeclsAttribute.init {
   name := attrName,
   descr := kind ++ " elaborator",
   valueTypeName := typeName,
-  evalKey := fun _ env arg => syntaxNodeKindOfAttrParam env parserNamespace arg,
+  evalKey := fun _ arg => syntaxNodeKindOfAttrParam parserNamespace arg,
 } attrDeclName
 
 unsafe def mkMacroAttribute : IO (KeyedDeclsAttribute Macro) :=

src/Lean/KeyedDeclsAttribute.lean

@@ -32,10 +32,10 @@ structure Def (γ : Type) :=
 (descr         : String)  -- Attribute description
 (valueTypeName : Name)
 -- Convert `Syntax` into a `Key`, the default implementation expects an identifier.
-(evalKey       : Bool → Environment → Syntax → Except String Key :=
-  fun builtin env arg => match attrParamSyntaxToIdentifier arg with
-    | some id => Except.ok id
-    | none    => Except.error "invalid attribute argument, expected identifier")
+(evalKey       : Bool → Syntax → AttrM Key :=
+  fun builtin arg => match attrParamSyntaxToIdentifier arg with
+    | some id => pure id
+    | none    => throwError "invalid attribute argument, expected identifier")
 
 instance Def.inhabited {γ} : Inhabited (Def γ) :=
 ⟨{ builtinName := arbitrary _, name := arbitrary _, descr := arbitrary _, valueTypeName := arbitrary _ }⟩
@@ -133,14 +133,14 @@ registerBuiltinAttribute {
   name  := df.builtinName,
   descr := "(builtin) " ++ df.descr,
   add   := fun declName arg persistent => do {
-    env ← getEnv;
     unless persistent $ throwError ("invalid attribute '" ++ df.builtinName ++ "', must be persistent");
-    key ← ofExcept $ df.evalKey true env arg;
+    key ← df.evalKey true arg;
     decl ← getConstInfo declName;
     match decl.type with
     | Expr.const c _ _ =>
       if c != df.valueTypeName then throwError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected")
       else do
+        env ← getEnv;
         env ← liftIO $ declareBuiltin df attrDeclName env key declName;
         setEnv env
     | _ => throwError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected")
@@ -151,8 +151,8 @@ registerBuiltinAttribute {
   name            := df.name,
   descr           := df.descr,
   add             := fun constName arg persistent => do
+    key ← df.evalKey false arg;
     env ← getEnv;
-    key ← ofExcept $ df.evalKey false env arg;
     val ← ofExcept $ env.evalConstCheck γ df.valueTypeName constName;
     setEnv $ ext.addEntry env { key := key, decl := constName, value := val },
   applicationTime := AttributeApplicationTime.afterCompilation

src/Lean/PrettyPrinter/Formatter.lean

@@ -58,13 +58,15 @@ KeyedDeclsAttribute.init {
 
 [formatter k] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `SyntaxNodeKind` `k`.",
   valueTypeName := `Lean.PrettyPrinter.Formatter,
-  evalKey := fun builtin env args => match attrParamSyntaxToIdentifier args with
+  evalKey := fun builtin args => do
+    env ← getEnv;
+    match attrParamSyntaxToIdentifier args with
     | some id =>
       -- `isValidSyntaxNodeKind` is updated only in the next stage for new `[builtin*Parser]`s, but we try to
       -- synthesize a formatter for it immediately, so we just check for a declaration in this case
       if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id
-      else throw ("invalid [formatter] argument, unknown syntax kind '" ++ toString id ++ "'")
-    | none    => throw "invalid [formatter] argument, expected identifier"
+      else throwError ("invalid [formatter] argument, unknown syntax kind '" ++ toString id ++ "'")
+    | none    => throwError "invalid [formatter] argument, expected identifier"
 } `Lean.PrettyPrinter.formatterAttribute
 @[init mkFormatterAttribute] constant formatterAttribute : KeyedDeclsAttribute Formatter := arbitrary _
 

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -118,13 +118,15 @@ KeyedDeclsAttribute.init {
 
 [parenthesizer k] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `SyntaxNodeKind` `k`.",
   valueTypeName := `Lean.PrettyPrinter.Parenthesizer,
-  evalKey := fun builtin env args => match attrParamSyntaxToIdentifier args with
+  evalKey := fun builtin args => do
+    env ← getEnv;
+    match attrParamSyntaxToIdentifier args with
     | some id =>
       -- `isValidSyntaxNodeKind` is updated only in the next stage for new `[builtin*Parser]`s, but we try to
       -- synthesize a parenthesizer for it immediately, so we just check for a declaration in this case
       if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id
-      else throw ("invalid [parenthesizer] argument, unknown syntax kind '" ++ toString id ++ "'")
-    | none    => throw "invalid [parenthesizer] argument, expected identifier"
+      else throwError ("invalid [parenthesizer] argument, unknown syntax kind '" ++ toString id ++ "'")
+    | none    => throwError "invalid [parenthesizer] argument, expected identifier"
 } `Lean.PrettyPrinter.parenthesizerAttribute
 @[init mkParenthesizerAttribute] constant parenthesizerAttribute : KeyedDeclsAttribute Parenthesizer := arbitrary _
 
@@ -141,11 +143,13 @@ which is used when parenthesizing calls of `categoryParser cat prec`. Implementa
 with the precedence and `cat`. If no category parenthesizer is registered, the category will never be parenthesized,
 but still be traversed for parenthesizing nested categories.",
   valueTypeName := `Lean.PrettyPrinter.CategoryParenthesizer,
-  evalKey := fun _ env args => match attrParamSyntaxToIdentifier args with
+  evalKey := fun _ args => do
+    env ← getEnv;
+    match attrParamSyntaxToIdentifier args with
     | some id =>
       if Parser.isParserCategory env id then pure id
-      else throw ("invalid [parenthesizer] argument, unknown parser category '" ++ toString id ++ "'")
-    | none    => throw "invalid [parenthesizer] argument, expected identifier"
+      else throwError ("invalid [parenthesizer] argument, unknown parser category '" ++ toString id ++ "'")
+    | none    => throwError "invalid [parenthesizer] argument, expected identifier"
 } `Lean.PrettyPrinter.categoryParenthesizerAttribute
 @[init mkCategoryParenthesizerAttribute] constant categoryParenthesizerAttribute : KeyedDeclsAttribute CategoryParenthesizer := arbitrary _
 

tests/lean/run/175.lean

@@ -0,0 +1,26 @@
+import Lean
+new_frontend
+
+namespace Foo
+open Lean.Elab.Term
+
+syntax[fooKind] "foo!" term : term
+
+@[termElab fooKind] def elabFoo : TermElab :=
+fun stx expectedType? => elabTerm (stx.getArg 1) expectedType?
+
+#check foo! 10
+
+end Foo
+
+namespace Lean
+namespace Elab
+namespace Tactic
+open Meta
+
+@[builtinTactic clear] def myEvalClear : Tactic := -- this fails in the old-frontend because it eagerly resolves `clear` as `Lean.Meta.clear`.
+fun _ => pure ()
+
+end Tactic
+end Elab
+end Lean