A position of a subexpression in an expression.
We use a simple encoding scheme for expression positions Pos:
every Expr constructor has at most 3 direct expression children. Considering an expression's type
to be one extra child as well, we can injectively map a path of childIdxs to a natural number
by computing the value of the 4-ary representation 1 :: childIdxs, since n-ary representations
without leading zeros are unique. Note that pos is initialized to 1 (case childIdxs == []).
See also SubExpr.
Instances For
The coordinate 3 = maxChildren - 1 is
reserved to denote the type of the expression.
Instances For
The Pos representing the root subexpression.
Instances For
The coordinate deepest in the Pos.
Equations
- p.head = if p.isRoot = true then panicWithPosWithDecl "Lean.SubExpr" "Lean.SubExpr.Pos.head" 44 19 "already at top" else p.asNat % Lean.SubExpr.Pos.maxChildren
Instances For
Equations
- p.tail = if p.isRoot = true then panicWithPosWithDecl "Lean.SubExpr" "Lean.SubExpr.Pos.tail" 48 19 "already at top" else (p.asNat - p.head) / Lean.SubExpr.Pos.maxChildren
Instances For
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
monad-fold over the position starting at the root and heading to the leaf
monad-fold over the position starting at the leaf and finishing at the root.
Returns true if pred is true for each coordinate in p.
Equations
- Lean.SubExpr.Pos.all pred p = Option.isSome (Lean.SubExpr.Pos.foldrM (fun (n : Nat) (a : Unit) => if pred n = true then pure a else failure) p ()).run
Instances For
Instances For
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.
Instances For
Decodes a subexpression Pos as a sequence of coordinates cs : Array Nat. See Pos.ofArray for details.
cs[0] is the coordinate for the root expression.
Equations
- p.toArray = Lean.SubExpr.Pos.foldl Array.push #[] p
Instances For
Equations
- p.pushBindingDomain = p.push 0
Instances For
Equations
- p.pushBindingBody = p.push 1
Instances For
Equations
- p.pushLetVarType = p.push 0
Instances For
Equations
- p.pushLetBody = p.push 2
Instances For
Equations
- p.pushType = p.push Lean.SubExpr.Pos.typeCoord
Instances For
Instances For
Equations
- Lean.SubExpr.Pos.pushNaryArg numArgs argIdx p = p.asNat * Lean.SubExpr.Pos.maxChildren ^ (numArgs - argIdx) + 1
Instances For
Equations
- Lean.SubExpr.Pos.pushNthBindingDomain 0 x = x.pushBindingDomain
- Lean.SubExpr.Pos.pushNthBindingDomain n.succ x = Lean.SubExpr.Pos.pushNthBindingDomain n x.pushBindingBody
Instances For
Equations
- Lean.SubExpr.Pos.pushNthBindingBody 0 x = x
- Lean.SubExpr.Pos.pushNthBindingBody n.succ x = Lean.SubExpr.Pos.pushNthBindingBody n x.pushBindingBody
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.SubExpr.Pos.fromString? "/" = Except.ok Lean.SubExpr.Pos.root
Instances For
Equations
- Lean.SubExpr.Pos.instOrd = inferInstance
Equations
- Lean.SubExpr.Pos.instToString = { toString := Lean.SubExpr.Pos.toString }
Equations
- Lean.SubExpr.Pos.instToJson = { toJson := Lean.toJson ∘ Lean.SubExpr.Pos.toString }
A subexpression of some root expression. Both its value and its position within the root are stored.
- expr : Lean.Expr
The subexpression.
- pos : Lean.SubExpr.Pos
The position of the subexpression within the root expression.
Instances For
Equations
- Lean.SubExpr.mkRoot e = { expr := e, pos := Lean.SubExpr.Pos.root }
Instances For
Returns true if the selected subexpression is the topmost one.
Instances For
Map from subexpr positions to values.
Instances For
Equations
- { expr := Lean.Expr.forallE binderName binderType b binderInfo, pos := p }.bindingBody! = { expr := b, pos := p.pushBindingBody }
- { expr := Lean.Expr.lam binderName binderType b binderInfo, pos := p }.bindingBody! = { expr := b, pos := p.pushBindingBody }
- x.bindingBody! = panicWithPosWithDecl "Lean.SubExpr" "Lean.SubExpr.bindingBody!" 179 9 "subexpr is not a binder"
Instances For
Equations
- { expr := Lean.Expr.forallE binderName binderType b binderInfo, pos := p }.bindingDomain! = { expr := binderType, pos := p.pushBindingDomain }
- { expr := Lean.Expr.lam binderName binderType b binderInfo, pos := p }.bindingDomain! = { expr := binderType, pos := p.pushBindingDomain }
- x.bindingDomain! = panicWithPosWithDecl "Lean.SubExpr" "Lean.SubExpr.bindingDomain!" 184 9 "subexpr is not a binder"
Instances For
Equations
- Lean.SubExpr.instToJsonFVarId = { toJson := fun (f : Lean.FVarId) => Lean.toJson f.name }
Equations
- Lean.SubExpr.instToJsonMVarId = { toJson := fun (f : Lean.MVarId) => Lean.toJson f.name }
Equations
- Lean.SubExpr.instFromJsonMVarId = { fromJson? := fun (j : Lean.Json) => Lean.MVarId.mk <$> Lean.fromJson? j }
A location within a goal.
- hyp: Lean.FVarId → Lean.SubExpr.GoalLocation
One of the hypotheses.
- hypType: Lean.FVarId → Lean.SubExpr.Pos → Lean.SubExpr.GoalLocation
A subexpression of the type of one of the hypotheses.
- hypValue: Lean.FVarId → Lean.SubExpr.Pos → Lean.SubExpr.GoalLocation
A subexpression of the value of one of the let-bound hypotheses.
- target: Lean.SubExpr.Pos → Lean.SubExpr.GoalLocation
A subexpression of the goal type.
Instances For
Equations
- Lean.SubExpr.instFromJsonGoalLocation = { fromJson? := Lean.SubExpr.fromJsonGoalLocation✝ }
A location within a goal state. It identifies a specific goal together with a GoalLocation
within it.
- mvarId : Lean.MVarId
Which goal the location is in.
Instances For
Equations
- Lean.SubExpr.instFromJsonGoalsLocation = { fromJson? := Lean.SubExpr.fromJsonGoalsLocation✝ }
Same as Expr.traverseApp but also includes a
SubExpr.Pos argument for tracking subexpression position.
Equations
- Lean.Expr.traverseAppWithPos visit p (f.app a) = (f.app a).updateApp! <$> Lean.Expr.traverseAppWithPos visit p.pushAppFn f <*> visit p.pushAppArg a
- Lean.Expr.traverseAppWithPos visit p e = visit p e