feat: private fields

closes #418

src/Lean/Elab/App.lean

@@ -683,14 +683,19 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       loop f lvals
     | LValResolution.projFn baseStructName structName fieldName =>
       let f ← mkBaseProjections baseStructName structName f
-      let projFn ← mkConst (baseStructName ++ fieldName)
-      addTermInfo lval.getRef projFn
-      if lvals.isEmpty then
-        let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
-        elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
+      if let some info := getFieldInfo? (← getEnv) baseStructName fieldName then
+        if isPrivateNameFromImportedModule (← getEnv) info.projFn then
+          throwError "field '{fieldName}' from structure '{structName}' is private"
+        let projFn ← mkConst info.projFn
+        addTermInfo lval.getRef projFn
+        if lvals.isEmpty then
+          let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
+          elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
+        else
+          let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
+          loop f lvals
       else
-        let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
-        loop f lvals
+        unreachable!
     | LValResolution.const baseStructName structName constName =>
       let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
       let projFn ← mkConst constName

src/Lean/Elab/Structure.lean

@@ -138,8 +138,6 @@ def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
     throwError "invalid use of 'unsafe' in field declaration"
   if modifiers.attrs.size != 0 then
     throwError "invalid use of attributes in field declaration"
-  if modifiers.isPrivate then
-    throwError "private fields are not supported yet"
 
 /-
 ```

src/Lean/Modifiers.lean

@@ -51,12 +51,17 @@ def privateToUserName? (n : Name) : Option Name :=
   if isPrivateName n then privateToUserNameAux n
   else none
 
+def isPrivateNameFromImportedModule (env : Environment) (n : Name) : Bool :=
+  match privateToUserName? n with
+  | some userName => mkPrivateName env userName != n
+  | _ => false
+
 private def privatePrefixAux : Name → Name
   | Name.str p _ _ => privatePrefixAux p
   | n              => n
 
 @[export lean_private_prefix]
-def privatePrefix (n : Name) : Option Name :=
+def privatePrefix? (n : Name) : Option Name :=
   if isPrivateName n then privatePrefixAux n
   else none
 

src/shell/CMakeLists.txt

@@ -195,3 +195,11 @@ add_test(NAME leanpkgtest_user_attr
            export PATH=${LEAN_BIN}:$PATH
            find . -name '*.olean' -delete
            leanpkg build")
+
+add_test(NAME leanpkgtest_prv
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/prv"
+         COMMAND bash -c "
+           set -eu
+           export PATH=${LEAN_BIN}:$PATH
+           find . -name '*.olean' -delete
+           leanpkg build 2>&1 | grep 'error: field.*private'")

tests/leanpkg/prv/Prv.lean

@@ -0,0 +1,5 @@
+import Prv.Foo
+
+#check { name := "leo", val := 15 : Foo }
+#check { name := "leo", val := 15 : Foo }.name
+#check { name := "leo", val := 15 : Foo }.val -- Error

tests/leanpkg/prv/Prv/Foo.lean

@@ -0,0 +1,6 @@
+structure Foo where
+  private val : Nat
+  name : String
+
+#check { name := "leo", val := 15 : Foo }
+#check { name := "leo", val := 15 : Foo }.val

tests/leanpkg/prv/leanpkg.toml

@@ -0,0 +1,3 @@
+[package]
+name = "Prv"
+version = "0.1"