Documentation

instance String.instInhabitedRange :

Inhabited String.Range

Equations

String.instInhabitedRange = { default := { start := default, stop := default } }

instance String.instReprRange :

Repr String.Range

Equations

String.instReprRange = { reprPrec := String.reprRange✝ }

instance String.instBEqRange :

BEq String.Range

Equations

String.instBEqRange = { beq := String.beqRange✝ }

instance String.instHashableRange :

Hashable String.Range

Equations

String.instHashableRange = { hash := String.hashRange✝ }

def String.Range.contains (r : String.Range) (pos : Pos) (includeStop : Bool := false) :

Equations

r.contains pos includeStop = (decide (r.start ≤ pos) && if includeStop = true then decide (pos ≤ r.stop) else decide (pos < r.stop))

def String.Range.includes (super sub : String.Range) :

Equations

super.includes sub = (decide (super.start ≤ sub.start) && decide (super.stop ≥ sub.stop))

def String.Range.overlaps (first second : String.Range) (includeFirstStop includeSecondStop : Bool := false) :

Equations

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

def String.Range.bsize (r : String.Range) :

Nat

Equations

r.bsize = r.stop.byteIdx - r.start.byteIdx

def Lean.SourceInfo.updateTrailing (trailing : Substring) :

SourceInfo → SourceInfo

Equations

Lean.SourceInfo.updateTrailing trailing (Lean.SourceInfo.original leading pos trailing_1 endPos) = Lean.SourceInfo.original leading pos trailing endPos
Lean.SourceInfo.updateTrailing trailing x✝ = x✝

def Lean.SourceInfo.getRange? (canonicalOnly : Bool := false) (info : SourceInfo) :

Equations

Lean.SourceInfo.getRange? canonicalOnly info = do let __do_lift ← info.getPos? canonicalOnly let __do_lift_1 ← info.getTailPos? canonicalOnly pure { start := __do_lift, stop := __do_lift_1 }

def Lean.SourceInfo.getRangeWithTrailing? (canonicalOnly : Bool := false) (info : SourceInfo) :

Equations

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

def Lean.SourceInfo.nonCanonicalSynthetic :

SourceInfo → SourceInfo

Converts an original or synthetic (canonical := true) SourceInfo to a synthetic (canonical := false) SourceInfo. This is sometimes useful when SourceInfo is being moved around between Syntaxes.

Equations

(Lean.SourceInfo.original leading pos trailing endPos).nonCanonicalSynthetic = Lean.SourceInfo.synthetic pos endPos
(Lean.SourceInfo.synthetic pos endPos canonical).nonCanonicalSynthetic = Lean.SourceInfo.synthetic pos endPos
Lean.SourceInfo.none.nonCanonicalSynthetic = Lean.SourceInfo.none

instance Lean.instBEqSourceInfo_lean :

BEq SourceInfo

Equations

Lean.instBEqSourceInfo_lean = { beq := Lean.beqSourceInfo✝ }

Syntax AST #

inductive Lean.IsNode :

Syntax → Prop

