Lean.Syntax

Lean.Syntax.getAtomVal! x = match x with | Lean.Syntax.atom x val => val | x => panicWithPosWithDecl "Lean.Syntax" "Lean.Syntax.getAtomVal!" 67 18 "getAtomVal!: not an atom"

source

def Lean.Syntax.setAtomVal :

Lean.Syntax → String → Lean.Syntax

Equations

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

source

@[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 := (_ : Lean.IsNode (Lean.Syntax.node i k args)) } | x => hno ()

source

@[inline]

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

β

Equations

Lean.Syntax.ifNodeKind stx kind hyes hno = match stx with | Lean.Syntax.node i k args => if (k == kind) = true then hyes { val := Lean.Syntax.node i k args, property := (_ : Lean.IsNode (Lean.Syntax.node i k args)) } else hno () | x => hno ()

source

def Lean.Syntax.asNode :

Lean.Syntax → Lean.SyntaxNode

Equations

Lean.Syntax.asNode x = match x with | Lean.Syntax.node info kind args => { val := Lean.Syntax.node info kind args, property := (_ : Lean.IsNode (Lean.Syntax.node info kind args)) } | x => { val := Lean.mkNullNode, property := Lean.Syntax.asNode.proof_1 }

source

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

Lean.Name

Equations

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

source

@[inline]

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

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

source

@[inline]

