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 : Lean.SubExpr.Pos → Nat

Equations

• Lean.SubExpr.Pos.asNat = id

def Lean.SubExpr.Pos.root : Lean.SubExpr.Pos

The Pos representing the root subexpression.

Equations

• Lean.SubExpr.Pos.root = 1

instance Lean.SubExpr.Pos.instInhabited : Inhabited Lean.SubExpr.Pos

Equations

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

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

Equations

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

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

The coordinate deepest in the Pos.

Equations

• p.head = if p.isRoot = true then panicWithPosWithDecl "Lean.SubExpr" "Lean.SubExpr.Pos.head" 43 19 "already at top" else p.asNat % Lean.SubExpr.Pos.maxChildren

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

Equations

• p.tail = if p.isRoot = true then panicWithPosWithDecl "Lean.SubExpr" "Lean.SubExpr.Pos.tail" 47 19 "already at top" else (p.asNat - p.head) / Lean.SubExpr.Pos.maxChildren

def Lean.SubExpr.Pos.push (p : Lean.SubExpr.Pos) (c : Nat) : Lean.SubExpr.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 : Lean.SubExpr.Pos) : α

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

partial def Lean.SubExpr.Pos.foldr {α : Type} (f : Nat → α → α) (p : Lean.SubExpr.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 : Lean.SubExpr.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 : Lean.SubExpr.Pos) (init : α) : M α

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

def Lean.SubExpr.Pos.depth (p : Lean.SubExpr.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 : Lean.SubExpr.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 : Lean.SubExpr.Pos → Lean.SubExpr.Pos → Lean.SubExpr.Pos

Equations

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

def Lean.SubExpr.Pos.ofArray (ps : Array Nat) : Lean.SubExpr.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 : Lean.SubExpr.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 : Lean.SubExpr.Pos) : Lean.SubExpr.Pos

Equations

• p.pushBindingDomain = p.push 0

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

Equations

• p.pushBindingBody = p.push 1

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

Equations

• p.pushLetVarType = p.push 0

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

Equations

• p.pushLetValue = p.push 1

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

Equations

• p.pushLetBody = p.push 2

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

Equations

• p.pushAppFn = p.push 0

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

Equations

• p.pushAppArg = p.push 1

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

Equations

• p.pushProj = p.push 0

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.SubExpr.Pos.pushNthBindingDomain (binderIdx : Nat) : Lean.SubExpr.Pos → Lean.SubExpr.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) : Lean.SubExpr.Pos → Lean.SubExpr.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 : Lean.SubExpr.Pos) : String

Equations

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

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

Equations

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

def Lean.SubExpr.Pos.fromString! (s : String) : Lean.SubExpr.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!" 139 16 e

instance Lean.SubExpr.Pos.instOrd : Ord Lean.SubExpr.Pos

Equations

• Lean.SubExpr.Pos.instOrd = let_fun this := inferInstance; this

instance Lean.SubExpr.Pos.instDecidableEq : DecidableEq Lean.SubExpr.Pos

Equations

• Lean.SubExpr.Pos.instDecidableEq = let_fun this := inferInstance; this

instance Lean.SubExpr.Pos.instToString : ToString Lean.SubExpr.Pos

Equations

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

instance Lean.SubExpr.Pos.instEmptyCollection : EmptyCollection Lean.SubExpr.Pos

Equations

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

instance Lean.SubExpr.Pos.instRepr : Repr Lean.SubExpr.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 : Lean.ToJson Lean.SubExpr.Pos

Equations

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

instance Lean.SubExpr.Pos.instFromJson : Lean.FromJson Lean.SubExpr.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 : Lean.Expr

  The subexpression.

• pos : Lean.SubExpr.Pos

  The position of the subexpression within the root expression.

instance Lean.instInhabitedSubExpr : Inhabited Lean.SubExpr

Equations

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

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

Equations

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

def Lean.SubExpr.isRoot (s : Lean.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! : Lean.SubExpr → Lean.SubExpr

Equations

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

def Lean.SubExpr.bindingDomain! : Lean.SubExpr → Lean.SubExpr

Equations

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

instance Lean.SubExpr.instToJsonFVarId : Lean.ToJson Lean.FVarId

Equations

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

instance Lean.SubExpr.instToJsonMVarId : Lean.ToJson Lean.MVarId

Equations

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

instance Lean.SubExpr.instFromJsonFVarId : Lean.FromJson Lean.FVarId

Equations

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

instance Lean.SubExpr.instFromJsonMVarId : Lean.FromJson Lean.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: 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.

instance Lean.SubExpr.instFromJsonGoalLocation : Lean.FromJson Lean.SubExpr.GoalLocation

Equations

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

instance Lean.SubExpr.instToJsonGoalLocation : Lean.ToJson Lean.SubExpr.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 : Lean.MVarId

  Which goal the location is in.

• loc : Lean.SubExpr.GoalLocation

instance Lean.SubExpr.instFromJsonGoalsLocation : Lean.FromJson Lean.SubExpr.GoalsLocation

Equations

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

instance Lean.SubExpr.instToJsonGoalsLocation : Lean.ToJson Lean.SubExpr.GoalsLocation

Equations

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

def Lean.Expr.traverseAppWithPos {M : Type → Type u_1} [Monad M] (visit : Lean.SubExpr.Pos → Lean.Expr → M Lean.Expr) (p : Lean.SubExpr.Pos) (e : Lean.Expr) : M Lean.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) = Seq.seq ((f.app a).updateApp! <$> Lean.Expr.traverseAppWithPos visit p.pushAppFn f) fun (x : Unit) => visit p.pushAppArg a
• Lean.Expr.traverseAppWithPos visit p e = visit p e