def Lean.SubExpr.Pos : Type

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.

Equations

• Lean.SubExpr.Pos = Nat

def Lean.SubExpr.Pos.maxChildren : Nat

Equations

• Lean.SubExpr.Pos.maxChildren = 4

def Lean.SubExpr.Pos.typeCoord : Nat

The coordinate 3 = maxChildren - 1 is reserved to denote the type of the expression.

Equations

• Lean.SubExpr.Pos.typeCoord = Lean.SubExpr.Pos.maxChildren - 1

def Lean.SubExpr.Pos.asNat : Pos → Nat

Equations

• Lean.SubExpr.Pos.asNat = id

def Lean.SubExpr.Pos.root : Pos

The Pos representing the root subexpression.

Equations

• Lean.SubExpr.Pos.root = 1

instance Lean.SubExpr.Pos.instInhabited : Inhabited Pos

Equations

• Lean.SubExpr.Pos.instInhabited = { default := Lean.SubExpr.Pos.root }

def Lean.SubExpr.Pos.isRoot (p : Pos) : Bool

Equations

• p.isRoot = decide (p.asNat < Lean.SubExpr.Pos.maxChildren)

def Lean.SubExpr.Pos.head (p : Pos) : Nat

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

def Lean.SubExpr.Pos.tail (p : Pos) : Pos

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

def Lean.SubExpr.Pos.push (p : Pos) (c : Nat) : Pos

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.SubExpr.Pos.foldl {α : Type} (f : α → Nat → α) (init : α) (p : Pos) : α

Fold over the position starting at the root and heading to the leaf

partial def Lean.SubExpr.Pos.foldr {α : Type} (f : Nat → α → α) (p : Pos) (init : α) : α

Fold over the position starting at the leaf and heading to the root

partial def Lean.SubExpr.Pos.foldlM {α : Type} [Inhabited α] {M : Type → Type u_1} [Monad M] (f : α → Nat → M α) (init : α) (p : Pos) : M α

monad-fold over the position starting at the root and heading to the leaf

partial def Lean.SubExpr.Pos.foldrM {α : Type} {M : Type → Type u_1} [Monad M] (f : Nat → α → M α) (p : Pos) (init : α) : M α

monad-fold over the position starting at the leaf and finishing at the root.

def Lean.SubExpr.Pos.depth (p : Pos) : Nat

Equations

• p.depth = Lean.SubExpr.Pos.foldr (fun (x : Nat) => Nat.succ) p 0

def Lean.SubExpr.Pos.all (pred : Nat → Bool) (p : Pos) : Bool

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

def Lean.SubExpr.Pos.append : Pos → Pos → Pos

Equations

• Lean.SubExpr.Pos.append = Lean.SubExpr.Pos.foldl Lean.SubExpr.Pos.push

def Lean.SubExpr.Pos.ofArray (ps : Array Nat) : Pos

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.

Equations

• Lean.SubExpr.Pos.ofArray ps = Array.foldl Lean.SubExpr.Pos.push Lean.SubExpr.Pos.root ps

def Lean.SubExpr.Pos.toArray (p : Pos) : Array Nat

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

def Lean.SubExpr.Pos.pushBindingDomain (p : Pos) : Pos

Equations

• p.pushBindingDomain = p.push 0

def Lean.SubExpr.Pos.pushBindingBody (p : Pos) : Pos

Equations

• p.pushBindingBody = p.push 1

def Lean.SubExpr.Pos.pushLetVarType (p : Pos) : Pos

Equations

• p.pushLetVarType = p.push 0

def Lean.SubExpr.Pos.pushLetValue (p : Pos) : Pos

Equations

• p.pushLetValue = p.push 1

def Lean.SubExpr.Pos.pushLetBody (p : Pos) : Pos

Equations

• p.pushLetBody = p.push 2

def Lean.SubExpr.Pos.pushAppFn (p : Pos) : Pos

Equations

• p.pushAppFn = p.push 0

def Lean.SubExpr.Pos.pushAppArg (p : Pos) : Pos

