feat: Printing field projection in sexp

Pantograph/Delate.lean

@@ -12,24 +12,27 @@ open Lean
 
 namespace Pantograph
 
-structure ProjectionApplication where
-  projector: Name
-  numParams: Nat
-  inner: Expr
+inductive Projection where
+  -- Normal field case
+  | field (projector : Name) (numParams : Nat)
+  -- Singular inductive case
+  | singular (recursor : Name) (numParams : Nat)
 
-@[export pantograph_expr_proj_to_app]
-def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
-  let (typeName, idx, inner) := match e with
-    | .proj typeName idx inner => (typeName, idx, inner)
+/-- 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, _) := match e with
+    | .proj typeName idx struct => (typeName, idx, struct)
     | _ => panic! "Argument must be proj"
-  let ctor := getStructureCtor env typeName
-  let fieldName := getStructureFields env typeName |>.get! idx
-  let projector := getProjFnForField? env typeName fieldName |>.get!
-  {
-    projector,
-    numParams := ctor.numParams,
-    inner,
-  }
+  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
+    let recursor := mkRecOnName typeName
+    let ctor := getStructureCtor env typeName
+    .singular recursor ctor.numParams
 
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
@@ -288,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
 
@@ -375,12 +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 _ _ _ => do
+    | .proj typeName idx inner => 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})"
+      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 => ""

Pantograph/Frontend/MetaTranslate.lean

@@ -68,8 +68,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
     match e with
     | .fvar fvarId =>
       let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
-      -- Delegating this to `Meta.check` later
-      --assert! (← getLCtx).contains fvarId'
+      assert! (← getLCtx).contains fvarId'
       return .done $ .fvar fvarId'
     | .mvar mvarId => do
       -- Must not be assigned

Pantograph/Library.lean

@@ -207,14 +207,6 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: Stri
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
-@[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := do
-  let expr ← match (← parseTermM expr) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  runTermElabM do
-    state.restoreElabM
-    state.tryTacticM goal (Tactic.evalDraft expr)
 @[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
   runTermElabM <| state.tryLet goal binderName type

Pantograph/Protocol.lean

@@ -237,7 +237,6 @@ structure GoalTactic where
   calc?: Option String := .none
   -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
   conv?: Option Bool := .none
-  draft?: Option String := .none
 
   -- In case of the `have` tactic, the new free variable name is provided here
   binderName?: Option String := .none

Repl.lean

@@ -145,27 +145,24 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let .some goal := goalState.goals.get? args.goalId |
       return .error $ errorIndex s!"Invalid goal index {args.goalId}"
     let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
-      -- NOTE: Should probably use a macro to handle this...
-      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft?  with
-      | .some tactic, .none, .none, .none, .none, .none, .none => do
+      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?  with
+      | .some tactic, .none, .none, .none, .none, .none => do
         pure <| Except.ok <| ← goalState.tryTactic goal tactic
-      | .none, .some expr, .none, .none, .none, .none, .none => do
+      | .none, .some expr, .none, .none, .none, .none => do
         pure <| Except.ok <| ← goalState.tryAssign goal expr
-      | .none, .none, .some type, .none, .none, .none, .none => do
+      | .none, .none, .some type, .none, .none, .none => do
         let binderName := args.binderName?.getD ""
         pure <| Except.ok <| ← goalState.tryHave goal binderName type
-      | .none, .none, .none, .some type, .none, .none, .none => do
+      | .none, .none, .none, .some type, .none, .none => do
         let binderName := args.binderName?.getD ""
         pure <| Except.ok <| ← goalState.tryLet goal binderName type
-      | .none, .none, .none, .none, .some pred, .none, .none => do
+      | .none, .none, .none, .none, .some pred, .none => do
         pure <| Except.ok <| ← goalState.tryCalc goal pred
-      | .none, .none, .none, .none, .none, .some true, .none => do
+      | .none, .none, .none, .none, .none, .some true => do
         pure <| Except.ok <| ← goalState.conv goal
-      | .none, .none, .none, .none, .none, .some false, .none => do
+      | .none, .none, .none, .none, .none, .some false => do
         pure <| Except.ok <| ← goalState.convExit
-      | .none, .none, .none, .none, .none, .none, .some draft => do
-        pure <| Except.ok <| ← goalState.tryDraft goal draft
-      | _, _, _, _, _, _, _ =>
+      | _, _, _, _, _, _ =>
         let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
         pure $ Except.error $ error
     match nextGoalState? with

Test/Delate.lean

@@ -96,6 +96,22 @@ 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 := analyzeProjection env expr |
+    fail "`Exists has no projectors"
+  checkEq "recursor" recursor `Exists.recOn
+  checkEq "numParams" numParams 2
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("serializeName", do pure test_serializeName),
@@ -104,6 +120,8 @@ 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

doc/repl.md

@@ -33,7 +33,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
     to the previous `rhs`.
   - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
     exit, the goal id is ignored.
-  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
   Execute continuation/resumption
   - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
@@ -45,12 +44,11 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   state. The user is responsible to ensure the sender/receiver instances share
   the same environment.
 * `frontend.process { ["fileName": <fileName>,] ["file": <str>], invocations:
-  <bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
-  Executes the Lean frontend on a file, collecting the tactic invocations
-  (`"invocations": true`), the sorrys and type errors into goal states
-  (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
-  `sorrys`, this command additionally outputs the position of each captured
-  `sorry`.
+  <bool>, sorrys: <bool>, newConstants: <bool> }`: Executes the Lean frontend on
+  a file, collecting the tactic invocations (`"invocations": true`), the
+  sorrys and type errors into goal states (`"sorrys": true`), and new constants
+  (`"newConstants": true`). In the case of `sorrys`, this command additionally
+  outputs the position of each captured `sorry`.
 
 ## Errors