feat: traversal functions for Expr and SubExpr
#1208
Conversation
EdAyers
force-pushed
the
expr-lens
branch
2 times, most recently
from
f9cba8d to
79d0943
Compare
@leodemoura and I briefly talked about this PR, we are fine with merging all this into core |
Instead of an abbreviation. It is easier to understand Pos operations in terms of 'push' and 'pop' rather than through arithmetic.
Lean.Meta.transform is created with a series of recursive visit functions. However these visit functions are useful on their own outside of transform for traversing expressions. This commit moves the visit functions outside the main function.
This found a bug in lensCoord which I fixed.
src/Lean/SubExpr.lean
Outdated
| variable {α : Type} [Inhabited α] | ||
|
|
||
| /-- Fold over the position starting at the root and heading to the leaf-/ | ||
| def foldl (f : α → Nat → α) : α → Pos → α := |
There was a problem hiding this comment.
foldup? folddown? When you imagine an expression tree is the root at the top or the bottom?
|
|
||
| /-- Similar to `traverseLambda` but with an additional pos argument to track position. -/ | ||
| def traverseLambdaWithPos | ||
| (f : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr := visit #[] p e |
There was a problem hiding this comment.
Alternative formulation: make
structure ExprTraverseContext with
(pos : Pos)
(fvars : Array Expr)
and then
traverseXXXWithPos (f : Expr → ReaderT ExprTraverseContext Expr) : Expr → ReaderT ExprTraverseContext Expr
Or perhaps instead include the variable instances [MonadReader ExprTraverseContext M] and [MonadReaderWith ExprTraverseContext M]?
|
Why is Linux fsanitize crashing? https://github.com/leanprover/lean4/runs/6909389488?check_suite_focus=true#step:15:2360 |
This is needed because JSON will otherwise lossily convert big nats to floats.
@leodemoura It looks like we're leaking Lines 31 to 32 in 7a3ee51 |
Please do not use these functions. I meant to remove them a long time ago. They have runtime support, and were added to solve performance problems in the old parser engine we had. The problem that motivated these primitives does not even exist anymore, and I don't see a strong motivation for having them as primitives in our runtime. |
|
@EdAyers Could you please rewrite the code and avoid the Thanks, |
I'm working on a 'contextual suggestion' API for the Lean infoview which lets the user click on subexpressions in the infoview and see suggested tactics for these. In order to create this I ended up with quite a few functions for working with
SubExpr.Posand traversing and lensing on expressions with these.I am happy to break these up in to multiple PRs if the reviewers find that appropriate.
I am also happy to instead merge any/all of these features in mathlib instead.
List of features in this PR:
SubExpr.Pos:pushpopisRootetc.Lean/Meta/ExprTraverse.leancontains a set of traversal functions for expressions. These generalise thevisitfunctions used intransform(it is possible to replace the implementation oftransformwith these traversal functions and all the tests still pass)Lean/Meta/ExprLens.leanis a set of methods for working on subexpressions ofe : Exprindexed byp : SubExpr.Pos. The main functions areviewSubexpr (visit : (fvars : Array Expr) → (subexpr: Expr) → M α) (p : Pos) (root : Expr) : M αwhich runsvisitat the subexpression ofrootaddressed byp. (with bound variables properly instantiated)replaceSubexpr (replace : (subexpr : Expr) → M Expr) (p : Pos) (root : Expr) : M Exprreplaces the expression at the given position using thereplacefunction. Again making sure that the Meta context is correct.Todo list
replaceSubExpr