dealing with mdata

Stream: lean4

[Tomas Skrivan]

What is the best way to deal with mdata when writing meta code? My code is slowly turning from e.isLet, e.getAppFn, e.getArg! to e.consumeMData.isLet, e.consumeMData.getAppFn, e.consumeMData.getAppFn. This is really ugly :(

[Jannis Limperg]

Std has a few variants of core functions that ignore mdata. There is also lean4#2026, which suggests a wider refactoring of the API to make most functions ignore mdata by default, but the core devs have not yet commented on this.

[Tomas Skrivan]

Now I'm super skeptical that I'm getting any of my pattern matching on Expr correct. For example the case | .lam _ _ (.letE ..) _ suddenly has to be

| .lam _ _ (.letE ..) _
| .mdata _ (.lam _ _ (.letE ..) _)
| .lam _ _ (.mdata _ (.letE ..)) _
| .mdata _ (.lam _ _ (.mdata _ (.letE ..)) _)

Is it a good or bad idea to just recursively purge all mdata from an expression before I start working with it?

[Mario Carneiro]

sounds like a bad idea to me

[Mario Carneiro]

rather, I think that pattern matching on exprs is the code smell here. Sometimes it is required, but if you can do something like Qq-match instead that will be more robust to things like mdata and reducible definitions in the way of the match

[Mario Carneiro]

if the expr is automatically generated / you know how it was constructed then you can probably use stricter notions of syntactic equality, but for arbitrary user exprs there could be lots of random things in there, and erasing mdata could cause problems if you weren't the one to put the mdata there

[Tomas Skrivan]

I'm implementing something similar to simp, but I need a special handling of fun x y => .., fun x => let y := ..; .. and a few other variants. This match decides what rewrite rule to apply.

[Tomas Skrivan]

I will look into the Qq match but is it sensitive to let bindings or not?

[Mario Carneiro]

I think you should write a recursive expr matcher for this, rather than trying to match all combinations in one go

[Mario Carneiro]

I don't think Qq will respect let bindings

[Tomas Skrivan]

What do you exactly mean by recursive matcher?

[Mario Carneiro]

something like this perhaps?

import Lean
open Lean

def matchLambdas : Expr → Array Expr → Array Expr × Expr
  | .mdata _ e, lams => matchLambdas e lams
  | .lam _x ty d _bi, lams => matchLambdas d (lams.push ty)
  | e, lams => (lams, e)

def matchLets : Expr → Array (Expr × Expr) → Array (Expr × Expr) × Expr
  | .mdata _ e, lets => matchLets e lets
  | .letE _x ty val body _, lets => matchLets body (lets.push (ty, val))
  | e, lets => (lets, e)

def matchLambdaThenLet (e : Expr) : Array Expr × Array (Expr × Expr) × Expr :=
  let (lams, e) := matchLambdas e #[]
  let (lets, e) := matchLets e #[]
  (lams, lets, e)

[Tomas Skrivan]

The program is not that recursive. It really matters if the expression is lambda followed by a lambda or let. What is happening deeper is not important.

[Tomas Skrivan]

If removing all the mdata is such a bad idea I will just try to carefully handle it. Let's see what kind of impact it will have on the code.

[Mario Carneiro]

the code I just posted only matches a sequence of lambdas followed by a sequence of lets

[Mario Carneiro]

but by writing it as individual recursive functions it is easier to make sure that mdata is skipped whenever needed