fix: copied 11940 fix for structure command (#12680)
This PR fixes an issue where `mutual public structure` would have a private constructor. The fix copies the fix from #11940. Closes #10067. Also recloses duplicate issue #11116 (its test case is added to the test suite).
This commit is contained in:
Kyle Miller
GitHub
parent
c86f82161a
commit
bd0c6a42c8
2 changed files with 108 additions and 52 deletions
|
|
@ -416,55 +416,59 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str
|
|||
let modifiers := if isClass then modifiers.addFirstAttr { name := `class } else modifiers
|
||||
let declId := stx[1]
|
||||
let ⟨name, declName, levelNames, docString?⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
|
||||
if modifiers.isMeta then
|
||||
modifyEnv (markMeta · declName)
|
||||
addDeclarationRangesForBuiltin declName modifiers.stx stx
|
||||
let (binders, type?) := expandOptDeclSig stx[2]
|
||||
let exts := stx[3]
|
||||
let type? ←
|
||||
-- Compatibility mode for `structure S extends P : Type` syntax
|
||||
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`"
|
||||
++ .note "The purpose of this change is to accommodate `structure S extends toP : P` syntax for naming parent projections."
|
||||
pure (some exts[0][2][0][1])
|
||||
else
|
||||
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`."
|
||||
++ .note "The purpose of this change is to accommodate `structure S extends toP : P` syntax for naming parent projections."
|
||||
pure type?
|
||||
let parents ← expandParents exts
|
||||
let derivingClasses ← getOptDerivingClasses stx[5]
|
||||
let fields ← expandFields stx modifiers declName
|
||||
-- Private fields imply a private constructor (in the module system only, for back-compat)
|
||||
let ctor ← expandCtor
|
||||
(forcePrivate := (← getEnv).header.isModule && fields.any (·.modifiers.isPrivate))
|
||||
stx modifiers declName
|
||||
fields.forM fun field => do
|
||||
if field.declName == ctor.declName then
|
||||
throwErrorAt field.ref "Invalid field name `{field.name}`: This is the name of the structure constructor"
|
||||
addDeclarationRangesFromSyntax field.declName field.ref
|
||||
return {
|
||||
ref := stx
|
||||
declId
|
||||
modifiers
|
||||
isClass
|
||||
shortDeclName := name
|
||||
declName
|
||||
levelNames
|
||||
binders
|
||||
type?
|
||||
allowIndices := false
|
||||
allowSortPolymorphism := false
|
||||
ctors := #[ctor]
|
||||
parents
|
||||
fields
|
||||
computedFields := #[]
|
||||
derivingClasses
|
||||
docString?
|
||||
}
|
||||
-- In the case of mutual inductives, this is the earliests point where we can establish the
|
||||
-- correct scope for each individual inductive declaration (used e.g. to infer ctor visibility
|
||||
-- below), so let's do that now.
|
||||
withExporting (isExporting := !isPrivateName declName) do
|
||||
if modifiers.isMeta then
|
||||
modifyEnv (markMeta · declName)
|
||||
addDeclarationRangesForBuiltin declName modifiers.stx stx
|
||||
let (binders, type?) := expandOptDeclSig stx[2]
|
||||
let exts := stx[3]
|
||||
let type? ←
|
||||
-- Compatibility mode for `structure S extends P : Type` syntax
|
||||
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`"
|
||||
++ .note "The purpose of this change is to accommodate `structure S extends toP : P` syntax for naming parent projections."
|
||||
pure (some exts[0][2][0][1])
|
||||
else
|
||||
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`."
|
||||
++ .note "The purpose of this change is to accommodate `structure S extends toP : P` syntax for naming parent projections."
|
||||
pure type?
|
||||
let parents ← expandParents exts
|
||||
let derivingClasses ← getOptDerivingClasses stx[5]
|
||||
let fields ← expandFields stx modifiers declName
|
||||
-- Private fields imply a private constructor (in the module system only, for back-compat)
|
||||
let ctor ← expandCtor
|
||||
(forcePrivate := (← getEnv).header.isModule && fields.any (·.modifiers.isPrivate))
|
||||
stx modifiers declName
|
||||
fields.forM fun field => do
|
||||
if field.declName == ctor.declName then
|
||||
throwErrorAt field.ref "Invalid field name `{field.name}`: This is the name of the structure constructor"
|
||||
addDeclarationRangesFromSyntax field.declName field.ref
|
||||
return {
|
||||
ref := stx
|
||||
declId
|
||||
modifiers
|
||||
isClass
|
||||
shortDeclName := name
|
||||
declName
|
||||
levelNames
|
||||
binders
|
||||
type?
|
||||
allowIndices := false
|
||||
allowSortPolymorphism := false
|
||||
ctors := #[ctor]
|
||||
parents
|
||||
fields
|
||||
computedFields := #[]
|
||||
derivingClasses
|
||||
docString?
|
||||
}
|
||||
|
||||
|
||||
/-!
|
||||
|
|
@ -1527,9 +1531,10 @@ def elabStructureCommand : InductiveElabDescr where
|
|||
addProjections params r fieldInfos
|
||||
registerStructure view.declName fieldInfos
|
||||
runStructElabM (init := state) do
|
||||
withOptions (warn.sorry.set · false) do
|
||||
mkFlatCtor levelParams params view.declName replaceIndFVars
|
||||
addDefaults levelParams params replaceIndFVars
|
||||
withExporting (isExporting := !isPrivateName view.ctor.declName) do
|
||||
withOptions (warn.sorry.set · false) do
|
||||
mkFlatCtor levelParams params view.declName replaceIndFVars
|
||||
addDefaults levelParams params replaceIndFVars
|
||||
let parentInfos ← withLCtx lctx localInsts <| runStructElabM (init := state) do
|
||||
withOptions (warn.sorry.set · false) do
|
||||
mkRemainingProjections levelParams params view
|
||||
|
|
|
|||
51
tests/lean/run/10067.lean
Normal file
51
tests/lean/run/10067.lean
Normal file
|
|
@ -0,0 +1,51 @@
|
|||
module
|
||||
|
||||
/-!
|
||||
# `mutual public structure`
|
||||
-/
|
||||
|
||||
namespace Issue10067
|
||||
|
||||
mutual
|
||||
public structure PubStruct where
|
||||
val : Nat
|
||||
i? : Option PubInduct
|
||||
|
||||
public inductive PubInduct
|
||||
| ofStruct (s : PubStruct)
|
||||
| alt (val : Nat)
|
||||
end
|
||||
|
||||
/-! Used to be "Unknown constant `PubInduct.alt`" -/
|
||||
@[expose] public def mkPubInduct (val : Nat) : PubInduct :=
|
||||
PubInduct.alt val
|
||||
|
||||
def mkPrivatePubInduct (val : Nat) : PubInduct :=
|
||||
PubInduct.alt val
|
||||
|
||||
/-! Used to be "invalid {...} notation, constructor for `PubStruct` is marked as private" -/
|
||||
@[expose] public def mkPubStruct (val : Nat) : PubStruct :=
|
||||
{val, i? := none}
|
||||
|
||||
/-! Used to be "Field `val` from structure `PubStruct` is private" -/
|
||||
@[expose] public def pubStructVal (s : PubStruct) : Nat :=
|
||||
s.val
|
||||
|
||||
end Issue10067
|
||||
|
||||
/-! Duplicate issue. -/
|
||||
namespace Issue11116
|
||||
|
||||
public structure A where
|
||||
|
||||
mutual
|
||||
public structure B where
|
||||
end
|
||||
|
||||
@[expose] public def testA1 := A.mk
|
||||
@[expose] public def testA2 : A := {}
|
||||
-- Used to be "unknown constant B.mk"
|
||||
@[expose] public def testB1 := B.mk
|
||||
@[expose] public def testB2 : B := {}
|
||||
|
||||
end Issue11116
|
||||
Loading…
Add table
Reference in a new issue