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 : String.Pos) (includeStop : optParam Bool false) :

Equations

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

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

Equations

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

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

Lean.SourceInfo → Lean.SourceInfo

Equations

Lean.SourceInfo.updateTrailing trailing x = match x with | Lean.SourceInfo.original leading pos trailing_1 endPos => Lean.SourceInfo.original leading pos trailing endPos | info => info

Syntax AST #

inductive Lean.IsNode :

Lean.Syntax → Prop

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

def Lean.SyntaxNode :

Equations

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

def Lean.unreachIsNodeMissing {β : Sort u_1} :

Lean.IsNode Lean.Syntax.missing → β

Equations

Lean.unreachIsNodeMissing a = nomatch a

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

Lean.IsNode (Lean.Syntax.atom info val) → β

Equations

Lean.unreachIsNodeAtom a = nomatch a

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

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

Equations

Lean.unreachIsNodeIdent a = nomatch a

def Lean.isLitKind (k : Lean.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 : Lean.SyntaxNode) :

Lean.SyntaxNodeKind

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Nat

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Array Lean.Syntax

Equations

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

@[inline]

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

Equations

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

def Lean.Syntax.getAtomVal :

Lean.Syntax → String

Equations

Lean.Syntax.getAtomVal x = match x with | Lean.Syntax.atom info val => val | x => ""

def Lean.Syntax.setAtomVal :

Lean.Syntax → String → Lean.Syntax

Equations

Lean.Syntax.setAtomVal x✝ x = match x✝, x with | Lean.Syntax.atom info val, v => Lean.Syntax.atom info v | stx, x => stx

@[inline]

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

Equations

Lean.Syntax.ifNode stx hyes hno = match stx with | Lean.Syntax.node i k args => hyes { val := Lean.Syntax.node i k args, property := ⋯ } | x => hno ()

@[inline]

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

Equations

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

def Lean.Syntax.asNode :

Lean.Syntax → Lean.SyntaxNode

Equations

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

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

Lake.Name

Equations

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

@[inline]

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

Equations

Lean.Syntax.modifyArgs stx fn = match stx with | Lean.Syntax.node i k args => Lean.Syntax.node i k (fn args) | stx => stx

@[inline]

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

Equations

Lean.Syntax.modifyArg stx i fn = match stx with | Lean.Syntax.node info k args => Lean.Syntax.node info k (Array.modify args i fn) | stx => stx

@[specialize #[]]

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

Lean.Syntax → m Lean.Syntax

@[specialize #[]]

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

Lean.Syntax → m Lean.Syntax

@[inline]

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

Equations

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

def Lean.Syntax.updateLeading :

Lean.Syntax → Lean.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

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

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

Lean.Syntax → Lean.Syntax

partial def Lean.Syntax.getTailWithPos :

Lean.Syntax → Option Lean.Syntax

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

List Lean.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.

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

List Lake.Name

Equations

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

structure Lean.Syntax.TopDown :

firstChoiceOnly : Bool
stx : Lean.Syntax

Instances For

Lean.Syntax.instForInTopDownSyntax

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

Lean.Syntax.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

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

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

ForIn m Lean.Syntax.TopDown Lean.Syntax

Equations

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

@[specialize #[]]

partial def Lean.Syntax.instForInTopDownSyntax.loop {m : Type u_1 → Type u_2} :

{β : Type u_1} → [inst : Monad m] → (Lean.Syntax → β → m (ForInStep β)) → Bool → Lean.Syntax → β → [inst : Inhabited β] → m (ForInStep β)

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

Option String

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

String

Equations

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

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

Equations

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

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

Option String.Range

Equations

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

def Lean.Syntax.ofRange (range : String.Range) (canonical : optParam 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 : Lean.Syntax
parents : Array Lean.Syntax
idxs : Array Nat

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

Equations

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

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

Equations

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

def Lean.Syntax.Traverser.down (t : Lean.Syntax.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 : Lean.Syntax.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 : Lean.Syntax.Traverser) :

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

Equations

Lean.Syntax.Traverser.left t = if Array.size t.parents > 0 then Lean.Syntax.Traverser.down (Lean.Syntax.Traverser.up t) (Array.back t.idxs - 1) else t

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

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

Equations

Lean.Syntax.Traverser.right t = if Array.size t.parents > 0 then Lean.Syntax.Traverser.down (Lean.Syntax.Traverser.up t) (Array.back t.idxs + 1) else t

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

Type 1

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

st : MonadState Lean.Syntax.Traverser m

Instances

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

m Lean.Syntax

Equations

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

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

m Unit

Equations

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

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

m Unit

Equations

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

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

m Unit

Equations

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

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

m Unit

Equations

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

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

m Unit

Equations

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

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

m Nat

Equations

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

@[inline]

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

Lake.Name

Equations

Lean.SyntaxNode.getIdAt n i = Lean.Syntax.getId (Lean.SyntaxNode.getArg n i)

def Lean.mkListNode (args : Array Lean.Syntax) :

Equations

Lean.mkListNode args = Lean.mkNullNode args

def Lean.Syntax.isQuot :

Lean.Syntax → Bool

Equations

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

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

Equations

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

def Lean.Syntax.isAntiquot :

Lean.Syntax → Bool

Equations

Lean.Syntax.isAntiquot x = match x with | Lean.Syntax.node info (Lean.Name.str pre "antiquot") args => true | x => false

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

Lean.Syntax.isEscapedAntiquot stx = !Array.isEmpty (Lean.Syntax.getArgs stx[1])

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

Equations

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

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

Equations

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

def Lean.Syntax.antiquotKind? :

Lean.Syntax → Option (Lean.SyntaxNodeKind × Bool)

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

Equations

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

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

List (Lean.SyntaxNodeKind × Bool)

Equations

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

def Lean.Syntax.antiquotSpliceKind? :

Lean.Syntax → Option Lean.SyntaxNodeKind

Equations

Lean.Syntax.antiquotSpliceKind? x = match x with | Lean.Syntax.node info (Lean.Name.str k "antiquot_scope") args => some k | x => none

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

Equations

Lean.Syntax.isAntiquotSplice stx = Option.isSome (Lean.Syntax.antiquotSpliceKind? stx)

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

Array Lean.Syntax

Equations

Lean.Syntax.getAntiquotSpliceContents stx = Lean.Syntax.getArgs stx[3]

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

Equations

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

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

Equations

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

def Lean.Syntax.antiquotSuffixSplice? :

Lean.Syntax → Option Lean.SyntaxNodeKind

Equations

Lean.Syntax.antiquotSuffixSplice? x = match x with | Lean.Syntax.node info (Lean.Name.str k "antiquot_suffix_splice") args => some k | x => none

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

Equations

Lean.Syntax.isAntiquotSuffixSplice stx = Option.isSome (Lean.Syntax.antiquotSuffixSplice? stx)

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

Equations

Lean.Syntax.getAntiquotSuffixSpliceInner stx = stx[0]

def Lean.Syntax.mkAntiquotSuffixSpliceNode (kind : Lean.SyntaxNodeKind) (inner : Lean.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 : Lean.Syntax) :

Equations

Lean.Syntax.isTokenAntiquot stx = Lean.Syntax.isOfKind stx `token_antiquot

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

Equations

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

@[inline, reducible]

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 : Lean.Syntax) (visit : Lean.Syntax → Bool) (accept : optParam (Lean.Syntax → Bool) fun (stx : Lean.Syntax) => !Lean.Syntax.hasArgs stx) :

Option Lean.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

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

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

Option Lean.Syntax.Stack

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