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 28 additions and 13 deletions
Showing only changes of commit 855e771609 - Show all commits

View File

@ -45,7 +45,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| "goal.continue" => run goal_continue | "goal.continue" => run goal_continue
| "goal.delete" => run goal_delete | "goal.delete" => run goal_delete
| "goal.print" => run goal_print | "goal.print" => run goal_print
| "compile.tactics" => run compile_tactics | "compile.unit" => run compile_unit
| cmd => | cmd =>
let error: Protocol.InteractionError := let error: Protocol.InteractionError :=
errorCommand s!"Unknown command {cmd}" errorCommand s!"Unknown command {cmd}"
@ -192,11 +192,19 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => runMetaM <| do | .some goalState => runMetaM <| do
return .ok (← goalPrint goalState state.options) return .ok (← goalPrint goalState state.options)
compile_tactics (args: Protocol.CompileTactics): MainM (CR Protocol.CompileTacticsResult) := do compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
let module := args.module.toName let module := args.module.toName
try try
let result ← Compile.compileAndCollectTacticInvocations module let steps ← Compile.processSource module
return .ok result let units? := if args.compilationUnits then
.some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
else
.none
let invocations? ← if args.invocations then
pure $ .some (← Compile.collectTacticsFromCompilation steps)
else
pure .none
return .ok { units?, invocations? }
catch e => catch e =>
return .error $ errorI "compile" (← e.toMessageData.toString) return .error $ errorI "compile" (← e.toMessageData.toString)

View File

@ -8,22 +8,23 @@ open Lean
namespace Pantograph.Compile namespace Pantograph.Compile
def compileAndCollectTacticInvocations (module : Name) : IO Protocol.CompileTacticsResult := do --def readCompilationUnits (module : Name) : IO Protocol.CompileUnitsResult := do
let steps ← processSource module -- let steps ← processSource module
-- return { units := steps.map (·.src.toString) }
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" IO.println s!"{steps.length} compilation steps, {infoTrees.length} trees found, {tacticInfoTrees.length} tactic trees, {tactics.length} tactics found"
let invocations : List Protocol.InvokedTactic ← 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
let tactic ← invocation.ctx.runMetaM {} do let tactic ← invocation.ctx.runMetaM {} do
let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
return t.pretty return t.pretty
return { goalBefore, goalAfter, tactic } return { goalBefore, goalAfter, tactic }
return { invocations }
end Pantograph.Compile end Pantograph.Compile

View File

@ -275,17 +275,23 @@ structure GoalDiag where
printAll: Bool := false printAll: Bool := false
instantiate: Bool := true instantiate: Bool := true
structure CompileTactics where
module: String
deriving Lean.FromJson
/-- Executes the Lean compiler on a single file -/
structure CompileUnit where
module: String
-- If set to true, query the string boundaries of compilation units
compilationUnits: Bool := false
-- If set to true, collect tactic invocations
invocations: Bool := false
deriving Lean.FromJson
structure InvokedTactic where structure InvokedTactic where
goalBefore: String goalBefore: String
goalAfter: String goalAfter: String
tactic: String tactic: String
deriving Lean.ToJson deriving Lean.ToJson
structure CompileTacticsResult where structure CompileUnitResult where
invocations: List InvokedTactic units?: Option $ List (Nat × Nat)
invocations?: Option $ List InvokedTactic
deriving Lean.ToJson deriving Lean.ToJson
abbrev CR α := Except InteractionError α abbrev CR α := Except InteractionError α