Working with ExprDiff

Stream: lean4

[Adam Topaz]

I have some term of ExprDiff, and I would like to extract the actual subexpressions that are part of the diff. I'm sure we have some functions that accomplish this but I can't seem to find anything useful. Note that ExprDiff itself contains only the positions of the diffs:

import Lean
import Qq
open Lean Qq

#eval show MetaM Unit from do
  let a : Q(Nat) ← mkFreshExprMVarQ q(Nat)
  let e1 := q(($a + 1) + 2)
  let e2 := q(($a + 4) + 2)
  let d ← Lean.Widget.exprDiff e1 e2
  for (i,j) in d.changesBefore do
    IO.println s!"{i}, {j}"
  for (i,j) in d.changesAfter do
    IO.println s!"{i}, {j}"

[Adam Topaz]

In the example above, i would like to somehow extract that exprs associated to 1 and 4.

[Kyle Miller]

Maybe it's docs#Lean.Meta.viewSubexpr or docs#Lean.Core.viewSubexpr ?

The first instantiates binders, creating a valid local context for the subexpression, and the second doesn't.

[Adam Topaz]

Thanks sounds promising! Thanks!

[Adam Topaz]

Works exactly as expected! Here is an example in case someone looks for this in the future:

import Lean
import Qq
open Lean Qq

#eval show MetaM Unit from do
  let a : Q(Nat) ← mkFreshExprMVarQ q(Nat)
  let e1 := q(($a + 1) + 2)
  let e2 := q(($a + 4) + 2)
  let d ← Lean.Widget.exprDiff e1 e2
  for (i,_) in d.changesBefore do
    IO.println s!"{← Core.viewSubexpr i e1}"
  for (i,_) in d.changesAfter do
    IO.println s!"{← Core.viewSubexpr i e2}"

[Kyle Miller]

(Note that if the diffs are under binders, then Core.viewSubexpr might give expressions with bvars)