get explicit args

Stream: lean4

[Patrick Massot]

Is there a version of docs4#Lean.Expr.getAppArgs that returns only explicit arguments? I understand the def of getAppargs but I don't know how to access this info. Working in MetaM is ok.

[Arthur Paulino]

Hm, do you mean to get explicit arguments from a telescoped lambda? Applications don't have the implicit/explicit dichotomy

[Patrick Massot]

I was indeed looking around the telescope stuff. I have a proof term that applies a lemma and I want to get the exprs corresponding to explicit arguments of the lemma.

[Arthur Paulino]

I'm not on my PC right now and I don't remember if the lambda telescope retrieves the binder info's. But that's something you can accumulate while traversing an expression

[Patrick Massot]

I guess I could get the type of the head app, try to get binder info there and then select the app arguments based on that but it feels very clunky.

[Jannis Limperg]

The telescope gives you FVarIds and the LocalDecls corresponding to these FVarIds have a BinderInfo field. This should tell you whether the argument was explicit or implicit.

[Arthur Paulino]

I think Patrick doesn't need a monadic telescope. Is there a pure one? (pretty amazing how I've already forgotten the MetaM API)

[Jannis Limperg]

The telescope functions are all monadic. I guess one could define a pure one for local variables which returns an explicit LocalContext. But almost every higher-level function on Exprs needs MetaM anyway to interpret potential metavariables, so I don't think there's much of a point.

[Patrick Massot]

Thanks Jannis. My question wasn't limited to FVarId. What I ended up using was: first some non-monadic function collecting indices of explicit arguments in a forall telescope

private def explicitIndicesAux : (all : Expr) → (exArgs : Array Nat) → Nat → Array Nat
| forallE _ _ body BinderInfo.default, as, n => explicitIndicesAux body (as.push n) (n+1)
| forallE _ _ body _, as, n => explicitIndicesAux body as (n+1)
| _, as, _ => as

/-- Get the indices of explicit arguments of a forall telescope. -/
def explicitIndices (all : Expr) := explicitIndicesAux all #[] 0

and then when I see a app telescope I infer its type using inferType and instantiateMVars (this is one of those pairs of functions that should always be called together if you want to use the result in any way...), use the above function and pick the arguments from docs4#Lean.Expr.getAppArgs that live at those indices. I feels super weird but I don't see another way to work around the fact that Expr.app has no binder info.

[Arthur Paulino]

Expr.app encodes stuff like f x (g y). How would it keep binder information when there's no binders?

[Jannis Limperg]

This general approach sounds fine to me; I would have done it similarly. I would, however, implement explicitIndices in terms of forallBoundedTelescope where the bound is the number of arguments n in your application f x1 ... xn. This ensures that explicitIndices catches explicit arguments even when the type of f is, for example, a definition T := forall X1 ... Xn, U, which your explicitIndices would treat as having zero explicit arguments.

[Patrick Massot]

Jannis, if this is really quick for your, I'd be interested in seeing an implementation using forallBoundedTelescope.

[Jannis Limperg]

Sure!

import Lean

open Lean Lean.Meta

/--
Given a type `e = ∀ (x₁ : X₁) ... (xₙ : Xₙ), U`, extract those `i` such that
`xᵢ` is an explicit argument.
-/
def explicitIndices (e : Expr) (n : Nat) : MetaM (Array Nat) :=
  forallBoundedTelescope e n λ args _ => do
    let mut indices := Array.mkEmpty n
    for h : i in [:args.size] do
      if (← (args[i]'h.2).fvarId!.getDecl).binderInfo == .default then
        indices := indices.push i
    return indices

def T := ∀ (x₁ : Nat) {x₂ : Nat} (x₃ : Nat) [x₄ : DecidableEq Nat] (x₅ : Nat), Nat

#eval explicitIndices (.const ``T []) 4

[Patrick Massot]

Thanks!