From 73ca0f4d958e7c6f28940c05377215b83c571ca0 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 26 May 2023 17:10:10 +0200
Subject: [PATCH] fix Statement inside a namespace

---
 server/GameServer/Commands.lean | 21 ++++++++++++++-------
 server/test/test_statement.lean | 11 +++++++++++
 2 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 2a7d02b..455b8a8 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -302,11 +302,14 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
   match statementName with
   | some name =>
     let env ← getEnv
-    if env.contains name.getId then
-      let origType := (env.constants.map₁.find! name.getId).type
+
+    let fullName := (← getCurrNamespace) ++ name.getId
+
+    if env.contains fullName then
+      let origType := (env.constants.map₁.find! fullName).type
       -- TODO: Check if `origType` agrees with `sig` and output `logInfo` instead of `logWarning`
       -- in that case.
-      logWarningAt name (m!"Environment already contains {name.getId}! Only the existing " ++
+      logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
       m!"statement will be available in later levels:\n\n{origType}")
       let thmStatement ← `(theorem $defaultDeclName $sig $val)
       elabCommand thmStatement
@@ -354,12 +357,16 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
   let scope ← getScope
   let env ← getEnv
 
+  -- TODO: Is this desired or would it be better to get `elabCommand` above to ignore
+  -- the namespace?
+  let currNamespace ← getCurrNamespace
+
   let st ← match statementName with
-  | some name => getStatementString name.getId
-  | none =>  getStatementString defaultDeclName.getId -- TODO: We dont want the internal lemma name here
+  | some name => getStatementString <| currNamespace ++ name.getId
+  | none =>  getStatementString <| currNamespace ++ (defaultDeclName).getId
 
   let head := match statementName with
-  | some name => Format.join ["theorem ", name.getId.toString]
+  | some name => Format.join ["theorem ", (currNamespace ++ name.getId).toString]
   | none => "example"
 
   modifyCurLevel fun level => pure { level with
@@ -369,7 +376,7 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
     descrText := descr
     statementName := match statementName with
     | none => default
-    | some name => name.getId
+    | some name => currNamespace ++ name.getId
     descrFormat := (Format.join [head, " ", st, " := by"]).pretty 10
     hints := hints }
 
diff --git a/server/test/test_statement.lean b/server/test/test_statement.lean
index 2a535e4..eb63b7a 100644
--- a/server/test/test_statement.lean
+++ b/server/test/test_statement.lean
@@ -14,6 +14,17 @@ Statement foo.bar "some text" : 5 ≤ 7 := by
 NewLemma foo.baz
 DisabledTactic tauto
 
+
+/- Namespace -/
+
+-- test that the command also works inside a namespace
+namespace myNamespace
+
+Statement anotherStatement "test" (n : Nat) : n + 0 = n := by
+  rfl
+
+end myNamespace
+
 /- Other tests -/
 
 LemmaDoc add_zero as "add_zero" in "Nat" "(nothing)"