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

fix: escaped $$x* antiquotation splices

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-24 19:11:51 +02:00
parent 105bfcc8f0
commit 7272235241
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/Quotation.lean
View file

@ -114,7 +114,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
match stx[0] with
| Syntax.atom _ val => `(Syntax.atom (Option.getD (getHeadInfo? $(getAntiquotTerm stx)) info) $(quote val))
| _ => throwErrorAt stx "expected token"
else if isAntiquotSuffixSplice stx && !isEscapedAntiquot stx then
else if isAntiquotSuffixSplice stx && !isEscapedAntiquot (getCanonicalAntiquot (getAntiquotSuffixSpliceInner stx)) then
-- splices must occur in a `many` node
throwErrorAt stx "unexpected antiquotation splice"
else if isAntiquotSplice stx && !isEscapedAntiquot stx then
@ -125,7 +125,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
let mut args := ArrayStxBuilder.empty
let appendName := if (← getEnv).contains ``Array.append then ``Array.append else ``Array.appendCore
for arg in stx.getArgs do
if k == nullKind && isAntiquotSuffixSplice arg then
if k == nullKind && isAntiquotSuffixSplice arg && !isEscapedAntiquot (getCanonicalAntiquot (getAntiquotSuffixSpliceInner arg)) then
let antiquot := getAntiquotSuffixSpliceInner arg
let ks := antiquotKinds antiquot |>.map (·.1)
let val := getAntiquotTerm (getCanonicalAntiquot antiquot)
@ -139,7 +139,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
let sep := quote <| getSepFromSplice arg
`(@TSepArray.elemsAndSeps $(quote ks) $sep $val)
| k => throwErrorAt arg "invalid antiquotation suffix splice kind '{k}'"
else if k == nullKind && isAntiquotSplice arg then
else if k == nullKind && isAntiquotSplice arg && !isEscapedAntiquot arg then
let k := antiquotSpliceKind? arg
let (arg, bindLets) ← floatOutAntiquotTerms arg |>.run pure
let inner ← (getAntiquotSpliceContents arg).mapM quoteSyntax