Compiling match with 6 Qq patterns takes 50s

Stream: lean4

[Bob Rubbens]

Good evening everyone, I have another metaprogramming question, I have I'm not through my question credits yet...

I'm at the following program now:

import Lean
import Qq

open Lean Elab Tactic Term Meta PrettyPrinter Qq

def simplifyLocalDecl (g : MVarId) (localDecl : LocalDecl): TacticM (Option (List MVarId)) := do
  let h := localDecl.fvarId
  let xx ← inferTypeQ (.fvar h)
  let res ← match xx with
  | ⟨0, ~q(¬(_ ∨ _)), _⟩ => return none
  | ⟨0, ~q(¬(_ ∧ _)), _⟩ => return none
  | ⟨0, ~q(¬¬_), _⟩ => return none
  | ⟨0, ~q(¬$p), _⟩ => return none
  | ⟨0, ~q(_ ∨ (_ ∧ _)), _⟩ => return none -- A
  | ⟨0, ~q((_ ∧ _) ∨ _), _⟩ => return none -- B
  | ⟨_, _, _⟩ => return none

It does exactly what I want, but it's a bit slow to compile. Without the lines marked A and B, its a second or so until the yellow bar on the left of the vscodeditor and the "busy" tooltip disappears. With the lines marked A and B included, it takes about 50 seconds. My laptop is by no means beefy but performance hasn't been a problem for me (yet...).

In the MWE I factored out the two or patterns into a separate def that just returns a bool if it matches, which brings compile time down to 5, so I can probably continue with that workaround. But it's a bit of a strange case. Is this just me abusing/misusing Qq or should I post an issue for this somewhere?

[Eric Wieser]

Is the issue the patterns themselves, or just the fact that there are lots of patterns?

[Kim Morrison]

Matches with many patterns, and each pattern looking deeply, have a known performance limitation. We'd like to have a language level fix, but realistically this is not within the next 6 months.

My personal recommendation is to avoid the quote4 library, and instead use nested match statements using e.getAppFnArgs.

[Eric Wieser]

I'm surprised the depth of the pattern affects the compilation time in a major way

[Eric Wieser]

I wonder if Qq is just missing some type annotations internally that would stop what I assume is elaborate blow up

[Eric Wieser]

I agree that some of the issues with ~q (#21, #36) are fixable only with language-level changes; do notation needs do extension hooks to allow custom matching, otherwise it's basically impossible to handle all the bells and whistles of do notation (let mut, return) correctly

[Eric Wieser]

Eric Wieser said:

Is the issue the patterns themselves, or just the fact that there are lots of patterns?

Filed as https://github.com/leanprover-community/quote4/issues/37 with a mwe

[Jannis Limperg]

I'd be very happy to supervise a project to implement matching up to reducible defeq 'done right', if anyone is interested.

[Eric Wieser]

I think the hard part is the syntax change to do notation and getting buy-in (of time spent reviewing an important part of Lean) from the FRO

[Jannis Limperg]

Solving these issues would also be nice, but they don't bother me too much. What bothers me more, and what the proposed project would address, is that Qq matching is very wasteful. Currently, the match in the example

import Lean
import Qq

open Lean Lean.Elab.Tactic Qq

def test (e : Expr) : TacticM Unit := do
  let ⟨0, t, _⟩ ← inferTypeQ e
    | return
  match t with
  | ~q(And _ _) => f1
  | ~q(Or _ (And _ _)) => f2
  | ~q(Or _ (Or _ _)) => f3
  | _ => sorry

#print test

essentially compiles to

let pat1 <- elabPattern `(And _ _)
if isDefEq e pat1 then
  f1
else
  let pat2 <- elabPattern `(Or _ (And _ _))
  if isDefEq e pat2 then
    f2
  else
    let pat3 <- elabPattern `(Or _ (Or _ _))
    if isDefEq e pat3 then
      f3
    else
      sorry

(Actually, Qq reorders the patterns for some reason.) This is a very effective hack, but what you would write by hand is this:

  match <- whnf t with
  | .app (.app (.const ``And _) _) _ => f1
  | .app (.app (.const ``Or _) _) x =>
    match <- whnf x with
    | .app (.app (.const ``And _) _) _ => f2
    | .app (.app (.const ``Or _) _) _ => f3
    | _ => sorry
  | _ => sorry

So instead of three isDefEqs you have two whnfs, one for each level of the pattern. It's conceptually easy to derive the latter implementation from the ~q match syntax, though the devil is probably in the details.

[Jannis Limperg]

Jannis Limperg said:

(Actually, Qq reorders the patterns for some reason.)

Scratch this, I just didn't understand the code.

[Eric Wieser]

is that Qq matching is very wasteful

Just to be clear, the title of this thread is about wastefulness at elaboration time, whereas it sounds like you're suggesting reducing wastefulness at runtime. Of course, both would be beneficial!

[Eric Wieser]

Solving these issues would also be nice, but they don't bother me too much.

I think return notation doing completely the wrong thing is pretty damning, and a big footgun

[Jireh Loreaux]

Sorry, what's the problem with return?

[Moritz Doll]

See Eric's example in https://github.com/leanprover-community/quote4/issues/21

[Eric Wieser]

The problem is that ¬q doesn't (can't?) participate in the do notation magic, so has to try and build something on top of it. I think this is impossible to do correctly (without other bad choices like duplicating syntax)

[Moritz Doll]

the return behaves like rust and not like haskell (if I remember correctly)

[Moritz Doll]

and for comparison:

def foo₃ (a : ℤ) : MetaM Bool := do
  let x : Unit ← match a with
    | 37 => return true
    | _ => return true
  return false -- `do` element is unreachable

[Jannis Limperg]

Eric Wieser said:

is that Qq matching is very wasteful

Just to be clear, the title of this thread is about wastefulness at elaboration time, whereas it sounds like you're suggesting reducing wastefulness at runtime. Of course, both would be beneficial!

Yes, sorry for the confusion. The alternative design I propose might also benefit elaboration, but only as a side effect.