From 7322345768e59dd89a85c9e6a635372972990f06 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Apr 2020 16:13:45 -0700 Subject: [PATCH] fix: private names @Kha I tried to fix a few issues with private names. The new test tries to cover them. If you have more, please create an issue. 1- Scoping. A private declaration should shadow one in a previous scope. 2- We should not be able to define the same `private` in the same module more than once. ``` private def x := 10 private def x := "hello" -- should produce error here ``` 3- Dot-notation should work with private declarations in the module where they were defined. 4- The following should work ``` namespace N private def x := 10 end N #check N.x ``` 5- The following should **not** work ``` def y := 10 private def y := "hello" -- produce error private def z := 10 def z := "hello" -- produce error ``` BTW, I am happy to change this behavior. I just mimicked C's behavior for `static`. It is not clear whether the following should work or not. ``` namespace N private def b := 10 end N open N #check b ``` --- src/Init/Lean/Elab/App.lean | 9 +++- src/Init/Lean/Elab/DeclModifiers.lean | 16 +++++-- src/Init/Lean/Elab/ResolveName.lean | 19 ++++++-- src/Init/Lean/Modifiers.lean | 11 +++-- tests/lean/private.lean | 68 +++++++++++++++++++++++++++ tests/lean/private.lean.expected.out | 13 +++++ 6 files changed, 121 insertions(+), 15 deletions(-) create mode 100644 tests/lean/private.lean create mode 100644 tests/lean/private.lean.expected.out diff --git a/src/Init/Lean/Elab/App.lean b/src/Init/Lean/Elab/App.lean index 577dd11eb6..4d744ff684 100644 --- a/src/Init/Lean/Elab/App.lean +++ b/src/Init/Lean/Elab/App.lean @@ -321,8 +321,13 @@ match eType.getAppFn, lval with let searchEnv (fullName : Name) : TermElabM LValResolution := do { match env.find? fullName with | some _ => pure $ LValResolution.const structName fullName - | none => throwLValError ref e eType $ - "invalid field notation, '" ++ fieldName ++ "' is not a valid \"field\" because environment does not contain '" ++ fullName ++ "'" + | none => + let fullNamePrv := mkPrivateName env fullName; + match env.find? fullNamePrv with + | some _ => pure $ LValResolution.const structName fullNamePrv + | none => + throwLValError ref e eType $ + "invalid field notation, '" ++ fieldName ++ "' is not a valid \"field\" because environment does not contain '" ++ fullName ++ "'" }; -- search local context first, then environment let searchCtx : Unit → TermElabM LValResolution := fun _ => do { diff --git a/src/Init/Lean/Elab/DeclModifiers.lean b/src/Init/Lean/Elab/DeclModifiers.lean index 525e413394..6f2c8a021c 100644 --- a/src/Init/Lean/Elab/DeclModifiers.lean +++ b/src/Init/Lean/Elab/DeclModifiers.lean @@ -110,16 +110,22 @@ let declName := currNamespace ++ atomicName; match modifiers.visibility with | Visibility.private => do env ← getEnv; - let (env, declName) := mkPrivateName env declName; - setEnv env; - -- TODO: alias? - pure declName + pure $ mkPrivateName env declName | _ => pure declName def checkNotAlreadyDeclared (ref : Syntax) (declName : Name) : CommandElabM Unit := do env ← getEnv; when (env.contains declName) $ - throwError ref ("'" ++ declName ++ "' has already been declared") + match privateToUserName? declName with + | none => throwError ref ("'" ++ declName ++ "' has already been declared") + | some declName => throwError ref ("private declaration '" ++ declName ++ "' has already been declared"); +when (env.contains (mkPrivateName env declName)) $ + throwError ref ("a private declaration '" ++ declName ++ "' has already been declared"); +match privateToUserName? declName with +| none => pure () +| some declName => + when (env.contains declName) $ + throwError ref ("a non-private declaration '" ++ declName ++ "' has already been declared") def applyAttributes (ref : Syntax) (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : CommandElabM Unit := attrs.forM $ fun attr => do diff --git a/src/Init/Lean/Elab/ResolveName.lean b/src/Init/Lean/Elab/ResolveName.lean index e90bf21bee..9408588fe8 100644 --- a/src/Init/Lean/Elab/ResolveName.lean +++ b/src/Init/Lean/Elab/ResolveName.lean @@ -34,10 +34,15 @@ n.replacePrefix rootNamespace Name.anonymous /- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/ private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name := -let resolvedId := ns ++ id; -let resolvedIds := getAliases env resolvedId; +let resolvedId := ns ++ id; +let resolvedIds := getAliases env resolvedId; if env.contains resolvedId && (!id.isAtomic || !isProtected env resolvedId) then resolvedId :: resolvedIds -else resolvedIds +else + -- Check whether environment contains the private version. That is, `_private..ns.id`. + let resolvedIdPrv := mkPrivateName env resolvedId; + if env.contains resolvedIdPrv then resolvedIdPrv :: resolvedIds + else resolvedIds + /- Check surrounding namespaces -/ private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name @@ -52,7 +57,13 @@ private def resolveExact (env : Environment) (id : Name) : Option Name := if id.isAtomic then none else let resolvedId := id.replacePrefix rootNamespace Name.anonymous; - if env.contains resolvedId then some resolvedId else none + if env.contains resolvedId then some resolvedId + else + -- We also allow `_root` when accessing private declarations. + -- If we change our minds, we should just replace `resolvedId` with `id` + let resolvedIdPrv := mkPrivateName env resolvedId; + if env.contains resolvedIdPrv then some resolvedIdPrv + else none /- Check open namespaces -/ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → List Name → List Name diff --git a/src/Init/Lean/Modifiers.lean b/src/Init/Lean/Modifiers.lean index 46ec9156cd..c370b0154a 100644 --- a/src/Init/Lean/Modifiers.lean +++ b/src/Init/Lean/Modifiers.lean @@ -43,17 +43,20 @@ constant privateExt : EnvExtension Nat := arbitrary _ def privateHeader : Name := `_private @[export lean_mk_private_prefix] -def mkPrivatePrefix (env : Environment) : Environment × Name := +def mkUniquePrivatePrefix (env : Environment) : Environment × Name := let idx := privateExt.getState env; let p := mkNameNum (privateHeader ++ env.mainModule) idx; let env := privateExt.setState env (idx+1); (env, p) @[export lean_mk_private_name] -def mkPrivateName (env : Environment) (n : Name) : Environment × Name := -let (env, p) := mkPrivatePrefix env; +def mkUniquePrivateName (env : Environment) (n : Name) : Environment × Name := +let (env, p) := mkUniquePrivatePrefix env; (env, p ++ n) +def mkPrivateName (env : Environment) (n : Name) : Name := +mkNameNum (privateHeader ++ env.mainModule) 0 ++ n + def isPrivateName : Name → Bool | n@(Name.str p _ _) => n == privateHeader || isPrivateName p | Name.num p _ _ => isPrivateName p @@ -68,7 +71,7 @@ private def privateToUserNameAux : Name → Name | _ => Name.anonymous @[export lean_private_to_user_name] -def privateToUserName (n : Name) : Option Name := +def privateToUserName? (n : Name) : Option Name := if isPrivateName n then privateToUserNameAux n else none diff --git a/tests/lean/private.lean b/tests/lean/private.lean new file mode 100644 index 0000000000..f12a0f88df --- /dev/null +++ b/tests/lean/private.lean @@ -0,0 +1,68 @@ +new_frontend + +-- Issue 1 +def foo := 10 + +def f (x : Nat) := x + x + +namespace Bla + +private def foo := "hello" + +#check foo == "world" -- `foo` resolves to private `Bla.foo` + +private def foo : Float := 1.0 -- should produce error like in other programming languages + +end Bla + +#check foo == 0 + +#check Bla.foo + +-- Issue 2 +namespace Boo + +def boo := 100 + +namespace Bla + +private def boo := "hello" + +#check boo == "world" -- resolving to `Boo.Bla.boo` as expected +#check boo ++ "world" -- should work + +end Bla + +#check Bla.boo == "world" +#check boo == 100 + +end Boo + +#check Boo.Bla.boo == "world" +#check Boo.boo == 100 + +/- +Should the following work? +``` + namespace N + private def b := 10 + end N + open N + #check b +``` +-/ + +-- Issue 3 +private def Nat.mul10 (x : Nat) := x * 10 +def x := 10 + +#check x.mul10 -- dot-notation should work with local private declarations + + +-- Issue 4 + +def y := 10 +private def y := "hello" -- produce error + +private def z := 10 +def z := "hello" -- produce error diff --git a/tests/lean/private.lean.expected.out b/tests/lean/private.lean.expected.out new file mode 100644 index 0000000000..51b52b82c4 --- /dev/null +++ b/tests/lean/private.lean.expected.out @@ -0,0 +1,13 @@ +Bla.foo=="world" : Bool +private.lean:14:8: error: private declaration 'Bla.foo' has already been declared +foo==0 : Bool +Bla.foo : String +Boo.Bla.boo=="world" : Bool +Boo.Bla.boo++"world" : String +Boo.Bla.boo=="world" : Bool +Boo.boo==100 : Bool +Boo.Bla.boo=="world" : Bool +Boo.boo==100 : Bool +Nat.mul10 x : Nat +private.lean:65:8: error: a non-private declaration 'y' has already been declared +private.lean:68:0: error: a private declaration 'z' has already been declared