fix: Conditional handling of `.proj`

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 => ""

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

@@ -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

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