From 27c661f08f754c08162d36000ebe7cec2f16ccd9 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 25 Mar 2024 21:15:35 +0100
Subject: [PATCH] modify generated statement in inventory

---
 server/GameServer/Commands.lean              |  2 +
 server/GameServer/Helpers.lean               | 23 +----
 server/GameServer/Helpers/PrettyPrinter.lean | 96 ++++++++++++++++++++
 3 files changed, 101 insertions(+), 20 deletions(-)
 create mode 100644 server/GameServer/Helpers/PrettyPrinter.lean

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index af87691..5849ae9 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -8,6 +8,8 @@ import I18n
 
 open Lean Meta Elab Command
 
+open GameServer
+
 set_option autoImplicit false
 
 /-! # Game metadata -/
diff --git a/server/GameServer/Helpers.lean b/server/GameServer/Helpers.lean
index debd3c2..dc6d953 100644
--- a/server/GameServer/Helpers.lean
+++ b/server/GameServer/Helpers.lean
@@ -1,4 +1,5 @@
 import Lean
+import GameServer.Helpers.PrettyPrinter
 
 /-! This document contains various things which cluttered `Commands.lean`. -/
 
@@ -6,6 +7,8 @@ open Lean Meta Elab Command
 
 /-! ## Doc Comment Parsing -/
 
+namespace GameServer
+
 /-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
 def parseDocComment! (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
     CommandElabM String := do
@@ -59,26 +62,6 @@ def parseDocCommentLegacy (doc: Option (TSyntax `Lean.Parser.Command.docComment)
         and remove the string following it!"
         pure <| ← parseDocComment! doc
 
-/-! ## Statement string -/
-
-def getStatement (name : Name) : CommandElabM MessageData := do
-  return ← addMessageContextPartial (.ofPPFormat { pp := fun
-    | 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`.
-
-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
-  catch
-  | _ => throwError m!"Could not find {name} in context."
-  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
-
 /-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
 syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
 -- TODO
diff --git a/server/GameServer/Helpers/PrettyPrinter.lean b/server/GameServer/Helpers/PrettyPrinter.lean
new file mode 100644
index 0000000..ae0b7cd
--- /dev/null
+++ b/server/GameServer/Helpers/PrettyPrinter.lean
@@ -0,0 +1,96 @@
+--import Lean
+import Lean.PrettyPrinter.Delaborator.Builtins
+import Lean.PrettyPrinter
+import Lean
+
+import Std.Tactic.OpenPrivate
+
+namespace GameServer
+
+namespace PrettyPrinter
+
+open Lean Meta
+open Lean.Parser Term
+open PrettyPrinter Delaborator SubExpr
+open TSyntax.Compat
+
+
+#check Command.declSig
+
+open private shouldGroupWithNext evalSyntaxConstant from Lean.PrettyPrinter.Delaborator.Builtins
+
+-- def typeSpec := leading_parser " :\\n: " >> termParser
+
+-- def declSig := leading_parser
+--   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> typeSpec
+
+
+@[inherit_doc Lean.PrettyPrinter.Delaborator.delabConstWithSignature]
+partial def delabConstWithSignature : Delab := do
+  let e ← getExpr
+  -- use virtual expression node of arity 2 to separate name and type info
+  let idStx ← descend e 0 <|
+    withOptions (pp.universes.set · true |> (pp.fullNames.set · true)) <|
+      delabConst
+  descend (← inferType e) 1 <|
+    delabParams idStx #[] #[]
+where
+  -- follows `delabBinders`, but does not uniquify binder names and accumulates all binder groups
+  delabParams (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
+    if let .forallE n d _ i ← getExpr then
+      let stxN ← annotateCurPos (mkIdent n)
+      let curIds := curIds.push ⟨stxN⟩
+      if ← shouldGroupWithNext then
+        withBindingBody n <| delabParams idStx groups curIds
+      else
+        let delabTy := withOptions (pp.piBinderTypes.set · false) delab
+        let group ← withBindingDomain do
+          match i with
+          | .implicit       => `(bracketedBinderF|{$curIds*})
+          | .strictImplicit => `(bracketedBinderF|⦃$curIds*⦄)
+          | .instImplicit   => `(bracketedBinderF|[$(← delabTy)])
+          | _ =>
+            if d.isOptParam then
+              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
+            else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
+              let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
+              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
+            else
+              `(bracketedBinderF|($curIds* : $(← delabTy)))
+        withBindingBody n <| delabParams idStx (groups.push group) #[]
+    else
+      let type ← delab
+
+      -- pure type
+      `(Command.declSig| $groups* : $type)
+
+@[inherit_doc Lean.PrettyPrinter.ppSignature]
+def ppSignature (c : Name) : MetaM FormatWithInfos := do
+  let decl ← getConstInfo c
+  let e := .const c (decl.levelParams.map mkLevelParam)
+  let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
+  return ⟨← ppTerm ⟨stx⟩, infos⟩  -- HACK: not a term
+
+end PrettyPrinter
+
+open Lean Meta Elab Command
+
+/-! ## Statement string -/
+
+def getStatement (name : Name) : CommandElabM MessageData := do
+  return ← addMessageContextPartial (.ofPPFormat { pp := fun
+    | some ctx => ctx.runMetaM <| GameServer.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`.
+
+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
+  --catch
+  --| _ => throwError m!"Could not find {name} in context."
+  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.