Documentation

Lean.SubExpr

def Lean.SubExpr.Pos :

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

Instances For

def Lean.SubExpr.Pos.maxChildren :

Equations

Lean.SubExpr.Pos.maxChildren = 4

def Lean.SubExpr.Pos.typeCoord :

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 :

Equations

Lean.SubExpr.Pos.asNat = id

def Lean.SubExpr.Pos.root :

The Pos representing the root subexpression.

Equations

Lean.SubExpr.Pos.root = 1

instance Lean.SubExpr.Pos.instInhabited :

Equations

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

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

Equations

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

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

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) :

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) :

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) :

Equations

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

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

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) :

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) :

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) :

Equations

p.pushBindingDomain = p.push 0

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

Equations

p.pushBindingBody = p.push 1

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

Equations

p.pushLetVarType = p.push 0

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

Equations

p.pushLetValue = p.push 1

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

Equations

p.pushLetBody = p.push 2

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

Equations

p.pushAppFn = p.push 0

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

Equations

p.pushAppArg = p.push 1

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

Equations

p.pushProj = p.push 0

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

Equations

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

def Lean.SubExpr.Pos.pushNaryFn (numArgs : Nat) (p : 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) :

Equations

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

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

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) :

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) :

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) :

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 :

Equations

Lean.SubExpr.Pos.instOrd = inferInstance

instance Lean.SubExpr.Pos.instDecidableEq :

DecidableEq Pos

Equations

Lean.SubExpr.Pos.instDecidableEq = inferInstance

instance Lean.SubExpr.Pos.instToString :

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 :

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 :

Equations

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

instance Lean.SubExpr.Pos.instFromJson :

Equations

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

structure Lean.SubExpr :

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.

Instances For

instance Lean.instInhabitedSubExpr :

Inhabited SubExpr

Equations

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

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

Equations

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

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

Returns true if the selected subexpression is the topmost one.

Equations

s.isRoot = s.pos.isRoot

@[reducible, inline]

abbrev Lean.SubExpr.PosMap (α : 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 :

Equations

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

instance Lean.SubExpr.instToJsonMVarId :

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 :

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.

Instances For

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 :

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

Instances For

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) :

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