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

fix: $(_):ident is not an infallible pattern

Browse source
This commit is contained in:
Sebastian Ullrich 2021-07-22 16:52:06 +02:00
parent 5866e2bbb7
commit 98634b5554
1 changed files with 25 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -272,32 +272,31 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
else if isAntiquot quoted && !isEscapedAntiquot quoted then
-- quotation contains a single antiquotation
let k := antiquotKind? quoted |>.get!
match getAntiquotTerm quoted with
| `(_) => unconditionally pure
| `($id:ident) =>
-- Antiquotation kinds like `$id:ident` influence the parser, but also need to be considered by
-- `match` (but not by quotation terms). For example, `($id:ident) and `($e) are not
-- distinguishable without checking the kind of the node to be captured. Note that some
-- antiquotations like the latter one for terms do not correspond to any actual node kind
-- (signified by `k == Name.anonymous`), so we would only check for `ident` here.
--
-- if stx.isOfKind `ident then
-- let id := stx; let e := stx; ...
-- else
-- let e := stx; ...
let rhsFn := (`(let $id := discr; $(·)))
if k == Name.anonymous then unconditionally rhsFn else pure {
check := shape k none,
onMatch := fun
| other _ => undecided
| taken@(shape k' sz) =>
if k' == k then
covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (exhaustive := sz.isNone)
else uncovered
| _ => uncovered,
doMatch := fun yes no => do `(cond (Syntax.isOfKind discr $(quote k)) $(← yes []) $(← no)),
}
| anti => throwErrorAt anti "unsupported antiquotation kind in pattern"
let rhsFn := match getAntiquotTerm quoted with
| `(_) => pure
| `($id:ident) => fun stx => `(let $id := discr; $(stx))
| anti => fun _ => throwErrorAt anti "unsupported antiquotation kind in pattern"
-- Antiquotation kinds like `$id:ident` influence the parser, but also need to be considered by
-- `match` (but not by quotation terms). For example, `($id:ident) and `($e) are not
-- distinguishable without checking the kind of the node to be captured. Note that some
-- antiquotations like the latter one for terms do not correspond to any actual node kind
-- (signified by `k == Name.anonymous`), so we would only check for `ident` here.
--
-- if stx.isOfKind `ident then
-- let id := stx; let e := stx; ...
-- else
-- let e := stx; ...
if k == Name.anonymous then unconditionally rhsFn else pure {
check := shape k none,
onMatch := fun
| other _ => undecided
| taken@(shape k' sz) =>
if k' == k then
covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (exhaustive := sz.isNone)
else uncovered
| _ => uncovered,
doMatch := fun yes no => do `(cond (Syntax.isOfKind discr $(quote k)) $(← yes []) $(← no)),
}
else if isAntiquotSuffixSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"
else if isAntiquotSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"
else if quoted.getArgs.size == 1 && isAntiquotSuffixSplice quoted[0] then