feat: Add REPL function for root expression

This commit is contained in:
Leni Aniva 2023-10-27 15:41:12 -07:00
parent 41e1f64d44
commit 045181356c
6 changed files with 36 additions and 16 deletions

View File

@ -39,6 +39,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| "goal.start" => run goal_start
| "goal.tactic" => run goal_tactic
| "goal.delete" => run goal_delete
| "goal.print" => run goal_print
| cmd =>
let error: Protocol.InteractionError :=
errorCommand s!"Unknown command {cmd}"
@ -174,5 +175,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates
set { state with goalStates }
return .ok {}
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
let state ← get
match state.goalStates.get? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => do
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
return .ok {
root?,
}
end Pantograph

View File

@ -190,7 +190,7 @@ protected def GoalState.continue (target: GoalState) (graftee: GoalState): Excep
newMVars := graftee.newMVars,
}
protected def GoalState.rootExpr (goalState: GoalState): Option Expr :=
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
let expr := goalState.mctx.eAssignment.find! goalState.root
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
if expr.hasMVar then

View File

@ -171,6 +171,15 @@ structure GoalDeleteResult where
deriving Lean.ToJson
structure GoalPrint where
stateId: Nat
deriving Lean.FromJson
structure GoalPrintResult where
-- The root expression
root?: Option Expression
deriving Lean.ToJson
-- Diagnostic Options, not available in REPL
structure GoalDiag where
printContext: Bool := true
printValue: Bool := true
printNewMVars: Bool := false

View File

@ -269,7 +269,7 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
/-- Print the metavariables in a readable format -/
protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrint := {}): MetaM Unit := do
protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
let savedState := goalState.savedState
savedState.term.meta.restore
let goals := savedState.tactic.goals

View File

@ -76,8 +76,9 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
have to be set via command line arguments.), for options, see `Pantograph/Commands.lean`
- `options.print`: Display the current set of options
- `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
- `goal.tactic {"goalId": <id>, "tactic": <tactic>}`: Execute a tactic string on a given goal
- `goal.remove {"goalIds": [<id>]}"`: Remove a bunch of stored goals.
- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
- `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
- `goal.print {"stateId": <id>}"`: Print a goal state
- `stat`: Display resource usage
## Errors

View File

@ -188,21 +188,21 @@ def proof_arith: TestM Unit := do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intros" (state1.goals.length = 1)
addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
addTest $ LSpec.check "(2 root)" state2.rootExpr.isNone
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "assumption" state3.goals.isEmpty
addTest $ LSpec.check "(3 root)" state3.rootExpr.isSome
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
return ()
-- Two ways to write the same theorem
@ -255,7 +255,7 @@ def proof_or_comm: TestM Unit := do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr.isNone
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with
| .success state => pure state
| other => do
@ -268,7 +268,7 @@ def proof_or_comm: TestM Unit := do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_2.goals.isEmpty
addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr.isNone
addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
-- Ensure the proof can continue from `state4_2`.
let state2b ← match state2.continue state4_2 with
| .error msg => do
@ -288,7 +288,7 @@ def proof_or_comm: TestM Unit := do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr.isSome
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome
return ()
where
@ -319,14 +319,14 @@ def proof_m_couple: TestM Unit := do
return ()
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-- Set m to 3
let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "(1b root)" state2.rootExpr.isNone
addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
let state1b ← match state1.continue state2 with
| .error msg => do
addTest $ assertUnreachable $ msg
@ -334,7 +334,7 @@ def proof_m_couple: TestM Unit := do
| .ok state => pure state
addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ 3", .some "3 ≤ 5"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr.isNone
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
return ()
def proof_proposition_generation: TestM Unit := do
@ -355,7 +355,7 @@ def proof_proposition_generation: TestM Unit := do
buildGoal [] "?fst" (caseName? := .some "snd"),
buildGoal [] "Prop" (caseName? := .some "fst")
])
addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with
| .success state => pure state
@ -364,7 +364,7 @@ def proof_proposition_generation: TestM Unit := do
return ()
addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
addTest $ LSpec.test "(2 root)" state2.rootExpr.isNone
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
| .success state => pure state
@ -373,7 +373,7 @@ def proof_proposition_generation: TestM Unit := do
return ()
addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
#[])
addTest $ LSpec.test "(3 root)" state3.rootExpr.isSome
addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
return ()
def suite: IO LSpec.TestSeq := do