From 35efb1a6e6b5581bda466925e70f29128e553b0f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 23 Oct 2024 11:21:50 +0200 Subject: [PATCH] refactor: nicer modifiers/ranges API (#5788) Cleanup of #5650 * default `Modifiers.stx` to missing * rename and clarify `addDeclarationRangesFromSyntax` as the main convenience function for user metaprograms --- src/Lean/Elab/BuiltinCommand.lean | 2 +- src/Lean/Elab/BuiltinEvalCommand.lean | 2 +- src/Lean/Elab/DeclModifiers.lean | 3 ++- src/Lean/Elab/Declaration.lean | 4 ++-- src/Lean/Elab/DeclarationRange.lean | 28 ++++++++++++++------------- src/Lean/Elab/Inductive.lean | 4 ++-- src/Lean/Elab/LetRec.lean | 2 +- src/Lean/Elab/MutualDef.lean | 3 +-- src/Lean/Elab/Structure.lean | 8 ++++---- src/Lean/Elab/Tactic/Ext.lean | 4 ++-- 10 files changed, 31 insertions(+), 29 deletions(-) diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 66d21a068ffa..79295519a126 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -343,7 +343,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do if let .none ← findDeclarationRangesCore? declName then -- this is only relevant for declarations added without a declaration range -- in particular `Quot.mk` et al which are added by `init_quot` - addAuxDeclarationRanges declName stx id + addDeclarationRangesFromSyntax declName stx id addDocString declName (← getDocStringText doc) | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean index 659908dda23f..3a11ed0fd81f 100644 --- a/src/Lean/Elab/BuiltinEvalCommand.lean +++ b/src/Lean/Elab/BuiltinEvalCommand.lean @@ -84,7 +84,7 @@ private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorr -- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once -- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages -- such as "failed to infer definition type" can surface. - let defView := mkDefViewOfDef { isUnsafe := true, stx := ⟨.missing⟩ } + let defView := mkDefViewOfDef { isUnsafe := true } (← `(Parser.Command.definition| def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value))) Term.elabMutualDef #[] { header := "" } #[defView] diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 55db381c1a40..a6c86a04e744 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -57,7 +57,8 @@ inductive RecKind where /-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/ structure Modifiers where - stx : TSyntax ``Parser.Command.declModifiers + /-- Input syntax, used for adjusting declaration range (unless missing) -/ + stx : TSyntax ``Parser.Command.declModifiers := ⟨.missing⟩ docString? : Option String := none visibility : Visibility := Visibility.regular isNoncomputable : Bool := false diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 138cac9fa5b3..33a7dcf9218c 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -105,7 +105,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do runTermElabM fun vars => do let scopeLevelNames ← Term.getLevelNames let ⟨shortName, declName, allUserLevelNames⟩ ← Term.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers - addDeclarationRanges declName modifiers.stx stx + addDeclarationRangesForBuiltin declName modifiers.stx stx Term.withAutoBoundImplicitForbiddenPred (fun n => shortName == n) do Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration @@ -332,7 +332,7 @@ def elabMutual : CommandElab := fun stx => do -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as -- otherwise the info context created by `with_decl_name` will be incomplete and break the -- call hierarchy - addDeclarationRanges fullId ⟨defStx.raw[0]⟩ defStx.raw[1] + addDeclarationRangesForBuiltin fullId ⟨defStx.raw[0]⟩ defStx.raw[1] elabCommand (← `( $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq $defStx:command)) diff --git a/src/Lean/Elab/DeclarationRange.lean b/src/Lean/Elab/DeclarationRange.lean index 610fad80a339..44e08e263cbf 100644 --- a/src/Lean/Elab/DeclarationRange.lean +++ b/src/Lean/Elab/DeclarationRange.lean @@ -49,29 +49,31 @@ def getDeclarationSelectionRef (stx : Syntax) : Syntax := else stx[0] +/-- +Derives and adds declaration ranges from given syntax trees. If `rangeStx` does not have a range, +nothing is added. If `selectionRangeStx` does not have a range, it is defaulted to that of +`rangeStx`. +-/ +def addDeclarationRangesFromSyntax [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) + (rangeStx : Syntax) (selectionRangeStx : Syntax := .missing) : m Unit := do + -- may fail on partial syntax, ignore in that case + let some range ← getDeclarationRange? rangeStx | return + let selectionRange ← (·.getD range) <$> getDeclarationRange? selectionRangeStx + Lean.addDeclarationRanges declName { range, selectionRange } /-- Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and `cmdStx` the remaining part of the syntax tree for `declName`. This method is for the builtin declarations only. User-defined commands should use -`Lean.addDeclarationRanges` to store this information for their commands. +`Lean.Elab.addDeclarationRangesFromSyntax` or `Lean.addDeclarationRanges` to store this information +for their commands. -/ -def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) +def addDeclarationRangesForBuiltin [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (modsStx : TSyntax ``Parser.Command.declModifiers) (declStx : Syntax) : m Unit := do if declStx.getKind == ``Parser.Command.«example» then return () let stx := mkNullNode #[modsStx, declStx] - -- may fail on partial syntax, ignore in that case - let some range ← getDeclarationRange? stx | return - let some selectionRange ← getDeclarationRange? (getDeclarationSelectionRef declStx) | return - Lean.addDeclarationRanges declName { range, selectionRange } - -/-- Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc. -/ -def addAuxDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) (header : Syntax) : m Unit := do - -- may fail on partial syntax, ignore in that case - let some range ← getDeclarationRange? stx | return - let some selectionRange ← getDeclarationRange? header | return - Lean.addDeclarationRanges declName { range, selectionRange } + addDeclarationRangesFromSyntax declName stx (getDeclarationSelectionRef declStx) end Lean.Elab diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 155cdcdc23c7..cb59576744d6 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -94,7 +94,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term let (binders, type?) := expandOptDeclSig decl[2] let declId := decl[1] let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers - addDeclarationRanges declName modifiers.stx decl + addDeclarationRangesForBuiltin declName modifiers.stx decl let ctors ← decl[4].getArgs.mapM fun ctor => withRef ctor do -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩ @@ -112,7 +112,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers.visibility ctorName let (binders, type?) := expandOptDeclSig ctor[4] addDocString' ctorName ctorModifiers.docString? - addAuxDeclarationRanges ctorName ctor ctor[3] + addDeclarationRangesFromSyntax ctorName ctor ctor[3] return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView } let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ } diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index 64b8b9f61141..32c3d4abc0a7 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -51,7 +51,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do checkNotAlreadyDeclared declName applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration addDocString' declName docStr? - addAuxDeclarationRanges declName decl declId + addDeclarationRangesFromSyntax declName decl declId let binders := decl[1].getArgs let typeStx := expandOptType declId decl[2] let (type, binderIds) ← elabBindersEx binders fun xs => do diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index a4646595d55b..ccb1af447708 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -887,7 +887,6 @@ def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind := else DefKind.«def» def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers := { - stx := ⟨mkNullNode #[]⟩ -- ignore when computing declaration range isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable recKind := if mainHeaders.any fun h => h.modifiers.isPartial then RecKind.partial else RecKind.default isUnsafe := mainHeaders.any fun h => h.modifiers.isUnsafe @@ -998,7 +997,7 @@ where for view in views, header in headers do -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting -- that depends only on a part of the ref - addDeclarationRanges header.declName view.modifiers.stx view.ref + addDeclarationRangesForBuiltin header.declName view.modifiers.stx view.ref processDeriving (headers : Array DefViewElabHeader) := do diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 5f2d4c9034ca..afa96659f6d7 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -94,7 +94,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc let useDefault := do let declName := structDeclName ++ defaultCtorName let ref := structStx[1].mkSynthetic - addAuxDeclarationRanges declName ref ref + addDeclarationRangesFromSyntax declName ref pure { ref, modifiers := default, name := defaultCtorName, declName } if structStx[5].isNone then useDefault @@ -115,7 +115,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc let declName := structDeclName ++ name let declName ← applyVisibility ctorModifiers.visibility declName addDocString' declName ctorModifiers.docString? - addAuxDeclarationRanges declName ctor[1] ctor[1] + addDeclarationRangesFromSyntax declName ctor[1] pure { ref := ctor[1], name, modifiers := ctorModifiers, declName } def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do @@ -815,7 +815,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do view.fields.forM fun field => do if field.declName == view.ctor.declName then throwErrorAt field.ref "invalid field name '{field.name}', it is equal to structure constructor name" - addAuxDeclarationRanges field.declName field.ref field.ref + addDeclarationRangesFromSyntax field.declName field.ref let type ← Term.elabType view.type unless validStructType type do throwErrorAt view.type "expected Type" withRef view.ref do @@ -912,7 +912,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := let scopeLevelNames ← Term.getLevelNames let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers Term.withAutoBoundImplicitForbiddenPred (fun n => name == n) do - addDeclarationRanges declName modifiers.stx stx + addDeclarationRangesForBuiltin declName modifiers.stx stx Term.withDeclName declName do let ctor ← expandCtor stx modifiers declName let fields ← expandFields stx modifiers declName diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean index dbfe47f4663d..d8011ad50351 100644 --- a/src/Lean/Elab/Tactic/Ext.lean +++ b/src/Lean/Elab/Tactic/Ext.lean @@ -123,7 +123,7 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl levelParams := info.levelParams } modifyEnv fun env => addProtected env extName - addAuxDeclarationRanges extName (← getRef) (← getRef) + addDeclarationRangesFromSyntax extName (← getRef) catch e => throwError m!"\ Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}" @@ -161,7 +161,7 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do -- Only declarations in a namespace can be protected: unless extIffName.isAtomic do modifyEnv fun env => addProtected env extIffName - addAuxDeclarationRanges extName (← getRef) (← getRef) + addDeclarationRangesFromSyntax extName (← getRef) catch e => throwError m!"\ Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\