Merge pull request 'fix: Use in-context environment in sorry collection' (#166) from bug/collect-sorry-generated-constants into dev

Reviewed-on: #166

Main.lean

@@ -10,23 +10,26 @@ open Pantograph.Protocol
 
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Command := do
-  let s := s.trim
+  match s.trim.get? 0 with
-  match s.get? 0 with
+  | .some '{' =>
-  | .some '{' => -- Parse in Json mode
+    -- Parse in Json mode
     Lean.fromJson? (← Lean.Json.parse s)
-  | .some _ => -- Parse in line mode
+  | .some _ =>
+    -- Parse in line mode
     let offset := s.posOf ' ' |> s.offsetOfPos
     if offset = s.length then
       return { cmd := s.take offset, payload := Lean.Json.null }
     else
       let payload ← s.drop offset |> Lean.Json.parse
       return { cmd := s.take offset, payload := payload }
-  | .none => throw "Command is empty"
+  | .none =>
+    throw "Command is empty"
 
-partial def loop : MainM Unit := do
+partial def loop : MainM Unit := do repeat do
   let state ← get
   let command ← (← IO.getStdin).getLine
-  if command.trim.length = 0 then return ()
+  -- Halt the program if empty line is given
+  if command.trim.length = 0 then break
   match parseCommand command with
   | .error error =>
     let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
@@ -43,25 +46,21 @@ partial def loop : MainM Unit := do
       let message ← e.toMessageData.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
       IO.println error.compress
-  loop
 
 
 unsafe def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
-  -- Separate imports and options
   if args == ["--version"] then do
     IO.println s!"{Pantograph.version}"
     return
 
   Pantograph.initSearch ""
 
-  let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
+  -- Separate imports and options
-    |>.toArray |> Pantograph.createCoreContext
+  let (options, imports) := args.partition (·.startsWith "--")
-  let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
+  let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext
   let coreState ← Pantograph.createCoreState imports.toArray
-  let context: Context := {
+  let context: Context := {}
-    imports
-  }
   try
     let coreM := loop.run context |>.run' {}
     IO.println "ready."

Pantograph/Delate.lean

@@ -12,24 +12,56 @@ open Lean
 
 namespace Pantograph
 
-structure ProjectionApplication where
+inductive Projection where
-  projector: Name
+  -- Normal field case
-  numParams: Nat
+  | field (projector : Name) (numParams : Nat)
-  inner: Expr
+  -- Singular inductive case
+  | singular (recursor : Name) (numParams : Nat) (numFields : Nat)
 
-@[export pantograph_expr_proj_to_app]
+/-- Converts a `.proj` expression to a form suitable for exporting/transpilation -/
-def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
+@[export pantograph_analyze_projection]
-  let (typeName, idx, inner) := match e with
+def analyzeProjection (env: Environment) (e: Expr): Projection :=
-    | .proj typeName idx inner => (typeName, idx, inner)
+  let (typeName, idx, _) := match e with
+    | .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
-    projector,
+  else
-    numParams := ctor.numParams,
+    let recursor := mkRecOnName typeName
-    inner,
+    let ctor := getStructureCtor env typeName
-  }
+    .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") _
 
@@ -264,38 +296,36 @@ def serializeName (name: Name) (sanitize: Bool := true): String :=
     if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
-partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
+partial def serializeSortLevel (level: Level) : String :=
   let k := level.getOffset
   let u := level.getLevelOffset
   let u_str := match u with
     | .zero => "0"
     | .succ _ => panic! "getLevelOffset should not return .succ"
     | .max v w =>
-      let v := serializeSortLevel v sanitize
+      let v := serializeSortLevel v
-      let w := serializeSortLevel w sanitize
+      let w := serializeSortLevel w
       s!"(:max {v} {w})"
     | .imax v w =>
-      let v := serializeSortLevel v sanitize
+      let v := serializeSortLevel v
-      let w := serializeSortLevel w sanitize
+      let w := serializeSortLevel w
       s!"(:imax {v} {w})"
     | .param name =>
-      let name := serializeName name sanitize
       s!"{name}"
     | .mvar id =>
-      let name := serializeName id.name sanitize
+      let name := id.name
       s!"(:mv {name})"
   match k, u with
   | 0, _ => u_str
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
 
-
 /--
  Completely serializes an expression tree. Json not used due to compactness
 
 A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
-partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
+partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
   self expr
   where
   delayedMVarToSexp (e: Expr): MetaM (Option String) := do
@@ -334,9 +364,10 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
         let name := mvarId.name
         pure s!"(:{pref} {name})"
     | .sort level =>
-      let level := serializeSortLevel level sanitize
+      let level := serializeSortLevel level
       pure s!"(:sort {level})"
     | .const declName _ =>
+      let declName := serializeName declName (sanitize := false)
       -- The universe level of the const expression is elided since it should be
       -- inferrable from surrounding expression
       pure s!"(:c {declName})"
@@ -369,24 +400,29 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       -- is wrapped in a :lit sexp.
       let v' := match v with
         | .natVal val => toString val
-        | .strVal val => s!"\"{val}\""
+        | .strVal val => IR.EmitC.quoteString val
       pure s!"(:lit {v'})"
     | .mdata _ inner =>
       -- 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
+      match analyzeProjection env e with
-      let autos := String.intercalate " " (List.replicate projApp.numParams "_")
+      | .field projector numParams =>
-      let inner ← self projApp.inner
+        let autos := String.intercalate " " (List.replicate numParams "_")
-      pure s!"((:c {projApp.projector}) {autos} {inner})"
+        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 => ""
-    | .implicit => " :implicit"
+    | .implicit => " :i"
-    | .strictImplicit => " :strictImplicit"
+    | .strictImplicit => " :si"
-    | .instImplicit => " :instImplicit"
+    | .instImplicit => " :ii"
 
 def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
   let pp?: Option String ← match options.printExprPretty with
@@ -532,7 +568,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
         then instantiateAll decl.type
         else pure $ decl.type
       let type_sexp ← if options.printSexp then
-          let sexp ← serializeExpressionSexp type (sanitize := false)
+          let sexp ← serializeExpressionSexp type
           pure <| " " ++ sexp
         else
           pure ""

