feat: Extraction of tactics from compiler #76

Merged
aniva merged 4 commits from compile/tactic into dev 2024-05-31 20:23:51 -07:00
3 changed files with 4 additions and 16 deletions
Showing only changes of commit a2c5c7448c - Show all commits

View File

@ -8,16 +8,12 @@ open Lean
namespace Pantograph.Compile namespace Pantograph.Compile
--def readCompilationUnits (module : Name) : IO Protocol.CompileUnitsResult := do
-- let steps ← processSource module
-- return { units := steps.map (·.src.toString) }
def collectTacticsFromCompilation (steps : List CompilationStep) : IO (List Protocol.InvokedTactic) := do def collectTacticsFromCompilation (steps : List CompilationStep) : IO (List Protocol.InvokedTactic) := do
let infoTrees := steps.bind (·.trees) let infoTrees := steps.bind (·.trees)
let tacticInfoTrees := infoTrees.bind λ tree => tree.filter λ let tacticInfoTrees := infoTrees.bind λ tree => tree.filter λ
| info@(.ofTacticInfo _) => info.isOriginal | info@(.ofTacticInfo _) => info.isOriginal
| _ => false | _ => false
let tactics := tacticInfoTrees.bind collectTactics let tactics := tacticInfoTrees.bind collectTactics
IO.println s!"{steps.length} compilation steps, {infoTrees.length} trees found, {tacticInfoTrees.length} tactic trees, {tactics.length} tactics found"
tactics.mapM λ invocation => do tactics.mapM λ invocation => do
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
@ -26,5 +22,4 @@ def collectTacticsFromCompilation (steps : List CompilationStep) : IO (List Prot
return t.pretty return t.pretty
return { goalBefore, goalAfter, tactic } return { goalBefore, goalAfter, tactic }
end Pantograph.Compile end Pantograph.Compile

View File

@ -109,12 +109,6 @@ protected def runMetaM (t : TacticInvocation) (x : MVarId → MetaM α) : IO α
| none => throw <| IO.userError s!"No goals at {← t.pp}" | none => throw <| IO.userError s!"No goals at {← t.pp}"
| some g => t.runMetaMGoalsBefore fun _ => do g.withContext <| x g | some g => t.runMetaMGoalsBefore fun _ => do g.withContext <| x g
protected def mainGoal (t : TacticInvocation) : IO Expr :=
t.runMetaM (fun g => do instantiateMVars (← g.getType))
protected def formatMainGoal (t : TacticInvocation) : IO Format :=
t.runMetaM (fun g => do Meta.ppExpr (← instantiateMVars (← g.getType)))
protected def goalState (t : TacticInvocation) : IO (List Format) := do protected def goalState (t : TacticInvocation) : IO (List Format) := do
t.runMetaMGoalsBefore (fun gs => gs.mapM fun g => do Meta.ppGoal g) t.runMetaMGoalsBefore (fun gs => gs.mapM fun g => do Meta.ppGoal g)
@ -137,17 +131,16 @@ partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pre
/-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics, /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
each equipped with its relevant `ContextInfo`, and any children info trees. -/ each equipped with its relevant `ContextInfo`, and any children info trees. -/
def collectTacticNodes (t : Elab.InfoTree) : List (Elab.TacticInfo × Elab.ContextInfo × PersistentArray Elab.InfoTree) := def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
let infos := findAllInfo t none fun i => match i with let infos := findAllInfo t none fun i => match i with
| .ofTacticInfo _ => true | .ofTacticInfo _ => true
| _ => false | _ => false
infos.filterMap fun p => match p with infos.filterMap fun p => match p with
| (.ofTacticInfo i, some ctx, children) => (i, ctx, children) | (.ofTacticInfo i, some ctx, children) => .some ⟨i, ctx, children⟩
| _ => none | _ => none
def collectTactics (t : Elab.InfoTree) : List TacticInvocation := def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
collectTacticNodes t |>.map (fun ⟨i, ctx, children⟩ => ⟨i, ctx, children⟩) collectTacticNodes t |>.filter fun i => i.info.isSubstantive
|>.filter fun i => i.info.isSubstantive
end Pantograph.Compile end Pantograph.Compile

View File

@ -1,6 +1,6 @@
namespace Pantograph namespace Pantograph
@[export pantograph_version] @[export pantograph_version]
def version := "0.2.15" def version := "0.2.16"
end Pantograph end Pantograph