From f4b5ec710f30ca6f8e820e72e15b7fe11d0bfa24 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Sep 2020 17:11:15 -0700 Subject: [PATCH] fix: fixes #175 --- src/Lean/Elab/Util.lean | 43 ++++++++++++++++------- src/Lean/KeyedDeclsAttribute.lean | 14 ++++---- src/Lean/PrettyPrinter/Formatter.lean | 8 +++-- src/Lean/PrettyPrinter/Parenthesizer.lean | 16 +++++---- tests/lean/run/175.lean | 26 ++++++++++++++ 5 files changed, 79 insertions(+), 28 deletions(-) create mode 100644 tests/lean/run/175.lean diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index 54b843e5de..b89d81fd8a 100644 --- a/src/Lean/Elab/Util.lean +++ b/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) := diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index 0bcb64fb27..f614d3cae0 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/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 diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 978aeb6087..65268524cc 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/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 _ diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 14bb7e5fde..2a53f125fa 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/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 _ diff --git a/tests/lean/run/175.lean b/tests/lean/run/175.lean new file mode 100644 index 0000000000..0b58912b95 --- /dev/null +++ b/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