From 9894ad7c7e2a8e7fde305e1a542f708fd1481c5e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 26 Nov 2024 12:16:14 -0800 Subject: [PATCH] refactor: InfoTree functions --- Pantograph/Frontend.lean | 2 +- Pantograph/Frontend/Elab.lean | 82 ++----------------------------- Pantograph/Frontend/InfoTree.lean | 81 ++++++++++++++++++++++++++++++ 3 files changed, 85 insertions(+), 80 deletions(-) create mode 100644 Pantograph/Frontend/InfoTree.lean diff --git a/Pantograph/Frontend.lean b/Pantograph/Frontend.lean index fd91823..9a41567 100644 --- a/Pantograph/Frontend.lean +++ b/Pantograph/Frontend.lean @@ -1,4 +1,4 @@ -/- Adapted from lean-training-data by semorrison -/ import Pantograph.Frontend.Basic import Pantograph.Frontend.Elab +import Pantograph.Frontend.InfoTree import Pantograph.Frontend.MetaTranslate diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index ceecfae..b3173a7 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -7,77 +7,10 @@ import Pantograph.Frontend.Basic import Pantograph.Frontend.MetaTranslate import Pantograph.Goal import Pantograph.Protocol +import Pantograph.Frontend.InfoTree 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.Frontend -- Info tree filtering functions @@ -131,19 +64,10 @@ protected def usedConstants (t: TacticInvocation) : NameSet := end TacticInvocation -/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/ -partial def findAllInfo (t : Elab.InfoTree) (context?: 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? context?) pred - | .node i children => - (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred) - | _ => [] - /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics, each equipped with its relevant `ContextInfo`, and any children info trees. -/ private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := - let infos := findAllInfo t none fun i => match i with + let infos := t.findAllInfo none fun i => match i with | .ofTacticInfo _ => true | _ => false infos.filterMap fun p => match p with @@ -178,7 +102,7 @@ structure InfoWithContext where context?: Option Elab.ContextInfo := .none private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext := - let infos := findAllInfo t none fun i => match i with + let infos := t.findAllInfo none fun i => match i with | .ofTermInfo { expectedType?, expr, stx, .. } => expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry | .ofTacticInfo { stx, goalsBefore, .. } => diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean new file mode 100644 index 0000000..4e60710 --- /dev/null +++ b/Pantograph/Frontend/InfoTree.lean @@ -0,0 +1,81 @@ +/- Adapted from lean-training-data by semorrison -/ +import Lean.Elab.InfoTree +import Lean.Parser.Term + +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 [] + +/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/ +partial def findAllInfo (t : InfoTree) (context?: 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? context?) pred + | .node i children => + (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred) + | _ => [] + +end Lean.Elab.InfoTree