def Lean.Syntax.modifyArg (stx : Lean.Syntax) (i : Nat) (fn : Lean.Syntax → 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

source

@[specialize]

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

Lean.Syntax → m Lean.Syntax

source

@[specialize]

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

Lean.Syntax → m Lean.Syntax

source

@[inline]

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

Lean.Syntax

Equations

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

source

def Lean.Syntax.updateLeading :

Lean.Syntax → Lean.Syntax

Equations

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

source

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

Lean.Syntax → Lean.Syntax

source

partial def Lean.Syntax.getTailWithPos :

Lean.Syntax → Option Lean.Syntax

source

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

List Lean.Syntax

Equations

Lean.Syntax.identComponents stx nFields? = (fun nameComps => match stx with | Lean.Syntax.ident (Lean.SourceInfo.original lead pos trail x) rawStr val x_1 => let val := Lean.Name.eraseMacroScopes val; let nameComps := nameComps val nFields?; let rawComps := Lean.Syntax.splitNameLit rawStr; let rawComps := match nFields? with | some nFields => let nPrefix := List.length rawComps - nFields; let prefixSz := List.foldl (fun acc ss => acc + Substring.bsize ss + 1) 0 (List.take nPrefix rawComps); let prefixSz := prefixSz - 1; Substring.extract rawStr 0 prefixSz :: List.drop nPrefix rawComps | x => rawComps; if (List.length nameComps == List.length rawComps) = true then List.map (fun x => match x with | (id, ss) => let off := ss.startPos - rawStr.startPos; let lead := if (off == 0) = true then lead else String.toSubstring ""; let trail := if (ss.stopPos == rawStr.stopPos) = true then trail else String.toSubstring ""; let info := Lean.SourceInfo.original lead (pos + off) trail (pos + off + Substring.bsize ss); Lean.Syntax.ident info ss id []) (List.zip nameComps rawComps) else panicWithPosWithDecl "Lean.Syntax" "Lean.Syntax.identComponents" 199 4 ("assertion violation: " ++ "nameComps.length == rawComps.length\n ") | Lean.Syntax.ident si x val x_1 => let val := Lean.Name.eraseMacroScopes val; List.map (fun n => Lean.Syntax.ident si (String.toSubstring (Lean.Name.toString n)) n []) (nameComps val nFields?) | x => panicWithPosWithDecl "Lean.Syntax" "Lean.Syntax.identComponents" 212 9 "unreachable code has been reached") Lean.Syntax.identComponents.nameComps

source

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

List Lean.Name

Equations

Lean.Syntax.identComponents.nameComps n nFields? = match nFields? with | some nFields => let nameComps := Lean.Name.components n; let nPrefix := List.length nameComps - nFields; let namePrefix := List.foldl (fun acc n => acc ++ n) Lean.Name.anonymous (List.take nPrefix nameComps); namePrefix :: List.drop nPrefix nameComps | x => Lean.Name.components n

source

structure Lean.Syntax.TopDown :

Type

firstChoiceOnly : Bool
stx : Lean.Syntax

source

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

Lean.Syntax.TopDown

Equations

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

source

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

ForIn m Lean.Syntax.TopDown Lean.Syntax

Equations

Lean.Syntax.instForInTopDownSyntax = { forIn := fun {β} [Monad m] x init f => match x with | { firstChoiceOnly := firstChoiceOnly, stx := stx } => (fun loop => do let a ← loop stx init { default := init } match a with | ForInStep.yield b => pure b | ForInStep.done b => pure b) (Lean.Syntax.instForInTopDownSyntax.loop f firstChoiceOnly) }

source

@[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 β)

source

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

Option String

source

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

String

Equations

Lean.Syntax.reprint.reprintLeaf info val = match info with | Lean.SourceInfo.original lead x trail x_1 => toString "" ++ toString lead ++ toString "" ++ toString val ++ toString "" ++ toString trail ++ toString "" | x => toString " " ++ toString val ++ toString " "

source

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

Bool

Equations

Lean.Syntax.hasMissing stx = Id.run do let r ← let col := Lean.Syntax.topDown stx; forIn col { fst := none, snd := PUnit.unit } fun stx r => let r := r.snd; if Lean.Syntax.isMissing stx = true then pure (ForInStep.done { fst := some true, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Id Bool := fun y => pure false match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

structure Lean.Syntax.Traverser :

Type

cur : Lean.Syntax
parents : Array Lean.Syntax
idxs : Array Nat

source

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

Lean.Syntax.Traverser

Equations

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

source

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

Lean.Syntax.Traverser

Equations

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

source

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

Lean.Syntax.Traverser

Equations

Lean.Syntax.Traverser.down t idx = if idx < Lean.Syntax.getNumArgs t.cur then { cur := Lean.Syntax.getArg t.cur idx, parents := Array.push t.parents (Lean.Syntax.setArg t.cur idx default), idxs := Array.push t.idxs idx } else { cur := Lean.Syntax.missing, parents := Array.push t.parents t.cur, idxs := Array.push t.idxs idx }

source

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

Lean.Syntax.Traverser

Equations

Lean.Syntax.Traverser.up t = if Array.size t.parents > 0 then let cur := if Array.back t.idxs < Lean.Syntax.getNumArgs (Array.back t.parents) then Lean.Syntax.setArg (Array.back t.parents) (Array.back t.idxs) t.cur else Array.back t.parents; { cur := cur, parents := Array.pop t.parents, idxs := Array.pop t.idxs } else t

source

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

Lean.Syntax.Traverser

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

source

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

Lean.Syntax.Traverser

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

source

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

Type 1

st : MonadState Lean.Syntax.Traverser m

Instances

source

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

m Lean.Syntax

Equations

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

source

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.setCur t stx

source

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.down t idx

source

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.up t

source

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.left t

source

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.right t

source

def Lean.Syntax.MonadTraverser.getIdx {m : Type → Type} [inst : 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)

source

@[inline]

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

Lean.Name

Equations

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

source

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

Lean.Syntax

Equations

Lean.mkListNode args = Lean.mkNullNode args

source

def Lean.Syntax.isQuot :

Lean.Syntax → Bool

Equations

Lean.Syntax.isQuot x = match x with | Lean.Syntax.node x (Lean.Name.str x_1 "quot" x_2) x_3 => true | Lean.Syntax.node x (Lean.Name.str (Lean.Name.str (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "Parser" x_3) "Term" x_4) "dynamicQuot" x_5) x_1 => true | x => false

source

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

Lean.Syntax

Equations

Lean.Syntax.getQuotContent stx = if Lean.Syntax.isOfKind stx `Lean.Parser.Term.dynamicQuot = true then Lean.Syntax.getOp stx 3 else Lean.Syntax.getOp stx 1

source

def Lean.Syntax.isAntiquot :

Lean.Syntax → Bool

Equations

Lean.Syntax.isAntiquot x = match x with | Lean.Syntax.node x (Lean.Name.str x_1 "antiquot" x_2) x_3 => true | x => false

source

def Lean.Syntax.mkAntiquotNode (term : Lean.Syntax) (nesting : optParam Nat 0) (name : optParam (Option String) none) (kind : optParam Lean.Name Lean.Name.anonymous) :

Lean.Syntax

Equations

Lean.Syntax.mkAntiquotNode term nesting name kind = let nesting := Lean.mkNullNode (mkArray nesting (Lean.mkAtom "$")); let term := match Lean.Syntax.isIdent term with | true => term | false => Lean.mkNode `antiquotNestedExpr #[Lean.mkAtom "(", term, Lean.mkAtom ")"]; let name := match name with | some name => Lean.mkNode `antiquotName #[Lean.mkAtom ":", Lean.mkAtom name] | none => Lean.mkNullNode; Lean.mkNode (kind ++ `antiquot) #[Lean.mkAtom "$", nesting, term, name]