Merge pull request 'feat: Draft tactic REPL interface' (#158) from tactic/draft into dev

Reviewed-on: #158

Pantograph/Delate.lean

@@ -12,27 +12,24 @@ open Lean
 
 namespace Pantograph
 
-inductive Projection where
-  -- Normal field case
-  | field (projector : Name) (numParams : Nat)
-  -- Singular inductive case
-  | singular (recursor : Name) (numParams : Nat)
+structure ProjectionApplication where
+  projector: Name
+  numParams: Nat
+  inner: Expr
 
-/-- 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)
+@[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)
     | _ => 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
-    let recursor := mkRecOnName typeName
-    let ctor := getStructureCtor env typeName
-    .singular recursor ctor.numParams
+  let ctor := getStructureCtor env typeName
+  let fieldName := getStructureFields env typeName |>.get! idx
+  let projector := getProjFnForField? env typeName fieldName |>.get!
+  {
+    projector,
+    numParams := ctor.numParams,
+    inner,
+  }
 
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
@@ -291,7 +288,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,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
-      | .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'})"
+      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})"
   -- Elides all unhygenic names
   binderInfoSexp : Lean.BinderInfo → String
     | .default => ""

Pantograph/Frontend/MetaTranslate.lean

@@ -68,7 +68,8 @@ 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}"
-      assert! (← getLCtx).contains fvarId'
+      -- Delegating this to `Meta.check` later
+      --assert! (← getLCtx).contains fvarId'
       return .done $ .fvar fvarId'
     | .mvar mvarId => do
       -- Must not be assigned

Pantograph/Library.lean

@@ -207,6 +207,14 @@ 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,6 +237,7 @@ 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,24 +145,27 @@ 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
-      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?  with
-      | .some tactic, .none, .none, .none, .none, .none => 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
         pure <| Except.ok <| ← goalState.tryTactic goal tactic
-      | .none, .some expr, .none, .none, .none, .none => do
+      | .none, .some expr, .none, .none, .none, .none, .none => do
         pure <| Except.ok <| ← goalState.tryAssign goal expr
-      | .none, .none, .some type, .none, .none, .none => do
+      | .none, .none, .some type, .none, .none, .none, .none => do
         let binderName := args.binderName?.getD ""
         pure <| Except.ok <| ← goalState.tryHave goal binderName type
-      | .none, .none, .none, .some type, .none, .none => do
+      | .none, .none, .none, .some type, .none, .none, .none => do
         let binderName := args.binderName?.getD ""
         pure <| Except.ok <| ← goalState.tryLet goal binderName type
-      | .none, .none, .none, .none, .some pred, .none => do
+      | .none, .none, .none, .none, .some pred, .none, .none => do
         pure <| Except.ok <| ← goalState.tryCalc goal pred
-      | .none, .none, .none, .none, .none, .some true => do
+      | .none, .none, .none, .none, .none, .some true, .none => do
         pure <| Except.ok <| ← goalState.conv goal
-      | .none, .none, .none, .none, .none, .some false => do
+      | .none, .none, .none, .none, .none, .some false, .none => 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,22 +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 := 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),
@@ -120,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

doc/repl.md

@@ -33,6 +33,7 @@ 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.
@@ -44,11 +45,12 @@ 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>, 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>, 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`.
 
 ## Errors