From 163b0a7a3fe44fd0a8ec7b05b6de3ea0e2a86e39 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Sep 2020 13:09:04 -0700
Subject: [PATCH] fix: `protected`

- `protected` outside of a namespace is an error.
- Fix `protected` in recursive definitions.

cc @Kha
---
 src/Lean/Elab/DeclModifiers.lean       | 18 ++++++++----
 tests/lean/protected.lean              | 40 ++++++++++++++++++++++++++
 tests/lean/protected.lean.expected.out | 29 +++++++++++++++++++
 3 files changed, 81 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index cce7bd237d..6dd03e6b6a 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -123,12 +123,18 @@ match visibility with
   checkNotAlreadyDeclared declName;
   pure declName
 
-def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (atomicName : Name) : m Name := do
-let name := (extractMacroScopes atomicName).name;
+def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) : m (Name × Name) := do
+let name := (extractMacroScopes shortName).name;
 unless (name.isAtomic || isFreshInstanceName name) $
-  throwError ("atomic identifier expected '" ++ atomicName ++ "'");
-let declName := currNamespace ++ atomicName;
-applyVisibility modifiers.visibility declName
+  throwError ("atomic identifier expected '" ++ shortName ++ "'");
+let declName := currNamespace ++ shortName;
+declName ← applyVisibility modifiers.visibility declName;
+match modifiers.visibility with
+| Visibility.protected =>
+  match currNamespace with
+  | Name.str _ s _ => pure (declName, mkNameSimple s ++ shortName)
+  | _ => throwError ("protected declarations must be in a namespace")
+| _ => pure (declName, shortName)
 
 /-
   `declId` is of the form
@@ -167,7 +173,7 @@ levelNames      ←
           pure (id :: levelNames))
       currLevelNames
   };
-declName ← withRef declId $ mkDeclName currNamespace modifiers shortName;
+(declName, shortName) ← withRef declId $ mkDeclName currNamespace modifiers shortName;
 pure { shortName := shortName, declName := declName, levelNames := levelNames }
 
 end Methods
diff --git a/tests/lean/protected.lean b/tests/lean/protected.lean
index 20692cca8d..4765e3d389 100644
--- a/tests/lean/protected.lean
+++ b/tests/lean/protected.lean
@@ -21,3 +21,43 @@ open Bla
 open Bla.Foo
 #check y -- error unknown identifier `y`
 #check z
+
+protected def x := 0  -- Error
+
+protected partial def Foo.f (x : Nat) :=
+if x > 0 then f (x-1) * 2 else 1 -- Error
+
+protected partial def Bla.f (x : Nat) :=
+if x > 0 then Bla.f (x-1) * 2 else 1
+
+#eval Bla.f 3
+
+namespace Foo
+
+protected partial def g (x : Nat) :=
+if x > 0 then g (x-1) * 2 else 1 -- error
+
+end Foo
+
+namespace Bla
+
+protected partial def g (x : Nat) :=
+if x > 0 then Bla.g (x-1) * 2 else 1
+
+#eval g 3 -- error
+
+#eval Bla.g 3
+
+end Bla
+
+
+def S (σ : Type) (m : Type → Type) (α : Type) :=
+σ → m (α × σ)
+
+namespace S
+variables {σ : Type} {m : Type → Type} [Monad m] {α : Type}
+
+protected def pure (a : α) : S σ m α :=
+fun s => pure (a, s) -- This `pure` is the top-level one. The `pure` being defined here is called `S.pure`.
+
+end S
diff --git a/tests/lean/protected.lean.expected.out b/tests/lean/protected.lean.expected.out
index c93d96ee3c..a206a70378 100644
--- a/tests/lean/protected.lean.expected.out
+++ b/tests/lean/protected.lean.expected.out
@@ -5,3 +5,32 @@ Bla.Foo.y : Nat
 protected.lean:22:7: error: unknown identifier 'y'
 (sorryAx ?m.67) : ?m.67
 Bla.Foo.z : Nat
+protected.lean:25:14: error: protected declarations must be in a namespace
+protected.lean:28:14: error: unknown identifier 'f'
+with resulting expansion
+  HasMul.mul._@._internal._hyg.0 f (x-1) 2 
+while expanding
+  f (x-1) * 2 
+while expanding
+  if x > 0 then f (x-1) * 2 else 1 
+while expanding
+  protected partial def Foo.f (x : Nat) :=
+  if x > 0 then f (x-1) * 2 else 1 
+8
+protected.lean:38:14: error: unknown identifier 'g'
+with resulting expansion
+  HasMul.mul._@._internal._hyg.0 g (x-1) 2 
+while expanding
+  g (x-1) * 2 
+while expanding
+  if x > 0 then g (x-1) * 2 else 1 
+protected.lean:47:6: error: unknown identifier 'g'
+protected.lean:47:0: error: application type mismatch
+  Lean.runEval (sorryAx ?m.781)
+argument
+  (sorryAx ?m.781)
+has type
+  ?m.781
+but is expected to have type
+  ?m.783
+8