max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add support for quoted literals in patterns

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-11 15:16:54 -07:00
parent 2c2a357f28
commit 9cd88807dd
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Elab/Match.lean
View file

@ -370,6 +370,16 @@ match f? with
| none => throwCtorExpected
| _ => processVar stx
private def nameToPattern : Name → TermElabM Syntax
| Name.anonymous => `(Name.anonymous)
| Name.str p s _ => do p ← nameToPattern p; `(Name.str $p $(quote s) _)
| Name.num p n _ => do p ← nameToPattern p; `(Name.num $p $(quote n) _)
private def quotedNameToPattern (stx : Syntax) : TermElabM Syntax :=
match (stx.getArg 0).isNameLit? with
| some val => nameToPattern val
| none => throwIllFormedSyntax
private partial def collect : Syntax → M Syntax
| stx@(Syntax.node k args) => withRef stx $ withFreshMacroScope $
if k == `Lean.Parser.Term.app then do
@ -434,6 +444,11 @@ private partial def collect : Syntax → M Syntax
pure stx
else if k == charLitKind then
pure stx
else if k == `Lean.Parser.Term.quotedName then
/- Quoted names have an elaboration function associated with them, and they will not be macro expanded.
Note that macro expansion is not a good option since it produces a term using the smart constructors `mkNameStr`, `mkNameNum`
instead of the constructors `Name.str` and `Name.num` -/
liftM $ quotedNameToPattern stx
else if k == choiceKind then
throwError "invalid pattern, notation is ambiguous"
else