From 8ce4cbdcf55e73589f3eca3052fadfa1843589d0 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 22 Jan 2025 13:01:47 -0800
Subject: [PATCH] feat: Printing field projection in sexp

---
 Pantograph/Delate.lean | 27 +++++++++++++++++----------
 Test/Delate.lean       |  8 +++-----
 2 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 18eaaf1..28f4851 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -14,25 +14,25 @@ namespace Pantograph
 
 inductive Projection where
   -- Normal field case
-  | field (projector : Name) (numParams : Nat) (struct : Expr)
+  | field (projector : Name) (numParams : Nat)
   -- Singular inductive case
-  | singular (recursor : Name) (numParams : Nat) (struct : Expr)
+  | singular (recursor : Name) (numParams : Nat)
 
 /-- Converts a `.proj` expression to a form suitable for exporting/transpilation -/
 @[export pantograph_analyze_projection]
 def analyzeProjection (env: Environment) (e: Expr): Projection :=
-  let (typeName, idx, struct) := match e with
+  let (typeName, idx, _) := match e with
     | .proj typeName idx struct => (typeName, idx, struct)
     | _ => panic! "Argument must be proj"
   if (getStructureInfo? env typeName).isSome then
     let ctor := getStructureCtor env typeName
     let fieldName := getStructureFields env typeName |>.get! idx
     let projector := getProjFnForField? env typeName fieldName |>.get!
-    .field projector ctor.numParams struct
+    .field projector ctor.numParams
   else
     let recursor := mkRecOnName typeName
     let ctor := getStructureCtor env typeName
-    .singular recursor ctor.numParams struct
+    .singular recursor ctor.numParams
 
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
@@ -291,7 +291,7 @@ partial def serializeSortLevel (level: Level) : String :=
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
 
-
+#check Exists.recOn
 /--
  Completely serializes an expression tree. Json not used due to compactness
 
@@ -378,10 +378,17 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
       -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
       -- It may become necessary to incorporate the metadata.
       self inner
-    | .proj typeName idx e => do
-      let typeName' := serializeName typeName (sanitize := false)
-      let e' ← self e
-      pure s!"(:proj {typeName'} {idx} {e'})"
+    | .proj typeName idx inner => do
+      let env ← getEnv
+      match analyzeProjection env e with
+      | .field projector numParams =>
+        let autos := String.intercalate " " (List.replicate numParams "_")
+        let inner' ← self inner
+        pure s!"((:c {projector}) {autos} {inner'})"
+      | .singular _ _ =>
+        let typeName' := serializeName typeName (sanitize := false)
+        let e' ← self e
+        pure s!"(:proj {typeName'} {idx} {e'})"
   -- Elides all unhygenic names
   binderInfoSexp : Lean.BinderInfo → String
     | .default => ""
diff --git a/Test/Delate.lean b/Test/Delate.lean
index aa5ea7c..befc60b 100644
--- a/Test/Delate.lean
+++ b/Test/Delate.lean
@@ -77,7 +77,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
             .default)
         .implicit)
       .implicit,
-      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) (:proj And 1 0)) :i) :i)"
+      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)"
     ),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
@@ -99,20 +99,18 @@ def test_instance (env: Environment): IO LSpec.TestSeq :=
 def test_projection_prod (env: Environment) : IO LSpec.TestSeq:= runTest do
   let struct := .app (.bvar 1) (.bvar 0)
   let expr := .proj `Prod 1 struct
-  let .field projector numParams struct' := analyzeProjection env expr |
+  let .field projector numParams := analyzeProjection env expr |
     fail "`Prod has fields"
   checkEq "projector" projector `Prod.snd
   checkEq "numParams" numParams 2
-  checkTrue "struct" $ struct.equal struct'
 
 def test_projection_exists (env: Environment) : IO LSpec.TestSeq:= runTest do
   let struct := .app (.bvar 1) (.bvar 0)
   let expr := .proj `Exists 1 struct
-  let .singular recursor numParams struct' := analyzeProjection env expr |
+  let .singular recursor numParams := analyzeProjection env expr |
     fail "`Exists has no projectors"
   checkEq "recursor" recursor `Exists.recOn
   checkEq "numParams" numParams 2
-  checkTrue "struct" $ struct.equal struct'
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [