feat: Convert holes to goals

This commit is contained in:
Leni Aniva 2024-09-09 12:26:46 -07:00
parent 08fb53c020
commit 4f5950ed78
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
5 changed files with 101 additions and 18 deletions

View File

@ -5,6 +5,7 @@ import Lean.Elab.InfoTree
import Pantograph.Protocol import Pantograph.Protocol
import Pantograph.Frontend.Basic import Pantograph.Frontend.Basic
import Pantograph.Goal
open Lean 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, /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
each equipped with its relevant `ContextInfo`, and any children info trees. -/ 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 let infos := findAllInfo t none fun i => match i with
| .ofTacticInfo _ => true | .ofTacticInfo _ => true
| _ => false | _ => false
@ -153,8 +154,32 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
let tactic ← invocation.ctx.runMetaM {} do 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 t.pretty
return { goalBefore, goalAfter, tactic } 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 end Pantograph.Frontend

View File

@ -46,6 +46,15 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
savedState, savedState,
parentMVar? := .none, 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] @[export pantograph_goal_state_is_conv]
protected def GoalState.isConv (state: GoalState): Bool := protected def GoalState.isConv (state: GoalState): Bool :=
state.convMVar?.isSome state.convMVar?.isSome
@ -143,6 +152,8 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
@[export pantograph_goal_state_root_expr] @[export pantograph_goal_state_root_expr]
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do 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 ← goalState.mctx.eAssignment.find? goalState.root
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
if expr.hasExprMVar then if expr.hasExprMVar then

View File

@ -302,6 +302,7 @@ structure FrontendProcessResult where
-- String boundaries of compilation units -- String boundaries of compilation units
units: List (Nat × Nat) units: List (Nat × Nat)
invocations?: Option (List InvokedTactic) := .none invocations?: Option (List InvokedTactic) := .none
goalStates?: Option (List (Nat × Array Goal)) := .none
deriving Lean.ToJson deriving Lean.ToJson
abbrev CR α := Except InteractionError α abbrev CR α := Except InteractionError α

View File

@ -54,6 +54,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
where where
errorCommand := errorI "command" errorCommand := errorI "command"
errorIndex := errorI "index" 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 -- Command Functions
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get 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 options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
return .ok (← get).options return .ok (← get).options
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
| .some expr, .none => goalStartExpr expr (args.levels.getD #[]) | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
@ -108,11 +115,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
match expr? with match expr? with
| .error error => return .error error | .error error => return .error error
| .ok goalState => | .ok goalState =>
let stateId := state.nextId let stateId ← newGoalState goalState
set { state with
goalStates := state.goalStates.insert stateId goalState,
nextId := state.nextId + 1
}
return .ok { stateId, root := goalState.root.name.toString } return .ok { stateId, root := goalState.root.name.toString }
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
let state ← get 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" let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals"
pure result pure result
| false, _ => pure nextGoalState | false, _ => pure nextGoalState
let nextStateId := state.nextId let nextStateId ← newGoalState nextGoalState
set { state with
goalStates := state.goalStates.insert state.nextId nextGoalState,
nextId := state.nextId + 1,
}
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
return .ok { return .ok {
nextStateId? := .some nextStateId, nextStateId? := .some nextStateId,
@ -202,6 +201,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let result ← runMetaInMainM <| goalPrint goalState state.options let result ← runMetaInMainM <| goalPrint goalState state.options
return .ok result return .ok result
frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
let options := (← get).options
try try
let (fileName, file) ← match args.fileName?, args.file? with let (fileName, file) ← match args.fileName?, args.file? with
| .some fileName, .none => do | .some fileName, .none => do
@ -222,14 +222,29 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
Frontend.collectTacticsFromCompilationStep step Frontend.collectTacticsFromCompilationStep step
else else
pure [] 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 li ← m.run context |>.run' state
let units := li.map λ (unit, _) => unit let units := li.map λ (unit, _, _) => unit
let invocations? := if args.invocations then let invocations? := if args.invocations then
.some $ li.bind λ (_, invocations) => invocations .some $ li.bind λ (_, invocations, _) => invocations
else else
.none .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 => catch e =>
return .error $ errorI "frontend" (← e.toMessageData.toString) return .error $ errorI "frontend" (← e.toMessageData.toString)

View File

@ -192,6 +192,36 @@ def test_frontend_process : Test :=
}: Protocol.FrontendProcessResult), }: 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 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
-- Setup the environment for execution -- 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), ("Manual Mode", test_automatic_mode false),
("Automatic Mode", test_automatic_mode true), ("Automatic Mode", test_automatic_mode true),
("env.add env.inspect", test_env_add_inspect), ("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)) tests.map (fun (name, test) => (name, runTest env test))