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

Reviewed-on: #158

Pantograph/Environment.lean

@@ -43,22 +43,6 @@ def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
   if isNameInternal n || info.isUnsafe
   then Option.none
   else Option.some <| toCompactSymbolName n info
-def describe (_: Protocol.EnvDescribe): CoreM Protocol.EnvDescribeResult := do
-  let env ← Lean.MonadEnv.getEnv
-  return {
-    imports := env.header.imports.map toString,
-    modules := env.header.moduleNames.map (·.toString),
-  }
-def moduleRead (args: Protocol.EnvModuleRead): CoreM (Protocol.CR Protocol.EnvModuleReadResult) := do
-  let env ← Lean.MonadEnv.getEnv
-  let .some i := env.header.moduleNames.findIdx? (· == args.module.toName) |
-    return .error $ Protocol.errorIndex s!"Module not found {args.module}"
-  let data := env.header.moduleData[i]!
-  return .ok {
-    imports := data.imports.map toString,
-    constNames := data.constNames.map (·.toString),
-    extraConstNames := data.extraConstNames.map (·.toString),
-  }
 def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
   let env ← Lean.MonadEnv.getEnv
   let names := env.constants.fold (init := #[]) (λ acc name info =>

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

@@ -112,24 +112,6 @@ structure ExprEchoResult where
   type: Expression
   deriving Lean.ToJson
 
--- Describe the current state of the environment
-structure EnvDescribe where
-  deriving Lean.FromJson
-structure EnvDescribeResult where
-  imports : Array String
-  modules : Array String
-  deriving Lean.ToJson
-
--- Describe a module
-structure EnvModuleRead where
-  module : String
-  deriving Lean.FromJson
-structure EnvModuleReadResult where
-  imports: Array String
-  constNames: Array String
-  extraConstNames: Array String
-  deriving Lean.ToJson
-
 -- Print all symbols in environment
 structure EnvCatalog where
   deriving Lean.FromJson
@@ -255,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

@@ -48,8 +48,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     | "reset"         => run reset
     | "stat"          => run stat
     | "expr.echo"     => run expr_echo
-    | "env.describe"  => run env_describe
-    | "env.module_read" => run env_module_read
     | "env.catalog"   => run env_catalog
     | "env.inspect"   => run env_inspect
     | "env.add"       => run env_add
@@ -87,11 +85,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let nGoals := state.goalStates.size
     return .ok { nGoals }
-  env_describe (args: Protocol.EnvDescribe): MainM (CR Protocol.EnvDescribeResult) := do
-    let result ← Environment.describe args
-    return .ok result
-  env_module_read (args: Protocol.EnvModuleRead): MainM (CR Protocol.EnvModuleReadResult) := do
-    Environment.moduleRead args
   env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
     let result ← Environment.catalog args
     return .ok result
@@ -152,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

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