From 7d91ddafebed5c4aa5a017d3623cb81cbb80d782 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 26 Sep 2020 07:15:42 -0700 Subject: [PATCH] feat: expose `getPatternVars` --- src/Lean/Elab/Match.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 6cff34ce32..49432830a1 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -405,7 +405,7 @@ match (stx.getArg 0).isNameLit? with | some val => nameToPattern val | none => throwIllFormedSyntax -private partial def collect : Syntax → M Syntax +partial def collect : Syntax → M Syntax | stx@(Syntax.node k args) => withRef stx $ withFreshMacroScope $ if k == `Lean.Parser.Term.app then do processCtorApp collect stx @@ -496,6 +496,12 @@ private def collectPatternVars (alt : MatchAltView) : TermElabM (Array PatternVa (alt, s) ← (CollectPatternVars.main alt).run {}; pure (s.vars, alt) +/- Return the pattern variables in the given pattern. + Remark: this method is not used here, but in other macros (e.g., at `Do.lean`). -/ +def getPatternVars (patternStx : Syntax) : TermElabM (Array PatternVar) := do +(_, s) ← (CollectPatternVars.collect patternStx).run {}; +pure s.vars + /- We convert the collected `PatternVar`s intro `PatternVarDecl` -/ inductive PatternVarDecl /- For `anonymousVar`, we create both a metavariable and a free variable. The free variable is used as an assignment for the metavariable