Equations

• p.pushAppArg = p.push 1

def Lean.SubExpr.Pos.pushProj (p : Pos) : Pos

Equations

• p.pushProj = p.push 0

def Lean.SubExpr.Pos.pushType (p : Pos) : Pos

Equations

• p.pushType = p.push Lean.SubExpr.Pos.typeCoord

def Lean.SubExpr.Pos.pushNaryFn (numArgs : Nat) (p : Pos) : Pos

Equations

• Lean.SubExpr.Pos.pushNaryFn numArgs p = p.asNat * Lean.SubExpr.Pos.maxChildren ^ numArgs

def Lean.SubExpr.Pos.pushNaryArg (numArgs argIdx : Nat) (p : Pos) : Pos

Equations

• Lean.SubExpr.Pos.pushNaryArg numArgs argIdx p = p.asNat * Lean.SubExpr.Pos.maxChildren ^ (numArgs - argIdx) + 1

def Lean.SubExpr.Pos.pushNthBindingDomain (binderIdx : Nat) : Pos → Pos

Equations

• Lean.SubExpr.Pos.pushNthBindingDomain 0 x✝ = x✝.pushBindingDomain
• Lean.SubExpr.Pos.pushNthBindingDomain n.succ x✝ = Lean.SubExpr.Pos.pushNthBindingDomain n x✝.pushBindingBody

def Lean.SubExpr.Pos.pushNthBindingBody (numBinders : Nat) : Pos → Pos

Equations

• Lean.SubExpr.Pos.pushNthBindingBody 0 x✝ = x✝
• Lean.SubExpr.Pos.pushNthBindingBody n.succ x✝ = Lean.SubExpr.Pos.pushNthBindingBody n x✝.pushBindingBody

def Lean.SubExpr.Pos.toString (p : Pos) : String

Equations

• p.toString = (fun (x : String) => "/" ++ x) ("/".intercalate (List.map toString p.toArray.toList))

def Lean.SubExpr.Pos.fromString? : String → Except String Pos

Equations

• One or more equations did not get rendered due to their size.
• Lean.SubExpr.Pos.fromString? "/" = Except.ok Lean.SubExpr.Pos.root

def Lean.SubExpr.Pos.fromString! (s : String) : Pos

Equations

• Lean.SubExpr.Pos.fromString! s = match Lean.SubExpr.Pos.fromString? s with | Except.ok a => a | Except.error e => panicWithPosWithDecl "Lean.SubExpr" "Lean.SubExpr.Pos.fromString!" 140 16 e

instance Lean.SubExpr.Pos.instOrd : Ord Pos

Equations

• Lean.SubExpr.Pos.instOrd = inferInstance

instance Lean.SubExpr.Pos.instDecidableEq : DecidableEq Pos

Equations

• Lean.SubExpr.Pos.instDecidableEq = inferInstance

instance Lean.SubExpr.Pos.instToString : ToString Pos

Equations

• Lean.SubExpr.Pos.instToString = { toString := Lean.SubExpr.Pos.toString }

instance Lean.SubExpr.Pos.instEmptyCollection : EmptyCollection Pos

Equations

• Lean.SubExpr.Pos.instEmptyCollection = { emptyCollection := Lean.SubExpr.Pos.root }

instance Lean.SubExpr.Pos.instRepr : Repr Pos

Equations

• Lean.SubExpr.Pos.instRepr = { reprPrec := fun (p : Lean.SubExpr.Pos) (x : Nat) => Std.format "Pos.fromString! " ++ Std.format (repr p.toString) ++ Std.format "" }

instance Lean.SubExpr.Pos.instToJson : ToJson Pos

Equations

• Lean.SubExpr.Pos.instToJson = { toJson := Lean.toJson ∘ Lean.SubExpr.Pos.toString }

instance Lean.SubExpr.Pos.instFromJson : FromJson Pos

Equations

• Lean.SubExpr.Pos.instFromJson = { fromJson? := fun (j : Lean.Json) => Lean.fromJson? j >>= Lean.SubExpr.Pos.fromString? }

structure Lean.SubExpr : Type

A subexpression of some root expression. Both its value and its position within the root are stored.

• expr : Expr

  The subexpression.

• pos : Pos

  The position of the subexpression within the root expression.

instance Lean.instInhabitedSubExpr : Inhabited SubExpr

Equations

• Lean.instInhabitedSubExpr = { default := { expr := default, pos := default } }

def Lean.SubExpr.mkRoot (e : Expr) : SubExpr

Equations

• Lean.SubExpr.mkRoot e = { expr := e, pos := Lean.SubExpr.Pos.root }

def Lean.SubExpr.isRoot (s : SubExpr) : Bool

Returns true if the selected subexpression is the topmost one.

Equations

• s.isRoot = s.pos.isRoot

@[reducible, inline]

abbrev Lean.SubExpr.PosMap (α : Type u) : Type u

Map from subexpr positions to values.

Equations

• Lean.SubExpr.PosMap α = Lean.RBMap Lean.SubExpr.Pos α compare

def Lean.SubExpr.bindingBody! : SubExpr → SubExpr

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"

def Lean.SubExpr.bindingDomain! : SubExpr → SubExpr

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"

instance Lean.SubExpr.instToJsonFVarId : ToJson FVarId

Equations

• Lean.SubExpr.instToJsonFVarId = { toJson := fun (f : Lean.FVarId) => Lean.toJson f.name }

instance Lean.SubExpr.instToJsonMVarId : ToJson MVarId

Equations

• Lean.SubExpr.instToJsonMVarId = { toJson := fun (f : Lean.MVarId) => Lean.toJson f.name }

instance Lean.SubExpr.instFromJsonFVarId : FromJson FVarId

Equations

• Lean.SubExpr.instFromJsonFVarId = { fromJson? := fun (j : Lean.Json) => Lean.FVarId.mk <$> Lean.fromJson? j }

instance Lean.SubExpr.instFromJsonMVarId : FromJson MVarId

Equations

• Lean.SubExpr.instFromJsonMVarId = { fromJson? := fun (j : Lean.Json) => Lean.MVarId.mk <$> Lean.fromJson? j }

inductive Lean.SubExpr.GoalLocation : Type

A location within a goal.

• hyp : FVarId → GoalLocation

  One of the hypotheses.

• hypType : FVarId → Pos → GoalLocation

  A subexpression of the type of one of the hypotheses.

• hypValue : FVarId → Pos → GoalLocation

  A subexpression of the value of one of the let-bound hypotheses.

• target : Pos → GoalLocation

  A subexpression of the goal type.

instance Lean.SubExpr.instFromJsonGoalLocation : FromJson GoalLocation

Equations

• Lean.SubExpr.instFromJsonGoalLocation = { fromJson? := Lean.SubExpr.fromJsonGoalLocation✝ }

instance Lean.SubExpr.instToJsonGoalLocation : ToJson GoalLocation

Equations

• Lean.SubExpr.instToJsonGoalLocation = { toJson := Lean.SubExpr.toJsonGoalLocation✝ }

structure Lean.SubExpr.GoalsLocation : Type

A location within a goal state. It identifies a specific goal together with a GoalLocation within it.

• mvarId : MVarId

  Which goal the location is in.

• loc : GoalLocation

instance Lean.SubExpr.instFromJsonGoalsLocation : FromJson GoalsLocation

Equations

• Lean.SubExpr.instFromJsonGoalsLocation = { fromJson? := Lean.SubExpr.fromJsonGoalsLocation✝ }

instance Lean.SubExpr.instToJsonGoalsLocation : ToJson GoalsLocation

Equations

• Lean.SubExpr.instToJsonGoalsLocation = { toJson := Lean.SubExpr.toJsonGoalsLocation✝ }

def Lean.Expr.traverseAppWithPos {M : Type → Type u_1} [Monad M] (visit : SubExpr.Pos → Expr → M Expr) (p : SubExpr.Pos) (e : Expr) : M Expr

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