discr_tree_simp_key for a simproc?

Stream: lean4

[Alex Keizer]

I'm trying to debug why a simproc is not being applied while a manual look at the goal state seems to suggest a match. For a regular simp-lemma I would try to either rw it or look at #discr_tree_simp_key to eliminate bad discrimination tree keys as the cause, but I wonder how I would do so for a simproc? Obviously, rw won't know what to do with a simproc, but even #discr_tree_simp_key doesn't actually show me the key for the simproc, see for (a non-minimal) example:

dsimproc [simp, simp_denote] reduceArgsToLLVM (argsToLLVM (tys := no_index _) (
    .cons (α := no_index _) (f := no_index _) (a := no_index _) (as := no_index _) _ _)
  ) := reduceArgsToLLVMAux

#discr_tree_simp_key reduceArgsToLLVM
/- ^^ This outputs:
ReaderT
  Lean.Meta.Simp.MethodsRef
  (ReaderT
     Lean.Meta.Simp.Context
     (StateRefT'
        IO.RealWorld
        Lean.Meta.Simp.State
        (ReaderT
           Lean.Meta.Context
           (StateRefT'
              IO.RealWorld
              Lean.Meta.State
              (ReaderT Lean.Core.Context (StateRefT' IO.RealWorld Lean.Core.State (EIO Lean.Exception)))))))
  Lean.TransformStep
-/

I've resorted to copying the pattern to a regular lemma, and looking at the #discr_tree_simp_key output of that, as in:

theorem foo (x : ⟦Ty.arith t⟧) (xs : HVector toType (Ty.arith <$> ts)) :
    argsToLLVM (tys := no_index (t :: ts)) (
      .cons (α := no_index _) (f := no_index _) (a := no_index (Ty.arith t)) (as := no_index (Ty.arith <$> ts)) x xs)
    = zs := by
  sorry
#discr_tree_simp_key foo

Is there a better way to debug simproc discrimination tree keys?

[Robin Arnez]

Something like

import Lean

open Lean Meta Elab Command DiscrTree Simp in
elab "#discr_tree_simproc_key " k:ident : command => liftTermElabM <| do
  let state := simprocDeclExt.getState (← getEnv)
  if let some keys := state.builtin[k.getId]? then
    Lean.logInfo (← keysAsPattern keys)
  else
    let n ← realizeGlobalConstNoOverloadWithInfo k
    if let some keys := state.newEntries.find? n then
      Lean.logInfo (← keysAsPattern keys)
    else
      throwErrorAt k "not a simproc: {k}"

#discr_tree_simproc_key reduceDIte

should do the trick

[Alex Keizer]

Thanks! This is specifically looking for built-in simprocs, right?

For anybody else also debugging a custom simproc, the command can be tweaked like so:

open Lean Meta Elab Command DiscrTree Simp in
elab "#discr_tree_simproc_key " k:ident : command => liftTermElabM <| do
  let state := simprocDeclExt.getState (← getEnv)
  if let some (some keys) := state.newEntries[k.getId]? then
    Lean.logInfo (← keysAsPattern keys)
  else
    let n ← realizeGlobalConstNoOverloadWithInfo k
    if let some (some keys) := state.newEntries[n]? then
      Lean.logInfo (← keysAsPattern keys)
    else
      throwErrorAt k "not a simproc: {k}"

[Alex Keizer]

Interestingly, this does not in fact give the same discr-tree key as the transcription into a theorem. Thanks, this gives me a potential lead to investigate!