147 lines
5.4 KiB
Plaintext
147 lines
5.4 KiB
Plaintext
|
||
import Lean.Elab.Import
|
||
import Lean.Elab.Command
|
||
import Lean.Elab.InfoTree
|
||
|
||
import Pantograph.Compile.Frontend
|
||
|
||
open Lean
|
||
|
||
namespace Lean.Elab.Info
|
||
/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
|
||
protected def stx? : Info → Option Syntax
|
||
| .ofTacticInfo info => info.stx
|
||
| .ofTermInfo info => info.stx
|
||
| .ofCommandInfo info => info.stx
|
||
| .ofMacroExpansionInfo info => info.stx
|
||
| .ofOptionInfo info => info.stx
|
||
| .ofFieldInfo info => info.stx
|
||
| .ofCompletionInfo info => info.stx
|
||
| .ofUserWidgetInfo info => info.stx
|
||
| .ofCustomInfo info => info.stx
|
||
| .ofFVarAliasInfo _ => none
|
||
| .ofFieldRedeclInfo info => info.stx
|
||
| .ofOmissionInfo info => info.stx
|
||
/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
|
||
protected def isOriginal (i : Info) : Bool :=
|
||
match i.stx? with
|
||
| none => true -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
|
||
| some stx => match stx.getHeadInfo with
|
||
| .original .. => true
|
||
| _ => false
|
||
end Lean.Elab.Info
|
||
|
||
namespace Lean.Elab.TacticInfo
|
||
|
||
/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
|
||
def name? (t : TacticInfo) : Option Name :=
|
||
match t.stx with
|
||
| Syntax.node _ n _ => some n
|
||
| _ => none
|
||
/-- Decide whether a tactic is "substantive",
|
||
or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
|
||
def isSubstantive (t : TacticInfo) : Bool :=
|
||
match t.name? with
|
||
| none => false
|
||
| some `null => false
|
||
| some ``cdot => false
|
||
| some ``cdotTk => false
|
||
| some ``Lean.Parser.Term.byTactic => false
|
||
| some ``Lean.Parser.Tactic.tacticSeq => false
|
||
| some ``Lean.Parser.Tactic.tacticSeq1Indented => false
|
||
| some ``Lean.Parser.Tactic.«tactic_<;>_» => false
|
||
| some ``Lean.Parser.Tactic.paren => false
|
||
| _ => true
|
||
|
||
end Lean.Elab.TacticInfo
|
||
|
||
namespace Lean.Elab.InfoTree
|
||
|
||
/--
|
||
Keep `.node` nodes and `.hole` nodes satisfying predicates.
|
||
|
||
Returns a `List InfoTree`, although in most situations this will be a singleton.
|
||
-/
|
||
partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
|
||
InfoTree → List InfoTree
|
||
| .context ctx tree => tree.filter p m |>.map (.context ctx)
|
||
| .node info children =>
|
||
if p info then
|
||
[.node info (children.toList.map (filter p m)).join.toPArray']
|
||
else
|
||
(children.toList.map (filter p m)).join
|
||
| .hole mvar => if m mvar then [.hole mvar] else []
|
||
|
||
end Lean.Elab.InfoTree
|
||
|
||
|
||
namespace Pantograph.Compile
|
||
|
||
-- Info tree filtering functions
|
||
|
||
structure TacticInvocation where
|
||
info : Elab.TacticInfo
|
||
ctx : Elab.ContextInfo
|
||
children : PersistentArray Elab.InfoTree
|
||
namespace TacticInvocation
|
||
|
||
/-- Return the range of the tactic, as a pair of file positions. -/
|
||
protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx
|
||
|
||
/-- Pretty print a tactic. -/
|
||
protected def pp (t : TacticInvocation) : IO Format :=
|
||
t.ctx.runMetaM {} try
|
||
Lean.PrettyPrinter.ppTactic ⟨t.info.stx⟩
|
||
catch _ =>
|
||
pure "<failed to pretty print>"
|
||
|
||
/-- Run a tactic on the goals stored in a `TacticInvocation`. -/
|
||
protected def runMetaMGoalsBefore (t : TacticInvocation) (x : List MVarId → MetaM α) : IO α := do
|
||
t.ctx.runMetaM {} <| Meta.withMCtx t.info.mctxBefore <| x t.info.goalsBefore
|
||
|
||
/-- Run a tactic on the after goals stored in a `TacticInvocation`. -/
|
||
protected def runMetaMGoalsAfter (t : TacticInvocation) (x : List MVarId → MetaM α) : IO α := do
|
||
t.ctx.runMetaM {} <| Meta.withMCtx t.info.mctxAfter <| x t.info.goalsAfter
|
||
|
||
/-- Run a tactic on the main goal stored in a `TacticInvocation`. -/
|
||
protected def runMetaM (t : TacticInvocation) (x : MVarId → MetaM α) : IO α := do
|
||
match t.info.goalsBefore.head? with
|
||
| none => throw <| IO.userError s!"No goals at {← t.pp}"
|
||
| some g => t.runMetaMGoalsBefore fun _ => do g.withContext <| x g
|
||
|
||
protected def goalState (t : TacticInvocation) : IO (List Format) := do
|
||
t.runMetaMGoalsBefore (fun gs => gs.mapM fun g => do Meta.ppGoal g)
|
||
|
||
protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
|
||
t.runMetaMGoalsAfter (fun gs => gs.mapM fun g => do Meta.ppGoal g)
|
||
|
||
protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
|
||
t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
|
||
|
||
end TacticInvocation
|
||
|
||
/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
|
||
partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
|
||
List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
|
||
match t with
|
||
| .context inner t => findAllInfo t (inner.mergeIntoOuter? ctx) pred
|
||
| .node i children =>
|
||
(if pred i then [(i, ctx, children)] else []) ++ children.toList.bind (fun t => findAllInfo t ctx pred)
|
||
| _ => []
|
||
|
||
/-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
|
||
each equipped with its relevant `ContextInfo`, and any children info trees. -/
|
||
def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
|
||
let infos := findAllInfo t none fun i => match i with
|
||
| .ofTacticInfo _ => true
|
||
| _ => false
|
||
infos.filterMap fun p => match p with
|
||
| (.ofTacticInfo i, some ctx, children) => .some ⟨i, ctx, children⟩
|
||
| _ => none
|
||
|
||
def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
|
||
collectTacticNodes t |>.filter fun i => i.info.isSubstantive
|
||
|
||
|
||
end Pantograph.Compile
|