Merge pull request 'feat: Extract used constants from invocation' (#119) from frontend/data into dev

Reviewed-on: #119
This commit is contained in:
Leni Aniva 2024-11-10 21:29:34 -08:00
commit 4f6ccd3e82
3 changed files with 24 additions and 6 deletions

View File

@ -122,6 +122,13 @@ protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
protected def usedConstants (t: TacticInvocation) : NameSet :=
let info := t.info
info.goalsBefore
|>.filterMap info.mctxAfter.getExprAssignmentCore?
|>.map Expr.getUsedConstantsAsSet
|>.foldl .union .empty
end TacticInvocation
/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
@ -158,7 +165,13 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
let tactic ← invocation.ctx.runMetaM {} do
let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
return t.pretty
return { goalBefore, goalAfter, tactic }
let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
return {
goalBefore,
goalAfter,
tactic,
usedConstants,
}
structure InfoWithContext where
info: Elab.Info

View File

@ -298,6 +298,9 @@ structure InvokedTactic where
goalBefore: String
goalAfter: String
tactic: String
-- List of used constants
usedConstants: Array String
deriving Lean.ToJson
structure CompilationUnit where

View File

@ -167,8 +167,8 @@ example : ∀ (p: Prop), p → p := by
def test_frontend_process : Test :=
[
let file := "example : ∀ (p: Prop), p → p := by\n intro p h\n exact h"
let goal1 := "p : Prop\nh : p\n⊢ p"
let file := "example : ∀ (p q: Prop), p → p q := by\n intro p q h\n exact Or.inl h"
let goal1 := "p q : Prop\nh : p\n⊢ p q"
step "frontend.process"
[
("file", .str file),
@ -180,14 +180,16 @@ def test_frontend_process : Test :=
boundary := (0, file.utf8ByteSize),
invocations? := .some [
{
goalBefore := "⊢ ∀ (p : Prop), p → p",
goalBefore := "⊢ ∀ (p q : Prop), p → p q",
goalAfter := goal1,
tactic := "intro p h",
tactic := "intro p q h",
usedConstants := #[],
},
{
goalBefore := goal1 ,
goalAfter := "",
tactic := "exact h",
tactic := "exact Or.inl h",
usedConstants := #["Or.inl"],
},
]
}],