Pantograph/Delate.lean

@@ -12,56 +12,24 @@ open Lean
 
 namespace Pantograph
 
-inductive Projection where
+structure ProjectionApplication where
-  -- Normal field case
+  projector: Name
-  | field (projector : Name) (numParams : Nat)
+  numParams: Nat
-  -- Singular inductive case
+  inner: Expr
-  | singular (recursor : Name) (numParams : Nat) (numFields : Nat)
 
-/-- Converts a `.proj` expression to a form suitable for exporting/transpilation -/
+@[export pantograph_expr_proj_to_app]
-@[export pantograph_analyze_projection]
+def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
-def analyzeProjection (env: Environment) (e: Expr): Projection :=
+  let (typeName, idx, inner) := match e with
-  let (typeName, idx, _) := match e with
+    | .proj typeName idx inner => (typeName, idx, inner)
-    | .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
+  {
-  else
+    projector,
-    let recursor := mkRecOnName typeName
+    numParams := ctor.numParams,
-    let ctor := getStructureCtor env typeName
+    inner,
-    .singular recursor ctor.numParams ctor.numFields
+  }
-
-def anonymousLevel : Level := .mvar ⟨.anonymous⟩
-
-@[export pantograph_expr_proj_to_app]
-def exprProjToApp (env: Environment) (e: Expr): Expr :=
-  let anon : Expr := .mvar ⟨.anonymous⟩
-  match analyzeProjection env e with
-  | .field projector numParams =>
-    let info := match env.find? projector with
-      | .some info => info
-      | _ => panic! "Illegal projector"
-    let callee := .const projector $ List.replicate info.numLevelParams anonymousLevel
-    let args := (List.replicate numParams anon) ++ [e.projExpr!]
-    mkAppN callee args.toArray
-  | .singular recursor numParams numFields =>
-    let info := match env.find? recursor with
-      | .some info => info
-      | _ => panic! "Illegal recursor"
-    let callee := .const recursor $ List.replicate info.numLevelParams anonymousLevel
-    let typeArgs := List.replicate numParams anon
-    -- Motive type can be inferred directly
-    let motive := .lam .anonymous anon anon .default
-    let major := e.projExpr!
-    -- Generate a lambda of `numFields` parameters, and returns the `e.projIdx!` one.
-    let induct := List.foldl
-      (λ acc _ => .lam .anonymous anon acc .default)
-      (.bvar $ (numFields - e.projIdx! - 1))
-      (List.range numFields)
-    mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
 
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
@@ -320,6 +288,7 @@ partial def serializeSortLevel (level: Level) : String :=
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
 
+
 /--
  Completely serializes an expression tree. Json not used due to compactness
 
@@ -406,17 +375,12 @@ 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 inner => do
+    | .proj _ _ _ => do
       let env ← getEnv
-      match analyzeProjection env e with
+      let projApp := exprProjToApp env e
-      | .field projector numParams =>
+      let autos := String.intercalate " " (List.replicate projApp.numParams "_")
-        let autos := String.intercalate " " (List.replicate numParams "_")
+      let inner ← self projApp.inner
-        let inner' ← self inner
+      pure s!"((:c {projApp.projector}) {autos} {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 => ""

Test/Delate.lean

@@ -96,23 +96,6 @@ def test_instance (env: Environment): IO LSpec.TestSeq :=
     let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
     return LSpec.TestSeq.done
 
-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 := analyzeProjection env expr |
-    fail "`Prod has fields"
-  checkEq "projector" projector `Prod.snd
-  checkEq "numParams" numParams 2
-
-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 numFields := analyzeProjection env expr |
-    fail "`Exists has no projectors"
-  checkEq "recursor" recursor `Exists.recOn
-  checkEq "numParams" numParams 2
-  checkEq "numFields" numFields 2
-
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("serializeName", do pure test_serializeName),
@@ -121,8 +104,6 @@ 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 Prod", test_projection_prod env),
-    ("Projection Exists", test_projection_exists env),
   ]
 
 end Pantograph.Test.Delate