From c2d606b9d9c9bbf5eb581e8b46a416925c056698 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 29 Oct 2023 11:18:35 -0700
Subject: [PATCH] feat: Simplify name printing

---
 Pantograph/Serial.lean | 14 ++++++++------
 Test/Serial.lean       |  2 +-
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 62321bd..d109188 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -46,12 +46,14 @@ def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
       return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
     return { binders, target := toString (← Meta.ppExpr body) }
 
-private def name_to_ast (name: Lean.Name) (sanitize: Bool := true): String := match name with
-  | .anonymous => ":anon"
-  | .num n i => match sanitize with
-    | false => s!"{toString n} {i}"
-    | true => ":anon"
-  | n@(.str _ _) => toString n
+private def name_to_ast (name: Name) (sanitize: Bool := true): String :=
+  if sanitize && name.isInternal then "_"
+  else name_to_ast_aux name |>.drop 1
+  where
+  name_to_ast_aux: Name → String
+    | .anonymous => ""
+    | .num n i => s!"{name_to_ast_aux n} {i}"
+    | .str init last => s!"{name_to_ast_aux init} {last}"
 
 private def level_depth: Level → Nat
   | .zero => 0
diff --git a/Test/Serial.lean b/Test/Serial.lean
index 9a42992..162a51d 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -36,7 +36,7 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
 def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × String) := [
     -- This one contains unhygienic variable names which must be suppressed
-    ("Nat.add", "(:forall :anon (:c Nat) (:forall :anon (:c Nat) (:c Nat)))"),
+    ("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"),
     -- These ones are normal and easy
     ("Nat.add_one", "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"),
     ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h (((((:c LE.le) (:c Nat)) (:c instLENat)) ((:c Nat.succ) 1)) 0) (((((:c LE.le) (:c Nat)) (:c instLENat)) 2) 1)) :implicit) :implicit)"),