From 427d819349ed5ece7e0904f5485323452ab48b09 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 27 Oct 2023 15:41:12 -0700 Subject: [PATCH] feat: Add REPL function for root expression --- Pantograph.lean | 10 ++++++++++ Pantograph/Goal.lean | 2 +- Pantograph/Protocol.lean | 9 +++++++++ Pantograph/Serial.lean | 2 +- README.md | 5 +++-- Test/Proofs.lean | 24 ++++++++++++------------ 6 files changed, 36 insertions(+), 16 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index dd25e9f..00782d5 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -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 diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 3be34ad..78a4194 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -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 diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 62700c4..e379782 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -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 diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 1a07444..62321bd 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -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 diff --git a/README.md b/README.md index 442b57d..0c19a3a 100644 --- a/README.md +++ b/README.md @@ -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": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol -- `goal.tactic {"goalId": , "tactic": }`: Execute a tactic string on a given goal -- `goal.remove {"goalIds": []}"`: Remove a bunch of stored goals. +- `goal.tactic {"stateId": , "goalId": , ["tactic": ], ["expr": ]}`: Execute a tactic string on a given goal +- `goal.remove {"stateIds": []}"`: Remove a bunch of stored goals. +- `goal.print {"stateId": }"`: Print a goal state - `stat`: Display resource usage ## Errors diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 809cf50..a726627 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -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