From d864afae919ee9454068587fe604eb07177f4228 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Aug 2021 20:20:21 -0700
Subject: [PATCH] feat: private fields

closes #418
---
 src/Lean/Elab/App.lean         | 19 ++++++++++++-------
 src/Lean/Elab/Structure.lean   |  2 --
 src/Lean/Modifiers.lean        |  7 ++++++-
 src/shell/CMakeLists.txt       |  8 ++++++++
 tests/leanpkg/prv/Prv.lean     |  5 +++++
 tests/leanpkg/prv/Prv/Foo.lean |  6 ++++++
 tests/leanpkg/prv/leanpkg.toml |  3 +++
 7 files changed, 40 insertions(+), 10 deletions(-)
 create mode 100644 tests/leanpkg/prv/Prv.lean
 create mode 100644 tests/leanpkg/prv/Prv/Foo.lean
 create mode 100644 tests/leanpkg/prv/leanpkg.toml

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 886e8990ed..920273258d 100644
--- a/src/Lean/Elab/App.lean
+++ b/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
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 176ca824fd..ffee34fa50 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/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"
 
 /-
 ```
diff --git a/src/Lean/Modifiers.lean b/src/Lean/Modifiers.lean
index 5d0ccd0d2b..c1d979cc99 100644
--- a/src/Lean/Modifiers.lean
+++ b/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
 
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index b3bdb5718a..a41814a05d 100644
--- a/src/shell/CMakeLists.txt
+++ b/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'")
diff --git a/tests/leanpkg/prv/Prv.lean b/tests/leanpkg/prv/Prv.lean
new file mode 100644
index 0000000000..7d4ffe3509
--- /dev/null
+++ b/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
diff --git a/tests/leanpkg/prv/Prv/Foo.lean b/tests/leanpkg/prv/Prv/Foo.lean
new file mode 100644
index 0000000000..5a386ecd88
--- /dev/null
+++ b/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
diff --git a/tests/leanpkg/prv/leanpkg.toml b/tests/leanpkg/prv/leanpkg.toml
new file mode 100644
index 0000000000..f9c5e825ef
--- /dev/null
+++ b/tests/leanpkg/prv/leanpkg.toml
@@ -0,0 +1,3 @@
+[package]
+name = "Prv"
+version = "0.1"