From 0725d865de5dbe0195c6cafa8e81b42f9e967fc5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 10 Dec 2024 12:40:00 -0800 Subject: [PATCH 1/2] feat: Print value of arbitrary mvar in goal state --- Pantograph/Library.lean | 16 +++++++++++----- Pantograph/Protocol.lean | 4 ++++ Repl.lean | 3 ++- 3 files changed, 17 insertions(+), 6 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 20c7c9b..ee17fa5 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -138,16 +138,22 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array runMetaM <| state.serializeGoals (parent := .none) options @[export pantograph_goal_print_m] -def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult := +def goalPrint (state: GoalState) (extraMVars : Array String) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult := runMetaM do state.restoreMetaM return { - root? := ← state.rootExpr?.mapM (λ expr => + root? := ← state.rootExpr?.mapM λ expr => state.withRootContext do - serializeExpression options (← instantiateAll expr)), - parent? := ← state.parentExpr?.mapM (λ expr => + serializeExpression options (← instantiateAll expr), + parent? := ← state.parentExpr?.mapM λ expr => state.withParentContext do - serializeExpression options (← instantiateAll expr)), + serializeExpression options (← instantiateAll expr), + extraMVars := ← extraMVars.mapM λ mvarId => do + let mvarId: MVarId := { name := mvarId.toName } + let .some _ ← mvarId.findDecl? | return {} + state.withContext mvarId do + let .some expr ← getExprMVarAssignment? mvarId | return {} + serializeExpression options (← instantiateAll expr), } @[export pantograph_goal_tactic_m] diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 0cb6cac..9b00dfe 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -271,12 +271,16 @@ structure GoalDeleteResult where structure GoalPrint where stateId: Nat + -- Print values of extra mvars + extraMVars?: Option (Array String) := .none deriving Lean.FromJson structure GoalPrintResult where -- The root expression root?: Option Expression := .none -- The filling expression of the parent goal parent?: Option Expression + + extraMVars: Array Expression := #[] deriving Lean.ToJson -- Diagnostic Options, not available in REPL diff --git a/Repl.lean b/Repl.lean index 3f8a3c6..0dd92d2 100644 --- a/Repl.lean +++ b/Repl.lean @@ -222,7 +222,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let .some goalState := state.goalStates[args.stateId]? | return .error $ errorIndex s!"Invalid state index {args.stateId}" - let result ← runMetaInMainM <| goalPrint goalState state.options + let extraMVars := args.extraMVars?.getD #[] + let result ← runMetaInMainM <| goalPrint goalState extraMVars state.options return .ok result goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do let state ← get -- 2.44.1 From 2f732a7f2094b0226990d4c89cd9586b51fc6f0b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 16:49:52 -0800 Subject: [PATCH 2/2] feat: Print goals in `goal.print` --- Pantograph/Library.lean | 47 +++++++++++++++++++++++++--------------- Pantograph/Protocol.lean | 13 ++++++++--- Repl.lean | 9 ++++++-- Test/Integration.lean | 2 +- 4 files changed, 48 insertions(+), 23 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index ee17fa5..bb094b6 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -138,23 +138,36 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array runMetaM <| state.serializeGoals (parent := .none) options @[export pantograph_goal_print_m] -def goalPrint (state: GoalState) (extraMVars : Array String) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult := - runMetaM do - state.restoreMetaM - return { - root? := ← state.rootExpr?.mapM λ expr => - state.withRootContext do - serializeExpression options (← instantiateAll expr), - parent? := ← state.parentExpr?.mapM λ expr => - state.withParentContext do - serializeExpression options (← instantiateAll expr), - extraMVars := ← extraMVars.mapM λ mvarId => do - let mvarId: MVarId := { name := mvarId.toName } - let .some _ ← mvarId.findDecl? | return {} - state.withContext mvarId do - let .some expr ← getExprMVarAssignment? mvarId | return {} - serializeExpression options (← instantiateAll expr), - } +def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options) + : CoreM Protocol.GoalPrintResult := runMetaM do + state.restoreMetaM + + let root? ← if rootExpr then + state.rootExpr?.mapM λ expr => state.withRootContext do + serializeExpression options (← instantiateAll expr) + else + pure .none + let parent? ← if parentExpr then + state.parentExpr?.mapM λ expr => state.withParentContext do + serializeExpression options (← instantiateAll expr) + else + pure .none + let goals ← if goals then + goalSerialize state options + else + pure #[] + let extraMVars ← extraMVars.mapM λ mvarId => do + let mvarId: MVarId := { name := mvarId.toName } + let .some _ ← mvarId.findDecl? | return {} + state.withContext mvarId do + let .some expr ← getExprMVarAssignment? mvarId | return {} + serializeExpression options (← instantiateAll expr) + return { + root?, + parent?, + goals, + extraMVars, + } @[export pantograph_goal_tactic_m] def goalTactic (state: GoalState) (goal: MVarId) (tactic: String): CoreM TacticResult := diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 88100a1..90ac149 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -271,15 +271,22 @@ structure GoalDeleteResult where structure GoalPrint where stateId: Nat - -- Print values of extra mvars + + -- Print root? + rootExpr?: Option Bool := .some False + -- Print the parent expr? + parentExpr?: Option Bool := .some False + -- Print goals? + goals?: Option Bool := .some False + -- Print values of extra mvars? extraMVars?: Option (Array String) := .none deriving Lean.FromJson structure GoalPrintResult where -- The root expression root?: Option Expression := .none -- The filling expression of the parent goal - parent?: Option Expression - + parent?: Option Expression := .none + goals: Array Goal := #[] extraMVars: Array Expression := #[] deriving Lean.ToJson diff --git a/Repl.lean b/Repl.lean index e42558d..eb02f59 100644 --- a/Repl.lean +++ b/Repl.lean @@ -223,8 +223,13 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let .some goalState := state.goalStates[args.stateId]? | return .error $ errorIndex s!"Invalid state index {args.stateId}" - let extraMVars := args.extraMVars?.getD #[] - let result ← runMetaInMainM <| goalPrint goalState extraMVars state.options + let result ← runMetaInMainM <| goalPrint + goalState + (rootExpr := args.rootExpr?.getD False) + (parentExpr := args.parentExpr?.getD False) + (goals := args.goals?.getD False) + (extraMVars := args.extraMVars?.getD #[]) + (options := state.options) return .ok result goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do let state ← get diff --git a/Test/Integration.lean b/Test/Integration.lean index 3e9bed2..77968f0 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -72,7 +72,7 @@ def test_tactic : Test := ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult), step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult), - step "goal.print" [("stateId", .num 1)] + step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)] ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult), step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult), -- 2.44.1