Transforming an expr when moving into the alts of a case

Stream: Is there code for X?

[Joachim Breitner]

Meta-programming question:

I am traversing an expression (a function definition), and I also have an e : Expr of interest at hand. As I go into the alts of a casesOn combinator, if that case analysis looks at e, I want to get the “refined” expression.

For example, say e is (a, b), and I enter PSigma.casesOn b (fun c d = …), then I want to know that instead of (a, b) I now have (a (c, d)).

There is something very close to that in Lean.Meta.CasesOnApp.addArg, which I can use if e is a type and I have an actual value v : e around that I can thread though, and as part of that process, that function does infer the “refined” type of v. But what do I do if I don’t have a value, and just the expression e that I want to transform?

(I tried cargo-culting addArg, but it doesn’t seem to work right.)

[Joachim Breitner]

This seem to be roughly doing what I think I need, but I have serious doubts that this is idiomatic good style…

/--
  Given a `casesOn` application `c` of the form
  ```
  casesOn As (fun is x => motive[i, xs]) is major  (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
  ```
  and a type `e : B[is, major]`, for every alternative `i`, construct the type
  ```
  B[C_i[ys_i]]
  ```
  (which `ys_i` as loose bound variable, ready to be `.instantiateRev`d)
-/
def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) :=
  lambdaTelescope c.motive fun motiveArgs _motiveBody => do
    unless motiveArgs.size == c.indices.size + 1 do
      throwError "failed to add argument to `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders"
    let discrs := c.indices ++ #[c.major]
    let mut eAbst := e
    for motiveArg in motiveArgs.reverse, discr in discrs.reverse do
      eAbst := (← kabstract eAbst discr).instantiate1 motiveArg
    -- Up to this point, this is cargo-culted from `CasesOn.App.addArg`
    -- Let's create something Prop-typed that mentions `e`, by writing `e = e`.
    let eEq ← mkEq eAbst eAbst
    let motive ← mkLambdaFVars motiveArgs eEq
    let us := if c.propOnly then c.us else levelZero :: c.us.tail!
    -- Now instantiate the casesOn wth this synthetic motive
    let aux := mkAppN (mkConst c.declName us) c.params
    let aux := mkApp aux motive
    let aux := mkAppN aux discrs
    check aux
    let auxType ← inferType aux
    -- The type of the remaining arguments will mention `e` instantiated for each arg
    -- so extract them
    let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType
    let altAuxTys ← altAuxs.mapM inferType
    let res ← altAuxTys.mapM fun altAux => do
      let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAux
      let body := body.getArg! 2
      -- and abstract over the parameters of the alternative again
      Expr.abstractM body fvs
    return res

[Scott Morrison]

Besides the repeated let aux := it doesn't seem crazy.

[Joachim Breitner]

Ha, and that's something I have carco-culted from the lean code:
https://github.com/leanprover/lean4/blob/baa4b68a71926a722b77d4ec2cba34bfc76cc5aa/src/Lean/Meta/CasesOn.lean#L74