mk (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : IsNode (Syntax.node info kind args)

def Lean.SyntaxNode :

Equations

Lean.SyntaxNode = { s : Lean.Syntax // Lean.IsNode s }

def Lean.unreachIsNodeMissing {β : Sort u_1} :

IsNode Syntax.missing → β

Equations

def Lean.unreachIsNodeAtom {β : Sort u_1} {info : SourceInfo} {val : String} :

IsNode (Syntax.atom info val) → β

Equations

def Lean.unreachIsNodeIdent {β : Sort u_1} {info : SourceInfo} {rawVal : Substring} {val : Name} {preresolved : List Syntax.Preresolved} :

IsNode (Syntax.ident info rawVal val preresolved) → β

Equations

def Lean.isLitKind (k : SyntaxNodeKind) :

Equations

Lean.isLitKind k = (k == Lean.strLitKind || k == Lean.numLitKind || k == Lean.charLitKind || k == Lean.nameLitKind || k == Lean.scientificLitKind)

@[inline]

def Lean.SyntaxNode.getKind (n : SyntaxNode) :

SyntaxNodeKind

Equations

Lean.SyntaxNode.getKind ⟨Lean.Syntax.node info k args, property⟩ = k
Lean.SyntaxNode.getKind ⟨Lean.Syntax.missing, h⟩ = Lean.unreachIsNodeMissing h
Lean.SyntaxNode.getKind ⟨Lean.Syntax.atom info val, h⟩ = Lean.unreachIsNodeAtom h
Lean.SyntaxNode.getKind ⟨Lean.Syntax.ident info rawVal val preresolved, h⟩ = Lean.unreachIsNodeIdent h

@[inline]

def Lean.SyntaxNode.withArgs {β : Sort u_1} (n : SyntaxNode) (fn : Array Syntax → β) :

Equations

Lean.SyntaxNode.withArgs ⟨Lean.Syntax.node info k args, property⟩ fn = fn args
Lean.SyntaxNode.withArgs ⟨Lean.Syntax.missing, h⟩ fn = Lean.unreachIsNodeMissing h
Lean.SyntaxNode.withArgs ⟨Lean.Syntax.atom info val, h⟩ fn = Lean.unreachIsNodeAtom h
Lean.SyntaxNode.withArgs ⟨Lean.Syntax.ident info rawVal val preresolved, h⟩ fn = Lean.unreachIsNodeIdent h

@[inline]

def Lean.SyntaxNode.getNumArgs (n : SyntaxNode) :

Nat

Equations

n.getNumArgs = n.withArgs fun (args : Array Lean.Syntax) => args.size

@[inline]

def Lean.SyntaxNode.getArg (n : SyntaxNode) (i : Nat) :

Equations

n.getArg i = n.withArgs fun (args : Array Lean.Syntax) => args[i]!

@[inline]

def Lean.SyntaxNode.getArgs (n : SyntaxNode) :

Array Syntax

Equations

n.getArgs = n.withArgs fun (args : Array Lean.Syntax) => args

@[inline]

def Lean.SyntaxNode.modifyArgs (n : SyntaxNode) (fn : Array Syntax → Array Syntax) :

Equations

Lean.SyntaxNode.modifyArgs ⟨Lean.Syntax.node info k args, property⟩ fn = Lean.Syntax.node info k (fn args)
Lean.SyntaxNode.modifyArgs ⟨Lean.Syntax.missing, h⟩ fn = Lean.unreachIsNodeMissing h
Lean.SyntaxNode.modifyArgs ⟨Lean.Syntax.atom info val, h⟩ fn = Lean.unreachIsNodeAtom h
Lean.SyntaxNode.modifyArgs ⟨Lean.Syntax.ident info rawVal val preresolved, h⟩ fn = Lean.unreachIsNodeIdent h

partial def Lean.Syntax.structRangeEq :

Syntax → Syntax → Bool

Compares syntax structures and position ranges, but not whitespace. We generally assume that if syntax trees equal in this way generate the same elaboration output, including positions contained in e.g. diagnostics and the info tree. However, as we have a few request handlers such as goalsAt? that are sensitive to whitespace information in the info tree, we currently use eqWithInfo instead for reuse checks.

def Lean.Syntax.structRangeEqWithTraceReuse (opts : Options) (stx1 stx2 : Syntax) :

Like structRangeEq but prints trace on failure if trace.Elab.reuse is activated.

Equations

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

partial def Lean.Syntax.eqWithInfo :

Syntax → Syntax → Bool

Full comparison of syntax structures and source infos.

def Lean.Syntax.eqWithInfoAndTraceReuse (opts : Options) (stx1 stx2 : Syntax) :

Like eqWithInfo but prints trace on failure if trace.Elab.reuse is activated.

Equations

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

def Lean.Syntax.getAtomVal :

Syntax → String

Equations

(Lean.Syntax.atom info val).getAtomVal = val
x✝.getAtomVal = ""

def Lean.Syntax.setAtomVal :

Syntax → String → Syntax

Equations

(Lean.Syntax.atom info val).setAtomVal x✝ = Lean.Syntax.atom info x✝
x✝¹.setAtomVal x✝ = x✝¹

@[inline]

def Lean.Syntax.ifNode {β : Sort u_1} (stx : Syntax) (hyes : SyntaxNode → β) (hno : Unit → β) :

Equations

(Lean.Syntax.node i k args).ifNode hyes hno = hyes ⟨Lean.Syntax.node i k args, ⋯⟩
stx.ifNode hyes hno = hno ()

@[inline]

def Lean.Syntax.ifNodeKind {β : Sort u_1} (stx : Syntax) (kind : SyntaxNodeKind) (hyes : SyntaxNode → β) (hno : Unit → β) :

Equations

(Lean.Syntax.node i k args).ifNodeKind kind hyes hno = if (k == kind) = true then hyes ⟨Lean.Syntax.node i k args, ⋯⟩ else hno ()
stx.ifNodeKind kind hyes hno = hno ()

def Lean.Syntax.asNode :

Syntax → SyntaxNode

Equations

(Lean.Syntax.node i k args).asNode = ⟨Lean.Syntax.node i k args, ⋯⟩
x✝.asNode = ⟨Lean.mkNullNode, Lean.Syntax.asNode.proof_1⟩

def Lean.Syntax.getIdAt (stx : Syntax) (i : Nat) :

Name

Equations

stx.getIdAt i = (stx.getArg i).getId

partial def Lean.Syntax.hasIdent (id : Name) :

Syntax → Bool

Check for a Syntax.ident of the given name anywhere in the tree. This is usually a bad idea since it does not check for shadowing bindings, but in the delaborator we assume that bindings are never shadowed.

@[inline]

def Lean.Syntax.modifyArgs (stx : Syntax) (fn : Array Syntax → Array Syntax) :

Equations

(Lean.Syntax.node i k args).modifyArgs fn = Lean.Syntax.node i k (fn args)
stx.modifyArgs fn = stx

@[inline]

def Lean.Syntax.modifyArg (stx : Syntax) (i : Nat) (fn : Syntax → Syntax) :

Equations

(Lean.Syntax.node i_1 k args).modifyArg i fn = Lean.Syntax.node i_1 k (args.modify i fn)
stx.modifyArg i fn = stx

@[specialize #[]]

partial def Lean.Syntax.replaceM {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) :

Syntax → m Syntax

@[specialize #[]]

partial def Lean.Syntax.rewriteBottomUpM {m : Type → Type} [Monad m] (fn : Syntax → m Syntax) :

Syntax → m Syntax

@[inline]

def Lean.Syntax.rewriteBottomUp (fn : Syntax → Syntax) (stx : Syntax) :

Equations

Lean.Syntax.rewriteBottomUp fn stx = (Lean.Syntax.rewriteBottomUpM fn stx).run

def Lean.Syntax.updateLeading :

Syntax → Syntax

Set SourceInfo.leading according to the trailing stop of the preceding token. The result is a round-tripping syntax tree IF, in the input syntax tree,

all leading stops, atom contents, and trailing starts are correct
trailing stops are between the trailing start and the next leading stop.

Remark: after parsing, all SourceInfo.leading fields are empty. The Syntax argument is the output produced by the parser for source. This function "fixes" the source.leading field.

Additionally, we try to choose "nicer" splits between leading and trailing stops according to some heuristics so that e.g. comments are associated to the (intuitively) correct token.

Note that the SourceInfo.trailing fields must be correct. The implementation of this Function relies on this property.

Equations

stx.updateLeading = StateT.run' (Lean.Syntax.replaceM Lean.Syntax.updateLeadingAux✝ stx) 0

partial def Lean.Syntax.updateTrailing (trailing : Substring) :

Syntax → Syntax

def Lean.Syntax.identComponents (stx : Syntax) (nFields? : Option Nat := none) :

List Syntax

Split an ident into its dot-separated components while preserving source info. Macro scopes are first erased. For example, `foo.bla.boo._@._hyg.4 ↦ [`foo, `bla, `boo]. If nFields is set, we take that many fields from the end and keep the remaining components as one name. For example, `foo.bla.boo with (nFields := 1) ↦ [`foo.bla, `boo].

Equations

One or more equations did not get rendered due to their size.
stx.identComponents nFields? = panicWithPosWithDecl "Lean.Syntax" "Lean.Syntax.identComponents" 316 9 "unreachable code has been reached"

def Lean.Syntax.identComponents.nameComps (n : Name) (nFields? : Option Nat) :

List Name

Equations

One or more equations did not get rendered due to their size.
Lean.Syntax.identComponents.nameComps n nFields? = n.components

structure Lean.Syntax.TopDown :

firstChoiceOnly : Bool
stx : Syntax

Instances For

Lean.Syntax.instForInTopDown

def Lean.Syntax.topDown (stx : Syntax) (firstChoiceOnly : Bool := false) :

TopDown

for _ in stx.topDown iterates through each node and leaf in stx top-down, left-to-right. If firstChoiceOnly is true, only visit the first argument of each choice node.

Equations

stx.topDown firstChoiceOnly = { firstChoiceOnly := firstChoiceOnly, stx := stx }

instance Lean.Syntax.instForInTopDown {m : Type u_1 → Type u_2} :

ForIn m TopDown Syntax

Equations

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

@[specialize #[]]

partial def Lean.Syntax.instForInTopDown.loop {m : Type u_1 → Type u_2} {β✝ : Type u_1} [Monad m] (f : Syntax → β✝ → m (ForInStep β✝)) (firstChoiceOnly : Bool) (stx : Syntax) (b : β✝) [Inhabited β✝] :

m (ForInStep β✝)

partial def Lean.Syntax.reprint (stx : Syntax) :

Option String

def Lean.Syntax.reprint.reprintLeaf (info : SourceInfo) (val : String) :

String

Equations

One or more equations did not get rendered due to their size.
Lean.Syntax.reprint.reprintLeaf info val = toString " " ++ toString val ++ toString " "

def Lean.Syntax.hasMissing (stx : Syntax) :

Equations

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

def Lean.Syntax.getRange? (stx : Syntax) (canonicalOnly : Bool := false) :

Equations

stx.getRange? canonicalOnly = match stx.getPos? canonicalOnly, stx.getTailPos? canonicalOnly with | some start, some stop => some { start := start, stop := stop } | x, x_1 => none

def Lean.Syntax.getRangeWithTrailing? (stx : Syntax) (canonicalOnly : Bool := false) :

Equations

stx.getRangeWithTrailing? canonicalOnly = do let __do_lift ← stx.getPos? canonicalOnly let __do_lift_1 ← stx.getTrailingTailPos? canonicalOnly pure { start := __do_lift, stop := __do_lift_1 }

def Lean.Syntax.ofRange (range : String.Range) (canonical : Bool := true) :

Returns a synthetic Syntax which has the specified String.Range.

Equations

Lean.Syntax.ofRange range canonical = Lean.Syntax.atom (Lean.SourceInfo.synthetic range.start range.stop canonical) ""

structure Lean.Syntax.Traverser :

Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right. Indices are allowed to be out-of-bound, in which case cur is Syntax.missing. If the Traverser is used linearly, updates are linear in the Syntax object as well.

cur : Syntax
parents : Array Syntax
idxs : Array Nat

def Lean.Syntax.Traverser.fromSyntax (stx : Syntax) :

Equations

Lean.Syntax.Traverser.fromSyntax stx = { cur := stx, parents := #[], idxs := #[] }

def Lean.Syntax.Traverser.setCur (t : Traverser) (stx : Syntax) :

Equations

t.setCur stx = { cur := stx, parents := t.parents, idxs := t.idxs }

def Lean.Syntax.Traverser.down (t : Traverser) (idx : Nat) :

Advance to the idx-th child of the current node.

Equations

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

def Lean.Syntax.Traverser.up (t : Traverser) :

Advance to the parent of the current node, if any.

Equations

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

def Lean.Syntax.Traverser.left (t : Traverser) :

Advance to the left sibling of the current node, if any.

Equations

t.left = if t.parents.size > 0 then t.up.down (t.idxs.back! - 1) else t

def Lean.Syntax.Traverser.right (t : Traverser) :

Advance to the right sibling of the current node, if any.

Equations

t.right = if t.parents.size > 0 then t.up.down (t.idxs.back! + 1) else t

class Lean.Syntax.MonadTraverser (m : Type → Type) :

Type 1

Monad class that gives read/write access to a Traverser.

st : MonadState Traverser m

Instances

def Lean.Syntax.MonadTraverser.getCur {m : Type → Type} [Monad m] [t : MonadTraverser m] :

m Syntax

Equations

Lean.Syntax.MonadTraverser.getCur = Lean.Syntax.Traverser.cur <$> get

def Lean.Syntax.MonadTraverser.setCur {m : Type → Type} [t : MonadTraverser m] (stx : Syntax) :

m Unit

Equations

Lean.Syntax.MonadTraverser.setCur stx = modify fun (t : Lean.Syntax.Traverser) => t.setCur stx

def Lean.Syntax.MonadTraverser.goDown {m : Type → Type} [t : MonadTraverser m] (idx : Nat) :

m Unit

Equations

Lean.Syntax.MonadTraverser.goDown idx = modify fun (t : Lean.Syntax.Traverser) => t.down idx

def Lean.Syntax.MonadTraverser.goUp {m : Type → Type} [t : MonadTraverser m] :

m Unit

Equations

Lean.Syntax.MonadTraverser.goUp = modify fun (t : Lean.Syntax.Traverser) => t.up

def Lean.Syntax.MonadTraverser.goLeft {m : Type → Type} [t : MonadTraverser m] :

m Unit

Equations

Lean.Syntax.MonadTraverser.goLeft = modify fun (t : Lean.Syntax.Traverser) => t.left

def Lean.Syntax.MonadTraverser.goRight {m : Type → Type} [t : MonadTraverser m] :

m Unit

Equations

Lean.Syntax.MonadTraverser.goRight = modify fun (t : Lean.Syntax.Traverser) => t.right

def Lean.Syntax.MonadTraverser.getIdx {m : Type → Type} [Monad m] [t : MonadTraverser m] :

m Nat

Equations

Lean.Syntax.MonadTraverser.getIdx = do let st ← get pure (st.idxs.back?.getD 0)

@[inline]

def Lean.SyntaxNode.getIdAt (n : SyntaxNode) (i : Nat) :

Name

Equations

n.getIdAt i = (n.getArg i).getId

def Lean.mkListNode (args : Array Syntax) :

Equations

Lean.mkListNode args = Lean.mkNullNode args

def Lean.Syntax.isQuot :

Syntax → Bool

def Lean.Syntax.getQuotContent (stx : Syntax) :

Equations

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

def Lean.Syntax.isAntiquot :

Syntax → Bool

Equations

(Lean.Syntax.node info (pre.str "antiquot") args).isAntiquot = true
x✝.isAntiquot = false

def Lean.Syntax.isAntiquots (stx : Syntax) :

Equations

stx.isAntiquots = (stx.isAntiquot || stx.isOfKind Lean.choiceKind && decide (stx.getNumArgs > 0) && stx.getArgs.all Lean.Syntax.isAntiquot)

def Lean.Syntax.getCanonicalAntiquot (stx : Syntax) :

Equations

stx.getCanonicalAntiquot = if stx.isOfKind Lean.choiceKind = true then stx[0] else stx

def Lean.Syntax.mkAntiquotNode (kind : Name) (term : Syntax) (nesting : Nat := 0) (name : Option String := none) (isPseudoKind : Bool := false) :

Equations

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

def Lean.Syntax.isEscapedAntiquot (stx : Syntax) :

Equations

stx.isEscapedAntiquot = !stx[1].getArgs.isEmpty

def Lean.Syntax.unescapeAntiquot (stx : Syntax) :

Equations

stx.unescapeAntiquot = if stx.isAntiquot = true then stx.setArg 1 (Lean.mkNullNode stx[1].getArgs.pop) else stx

def Lean.Syntax.getAntiquotTerm (stx : Syntax) :

Equations

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

def Lean.Syntax.antiquotKind? :

Syntax → Option (SyntaxNodeKind × Bool)

Return kind of parser expected at this antiquotation, and whether it is a "pseudo" kind (see mkAntiquot).

Equations

(Lean.Syntax.node info ((k.str "pseudo").str "antiquot") args).antiquotKind? = some (k, true )
(Lean.Syntax.node info (k.str "antiquot") args).antiquotKind? = some (k, false )
x✝.antiquotKind? = none

def Lean.Syntax.antiquotKinds (stx : Syntax) :

List (SyntaxNodeKind × Bool)

Equations

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

def Lean.Syntax.antiquotSpliceKind? :

Syntax → Option SyntaxNodeKind

Equations

(Lean.Syntax.node info (k.str "antiquot_scope") args).antiquotSpliceKind? = some k
x✝.antiquotSpliceKind? = none

def Lean.Syntax.isAntiquotSplice (stx : Syntax) :

Equations

stx.isAntiquotSplice = stx.antiquotSpliceKind?.isSome

def Lean.Syntax.getAntiquotSpliceContents (stx : Syntax) :

Array Syntax

Equations

stx.getAntiquotSpliceContents = stx[3].getArgs

def Lean.Syntax.getAntiquotSpliceSuffix (stx : Syntax) :

Equations

stx.getAntiquotSpliceSuffix = if stx.isAntiquotSplice = true then stx[5] else stx[1]

def Lean.Syntax.mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suffix : String) (nesting : Nat := 0) :

Equations

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

def Lean.Syntax.antiquotSuffixSplice? :

Syntax → Option SyntaxNodeKind

Equations

(Lean.Syntax.node info (k.str "antiquot_suffix_splice") args).antiquotSuffixSplice? = some k
x✝.antiquotSuffixSplice? = none

def Lean.Syntax.isAntiquotSuffixSplice (stx : Syntax) :

Equations

stx.isAntiquotSuffixSplice = stx.antiquotSuffixSplice?.isSome

def Lean.Syntax.getAntiquotSuffixSpliceInner (stx : Syntax) :

Equations

stx.getAntiquotSuffixSpliceInner = stx[0]

def Lean.Syntax.mkAntiquotSuffixSpliceNode (kind : SyntaxNodeKind) (inner : Syntax) (suffix : String) :

Equations

Lean.Syntax.mkAntiquotSuffixSpliceNode kind inner suffix = (Lean.mkNode (kind ++ `antiquot_suffix_splice) #[inner, Lean.mkAtom suffix]).raw

def Lean.Syntax.isTokenAntiquot (stx : Syntax) :

Equations

stx.isTokenAntiquot = stx.isOfKind `token_antiquot

def Lean.Syntax.isAnyAntiquot (stx : Syntax) :

Equations

stx.isAnyAntiquot = (stx.isAntiquot || stx.isAntiquotSplice || stx.isAntiquotSuffixSplice || stx.isTokenAntiquot)

@[reducible, inline]

abbrev Lean.Syntax.Stack :

List of Syntax nodes in which each succeeding element is the parent of the current. The associated index is the index of the preceding element in the list of children of the current element.

Equations

Lean.Syntax.Stack = List (Lean.Syntax × Nat)

def Lean.Syntax.findStack? (root : Syntax) (visit : Syntax → Bool) (accept : Syntax → Bool := fun (stx : Syntax) => !stx.hasArgs) :

Option Syntax.Stack

Return stack of syntax nodes satisfying visit, starting with such a node that also fulfills accept (default "is leaf"), and ending with the root.

Equations

root.findStack? visit accept = if visit root = true then Lean.Syntax.findStack?.go visit accept [] root else none

partial def Lean.Syntax.findStack?.go (visit : Syntax → Bool) (accept : Syntax → Bool := fun (stx : Syntax) => !stx.hasArgs) (stack : Syntax.Stack) (stx : Syntax) :

Option Syntax.Stack

def Lean.Syntax.Stack.matches (stack : Syntax.Stack) (pattern : List (Option SyntaxNodeKind)) :