How to WHNF without exposing recursors?

Stream: lean4

[Gabriel Ebner]

I'm trying to whnf an expression in an elaborator and then return the normalized expression. However the whnf exposes the .rec recursor, which is a problem because the result can then no longer be compiled. Simplified MWE:

import Lean

open Lean Meta Elab Term in
elab "whnf%" t:term : term <= expectedType => do
  whnf (← elabTerm t expectedType)

constant x : Option Nat := some 42

#eval whnf% x.getD 0
-- code generator does not support recursor 'Option.rec' yet, consider using 'match ... with' and/or structural recursion

Is there an obvious flag that I need to set here? (Potentially related to https://github.com/leanprover/lean4/issues/445)

[Sebastian Ullrich]

I fear the immediate answer is that you're the first one trying this and there is no such flag currently

[Leonardo de Moura]

We have variants of whnf. Example:

@[specialize] partial def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : MetaM Expr :=

Here is another one (at DiscrTree.lean) that may be useful as a reference if you want to implement your own variants.

private partial def whnfUntilBadKey (e : Expr) : MetaM Expr := do

That being said, your whnf% is not going to do what you want when elabTerm returns a term containing metavariables (corresponding to elaboration tasks that have been postponed).

[Gabriel Ebner]

We have variants of whnf.

That works, thank you. IIRC you added smart unfolding a couple years back so that the internals of the equation compiler don't leak, so I was really surprised to get a recursor out of whnf. In Lean 3, whnf didn't reduce this example:

open tactic
example (x : option ℕ) := by do
  to_expr ```(x.get_or_else 0) >>= whnf >>= trace
-- x.get_or_else 0

[Leonardo de Moura]

I will change the behavior of unfoldDefinition? for the auxiliary match_<idx> definitions created by the elaborator when "smart unfolding" is enabled. They will not be unfolded if the result cannot be reduced.
Then, whnf will produce the following expression in your example.

match x, 0 with
  | some x, x_1 => x
  | none, e =>

It is different than the one produce by Lean 3 because

def Option.getD : Option α → α → α
  | some x, _ => x
  | none,   e => e

is macro expanded into

def Option.getD : Option α → α → α => fun a b =>
  match a, b with
  | some x, _ => x
  | none,   e => e

If we define get_or_else using a match .. with in Lean 3, we would get

option.get_or_else._match_1 0 x