From 624fa60b9c319a35b9f3ec6f76e63191dd3d4deb Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 3 Jun 2022 15:12:23 -0400 Subject: [PATCH 01/16] refactor: make SubExpr.Pos a definition Instead of an abbreviation. It is easier to understand Pos operations in terms of 'push' and 'pop' rather than through arithmetic. --- .../PrettyPrinter/Delaborator/SubExpr.lean | 14 ++-- src/Lean/SubExpr.lean | 81 ++++++++++++++++++- src/Lean/Widget/InteractiveCode.lean | 4 +- tests/lean/PPRoundtrip.lean | 2 +- tests/lean/run/subexpr.lean | 13 +++ 5 files changed, 100 insertions(+), 14 deletions(-) create mode 100644 tests/lean/run/subexpr.lean diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index b00e20da7091..3e93c1f46204 100644 --- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -33,14 +33,14 @@ variable [MonadLiftT IO m] def getExpr : m Expr := return (← readThe SubExpr).expr def getPos : m Pos := return (← readThe SubExpr).pos -def descend (child : Expr) (childIdx : Pos) (x : m α) : m α := - withTheReader SubExpr (fun cfg => { cfg with expr := child, pos := cfg.pos * maxChildren + childIdx }) x +def descend (child : Expr) (childIdx : Nat) (x : m α) : m α := + withTheReader SubExpr (fun cfg => { cfg with expr := child, pos := cfg.pos.push childIdx }) x def withAppFn (x : m α) : m α := do descend (← getExpr).appFn! 0 x def withAppArg (x : m α) : m α := do descend (← getExpr).appArg! 1 x def withType (x : m α) : m α := do - descend (← Meta.inferType (← getExpr)) (maxChildren - 1) x -- phantom positions for types + descend (← Meta.inferType (← getExpr)) Pos.typeCoord x -- phantom positions for types partial def withAppFnArgs (xf : m α) (xa : α → m α) : m α := do if (← getExpr).isApp then @@ -80,20 +80,20 @@ def withLetBody (x : m α) : m α := do def withNaryFn (x : m α) : m α := do let e ← getExpr let n := e.getAppNumArgs - let newPos := (← getPos) * (maxChildren ^ n) + let newPos := (← getPos).asNat * (Pos.maxChildren ^ n) withTheReader SubExpr (fun cfg => { cfg with expr := e.getAppFn, pos := newPos }) x def withNaryArg (argIdx : Nat) (x : m α) : m α := do let e ← getExpr let args := e.getAppArgs - let newPos := (← getPos) * (maxChildren ^ (args.size - argIdx)) + 1 + let newPos := (← getPos).asNat * (Pos.maxChildren ^ (args.size - argIdx)) + 1 withTheReader SubExpr (fun cfg => { cfg with expr := args[argIdx], pos := newPos }) x end Descend structure HoleIterator where curr : Nat := 2 - top : Nat := maxChildren + top : Nat := Pos.maxChildren deriving Inhabited section Hole @@ -107,7 +107,7 @@ def HoleIterator.toPos (iter : HoleIterator) : Pos := def HoleIterator.next (iter : HoleIterator) : HoleIterator := if (iter.curr+1) == iter.top then - ⟨2*iter.top, maxChildren*iter.top⟩ + ⟨2*iter.top, Pos.maxChildren*iter.top⟩ else ⟨iter.curr+1, iter.top⟩ /-- The positioning scheme guarantees that there will be an infinite number of extra positions diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index 0da91e00dc0f..07af20a33961 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -1,9 +1,10 @@ /- Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki +Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki, E.W.Ayers -/ import Lean.Meta.Basic +import Lean.Data.Json import Std.Data.RBMap namespace Lean @@ -11,7 +12,80 @@ namespace Lean /-- A position of a subexpression in an expression. See docstring of `SubExpr` for more detail.-/ -abbrev SubExpr.Pos := Nat +def SubExpr.Pos := Nat + +namespace SubExpr.Pos + +def maxChildren := 4 + +/-- The coordinate `3 = maxChildren - 1` is +reserved to denote the type of the expression. -/ +def typeCoord : Nat := maxChildren - 1 + +def asNat : Pos → Nat := id + +instance : Inhabited Pos := show Inhabited Nat by infer_instance +instance : Ord Pos := show Ord Nat by infer_instance +instance : FromJson Pos := show FromJson Nat by infer_instance +instance : ToJson Pos := show ToJson Nat by infer_instance +instance : Repr Pos := show Repr Nat by infer_instance +instance : ToString Pos := show ToString Nat by infer_instance + +/-- The Pos representing the root subexpression. -/ +def root : Pos := (1 : Nat) + +def isRoot (p : Pos) : Bool := p.asNat == 1 + +/-- The coordinate deepest in the Pos. -/ +def head (p : Pos) : Nat := + if p.isRoot then panic! "already at top" + else p.asNat % maxChildren + +def tail (p : Pos) : Pos := + if p.isRoot then panic! "already at top" + else (p.asNat - p.head) / maxChildren + +def push (p : Pos) (c : Nat) : Pos := + if c >= maxChildren then panic! s!"invalid coordinate {c}" + else p.asNat * maxChildren + c + +/-- `pushNZeros p count` runs `.push 0` `count` times. -/ +def pushNZeros (p : Pos) (count : Nat) : Pos := + p.asNat * (maxChildren ^ count) + +variable {α : Type} [Inhabited α] + +/-- Fold over the position starting at the root and heading to the leaf-/ +def foldl (f : α → Nat → α) : α → Pos → α := + fix2 (fun r a p => if p.isRoot then a else f (r a p.tail) p.head) + +/-- Fold over the position starting at the root and heading to the leaf-/ +def foldr (f : Nat → α → α) : Pos → α → α := + fix2 (fun r p a => if p.isRoot then a else r p.tail (f p.head a)) + +def foldrM [Monad M] (f : Nat → α → M α) : Pos → α → M α := + fix2 (fun r p a => if p.isRoot then pure a else f p.head a >>= r p.tail) + +def depth (p : Pos) := + p.foldr (fun _ => Nat.succ) 0 + +/-- Returns true if `pred` is true for each coordinate in `p`.-/ +def all (pred : Nat → Bool) (p : Pos) : Bool := + OptionT.run (m := Id) (foldrM (fun n a => if pred n then pure a else failure) p ()) |>.isSome + +def append : Pos → Pos → Pos := foldl push + +/-- Creates a subexpression `Pos` from an array of 'coordinates'. +Each coordinate is a number {0,1,2} expressing which child subexpression should be explored. +The first coordinate in the array corresponds to the root of the expression tree. -/ +def ofArray (ps : Array Nat) : Pos := + ps.foldl push root + +/-- Decodes a subexpression `Pos` as a sequence of coordinates. See `Pos.fromArray` for details.-/ +def toArray (p : Pos) : Array Nat := + foldl Array.push #[] p + +end SubExpr.Pos /-- An expression and the position of a subexpression within this expression. @@ -30,8 +104,7 @@ structure SubExpr where namespace SubExpr -abbrev maxChildren : Pos := 4 -def mkRoot (e : Expr) : SubExpr := ⟨e, 1⟩ +def mkRoot (e : Expr) : SubExpr := ⟨e, Pos.root⟩ end SubExpr diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean index 965b34c11cc1..7f25dd8b8cc7 100644 --- a/src/Lean/Widget/InteractiveCode.lean +++ b/src/Lean/Widget/InteractiveCode.lean @@ -46,8 +46,8 @@ where def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do let optsPerPos := if explicit then Std.RBMap.ofList [ - (1, KVMap.empty.setBool `pp.all true), - (1, KVMap.empty.setBool `pp.tagAppFns true) + (SubExpr.Pos.root, KVMap.empty.setBool `pp.all true), + (SubExpr.Pos.root, KVMap.empty.setBool `pp.tagAppFns true) ] else {} diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 0ee518c05353..221f412a5946 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -58,7 +58,7 @@ section #eval checkM `(id Nat) #eval checkM `(Sum Nat Nat) end -#eval checkM `(id (id Nat)) (Std.RBMap.empty.insert 5 $ KVMap.empty.insert `pp.explicit true) +#eval checkM `(id (id Nat)) (Std.RBMap.empty.insert (SubExpr.Pos.encode #[1]) $ KVMap.empty.insert `pp.explicit true) -- specify the expected type of `a` in a way that is not erased by the delaborator def typeAs.{u} (α : Type u) (a : α) := () diff --git a/tests/lean/run/subexpr.lean b/tests/lean/run/subexpr.lean new file mode 100644 index 000000000000..4af899d20458 --- /dev/null +++ b/tests/lean/run/subexpr.lean @@ -0,0 +1,13 @@ +import Lean +open Lean.SubExpr + +def ps := [#[], #[0], #[1], #[0,1], #[1,0] , #[0,0], #[1,2,3]] +theorem Pos.roundtrip : + true = ps.all fun x => x == (Pos.toArray <| Pos.ofArray <| x) + := by native_decide + +theorem Pos.append_roundtrip : + true = (List.all + (ps.bind fun p => ps.map fun q => (p,q)) + (fun (x,y) => (x ++ y) == (Pos.toArray <| (Pos.append (Pos.ofArray x) (Pos.ofArray y)))) + ) := by native_decide From 328f82280b6da372cde04761bf618c8d22a506aa Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 3 Jun 2022 16:10:37 -0400 Subject: [PATCH 02/16] feat: add Expr lensing functions using SubExpr.Pos --- src/Lean/Meta.lean | 1 + src/Lean/Meta/ExprLens.lean | 151 ++++++++++++++++++++++++++++++++++++ src/Lean/SubExpr.lean | 6 ++ 3 files changed, 158 insertions(+) create mode 100644 src/Lean/Meta/ExprLens.lean diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean index 5147a725442c..e2cbdbf943ea 100644 --- a/src/Lean/Meta.lean +++ b/src/Lean/Meta.lean @@ -40,3 +40,4 @@ import Lean.Meta.Constructions import Lean.Meta.CongrTheorems import Lean.Meta.Eqns import Lean.Meta.CasesOn +import Lean.Meta.ExprLens diff --git a/src/Lean/Meta/ExprLens.lean b/src/Lean/Meta/ExprLens.lean new file mode 100644 index 000000000000..56384ef709c3 --- /dev/null +++ b/src/Lean/Meta/ExprLens.lean @@ -0,0 +1,151 @@ +import Lean.Meta.Basic +import Lean.SubExpr + +namespace Lean.Meta + +section ExprLens + +open Lean.SubExpr + +/-! +## SubExpr as a Lens + +A `s : SubExpr` object can be considered as a [Lens](https://hackage.haskell.org/package/optics-core-0.4.1/docs/Optics-Lens.html). +However in order to perform meaningful lensing and viewing we need to adjust the local context when we lens under a binder in `s.expr`. +-/ + +variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M] + +/-- Given a constructor index for Expr, runs `g` on the value of that subexpression and replaces it. +If the subexpression is under a binder it will instantiate and abstract the binder body correctly. +Mdata is ignored. An index of 3 is interpreted as the type of the expression. An index of 3 will throw since we can't replace types. + +See also `Lean.Meta.transform`. -/ +private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr + | 0, e@(Expr.app f a _) => return e.updateApp! (← g f) a + | 1, e@(Expr.app f a _) => return e.updateApp! f (← g a) + | 0, e@(Expr.lam _ y b _) => return e.updateLambdaE! (← g y) b + | 1, e@(Expr.lam n y b c) => return e.updateLambdaE! y <|← withLocalDecl n c.binderInfo y fun x => do mkLambdaFVars #[x] (← g (b.instantiateRev #[x])) + | 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b + | 1, e@(Expr.forallE n y b c) => return e.updateForallE! y <|← withLocalDecl n c.binderInfo y fun x => do mkForallFVars #[x] (← g (b.instantiateRev #[x])) + | 0, e@(Expr.letE _ y a b _) => return e.updateLet! (← g y) a b + | 1, e@(Expr.letE _ y a b _) => return e.updateLet! y (← g a) b + | 2, e@(Expr.letE n y a b _) => return e.updateLet! y a (← withLetDecl n y a fun x => do mkLetFVars #[x] (← g (b.instantiateRev #[x]))) + | 0, e@(Expr.proj _ _ b _) => pure e.updateProj! <*> g b + | n, e@(Expr.mdata _ a _) => pure e.updateMData! <*> lensCoord g n a + | 3, _ => throwError "Lensing on types is not supported" + | c, e => throwError "Invalid coordinate {c} for {e}" + +private def lensAux (g : Expr → M Expr) : List Nat → Expr → M Expr + | [], e => g e + | head::tail, e => lensCoord (lensAux g tail) head e + +/-- Run the given `g` function to replace the expression at the subexpression position. If the subexpression is below a binder +the bound variables will be appropriately instantiated with free variables and reabstracted after the replacement. +If the subexpression is invalid or points to a type then this will throw. -/ +def lensSubexpr (g : (subexpr : Expr) → M Expr) (p : Pos) (e : Expr) : M Expr := + lensAux g p.toArray.toList e + +/-- Runs `k` on the given coordinate, including handling binders properly. +The subexpression value passed to `k` is not instantiated with respect to the +array of free variables. -/ +private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) : Nat → Expr → M α + | 3, _ => throwError "Internal: Types should be handled by viewAux" + | 0, (Expr.app f _ _) => k fvars f + | 1, (Expr.app _ a _) => k fvars a + | 0, (Expr.lam _ y _ _) => k fvars y + | 1, (Expr.lam n y b c) => withLocalDecl n c.binderInfo (y.instantiateRev fvars) fun x => k (fvars.push x) b + | 0, (Expr.forallE _ y _ _) => k fvars y + | 1, (Expr.forallE n y b c) => withLocalDecl n c.binderInfo (y.instantiateRev fvars) fun x => k (fvars.push x) b + | 0, (Expr.letE _ y _ _ _) => k fvars y + | 1, (Expr.letE _ _ a _ _) => k fvars a + | 2, (Expr.letE n y a b _) => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b + | 0, (Expr.proj _ _ b _) => k fvars b + | n, (Expr.mdata _ a _) => viewCoordAux k fvars n a + | c, e => throwError "Invalid coordinate {c} for {e}" + +private def viewAux (k : Array Expr → Expr → M α) (fvars : Array Expr) : List Nat → Expr → M α + | [], e => k fvars <| e.instantiateRev fvars + | 3::tail, e => do + let y ← inferType <| e.instantiateRev fvars + viewAux (fun otherFvars => k (fvars ++ otherFvars)) #[] tail y + | head::tail, e => viewCoordAux (fun fvars => viewAux k fvars tail) fvars head e + +/-- `view k p e` runs `k fvars s` where `s : Expr` is the subexpression of `e` at `p`. +and `fvars` are the free variables for the binders that `s` is under. +`s` is already instantiated with respect to these. +The role of the `k` function is analogous to the `k` function in `Lean.Meta.forallTelescope`. -/ +def viewSubexpr + (k : (fvars : Array Expr) → (subexpr : Expr) → M α) + : Pos → Expr → M α + | p, e => viewAux k #[] p.toArray.toList e + +private def foldAncestorsAux + (k : Array Expr → Expr → Nat → α → M α) + (acc : α) (address : List Nat) (fvars : Array Expr) (current : Expr) : M α := + match address with + | [] => return acc + | 3 :: tail => do + let current := current.instantiateRev fvars + let y ← inferType current + let acc ← k fvars current 3 acc + foldAncestorsAux (fun otherFvars => k (fvars ++ otherFvars)) acc tail #[] y + | head :: tail => do + let acc ← k fvars (current.instantiateRev fvars) head acc + viewCoordAux (foldAncestorsAux k acc tail) fvars head current + +/-- `foldAncestors k init p e` folds over the strict ancestor subexpressions of the given expression `e` above position `p`, starting at the root expression and working down. +The fold function `k` is given the newly instantiated free variables, the ancestor subexpression, and the coordinate +that will be explored next.-/ +def foldAncestors + (k : (fvars: Array Expr) → (subexpr : Expr) → (nextCoord : Nat) → α → M α) + (init : α) (p : Pos) (e : Expr) : M α := + foldAncestorsAux k init p.toArray.toList #[] e + +end ExprLens + +end Lean.Meta + +namespace Lean.SubExpr + +section ViewRaw + +open Except in +/-- Get the raw subexpression without performing any instantiation. -/ +private def viewCoordRaw: Nat → Expr → Except String Expr + | 3, e => error s!"Can't viewRaw the type of {e}" + | 0, (Expr.app f _ _) => ok f + | 1, (Expr.app _ a _) => ok a + | 0, (Expr.lam _ y _ _) => ok y + | 1, (Expr.lam _ _ b _) => ok b + | 0, (Expr.forallE _ y _ _) => ok y + | 1, (Expr.forallE _ _ b _) => ok b + | 0, (Expr.letE _ y _ _ _) => ok y + | 1, (Expr.letE _ _ a _ _) => ok a + | 2, (Expr.letE _ _ _ b _) => ok b + | 0, (Expr.proj _ _ b _) => ok b + | n, (Expr.mdata _ a _) => viewCoordRaw n a + | c, e => error s!"Bad coordinate {c} for {e}" + +open Except in +/-- Given a valid SubExpr, will return the raw current expression without performing any instantiation. +If the SubExpr has a type subexpression coordinate then will error. + +This is a cheaper version of `SubExpr.view` and can be used to quickly view the +subexpression at a position. Note that because the resulting expression will contain +loose bound variables it can't be used in any `MetaM` methods. -/ +def viewRaw (p : Pos) (e : Expr) : Except String Expr := + aux e p.toArray.toList + where + aux (e : Expr) + | head :: tail => + match viewCoordRaw head e with + | ok e => aux e tail + | error m => error m + | [] => ok e + +end ViewRaw + +end Lean.SubExpr + + diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index 07af20a33961..8176663d7f60 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -106,6 +106,12 @@ namespace SubExpr def mkRoot (e : Expr) : SubExpr := ⟨e, Pos.root⟩ +/-- Returns true if the selected subexpression is the topmost one.-/ +def isRoot (s : SubExpr) : Bool := s.pos.isRoot + +def mapPos (f : Pos → Pos) : SubExpr → SubExpr + | ⟨e,p⟩ => ⟨e, f p⟩ + end SubExpr end Lean From 13a852ac1d8e590fcb817f41571fbe2a83fd991c Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 3 Jun 2022 19:29:57 -0400 Subject: [PATCH 03/16] refactor: extract methods from Lean.Meta.transform 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. --- src/Lean/Meta/Transform.lean | 101 ++++++++++++++++++++++------------- 1 file changed, 65 insertions(+), 36 deletions(-) diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index d5dc31eb7063..9a7da21678b0 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, E.W.Ayers -/ import Lean.Meta.Basic @@ -11,6 +11,13 @@ inductive TransformStep where | done (e : Expr) | visit (e : Expr) + +/-- Given `e = fn a₁ ... aₙ`, runs `f` on `fn` and each of the arguments `aᵢ` and +makes a new function application with the results. -/ +def Expr.traverseApp {M} [Monad M] + (f : Expr → M Expr) (e : Expr) : M Expr := + e.withApp fun fn args => (pure mkAppN) <*> (f fn) <*> (args.mapM f) + namespace Core /-- @@ -58,10 +65,59 @@ end Core namespace Meta +variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M] + +def usedLetOnly : M Bool := getBoolOption `visit.usedLetOnly false + +/-- Given an expression `fun (x₁ : α₁) ... (xₙ : αₙ) => b`, will run +`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, +replacing each expression with the output of `f` and creating a new lambda. +(that is, correctly instantiating bound variables and repackaging them after) -/ +def traverseLambda + (f : Expr → M Expr) (e : Expr) : M Expr := visit #[] e + where visit (fvars : Array Expr) : Expr → M Expr + | (Expr.lam n d b c) => do withLocalDecl n c.binderInfo (← f (d.instantiateRev fvars)) fun x => visit (fvars.push x) b + | e => do mkLambdaFVars (usedLetOnly := ← usedLetOnly) fvars (← f (e.instantiateRev fvars)) + +/-- Given an expression ` (x₁ : α₁) → ... → (xₙ : αₙ) → b`, will run +`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, +replacing the expression with the output of `f` and creating a new forall expression. +(that is, correctly instantiating bound variables and repackaging them after) -/ +def traverseForall + (f : Expr → M Expr) (e : Expr) : M Expr := visit #[] e + where visit fvars : Expr → M Expr + | (Expr.forallE n d b c) => do withLocalDecl n c.binderInfo (← f (d.instantiateRev fvars)) fun x => visit (fvars.push x) b + | e => do mkForallFVars (usedLetOnly := ←usedLetOnly) fvars (← f (e.instantiateRev fvars)) + +/-- Similar to traverseLambda and traverseForall but with let binders. -/ +def traverseLet + (f : Expr → M Expr) (e : Expr) : M Expr := visit #[] e + where visit fvars + | Expr.letE n t v b _ => do + withLetDecl n (← f (t.instantiateRev fvars)) (← f (v.instantiateRev fvars)) fun x => + visit (fvars.push x) b + | e => do mkLetFVars (usedLetOnly := ←usedLetOnly) fvars (← f (e.instantiateRev fvars)) + +/-- Maps `f` on each child of the given expression. + +Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...). +So `traverseChildren f e` where ``e = `(fn a₁ ... aₙ)`` will return +``(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))`` rather than ``(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))`` + -/ +def traverseChildren (f : Expr → M Expr) (e: Expr) : M Expr := do + match e with + | Expr.forallE .. => traverseForall f e + | Expr.lam .. => traverseLambda f e + | Expr.letE .. => traverseLet f e + | Expr.app .. => Expr.traverseApp f e + | Expr.mdata _ b _ => return e.updateMData! (← f b) + | Expr.proj _ _ b _ => return e.updateProj! (← f b) + | _ => return e + /-- Similar to `Core.transform`, but terms provided to `pre` and `post` do not contain loose bound variables. So, it is safe to use any `MetaM` method at `pre` and `post`. -/ -partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadTrace m] [MonadRef m] [MonadOptions m] [AddMessageContext m] +partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadTrace m] [MonadRef m] [MonadOptions m] [MonadWithOptions m] [AddMessageContext m] (input : Expr) (pre : Expr → m TransformStep := fun e => return TransformStep.visit e) (post : Expr → m TransformStep := fun e => return TransformStep.done e) @@ -71,42 +127,15 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) } let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do - let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do - match (← post e) with - | TransformStep.done e => pure e - | TransformStep.visit e => visit e - let rec visitLambda (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do - match e with - | Expr.lam n d b c => - withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x => - visitLambda (fvars.push x) b - | e => visitPost (← mkLambdaFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars))) - let rec visitForall (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do - match e with - | Expr.forallE n d b c => - withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x => - visitForall (fvars.push x) b - | e => visitPost (← mkForallFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars))) - let rec visitLet (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do - match e with - | Expr.letE n t v b _ => - withLetDecl n (← visit (t.instantiateRev fvars)) (← visit (v.instantiateRev fvars)) fun x => - visitLet (fvars.push x) b - | e => visitPost (← mkLetFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars))) - let visitApp (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := - e.withApp fun f args => do - visitPost (mkAppN (← visit f) (← args.mapM visit)) match (← pre e) with | TransformStep.done e => pure e - | TransformStep.visit e => match e with - | Expr.forallE .. => visitForall #[] e - | Expr.lam .. => visitLambda #[] e - | Expr.letE .. => visitLet #[] e - | Expr.app .. => visitApp e - | Expr.mdata _ b _ => visitPost (e.updateMData! (← visit b)) - | Expr.proj _ _ b _ => visitPost (e.updateProj! (← visit b)) - | _ => visitPost e - visit input |>.run + | TransformStep.visit e => + let e ← traverseChildren visit e + match (← post e) with + | TransformStep.done e => pure e + | TransformStep.visit e => visit e + withOptions (fun o => o.setBool `visit.usedLetOnly usedLetOnly) + (visit input |>.run) def zetaReduce (e : Expr) : MetaM Expr := do let pre (e : Expr) : MetaM TransformStep := do From fad151cacd61af3e9ac112f2bcb07043291d9845 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 3 Jun 2022 19:54:32 -0400 Subject: [PATCH 04/16] fix: test --- tests/lean/PPRoundtrip.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 221f412a5946..81e1d980892c 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -58,7 +58,7 @@ section #eval checkM `(id Nat) #eval checkM `(Sum Nat Nat) end -#eval checkM `(id (id Nat)) (Std.RBMap.empty.insert (SubExpr.Pos.encode #[1]) $ KVMap.empty.insert `pp.explicit true) +#eval checkM `(id (id Nat)) (Std.RBMap.empty.insert (SubExpr.Pos.ofArray #[1]) $ KVMap.empty.insert `pp.explicit true) -- specify the expected type of `a` in a way that is not erased by the delaborator def typeAs.{u} (α : Type u) (a : α) := () From e062c52ec412eee511003de635e80fa81fcdb726 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Sun, 5 Jun 2022 17:02:46 -0400 Subject: [PATCH 05/16] refactor: more extract methods from transform --- src/Lean/Expr.lean | 6 +++++ src/Lean/Meta/Transform.lean | 45 +++++++++++++++++++++--------------- 2 files changed, 32 insertions(+), 19 deletions(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index b24d2fdd134d..666b3e593ff5 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -597,6 +597,12 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr let nargs := e.getAppNumArgs withAppAux k e (mkArray nargs dummy) (nargs-1) +/-- Given `e = fn a₁ ... aₙ`, runs `f` on `fn` and each of the arguments `aᵢ` and +makes a new function application with the results. -/ +def traverseApp {M} [Monad M] + (f : Expr → M Expr) (e : Expr) : M Expr := + e.withApp fun fn args => mkAppN <$> f fn <*> args.mapM f + @[specialize] private def withAppRevAux (k : Expr → Array Expr → α) : Expr → Array Expr → α | app f a _, as => withAppRevAux k f (as.push a) | f, as => k f as diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index 9a7da21678b0..edfe597bc970 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -11,14 +11,26 @@ inductive TransformStep where | done (e : Expr) | visit (e : Expr) +namespace Core -/-- Given `e = fn a₁ ... aₙ`, runs `f` on `fn` and each of the arguments `aᵢ` and -makes a new function application with the results. -/ -def Expr.traverseApp {M} [Monad M] - (f : Expr → M Expr) (e : Expr) : M Expr := - e.withApp fun fn args => (pure mkAppN) <*> (f fn) <*> (args.mapM f) +/-- Maps `visit` on each child of the given expression. -namespace Core +Loose bound variables are not instantiated. +Use `Lean.Meta.traverseChildren` to avoid loose bound variables. + +Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...). +So `traverseChildren f e` where ``e = `(fn a₁ ... aₙ)`` will return +``(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))`` rather than ``(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))`` + -/ +def traverseChildren {M} [Monad M] (visit : Expr → M Expr) (e: Expr) : M Expr := + match e with + | Expr.forallE _ d b _ => e.updateForallE! <$> visit d <*> visit b + | Expr.lam _ d b _ => e.updateLambdaE! <$> visit d <*> visit b + | Expr.letE _ t v b _ => e.updateLet! <$> visit t <*> visit v <*> visit b + | Expr.app .. => e.traverseApp visit + | Expr.mdata _ b _ => e.updateMData! <$> visit b + | Expr.proj _ _ b _ => e.updateProj! <$> visit b + | _ => pure e /-- Tranform the expression `input` using `pre` and `post`. @@ -42,20 +54,13 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m] let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := CoreM) (liftM (m := ST IO.RealWorld) x) } let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := checkCache { val := e : ExprStructEq } fun _ => Core.withIncRecDepth do - let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do - match (← post e) with - | TransformStep.done e => pure e - | TransformStep.visit e => visit e match (← pre e) with | TransformStep.done e => pure e - | TransformStep.visit e => match e with - | Expr.forallE _ d b _ => visitPost (e.updateForallE! (← visit d) (← visit b)) - | Expr.lam _ d b _ => visitPost (e.updateLambdaE! (← visit d) (← visit b)) - | Expr.letE _ t v b _ => visitPost (e.updateLet! (← visit t) (← visit v) (← visit b)) - | Expr.app .. => e.withApp fun f args => do visitPost (mkAppN (← visit f) (← args.mapM visit)) - | Expr.mdata _ b _ => visitPost (e.updateMData! (← visit b)) - | Expr.proj _ _ b _ => visitPost (e.updateProj! (← visit b)) - | _ => visitPost e + | TransformStep.visit e => do + let e ← traverseChildren visit e + match (← post e) with + | TransformStep.done e => pure e + | TransformStep.visit e => visit e visit input |>.run def betaReduce (e : Expr) : CoreM Expr := @@ -67,7 +72,7 @@ namespace Meta variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M] -def usedLetOnly : M Bool := getBoolOption `visit.usedLetOnly false +private def usedLetOnly : M Bool := getBoolOption `visit.usedLetOnly false /-- Given an expression `fun (x₁ : α₁) ... (xₙ : αₙ) => b`, will run `f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, @@ -103,6 +108,8 @@ def traverseLet Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...). So `traverseChildren f e` where ``e = `(fn a₁ ... aₙ)`` will return ``(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))`` rather than ``(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))`` + +See also `Lean.Core.traverseChildren`. -/ def traverseChildren (f : Expr → M Expr) (e: Expr) : M Expr := do match e with From 880dadf7b62187e5fb15b3983b5ab15deba04904 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 8 Jun 2022 15:50:57 -0400 Subject: [PATCH 06/16] feat: with pos expr traversal functions --- src/Lean/Meta/ExprLens.lean | 10 ++- src/Lean/Meta/ExprTraverse.lean | 90 +++++++++++++++++++ src/Lean/Meta/Transform.lean | 52 +---------- .../PrettyPrinter/Delaborator/SubExpr.lean | 5 +- src/Lean/SubExpr.lean | 25 ++++++ 5 files changed, 124 insertions(+), 58 deletions(-) create mode 100644 src/Lean/Meta/ExprTraverse.lean diff --git a/src/Lean/Meta/ExprLens.lean b/src/Lean/Meta/ExprLens.lean index 56384ef709c3..b9e42a2f84e6 100644 --- a/src/Lean/Meta/ExprLens.lean +++ b/src/Lean/Meta/ExprLens.lean @@ -106,7 +106,9 @@ end ExprLens end Lean.Meta -namespace Lean.SubExpr +namespace Lean.Core + +open Lean.SubExpr section ViewRaw @@ -131,10 +133,10 @@ open Except in /-- Given a valid SubExpr, will return the raw current expression without performing any instantiation. If the SubExpr has a type subexpression coordinate then will error. -This is a cheaper version of `SubExpr.view` and can be used to quickly view the +This is a cheaper version of `Lean.Meta.viewSubexpr` and can be used to quickly view the subexpression at a position. Note that because the resulting expression will contain loose bound variables it can't be used in any `MetaM` methods. -/ -def viewRaw (p : Pos) (e : Expr) : Except String Expr := +def viewSubexpr (p : Pos) (e : Expr) : Except String Expr := aux e p.toArray.toList where aux (e : Expr) @@ -146,6 +148,6 @@ def viewRaw (p : Pos) (e : Expr) : Except String Expr := end ViewRaw -end Lean.SubExpr +end Lean.Core diff --git a/src/Lean/Meta/ExprTraverse.lean b/src/Lean/Meta/ExprTraverse.lean new file mode 100644 index 000000000000..4f1ee405ec21 --- /dev/null +++ b/src/Lean/Meta/ExprTraverse.lean @@ -0,0 +1,90 @@ +/- +Copyright (c) 2022 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: E.W.Ayers +-/ +import Lean.Meta.Basic +import Lean.SubExpr + +namespace Lean.Meta + +open Lean.SubExpr (Pos) +open Lean.SubExpr.Pos + +variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M] + + +variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M] + +private def usedLetOnly : M Bool := getBoolOption `visit.usedLetOnly false + +private def forgetPos (t : (Pos → Expr → M Expr) → (Pos → Expr → M Expr)) (visit : Expr → M Expr) (e : Expr) : M Expr := + t (fun _ => visit) Pos.root e + +/-- Given an expression `fun (x₁ : α₁) ... (xₙ : αₙ) => b`, will run +`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, +replacing each expression with the output of `f` and creating a new lambda. +(that is, correctly instantiating bound variables and repackaging them after) -/ +def traverseLambdaWithPos + (f : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr := visit #[] p e + where visit (fvars : Array Expr) (p : Pos) : Expr → M Expr + | (Expr.lam n d b c) => do + let d ← f p.pushBindingDomain <| d.instantiateRev fvars + withLocalDecl n c.binderInfo d fun x => + visit (fvars.push x) p.pushBindingBody b + | e => do + let body ← f p <| e.instantiateRev fvars + mkLambdaFVars (usedLetOnly := ← usedLetOnly) fvars body + +/-- Given an expression ` (x₁ : α₁) → ... → (xₙ : αₙ) → b`, will run +`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, +replacing the expression with the output of `f` and creating a new forall expression. +(that is, correctly instantiating bound variables and repackaging them after) -/ +def traverseForallWithPos + (f : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr := visit #[] p e + where visit fvars (p : Pos): Expr → M Expr + | (Expr.forallE n d b c) => do + let d ← f p.pushBindingDomain <| d.instantiateRev fvars + withLocalDecl n c.binderInfo d fun x => + visit (fvars.push x) p.pushBindingBody b + | e => do + let body ← f p <| e.instantiateRev fvars + mkForallFVars (usedLetOnly := ←usedLetOnly) fvars body + +/-- Similar to traverseLambda and traverseForall but with let binders. -/ +def traverseLetWithPos + (f : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr := visit #[] p e + where visit fvars (p : Pos) + | Expr.letE n t v b _ => do + let type ← f p.pushLetVarType <| t.instantiateRev fvars + let value ← f p.pushLetValue <| v.instantiateRev fvars + withLetDecl n type value fun x => + visit (fvars.push x) p.pushLetBody b + | e => do + let body ← f p <| e.instantiateRev fvars + mkLetFVars (usedLetOnly := ←usedLetOnly) fvars body + +/-- Maps `f` on each child of the given expression. + +Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...). +So `traverseChildren f e` where ``e = `(fn a₁ ... aₙ)`` will return +``(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))`` rather than ``(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))`` + +See also `Lean.Core.traverseChildren`. + -/ +def traverseChildrenWithPos (visit : Pos → Expr → M Expr) (p : Pos) (e: Expr) : M Expr := + match e with + | Expr.forallE .. => traverseForallWithPos visit p e + | Expr.lam .. => traverseLambdaWithPos visit p e + | Expr.letE .. => traverseLetWithPos visit p e + | Expr.app .. => Expr.traverseAppWithPos visit p e + | Expr.mdata _ b _ => e.updateMData! <$> traverseChildrenWithPos visit p b + | Expr.proj _ _ b _ => e.updateProj! <$> visit p.pushProj b + | _ => pure e + +def traverseLambda (visit : Expr → M Expr) := forgetPos traverseLambdaWithPos visit +def traverseForall (visit : Expr → M Expr) := forgetPos traverseForallWithPos visit +def traverseLet (visit : Expr → M Expr) := forgetPos traverseLetWithPos visit +def traverseChildren (visit : Expr → M Expr) := forgetPos traverseChildrenWithPos visit + +end Lean.Meta diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index edfe597bc970..7ea7a0c0e9c8 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, E.W.Ayers -/ import Lean.Meta.Basic +import Lean.Meta.ExprTraverse namespace Lean @@ -70,57 +71,6 @@ end Core namespace Meta -variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M] - -private def usedLetOnly : M Bool := getBoolOption `visit.usedLetOnly false - -/-- Given an expression `fun (x₁ : α₁) ... (xₙ : αₙ) => b`, will run -`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, -replacing each expression with the output of `f` and creating a new lambda. -(that is, correctly instantiating bound variables and repackaging them after) -/ -def traverseLambda - (f : Expr → M Expr) (e : Expr) : M Expr := visit #[] e - where visit (fvars : Array Expr) : Expr → M Expr - | (Expr.lam n d b c) => do withLocalDecl n c.binderInfo (← f (d.instantiateRev fvars)) fun x => visit (fvars.push x) b - | e => do mkLambdaFVars (usedLetOnly := ← usedLetOnly) fvars (← f (e.instantiateRev fvars)) - -/-- Given an expression ` (x₁ : α₁) → ... → (xₙ : αₙ) → b`, will run -`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, -replacing the expression with the output of `f` and creating a new forall expression. -(that is, correctly instantiating bound variables and repackaging them after) -/ -def traverseForall - (f : Expr → M Expr) (e : Expr) : M Expr := visit #[] e - where visit fvars : Expr → M Expr - | (Expr.forallE n d b c) => do withLocalDecl n c.binderInfo (← f (d.instantiateRev fvars)) fun x => visit (fvars.push x) b - | e => do mkForallFVars (usedLetOnly := ←usedLetOnly) fvars (← f (e.instantiateRev fvars)) - -/-- Similar to traverseLambda and traverseForall but with let binders. -/ -def traverseLet - (f : Expr → M Expr) (e : Expr) : M Expr := visit #[] e - where visit fvars - | Expr.letE n t v b _ => do - withLetDecl n (← f (t.instantiateRev fvars)) (← f (v.instantiateRev fvars)) fun x => - visit (fvars.push x) b - | e => do mkLetFVars (usedLetOnly := ←usedLetOnly) fvars (← f (e.instantiateRev fvars)) - -/-- Maps `f` on each child of the given expression. - -Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...). -So `traverseChildren f e` where ``e = `(fn a₁ ... aₙ)`` will return -``(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))`` rather than ``(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))`` - -See also `Lean.Core.traverseChildren`. - -/ -def traverseChildren (f : Expr → M Expr) (e: Expr) : M Expr := do - match e with - | Expr.forallE .. => traverseForall f e - | Expr.lam .. => traverseLambda f e - | Expr.letE .. => traverseLet f e - | Expr.app .. => Expr.traverseApp f e - | Expr.mdata _ b _ => return e.updateMData! (← f b) - | Expr.proj _ _ b _ => return e.updateProj! (← f b) - | _ => return e - /-- Similar to `Core.transform`, but terms provided to `pre` and `post` do not contain loose bound variables. So, it is safe to use any `MetaM` method at `pre` and `post`. -/ diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index 3e93c1f46204..02fd7d25d6c3 100644 --- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -79,14 +79,13 @@ def withLetBody (x : m α) : m α := do def withNaryFn (x : m α) : m α := do let e ← getExpr - let n := e.getAppNumArgs - let newPos := (← getPos).asNat * (Pos.maxChildren ^ n) + let newPos := (← getPos).pushNaryFn e.getAppNumArgs withTheReader SubExpr (fun cfg => { cfg with expr := e.getAppFn, pos := newPos }) x def withNaryArg (argIdx : Nat) (x : m α) : m α := do let e ← getExpr let args := e.getAppArgs - let newPos := (← getPos).asNat * (Pos.maxChildren ^ (args.size - argIdx)) + 1 + let newPos := (← getPos).pushNaryArg args.size argIdx withTheReader SubExpr (fun cfg => { cfg with expr := args[argIdx], pos := newPos }) x end Descend diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index 8176663d7f60..c358570c65af 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -85,6 +85,20 @@ def ofArray (ps : Array Nat) : Pos := def toArray (p : Pos) : Array Nat := foldl Array.push #[] p +def pushBindingDomain (p : Pos) := p.push 0 +def pushBindingBody (p : Pos) := p.push 1 +def pushLetVarType (p : Pos) := p.push 0 +def pushLetValue (p : Pos) := p.push 1 +def pushLetBody (p : Pos) := p.push 2 +def pushAppFn (p : Pos) := p.push 0 +def pushAppArg (p : Pos) := p.push 1 +def pushProj (p : Pos) := p.push 0 + +def pushNaryFn (numArgs : Nat) (p : Pos) : Pos := + p.asNat * (maxChildren ^ numArgs) +def pushNaryArg (numArgs argIdx : Nat) (p : Pos) : Pos := + show Nat from p.asNat * (maxChildren ^ (numArgs - argIdx)) + 1 + end SubExpr.Pos /-- An expression and the position of a subexpression within this expression. @@ -114,4 +128,15 @@ def mapPos (f : Pos → Pos) : SubExpr → SubExpr end SubExpr +open SubExpr in +/-- Same as `Expr.traverseApp` but also includes a +`SubExpr.Pos` argument for tracking subexpression position. -/ +def Expr.traverseAppWithPos {M} [Monad M] (visit : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr := + match e with + | Expr.app f a _ => + e.updateApp! + <$> traverseAppWithPos visit p.pushAppFn f + <*> visit p.pushAppArg a + | e => visit p e + end Lean From c9af6e65886e24f1c682607553cb5e5a744c7912 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 8 Jun 2022 18:20:23 -0400 Subject: [PATCH 07/16] fix: traverseChildrenWithPos bug --- src/Lean/Meta/ExprTraverse.lean | 5 +- src/Lean/Meta/Transform.lean | 82 +++++++++++++++++++-------------- 2 files changed, 49 insertions(+), 38 deletions(-) diff --git a/src/Lean/Meta/ExprTraverse.lean b/src/Lean/Meta/ExprTraverse.lean index 4f1ee405ec21..f801eec70e22 100644 --- a/src/Lean/Meta/ExprTraverse.lean +++ b/src/Lean/Meta/ExprTraverse.lean @@ -11,9 +11,6 @@ namespace Lean.Meta open Lean.SubExpr (Pos) open Lean.SubExpr.Pos -variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M] - - variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M] private def usedLetOnly : M Bool := getBoolOption `visit.usedLetOnly false @@ -78,7 +75,7 @@ def traverseChildrenWithPos (visit : Pos → Expr → M Expr) (p : Pos) (e: Expr | Expr.lam .. => traverseLambdaWithPos visit p e | Expr.letE .. => traverseLetWithPos visit p e | Expr.app .. => Expr.traverseAppWithPos visit p e - | Expr.mdata _ b _ => e.updateMData! <$> traverseChildrenWithPos visit p b + | Expr.mdata _ b _ => e.updateMData! <$> visit p b | Expr.proj _ _ b _ => e.updateProj! <$> visit p.pushProj b | _ => pure e diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index 7ea7a0c0e9c8..d5dc31eb7063 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -1,10 +1,9 @@ /- Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, E.W.Ayers +Authors: Leonardo de Moura -/ import Lean.Meta.Basic -import Lean.Meta.ExprTraverse namespace Lean @@ -14,25 +13,6 @@ inductive TransformStep where namespace Core -/-- Maps `visit` on each child of the given expression. - -Loose bound variables are not instantiated. -Use `Lean.Meta.traverseChildren` to avoid loose bound variables. - -Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...). -So `traverseChildren f e` where ``e = `(fn a₁ ... aₙ)`` will return -``(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))`` rather than ``(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))`` - -/ -def traverseChildren {M} [Monad M] (visit : Expr → M Expr) (e: Expr) : M Expr := - match e with - | Expr.forallE _ d b _ => e.updateForallE! <$> visit d <*> visit b - | Expr.lam _ d b _ => e.updateLambdaE! <$> visit d <*> visit b - | Expr.letE _ t v b _ => e.updateLet! <$> visit t <*> visit v <*> visit b - | Expr.app .. => e.traverseApp visit - | Expr.mdata _ b _ => e.updateMData! <$> visit b - | Expr.proj _ _ b _ => e.updateProj! <$> visit b - | _ => pure e - /-- Tranform the expression `input` using `pre` and `post`. - `pre s` is invoked before visiting the children of subterm 's'. If the result is `TransformStep.visit sNew`, then @@ -55,13 +35,20 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m] let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := CoreM) (liftM (m := ST IO.RealWorld) x) } let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := checkCache { val := e : ExprStructEq } fun _ => Core.withIncRecDepth do + let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do + match (← post e) with + | TransformStep.done e => pure e + | TransformStep.visit e => visit e match (← pre e) with | TransformStep.done e => pure e - | TransformStep.visit e => do - let e ← traverseChildren visit e - match (← post e) with - | TransformStep.done e => pure e - | TransformStep.visit e => visit e + | TransformStep.visit e => match e with + | Expr.forallE _ d b _ => visitPost (e.updateForallE! (← visit d) (← visit b)) + | Expr.lam _ d b _ => visitPost (e.updateLambdaE! (← visit d) (← visit b)) + | Expr.letE _ t v b _ => visitPost (e.updateLet! (← visit t) (← visit v) (← visit b)) + | Expr.app .. => e.withApp fun f args => do visitPost (mkAppN (← visit f) (← args.mapM visit)) + | Expr.mdata _ b _ => visitPost (e.updateMData! (← visit b)) + | Expr.proj _ _ b _ => visitPost (e.updateProj! (← visit b)) + | _ => visitPost e visit input |>.run def betaReduce (e : Expr) : CoreM Expr := @@ -74,7 +61,7 @@ namespace Meta /-- Similar to `Core.transform`, but terms provided to `pre` and `post` do not contain loose bound variables. So, it is safe to use any `MetaM` method at `pre` and `post`. -/ -partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadTrace m] [MonadRef m] [MonadOptions m] [MonadWithOptions m] [AddMessageContext m] +partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadTrace m] [MonadRef m] [MonadOptions m] [AddMessageContext m] (input : Expr) (pre : Expr → m TransformStep := fun e => return TransformStep.visit e) (post : Expr → m TransformStep := fun e => return TransformStep.done e) @@ -84,15 +71,42 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) } let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do - match (← pre e) with - | TransformStep.done e => pure e - | TransformStep.visit e => - let e ← traverseChildren visit e + let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do match (← post e) with - | TransformStep.done e => pure e + | TransformStep.done e => pure e | TransformStep.visit e => visit e - withOptions (fun o => o.setBool `visit.usedLetOnly usedLetOnly) - (visit input |>.run) + let rec visitLambda (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do + match e with + | Expr.lam n d b c => + withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x => + visitLambda (fvars.push x) b + | e => visitPost (← mkLambdaFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars))) + let rec visitForall (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do + match e with + | Expr.forallE n d b c => + withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x => + visitForall (fvars.push x) b + | e => visitPost (← mkForallFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars))) + let rec visitLet (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do + match e with + | Expr.letE n t v b _ => + withLetDecl n (← visit (t.instantiateRev fvars)) (← visit (v.instantiateRev fvars)) fun x => + visitLet (fvars.push x) b + | e => visitPost (← mkLetFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars))) + let visitApp (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := + e.withApp fun f args => do + visitPost (mkAppN (← visit f) (← args.mapM visit)) + match (← pre e) with + | TransformStep.done e => pure e + | TransformStep.visit e => match e with + | Expr.forallE .. => visitForall #[] e + | Expr.lam .. => visitLambda #[] e + | Expr.letE .. => visitLet #[] e + | Expr.app .. => visitApp e + | Expr.mdata _ b _ => visitPost (e.updateMData! (← visit b)) + | Expr.proj _ _ b _ => visitPost (e.updateProj! (← visit b)) + | _ => visitPost e + visit input |>.run def zetaReduce (e : Expr) : MetaM Expr := do let pre (e : Expr) : MetaM TransformStep := do From f674d04388eacaa8b6f0882453ead16a9830a219 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Thu, 9 Jun 2022 15:38:48 -0400 Subject: [PATCH 08/16] doc: docstrings for List.isPrefixOf --- src/Init/Data/Array/Basic.lean | 3 ++- src/Init/Data/List/Basic.lean | 6 ++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index bd14f8aa9ca5..31c19b58eaad 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -765,7 +765,8 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N true termination_by _ => as.size - i -/- Return true iff `as` is a prefix of `bs` -/ +/-- Return true iff `as` is a prefix of `bs`. +That is, `bs = as ++ t` for some `t : List α`.-/ def isPrefixOf [BEq α] (as bs : Array α) : Bool := if h : as.size ≤ bs.size then isPrefixOfAux as bs h 0 diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 1873759a3a56..e26da03ebefa 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -423,13 +423,15 @@ instance [LT α] : LE (List α) := ⟨List.le⟩ instance [LT α] [DecidableRel ((· < ·) : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) := fun _ _ => inferInstanceAs (Decidable (Not _)) -/-- `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/ +/-- `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. +That is, there exists a `t` such that `l₂ == l₁ ++ t`. -/ def isPrefixOf [BEq α] : List α → List α → Bool | [], _ => true | _, [] => false | a::as, b::bs => a == b && isPrefixOf as bs -/-- `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`. -/ +/-- `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`. +That is, there exists a `t` such that `l₂ == t ++ l₁`. -/ def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool := isPrefixOf l₁.reverse l₂.reverse From d75047478213bfd00016af4aabe80003c76da2b2 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Thu, 9 Jun 2022 16:07:06 -0400 Subject: [PATCH 09/16] test: add unit test for Expr lens --- src/Lean/Meta/ExprLens.lean | 20 ++++++++++++ tests/lean/run/ExprLens.lean | 63 ++++++++++++++++++++++++++++++++++++ 2 files changed, 83 insertions(+) create mode 100644 tests/lean/run/ExprLens.lean diff --git a/src/Lean/Meta/ExprLens.lean b/src/Lean/Meta/ExprLens.lean index b9e42a2f84e6..8ee30b78b575 100644 --- a/src/Lean/Meta/ExprLens.lean +++ b/src/Lean/Meta/ExprLens.lean @@ -146,6 +146,26 @@ def viewSubexpr (p : Pos) (e : Expr) : Except String Expr := | error m => error m | [] => ok e +private def viewBindersCoord : Nat → Expr → Option (Name × Expr) + | 1, (Expr.lam n y _ _) => some (n, y) + | 1, (Expr.forallE n y _ _) => some (n, y) + | 2, (Expr.letE n y _ _ _) => some (n, y) + | _, _ => none + +def viewBinders (p : Pos) (e : Expr) : Except String (Array (Name × Expr)) := do + let (acc, _) ← Pos.foldrM (fun c (acc, e) => do + let e₂ ← viewCoordRaw c e + let acc : Array (Name × Expr) := + match viewBindersCoord c e with + | none => acc + | some b => acc.push b + return (acc, e₂) + ) p (#[], e) + return acc + +def numBinders (p : Pos) (e : Expr) : Except String Nat := + Array.size <$> viewBinders p e + end ViewRaw end Lean.Core diff --git a/tests/lean/run/ExprLens.lean b/tests/lean/run/ExprLens.lean new file mode 100644 index 000000000000..9b7f33b1980b --- /dev/null +++ b/tests/lean/run/ExprLens.lean @@ -0,0 +1,63 @@ +import Lean.Meta.ExprLens +import Lean.Meta.ExprTraverse +import Lean + +open Lean Meta Elab Term SubExpr + +def Lean.LocalContext.subtract (Γ Δ : LocalContext) : Array Expr := + -- have Δ = Γ ++ E + let Δ := Δ.getFVars + let Γ := Γ.getFVars + let E := Δ[:(Δ.size - Γ.size)] + E.toArray + +def ExprTraversal := ∀{M : _} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M], (Pos → Expr → M Expr) → Pos → Expr → M Expr + +instance : Inhabited ExprTraversal where + default := traverseChildrenWithPos + +partial def traverseAll : ExprTraversal := fun + | visit, p, e => visit p e >>= traverseChildrenWithPos (fun p e => traverseAll visit p e) p + +def testTraversal + (traversalWithPos : ExprTraversal) + (expectedLen : Nat): TermElabM Unit := do + let s ← `( + ∀ x y : Nat, + ∃ (z : {z: Nat // z = x + y}), + let p := z.1 + p + x + y = 3 + ) + let e ← elabTerm s none + let Γ ← getLCtx + let (e', subexprs) ← StateT.run ( + traversalWithPos (fun p e => do + let a ← get + let Δ ← getLCtx + let s := Expr.abstract e <| Lean.LocalContext.subtract Γ Δ + set <| a.push (p, s) + return e + ) Pos.root e) #[] + if not (← liftM $ isDefEq e e') then + throwError "{e} and {e'} are different!" + if subexprs.size != expectedLen then + for (p, s) in subexprs do + let ppt ← PrettyPrinter.delab s >>= (liftM ∘ PrettyPrinter.ppTerm) + dbg_trace s!"{p}, {ppt}\n" + throwError "expected size: {expectedLen}\nactual size: {subexprs.size}" + for (p, s) in subexprs do + let e3 ← viewSubexpr (fun fvars t => do + let t := Expr.abstract t fvars + let de ← liftM $ isDefEq t s + if not de then + throwError "{t} and {s} are different!" + ) p e + + +#eval ((do + testTraversal traverseLambdaWithPos 1 + testTraversal traverseChildrenWithPos 3 + testTraversal traverseAll 100 + return ()) + : TermElabM Unit +) From 17d044f6370450759a299be0a66cb386d5bc95cc Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Thu, 9 Jun 2022 16:53:27 -0400 Subject: [PATCH 10/16] style: minor formatting changes --- src/Lean/Meta/ExprLens.lean | 55 +++++++++++++++++++-------------- src/Lean/Meta/ExprTraverse.lean | 2 +- src/Lean/SubExpr.lean | 5 +-- 3 files changed, 33 insertions(+), 29 deletions(-) diff --git a/src/Lean/Meta/ExprLens.lean b/src/Lean/Meta/ExprLens.lean index 8ee30b78b575..f3cab7c3b22a 100644 --- a/src/Lean/Meta/ExprLens.lean +++ b/src/Lean/Meta/ExprLens.lean @@ -1,19 +1,25 @@ +/- +Copyright (c) 2022 E.W.Ayers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: E.W.Ayers +-/ import Lean.Meta.Basic import Lean.SubExpr +/-! + +# Expression Lenses + +Functions for manipulating subexpressions using `SubExpr.Pos`. + +-/ + namespace Lean.Meta section ExprLens open Lean.SubExpr -/-! -## SubExpr as a Lens - -A `s : SubExpr` object can be considered as a [Lens](https://hackage.haskell.org/package/optics-core-0.4.1/docs/Optics-Lens.html). -However in order to perform meaningful lensing and viewing we need to adjust the local context when we lens under a binder in `s.expr`. --/ - variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M] /-- Given a constructor index for Expr, runs `g` on the value of that subexpression and replaces it. @@ -25,14 +31,14 @@ private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr | 0, e@(Expr.app f a _) => return e.updateApp! (← g f) a | 1, e@(Expr.app f a _) => return e.updateApp! f (← g a) | 0, e@(Expr.lam _ y b _) => return e.updateLambdaE! (← g y) b - | 1, e@(Expr.lam n y b c) => return e.updateLambdaE! y <|← withLocalDecl n c.binderInfo y fun x => do mkLambdaFVars #[x] (← g (b.instantiateRev #[x])) + | 1, e@(Expr.lam n y b c) => return e.updateLambdaE! y <|← withLocalDecl n c.binderInfo y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b - | 1, e@(Expr.forallE n y b c) => return e.updateForallE! y <|← withLocalDecl n c.binderInfo y fun x => do mkForallFVars #[x] (← g (b.instantiateRev #[x])) + | 1, e@(Expr.forallE n y b c) => return e.updateForallE! y <|← withLocalDecl n c.binderInfo y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.letE _ y a b _) => return e.updateLet! (← g y) a b | 1, e@(Expr.letE _ y a b _) => return e.updateLet! y (← g a) b - | 2, e@(Expr.letE n y a b _) => return e.updateLet! y a (← withLetDecl n y a fun x => do mkLetFVars #[x] (← g (b.instantiateRev #[x]))) - | 0, e@(Expr.proj _ _ b _) => pure e.updateProj! <*> g b - | n, e@(Expr.mdata _ a _) => pure e.updateMData! <*> lensCoord g n a + | 2, e@(Expr.letE n y a b _) => return e.updateLet! y a <|← withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x] + | 0, e@(Expr.proj _ _ b _) => e.updateProj! <$> g b + | n, e@(Expr.mdata _ a _) => e.updateMData! <$> lensCoord g n a | 3, _ => throwError "Lensing on types is not supported" | c, e => throwError "Invalid coordinate {c} for {e}" @@ -40,11 +46,11 @@ private def lensAux (g : Expr → M Expr) : List Nat → Expr → M Expr | [], e => g e | head::tail, e => lensCoord (lensAux g tail) head e -/-- Run the given `g` function to replace the expression at the subexpression position. If the subexpression is below a binder +/-- Run the given `replace` function to replace the expression at the subexpression position. If the subexpression is below a binder the bound variables will be appropriately instantiated with free variables and reabstracted after the replacement. If the subexpression is invalid or points to a type then this will throw. -/ -def lensSubexpr (g : (subexpr : Expr) → M Expr) (p : Pos) (e : Expr) : M Expr := - lensAux g p.toArray.toList e +def replaceSubexpr (replace : (subexpr : Expr) → M Expr) (p : Pos) (root : Expr) : M Expr := + lensAux replace p.toArray.toList root /-- Runs `k` on the given coordinate, including handling binders properly. The subexpression value passed to `k` is not instantiated with respect to the @@ -71,14 +77,14 @@ private def viewAux (k : Array Expr → Expr → M α) (fvars : Array Expr) : Li viewAux (fun otherFvars => k (fvars ++ otherFvars)) #[] tail y | head::tail, e => viewCoordAux (fun fvars => viewAux k fvars tail) fvars head e -/-- `view k p e` runs `k fvars s` where `s : Expr` is the subexpression of `e` at `p`. +/-- `view visit p e` runs `visit fvars s` where `s : Expr` is the subexpression of `e` at `p`. and `fvars` are the free variables for the binders that `s` is under. `s` is already instantiated with respect to these. -The role of the `k` function is analogous to the `k` function in `Lean.Meta.forallTelescope`. -/ +The role of the `visit` function is analogous to the `k` function in `Lean.Meta.forallTelescope`. -/ def viewSubexpr - (k : (fvars : Array Expr) → (subexpr : Expr) → M α) - : Pos → Expr → M α - | p, e => viewAux k #[] p.toArray.toList e + (visit : (fvars : Array Expr) → (subexpr : Expr) → M α) + (p : Pos) (root : Expr) : M α := + viewAux visit #[] p.toArray.toList root private def foldAncestorsAux (k : Array Expr → Expr → Nat → α → M α) @@ -136,8 +142,8 @@ If the SubExpr has a type subexpression coordinate then will error. This is a cheaper version of `Lean.Meta.viewSubexpr` and can be used to quickly view the subexpression at a position. Note that because the resulting expression will contain loose bound variables it can't be used in any `MetaM` methods. -/ -def viewSubexpr (p : Pos) (e : Expr) : Except String Expr := - aux e p.toArray.toList +def viewSubexpr (p : Pos) (root : Expr) : Except String Expr := + aux root p.toArray.toList where aux (e : Expr) | head :: tail => @@ -152,7 +158,8 @@ private def viewBindersCoord : Nat → Expr → Option (Name × Expr) | 2, (Expr.letE n y _ _ _) => some (n, y) | _, _ => none -def viewBinders (p : Pos) (e : Expr) : Except String (Array (Name × Expr)) := do +/-- `viewBinders p e` returns a list of all of the binders (name, type) above the given position `p` in the root expression `e` -/ +def viewBinders (p : Pos) (root : Expr) : Except String (Array (Name × Expr)) := do let (acc, _) ← Pos.foldrM (fun c (acc, e) => do let e₂ ← viewCoordRaw c e let acc : Array (Name × Expr) := @@ -160,7 +167,7 @@ def viewBinders (p : Pos) (e : Expr) : Except String (Array (Name × Expr)) := d | none => acc | some b => acc.push b return (acc, e₂) - ) p (#[], e) + ) p (#[], root) return acc def numBinders (p : Pos) (e : Expr) : Except String Nat := diff --git a/src/Lean/Meta/ExprTraverse.lean b/src/Lean/Meta/ExprTraverse.lean index f801eec70e22..d9ed2af1186e 100644 --- a/src/Lean/Meta/ExprTraverse.lean +++ b/src/Lean/Meta/ExprTraverse.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2022 Microsoft Corporation. All rights reserved. +Copyright (c) 2022 E.W.Ayers. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: E.W.Ayers -/ diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index c358570c65af..64b8ba6efd37 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -49,10 +49,6 @@ def push (p : Pos) (c : Nat) : Pos := if c >= maxChildren then panic! s!"invalid coordinate {c}" else p.asNat * maxChildren + c -/-- `pushNZeros p count` runs `.push 0` `count` times. -/ -def pushNZeros (p : Pos) (count : Nat) : Pos := - p.asNat * (maxChildren ^ count) - variable {α : Type} [Inhabited α] /-- Fold over the position starting at the root and heading to the leaf-/ @@ -96,6 +92,7 @@ def pushProj (p : Pos) := p.push 0 def pushNaryFn (numArgs : Nat) (p : Pos) : Pos := p.asNat * (maxChildren ^ numArgs) + def pushNaryArg (numArgs argIdx : Nat) (p : Pos) : Pos := show Nat from p.asNat * (maxChildren ^ (numArgs - argIdx)) + 1 From 68fe752b7455662c746275a1f130e5c94d18d795 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Thu, 9 Jun 2022 20:03:30 -0400 Subject: [PATCH 11/16] fix: add ExprTraversal to Meta --- src/Lean/Meta.lean | 1 + tests/lean/run/ExprLens.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean index e2cbdbf943ea..4d7509d010c7 100644 --- a/src/Lean/Meta.lean +++ b/src/Lean/Meta.lean @@ -41,3 +41,4 @@ import Lean.Meta.CongrTheorems import Lean.Meta.Eqns import Lean.Meta.CasesOn import Lean.Meta.ExprLens +import Lean.Meta.ExprTraverse diff --git a/tests/lean/run/ExprLens.lean b/tests/lean/run/ExprLens.lean index 9b7f33b1980b..b7ade10c2572 100644 --- a/tests/lean/run/ExprLens.lean +++ b/tests/lean/run/ExprLens.lean @@ -46,7 +46,7 @@ def testTraversal dbg_trace s!"{p}, {ppt}\n" throwError "expected size: {expectedLen}\nactual size: {subexprs.size}" for (p, s) in subexprs do - let e3 ← viewSubexpr (fun fvars t => do + let _ ← viewSubexpr (fun fvars t => do let t := Expr.abstract t fvars let de ← liftM $ isDefEq t s if not de then From 2a4659dafb0e97768dffb9e17c1fe41abb07a4c8 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 15 Jun 2022 17:29:34 -0400 Subject: [PATCH 12/16] test: replaceSubexpr pure p e = e This found a bug in lensCoord which I fixed. --- src/Lean/Meta/ExprLens.lean | 6 +++--- tests/lean/run/ExprLens.lean | 20 +++++++++++++++++++- 2 files changed, 22 insertions(+), 4 deletions(-) diff --git a/src/Lean/Meta/ExprLens.lean b/src/Lean/Meta/ExprLens.lean index f3cab7c3b22a..5982ddbc7aeb 100644 --- a/src/Lean/Meta/ExprLens.lean +++ b/src/Lean/Meta/ExprLens.lean @@ -31,12 +31,12 @@ private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr | 0, e@(Expr.app f a _) => return e.updateApp! (← g f) a | 1, e@(Expr.app f a _) => return e.updateApp! f (← g a) | 0, e@(Expr.lam _ y b _) => return e.updateLambdaE! (← g y) b - | 1, e@(Expr.lam n y b c) => return e.updateLambdaE! y <|← withLocalDecl n c.binderInfo y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x] + | 1, e@(Expr.lam n y b c) => withLocalDecl n c.binderInfo y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b - | 1, e@(Expr.forallE n y b c) => return e.updateForallE! y <|← withLocalDecl n c.binderInfo y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x] + | 1, e@(Expr.forallE n y b c) => withLocalDecl n c.binderInfo y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.letE _ y a b _) => return e.updateLet! (← g y) a b | 1, e@(Expr.letE _ y a b _) => return e.updateLet! y (← g a) b - | 2, e@(Expr.letE n y a b _) => return e.updateLet! y a <|← withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x] + | 2, e@(Expr.letE n y a b _) => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.proj _ _ b _) => e.updateProj! <$> g b | n, e@(Expr.mdata _ a _) => e.updateMData! <$> lensCoord g n a | 3, _ => throwError "Lensing on types is not supported" diff --git a/tests/lean/run/ExprLens.lean b/tests/lean/run/ExprLens.lean index b7ade10c2572..9c4ae43a7d7b 100644 --- a/tests/lean/run/ExprLens.lean +++ b/tests/lean/run/ExprLens.lean @@ -22,6 +22,7 @@ partial def traverseAll : ExprTraversal := fun def testTraversal (traversalWithPos : ExprTraversal) (expectedLen : Nat): TermElabM Unit := do + -- make a sample expression `e` that has all of the right stuff. let s ← `( ∀ x y : Nat, ∃ (z : {z: Nat // z = x + y}), @@ -30,6 +31,10 @@ def testTraversal ) let e ← elabTerm s none let Γ ← getLCtx + + -- traverse `e` using the `traversalWithPos` function + -- leave `e` unmodified but at each point accumulate + -- the abstracted subexpression let (e', subexprs) ← StateT.run ( traversalWithPos (fun p e => do let a ← get @@ -38,21 +43,34 @@ def testTraversal set <| a.push (p, s) return e ) Pos.root e) #[] + -- the traversal output should be equal to the original + -- that is: `traversal pure e ≡ e` if not (← liftM $ isDefEq e e') then throwError "{e} and {e'} are different!" + + -- check that the number of subexpressions is what we expect + -- and if it isn't then print them out for debugging. if subexprs.size != expectedLen then for (p, s) in subexprs do let ppt ← PrettyPrinter.delab s >>= (liftM ∘ PrettyPrinter.ppTerm) dbg_trace s!"{p}, {ppt}\n" throwError "expected size: {expectedLen}\nactual size: {subexprs.size}" + + -- for each subexpression `p`, make sure that viewSubexpr produces the same + -- subexpression as that found in the traversal. for (p, s) in subexprs do - let _ ← viewSubexpr (fun fvars t => do + viewSubexpr (fun fvars t => do let t := Expr.abstract t fvars let de ← liftM $ isDefEq t s if not de then throwError "{t} and {s} are different!" + return () ) p e + -- check that replaceSubexpr pure is the identity + let e' ← replaceSubexpr pure p e + if not (← liftM $ isDefEq e e') then + throwError "{e} and {e'} are different!" #eval ((do testTraversal traverseLambdaWithPos 1 From 4861a7781dbf56304e6efab78458e78447b7f62a Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 15 Jun 2022 18:39:32 -0400 Subject: [PATCH 13/16] test: numBinders --- src/Lean/Meta/ExprLens.lean | 67 +++++++++++++++------------------ src/Lean/Meta/ExprTraverse.lean | 55 ++++++++++++++++----------- src/Lean/SubExpr.lean | 7 +++- tests/lean/run/ExprLens.lean | 29 ++++++++------ 4 files changed, 87 insertions(+), 71 deletions(-) diff --git a/src/Lean/Meta/ExprLens.lean b/src/Lean/Meta/ExprLens.lean index 5982ddbc7aeb..04fcde4cc1fa 100644 --- a/src/Lean/Meta/ExprLens.lean +++ b/src/Lean/Meta/ExprLens.lean @@ -26,17 +26,17 @@ variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError If the subexpression is under a binder it will instantiate and abstract the binder body correctly. Mdata is ignored. An index of 3 is interpreted as the type of the expression. An index of 3 will throw since we can't replace types. -See also `Lean.Meta.transform`. -/ +See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`. -/ private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr | 0, e@(Expr.app f a _) => return e.updateApp! (← g f) a | 1, e@(Expr.app f a _) => return e.updateApp! f (← g a) | 0, e@(Expr.lam _ y b _) => return e.updateLambdaE! (← g y) b - | 1, e@(Expr.lam n y b c) => withLocalDecl n c.binderInfo y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x] + | 1, (Expr.lam n y b c) => withLocalDecl n c.binderInfo y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b - | 1, e@(Expr.forallE n y b c) => withLocalDecl n c.binderInfo y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x] + | 1, (Expr.forallE n y b c) => withLocalDecl n c.binderInfo y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.letE _ y a b _) => return e.updateLet! (← g y) a b | 1, e@(Expr.letE _ y a b _) => return e.updateLet! y (← g a) b - | 2, e@(Expr.letE n y a b _) => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x] + | 2, (Expr.letE n y a b _) => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.proj _ _ b _) => e.updateProj! <$> g b | n, e@(Expr.mdata _ a _) => e.updateMData! <$> lensCoord g n a | 3, _ => throwError "Lensing on types is not supported" @@ -118,39 +118,33 @@ open Lean.SubExpr section ViewRaw -open Except in +variable {M} [Monad M] [MonadError M] + /-- Get the raw subexpression without performing any instantiation. -/ -private def viewCoordRaw: Nat → Expr → Except String Expr - | 3, e => error s!"Can't viewRaw the type of {e}" - | 0, (Expr.app f _ _) => ok f - | 1, (Expr.app _ a _) => ok a - | 0, (Expr.lam _ y _ _) => ok y - | 1, (Expr.lam _ _ b _) => ok b - | 0, (Expr.forallE _ y _ _) => ok y - | 1, (Expr.forallE _ _ b _) => ok b - | 0, (Expr.letE _ y _ _ _) => ok y - | 1, (Expr.letE _ _ a _ _) => ok a - | 2, (Expr.letE _ _ _ b _) => ok b - | 0, (Expr.proj _ _ b _) => ok b - | n, (Expr.mdata _ a _) => viewCoordRaw n a - | c, e => error s!"Bad coordinate {c} for {e}" - -open Except in +private def viewCoordRaw: Expr → Nat → M Expr + | e , 3 => throwError "Can't viewRaw the type of {e}" + | (Expr.app f _ _) , 0 => pure f + | (Expr.app _ a _) , 1 => pure a + | (Expr.lam _ y _ _) , 0 => pure y + | (Expr.lam _ _ b _) , 1 => pure b + | (Expr.forallE _ y _ _), 0 => pure y + | (Expr.forallE _ _ b _), 1 => pure b + | (Expr.letE _ y _ _ _) , 0 => pure y + | (Expr.letE _ _ a _ _) , 1 => pure a + | (Expr.letE _ _ _ b _) , 2 => pure b + | (Expr.proj _ _ b _) , 0 => pure b + | (Expr.mdata _ a _) , n => viewCoordRaw a n + | e , c => throwError "Bad coordinate {c} for {e}" + + /-- Given a valid SubExpr, will return the raw current expression without performing any instantiation. If the SubExpr has a type subexpression coordinate then will error. This is a cheaper version of `Lean.Meta.viewSubexpr` and can be used to quickly view the subexpression at a position. Note that because the resulting expression will contain loose bound variables it can't be used in any `MetaM` methods. -/ -def viewSubexpr (p : Pos) (root : Expr) : Except String Expr := - aux root p.toArray.toList - where - aux (e : Expr) - | head :: tail => - match viewCoordRaw head e with - | ok e => aux e tail - | error m => error m - | [] => ok e +def viewSubexpr (p : Pos) (root : Expr) : M Expr := + p.foldlM viewCoordRaw root private def viewBindersCoord : Nat → Expr → Option (Name × Expr) | 1, (Expr.lam n y _ _) => some (n, y) @@ -159,18 +153,19 @@ private def viewBindersCoord : Nat → Expr → Option (Name × Expr) | _, _ => none /-- `viewBinders p e` returns a list of all of the binders (name, type) above the given position `p` in the root expression `e` -/ -def viewBinders (p : Pos) (root : Expr) : Except String (Array (Name × Expr)) := do - let (acc, _) ← Pos.foldrM (fun c (acc, e) => do - let e₂ ← viewCoordRaw c e - let acc : Array (Name × Expr) := +def viewBinders (p : Pos) (root : Expr) : M (Array (Name × Expr)) := do + let (acc, _) ← p.foldlM (fun (acc, e) c => do + let e₂ ← viewCoordRaw e c + let acc := match viewBindersCoord c e with | none => acc | some b => acc.push b return (acc, e₂) - ) p (#[], root) + ) (#[], root) return acc -def numBinders (p : Pos) (e : Expr) : Except String Nat := +/-- Returns the number of binders above a given subexpr position. -/ +def numBinders (p : Pos) (e : Expr) : M Nat := Array.size <$> viewBinders p e end ViewRaw diff --git a/src/Lean/Meta/ExprTraverse.lean b/src/Lean/Meta/ExprTraverse.lean index d9ed2af1186e..9e51f0c7b40b 100644 --- a/src/Lean/Meta/ExprTraverse.lean +++ b/src/Lean/Meta/ExprTraverse.lean @@ -11,17 +11,13 @@ namespace Lean.Meta open Lean.SubExpr (Pos) open Lean.SubExpr.Pos -variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M] - -private def usedLetOnly : M Bool := getBoolOption `visit.usedLetOnly false +variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] +/-- Convert a traversal function to a form without the `Pos` argument. -/ private def forgetPos (t : (Pos → Expr → M Expr) → (Pos → Expr → M Expr)) (visit : Expr → M Expr) (e : Expr) : M Expr := t (fun _ => visit) Pos.root e -/-- Given an expression `fun (x₁ : α₁) ... (xₙ : αₙ) => b`, will run -`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, -replacing each expression with the output of `f` and creating a new lambda. -(that is, correctly instantiating bound variables and repackaging them after) -/ +/-- 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 where visit (fvars : Array Expr) (p : Pos) : Expr → M Expr @@ -31,12 +27,9 @@ def traverseLambdaWithPos visit (fvars.push x) p.pushBindingBody b | e => do let body ← f p <| e.instantiateRev fvars - mkLambdaFVars (usedLetOnly := ← usedLetOnly) fvars body + mkLambdaFVars fvars body -/-- Given an expression ` (x₁ : α₁) → ... → (xₙ : αₙ) → b`, will run -`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, -replacing the expression with the output of `f` and creating a new forall expression. -(that is, correctly instantiating bound variables and repackaging them after) -/ +/-- Similar to `traverseForall` but with an additional pos argument to track position. -/ def traverseForallWithPos (f : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr := visit #[] p e where visit fvars (p : Pos): Expr → M Expr @@ -46,9 +39,9 @@ def traverseForallWithPos visit (fvars.push x) p.pushBindingBody b | e => do let body ← f p <| e.instantiateRev fvars - mkForallFVars (usedLetOnly := ←usedLetOnly) fvars body + mkForallFVars fvars body -/-- Similar to traverseLambda and traverseForall but with let binders. -/ +/-- Similar to `traverseLet` but with an additional pos argument to track position. -/ def traverseLetWithPos (f : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr := visit #[] p e where visit fvars (p : Pos) @@ -59,16 +52,12 @@ def traverseLetWithPos visit (fvars.push x) p.pushLetBody b | e => do let body ← f p <| e.instantiateRev fvars - mkLetFVars (usedLetOnly := ←usedLetOnly) fvars body + -- if usedLetOnly = true then let binders will be eliminated + -- if their var doesn't appear in the body. + mkLetFVars (usedLetOnly := false) fvars body -/-- Maps `f` on each child of the given expression. - -Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...). -So `traverseChildren f e` where ``e = `(fn a₁ ... aₙ)`` will return -``(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))`` rather than ``(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))`` - -See also `Lean.Core.traverseChildren`. - -/ +/-- Similar to `Lean.Meta.traverseChildren` except that `visit` also includes a `Pos` argument so you can +track the subexpression position. -/ def traverseChildrenWithPos (visit : Pos → Expr → M Expr) (p : Pos) (e: Expr) : M Expr := match e with | Expr.forallE .. => traverseForallWithPos visit p e @@ -79,9 +68,29 @@ def traverseChildrenWithPos (visit : Pos → Expr → M Expr) (p : Pos) (e: Expr | Expr.proj _ _ b _ => e.updateProj! <$> visit p.pushProj b | _ => pure e +/-- Given an expression `fun (x₁ : α₁) ... (xₙ : αₙ) => b`, will run +`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, +replacing each expression with the output of `f` and creating a new lambda. +(that is, correctly instantiating bound variables and repackaging them after) -/ def traverseLambda (visit : Expr → M Expr) := forgetPos traverseLambdaWithPos visit + +/-- Given an expression ` (x₁ : α₁) → ... → (xₙ : αₙ) → b`, will run +`f` on each of the variable types `αᵢ` and `b` with the correct MetaM context, +replacing the expression with the output of `f` and creating a new forall expression. +(that is, correctly instantiating bound variables and repackaging them after) -/ def traverseForall (visit : Expr → M Expr) := forgetPos traverseForallWithPos visit + +/-- Similar to `traverseLambda` and `traverseForall` but with let binders. -/ def traverseLet (visit : Expr → M Expr) := forgetPos traverseLetWithPos visit + +/-- Maps `visit` on each child of the given expression. + +Applications, foralls, lambdas and let binders are bundled (as they are bundled in `Expr.traverseApp`, `traverseForall`, ...). +So `traverseChildren f e` where ``e = `(fn a₁ ... aₙ)`` will return +``(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))`` rather than ``(← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))`` + +See also `Lean.Core.traverseChildren`. + -/ def traverseChildren (visit : Expr → M Expr) := forgetPos traverseChildrenWithPos visit end Lean.Meta diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index 64b8ba6efd37..237770b43f18 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -55,10 +55,15 @@ variable {α : Type} [Inhabited α] def foldl (f : α → Nat → α) : α → Pos → α := fix2 (fun r a p => if p.isRoot then a else f (r a p.tail) p.head) -/-- Fold over the position starting at the root and heading to the leaf-/ +/-- Fold over the position starting at the leaf and heading to the root-/ def foldr (f : Nat → α → α) : Pos → α → α := fix2 (fun r p a => if p.isRoot then a else r p.tail (f p.head a)) +/-- monad-fold over the position starting at the root and heading to the leaf-/ +def foldlM [Monad M] (f : α → Nat → M α) : α → Pos → M α := + fix2 (fun r a p => if p.isRoot then pure a else do f (← r a p.tail) p.head) + +/-- monad-fold over the position starting at the leaf and finishing at the root. -/ def foldrM [Monad M] (f : Nat → α → M α) : Pos → α → M α := fix2 (fun r p a => if p.isRoot then pure a else f p.head a >>= r p.tail) diff --git a/tests/lean/run/ExprLens.lean b/tests/lean/run/ExprLens.lean index 9c4ae43a7d7b..8008fbc27ef4 100644 --- a/tests/lean/run/ExprLens.lean +++ b/tests/lean/run/ExprLens.lean @@ -22,9 +22,10 @@ partial def traverseAll : ExprTraversal := fun def testTraversal (traversalWithPos : ExprTraversal) (expectedLen : Nat): TermElabM Unit := do - -- make a sample expression `e` that has all of the right stuff. + -- make a sample expression `e` that has all of the different kinds of expressions. let s ← `( ∀ x y : Nat, + ∀ {zz : Fin x}, ∃ (z : {z: Nat // z = x + y}), let p := z.1 p + x + y = 3 @@ -36,23 +37,29 @@ def testTraversal -- leave `e` unmodified but at each point accumulate -- the abstracted subexpression let (e', subexprs) ← StateT.run ( - traversalWithPos (fun p e => do + traversalWithPos (fun p s => do let a ← get let Δ ← getLCtx - let s := Expr.abstract e <| Lean.LocalContext.subtract Γ Δ - set <| a.push (p, s) - return e + let E := Lean.LocalContext.subtract Γ Δ + + -- check that numBinders works + let nBinders ← Lean.Core.numBinders p e + if E.size != nBinders then + throwError "bad number of binders" + + set <| a.push (p, Expr.abstract s E) + return s ) Pos.root e) #[] -- the traversal output should be equal to the original -- that is: `traversal pure e ≡ e` if not (← liftM $ isDefEq e e') then - throwError "{e} and {e'} are different!" + throwError "\n{e} \nand \n{e'} are different!" -- check that the number of subexpressions is what we expect -- and if it isn't then print them out for debugging. if subexprs.size != expectedLen then for (p, s) in subexprs do - let ppt ← PrettyPrinter.delab s >>= (liftM ∘ PrettyPrinter.ppTerm) + let ppt ← PrettyPrinter.ppExpr s dbg_trace s!"{p}, {ppt}\n" throwError "expected size: {expectedLen}\nactual size: {subexprs.size}" @@ -63,19 +70,19 @@ def testTraversal let t := Expr.abstract t fvars let de ← liftM $ isDefEq t s if not de then - throwError "{t} and {s} are different!" + throwError "\n{t} \nand \n{s} are different!" return () ) p e -- check that replaceSubexpr pure is the identity let e' ← replaceSubexpr pure p e if not (← liftM $ isDefEq e e') then - throwError "{e} and {e'} are different!" + throwError "\n{e} \nand \n{e'} are different!" #eval ((do testTraversal traverseLambdaWithPos 1 - testTraversal traverseChildrenWithPos 3 - testTraversal traverseAll 100 + testTraversal traverseChildrenWithPos 4 + testTraversal traverseAll 103 return ()) : TermElabM Unit ) From 5b2fac8bec62530831aea64d64724f140ff5b933 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Wed, 15 Jun 2022 18:50:24 -0400 Subject: [PATCH 14/16] chore: rm SubExpr.mapPos because it is not useful --- src/Lean/SubExpr.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index 237770b43f18..b5a22ebad760 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -125,9 +125,6 @@ def mkRoot (e : Expr) : SubExpr := ⟨e, Pos.root⟩ /-- Returns true if the selected subexpression is the topmost one.-/ def isRoot (s : SubExpr) : Bool := s.pos.isRoot -def mapPos (f : Pos → Pos) : SubExpr → SubExpr - | ⟨e,p⟩ => ⟨e, f p⟩ - end SubExpr open SubExpr in From eedc7303770e0b7b1ae395698473051e6ef595e9 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Thu, 16 Jun 2022 11:50:42 -0400 Subject: [PATCH 15/16] feat: string representation of Pos This is needed because JSON will otherwise lossily convert big nats to floats. --- src/Lean/SubExpr.lean | 40 +++++++++++++++++++++++++++++-------- tests/lean/run/subexpr.lean | 6 ++++++ 2 files changed, 38 insertions(+), 8 deletions(-) diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index b5a22ebad760..af7d3169dc5c 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -24,16 +24,11 @@ def typeCoord : Nat := maxChildren - 1 def asNat : Pos → Nat := id -instance : Inhabited Pos := show Inhabited Nat by infer_instance -instance : Ord Pos := show Ord Nat by infer_instance -instance : FromJson Pos := show FromJson Nat by infer_instance -instance : ToJson Pos := show ToJson Nat by infer_instance -instance : Repr Pos := show Repr Nat by infer_instance -instance : ToString Pos := show ToString Nat by infer_instance - /-- The Pos representing the root subexpression. -/ def root : Pos := (1 : Nat) +instance : Inhabited Pos := ⟨root⟩ + def isRoot (p : Pos) : Bool := p.asNat == 1 /-- The coordinate deepest in the Pos. -/ @@ -82,7 +77,8 @@ The first coordinate in the array corresponds to the root of the expression tree def ofArray (ps : Array Nat) : Pos := ps.foldl push root -/-- Decodes a subexpression `Pos` as a sequence of coordinates. See `Pos.fromArray` for details.-/ +/-- Decodes a subexpression `Pos` as a sequence of coordinates `cs : Array Nat`. See `Pos.fromArray` for details. +`cs[0]` is the coordinate for the root expression. -/ def toArray (p : Pos) : Array Nat := foldl Array.push #[] p @@ -101,6 +97,34 @@ def pushNaryFn (numArgs : Nat) (p : Pos) : Pos := def pushNaryArg (numArgs argIdx : Nat) (p : Pos) : Pos := show Nat from p.asNat * (maxChildren ^ (numArgs - argIdx)) + 1 +protected def toString (p : Pos) : String := + p.toArray.toList + |>.map toString + |> String.intercalate "/" + |> ("/" ++ ·) + +open Except in +private def ofStringCoord : String → Except String Nat + | "0" => ok 0 | "1" => ok 1 | "2" => ok 2 | "3" => ok 3 + | c => error s!"Invalid coordinate {c}" + +open Except in +protected def fromString? : String → Except String Pos + | "/" => Except.ok Pos.root + | s => + match String.splitOn s "/" with + | "" :: tail => Pos.ofArray <$> tail.toArray.mapM ofStringCoord + | ss => error s!"malformed {ss}" + +instance : Ord Pos := show Ord Nat by infer_instance +instance : DecidableEq Pos := show DecidableEq Nat by infer_instance +instance : ToString Pos := ⟨Pos.toString⟩ + +-- Note: we can't send the bare Nat over the wire because Json will convert to float +-- if the nat is too big and least significant bits will be lost. +instance : ToJson Pos := ⟨toJson ∘ Pos.toString⟩ +instance : FromJson Pos := ⟨fun j => fromJson? j >>= Pos.fromString?⟩ + end SubExpr.Pos /-- An expression and the position of a subexpression within this expression. diff --git a/tests/lean/run/subexpr.lean b/tests/lean/run/subexpr.lean index 4af899d20458..0f6de6d1cdf3 100644 --- a/tests/lean/run/subexpr.lean +++ b/tests/lean/run/subexpr.lean @@ -11,3 +11,9 @@ theorem Pos.append_roundtrip : (ps.bind fun p => ps.map fun q => (p,q)) (fun (x,y) => (x ++ y) == (Pos.toArray <| (Pos.append (Pos.ofArray x) (Pos.ofArray y)))) ) := by native_decide + +theorem Pos.stringRoundtrip : + true = ps.all (fun p => + let x := Pos.ofArray p + some x == (Except.toOption $ Pos.fromString? $ Pos.toString $ x) + ) := by native_decide From 7091db692692b7212d28019724923591b7f693a4 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Thu, 16 Jun 2022 18:26:41 -0400 Subject: [PATCH 16/16] fix: remove fix2 --- src/Lean/SubExpr.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index af7d3169dc5c..a246e84b03e9 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -47,20 +47,21 @@ def push (p : Pos) (c : Nat) : Pos := variable {α : Type} [Inhabited α] /-- Fold over the position starting at the root and heading to the leaf-/ -def foldl (f : α → Nat → α) : α → Pos → α := - fix2 (fun r a p => if p.isRoot then a else f (r a p.tail) p.head) +partial def foldl (f : α → Nat → α) (a : α) (p : Pos) : α := + if p.isRoot then a else f (foldl f a p.tail) p.head /-- Fold over the position starting at the leaf and heading to the root-/ -def foldr (f : Nat → α → α) : Pos → α → α := - fix2 (fun r p a => if p.isRoot then a else r p.tail (f p.head a)) +partial def foldr (f : Nat → α → α) (p : Pos) (a : α) : α := + if p.isRoot then a else foldr f p.tail (f p.head a) -/-- monad-fold over the position starting at the root and heading to the leaf-/ -def foldlM [Monad M] (f : α → Nat → M α) : α → Pos → M α := - fix2 (fun r a p => if p.isRoot then pure a else do f (← r a p.tail) p.head) +/-- monad-fold over the position starting at the root and heading to the leaf -/ +partial def foldlM [Monad M] (f : α → Nat → M α) (a : α) (p : Pos) : M α := + have : Inhabited (M α) := inferInstance + if p.isRoot then pure a else do foldlM f a p.tail >>= (f · p.head) /-- monad-fold over the position starting at the leaf and finishing at the root. -/ -def foldrM [Monad M] (f : Nat → α → M α) : Pos → α → M α := - fix2 (fun r p a => if p.isRoot then pure a else f p.head a >>= r p.tail) +partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (a : α) : M α := + if p.isRoot then pure a else f p.head a >>= foldrM f p.tail def depth (p : Pos) := p.foldr (fun _ => Nat.succ) 0