From 5994f0ddf03b71b9b1c6fbb80a7a8e153a24e17d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 Jan 2025 23:10:03 -0800
Subject: [PATCH] fix: Conditional handling of `.proj`

---
 Pantograph/Delate.lean | 17 +++++++++--------
 Test/Delate.lean       | 15 ++++++++++++++-
 2 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 38d8bda..a404fba 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -17,15 +17,18 @@ structure ProjectionApplication where
   numParams: Nat
   inner: Expr
 
+/-- Converts a `.proj` expression to a function application if possible. Not all
+such expressions are convertible. -/
 @[export pantograph_expr_proj_to_app]
-def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
+def exprProjToApp (env: Environment) (e: Expr): Option ProjectionApplication := do
   let (typeName, idx, inner) := match e with
     | .proj typeName idx inner => (typeName, idx, inner)
     | _ => panic! "Argument must be proj"
+  let _ ← getStructureInfo? env typeName
   let ctor := getStructureCtor env typeName
   let fieldName := getStructureFields env typeName |>.get! idx
   let projector := getProjFnForField? env typeName fieldName |>.get!
-  {
+  return {
     projector,
     numParams := ctor.numParams,
     inner,
@@ -375,12 +378,10 @@ 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 _ _ _ => do
-      let env ← getEnv
-      let projApp := exprProjToApp env e
-      let autos := String.intercalate " " (List.replicate projApp.numParams "_")
-      let inner ← self projApp.inner
-      pure s!"((:c {projApp.projector}) {autos} {inner})"
+    | .proj typeName idx e => do
+      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 013be73..7b449bf 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) ((:c And.right) _ _ 0)) :i) :i)"
+      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) (:proj And 1 0)) :i) :i)"
     ),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
@@ -96,6 +96,18 @@ def test_instance (env: Environment): IO LSpec.TestSeq :=
     let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
     return LSpec.TestSeq.done
 
+def test_projection (env: Environment) : IO LSpec.TestSeq:= runTest do
+  let prod := .app (.bvar 1) (.bvar 0)
+  let expr := .proj `Prod 1 prod
+  let .some { projector, numParams, inner }:= exprProjToApp env expr |
+    fail "`Prod should have projection function"
+  checkEq "projector" projector `Prod.snd
+  checkEq "numParams" numParams 2
+  checkTrue "inner" $ inner.equal prod
+
+  let expr := .proj `Exists 1 prod
+  checkTrue "Exists" (exprProjToApp env expr).isNone
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("serializeName", do pure test_serializeName),
@@ -104,6 +116,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Sexp from elaborated expr", test_sexp_of_elab env),
     ("Sexp from expr", test_sexp_of_expr env),
     ("Instance", test_instance env),
+    ("Projection", test_projection env),
   ]
 
 end Pantograph.Test.Delate