Documentation

Lean.SubExpr

source
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
Instances For
source
def Lean.SubExpr.Pos.maxChildren :
Nat
Equations
source
def Lean.SubExpr.Pos.typeCoord :
Nat

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

Equations
source
def Lean.SubExpr.Pos.asNat :
Pos → Nat
Equations
source
def Lean.SubExpr.Pos.root :
Pos

The Pos representing the root subexpression.

Equations
source
instance Lean.SubExpr.Pos.instInhabited :
Inhabited Pos
Equations
source
def Lean.SubExpr.Pos.isRoot (p : Pos) :
Bool
Equations
source
def Lean.SubExpr.Pos.head (p : Pos) :
Nat

The coordinate deepest in the Pos.

Equations
source
def Lean.SubExpr.Pos.tail (p : Pos) :
Pos
Equations
source
def Lean.SubExpr.Pos.push (p : Pos) (c : Nat) :
Pos
Equations
  • One or more equations did not get rendered due to their size.
source
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

source
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

source
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

source
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.

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

Returns true if pred is true for each coordinate in p.

Equations
source
def Lean.SubExpr.Pos.append :
Pos → Pos → Pos
Equations
source
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
source
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
source
def Lean.SubExpr.Pos.pushBindingDomain (p : Pos) :
Pos
Equations
  • p.pushBindingDomain = p.push 0
source
def Lean.SubExpr.Pos.pushBindingBody (p : Pos) :
Pos
Equations
  • p.pushBindingBody = p.push 1
source
def Lean.SubExpr.Pos.pushLetVarType (p : Pos) :
Pos
Equations
  • p.pushLetVarType = p.push 0
source
def Lean.SubExpr.Pos.pushLetValue (p : Pos) :
Pos
Equations
  • p.pushLetValue = p.push 1
source
def Lean.SubExpr.Pos.pushLetBody (p : Pos) :
Pos
Equations
  • p.pushLetBody = p.push 2
source
def Lean.SubExpr.Pos.pushAppFn (p : Pos) :
Pos
Equations
  • p.pushAppFn = p.push 0
source
def Lean.SubExpr.Pos.pushAppArg (p : Pos) :
Pos
Equations
  • p.pushAppArg = p.push 1
source
def Lean.SubExpr.Pos.pushProj (p : Pos) :
Pos
Equations
  • p.pushProj = p.push 0
source
def Lean.SubExpr.Pos.pushType (p : Pos) :
Pos
Equations
source
def Lean.SubExpr.Pos.pushNaryFn (numArgs : Nat) (p : Pos) :
Pos
Equations
source
def Lean.SubExpr.Pos.pushNaryArg (numArgs argIdx : Nat) (p : Pos) :
Pos
Equations
source
def Lean.SubExpr.Pos.pushNthBindingDomain (binderIdx : Nat) :
Pos → Pos
Equations
source
def Lean.SubExpr.Pos.pushNthBindingBody (numBinders : Nat) :
Pos → Pos
Equations
source
def Lean.SubExpr.Pos.toString (p : Pos) :
String
Equations
source
def Lean.SubExpr.Pos.fromString? :
String → Except String Pos
Equations
source
def Lean.SubExpr.Pos.fromString! (s : String) :
Pos
Equations
source
instance Lean.SubExpr.Pos.instOrd :
Ord Pos
Equations
source
instance Lean.SubExpr.Pos.instDecidableEq :
DecidableEq Pos
Equations
source
instance Lean.SubExpr.Pos.instToString :
ToString Pos
Equations
source
instance Lean.SubExpr.Pos.instEmptyCollection :
EmptyCollection Pos
Equations
source
instance Lean.SubExpr.Pos.instRepr :
Repr Pos
Equations
source
instance Lean.SubExpr.Pos.instToJson :
ToJson Pos
Equations
source
instance Lean.SubExpr.Pos.instFromJson :
FromJson Pos
Equations
source
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.

Instances For
source
instance Lean.instInhabitedSubExpr :
Inhabited SubExpr
Equations
source
def Lean.SubExpr.mkRoot (e : Expr) :
SubExpr
Equations
source
def Lean.SubExpr.isRoot (s : SubExpr) :
Bool

Returns true if the selected subexpression is the topmost one.

Equations
  • s.isRoot = s.pos.isRoot
source
@[reducible, inline]
abbrev Lean.SubExpr.PosMap (α : Type u) :
Type u

Map from subexpr positions to values.

Equations
source
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"
source
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"
source
instance Lean.SubExpr.instToJsonFVarId :
ToJson FVarId
Equations
source
instance Lean.SubExpr.instToJsonMVarId :
ToJson MVarId
Equations
source
instance Lean.SubExpr.instFromJsonFVarId :
FromJson FVarId
Equations
source
instance Lean.SubExpr.instFromJsonMVarId :
FromJson MVarId
Equations
source
inductive Lean.SubExpr.GoalLocation :
Type

A location within a goal.

Instances For
source
instance Lean.SubExpr.instFromJsonGoalLocation :
FromJson GoalLocation
Equations
source
instance Lean.SubExpr.instToJsonGoalLocation :
ToJson GoalLocation
Equations
source
structure Lean.SubExpr.GoalsLocation :
Type

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

Instances For
source
instance Lean.SubExpr.instFromJsonGoalsLocation :
FromJson GoalsLocation
Equations
source
instance Lean.SubExpr.instToJsonGoalsLocation :
ToJson GoalsLocation
Equations
source
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