From 4fc06bfccacffd8dbca225a42708102a91768c23 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Dec 2020 10:02:12 -0800 Subject: [PATCH] feat: add optional `(priority := )` to `instance` command --- src/Lean/Elab/Declaration.lean | 4 ++-- src/Lean/Elab/DefView.lean | 12 +++++++----- src/Lean/Elab/Syntax.lean | 15 --------------- src/Lean/Elab/Util.lean | 15 +++++++++++++++ src/Lean/Meta/Instances.lean | 5 +---- src/Lean/Parser/Command.lean | 6 +++++- src/Lean/Parser/Syntax.lean | 2 -- tests/lean/run/instprio.lean | 17 +++++++++++++++++ 8 files changed, 47 insertions(+), 29 deletions(-) create mode 100644 tests/lean/run/instprio.lean diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 7304133217..09bc6c6eba 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -45,10 +45,10 @@ def expandDeclNamespace? (stx : Syntax) : Option (Name × Syntax) := | some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 1 declId)) | none => none else if k == `Lean.Parser.Command.instance then - let optDeclId := decl[2] + let optDeclId := decl[3] if optDeclId.isNone then none else match expandDeclIdNamespace? optDeclId[0] with - | some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 2 (optDeclId.setArg 0 declId))) + | some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 3 (optDeclId.setArg 0 declId))) | none => none else none diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index c49c2b7e02..f744f38b4f 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -138,18 +138,20 @@ def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM De } def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do - -- parser! attrKind >> "instance " >> optional declId >> declSig >> declVal + -- parser! Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal let attrKind ← toAttributeKind stx[0] - let (binders, type) := expandDeclSig stx[3] - let modifiers := modifiers.addAttribute { kind := attrKind, name := `instance } - let declId ← match stx[2].getOptional? with + let prio ← liftMacroM <| expandOptNamedPrio stx[2] + let attrStx ← `(attr| instance $(quote prio):numLit) + let (binders, type) := expandDeclSig stx[4] + let modifiers := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx } + let declId ← match stx[3].getOptional? with | some declId => pure declId | none => let id ← MkInstanceName.main type pure <| Syntax.node ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode] return { ref := stx, kind := DefKind.def, modifiers := modifiers, - declId := declId, binders := binders, type? := type, value := stx[4] + declId := declId, binders := binders, type? := type, value := stx[5] } def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView := diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index a8457eda5e..9457fe9a51 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -230,21 +230,6 @@ where | Name.str _ s _ => s ++ str | _ => str - -def expandOptNamedPrio (stx : Syntax) : MacroM Nat := - if stx.isNone then - return evalPrio! default - else match stx[0] with - | `(Parser.Command.namedPrio| (priority := $prio)) => evalPrio prio - | _ => Macro.throwUnsupported - -def expandOptNamedName (stx : Syntax) : MacroM (Option Name) := do - if stx.isNone then - return none - else match stx[0] with - | `(Parser.Command.namedName| (name := $name)) => return name.getId - | _ => Macro.throwUnsupported - /- We assume a new syntax can be treated as an atom when it starts and ends with a token. Here are examples of atom-like syntax. ``` diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index 29678ff8ba..6994b63425 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Util.Trace +import Lean.Parser.Syntax import Lean.Parser.Extension import Lean.KeyedDeclsAttribute import Lean.Elab.Exception @@ -26,6 +27,20 @@ def MacroScopesView.format (view : MacroScopesView) (mainModule : Name) : Format namespace Elab +def expandOptNamedPrio (stx : Syntax) : MacroM Nat := + if stx.isNone then + return evalPrio! default + else match stx[0] with + | `(Parser.Command.namedPrio| (priority := $prio)) => evalPrio prio + | _ => Macro.throwUnsupported + +def expandOptNamedName (stx : Syntax) : MacroM (Option Name) := do + if stx.isNone then + return none + else match stx[0] with + | `(Parser.Command.namedName| (name := $name)) => return name.getId + | _ => Macro.throwUnsupported + structure MacroStackElem where before : Syntax after : Syntax diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 1a42ffea49..343e0225b0 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -55,10 +55,7 @@ builtin_initialize name := `instance descr := "type class instance" add := fun declName stx attrKind => do - let prio ← match stx with - | Syntax.missing => pure <| evalPrio! default -- small hack, in the elaborator we use `Syntax.missing` when creating attribute views for `instance - | _ => getAttrParamOptPrio stx[1] - -- TODO use prio + let prio ← getAttrParamOptPrio stx[1] discard <| addInstance declName attrKind prio |>.run {} {} } diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 3eca180d17..1427ccd105 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -18,6 +18,10 @@ namespace Parser @[builtinTermParser] def Term.quot := parser! "`(" >> toggleInsideQuot (termParser <|> many1Unbox commandParser) >> ")" namespace Command + +def namedPrio := parser! (atomic ("(" >> nonReservedSymbol "priority") >> " := " >> priorityParser >> ")") +def optNamedPrio := optional namedPrio + def commentBody : Parser := { fn := rawFn (finishCommentBlock 1) true } @@ -42,7 +46,7 @@ def «abbrev» := parser! "abbrev " >> declId >> optDeclSig >> declVal def «def» := parser! "def " >> declId >> optDeclSig >> declVal def «theorem» := parser! "theorem " >> declId >> declSig >> declVal def «constant» := parser! "constant " >> declId >> declSig >> optional declValSimple -def «instance» := parser! Term.attrKind >> "instance " >> optional declId >> declSig >> declVal +def «instance» := parser! Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal def «axiom» := parser! "axiom " >> declId >> declSig def «example» := parser! "example " >> declSig >> declVal def inferMod := parser! atomic (symbol "{" >> "}") diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 09678854ff..f17d4673b2 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -50,9 +50,7 @@ end Term namespace Command -def namedPrio := parser! (atomic ("(" >> nonReservedSymbol "priority") >> " := " >> priorityParser >> ")") def namedName := parser! (atomic ("(" >> nonReservedSymbol "name") >> " := " >> ident >> ")") -def optNamedPrio := optional namedPrio def optNamedName := optional namedName def «prefix» := parser! "prefix" diff --git a/tests/lean/run/instprio.lean b/tests/lean/run/instprio.lean new file mode 100644 index 0000000000..1555bcbbb6 --- /dev/null +++ b/tests/lean/run/instprio.lean @@ -0,0 +1,17 @@ +class Def (α : Type u) where + val : α + +instance : Def Nat where + val := 10 + +theorem ex1 : Def.val = 10 := rfl + +instance (priority := default+1) : Def Nat where + val := 20 + +theorem ex2 : Def.val = 20 := rfl + +instance : Def Nat where + val := 30 + +theorem ex3 : Def.val = 20 := rfl