Pantograph/Environment.lean

@@ -43,6 +43,22 @@ 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 =>
@@ -58,7 +74,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
     | some info => pure info
   let module? := env.getModuleIdxFor? name >>=
-    (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
+    (λ idx => env.allImportedModuleNames.get? idx.toNat)
   let value? := match args.value?, info with
     | .some true, _ => info.value?
     | .some false, _ => .none
@@ -80,7 +96,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       then value?.map (λ e =>
         e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
       else .none,
-    module? := module?
+    module? := module?.map (·.toString)
   }
   let result ← match info with
     | .inductInfo induct => pure { core with inductInfo? := .some {
@@ -113,6 +129,20 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           k := r.k,
       } }
     | _ => pure core
+  let result ← if args.source?.getD false then
+      let srcSearchPath ← initSrcSearchPath
+      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
+      let declRange? ← findDeclarationRanges? name
+      let sourceStart? := declRange?.map (·.range.pos)
+      let sourceEnd? := declRange?.map (·.range.endPos)
+      .pure {
+        result with
+        sourceUri?,
+        sourceStart?,
+        sourceEnd?,
+      }
+    else
+      .pure result
   return .ok result
 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
   let env ← Lean.MonadEnv.getEnv

Pantograph/Frontend/Basic.lean

@@ -67,7 +67,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let s := (← get).commandState
   let before := s.env
   let done ← Elab.Frontend.processCommand
-  let stx := (← get).commands.back
+  let stx := (← get).commands.back!
   let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
   let s' := (← get).commandState
   let after := s'.env

Pantograph/Frontend/Elab.lean

@@ -80,10 +80,10 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
 
 @[export pantograph_frontend_collect_tactics_from_compilation_step_m]
 def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
-  let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
+  let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ
     | info@(.ofTacticInfo _) => info.isOriginal
     | _ => false
-  let tactics := tacticInfoTrees.bind collectTactics
+  let tactics := tacticInfoTrees.flatMap collectTactics
   tactics.mapM λ invocation => do
     let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
     let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
@@ -104,14 +104,20 @@ structure InfoWithContext where
   info: Elab.Info
   context?: Option Elab.ContextInfo := .none
 
-private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
+structure GoalCollectionOptions where
+  collectTypeErrors : Bool := false
+
+private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOptions := {})
+    : IO (List InfoWithContext) := do
   let infos ← t.findAllInfoM none fun i ctx? => match i with
-    | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
+    | .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
       let .some ctx := ctx? | return (false, true)
       if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
         if expectedType?.isNone then
           throw $ .userError "Sorry of indeterminant type is not allowed"
         return (true, false)
+      unless options.collectTypeErrors do
+        return (false, true)
       let .some expectedType := expectedType? | return (false, true)
       let typeMatch ← ctx.runMetaM lctx do
         let type ← Meta.inferType expr
@@ -130,8 +136,9 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
 
 -- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
+def collectSorrys (step: CompilationStep) (options : GoalCollectionOptions := {})
-  return (← step.trees.mapM collectSorrysInTree).join
+    : IO (List InfoWithContext) := do
+  return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).flatten
 
 structure AnnotatedGoalState where
   state : GoalState
@@ -141,21 +148,31 @@ structure AnnotatedGoalState where
 Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
 the current `MetavarContext`.
