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 1/5] 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)"),

From e2526f11b1e5d7709a04dda7f2156b845d03db7b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 29 Oct 2023 11:56:56 -0700
Subject: [PATCH 2/5] feat: Print names in one segment separated with .

---
 Pantograph/Serial.lean | 14 +++++++-------
 Test/Integration.lean  |  2 +-
 Test/Serial.lean       | 10 +++++++++-
 3 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index d109188..89bc076 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -46,14 +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: Name) (sanitize: Bool := true): String :=
-  if sanitize && name.isInternal then "_"
-  else name_to_ast_aux name |>.drop 1
+def name_to_ast (name: Name) (sanitize: Bool := true): String :=
+  let internal := name.isInaccessibleUserName || name.hasMacroScopes
+  if sanitize && internal then "_"
+  else toString name |> enclose_if_escaped
   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}"
+  enclose_if_escaped (n: String) :=
+    let quote := "̈̈\""
+    if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 
 private def level_depth: Level → Nat
   | .zero => 0
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 39f145e..a77cb12 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -85,7 +85,7 @@ def test_malformed_command : IO LSpec.TestSeq :=
 def test_tactic : IO LSpec.TestSeq :=
   let goal: Protocol.Goal := {
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[{ name := "_uniq 9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
+    vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
   }
   subroutine_runner [
     subroutine_step "goal.start"
diff --git a/Test/Serial.lean b/Test/Serial.lean
index 162a51d..575749d 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -10,7 +10,14 @@ open Lean
 deriving instance Repr, DecidableEq for Protocol.BoundExpression
 
 def test_str_to_name: LSpec.TestSeq :=
-    LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
+  LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
+
+def test_name_to_ast: LSpec.TestSeq :=
+  let quote := "̈̈\""
+  LSpec.test "a.b.1" (name_to_ast (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
+  LSpec.test "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}")
+  -- Pathological test case
+  --LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«̈{escape}{quote}»{quote}")
 
 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × Protocol.BoundExpression) := [
@@ -70,6 +77,7 @@ def suite: IO LSpec.TestSeq := do
 
   return LSpec.group "Serialization" $
     (LSpec.group "str_to_name" test_str_to_name) ++
+    (LSpec.group "name_to_ast" test_name_to_ast) ++
     (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
     (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))
 

From afed5bbc8dadc0569abecdf387ded0fa0d6da49f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 29 Oct 2023 11:57:24 -0700
Subject: [PATCH 3/5] chore: Version bump (breaking change)

---
 Pantograph/Version.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean
index ec93fa9..29b3613 100644
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@@ -1,5 +1,5 @@
 namespace Pantograph
 
-def version := "0.2.6"
+def version := "0.2.7"
 
 end Pantograph

From 454a5bc6b9b2d7f65650a89707864cefbb08ca9b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 29 Oct 2023 12:50:36 -0700
Subject: [PATCH 4/5] feat: Simplify printing of function applications

---
 Pantograph/Serial.lean | 34 +++++++---------------------------
 Test/Integration.lean  |  2 +-
 Test/Serial.lean       |  4 ++--
 3 files changed, 10 insertions(+), 30 deletions(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 89bc076..63f5949 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -55,26 +55,8 @@ def name_to_ast (name: Name) (sanitize: Bool := true): String :=
     let quote := "̈̈\""
     if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 
-private def level_depth: Level → Nat
-  | .zero => 0
-  | .succ l => 1 + (level_depth l)
-  | .max u v | .imax u v => 1 + max (level_depth u) (level_depth v)
-  | .param _ | .mvar _ => 0
-
-theorem level_depth_max_imax (u v: Level): (level_depth (Level.max u v) = level_depth (Level.imax u v)) := by
-  constructor
-theorem level_max_depth_decrease (u v: Level): (level_depth u < level_depth (Level.max u v)) := by
-  have h1: level_depth (Level.max u v) = 1 + Nat.max (level_depth u) (level_depth v) := by constructor
-  rewrite [h1]
-  simp_arith
-  conv =>
-    rhs
-    apply Nat.max_def
-  sorry
-theorem level_offset_decrease (u v: Level): (level_depth u ≤ level_depth (Level.max u v).getLevelOffset) := sorry
-
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
-def serialize_sort_level_ast (level: Level): String :=
+partial def serialize_sort_level_ast (level: Level): String :=
   let k := level.getOffset
   let u := level.getLevelOffset
   let u_str := match u with
@@ -98,14 +80,11 @@ def serialize_sort_level_ast (level: Level): String :=
   | 0, _ => u_str
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
-  termination_by serialize_sort_level_ast level => level_depth level
-  decreasing_by
-  . sorry
 
 /--
  Completely serializes an expression tree. Json not used due to compactness
 -/
-def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
+partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
   self expr
   where
   self (e: Expr): String :=
@@ -128,10 +107,11 @@ def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
       -- The universe level of the const expression is elided since it should be
       -- inferrable from surrounding expression
       s!"(:c {declName})"
-    | .app fn arg =>
-      let fn' := self fn
-      let arg' := self arg
-      s!"({fn'} {arg'})"
+    | .app _ _ =>
+      let fn' := self e.getAppFn
+      let args := e.getAppArgs.map self |>.toList
+      let args := " ".intercalate args
+      s!"({fn'} {args})"
     | .lam binderName binderType body binderInfo =>
       let binderName' := of_name binderName
       let binderType' := self binderType
diff --git a/Test/Integration.lean b/Test/Integration.lean
index a77cb12..6400cca 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -45,7 +45,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
 
 def test_option_modify : IO LSpec.TestSeq :=
   let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
-  let sexp? := Option.some "(: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)))"
+  let sexp? := Option.some "(: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)))"
   let module? := Option.some "Init.Data.Nat.Basic"
   let options: Protocol.Options := {}
   subroutine_runner [
diff --git a/Test/Serial.lean b/Test/Serial.lean
index 575749d..f1b0a9d 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -45,8 +45,8 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
     -- This one contains unhygienic variable names which must be suppressed
     ("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)"),
+    ("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)"),
     -- Handling of higher order types
     ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
     ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")

From e5acd4b26c1de2691557b0a750df10e0882fbf16 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 29 Oct 2023 13:03:48 -0700
Subject: [PATCH 5/5] fix: Sanitize name in universe levels

---
 Pantograph/Serial.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 63f5949..615d9b9 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -56,25 +56,25 @@ def name_to_ast (name: Name) (sanitize: Bool := true): String :=
     if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
-partial def serialize_sort_level_ast (level: Level): String :=
+partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
   let k := level.getOffset
   let u := level.getLevelOffset
   let u_str := match u with
     | .zero => "0"
     | .succ _ => panic! "getLevelOffset should not return .succ"
     | .max v w =>
-      let v := serialize_sort_level_ast v
-      let w := serialize_sort_level_ast w
+      let v := serialize_sort_level_ast v sanitize
+      let w := serialize_sort_level_ast w sanitize
       s!"(:max {v} {w})"
     | .imax v w =>
-      let v := serialize_sort_level_ast v
-      let w := serialize_sort_level_ast w
+      let v := serialize_sort_level_ast v sanitize
+      let w := serialize_sort_level_ast w sanitize
       s!"(:imax {v} {w})"
     | .param name =>
-      let name := name_to_ast name
+      let name := name_to_ast name sanitize
       s!"{name}"
     | .mvar id =>
-      let name := name_to_ast id.name
+      let name := name_to_ast id.name sanitize
       s!"(:mv {name})"
   match k, u with
   | 0, _ => u_str
@@ -101,7 +101,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Stri
       let name := of_name mvarId.name
       s!"(:mv {name})"
     | .sort level =>
-      let level := serialize_sort_level_ast level
+      let level := serialize_sort_level_ast level sanitize
       s!"(:sort {level})"
     | .const declName _ =>
       -- The universe level of the const expression is elided since it should be