feat: Add REPL function for root expression
This commit is contained in:
parent
ca7a081cac
commit
427d819349
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue