From b5927a10240fcc02467d9b0a4bec8c811fc62b67 Mon Sep 17 00:00:00 2001
From: joneugster <eugster.jon@gmail.com>
Date: Fri, 20 Oct 2023 21:59:47 +0200
Subject: [PATCH] Fix assumption display in inventory and editor mode #84

---
 client/src/components/infoview/main.tsx | 23 +++++++++++----
 client/src/components/level.css         | 14 +++++++++
 server/GameServer/Commands.lean         | 38 +++++++------------------
 3 files changed, 42 insertions(+), 33 deletions(-)

diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index 4b54452..36189e6 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -44,7 +44,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize })
   const { typewriterMode } = React.useContext(InputModeContext)
   return <>
     <div className={typewriterMode ? 'hidden' : ''}>
-      <ExerciseStatement data={level} />
+      <ExerciseStatement data={level} showLeanStatement={true} />
       <div ref={codeviewRef} className={'codeview'}></div>
     </div>
     {ec ?
@@ -131,12 +131,23 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
  * - Theorem xyz: description
  * - Theorem xyz
  * - Exercises: description
+ *
+ * If `showLeanStatement` is true, it will additionally display the lean code.
  */
-function ExerciseStatement({ data }) {
-  if (!data?.descrText) { return <></> }
-  return <div className="exercise-statement"><Markdown>
-    {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}`}
-  </Markdown></div>
+function ExerciseStatement({ data, showLeanStatement = false }) {
+  if (!(data?.descrText || data?.descrFormat)) { return <></> }
+  return <>
+    <div className="exercise-statement">
+      {data?.descrText &&
+        <Markdown>
+          {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : data?.descrText && "**Exercise**: ") + data?.descrText}
+        </Markdown>
+      }
+      {data?.descrFormat && showLeanStatement &&
+        <p><code className="lean-code">{data?.descrFormat}</code></p>
+      }
+    </div>
+  </>
 }
 
 // TODO: This is only used in `EditorInterface`
diff --git a/client/src/components/level.css b/client/src/components/level.css
index 923105d..faa2c0d 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -41,6 +41,20 @@
   padding-right: .5em;
 }
 
+.exercise-statement {
+  padding-top: 1em;
+  padding-bottom: 1em;
+}
+
+.exercise-statement p {
+  margin: 0;
+}
+
+.exercise-statement .lean-code {
+  color: rgba(0, 32, 90, 0.87);
+  font-size: 12px; /* TODO: is the monaco font-size hardcoded? */
+}
+
 .conclusion {
   padding: 1em;
 }
diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 7d4165e..69ad5e9 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -255,31 +255,17 @@ elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
 
 /-! ## Add inventory items -/
 
--- namespace Lean.PrettyPrinter
--- def ppSignature' (c : Name) : MetaM String := do
---   let decl ← getConstInfo c
---   let e := .const c (decl.levelParams.map mkLevelParam)
---   let (stx, _) ← delabCore e (delab := Delaborator.delabConstWithSignature)
---   let f ← ppTerm stx
---   return toString f
--- end Lean.PrettyPrinter
-
 def getStatement (name : Name) : CommandElabM MessageData := do
-  -- let c := name.getId
-
-  let decl ← getConstInfo name
-  -- -- TODO: How to go between CommandElabM and MetaM
-
-  -- addCompletionInfo <| .id name c (danglingDot := false) {} none
   return ← addMessageContextPartial (.ofPPFormat { pp := fun
-    | some ctx => ctx.runMetaM <| ppExpr decl.type
-    -- PrettyPrinter.ppSignature' c
-    -- PrettyPrinter.ppSignature c
+    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
     | none     => return "that's a bug." })
 
 -- Note: We use `String` because we can't send `MessageData` as json, but
 -- `MessageData` might be better for interactive highlighting.
-/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`. -/
+/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
+
+Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
+`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
 def getStatementString (name : Name) : CommandElabM String := do
   try
     return ← (← getStatement name).toString
@@ -489,13 +475,11 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
   -- the namespace?
   let currNamespace ← getCurrNamespace
 
-  let st ← match statementName with
-  | some name => getStatementString <| currNamespace ++ name.getId
-  | none =>  getStatementString <| currNamespace ++ (defaultDeclName).getId
-
-  let head := match statementName with
-  | some name => Format.join ["theorem ", (currNamespace ++ name.getId).toString]
-  | none => "example"
+  -- Format theorem statement for displaying
+  let sigString := sig.raw.reprint.getD ""
+  let descrFormat : String := match statementName with
+  | some name =>  s!"theorem {name.getId} {sigString} := by"
+  | none => s!"example {sigString} := by"
 
   modifyCurLevel fun level => pure { level with
     module := env.header.mainModule
@@ -505,7 +489,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     statementName := match statementName with
     | none => default
     | some name => currNamespace ++ name.getId
-    descrFormat := (Format.join [head, " ", st, " := by"]).pretty 10
+    descrFormat := descrFormat
     hints := hints
     tactics := {level.tactics with used := usedInventory.tactics.toArray}
     definitions := {level.definitions with used := usedInventory.definitions.toArray}