From ff89c2933b98c1e2471487d9ca94abc0790d6ed7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 4 Jan 2023 12:39:07 +0100 Subject: [PATCH 1/2] fix: be more careful with `MatchResult.uncovered` in syntax match --- src/Lean/Elab/Quotation.lean | 27 ++++++++++++++++++--------- tests/lean/2005.lean | 11 +++++++++++ tests/lean/2005.lean.expected.out | 1 + 3 files changed, 30 insertions(+), 9 deletions(-) create mode 100644 tests/lean/2005.lean create mode 100644 tests/lean/2005.lean.expected.out diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 3673a1159a74..f413d1c0be7d 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -307,6 +307,12 @@ inductive MatchResult where /-- Pattern is not quite sure yet; include unchanged in both branches -/ | undecided +instance : Repr MatchResult where + reprPrec + | .covered _ e, _ => f!"covered _ {repr e}" + | .uncovered, _ => "uncovered" + | .undecided, _ => "undecided" + open MatchResult /-- All necessary information on a pattern head. -/ @@ -365,12 +371,11 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo := if (getCanonicalAntiquot quoted)[3].isNone || pseudoKinds.all id then unconditionally rhsFn else pure { check := shape ks none, onMatch := fun - | other _ => undecided | taken@(shape ks' sz) => if ks' == ks then covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (exhaustive := sz.isNone) else uncovered - | _ => uncovered, + | _ => undecided, doMatch := fun yes no => do let cond ← ks.foldlM (fun cond k => `(or $cond (Syntax.isOfKind __discr $(quote k)))) (← `(false)) `(cond $cond $(← yes []) $(← no)), @@ -443,7 +448,6 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo := pure { check := slice idx numSuffix onMatch := fun - | other _ => undecided | slice p s => if p == idx && s == numSuffix then let argPats := quoted.getArgs.mapIdx fun i arg => @@ -451,7 +455,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo := Unhygienic.run `(`($(arg))) covered (fun (pats, rhs) => pure (argPats.toList ++ pats, rhs)) (exhaustive := true) else uncovered - | _ => uncovered + | _ => undecided doMatch := fun yes no => do let prefixDiscrs ← (List.range idx).mapM (`(Syntax.getArg __discr $(quote ·))) let sliceDiscr ← `(mkNullNode (__discr.getArgs.extract $(quote idx) (__discr.getNumArgs - $(quote numSuffix)))) @@ -480,16 +484,19 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo := shape [kind] argPats.size, onMatch := fun | other stx' => - if (quoted.isIdent || lit) && quoted == stx' then - covered pure (exhaustive := true) + if quoted.isIdent || lit then + if quoted == stx' then + covered pure (exhaustive := true) + else + uncovered else - uncovered + undecided | shape ks sz => if ks == [kind] && sz == argPats.size then covered (fun (pats, rhs) => pure (argPats.toList ++ pats, rhs)) (exhaustive := true) else uncovered - | _ => uncovered, + | _ => undecided, doMatch := fun yes no => do let (cond, newDiscrs) ← if lit then let cond ← `(Syntax.matchesLit __discr $(quote kind) $(quote (isLit? kind quoted).get!)) @@ -546,6 +553,7 @@ private partial def compileStxMatch (discrs : List Term) (alts : List Alt) : Ter let mut floatedLetDecls := #[] for (x, alt') in alts do let mut alt' := alt' + trace[Elab.match_syntax.onMatch] "{alt'} ~> {repr x}" match x with | covered f exh => -- we can only factor out a common check if there are no undecided patterns in between; @@ -673,6 +681,7 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do builtin_initialize registerTraceClass `Elab.match_syntax - registerTraceClass `Elab.match_syntax.result + registerTraceClass `Elab.match_syntax.alt (inherited := true) + registerTraceClass `Elab.match_syntax.result (inherited := true) end Lean.Elab.Term.Quotation diff --git a/tests/lean/2005.lean b/tests/lean/2005.lean new file mode 100644 index 000000000000..79616ee7e43b --- /dev/null +++ b/tests/lean/2005.lean @@ -0,0 +1,11 @@ +import Lean +open Lean + +syntax (docComment)? "foo" term : command + +def foo2 : Syntax → Nat + | `($[$_]? foo !$_) => 1 + | `(foo -$_) => 2 + | _ => 0 + +#eval foo2 (Unhygienic.run `(foo -x)) diff --git a/tests/lean/2005.lean.expected.out b/tests/lean/2005.lean.expected.out new file mode 100644 index 000000000000..0cfbf08886fc --- /dev/null +++ b/tests/lean/2005.lean.expected.out @@ -0,0 +1 @@ +2 From d8387db825adc841f357575da164a31031a3c261 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 4 Jan 2023 14:48:21 +0100 Subject: [PATCH 2/2] perf: avoid duplicate computation in syntax match elaborator --- src/Lean/Elab/Quotation.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index f413d1c0be7d..9d247413c11b 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -546,7 +546,8 @@ private partial def compileStxMatch (discrs : List Term) (alts : List Alt) : Ter pure Syntax.missing | discr::discrs, alt::alts => do let info ← getHeadInfo alt - let alts ← (alt::alts).mapM fun alt => return ((← getHeadInfo alt).onMatch info.check, alt) + let alts := (info.onMatch info.check, alt) :: (← alts.mapM fun alt => + return ((← getHeadInfo alt).onMatch info.check, alt)) let mut yesAlts := #[] let mut undecidedAlts := #[] let mut nonExhaustiveAlts := #[]