+
+WARNING: Behaviour is unstable when there are multiple `sorry`s. Consider using
+the draft tactic instead.
 -/
 @[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
+  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
   assert! !sorrys.isEmpty
+  withEnv env do
     let goalsM := sorrys.mapM λ i => do
       match i.info with
       | .ofTermInfo termInfo  => do
         let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
+        if (← mvarId.getType).hasSorry then
+          throwError s!"Coupling is not allowed in drafting"
         return [(mvarId, stxByteRange termInfo.stx)]
       | .ofTacticInfo tacticInfo => do
         let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+        for mvarId in mvarIds do
+          if (← mvarId.getType).hasSorry then
+            throwError s!"Coupling is not allowed in drafting"
         let range := stxByteRange tacticInfo.stx
         return mvarIds.map (·, range)
       | _ => panic! "Invalid info"
-  let annotatedGoals := List.join (← goalsM.run {} |>.run' {})
+    let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
     let goals := annotatedGoals.map Prod.fst
     let srcBoundaries := annotatedGoals.map Prod.snd
     let root := match goals with

Pantograph/Frontend/InfoTree.lean

@@ -26,6 +26,8 @@ protected def Info.stx? : Info → Option Syntax
   | .ofFVarAliasInfo      _    => none
   | .ofFieldRedeclInfo    info => info.stx
   | .ofOmissionInfo       info => info.stx
+  | .ofChoiceInfo         info => info.stx
+  | .ofPartialTermInfo    info => info.stx
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 protected def Info.isOriginal (i : Info) : Bool :=
   match i.stx? with
@@ -87,9 +89,9 @@ partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ =>
   | .context ctx tree => tree.filter p m |>.map (.context ctx)
   | .node info children =>
     if p info then
-      [.node info (children.toList.map (filter p m)).join.toPArray']
+      [.node info (children.toList.map (filter p m)).flatten.toPArray']
     else
-      (children.toList.map (filter p m)).join
+      (children.toList.map (filter p m)).flatten
   | .hole mvar => if m mvar then [.hole mvar] else []
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
@@ -103,7 +105,7 @@ partial def InfoTree.findAllInfo
   | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
   | .node i children  =>
     let head := if pred i then [(i, context?, children)] else []
-    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
+    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.flatMap (fun t => findAllInfo t context? haltOnMatch pred)
     head ++ tail
   | _ => []
 
@@ -119,7 +121,7 @@ partial def InfoTree.findAllInfoM [Monad m]
     let (flagCollect, flagRecurse) ← pred i context?
     let head := if flagCollect then [(i, context?, children)] else []
     let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred)
-    return head ++ (← tail).join
+    return head ++ (← tail).flatten
   | _ => return []
 
 @[export pantograph_infotree_to_string_m]
@@ -141,6 +143,8 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
       | .ofFVarAliasInfo _ => pure "[fvar]"
       | .ofFieldRedeclInfo _ => pure "[field_redecl]"
       | .ofOmissionInfo _ => pure "[omission]"
+      | .ofChoiceInfo _ => pure "[choice]"
+      | .ofPartialTermInfo  _ => pure "[partial_term]"
       let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
       return s!"{node}\n{children}"
     else throw <| IO.userError "No `ContextInfo` available."

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/Goal.lean

@@ -183,7 +183,8 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
   -- to one of these seed mvars, it means an error has occurred when a tactic
   -- was executing on `src`. `evalTactic`, will not capture these mvars, so we
   -- need to manually find them and save them into the goal list.
-  let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar src)
+
+  let descendants ←  Meta.getMVars (.mvar src)
   --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
   let mut alreadyVisited : MVarIdSet := {}
   let mut result : MVarIdSet := {}
@@ -237,25 +238,34 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
-/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
+private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
-protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false):
+  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
-      Elab.TermElabM TacticResult := do
-  try
-    let nextState ← state.step goal tacticM guardMVarErrors
-
-    -- Check if error messages have been generated in the core.
-    let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length
     |>.filterMapM λ m => do
       if m.severity == .error then
         return .some $ ← m.toString
       else
         return .none
   Core.resetMessageLog
+  return newMessages.toArray
+
+/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
+protected def GoalState.tryTacticM
+    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+    (guardMVarErrors : Bool := false)
+    : Elab.TermElabM TacticResult := do
+  let prevMessageLength := state.coreState.messages.toList.length
+  try
+    let nextState ← state.step goal tacticM guardMVarErrors
+
+    -- Check if error messages have been generated in the core.
+    let newMessages ← dumpMessageLog prevMessageLength
     if ¬ newMessages.isEmpty then
-      return .failure newMessages.toArray
+      return .failure newMessages
     return .success nextState
   catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+    match exception with
+    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
+    | _ => return .failure #[← exception.toMessageData.toString]
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
 @[export pantograph_goal_state_try_tactic_m]

Pantograph/Library.lean

@@ -138,16 +138,35 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array
   runMetaM <| state.serializeGoals (parent := .none) options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
+def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
-  runMetaM do
+  : CoreM Protocol.GoalPrintResult := runMetaM do
   state.restoreMetaM
+
+  let root? ← if rootExpr then
+      state.rootExpr?.mapM λ expr => state.withRootContext do
+        serializeExpression options (← instantiateAll expr)
+    else
+      pure .none
+  let parent? ← if parentExpr then
+      state.parentExpr?.mapM λ expr => state.withParentContext do
+        serializeExpression options (← instantiateAll expr)
+    else
+      pure .none
+  let goals ← if goals then
+      goalSerialize state options
+    else
+      pure #[]
+  let extraMVars ← extraMVars.mapM λ mvarId => do
+    let mvarId: MVarId := { name := mvarId.toName }
+    let .some _ ← mvarId.findDecl? | return {}
+    state.withContext mvarId do
+      let .some expr ← getExprMVarAssignment? mvarId | return {}
+      serializeExpression options (← instantiateAll expr)
   return {
-      root? := ← state.rootExpr?.mapM (λ expr =>
+    root?,
-        state.withRootContext do
+    parent?,
-          serializeExpression options (← instantiateAll expr)),
+    goals,
-      parent? := ← state.parentExpr?.mapM (λ expr =>
+    extraMVars,
-        state.withParentContext do
-          serializeExpression options (← instantiateAll expr)),
   }
 
 @[export pantograph_goal_tactic_m]
@@ -188,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

@@ -5,6 +5,7 @@ Note that no command other than `InteractionError` may have `error` as one of
 its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json
+import Lean.Data.Position
 
 namespace Pantograph.Protocol
 
@@ -111,6 +112,24 @@ 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
@@ -121,11 +140,13 @@ structure EnvCatalogResult where
 -- Print the type of a symbol
 structure EnvInspect where
   name: String
-  -- If true/false, show/hide the value expressions; By default definitions
+  -- Show the value expressions; By default definitions values are shown and
-  -- values are shown and theorem values are hidden.
+  -- theorem values are hidden.
   value?: Option Bool := .some false
-  -- If true, show the type and value dependencies
+  -- Show the type and value dependencies
   dependency?: Option Bool := .some false
+  -- Show source location
+  source?: Option Bool := .some false
   deriving Lean.FromJson
 -- See `InductiveVal`
 structure InductInfo where
@@ -172,6 +193,11 @@ structure EnvInspectResult where
   inductInfo?:      Option InductInfo      := .none
   constructorInfo?: Option ConstructorInfo := .none
   recursorInfo?:    Option RecursorInfo    := .none
+
+  -- Location in source
+  sourceUri?: Option String := .none
+  sourceStart?: Option Lean.Position := .none
+  sourceEnd?: Option Lean.Position := .none
   deriving Lean.ToJson
 
 structure EnvAdd where
@@ -229,6 +255,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
@@ -271,12 +298,23 @@ structure GoalDeleteResult where
 
 structure GoalPrint where
   stateId: Nat
+
+  -- Print root?
+  rootExpr?: Option Bool := .some False
+  -- Print the parent expr?
+  parentExpr?: Option Bool := .some False
+  -- Print goals?
+  goals?: Option Bool := .some False
+  -- Print values of extra mvars?
+  extraMVars?: Option (Array String) := .none
   deriving Lean.FromJson
 structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
-  parent?: Option Expression
+  parent?: Option Expression := .none
+  goals: Array Goal := #[]
+  extraMVars: Array Expression := #[]
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL
@@ -308,11 +346,13 @@ structure FrontendProcess where
   -- One of these two must be supplied: Either supply the file name or the content.
   fileName?: Option String := .none
   file?: Option String := .none
-  -- If set to true, collect tactic invocations
+  -- collect tactic invocations
   invocations: Bool := false
-  -- If set to true, collect `sorry`s
+  -- collect `sorry`s
   sorrys: Bool := false
-  -- If set to true, extract new constants
+  -- collect type errors
+  typeErrorsAsGoals: Bool := false
+  -- list new constants from each compilation step
   newConstants: Bool := false
   deriving Lean.FromJson
 structure InvokedTactic where

Pantograph/Serial.lean

@@ -59,6 +59,12 @@ and then add the new constants.
 def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit :=
   Pantograph.pickle path (env.header.imports, env.constants.map₂)
 
+def resurrectEnvironment
+  (imports : Array Import)
+  (map₂ : PHashMap Name ConstantInfo)
+  : IO Environment := do
+  let env ← importModules imports {} 0
+  env.replay (Std.HashMap.ofList map₂.toList)
 /--
 Unpickle an `Environment` from disk.
 
@@ -68,8 +74,7 @@ and then replace the new constants.
 @[export pantograph_env_unpickle_m]
 def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
   let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
-  let env ← importModules imports {} 0
+  return (← resurrectEnvironment imports map₂, region)
-  return (← env.replay (Std.HashMap.ofList map₂.toList), region)
 
 
 open Lean.Core in
@@ -88,7 +93,9 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
     savedState := {
       term := {
         meta := {
-          core,
+          core := {
+            env, nextMacroScope, ngen, ..
+          },
           meta,
         }
         «elab»,
@@ -100,9 +107,10 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
     convMVar?,
     calcPrevRhs?,
   } := goalState
-  --let env := core.env
   Pantograph.pickle path (
-    ({ core with } : CompactCoreState),
+    env.constants.map₂,
+
+    ({ nextMacroScope, ngen } : CompactCoreState),
     meta,
     «elab»,
     tactic,
@@ -117,6 +125,8 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
 def goalStateUnpickle (path : System.FilePath) (env : Environment)
     : IO (GoalState × CompactedRegion) := unsafe do
   let ((
+    map₂,
+
     compactCore,
     meta,
     «elab»,
@@ -127,6 +137,8 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
     convMVar?,
     calcPrevRhs?,
   ), region) ← Pantograph.unpickle (
+    PHashMap Name ConstantInfo ×
+
     CompactCoreState ×
     Meta.State ×
     Elab.Term.State ×
@@ -137,6 +149,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
     Option (MVarId × MVarId × List MVarId) ×
     Option (MVarId × Expr)
   ) path
+  let env ← env.replay (Std.HashMap.ofList map₂.toList)
   let goalState := {
     savedState := {
       term := {

Pantograph/Tactic/Assign.lean

@@ -27,5 +27,38 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
   goal.assign expr
   Elab.Tactic.replaceMainGoal nextGoals
 
+def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
+  Meta.transform src λ
+    | .app (.app (.const ``sorryAx ..) type) .. => do
+      let type ← instantiateMVars type
+      if type.hasSorry then
+        throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
+      let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
+      modify (mvar.mvarId! :: .)
+      pure $ .done mvar
+    | _ => pure .continue
+
+-- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals.
+def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do
+  goal.checkNotAssigned `Pantograph.Tactic.draft
+  let exprType ← Meta.inferType expr
+  let goalType ← goal.getType
+  unless ← Meta.isDefEq goalType exprType do
+    throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
+
+  let (expr', holes) ← sorryToHole expr |>.run []
+  goal.assign expr'
+  return holes.reverse
+
+def evalDraft : Elab.Tactic.Tactic := fun stx ↦ Elab.Tactic.withMainContext do
+  let target ← Elab.Tactic.getMainTarget
+  let goal ← Elab.Tactic.getMainGoal
+  let (expr, holeGoals) ← Elab.Tactic.elabTermWithHoles stx
+    (expectedType? := .some target)
+    (tagSuffix := .anonymous)
+    (allowNaturalHoles := true)
+  let draftGoals ← draft goal expr
+  Elab.Tactic.replaceMainGoal $ holeGoals ++ draftGoals
+
 
 end Pantograph.Tactic

Pantograph/Tactic/Prograde.lean

@@ -40,7 +40,7 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
   let fvarId ← mkFreshFVarId
   let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
   let mvarUpstream ←
-    withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
+    Meta.withLCtx lctxUpstream #[] do
       Meta.withNewLocalInstances #[.fvar fvarId] 0 do
         let mvarUpstream ← mkUpstreamMVar mvarId
         --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream

Pantograph/Version.lean

@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.2.22"
+def version := "0.2.25"
 
 end Pantograph

Repl.lean

@@ -3,8 +3,9 @@ import Pantograph
 
 namespace Pantograph.Repl
 
+open Lean
+
 structure Context where
-  imports: List String
 
 /-- Stores state of the REPL -/
 structure State where
@@ -13,7 +14,9 @@ structure State where
   goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
 
 /-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
+abbrev MainM := ReaderT Context $ StateRefT State CoreM
+/-- Fallible subroutine return type -/
+abbrev CR α := Except Protocol.InteractionError α
 
 def newGoalState (goalState: GoalState) : MainM Nat := do
   let state ← get
@@ -25,29 +28,105 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
   return stateId
 
 
--- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
+def runMetaInMainM { α } (metaM: MetaM α): MainM α :=
--- certain monadic features in `MainM`
-abbrev CR α := Except Protocol.InteractionError α
-
-def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
   metaM.run'
-def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
+def runTermElabInMainM { α } (termElabM: Elab.TermElabM α) : MainM α :=
   termElabM.run' (ctx := defaultElabContext) |>.run'
 
+section Frontend
+
+structure CompilationUnit where
+  -- Should be the penultimate environment, but this is ok
+  env : Environment
+  boundary : Nat × Nat
+  invocations : List Protocol.InvokedTactic
+  sorrys : List Frontend.InfoWithContext
+  messages : Array String
+  newConstants : List Name
+
+def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
+  let options := (← get).options
+  let (fileName, file) ← match args.fileName?, args.file? with
+    | .some fileName, .none => do
+      let file ← IO.FS.readFile fileName
+      pure (fileName, file)
+    | .none, .some file =>
+      pure ("<anonymous>", file)
+    | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
+  let env?: Option Environment ← if args.fileName?.isSome then
+      pure .none
+    else do
+      let env ← getEnv
+      pure <| .some env
+  let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
+  let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) :=
+    Frontend.mapCompilationSteps λ step => do
+    let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
+    let invocations: Option (List Protocol.InvokedTactic) ← if args.invocations then
+        Frontend.collectTacticsFromCompilationStep step
+      else
+        pure []
+    let sorrys ← if args.sorrys then
+        Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
+      else
+        pure []
+    let messages ← step.messageStrings
+    let newConstants ← if args.newConstants then
+        Frontend.collectNewDefinedConstants step
+      else
+        pure []
+    return {
+      env := step.before,
+      boundary,
+      invocations,
+      sorrys,
+      messages,
+      newConstants
+    }
+  let li ← frontendM.run context |>.run' state
+  let units ← li.mapM λ step => withEnv step.env do
+    let newConstants? := if args.newConstants then
+        .some $ step.newConstants.toArray.map λ name => name.toString
+      else
+        .none
+    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
+        pure (.none, .none, .none)
+      else do
+        let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState step.sorrys
+        let stateId ← newGoalState state
+        let goals ← goalSerialize state options
+        let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
+        pure (.some stateId, .some goals, .some srcBoundaries)
+    let invocations? := if args.invocations then .some step.invocations else .none
+    return {
+      boundary := step.boundary,
+      messages := step.messages,
+      invocations?,
+      goalStateId?,
+      goals?,
+      goalSrcBoundaries?,
+      newConstants?,
+    }
+  return .ok { units }
+
+end Frontend
+
 /-- Main loop command of the REPL -/
-def execute (command: Protocol.Command): MainM Lean.Json := do
+def execute (command: Protocol.Command): MainM Json := do
-  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
+  let run { α β: Type } [FromJson α] [ToJson β] (comm: α → MainM (CR β)): MainM Json :=
-    match Lean.fromJson? command.payload with
+    match fromJson? command.payload with
     | .ok args => do
       match (← comm args) with
-      | .ok result =>  return Lean.toJson result
+      | .ok result =>  return toJson result
-      | .error ierror => return Lean.toJson ierror
+      | .error ierror => return toJson ierror
-    | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
+    | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
   try
     match command.cmd with
     | "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
@@ -66,10 +145,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     | cmd =>
       let error: Protocol.InteractionError :=
         errorCommand s!"Unknown command {cmd}"
-      return Lean.toJson error
+      return toJson error
   catch ex => do
     let error ← ex.toMessageData.toString
-    return Lean.toJson $ errorIO error
+    return toJson $ errorIO error
   where
   errorCommand := errorI "command"
   errorIndex := errorI "index"
@@ -79,12 +158,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let nGoals := state.goalStates.size
     set { state with nextId := 0, goalStates := .empty }
-    Lean.Core.resetMessageLog
+    Core.resetMessageLog
     return .ok { nGoals }
   stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := 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
@@ -94,12 +178,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
     Environment.addDecl args
   env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
-    let env ← Lean.MonadEnv.getEnv
+    let env ← MonadEnv.getEnv
     environmentPickle env args.path
     return .ok {}
   env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
     let (env, _) ← environmentUnpickle args.path
-    Lean.setEnv env
+    setEnv env
     return .ok {}
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
@@ -124,7 +208,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
     return .ok (← get).options
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
-    let env ← Lean.MonadEnv.getEnv
+    let env ← MonadEnv.getEnv
     let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
       | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
       | .none, .some copyFrom =>
@@ -145,24 +229,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
+      -- NOTE: Should probably use a macro to handle this...
-      | .some tactic, .none, .none, .none, .none, .none => do
+      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
@@ -223,7 +310,13 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let .some goalState := state.goalStates[args.stateId]? |
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← runMetaInMainM <| goalPrint goalState state.options
+    let result ← runMetaInMainM <| goalPrint
+        goalState
+        (rootExpr := args.rootExpr?.getD False)
+        (parentExpr := args.parentExpr?.getD False)
+        (goals := args.goals?.getD False)
+        (extraMVars := args.extraMVars?.getD #[])
+        (options := state.options)
     return .ok result
   goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
     let state ← get
@@ -232,66 +325,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     goalStatePickle goalState args.path
     return .ok {}
   goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do
-    let (goalState, _) ← goalStateUnpickle args.path (← Lean.MonadEnv.getEnv)
+    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
     let id ← newGoalState goalState
     return .ok { id }
   frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
-    let options := (← get).options
     try
-      let (fileName, file) ← match args.fileName?, args.file? with
+      frontend_process_inner args
-        | .some fileName, .none => do
-          let file ← IO.FS.readFile fileName
-          pure (fileName, file)
-        | .none, .some file =>
-          pure ("<anonymous>", file)
-        | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
-      let env?: Option Lean.Environment ← if args.fileName?.isSome then
-          pure .none
-        else do
-          let env ← Lean.MonadEnv.getEnv
-          pure <| .some env
-      let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
-      let frontendM := Frontend.mapCompilationSteps λ step => do
-        let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-        let invocations?: Option (List Protocol.InvokedTactic) ← if args.invocations then
-            let invocations ← Frontend.collectTacticsFromCompilationStep step
-            pure $ .some invocations
-          else
-            pure .none
-        let sorrys ← if args.sorrys then
-            Frontend.collectSorrys step
-          else
-            pure []
-        let messages ← step.messageStrings
-        let newConstants ← if args.newConstants then
-            Frontend.collectNewDefinedConstants step
-          else
-            pure []
-        return (step.before, boundary, invocations?, sorrys, messages, newConstants)
-      let li ← frontendM.run context |>.run' state
-      let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do
-        let newConstants? := if args.newConstants then
-            .some $ newConstants.toArray.map λ name => name.toString
-          else
-            .none
-        let (goalStateId?, goals?, goalSrcBoundaries?) ← if sorrys.isEmpty then do
-            pure (.none, .none, .none)
-          else do
-            let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
-            let stateId ← newGoalState state
-            let goals ← goalSerialize state options
-            let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
-            pure (.some stateId, .some goals, .some srcBoundaries)
-        return {
-          boundary,
-          messages,
-          invocations?,
-          goalStateId?,
-          goals?,
-          goalSrcBoundaries?,
-          newConstants?,
-        }
-      return .ok { units }
     catch e =>
       return .error $ errorI "frontend" (← e.toMessageData.toString)
 

Test/Common.lean

@@ -48,6 +48,12 @@ namespace Condensed
 deriving instance BEq, Repr for LocalDecl
 deriving instance BEq, Repr for Goal
 
+-- Enable string interpolation
+instance : ToString FVarId where
+  toString id := id.name.toString
+instance : ToString MVarId where
+  toString id := id.name.toString
+
 protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
   {
     decl with fvarId := { name := .anonymous }
@@ -143,6 +149,8 @@ def runTest (t: TestT m Unit): m LSpec.TestSeq :=
   Prod.snd <$> t.run LSpec.TestSeq.done
 def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) :=
   t.run LSpec.TestSeq.done
+def runTestCoreM (env: Environment) (coreM: TestT CoreM Unit) (options: Array String := #[]): IO LSpec.TestSeq := do
+  runCoreMSeq env (runTest coreM) options
 
 end Monadic
 

Test/Delate.lean

@@ -35,7 +35,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
     ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"),
     -- These ones are normal and easy
     ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
-    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),
+    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :i) :i)"),
     -- Handling of higher order types
     ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
     ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
@@ -50,8 +50,8 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × (List Name) × String) := [
     ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
     ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
-    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
-    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
     ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
   ]
   entries.foldlM (λ suites (source, levels, target) =>
@@ -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)) :implicit) :implicit)"
+      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)"
     ),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
@@ -96,6 +96,23 @@ 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),
@@ -104,6 +121,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

Test/Environment.lean

@@ -97,11 +97,29 @@ def test_inspect: IO LSpec.TestSeq := do
     ) LSpec.TestSeq.done
   runCoreMSeq env inner
 
+def test_symbol_location : TestT IO Unit := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
+  addTest $ ← runTestCoreM env do
+    let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
+    checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
+
+    -- Extraction of source doesn't work for symbols in `Init` for some reason
+    checkTrue "file" result.sourceUri?.isNone
+    checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
+    checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
+    let .ok { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
+    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
+    checkTrue "constNames" $ constNames.contains "Nat.succ_add"
+
 def suite: List (String × IO LSpec.TestSeq) :=
   [
     ("Catalog", test_catalog),
     ("Symbol Visibility", test_symbol_visibility),
     ("Inspect", test_inspect),
+    ("Symbol Location", runTest test_symbol_location),
   ]
 
 end Pantograph.Test.Environment

Test/Frontend.lean

@@ -6,11 +6,12 @@ import Test.Common
 open Lean Pantograph
 namespace Pantograph.Test.Frontend
 
-def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
+def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
+    : MetaM (List GoalState) := do
   let filename := "<anonymous>"
   let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
   let m := Frontend.mapCompilationSteps λ step => do
-    return (step.before, ← Frontend.collectSorrys step)
+    return (step.before, ← Frontend.collectSorrys step options)
   let li ← m.run context |>.run' state
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
     if sorrys.isEmpty then
@@ -181,9 +182,10 @@ def test_capture_type_mismatch : TestT MetaM Unit := do
   let input := "
 def mystery (k: Nat) : Nat := true
   "
-  let goalStates ← (collectSorrysFromSource input).run' {}
+  let options := { collectTypeErrors := true }
+  let goalStates ← (collectSorrysFromSource input options).run' {}
   let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
-  checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
+  checkEq "goals" ((← goalState.serializeGoals).map (·.devolatilize)) #[
     {
       target := { pp? := "Nat" },
       vars := #[{
@@ -193,6 +195,16 @@ def mystery (k: Nat) : Nat := true
     }
   ]
 
+def test_capture_type_mismatch_in_binder : TestT MetaM Unit := do
+  let input := "
+example (p: Prop) (h: (∀ (x: Prop), Nat) → p): p := h (λ (y: Nat) => 5)
+  "
+  let options := { collectTypeErrors := true }
+  let goalStates ← (collectSorrysFromSource input options).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
+  ]
+
 def collectNewConstants (source: String) : MetaM (List (List Name)) := do
   let filename := "<anonymous>"
   let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
@@ -227,6 +239,7 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
     ("sorry_in_coupled", test_sorry_in_coupled),
     ("environment_capture", test_environment_capture),
     ("capture_type_mismatch", test_capture_type_mismatch),
+    --("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder),
     ("collect_one_constant", test_collect_one_constant),
     ("collect_one_theorem", test_collect_one_theorem),
   ]

Test/Integration.lean

@@ -72,8 +72,8 @@ def test_tactic : Test :=
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
     step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.print" [("stateId", .num 1)]
+    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
-     ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
+     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
     step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
   ]
@@ -90,27 +90,27 @@ def test_automatic_mode (automatic: Bool): Test :=
     ],
   }
   let goal2l: Protocol.Goal := {
-    name := "_uniq.59",
+    name := "_uniq.61",
     userName? := .some "inl",
     target := { pp? := .some "q ∨ p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
     ],
   }
   let goal2r: Protocol.Goal := {
-    name := "_uniq.72",
+    name := "_uniq.74",
     userName? := .some "inr",
     target := { pp? := .some "q ∨ p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
+      { name := "_uniq.62", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
     ],
   }
   let goal3l: Protocol.Goal := {
-    name := "_uniq.78",
+    name := "_uniq.80",
     userName? := .some "inl.h",
     target := { pp? := .some "p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
     ],
   }
   [
@@ -174,6 +174,7 @@ def test_frontend_process : Test :=
         ("file",              .str file),
         ("invocations",       .bool true),
         ("sorrys",            .bool false),
+        ("typeErrorsAsGoals", .bool false),
         ("newConstants",      .bool false),
       ]
      ({
@@ -215,6 +216,7 @@ def test_frontend_process_sorry : Test :=
         ("file", .str file),
         ("invocations", .bool false),
         ("sorrys", .bool true),
+        ("typeErrorsAsGoals", .bool false),
         ("newConstants", .bool false),
       ]
      ({
@@ -233,9 +235,7 @@ def test_frontend_process_sorry : Test :=
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
-  let context: Context := {
+  let context: Context := {}
-    imports := ["Init"]
-  }
   let commands: MainM LSpec.TestSeq :=
     steps.foldlM (λ suite step => do
       let result ← step

Test/Main.lean

@@ -53,6 +53,7 @@ def main (args: List String) := do
     ("Proofs", Proofs.suite env_default),
     ("Delate", Delate.suite env_default),
     ("Serial", Serial.suite env_default),
+    ("Tactic/Assign", Tactic.Assign.suite env_default),
     ("Tactic/Congruence", Tactic.Congruence.suite env_default),
     ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
     ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),

Test/Metavar.lean

@@ -239,7 +239,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Roundtrip
@@ -253,7 +253,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Continuation should fail if the state does not exist:

Test/Proofs.lean

@@ -97,7 +97,7 @@ def test_identity: TestM Unit := do
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
     #[inner])
   let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
 
 -- Individual test cases
@@ -241,13 +241,15 @@ def test_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let fvP := "_uniq.10"
+  let [state1g0] := state1.goals | fail "Should have 1 goal"
-  let fvQ := "_uniq.13"
+  let (fvP, fvQ, fvH) ← state1.withContext state1g0 do
-  let fvH := "_uniq.16"
+    let lctx ← getLCtx
-  let state1g0 := "_uniq.17"
+    let #[fvP, fvQ, fvH] := lctx.getFVarIds.map (toString ·.name) |
+      panic! "Incorrect number of decls"
+    pure (fvP, fvQ, fvH)
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
     #[{
-      name := state1g0,
+      name := state1g0.name.toString,
       target := { pp? := .some "q ∨ p" },
       vars := #[
         { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
@@ -259,7 +261,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
 
   let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
   let tactic := "cases h"
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
@@ -269,14 +271,16 @@ def test_or_comm: TestM Unit := do
       return ()
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[branchGoal "inl" "p", branchGoal "inr" "q"])
-  let (caseL, caseR) := ("_uniq.64", "_uniq.77")
+  let [state2g0, state2g1] := state2.goals |
+    fail s!"Should have 2 goals, but it has {state2.goals.length}"
+  let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
     #[caseL, caseR])
   addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
   let state2parent ← state2.withParentContext do
-    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
   let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
   let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
   let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
@@ -292,8 +296,9 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   let state3_1parent ← state3_1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
-  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
+  let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
@@ -559,12 +564,15 @@ def test_nat_zero_add: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
+  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
+      fail "Incorrect number of goals"
+  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal mvarMotive.name.toString  [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
+      buildNamedGoal mvarMajor.name.toString   [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal mvarInduct.name.toString  [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "exact n"
@@ -647,13 +655,15 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let major := "_uniq.68"
+  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
+      fail "Incorrect number of goals"
+  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal major [("n", "Nat")] "Nat",
+      buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "intro x"
@@ -670,8 +680,7 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
+  let [eqL, eqR, eqT] := state3m2.goals | fail "Incorrect number of goals"
-  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
   let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
   let state2b ← match state3m2.resume [conduit] with
     | .ok state => pure state
@@ -681,20 +690,26 @@ def test_nat_zero_add_alt: TestM Unit := do
 
   let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
   let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
-  let fvN := "_uniq.63"
+  let fvN ← state2b.withContext conduit do
+    let lctx ← getLCtx
+    pure $ lctx.getFVarIds.get! 0 |>.name
   let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
-  let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
+  let substOf (mvarId: MVarId) := s!"(:subst (:mv {mvarId.name}) (:fv {fvN}) (:mv {mvarMajor}))"
+  let .num _ nL := eqL.name | fail "Incorrect form of mvar id"
+  let .num _ nR := eqR.name | fail "Incorrect form of mvar id"
+  let nL' := nL + 4
+  let nR' := nR + 5
   addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
     #[
       {
-        name := "_uniq.70",
+        name := mvarConduit.name.toString,
         userName? := .some "conduit",
         target := {
-          pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
+          pp? := .some s!"(?m.{nL'} ?m.{major} = ?m.{nR'} ?m.{major}) = (n + 0 = n)",
           sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
         },
         vars := #[{
-          name := fvN,
+          name := fvN.toString,
           userName := "n",
           type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
         }],
@@ -720,7 +735,6 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do
   let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
   checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]
 
-
 def test_tactic_failure_synthesize_placeholder : TestM Unit := do
   let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r")
   let state0 ← match state? with
@@ -737,19 +751,22 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
       return ()
 
   let tactic := "simpa [h] using And.imp_left h _"
-  let state2 ← match ← state1.tacticOn 0 tactic with
+  --let state2 ← match ← state1.tacticOn 0 tactic with
-    | .success state => pure state
+  --  | .success state => pure state
-    | other => do
+  --  | other => do
-      addTest $ assertUnreachable $ other.toString
+  --    addTest $ assertUnreachable $ other.toString
-      return ()
+  --    return ()
 
-  checkEq tactic ((← state2.serializeGoals).map (·.devolatilize))  #[
+  -- Volatile behaviour. This easily changes across Lean versions
-    buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r"
+
-  ]
+  --checkEq tactic ((← state2.serializeGoals).map (·.devolatilize))  #[
+  --  buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r"
+  --]
+
+  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
+  let message := s!"<Pantograph>:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
+  checkEq s!"{tactic} fails" messages #[message]
 
-  --let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
-  --let message := s!"<Pantograph>:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
-  --checkEq s!"{tactic} fails" messages #[message]
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [

Test/Tactic.lean

@@ -1,3 +1,4 @@
+import Test.Tactic.Assign
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse

Test/Tactic/Assign.lean

@@ -0,0 +1,33 @@
+import Lean.Meta
+import Lean.Elab
+import LSpec
+import Test.Common
+
+open Lean
+
+namespace Pantograph.Test.Tactic.Assign
+
+def test_draft : TestT Elab.TermElabM Unit := do
+  let expr := "forall (p : Prop), (p ∨ p) ∨ p"
+  let skeleton := "by\nhave a : p ∨ p := sorry\nsorry"
+  let expr ← parseSentence expr
+  Meta.forallTelescope expr $ λ _ body => do
+    let skeleton' ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := skeleton)
+      (fileName := ← getFileName) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.evalDraft skeleton'
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = ["p ∨ p", "(p ∨ p) ∨ p"])
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("draft", test_draft),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Assign

Test/Tactic/Congruence.lean

@@ -28,7 +28,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do
     let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse")
     addTest $ LSpec.check "apply" (results.length = 0)
     addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
-    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
+    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(List.reverse ?a₁ = List.reverse ?a₂) = (l1.reverse = l2.reverse)")
 def test_congr_arg : TestT Elab.TermElabM Unit := do
   let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
   let expr ← parseSentence expr
@@ -37,7 +37,7 @@ def test_congr_arg : TestT Elab.TermElabM Unit := do
     let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
     addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
-        (`α, "Sort ?u.70"),
+        (`α, "Sort ?u.73"),
         (`a₁, "?α"),
         (`a₂, "?α"),
         (`f, "?α → Nat"),
@@ -52,7 +52,7 @@ def test_congr_fun : TestT Elab.TermElabM Unit := do
     let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
     addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
-        (`α, "Sort ?u.159"),
+        (`α, "Sort ?u.165"),
         (`f₁, "?α → Nat"),
         (`f₂, "?α → Nat"),
         (`h, "?f₁ = ?f₂"),

Test/Tactic/MotivatedApply.lean

@@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
         "Nat → Prop",
         "Nat",
         "∀ (t : Nat), Nat.below t → ?motive t",
-        "?motive ?m.67 = (n + 0 = n)",
+        "?motive ?m.74 = (n + 0 = n)",
       ])
     addTest test
 
@@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
     let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let majorId := 67
+    let majorId := 74
     addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
         "Nat → Prop",
@@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
 
     addTest $ ← conduit.withContext do
       let t := toString (← Meta.ppExpr $ ← conduit.getType)
-      return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
+      return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [

doc/repl.md

@@ -13,6 +13,8 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   only the values of definitions are printed.
 * `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
   current environment to/from a file
+* `env.module_read { "module": <name }`: Reads a list of symbols from a module
+* `env.describe {}`: Describes the imports and modules in the current environment
 * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
   have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
 
@@ -33,6 +35,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 +47,13 @@ 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
+  <bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
-  a file, collecting the tactic invocations (`"invocations": true`), the
+  Executes the Lean frontend on a file, collecting the tactic invocations
-  sorrys and type errors into goal states (`"sorrys": true`), and new constants
+  (`"invocations": true`), the sorrys and type errors into goal states
-  (`"newConstants": true`). In the case of `sorrys`, this command additionally
+  (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
-  outputs the position of each captured `sorry`.
+  `sorrys`, this command additionally outputs the position of each captured
+  `sorry`. Warning: Behaviour is unstable in case of multiple `sorry`s. Use the
+  draft tactic if possible.
 
 ## Errors
 

flake.lock

@@ -42,11 +42,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1731711316,
+        "lastModified": 1736388194,
-        "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
+        "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "136fc6057c48de970579e960b62421e9c295b67d",
+        "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2",
         "type": "github"
       },
       "original": {

flake.nix

@@ -18,7 +18,8 @@
     lean4-nix,
     lspec,
     ...
-  } : flake-parts.lib.mkFlake { inherit inputs; } {
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
       flake = {
       };
       systems = [
@@ -27,36 +28,40 @@
         "x86_64-linux"
         "x86_64-darwin"
       ];
-    perSystem = { system, pkgs, ... }: let
+      perSystem = {
+        system,
+        pkgs,
+        ...
+      }: let
         pkgs = import nixpkgs {
           inherit system;
-        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
+          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
         };
         lspecLib = pkgs.lean.buildLeanPackage {
           name = "LSpec";
-        roots = [ "Main" "LSpec" ];
+          roots = ["Main" "LSpec"];
           src = "${lspec}";
         };
         project = pkgs.lean.buildLeanPackage {
           name = "Pantograph";
-        roots = [ "Pantograph" ];
+          roots = ["Pantograph"];
           src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
             src = ./.;
             filter = path: type:
-            !(pkgs.lib.hasInfix "/Test/" path) &&
+              !(pkgs.lib.hasInfix "/Test/" path)
-            !(pkgs.lib.hasSuffix ".md" path) &&
+              && !(pkgs.lib.hasSuffix ".md" path)
-            !(pkgs.lib.hasSuffix "Repl.lean" path);
+              && !(pkgs.lib.hasSuffix "Repl.lean" path);
           });
         };
         repl = pkgs.lean.buildLeanPackage {
           name = "Repl";
-        roots = [ "Main" "Repl" ];
+          roots = ["Main" "Repl"];
-        deps = [ project ];
+          deps = [project];
           src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
             src = ./.;
             filter = path: type:
-            !(pkgs.lib.hasInfix "/Test/" path) &&
+              !(pkgs.lib.hasInfix "/Test/" path)
-            !(pkgs.lib.hasSuffix ".md" path);
+              && !(pkgs.lib.hasSuffix ".md" path);
           });
         };
         test = pkgs.lean.buildLeanPackage {
@@ -64,8 +69,8 @@
           # NOTE: The src directory must be ./. since that is where the import
           # root begins (e.g. `import Test.Environment` and not `import
           # Environment`) and thats where `lakefile.lean` resides.
-        roots = [ "Test.Main" ];
+          roots = ["Test.Main"];
-        deps = [ lspecLib repl ];
+          deps = [lspecLib repl];
           src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
             src = ./.;
             filter = path: type:
@@ -84,15 +89,17 @@
           leanPkgs = pkgs.lean;
         };
         checks = {
-        test = pkgs.runCommand "test" {
+          test =
-          buildInputs = [ test.executable pkgs.lean.lean-all ];
+            pkgs.runCommand "test" {
+              buildInputs = [test.executable pkgs.lean.lean-all];
             } ''
               #export LEAN_SRC_PATH="${./.}"
               ${test.executable}/bin/test > $out
             '';
         };
+        formatter = pkgs.alejandra;
         devShells.default = pkgs.mkShell {
-        buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
+          buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
         };
       };
     };

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.15.0