From 92dec7e864911392de52d2e8bec4f12e6895f4f1 Mon Sep 17 00:00:00 2001 From: Parth Shastri <31370288+cppio@users.noreply.github.com> Date: Tue, 17 Jun 2025 13:40:18 -0400 Subject: [PATCH] feat: allow structures to have non-bracketed binders (#8671) This PR allow structures to have non-bracketed binders, making it consistent with `inductive`. The change allows the following to be written instead of having to write `S (n)`: ```lean structure S n where field : Fin n ``` --- src/Lean/Elab/Structure.lean | 44 +++++------ src/Lean/Linter/MissingDocs.lean | 4 +- src/Lean/Linter/UnusedVariables.lean | 16 ++-- src/Lean/Parser/Command.lean | 2 +- tests/lean/1705.lean.expected.out | 7 +- tests/lean/run/structBinderIdent.lean | 104 ++++++++++++++++++++++++++ 6 files changed, 139 insertions(+), 38 deletions(-) create mode 100644 tests/lean/run/structBinderIdent.lean diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index e583fe9a91..726addbc9c 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -30,7 +30,7 @@ namespace Structure /-! Recall that the `structure command syntax is ``` -leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> Term.optType >> optional «extends» >> optional (" := " >> optional structCtor >> structFields) +leading_parser (structureTk <|> classTk) >> declId >> optDeclSig >> optional «extends» >> optional (" := " >> optional structCtor >> structFields) ``` -/ @@ -206,10 +206,10 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc let ref := structStx[1].mkSynthetic addDeclarationRangesFromSyntax declName ref pure { ref, declId := ref, modifiers := default, declName } - if structStx[5].isNone then + if structStx[4].isNone then useDefault else - let optCtor := structStx[5][1] + let optCtor := structStx[4][1] if optCtor.isNone then useDefault else @@ -278,12 +278,12 @@ def structFields := leading_parser many (structExplicitBinder <|> struct ``` -/ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM (Array StructFieldView) := do - if structStx[5][0].isToken ":=" then + if structStx[4][0].isToken ":=" then -- https://github.com/leanprover/lean4/issues/5236 let cmd := if structStx[0].getKind == ``Parser.Command.classTk then "class" else "structure" - withRef structStx[0] <| Linter.logLintIf Linter.linter.deprecated structStx[5][0] + withRef structStx[0] <| Linter.logLintIf Linter.linter.deprecated structStx[4][0] s!"{cmd} ... :=' has been deprecated in favor of '{cmd} ... where'." - let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs + let fieldBinders := if structStx[4].isNone then #[] else structStx[4][2][0].getArgs fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do let mut fieldBinder := fieldBinder if fieldBinder.getKind == ``Parser.Command.structSimpleBinder then @@ -342,43 +342,45 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str } /- -leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> Term.optType >> optional «extends» >> +leading_parser (structureTk <|> classTk) >> declId >> optDeclSig >> optional «extends» >> optional (("where" <|> ":=") >> optional structCtor >> structFields) >> optDeriving where def structParent := leading_parser optional (atomic (ident >> " : ")) >> termParser -def «extends» := leading_parser " extends " >> sepBy1 structParent ", " -def typeSpec := leading_parser " : " >> termParser -def optType : Parser := optional typeSpec +def «extends» := leading_parser " extends " >> sepBy1 structParent ", " >> optType def structFields := leading_parser many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder) def structCtor := leading_parser try (declModifiers >> ident >> " :: ") -/ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM StructView := do + let stx := -- for bootstrap compatibility, remove this after stage0 update + if stx.getNumArgs == 7 + then stx.setArgs #[stx[0], stx[1], .node .none ``Parser.Command.optDeclSig #[stx[2], stx[3]], stx[4], stx[5], stx[6]] + else stx checkValidInductiveModifier modifiers let isClass := stx[0].getKind == ``Parser.Command.classTk let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers let declId := stx[1] let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers addDeclarationRangesForBuiltin declName modifiers.stx stx - let binders := stx[2] - let (optType, exts) ← + let (binders, type?) := expandOptDeclSig stx[2] + let exts := stx[3] + let type? ← -- Compatibility mode for `structure S extends P : Type` syntax - if stx[3].isNone && !stx[4].isNone && !stx[4][0][2].isNone then - logWarningAt stx[4][0][2][0] "\ + if type?.isNone && !exts.isNone && !exts[0][2].isNone then + logWarningAt exts[0][2][0] "\ The syntax is now 'structure S : Type extends P' rather than 'structure S extends P : Type'.\n\n\ The purpose of this change is to accommodate 'structure S extends toP : P' syntax for naming parent projections." - pure (stx[4][0][2], stx[4]) + pure (some exts[0][2][0][1]) else - if !stx[4].isNone && !stx[4][0][2].isNone then - logErrorAt stx[4][0][2][0] "\ + if !exts.isNone && !exts[0][2].isNone then + logErrorAt exts[0][2][0] "\ Unexpected additional resulting type. \ The syntax is now 'structure S : Type extends P' rather than 'structure S extends P : Type'.\n\n\ The purpose of this change is to accommodate 'structure S extends toP : P' syntax for naming parent projections." - pure (stx[3], stx[4]) - let parents ← expandParents exts - let derivingClasses ← getOptDerivingClasses stx[6] - let type? := if optType.isNone then none else some optType[0][1] + pure type? + let parents ← expandParents exts + let derivingClasses ← getOptDerivingClasses stx[5] let ctor ← expandCtor stx modifiers declName let fields ← expandFields stx modifiers declName fields.forM fun field => do diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index d156bcf6be..bbe82a2887 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/src/Lean/Linter/MissingDocs.lean @@ -149,7 +149,7 @@ def checkDecl : SimpleHandler := fun stx => do if declModifiersPubNoDoc head then -- no doc string lintField rest[1][0] stx[1] "computed field" else if rest.getKind == ``«structure» then - unless rest[5][2].isNone do + unless rest[4][2].isNone do let redecls : Std.HashSet String.Pos := (← get).infoState.trees.foldl (init := {}) fun s tree => tree.foldInfo (init := s) fun _ info s => @@ -163,7 +163,7 @@ def checkDecl : SimpleHandler := fun stx => do if let some range := stx.getRange? then if redecls.contains range.start then return lintField parent stx "public field" - for stx in rest[5][2][0].getArgs do + for stx in rest[4][2][0].getArgs do let head := stx[0] if declModifiersPubNoDoc head then if stx.getKind == ``structSimpleBinder then diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index b5ed43cf92..ac495504c9 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -189,16 +189,14 @@ builtin_initialize builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ => stack.matches [`null, none, `null, ``Lean.Parser.Command.variable]) -/-- `structure Foo where unused : Nat` -/ +/-- +* `structure Foo (unused : Nat)` +* `inductive Foo (unused : Foo)` +-/ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ => - stack.matches [`null, none, `null, ``Lean.Parser.Command.structure]) - -/-- `inductive Foo where | unused : Foo` -/ -builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ => - stack.matches [`null, none, `null, none, ``Lean.Parser.Command.inductive] && - (stack[3]? |>.any fun (stx, pos) => - pos == 0 && - [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·))) + stack.matches [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] && + (stack[4]? |>.any fun (stx, _) => + [``Lean.Parser.Command.structure, ``Lean.Parser.Command.inductive].any (stx.isOfKind ·))) /-- * `structure Foo where foo (unused : Nat) : Nat` diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 20e769bb24..4d7a36ec41 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -236,7 +236,7 @@ def «structure» := leading_parser (structureTk <|> classTk) >> -- Note: no error recovery here due to clashing with the `class abbrev` syntax declId >> - ppIndent (many (ppSpace >> Term.bracketedBinder) >> Term.optType >> optional «extends») >> + ppIndent (optDeclSig >> optional «extends») >> optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields) >> optDeriving @[builtin_command_parser] def declaration := leading_parser diff --git a/tests/lean/1705.lean.expected.out b/tests/lean/1705.lean.expected.out index 3f3dd8b54d..934b40c0ae 100644 --- a/tests/lean/1705.lean.expected.out +++ b/tests/lean/1705.lean.expected.out @@ -1,5 +1,2 @@ -1705.lean:1:13-1:16: error: function expected at - T -term has type - ?m -1705.lean:1:18-1:19: error: unexpected identifier; expected command +1705.lean:1:22-1:23: error: type expected, got + (R : ?m) diff --git a/tests/lean/run/structBinderIdent.lean b/tests/lean/run/structBinderIdent.lean new file mode 100644 index 0000000000..9b2e7a89eb --- /dev/null +++ b/tests/lean/run/structBinderIdent.lean @@ -0,0 +1,104 @@ +/-! +# Testing structure declarations, including unbracketed parameters +-/ + +/-! +Structure with no parameters, no type, named constructor, and derived instance +-/ +structure NatPair where + mkPair :: + fst : Nat + snd : Nat + deriving Inhabited + +/-- info: NatPair : Type -/ +#guard_msgs in +#check NatPair + +/-- info: NatPair.mkPair (fst snd : Nat) : NatPair -/ +#guard_msgs in +#check NatPair.mkPair + +/-- info: instInhabitedNatPair -/ +#guard_msgs in +#synth Inhabited NatPair + +/-! +Structure with type and no parameters +-/ +structure Pointed : Type u where + α : Sort u + x : α + +/-- info: Pointed.{u} : Type u -/ +#guard_msgs in +#check Pointed + +/-- info: Pointed.mk.{u} (α : Sort u) (x : α) : Pointed -/ +#guard_msgs in +#check Pointed.mk + +/-! +Structure with unbracketed parameter, no type, and derived instance +-/ +structure Δ n where + val : Fin (n + 1) + deriving Inhabited + +/-- info: Δ (n : Nat) : Type -/ +#guard_msgs in +#check Δ + +/-- info: Δ.mk {n : Nat} (val : Fin (n + 1)) : Δ n -/ +#guard_msgs in +#check Δ.mk + +/-- info: @instInhabitedΔ -/ +#guard_msgs in +#synth ∀ n, Inhabited (Δ n) + +/-! +Structure with unbracketed parameters, type, and extends +-/ +structure Prod₃ α β γ : Type u extends toProd : α × β where + trd : (γ : Type u) + +/-- info: Prod₃.{u} (α β γ : Type u) : Type u -/ +#guard_msgs in +#check Prod₃ + +/-- info: Prod₃.mk.{u} {α β γ : Type u} (toProd : α × β) (trd : γ) : Prod₃ α β γ -/ +#guard_msgs in +#check Prod₃.mk + +/-- info: Prod₃.toProd.{u} {α β γ : Type u} (self : Prod₃ α β γ) : α × β -/ +#guard_msgs in +#check Prod₃.toProd + +/-! +Structure with no type and mixture of bracketed and unbracketed parameters +-/ +structure IsLt {n} (i : Fin n) j where + pf : i < j + +/-- info: IsLt {n : Nat} (i j : Fin n) : Prop -/ +#guard_msgs in +#check IsLt + +/-- info: IsLt.mk {n : Nat} {i j : Fin n} (pf : i < j) : IsLt i j -/ +#guard_msgs in +#check IsLt.mk + +/-! +Structure with type and mixture of bracketed and unbracketed parameters +-/ +structure Eval {n} (F : Fin n → Sort u) i : Sort (max 1 u) where + value : F i + +/-- info: Eval.{u} {n : Nat} (F : Fin n → Sort u) (i : Fin n) : Sort (max 1 u) -/ +#guard_msgs in +#check Eval + +/-- info: Eval.mk.{u} {n : Nat} {F : Fin n → Sort u} {i : Fin n} (value : F i) : Eval F i -/ +#guard_msgs in +#check Eval.mk