From 4f5950ed7878f17de50d9b535b3bd030f1965af8 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 12:26:46 -0700 Subject: [PATCH] feat: Convert holes to goals --- Pantograph/Frontend/Elab.lean | 29 ++++++++++++++++++++-- Pantograph/Goal.lean | 11 +++++++++ Pantograph/Protocol.lean | 1 + Repl.lean | 45 +++++++++++++++++++++++------------ Test/Integration.lean | 33 ++++++++++++++++++++++++- 5 files changed, 101 insertions(+), 18 deletions(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index e29d8f9..8deac23 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -5,6 +5,7 @@ import Lean.Elab.InfoTree import Pantograph.Protocol import Pantograph.Frontend.Basic +import Pantograph.Goal open Lean @@ -132,7 +133,7 @@ partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pre /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics, each equipped with its relevant `ContextInfo`, and any children info trees. -/ -def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := +private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := let infos := findAllInfo t none fun i => match i with | .ofTacticInfo _ => true | _ => false @@ -153,8 +154,32 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty let tactic ← invocation.ctx.runMetaM {} do - let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ + let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ return t.pretty return { goalBefore, goalAfter, tactic } +private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.TermInfo := + let infos := findAllInfo t none fun i => match i with + | .ofTermInfo { expectedType?, expr, stx, .. } => + expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry + | _ => false + infos.filterMap fun p => match p with + | (.ofTermInfo i, _, _) => .some i + | _ => none + +@[export pantograph_frontend_collect_sorrys_m] +def collectSorrys (step: CompilationStep) : List Elab.TermInfo := + step.trees.bind collectSorrysInTree + +@[export pantograph_frontend_sorrys_to_goal_state] +def sorrysToGoalState (sorrys : List Elab.TermInfo) : MetaM GoalState := do + assert! !sorrys.isEmpty + let goals ← sorrys.mapM λ termInfo => Meta.withLCtx termInfo.lctx #[] do + let type := termInfo.expectedType?.get! + let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type + return mvar.mvarId! + GoalState.createFromMVars goals (root := { name := .anonymous }) + + + end Pantograph.Frontend diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b4a6fc7..79e3004 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -46,6 +46,15 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do savedState, parentMVar? := .none, } +@[export pantograph_goal_state_create_from_mvars_m] +protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do + let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState + let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals } |>.run' {} + return { + root, + savedState, + parentMVar? := .none, + } @[export pantograph_goal_state_is_conv] protected def GoalState.isConv (state: GoalState): Bool := state.convMVar?.isSome @@ -143,6 +152,8 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except @[export pantograph_goal_state_root_expr] protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do + if goalState.root.name == .anonymous then + .none let expr ← goalState.mctx.eAssignment.find? goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) if expr.hasExprMVar then diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 12a75a2..26cae09 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -302,6 +302,7 @@ structure FrontendProcessResult where -- String boundaries of compilation units units: List (Nat × Nat) invocations?: Option (List InvokedTactic) := .none + goalStates?: Option (List (Nat × Array Goal)) := .none deriving Lean.ToJson abbrev CR α := Except InteractionError α diff --git a/Repl.lean b/Repl.lean index 2f92eb8..1277e73 100644 --- a/Repl.lean +++ b/Repl.lean @@ -54,6 +54,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do where errorCommand := errorI "command" errorIndex := errorI "index" + newGoalState (goalState: GoalState) : MainM Nat := do + let state ← get + let stateId := state.nextId + set { state with + goalStates := state.goalStates.insert stateId goalState, + nextId := state.nextId + 1 + } + return stateId -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -95,7 +103,6 @@ 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 state ← get let env ← Lean.MonadEnv.getEnv let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) @@ -108,11 +115,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match expr? with | .error error => return .error error | .ok goalState => - let stateId := state.nextId - set { state with - goalStates := state.goalStates.insert stateId goalState, - nextId := state.nextId + 1 - } + let stateId ← newGoalState goalState return .ok { stateId, root := goalState.root.name.toString } goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do let state ← get @@ -151,11 +154,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals" pure result | false, _ => pure nextGoalState - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert state.nextId nextGoalState, - nextId := state.nextId + 1, - } + let nextStateId ← newGoalState nextGoalState let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' return .ok { nextStateId? := .some nextStateId, @@ -202,6 +201,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let result ← runMetaInMainM <| goalPrint goalState state.options return .ok result frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do + let options := (← get).options try let (fileName, file) ← match args.fileName?, args.file? with | .some fileName, .none => do @@ -222,14 +222,29 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Frontend.collectTacticsFromCompilationStep step else pure [] - return (unitBoundary, tacticInvocations) + let sorrys := if args.sorrys then + Frontend.collectSorrys step + else + [] + return (unitBoundary, tacticInvocations, sorrys) let li ← m.run context |>.run' state - let units := li.map λ (unit, _) => unit + let units := li.map λ (unit, _, _) => unit let invocations? := if args.invocations then - .some $ li.bind λ (_, invocations) => invocations + .some $ li.bind λ (_, invocations, _) => invocations else .none - return .ok { units, invocations? } + let goalStates? ← if args.sorrys then do + let stateIds ← li.filterMapM λ (_, _, sorrys) => do + if sorrys.isEmpty then + return .none + let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys + let stateId ← newGoalState goalState + let goals ← goalSerialize goalState options + return .some (stateId, goals) + pure $ .some stateIds + else + pure .none + return .ok { units, invocations?, goalStates? } catch e => return .error $ errorI "frontend" (← e.toMessageData.toString) diff --git a/Test/Integration.lean b/Test/Integration.lean index 3681d4e..4a8e418 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -192,6 +192,36 @@ def test_frontend_process : Test := }: Protocol.FrontendProcessResult), ] +example : 1 + 2 = 3 := rfl +example (p: Prop): p → p := by simp + +def test_frontend_process_sorry : Test := + let solved := "example : 1 + 2 = 3 := rfl\n" + let withSorry := "example (p: Prop): p → p := sorry" + [ + let file := s!"{solved}{withSorry}" + let goal1: Protocol.Goal := { + name := "_uniq.1", + target := { pp? := .some "p → p" }, + vars := #[{ name := "_uniq.168", userName := "p", type? := .some { pp? := .some "Prop" }}], + } + step "frontend.process" + [ + ("file", .str file), + ("invocations", .bool false), + ("sorrys", .bool true), + ] + ({ + units := [ + (0, solved.utf8ByteSize), + (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize), + ], + goalStates? := [ + (0, #[goal1]), + ] + }: Protocol.FrontendProcessResult), + ] + def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do -- Setup the environment for execution @@ -214,7 +244,8 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := ("Manual Mode", test_automatic_mode false), ("Automatic Mode", test_automatic_mode true), ("env.add env.inspect", test_env_add_inspect), - ("frontend.process", test_frontend_process), + ("frontend.process invocation", test_frontend_process), + ("frontend.process sorry", test_frontend_process_sorry), ] tests.map (fun (name, test) => (name, runTest env test))