From 9a9659fdb2dfd4981773034c19b8f6601049f76d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 26 Jun 2025 14:22:51 -0700 Subject: [PATCH] feat(delate): Show fragments for each goal --- Pantograph/Delate.lean | 9 ++++++--- Pantograph/Protocol.lean | 17 +++++++++++------ Test/Tactic/Fragment.lean | 20 ++++++++++---------- doc/repl.md | 21 ++++++++++++--------- 4 files changed, 39 insertions(+), 28 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index ca65175..8f7c1cd 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -454,7 +454,6 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol. dependentMVars?, } - /-- Adapted from ppGoal -/ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none) : MetaM Protocol.Goal := do @@ -520,7 +519,6 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava return { name := goal.name.toString, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), - isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serializeExpression options (← instantiate mvarDecl.type)), vars := vars.reverse.toArray } @@ -535,10 +533,15 @@ protected def GoalState.serializeGoals state.restoreMetaM let goals := state.goals.toArray goals.mapM fun goal => do + let fragment := match state.fragments[goal]? with + | .none => .tactic + | .some $ .calc .. => .calc + | .some $ .conv .. => .conv + | .some $ .convSentinel .. => .conv match state.mctx.findDecl? goal with | .some mvarDecl => let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := .none) - pure serializedGoal + pure { serializedGoal with fragment } | .none => throwError s!"Metavariable does not exist in context {goal.name}" /-- Print the metavariables in a readable format -/ diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 8773b1d..4c02f4d 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -60,16 +60,21 @@ structure Variable where type?: Option Expression := .none value?: Option Expression := .none deriving Lean.ToJson +inductive Fragment where + | tactic + | conv + | calc + deriving BEq, DecidableEq, Repr, Lean.ToJson structure Goal where - name: String := "" /-- Name of the metavariable -/ - userName?: Option String := .none - /-- Is the goal in conversion mode -/ - isConversion: Bool := false + name : String := "" + /-- User-facing name -/ + userName? : Option String := .none + fragment : Fragment := .tactic /-- target expression type -/ - target: Expression + target : Expression /-- Variables -/ - vars: Array Variable := #[] + vars : Array Variable := #[] deriving Lean.ToJson diff --git a/Test/Tactic/Fragment.lean b/Test/Tactic/Fragment.lean index 0c54b7a..51b3a3e 100644 --- a/Test/Tactic/Fragment.lean +++ b/Test/Tactic/Fragment.lean @@ -46,7 +46,7 @@ def test_conv_simple: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals).map (·.devolatilize) = - #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }]) + #[{ interiorGoal [] "a + b + c1 = b + a + c2" with fragment := .conv }]) let convTactic := "rhs" let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with @@ -55,7 +55,7 @@ def test_conv_simple: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check s!" {convTactic} (discard)" ((← state3R.serializeGoals).map (·.devolatilize) = - #[{ interiorGoal [] "b + a + c2" with isConversion := true }]) + #[{ interiorGoal [] "b + a + c2" with fragment := .conv }]) let convTactic := "lhs" let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with @@ -64,7 +64,7 @@ def test_conv_simple: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check s!" {convTactic}" ((← state3L.serializeGoals).map (·.devolatilize) = - #[{ interiorGoal [] "a + b + c1" with isConversion := true }]) + #[{ interiorGoal [] "a + b + c1" with fragment := .conv }]) let convTactic := "congr" let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with @@ -74,8 +74,8 @@ def test_conv_simple: TestM Unit := do return () addTest $ LSpec.check s!" {convTactic}" ((← state4.serializeGoals).map (·.devolatilize) = #[ - { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" }, - { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" } + { interiorGoal [] "a + b" with fragment := .conv, userName? := .some "a" }, + { interiorGoal [] "c1" with fragment := .conv, userName? := .some "a" } ]) let convTactic := "rw [Nat.add_comm]" @@ -85,7 +85,7 @@ def test_conv_simple: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check s!" · {convTactic}" ((← state5_1.serializeGoals).map (·.devolatilize) = - #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }]) + #[{ interiorGoal [] "b + a" with fragment := .conv, userName? := .some "a" }]) let convTactic := "rfl" let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with @@ -159,7 +159,7 @@ def test_conv_unshielded : TestM Unit := do let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed" checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize)) #[ - { interiorGoal [] "y" with isConversion := true }, + { interiorGoal [] "y" with fragment := .conv }, { interiorGoal [] "p" with userName? := "right", }, ] let tactic := "rw [←hi]" @@ -206,13 +206,13 @@ def test_conv_unfinished : TestM Unit := do let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed" checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize)) #[ - { interiorGoal [] "y" with isConversion := true }, + { interiorGoal [] "y" with fragment := .conv }, ] let tactic := "rw [hyz]" let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed" checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize)) #[ - { interiorGoal [] "z" with isConversion := true }, + { interiorGoal [] "z" with fragment := .conv }, ] checkTrue " (fragment)" $ state.fragments.contains state.mainGoal?.get! checkTrue " (fragment parent)" $ state.fragments.contains convParent @@ -260,7 +260,7 @@ def test_calc: TestM Unit := do addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals).map (·.devolatilize) = #[ { interiorGoal [] "a + b = b + c" with userName? := .some "calc" }, - interiorGoal [] "b + c = c + d" + { interiorGoal [] "b + c = c + d" with fragment := .calc }, ]) addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone) addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome) diff --git a/doc/repl.md b/doc/repl.md index 180505c..02d1735 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -13,7 +13,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va only the values of definitions are printed. * `env.save { "path": }`, `env.load { "path": }`: Save/Load the current environment to/from a file -* `env.module_read { "module": }`: Reads a list of symbols from a module * `env.describe {}`: Describes the imports and modules in the current environment * `options.set { key: value, ... }`: Set one or more options (not Lean options; those have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` @@ -28,16 +28,19 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va * `options.print`: Display the current set of options * `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: Start a new proof from a given expression or symbol -* `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a - given goal. The tactic is supplied as additional key-value pairs in one of the following formats: - - `{ "tactic": }`: Execute an ordinary tactic - - `{ "expr": }`: Assign the given proof term to the current goal - - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal - - `{ "calc": }`: Execute one step of a `calc` tactic. Each step must +* `goal.tactic {"stateId": , ["goalId": ], ["autoResume": ], ...}`: + Execute a tactic string on a given goal site. The tactic is supplied as additional + key-value pairs in one of the following formats: + - `{ "tactic": }`: Executes a tactic in the current mode + - `{ "mode": }`: Enter a different tactic mode. The permitted values + are `tactic` (default), `conv`, `calc`. In case of `calc`, each step must be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set to the previous `rhs`. - - `{ "conv": }`: Enter or exit conversion tactic mode. - - `{ "draft": }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed. + - `{ "expr": }`: Assign the given proof term to the current goal + - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal + - `{ "let": , "binderName": }`: Execute `let` and creates a branch goal + - `{ "draft": }`: Draft an expression with `sorry`s, turning them into + goals. Coupling is not allowed. If the `goals` field does not exist, the tactic execution has failed. Read `messages` to find the reason. * `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: