From 162c317990e2f1ca0dd933ede8d86f07a401ba25 Mon Sep 17 00:00:00 2001 From: shanjiaming Date: Sun, 29 Jun 2025 15:30:06 -0700 Subject: [PATCH] add removeProofState --- REPL/JSON.lean | 10 ++++++++++ REPL/Main.lean | 20 ++++++++++++++++---- test/remove_proof_step.expected.out | 24 ++++++++++++++++++++++++ test/remove_proof_step.in | 9 +++++++++ 4 files changed, 59 insertions(+), 4 deletions(-) create mode 100644 test/remove_proof_step.expected.out create mode 100644 test/remove_proof_step.in diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 24db8402..634c4b98 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -169,6 +169,11 @@ structure Error where message : String deriving ToJson, FromJson +/-- Simple success response. -/ +structure SuccessResponse where + success : Bool := true +deriving ToJson, FromJson + structure PickleEnvironment where env : Nat pickleTo : System.FilePath @@ -188,4 +193,9 @@ structure UnpickleProofState where env : Option Nat deriving ToJson, FromJson +/-- Remove a proof state. -/ +structure RemoveProofState where + removeProofState : Nat +deriving ToJson, FromJson + end REPL diff --git a/REPL/Main.lean b/REPL/Main.lean index b00b6833..fa598e29 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -71,7 +71,7 @@ structure State where Declarations with containing `sorry` record a proof state at each sorry, and report the numerical index for the recorded state at each sorry. -/ - proofStates : Array ProofSnapshot := #[] + proofStates : Array (Option ProofSnapshot) := #[] /-- The Lean REPL monad. @@ -91,7 +91,7 @@ def recordCommandSnapshot (state : CommandSnapshot) : M m Nat := do /-- Record a `ProofSnapshot` into the REPL state, returning its index for future use. -/ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do let id := (← get).proofStates.size - modify fun s => { s with proofStates := s.proofStates.push proofState } + modify fun s => { s with proofStates := s.proofStates.push (some proofState) } return id def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId)) @@ -271,7 +271,7 @@ def unpickleCommandSnapshot (n : UnpickleEnvironment) : M IO CommandResponse := /-- Pickle a `ProofSnapshot`, generating a JSON response. -/ -- This generates a new identifier, which perhaps is not what we want? def pickleProofSnapshot (n : PickleProofState) : M m (ProofStepResponse ⊕ Error) := do - match (← get).proofStates[n.proofState]? with + match (← get).proofStates[n.proofState]?.join with | none => return .inr ⟨"Unknown proof State."⟩ | some proofState => discard <| proofState.pickle n.pickleTo @@ -289,6 +289,14 @@ def unpickleProofSnapshot (n : UnpickleProofState) : M IO (ProofStepResponse ⊕ let (proofState, _) ← ProofSnapshot.unpickle n.unpickleProofStateFrom cmdSnapshot? Sum.inl <$> createProofStepReponse proofState +/-- Remove a proof state from the REPL state. -/ +def removeProofState (n : RemoveProofState) : M m (SuccessResponse ⊕ Error) := do + match (← get).proofStates[n.removeProofState]?.join with + | none => return .inr ⟨"Unknown proof state."⟩ + | some _ => + modify fun s => { s with proofStates := s.proofStates.set! n.removeProofState none } + return .inl (SuccessResponse.mk true) + /-- Run a command, returning the id of the new environment, and any messages and sorries. -/ @@ -352,7 +360,7 @@ Run a single tactic, returning the id of the new proof statement, and the new go -/ -- TODO detect sorries? def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error) := do - match (← get).proofStates[s.proofState]? with + match (← get).proofStates[s.proofState]?.join with | none => return .inr ⟨"Unknown proof state."⟩ | some proofState => try @@ -387,6 +395,7 @@ inductive Input | unpickleEnvironment : REPL.UnpickleEnvironment → Input | pickleProofSnapshot : REPL.PickleProofState → Input | unpickleProofSnapshot : REPL.UnpickleProofState → Input +| removeProofState : REPL.RemoveProofState → Input /-- Parse a user input string to an input command. -/ def parse (query : String) : IO Input := do @@ -405,6 +414,8 @@ def parse (query : String) : IO Input := do | .error _ => match fromJson? j with | .ok (r : REPL.UnpickleProofState) => return .unpickleProofSnapshot r | .error _ => match fromJson? j with + | .ok (r : REPL.RemoveProofState) => return .removeProofState r + | .error _ => match fromJson? j with | .ok (r : REPL.Command) => return .command r | .error _ => match fromJson? j with | .ok (r : REPL.File) => return .file r @@ -433,6 +444,7 @@ where loop : M IO Unit := do | .unpickleEnvironment r => return toJson (← unpickleCommandSnapshot r) | .pickleProofSnapshot r => return toJson (← pickleProofSnapshot r) | .unpickleProofSnapshot r => return toJson (← unpickleProofSnapshot r) + | .removeProofState r => return toJson (← removeProofState r) printFlush "\n" -- easier to parse the output if there are blank lines loop diff --git a/test/remove_proof_step.expected.out b/test/remove_proof_step.expected.out new file mode 100644 index 00000000..359dbd2d --- /dev/null +++ b/test/remove_proof_step.expected.out @@ -0,0 +1,24 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 18}, + "goal": "⊢ Nat", + "endPos": {"line": 1, "column": 23}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 4}, + "endPos": {"line": 1, "column": 5}, + "data": "declaration uses 'sorry'"}], + "env": 0} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, + "goals": ["⊢ Int"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 2, + "goals": ["t : Nat\n⊢ Nat"]} + +{"success": true} + +{"message": "Unknown proof state."} + diff --git a/test/remove_proof_step.in b/test/remove_proof_step.in new file mode 100644 index 00000000..f9a0314f --- /dev/null +++ b/test/remove_proof_step.in @@ -0,0 +1,9 @@ +{"cmd" : "def f : Nat := by sorry"} + +{"tactic": "apply Int.natAbs", "proofState": 0} + +{"tactic": "have t : Nat := 42", "proofState": 0} + +{"removeProofState": 2} + +{"tactic": "exact t", "proofState": 2}