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

fix: pattern reordering in syntax match

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-20 13:52:25 +01:00
parent acfdd7d5b7
commit fdbec9101f
3 changed files with 32 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -335,27 +335,37 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
let info ← getHeadInfo alt
let pat := alt.1.head!
let alts ← (alt::alts).mapM fun alt => do ((← getHeadInfo alt).onMatch info.check, alt)
let mut yesAlts := #[]
let mut undecidedAlts := #[]
let mut nonExhaustiveAlts := #[]
for alt in alts do match alt with
| (covered f exh, alt) =>
-- we can only factor out a common check if there are no undecided patterns in between;
-- otherwise we would change the order of alternatives
if undecidedAlts.isEmpty then
yesAlts ← yesAlts.push <$> f (alt.1.tail!, alt.2)
if !exh then
nonExhaustiveAlts := nonExhaustiveAlts.push alt
else
undecidedAlts := undecidedAlts.push alt
nonExhaustiveAlts := nonExhaustiveAlts.push alt
| (undecided, alt) =>
undecidedAlts := undecidedAlts.push alt
nonExhaustiveAlts := nonExhaustiveAlts.push alt
| (uncovered, alt) =>
nonExhaustiveAlts := nonExhaustiveAlts.push alt
let m ← info.doMatch
(yes := fun newDiscrs => do
let mut yesAlts ← alts.filterMapM fun
| (covered f _, (_::pats, rhs)) => some <$> f (pats, rhs)
| _ => pure none
let undecidedAlts := alts.filterMap fun
| (undecided, alt) => some alt
| _ => none
let mut yesAlts := yesAlts
if !undecidedAlts.isEmpty then
-- group undecided alternatives in a new default case `| discr2, ... => match discr, discr2, ... with ...`
let vars ← discrs.mapM fun _ => withFreshMacroScope `(discr)
let pats := List.replicate newDiscrs.length (Unhygienic.run `(_)) ++ vars
let alts ← undecidedAlts.toArray.mapM fun alt => `(matchAltExpr| | $(alt.1.toArray),* => $(alt.2))
let alts ← undecidedAlts.mapM fun alt => `(matchAltExpr| | $(alt.1.toArray),* => $(alt.2))
let rhs ← `(match discr, $[$(vars.toArray):term],* with $alts:matchAlt*)
yesAlts := yesAlts ++ [(pats, rhs)]
withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts)
(no := do
let nonExhaustiveAlts := alts.filterMap fun
| (covered f (exhaustive := true), alt) => none
| (_, alt) => some alt
withFreshMacroScope $ compileStxMatch (discr::discrs) nonExhaustiveAlts)
yesAlts := yesAlts.push (pats, rhs)
withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts.toList)
(no := withFreshMacroScope $ compileStxMatch (discr::discrs) nonExhaustiveAlts.toList)
`(let discr := $discr; $m)
| _, _ => unreachable!

6
tests/lean/StxQuot.lean
View file

@ -68,4 +68,10 @@ open Parser.Term
| `(Parser.Term.structInstField| $lhs:ident := $rhs) => #[lhs, rhs]
| _ => unreachable!
#eval run do
match ← `({ a := a : a }) with
| `({ a := a : 0 }) => "0"
| `({ a := a $[: $a?]?}) => "1"
| stx => "2"
#eval run `(sufficesDecl|x from x)

3
tests/lean/StxQuot.lean.expected.out
View file

@ -35,4 +35,5 @@
"(Term.match\n \"match\"\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
"(Term.match\n \"match\"\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
"#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]"
StxQuot.lean:71:33: error: expected parser to return exactly one syntax object
"1"
StxQuot.lean:77:33: error: expected parser to return exactly one syntax object