feat: Extract used constants from invocation #119
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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"],
|
||||
},
|
||||
]
|
||||
}],
|
||||
|
|
Loading…
Reference in New Issue