From db53d0aa7ea1ee974afa7c0bbb80f4183c167328 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jul 2020 15:09:05 -0700 Subject: [PATCH] fix: validate visibility modifiers --- src/Lean/Elab/Structure.lean | 32 +++++++++++++++++----------- tests/lean/struct1.lean | 15 +++++++++++++ tests/lean/struct1.lean.expected.out | 5 +++++ 3 files changed, 40 insertions(+), 12 deletions(-) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index c46cd936f9..cd02431c74 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -73,19 +73,23 @@ The structore constructor syntax is parser! try (declModifiers >> ident >> optional inferMod >> " :: ") ``` -/ -private def expandCtor (structStx : Syntax) (structDeclName : Name) : CommandElabM StructCtorView := +private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM StructCtorView := let optCtor := structStx.getArg 6; if optCtor.isNone then pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName := structDeclName ++ defaultCtorName } else do let ctor := optCtor.getArg 0; - modifiers ← elabModifiers (ctor.getArg 0); - checkValidCtorModifier ctor modifiers; + ctorModifiers ← elabModifiers (ctor.getArg 0); + checkValidCtorModifier ctor ctorModifiers; + when (ctorModifiers.isPrivate && structModifiers.isPrivate) $ + throwError ctor "invalid 'private' constructor in a 'private' structure"; + when (ctorModifiers.isProtected && structModifiers.isPrivate) $ + throwError ctor "invalid 'protected' constructor in a 'private' structure"; let inferMod := !(ctor.getArg 2).isNone; let name := ctor.getIdAt 1; let declName := structDeclName ++ name; - declName ← applyVisibility ctor modifiers.visibility declName; - pure { ref := ctor, name := name, modifiers := modifiers, inferMod := inferMod, declName := declName } + declName ← applyVisibility ctor ctorModifiers.visibility declName; + pure { ref := ctor, name := name, modifiers := ctorModifiers, inferMod := inferMod, declName := declName } def checkValidFieldModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do when modifiers.isNoncomputable $ @@ -108,7 +112,7 @@ def structInstBinder := parser! try (declModifiers >> "[") >> many1 ident >> def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder) ``` -/ -private def expandFields (structStx : Syntax) (structDeclName : Name) : CommandElabM (Array StructFieldView) := +private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) := let fieldBinders := ((structStx.getArg 7).getArg 0).getArgs; fieldBinders.foldlM (fun (views : Array StructFieldView) fieldBinder => do @@ -118,8 +122,12 @@ fieldBinders.foldlM else if k == `Lean.Parser.Command.structImplicitBinder then pure BinderInfo.implicit else if k == `Lean.Parser.Command.structInstBinder then pure BinderInfo.instImplicit else throwError fieldBinder "unexpected kind of structure field"; - modifiers ← elabModifiers (fieldBinder.getArg 0); - checkValidFieldModifier fieldBinder modifiers; + fieldModifiers ← elabModifiers (fieldBinder.getArg 0); + checkValidFieldModifier fieldBinder fieldModifiers; + when (fieldModifiers.isPrivate && structModifiers.isPrivate) $ + throwError fieldBinder "invalid 'private' field in a 'private' structure"; + when (fieldModifiers.isProtected && structModifiers.isPrivate) $ + throwError fieldBinder "invalid 'protected' field in a 'private' structure"; let inferMod := !(fieldBinder.getArg 3).isNone; let (binders, type?) := if binfo == BinderInfo.default then @@ -142,10 +150,10 @@ fieldBinders.foldlM when (isInternalSubobjectFieldName name) $ throwError ident ("invalid field name '" ++ name ++ "', identifiers starting with '_' are reserved to the system"); let declName := structDeclName ++ name; - declName ← applyVisibility ident modifiers.visibility declName; + declName ← applyVisibility ident fieldModifiers.visibility declName; pure $ views.push { ref := ident, - modifiers := modifiers, + modifiers := fieldModifiers, binderInfo := binfo, inferMod := inferMod, declName := declName, @@ -422,8 +430,8 @@ scopeLevelNames ← getLevelNames; withDeclId declId $ fun name => do declName ← mkDeclName declId modifiers name; allUserLevelNames ← getLevelNames; - ctor ← expandCtor stx declName; - fields ← expandFields stx declName; + ctor ← expandCtor stx modifiers declName; + fields ← expandFields stx modifiers declName; r ← runTermElabM declName $ fun scopeVars => Term.elabBinders params $ fun params => elabStructureView { ref := stx, modifiers := modifiers, diff --git a/tests/lean/struct1.lean b/tests/lean/struct1.lean index ba6ec0ea98..069ec58a9d 100644 --- a/tests/lean/struct1.lean +++ b/tests/lean/struct1.lean @@ -39,3 +39,18 @@ structure S extends A Nat := structure S := (x : Nat := true) -- error type mismatch + +private structure S := +private mk :: (x : Nat) + +private structure S := +protected mk :: (x : Nat) + +private structure S := +protected (x : Nat) + +private structure S := +mk2 :: (x : Nat) + +#check S +#check S.mk2 diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out index d765df5cbe..a49ab6694f 100644 --- a/tests/lean/struct1.lean.expected.out +++ b/tests/lean/struct1.lean.expected.out @@ -23,3 +23,8 @@ but it is expected to have type Nat failed to synthesize instance CoeT Bool true Nat +struct1.lean:44:0: error: invalid 'private' constructor in a 'private' structure +struct1.lean:47:0: error: invalid 'protected' constructor in a 'private' structure +struct1.lean:50:0: error: invalid 'protected' field in a 'private' structure +S : Type +S.mk2 : Nat → S