feat: Unfold aux lemmas when printing root expr

This commit is contained in:
Leni Aniva 2024-03-28 18:56:42 -07:00
parent 47fabf333b
commit a698a4250f
6 changed files with 22 additions and 9 deletions

View File

@ -165,13 +165,21 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat
def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options
def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
@[export pantograph_goal_print_m]
def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
let metaM := do
state.restoreMetaM
return {
root? := ← state.rootExpr?.mapM (λ expr => serialize_expression options expr),
parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr),
root? := ← state.rootExpr?.mapM (λ expr => do
serialize_expression options (← unfoldAuxLemmas expr)),
parent? := ← state.parentExpr?.mapM (λ expr => do
serialize_expression options (← unfoldAuxLemmas expr)),
}
runMetaM metaM

View File

@ -1,8 +1,11 @@
import Pantograph.Goal
import Pantograph.Library
import Pantograph.Protocol
import Lean
import LSpec
open Lean
namespace Pantograph
namespace Protocol

View File

@ -2,11 +2,12 @@ import LSpec
import Pantograph.Serial
import Pantograph.Environment
import Test.Common
import Lean
open Lean
namespace Pantograph.Test.Environment
open Pantograph
open Lean
deriving instance DecidableEq, Repr for Protocol.InductInfo
deriving instance DecidableEq, Repr for Protocol.ConstructorInfo

View File

@ -1,6 +1,6 @@
import LSpec
import Test.Environment
import Test.Holes
import Test.Metavar
import Test.Integration
import Test.Proofs
import Test.Serial
@ -11,7 +11,7 @@ def main := do
Lean.initSearchPath (← Lean.findSysroot)
let suites := [
Holes.suite,
Metavar.suite,
Integration.suite,
Proofs.suite,
Serial.suite,

View File

@ -3,7 +3,7 @@ import Pantograph.Goal
import Pantograph.Serial
import Test.Common
namespace Pantograph.Test.Holes
namespace Pantograph.Test.Metavar
open Pantograph
open Lean
@ -204,6 +204,6 @@ def suite: IO LSpec.TestSeq := do
let tests ← proofRunner env tests
return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
return LSpec.group "Holes" tests
return LSpec.group "Metavar" tests
end Pantograph.Test.Holes
end Pantograph.Test.Metavar

View File

@ -1,11 +1,12 @@
import LSpec
import Pantograph.Serial
import Test.Common
import Lean
open Lean
namespace Pantograph.Test.Serial
open Pantograph
open Lean
deriving instance Repr, DecidableEq for Protocol.BoundExpression