Lexicographic order on `SubExpr.Pos`

Stream: lean4

[Eric Wieser]

Does the order which sorts SubExpr.Pos from left to right exist? It would allow lookup in an RBMap for "match or ancestor", using docs#RBMap.lowerBound and something like

/-- Determine if `a` is an ancestor of `b`. -/
partial def Lean.SubExpr.Pos.isAncestorOf (a b : SubExpr.Pos) : Bool :=
  if (a.push 0).asNat ≤ b.asNat then
    a.isAncestorOf b.tail
  else
    a.asNat == b.asNat

[Kyle Miller]

If this is for doing computations on positions that come from the delaborator, something to watch out for is that some positions are non-hierarchical, coming from docs#Lean.PrettyPrinter.Delaborator.SubExpr.nextExtraPos. These are characterized by the fact that in base-4 they start with 2 or 3, unlike the hierarchical positions, which start with 1.

For hierarchical positions, I think using lex order on the result of docs#Lean.SubExpr.Pos.toArray gives what you want.

An algorithm that would involve less memory allocation would be to take positions a and b (represented as Nat), find m and n such that the log-base-4 of a*4^m and b*4^n have the same integer part (one of m or n can be zero), and then use the usual Nat order.

[Kyle Miller]

Maybe this?

def log4 (n : Nat) : Nat :=
  let rec go (n : Nat) (acc : Nat) : Nat :=
    if n < 4 then
      acc
    else
      go (n / 4) (acc + 1)
  go n 0

def Lean.SubExpr.Pos.compare (a b : Pos) : Ordering :=
  let m := log4 a.asNat
  let n := log4 b.asNat
  Ord.compare (a.asNat * 4^(n-m)) (b.asNat * 4^(m-n))

[Eric Wieser]

log4 is docs#Lean.SubExpr.Pos.depth, right?

[Kyle Miller]

Yes, looks like it

[Eric Wieser]

Is the non-heirarchical representation documented anywhere?

[Kyle Miller]

(Side note: it's pretty amazing that the termination checker works for definitions like log4 now)

[Eric Wieser]

(I guess foldr could be made non-partial then?)

[Kyle Miller]

Eric Wieser said:

Is the non-heirarchical representation documented anywhere?

Only barely, near nextExtraPos, but it doesn't say what they're for.

[Eric Wieser]

The context of this question was working out how to expand the positions in the return value of docs#Lean.Widget.exprDiff to correspond to the actual subexpressions that exist in the tagged text

[Eric Wieser]

Since right now, the diff can compute a diff in a position which isn't hoverable in the infoview, and so no diff appears

[Kyle Miller]

I think something to keep in mind is that SubExpr.Pos is not meant to be an index into the expression

[Kyle Miller]

It's simply a scheme to get unique identifiers without needing to keep track of global state

[Kyle Miller]

Delaborators are allowed to synthesize new subexpr positions as needed, so long as it's done in a way that won't collide with others

[Kyle Miller]

The linkage of a Pos to an expr is in the collected State.infos map

[Kyle Miller]

Eric Wieser said:

Since right now, the diff can compute a diff in a position which isn't hoverable in the infoview, and so no diff appears

Hmm, the diff code assumes that positions really do correspond to subexpressions...

[Kyle Miller]

Regarding non-hierarchical positions, they only really show up in a couple places: structure instance fields, so you can hover over x and y in {x := 1, y := 2}, and on binders.

[Kyle Miller]

Something that would be more robust would be if the diff code left mdata nodes in the expression with pp configuration

[Kyle Miller]

Eric Wieser said:

Since right now, the diff can compute a diff in a position which isn't hoverable in the infoview, and so no diff appears

Did you run into cases that aren't literals? Arguably the diff routine should know about OfNat expressions.

[Eric Wieser]

The case I was trying to handle was display the diff between a_very_long_name + another_long_name and a_very_long_name - another_long_name as just on the + / - character, though obviously that's not the same example as the one I summarize above.

[Kyle Miller]

For that, if you add pp.tagAppFns at the position of a + b/a - b, it'll make + and - hoverable, though I think the Pos will be for HAdd.hAdd and HSub.hSub

[Eric Wieser]

Do you think it would be reasonable for the diffing machinery to do this automatically?

[Kyle Miller]

You can at least do set_option pp.tagAppFns true to experiment to see if it works, without spending time trying to make the option be precisely set

[Eric Wieser]

Great, thanks!

[Eric Wieser]

In particular, I'm thinking about things like fooHom x y vs foo x y, where seeing only the function application changing would be helpful

[Kyle Miller]

Eric Wieser said:

Do you think it would be reasonable for the diffing machinery to do this automatically?

I'm wondering if diffing should be "inside" the delaborator, like a variant of docs#Lean.PrettyPrinter.delabCore that takes two expressions and annotates expressions in a delaborator-aware way. Note for example that delabCore can do transformations like beta reduction or metavariable instantiation (plus, some delaborators do eta reduction of certain terms).

Or, there's docs#Lean.Meta.addPPExplicitToExposeDiff, which adds pp.explicit meta nodes to show differences. It's still trying to recapitulate the delaborator by making educated guesses of where pp.explicits are needed, but at least it's not messing around with getting positions right.

[Kyle Miller]

I could see something like addPPExplicitToExposeDiff that inserts annotations (including tagAppFns if the differences is on the function), and then having a post-delaboration pass that works on Syntax directly, if you want to mark differences with colors.

[Kyle Miller]

It might take some fixes to core delaborators to make sure these annotations are respected in all cases, which I think we can allocate some resources doing.