Lean.Parser.Basic

Lean.Parser.ParserContext.resolveName ctx id = Lean.ResolveName.resolveGlobalName ctx.toParserModuleContext.env ctx.toParserModuleContext.currNamespace ctx.toParserModuleContext.openDecls id

source

structure Lean.Parser.Error :

Type

unexpected : String
expected : List String

source

instance Lean.Parser.instInhabitedError :

Inhabited Lean.Parser.Error

Equations

Lean.Parser.instInhabitedError = { default := { unexpected := default, expected := default } }

source

instance Lean.Parser.instBEqError :

BEq Lean.Parser.Error

Equations

Lean.Parser.instBEqError = { beq := [anonymous] }

source

def Lean.Parser.Error.toString (e : Lean.Parser.Error) :

String

Equations

Lean.Parser.Error.toString e = let unexpected := if (e.unexpected == "") = true then [] else [e.unexpected]; let expected := if (e.expected == []) = true then [] else let expected := Array.qsort (List.toArray e.expected) (fun e e' => decide (e < e')) 0 (Array.size (List.toArray e.expected) - 1); let expected := List.eraseReps (Array.toList expected); ["expected " ++ Lean.Parser.Error.expectedToString expected]; String.intercalate "; " (unexpected ++ expected)

source

instance Lean.Parser.Error.instToStringError :

ToString Lean.Parser.Error

Equations

Lean.Parser.Error.instToStringError = { toString := Lean.Parser.Error.toString }

source

def Lean.Parser.Error.merge (e₁ : Lean.Parser.Error) (e₂ : Lean.Parser.Error) :

Lean.Parser.Error

Equations

Lean.Parser.Error.merge e₁ e₂ = match e₂ with | { unexpected := u, expected := x } => { unexpected := if (u == "") = true then e₁.unexpected else u, expected := e₁.expected ++ e₂.expected }

source

structure Lean.Parser.ParserState :

Type

stxStack : Array Lean.Syntax
lhsPrec : Nat
pos : String.Pos
cache : Lean.Parser.ParserCache
errorMsg : Option Lean.Parser.Error

source

@[inline]

def Lean.Parser.ParserState.hasError (s : Lean.Parser.ParserState) :

Bool

Equations

Lean.Parser.ParserState.hasError s = (s.errorMsg != none)

source

@[inline]

def Lean.Parser.ParserState.stackSize (s : Lean.Parser.ParserState) :

Nat

Equations

Lean.Parser.ParserState.stackSize s = Array.size s.stxStack

source

def Lean.Parser.ParserState.restore (s : Lean.Parser.ParserState) (iniStackSz : Nat) (iniPos : Nat) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.restore s iniStackSz iniPos = { stxStack := Array.shrink s.stxStack iniStackSz, lhsPrec := s.lhsPrec, pos := iniPos, cache := s.cache, errorMsg := none }

source

def Lean.Parser.ParserState.setPos (s : Lean.Parser.ParserState) (pos : Nat) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.setPos s pos = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := pos, cache := s.cache, errorMsg := s.errorMsg }

source

def Lean.Parser.ParserState.setCache (s : Lean.Parser.ParserState) (cache : Lean.Parser.ParserCache) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.setCache s cache = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := s.pos, cache := cache, errorMsg := s.errorMsg }

source

def Lean.Parser.ParserState.pushSyntax (s : Lean.Parser.ParserState) (n : Lean.Syntax) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.pushSyntax s n = { stxStack := Array.push s.stxStack n, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg }

source

def Lean.Parser.ParserState.popSyntax (s : Lean.Parser.ParserState) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.popSyntax s = { stxStack := Array.pop s.stxStack, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg }

source

def Lean.Parser.ParserState.shrinkStack (s : Lean.Parser.ParserState) (iniStackSz : Nat) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.shrinkStack s iniStackSz = { stxStack := Array.shrink s.stxStack iniStackSz, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg }

source

def Lean.Parser.ParserState.next (s : Lean.Parser.ParserState) (input : String) (pos : Nat) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.next s input pos = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := String.next input pos, cache := s.cache, errorMsg := s.errorMsg }

source

def Lean.Parser.ParserState.toErrorMsg (ctx : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) :

String

Equations

Lean.Parser.ParserState.toErrorMsg ctx s = match s.errorMsg with | none => "" | some msg => let pos := Lean.FileMap.toPosition ctx.toInputContext.fileMap s.pos; Lean.mkErrorStringWithPos ctx.toInputContext.fileName pos (toString msg)

source

def Lean.Parser.ParserState.mkNode (s : Lean.Parser.ParserState) (k : Lean.SyntaxNodeKind) (iniStackSz : Nat) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.mkNode s k iniStackSz = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := err } => if (err != none && Array.size stack == iniStackSz) = true then let stack := Array.push stack Lean.Syntax.missing; { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := err } else let newNode := Lean.Syntax.node Lean.SourceInfo.none k (Array.extract stack iniStackSz (Array.size stack)); let stack := Array.shrink stack iniStackSz; let stack := Array.push stack newNode; { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := err }

source

def Lean.Parser.ParserState.mkTrailingNode (s : Lean.Parser.ParserState) (k : Lean.SyntaxNodeKind) (iniStackSz : Nat) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.mkTrailingNode s k iniStackSz = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := err } => let newNode := Lean.Syntax.node Lean.SourceInfo.none k (Array.extract stack (iniStackSz - 1) (Array.size stack)); let stack := Array.shrink stack (iniStackSz - 1); let stack := Array.push stack newNode; { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := err }

source

def Lean.Parser.ParserState.setError (s : Lean.Parser.ParserState) (msg : String) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.setError s msg = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := x } => { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some { unexpected := "", expected := [msg] } }

source

def Lean.Parser.ParserState.mkError (s : Lean.Parser.ParserState) (msg : String) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.mkError s msg = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := x } => { stxStack := Array.push stack Lean.Syntax.missing, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some { unexpected := "", expected := [msg] } }

source

def Lean.Parser.ParserState.mkUnexpectedError (s : Lean.Parser.ParserState) (msg : String) (expected : optParam (List String) []) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.mkUnexpectedError s msg expected = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := x } => { stxStack := Array.push stack Lean.Syntax.missing, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some { unexpected := msg, expected := expected } }

source

def Lean.Parser.ParserState.mkEOIError (s : Lean.Parser.ParserState) (expected : optParam (List String) []) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.mkEOIError s expected = Lean.Parser.ParserState.mkUnexpectedError s "unexpected end of input" expected

source

def Lean.Parser.ParserState.mkErrorAt (s : Lean.Parser.ParserState) (msg : String) (pos : String.Pos) (initStackSz? : optParam (Option Nat) none) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.mkErrorAt s msg pos initStackSz? = match s, initStackSz? with | { stxStack := stack, lhsPrec := lhsPrec, pos := x, cache := cache, errorMsg := x_1 }, none => { stxStack := Array.push stack Lean.Syntax.missing, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some { unexpected := "", expected := [msg] } } | { stxStack := stack, lhsPrec := lhsPrec, pos := x, cache := cache, errorMsg := x_1 }, some sz => { stxStack := Array.push (Array.shrink stack sz) Lean.Syntax.missing, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some { unexpected := "", expected := [msg] } }

source

def Lean.Parser.ParserState.mkErrorsAt (s : Lean.Parser.ParserState) (ex : List String) (pos : String.Pos) (initStackSz? : optParam (Option Nat) none) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.mkErrorsAt s ex pos initStackSz? = match s, initStackSz? with | { stxStack := stack, lhsPrec := lhsPrec, pos := x, cache := cache, errorMsg := x_1 }, none => { stxStack := Array.push stack Lean.Syntax.missing, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some { unexpected := "", expected := ex } } | { stxStack := stack, lhsPrec := lhsPrec, pos := x, cache := cache, errorMsg := x_1 }, some sz => { stxStack := Array.push (Array.shrink stack sz) Lean.Syntax.missing, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some { unexpected := "", expected := ex } }

source

def Lean.Parser.ParserState.mkUnexpectedErrorAt (s : Lean.Parser.ParserState) (msg : String) (pos : String.Pos) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.mkUnexpectedErrorAt s msg pos = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := x, cache := cache, errorMsg := x_1 } => { stxStack := Array.push stack Lean.Syntax.missing, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some { unexpected := msg, expected := [] } }

source

noncomputable def Lean.Parser.ParserFn :

Type

Equations

Lean.Parser.ParserFn = (Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState)

source

instance Lean.Parser.instInhabitedParserFn :

Inhabited Lean.Parser.ParserFn

Equations

Lean.Parser.instInhabitedParserFn = { default := fun ctx s => s }

source

inductive Lean.Parser.FirstTokens :

Type

epsilon: Lean.Parser.FirstTokens
unknown: Lean.Parser.FirstTokens
tokens: List Lean.Parser.Token → Lean.Parser.FirstTokens
optTokens: List Lean.Parser.Token → Lean.Parser.FirstTokens

source

instance Lean.Parser.instInhabitedFirstTokens :

Inhabited Lean.Parser.FirstTokens

Equations

Lean.Parser.instInhabitedFirstTokens = { default := Lean.Parser.FirstTokens.epsilon }

source

def Lean.Parser.FirstTokens.seq :

Lean.Parser.FirstTokens → Lean.Parser.FirstTokens → Lean.Parser.FirstTokens

Equations

Lean.Parser.FirstTokens.seq x x = match x, x with | Lean.Parser.FirstTokens.epsilon, tks => tks | Lean.Parser.FirstTokens.optTokens s₁, Lean.Parser.FirstTokens.optTokens s₂ => Lean.Parser.FirstTokens.optTokens (s₁ ++ s₂) | Lean.Parser.FirstTokens.optTokens s₁, Lean.Parser.FirstTokens.tokens s₂ => Lean.Parser.FirstTokens.tokens (s₁ ++ s₂) | tks, x => tks

source

def Lean.Parser.FirstTokens.toOptional :

Lean.Parser.FirstTokens → Lean.Parser.FirstTokens

Equations

Lean.Parser.FirstTokens.toOptional x = match x with | Lean.Parser.FirstTokens.tokens tks => Lean.Parser.FirstTokens.optTokens tks | tks => tks

source

def Lean.Parser.FirstTokens.merge :

Lean.Parser.FirstTokens → Lean.Parser.FirstTokens → Lean.Parser.FirstTokens

Equations

Lean.Parser.FirstTokens.merge x x = match x, x with | Lean.Parser.FirstTokens.epsilon, tks => Lean.Parser.FirstTokens.toOptional tks | tks, Lean.Parser.FirstTokens.epsilon => Lean.Parser.FirstTokens.toOptional tks | Lean.Parser.FirstTokens.tokens s₁, Lean.Parser.FirstTokens.tokens s₂ => Lean.Parser.FirstTokens.tokens (s₁ ++ s₂) | Lean.Parser.FirstTokens.optTokens s₁, Lean.Parser.FirstTokens.optTokens s₂ => Lean.Parser.FirstTokens.optTokens (s₁ ++ s₂) | Lean.Parser.FirstTokens.tokens s₁, Lean.Parser.FirstTokens.optTokens s₂ => Lean.Parser.FirstTokens.optTokens (s₁ ++ s₂) | Lean.Parser.FirstTokens.optTokens s₁, Lean.Parser.FirstTokens.tokens s₂ => Lean.Parser.FirstTokens.optTokens (s₁ ++ s₂) | x, x_1 => Lean.Parser.FirstTokens.unknown

source

def Lean.Parser.FirstTokens.toStr :

Lean.Parser.FirstTokens → String

Equations

Lean.Parser.FirstTokens.toStr x = match x with | Lean.Parser.FirstTokens.epsilon => "epsilon" | Lean.Parser.FirstTokens.unknown => "unknown" | Lean.Parser.FirstTokens.tokens tks => toString tks | Lean.Parser.FirstTokens.optTokens tks => "?" ++ toString tks

source

instance Lean.Parser.FirstTokens.instToStringFirstTokens :

ToString Lean.Parser.FirstTokens

Equations

Lean.Parser.FirstTokens.instToStringFirstTokens = { toString := Lean.Parser.FirstTokens.toStr }

source

structure Lean.Parser.ParserInfo :

Type

collectTokens : List Lean.Parser.Token → List Lean.Parser.Token
collectKinds : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet
firstTokens : Lean.Parser.FirstTokens

source

instance Lean.Parser.instInhabitedParserInfo :

Inhabited Lean.Parser.ParserInfo

Equations

Lean.Parser.instInhabitedParserInfo = { default := { collectTokens := default, collectKinds := default, firstTokens := default } }

source

structure Lean.Parser.Parser :

Type

info : Lean.Parser.ParserInfo
fn : Lean.Parser.ParserFn

source

instance Lean.Parser.instInhabitedParser :

Inhabited Lean.Parser.Parser

Equations

Lean.Parser.instInhabitedParser = { default := { info := default, fn := default } }

source

@[inline]

abbrev Lean.Parser.TrailingParser :

Type

Equations

Lean.Parser.TrailingParser = Lean.Parser.Parser

source

def Lean.Parser.dbgTraceStateFn (label : String) (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.dbgTraceStateFn label p c s = let sz := Array.size s.stxStack; let s' := p c s; dbgTrace (toString "" ++ toString label ++ toString "\n pos: " ++ toString s'.pos ++ toString "\n err: " ++ toString s'.errorMsg ++ toString "\n out: " ++ toString (Array.extract s'.stxStack sz (Array.size s'.stxStack)) ++ toString "") fun x => s'

source

def Lean.Parser.dbgTraceState (label : String) (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.dbgTraceState label p = { info := p.info, fn := Lean.Parser.dbgTraceStateFn label p.fn }

source

@[noinline]

def Lean.Parser.epsilonInfo :

Lean.Parser.ParserInfo

Equations

Lean.Parser.epsilonInfo = { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.epsilon }

source

@[inline]

def Lean.Parser.checkStackTopFn (p : Lean.Syntax → Bool) (msg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkStackTopFn p msg c s = if p (Array.back s.stxStack) = true then s else Lean.Parser.ParserState.mkUnexpectedError s msg

source

@[inline]

def Lean.Parser.checkStackTop (p : Lean.Syntax → Bool) (msg : String) :

Lean.Parser.Parser

Equations

Lean.Parser.checkStackTop p msg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkStackTopFn p msg }

source

@[inline]

def Lean.Parser.andthenFn (p : Lean.Parser.ParserFn) (q : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.andthenFn p q c s = let s := p c s; if Lean.Parser.ParserState.hasError s = true then s else q c s

source

@[noinline]

def Lean.Parser.andthenInfo (p : Lean.Parser.ParserInfo) (q : Lean.Parser.ParserInfo) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.andthenInfo p q = { collectTokens := p.collectTokens ∘ q.collectTokens, collectKinds := p.collectKinds ∘ q.collectKinds, firstTokens := Lean.Parser.FirstTokens.seq p.firstTokens q.firstTokens }

source

@[inline]

def Lean.Parser.andthen (p : Lean.Parser.Parser) (q : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.andthen p q = { info := Lean.Parser.andthenInfo p.info q.info, fn := Lean.Parser.andthenFn p.fn q.fn }

source

instance Lean.Parser.instAndThenParser :

AndThen Lean.Parser.Parser

Equations

Lean.Parser.instAndThenParser = { andThen := fun a b => Lean.Parser.andthen a (b ()) }

source

@[inline]

def Lean.Parser.nodeFn (n : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.nodeFn n p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let s := p c s; Lean.Parser.ParserState.mkNode s n iniSz

source

@[inline]

def Lean.Parser.trailingNodeFn (n : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.trailingNodeFn n p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let s := p c s; Lean.Parser.ParserState.mkTrailingNode s n iniSz

source

@[noinline]

def Lean.Parser.nodeInfo (n : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserInfo) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.nodeInfo n p = { collectTokens := p.collectTokens, collectKinds := fun s => Lean.Parser.SyntaxNodeKindSet.insert (Lean.Parser.ParserInfo.collectKinds p s) n, firstTokens := p.firstTokens }

source

@[inline]

def Lean.Parser.node (n : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.node n p = { info := Lean.Parser.nodeInfo n p.info, fn := Lean.Parser.nodeFn n p.fn }

source

def Lean.Parser.errorFn (msg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.errorFn msg x s = Lean.Parser.ParserState.mkUnexpectedError s msg

source

@[inline]

def Lean.Parser.error (msg : String) :

Lean.Parser.Parser

Equations

Lean.Parser.error msg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.errorFn msg }

source

def Lean.Parser.errorAtSavedPosFn (msg : String) (delta : Bool) :

Lean.Parser.ParserFn

Equations

Lean.Parser.errorAtSavedPosFn msg delta c s = match c.savedPos? with | none => s | some pos => let pos := if delta = true then String.next c.toInputContext.input pos else pos; match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := x, cache := cache, errorMsg := x_1 } => { stxStack := Array.push stack Lean.Syntax.missing, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some { unexpected := msg, expected := [] } }

source

@[inline]

def Lean.Parser.errorAtSavedPos (msg : String) (delta : Bool) :

Lean.Parser.Parser

Equations

Lean.Parser.errorAtSavedPos msg delta = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.errorAtSavedPosFn msg delta }

source

def Lean.Parser.checkPrecFn (prec : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkPrecFn prec c s = if c.prec ≤ prec then s else Lean.Parser.ParserState.mkUnexpectedError s "unexpected token at this precedence level; consider parenthesizing the term"

source

@[inline]

def Lean.Parser.checkPrec (prec : Nat) :

Lean.Parser.Parser

Equations

Lean.Parser.checkPrec prec = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkPrecFn prec }

source

def Lean.Parser.checkLhsPrecFn (prec : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkLhsPrecFn prec c s = if s.lhsPrec ≥ prec then s else Lean.Parser.ParserState.mkUnexpectedError s "unexpected token at this precedence level; consider parenthesizing the term"

source

@[inline]

def Lean.Parser.checkLhsPrec (prec : Nat) :

Lean.Parser.Parser

Equations

Lean.Parser.checkLhsPrec prec = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkLhsPrecFn prec }

source

def Lean.Parser.setLhsPrecFn (prec : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.setLhsPrecFn prec c s = if Lean.Parser.ParserState.hasError s = true then s else { stxStack := s.stxStack, lhsPrec := prec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg }

source

@[inline]

def Lean.Parser.setLhsPrec (prec : Nat) :

Lean.Parser.Parser

Equations

Lean.Parser.setLhsPrec prec = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.setLhsPrecFn prec }

source

def Lean.Parser.checkInsideQuotFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkInsideQuotFn c s = if (decide (c.quotDepth > 0) && !c.suppressInsideQuot) = true then s else Lean.Parser.ParserState.mkUnexpectedError s "unexpected syntax outside syntax quotation"

source

@[inline]

def Lean.Parser.checkInsideQuot :

Lean.Parser.Parser

Equations

Lean.Parser.checkInsideQuot = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkInsideQuotFn }

source

def Lean.Parser.checkOutsideQuotFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkOutsideQuotFn c s = if (!c.quotDepth == 0 || c.suppressInsideQuot) = true then s else Lean.Parser.ParserState.mkUnexpectedError s "unexpected syntax inside syntax quotation"

source

@[inline]

def Lean.Parser.checkOutsideQuot :

Lean.Parser.Parser

Equations

Lean.Parser.checkOutsideQuot = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkOutsideQuotFn }

source

def Lean.Parser.addQuotDepthFn (i : Int) (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.addQuotDepthFn i p c s = p { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := c.prec, tokens := c.tokens, quotDepth := Int.toNat (Int.ofNat c.quotDepth + i), suppressInsideQuot := c.suppressInsideQuot, savedPos? := c.savedPos?, forbiddenTk? := c.forbiddenTk? } s

source

@[inline]

def Lean.Parser.incQuotDepth (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.incQuotDepth p = { info := p.info, fn := Lean.Parser.addQuotDepthFn 1 p.fn }

source

@[inline]

def Lean.Parser.decQuotDepth (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.decQuotDepth p = { info := p.info, fn := Lean.Parser.addQuotDepthFn (-1) p.fn }

source

def Lean.Parser.suppressInsideQuotFn (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.suppressInsideQuotFn p c s = p { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := c.prec, tokens := c.tokens, quotDepth := c.quotDepth, suppressInsideQuot := true, savedPos? := c.savedPos?, forbiddenTk? := c.forbiddenTk? } s

source

@[inline]

def Lean.Parser.suppressInsideQuot (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.suppressInsideQuot p = { info := p.info, fn := Lean.Parser.suppressInsideQuotFn p.fn }

source

@[inline]

def Lean.Parser.leadingNode (n : Lean.SyntaxNodeKind) (prec : Nat) (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.leadingNode n prec p = HAndThen.hAndThen (Lean.Parser.checkPrec prec) fun x => HAndThen.hAndThen (Lean.Parser.node n p) fun x => Lean.Parser.setLhsPrec prec

source

@[inline]

def Lean.Parser.trailingNodeAux (n : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) :

Lean.Parser.TrailingParser

Equations

Lean.Parser.trailingNodeAux n p = { info := Lean.Parser.nodeInfo n p.info, fn := Lean.Parser.trailingNodeFn n p.fn }

source

@[inline]

def Lean.Parser.trailingNode (n : Lean.SyntaxNodeKind) (prec : Nat) (lhsPrec : Nat) (p : Lean.Parser.Parser) :

Lean.Parser.TrailingParser

Equations

Lean.Parser.trailingNode n prec lhsPrec p = HAndThen.hAndThen (Lean.Parser.checkPrec prec) fun x => HAndThen.hAndThen (Lean.Parser.checkLhsPrec lhsPrec) fun x => HAndThen.hAndThen (Lean.Parser.trailingNodeAux n p) fun x => Lean.Parser.setLhsPrec prec

source

def Lean.Parser.mergeOrElseErrors (s : Lean.Parser.ParserState) (error1 : Lean.Parser.Error) (iniPos : Nat) (mergeErrors : Bool) :

Lean.Parser.ParserState

Equations

Lean.Parser.mergeOrElseErrors s error1 iniPos mergeErrors = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some error2 } => if (pos == iniPos) = true then { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some (if mergeErrors = true then Lean.Parser.Error.merge error1 error2 else error2) } else s | other => other

source

def Lean.Parser.orelseFnCore (p : Lean.Parser.ParserFn) (q : Lean.Parser.ParserFn) (mergeErrors : Bool) :

Lean.Parser.ParserFn

Equations

Lean.Parser.orelseFnCore p q mergeErrors c s = let iniSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := p c s; match s.errorMsg with | some errorMsg => if (s.pos == iniPos) = true then Lean.Parser.mergeOrElseErrors (q c (Lean.Parser.ParserState.restore s iniSz iniPos)) errorMsg iniPos mergeErrors else s | none => s

source

@[inline]

def Lean.Parser.orelseFn (p : Lean.Parser.ParserFn) (q : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.orelseFn p q = Lean.Parser.orelseFnCore p q true

source

@[noinline]

def Lean.Parser.orelseInfo (p : Lean.Parser.ParserInfo) (q : Lean.Parser.ParserInfo) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.orelseInfo p q = { collectTokens := p.collectTokens ∘ q.collectTokens, collectKinds := p.collectKinds ∘ q.collectKinds, firstTokens := Lean.Parser.FirstTokens.merge p.firstTokens q.firstTokens }

source

@[inline]

def Lean.Parser.orelse (p : Lean.Parser.Parser) (q : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.orelse p q = { info := Lean.Parser.orelseInfo p.info q.info, fn := Lean.Parser.orelseFn p.fn q.fn }

source

instance Lean.Parser.instOrElseParser :

OrElse Lean.Parser.Parser

Equations

Lean.Parser.instOrElseParser = { orElse := fun a b => Lean.Parser.orelse a (b ()) }

source

@[noinline]

def Lean.Parser.noFirstTokenInfo (info : Lean.Parser.ParserInfo) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.noFirstTokenInfo info = { collectTokens := info.collectTokens, collectKinds := info.collectKinds, firstTokens := Lean.Parser.FirstTokens.unknown }

source

def Lean.Parser.atomicFn (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.atomicFn p c s = let iniPos := s.pos; match p c s with | { stxStack := stack, lhsPrec := lhsPrec, pos := x, cache := cache, errorMsg := some msg } => { stxStack := stack, lhsPrec := lhsPrec, pos := iniPos, cache := cache, errorMsg := some msg } | other => other

source

@[inline]

def Lean.Parser.atomic (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.atomic p = { info := p.info, fn := Lean.Parser.atomicFn p.fn }

source

def Lean.Parser.optionalFn (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.optionalFn p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := p c s; let s := if (Lean.Parser.ParserState.hasError s && s.pos == iniPos) = true then Lean.Parser.ParserState.restore s iniSz iniPos else s; Lean.Parser.ParserState.mkNode s Lean.nullKind iniSz

source

@[noinline]

def Lean.Parser.optionaInfo (p : Lean.Parser.ParserInfo) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.optionaInfo p = { collectTokens := p.collectTokens, collectKinds := p.collectKinds, firstTokens := Lean.Parser.FirstTokens.toOptional p.firstTokens }

source

@[inline]

def Lean.Parser.optionalNoAntiquot (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.optionalNoAntiquot p = { info := Lean.Parser.optionaInfo p.info, fn := Lean.Parser.optionalFn p.fn }

source

def Lean.Parser.lookaheadFn (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.lookaheadFn p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := p c s; if Lean.Parser.ParserState.hasError s = true then s else Lean.Parser.ParserState.restore s iniSz iniPos

source

@[inline]

def Lean.Parser.lookahead (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.lookahead p = { info := p.info, fn := Lean.Parser.lookaheadFn p.fn }

source

def Lean.Parser.notFollowedByFn (p : Lean.Parser.ParserFn) (msg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.notFollowedByFn p msg c s = let iniSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := p c s; if Lean.Parser.ParserState.hasError s = true then Lean.Parser.ParserState.restore s iniSz iniPos else let s := Lean.Parser.ParserState.restore s iniSz iniPos; Lean.Parser.ParserState.mkUnexpectedError s (toString "unexpected " ++ toString msg ++ toString "")

source

@[inline]

def Lean.Parser.notFollowedBy (p : Lean.Parser.Parser) (msg : String) :

Lean.Parser.Parser

Equations

Lean.Parser.notFollowedBy p msg = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.notFollowedByFn p.fn msg }

source

partial def Lean.Parser.manyAux (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

source

@[inline]

def Lean.Parser.manyFn (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.manyFn p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let s := Lean.Parser.manyAux p c s; Lean.Parser.ParserState.mkNode s Lean.nullKind iniSz

source

@[inline]

def Lean.Parser.manyNoAntiquot (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.manyNoAntiquot p = { info := Lean.Parser.noFirstTokenInfo p.info, fn := Lean.Parser.manyFn p.fn }

source

@[inline]

def Lean.Parser.many1Fn (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.many1Fn p c s = let iniSz := Lean.Parser.ParserState.stackSize s; let s := Lean.Parser.andthenFn p (Lean.Parser.manyAux p) c s; Lean.Parser.ParserState.mkNode s Lean.nullKind iniSz

source

@[inline]

def Lean.Parser.many1NoAntiquot (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.many1NoAntiquot p = { info := p.info, fn := Lean.Parser.many1Fn p.fn }

source

def Lean.Parser.sepByFn (allowTrailingSep : Bool) (p : Lean.Parser.ParserFn) (sep : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.sepByFn allowTrailingSep p sep c s = let iniSz := Lean.Parser.ParserState.stackSize s; Lean.Parser.sepByFnAux p sep allowTrailingSep iniSz true c s

source

def Lean.Parser.sepBy1Fn (allowTrailingSep : Bool) (p : Lean.Parser.ParserFn) (sep : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.sepBy1Fn allowTrailingSep p sep c s = let iniSz := Lean.Parser.ParserState.stackSize s; Lean.Parser.sepByFnAux p sep allowTrailingSep iniSz false c s

source

@[noinline]

def Lean.Parser.sepByInfo (p : Lean.Parser.ParserInfo) (sep : Lean.Parser.ParserInfo) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.sepByInfo p sep = { collectTokens := p.collectTokens ∘ sep.collectTokens, collectKinds := p.collectKinds ∘ sep.collectKinds, firstTokens := Lean.Parser.FirstTokens.unknown }

source

@[noinline]

def Lean.Parser.sepBy1Info (p : Lean.Parser.ParserInfo) (sep : Lean.Parser.ParserInfo) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.sepBy1Info p sep = { collectTokens := p.collectTokens ∘ sep.collectTokens, collectKinds := p.collectKinds ∘ sep.collectKinds, firstTokens := p.firstTokens }

source

@[inline]

def Lean.Parser.sepByNoAntiquot (p : Lean.Parser.Parser) (sep : Lean.Parser.Parser) (allowTrailingSep : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.sepByNoAntiquot p sep allowTrailingSep = { info := Lean.Parser.sepByInfo p.info sep.info, fn := Lean.Parser.sepByFn allowTrailingSep p.fn sep.fn }

source

@[inline]

def Lean.Parser.sepBy1NoAntiquot (p : Lean.Parser.Parser) (sep : Lean.Parser.Parser) (allowTrailingSep : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.sepBy1NoAntiquot p sep allowTrailingSep = { info := Lean.Parser.sepBy1Info p.info sep.info, fn := Lean.Parser.sepBy1Fn allowTrailingSep p.fn sep.fn }

source

def Lean.Parser.withResultOfFn (p : Lean.Parser.ParserFn) (f : Lean.Syntax → Lean.Syntax) :

Lean.Parser.ParserFn

Equations

Lean.Parser.withResultOfFn p f c s = let s := p c s; if Lean.Parser.ParserState.hasError s = true then s else let stx := Array.back s.stxStack; Lean.Parser.ParserState.pushSyntax (Lean.Parser.ParserState.popSyntax s) (f stx)

source

@[noinline]

def Lean.Parser.withResultOfInfo (p : Lean.Parser.ParserInfo) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.withResultOfInfo p = { collectTokens := p.collectTokens, collectKinds := p.collectKinds, firstTokens := Lean.Parser.FirstTokens.unknown }

source

@[inline]

def Lean.Parser.withResultOf (p : Lean.Parser.Parser) (f : Lean.Syntax → Lean.Syntax) :

Lean.Parser.Parser

Equations

Lean.Parser.withResultOf p f = { info := Lean.Parser.withResultOfInfo p.info, fn := Lean.Parser.withResultOfFn p.fn f }

source

@[inline]

def Lean.Parser.many1Unbox (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.many1Unbox p = Lean.Parser.withResultOf (Lean.Parser.many1NoAntiquot p) fun stx => if (Lean.Syntax.getNumArgs stx == 1) = true then Lean.Syntax.getArg stx 0 else stx

source

def Lean.Parser.satisfyFn (p : Char → Bool) (errorMsg : optParam String "unexpected character") :

Lean.Parser.ParserFn

Equations

Lean.Parser.satisfyFn p errorMsg c s = let i := s.pos; if String.atEnd c.toInputContext.input i = true then Lean.Parser.ParserState.mkEOIError s else if p (String.get c.toInputContext.input i) = true then Lean.Parser.ParserState.next s c.toInputContext.input i else Lean.Parser.ParserState.mkUnexpectedError s errorMsg

source

partial def Lean.Parser.takeUntilFn (p : Char → Bool) :

Lean.Parser.ParserFn

source

def Lean.Parser.takeWhileFn (p : Char → Bool) :

Lean.Parser.ParserFn

Equations

Lean.Parser.takeWhileFn p = Lean.Parser.takeUntilFn fun c => !p c

source

@[inline]

def Lean.Parser.takeWhile1Fn (p : Char → Bool) (errorMsg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.takeWhile1Fn p errorMsg = Lean.Parser.andthenFn (Lean.Parser.satisfyFn p errorMsg) (Lean.Parser.takeWhileFn p)

source

partial def Lean.Parser.finishCommentBlock (nesting : Nat) :

Lean.Parser.ParserFn

source

def Lean.Parser.finishCommentBlock.eoi (s : Lean.Parser.ParserState) :

Lean.Parser.ParserState

Equations

Lean.Parser.finishCommentBlock.eoi s = Lean.Parser.ParserState.mkUnexpectedError s "unterminated comment"

source

partial def Lean.Parser.whitespace :

Lean.Parser.ParserFn

source

def Lean.Parser.mkEmptySubstringAt (s : String) (p : Nat) :

Substring

Equations

Lean.Parser.mkEmptySubstringAt s p = { str := s, startPos := p, stopPos := p }

source

@[inline]

def Lean.Parser.rawFn (p : Lean.Parser.ParserFn) (trailingWs : optParam Bool false) :

Lean.Parser.ParserFn

Equations

Lean.Parser.rawFn p trailingWs c s = let startPos := s.pos; let s := p c s; if Lean.Parser.ParserState.hasError s = true then s else Lean.Parser.rawAux startPos trailingWs c s

source

@[inline]

def Lean.Parser.chFn (c : Char) (trailingWs : optParam Bool false) :

Lean.Parser.ParserFn

Equations

Lean.Parser.chFn c trailingWs = Lean.Parser.rawFn (Lean.Parser.satisfyFn (fun d => c == d) ("'" ++ toString c ++ "'")) trailingWs

source

def Lean.Parser.rawCh (c : Char) (trailingWs : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.rawCh c trailingWs = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.chFn c trailingWs }

source

def Lean.Parser.hexDigitFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.hexDigitFn c s = let input := c.toInputContext.input; let i := s.pos; if String.atEnd input i = true then Lean.Parser.ParserState.mkEOIError s else let curr := String.get input i; let i := String.next input i; if (Char.isDigit curr || decide (Char.ofNat 97 ≤ curr) && decide (curr ≤ Char.ofNat 102) || decide (Char.ofNat 65 ≤ curr) && decide (curr ≤ Char.ofNat 70)) = true then Lean.Parser.ParserState.setPos s i else Lean.Parser.ParserState.mkUnexpectedError s "invalid hexadecimal numeral"

source

def Lean.Parser.quotedCharCoreFn (isQuotable : Char → Bool) :

Lean.Parser.ParserFn

Equations

Lean.Parser.quotedCharCoreFn isQuotable c s = let input := c.toInputContext.input; let i := s.pos; if String.atEnd input i = true then Lean.Parser.ParserState.mkEOIError s else let curr := String.get input i; if isQuotable curr = true then Lean.Parser.ParserState.next s input i else if (curr == Char.ofNat 120) = true then Lean.Parser.andthenFn Lean.Parser.hexDigitFn Lean.Parser.hexDigitFn c (Lean.Parser.ParserState.next s input i) else if (curr == Char.ofNat 117) = true then Lean.Parser.andthenFn Lean.Parser.hexDigitFn (Lean.Parser.andthenFn Lean.Parser.hexDigitFn (Lean.Parser.andthenFn Lean.Parser.hexDigitFn Lean.Parser.hexDigitFn)) c (Lean.Parser.ParserState.next s input i) else Lean.Parser.ParserState.mkUnexpectedError s "invalid escape sequence"

source

def Lean.Parser.isQuotableCharDefault (c : Char) :

Bool

Equations

Lean.Parser.isQuotableCharDefault c = (c == Char.ofNat 92 || c == Char.ofNat 34 || c == Char.ofNat 39 || c == Char.ofNat 114 || c == Char.ofNat 110 || c == Char.ofNat 116)

source

def Lean.Parser.quotedCharFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.quotedCharFn = Lean.Parser.quotedCharCoreFn Lean.Parser.isQuotableCharDefault

source

def Lean.Parser.mkNodeToken (n : Lean.SyntaxNodeKind) (startPos : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.mkNodeToken n startPos c s = let input := c.toInputContext.input; let stopPos := s.pos; let leading := Lean.Parser.mkEmptySubstringAt input startPos; let val := String.extract input startPos stopPos; let s := Lean.Parser.whitespace c s; let wsStopPos := s.pos; let trailing := { str := input, startPos := stopPos, stopPos := wsStopPos }; let info := Lean.SourceInfo.original leading startPos trailing stopPos; Lean.Parser.ParserState.pushSyntax s (Lean.Syntax.mkLit n val info)

source

def Lean.Parser.charLitFnAux (startPos : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.charLitFnAux startPos c s = let input := c.toInputContext.input; let i := s.pos; if String.atEnd input i = true then Lean.Parser.ParserState.mkEOIError s else let curr := String.get input i; let s := Lean.Parser.ParserState.setPos s (String.next input i); let s := if (curr == Char.ofNat 92) = true then Lean.Parser.quotedCharFn c s else s; if Lean.Parser.ParserState.hasError s = true then s else let i := s.pos; let curr := String.get input i; let s := Lean.Parser.ParserState.setPos s (String.next input i); if (curr == Char.ofNat 39) = true then Lean.Parser.mkNodeToken Lean.charLitKind startPos c s else Lean.Parser.ParserState.mkUnexpectedError s "missing end of character literal"

source

partial def Lean.Parser.strLitFnAux (startPos : Nat) :

Lean.Parser.ParserFn

source

def Lean.Parser.decimalNumberFn (startPos : Nat) (c : Lean.Parser.ParserContext) :

Lean.Parser.ParserState → Lean.Parser.ParserState

Equations

Lean.Parser.decimalNumberFn startPos c = (fun parseOptExp s => let s := Lean.Parser.takeWhileFn (fun c => Char.isDigit c) c s; let input := c.toInputContext.input; let i := s.pos; let curr := String.get input i; if (curr == Char.ofNat 46 || curr == Char.ofNat 101 || curr == Char.ofNat 69) = true then let s := parseOptDot s; let s := parseOptExp s; Lean.Parser.mkNodeToken Lean.scientificLitKind startPos c s else Lean.Parser.mkNodeToken Lean.numLitKind startPos c s) (Lean.Parser.decimalNumberFn.parseOptDot c) (Lean.Parser.decimalNumberFn.parseOptExp c)

source

def Lean.Parser.decimalNumberFn.parseOptDot (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) :

Lean.Parser.ParserState

Equations

Lean.Parser.decimalNumberFn.parseOptDot c s = let input := c.toInputContext.input; let i := s.pos; let curr := String.get input i; if (curr == Char.ofNat 46) = true then let i := String.next input i; let curr := String.get input i; if Char.isDigit curr = true then Lean.Parser.takeWhileFn (fun c => Char.isDigit c) c (Lean.Parser.ParserState.setPos s i) else Lean.Parser.ParserState.setPos s i else s

source

def Lean.Parser.decimalNumberFn.parseOptExp (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) :

Lean.Parser.ParserState

Equations

Lean.Parser.decimalNumberFn.parseOptExp c s = let input := c.toInputContext.input; let i := s.pos; let curr := String.get input i; if (curr == Char.ofNat 101 || curr == Char.ofNat 69) = true then let i := String.next input i; let i := if (String.get input i == Char.ofNat 45) = true then String.next input i else i; let curr := String.get input i; if Char.isDigit curr = true then Lean.Parser.takeWhileFn (fun c => Char.isDigit c) c (Lean.Parser.ParserState.setPos s i) else Lean.Parser.ParserState.setPos s i else s

source

def Lean.Parser.binNumberFn (startPos : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.binNumberFn startPos c s = let s := Lean.Parser.takeWhile1Fn (fun c => c == Char.ofNat 48 || c == Char.ofNat 49) "binary number" c s; Lean.Parser.mkNodeToken Lean.numLitKind startPos c s

source

def Lean.Parser.octalNumberFn (startPos : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.octalNumberFn startPos c s = let s := Lean.Parser.takeWhile1Fn (fun c => decide (Char.ofNat 48 ≤ c) && decide (c ≤ Char.ofNat 55)) "octal number" c s; Lean.Parser.mkNodeToken Lean.numLitKind startPos c s

source

def Lean.Parser.hexNumberFn (startPos : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.hexNumberFn startPos c s = let s := Lean.Parser.takeWhile1Fn (fun c => decide (Char.ofNat 48 ≤ c) && decide (c ≤ Char.ofNat 57) || decide (Char.ofNat 97 ≤ c) && decide (c ≤ Char.ofNat 102) || decide (Char.ofNat 65 ≤ c) && decide (c ≤ Char.ofNat 70)) "hexadecimal number" c s; Lean.Parser.mkNodeToken Lean.numLitKind startPos c s

source

def Lean.Parser.numberFnAux :

Lean.Parser.ParserFn

Equations

Lean.Parser.numberFnAux c s = let input := c.toInputContext.input; let startPos := s.pos; if String.atEnd input startPos = true then Lean.Parser.ParserState.mkEOIError s else let curr := String.get input startPos; if (curr == Char.ofNat 48) = true then let i := String.next input startPos; let curr := String.get input i; if (curr == Char.ofNat 98 || curr == Char.ofNat 66) = true then Lean.Parser.binNumberFn startPos c (Lean.Parser.ParserState.next s input i) else if (curr == Char.ofNat 111 || curr == Char.ofNat 79) = true then Lean.Parser.octalNumberFn startPos c (Lean.Parser.ParserState.next s input i) else if (curr == Char.ofNat 120 || curr == Char.ofNat 88) = true then Lean.Parser.hexNumberFn startPos c (Lean.Parser.ParserState.next s input i) else Lean.Parser.decimalNumberFn startPos c (Lean.Parser.ParserState.setPos s i) else if Char.isDigit curr = true then Lean.Parser.decimalNumberFn startPos c (Lean.Parser.ParserState.next s input startPos) else Lean.Parser.ParserState.mkError s "numeral"

source

def Lean.Parser.isIdCont :

String → Lean.Parser.ParserState → Bool

Equations

Lean.Parser.isIdCont input s = let i := s.pos; let curr := String.get input i; if (curr == Char.ofNat 46) = true then let i := String.next input i; if String.atEnd input i = true then false else let curr := String.get input i; Lean.isIdFirst curr || Lean.isIdBeginEscape curr else false

source

def Lean.Parser.mkTokenAndFixPos (startPos : Nat) (tk : Option Lean.Parser.Token) :

Lean.Parser.ParserFn

Equations

Lean.Parser.mkTokenAndFixPos startPos tk c s = match tk with | none => Lean.Parser.ParserState.mkErrorAt s "token" startPos | some tk => if (c.forbiddenTk? == some tk) = true then Lean.Parser.ParserState.mkErrorAt s "forbidden token" startPos else let input := c.toInputContext.input; let leading := Lean.Parser.mkEmptySubstringAt input startPos; let stopPos := startPos + String.bsize tk; let s := Lean.Parser.ParserState.setPos s stopPos; let s := Lean.Parser.whitespace c s; let wsStopPos := s.pos; let trailing := { str := input, startPos := stopPos, stopPos := wsStopPos }; let atom := Lean.Parser.mkAtom (Lean.SourceInfo.original leading startPos trailing stopPos) tk; Lean.Parser.ParserState.pushSyntax s atom

source

def Lean.Parser.mkIdResult (startPos : Nat) (tk : Option Lean.Parser.Token) (val : Lean.Name) :

Lean.Parser.ParserFn

Equations

Lean.Parser.mkIdResult startPos tk val c s = let stopPos := s.pos; if Lean.Parser.isToken startPos stopPos tk = true then Lean.Parser.mkTokenAndFixPos startPos tk c s else let input := c.toInputContext.input; let rawVal := { str := input, startPos := startPos, stopPos := stopPos }; let s := Lean.Parser.whitespace c s; let trailingStopPos := s.pos; let leading := Lean.Parser.mkEmptySubstringAt input startPos; let trailing := { str := input, startPos := stopPos, stopPos := trailingStopPos }; let info := Lean.SourceInfo.original leading startPos trailing stopPos; let atom := Lean.Parser.mkIdent info rawVal val; Lean.Parser.ParserState.pushSyntax s atom

source

def Lean.Parser.identFnAux (startPos : Nat) (tk : Option Lean.Parser.Token) (r : Lean.Name) :

Lean.Parser.ParserFn

Equations

Lean.Parser.identFnAux startPos tk r = (fun parse => parse r) (Lean.Parser.identFnAux.parse startPos tk)

source

partial def Lean.Parser.identFnAux.parse (startPos : Nat) (tk : Option Lean.Parser.Token) (r : Lean.Name) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) :

Id Lean.Parser.ParserState

source

def Lean.Parser.tokenFn (expected : optParam (List String) []) :

Lean.Parser.ParserFn

Equations

Lean.Parser.tokenFn expected c s = let input := c.toInputContext.input; let i := s.pos; if String.atEnd input i = true then Lean.Parser.ParserState.mkEOIError s expected else let tkc := s.cache.tokenCache; if (tkc.startPos == i) = true then let s := Lean.Parser.ParserState.pushSyntax s tkc.token; Lean.Parser.ParserState.setPos s tkc.stopPos else let s := Lean.Parser.tokenFnAux c s; Lean.Parser.updateCache i s

source

def Lean.Parser.peekTokenAux (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) :

Lean.Parser.ParserState × Except Lean.Parser.ParserState Lean.Syntax

Equations

Lean.Parser.peekTokenAux c s = let iniSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := Lean.Parser.tokenFn [] c s; match s.errorMsg with | some e => (Lean.Parser.ParserState.restore s iniSz iniPos, Except.error s) | x => let stx := Array.back s.stxStack; (Lean.Parser.ParserState.restore s iniSz iniPos, Except.ok stx)

source

def Lean.Parser.peekToken (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) :

Lean.Parser.ParserState × Except Lean.Parser.ParserState Lean.Syntax

Equations

Lean.Parser.peekToken c s = let tkc := s.cache.tokenCache; if (tkc.startPos == s.pos) = true then (s, Except.ok tkc.token) else Lean.Parser.peekTokenAux c s

source

def Lean.Parser.rawIdentFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.rawIdentFn c s = let input := c.toInputContext.input; let i := s.pos; if String.atEnd input i = true then Lean.Parser.ParserState.mkEOIError s else Lean.Parser.identFnAux i none Lean.Name.anonymous c s

source

@[inline]

def Lean.Parser.satisfySymbolFn (p : String → Bool) (expected : List String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.satisfySymbolFn p expected c s = let initStackSz := Lean.Parser.ParserState.stackSize s; let startPos := s.pos; let s := Lean.Parser.tokenFn expected c s; if Lean.Parser.ParserState.hasError s = true then s else match Array.back s.stxStack with | Lean.Syntax.atom x sym => if p sym = true then s else Lean.Parser.ParserState.mkErrorsAt s expected startPos (some initStackSz) | x => Lean.Parser.ParserState.mkErrorsAt s expected startPos (some initStackSz)

source

def Lean.Parser.symbolFnAux (sym : String) (errorMsg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.symbolFnAux sym errorMsg = Lean.Parser.satisfySymbolFn (fun s => s == sym) [errorMsg]

source

def Lean.Parser.symbolInfo (sym : String) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.symbolInfo sym = { collectTokens := fun tks => sym :: tks, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.tokens [sym] }

source

@[inline]

def Lean.Parser.symbolFn (sym : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.symbolFn sym = Lean.Parser.symbolFnAux sym ("'" ++ sym ++ "'")

source

@[inline]

def Lean.Parser.symbolNoAntiquot (sym : String) :

Lean.Parser.Parser

Equations

Lean.Parser.symbolNoAntiquot sym = let sym := String.trim sym; { info := Lean.Parser.symbolInfo sym, fn := Lean.Parser.symbolFn sym }

source

def Lean.Parser.checkTailNoWs (prev : Lean.Syntax) :

Bool

Equations

Lean.Parser.checkTailNoWs prev = match Lean.Syntax.getTailInfo prev with | Lean.SourceInfo.original x x_1 trailing x_2 => trailing.stopPos == trailing.startPos | x => false

source

def Lean.Parser.nonReservedSymbolFnAux (sym : String) (errorMsg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.nonReservedSymbolFnAux sym errorMsg c s = let initStackSz := Lean.Parser.ParserState.stackSize s; let startPos := s.pos; let s := Lean.Parser.tokenFn [errorMsg] c s; if Lean.Parser.ParserState.hasError s = true then s else match Array.back s.stxStack with | Lean.Syntax.atom x sym' => if (sym == sym') = true then s else Lean.Parser.ParserState.mkErrorAt s errorMsg startPos (some initStackSz) | Lean.Syntax.ident info rawVal x x_1 => if (sym == Substring.toString rawVal) = true then let s := Lean.Parser.ParserState.popSyntax s; Lean.Parser.ParserState.pushSyntax s (Lean.Syntax.atom info sym) else Lean.Parser.ParserState.mkErrorAt s errorMsg startPos (some initStackSz) | x => Lean.Parser.ParserState.mkErrorAt s errorMsg startPos (some initStackSz)

source

@[inline]

def Lean.Parser.nonReservedSymbolFn (sym : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.nonReservedSymbolFn sym = Lean.Parser.nonReservedSymbolFnAux sym ("'" ++ sym ++ "'")

source

def Lean.Parser.nonReservedSymbolInfo (sym : String) (includeIdent : Bool) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.nonReservedSymbolInfo sym includeIdent = { collectTokens := id, collectKinds := id, firstTokens := if includeIdent = true then Lean.Parser.FirstTokens.tokens [sym, "ident"] else Lean.Parser.FirstTokens.tokens [sym] }

source

@[inline]

def Lean.Parser.nonReservedSymbolNoAntiquot (sym : String) (includeIdent : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.nonReservedSymbolNoAntiquot sym includeIdent = let sym := String.trim sym; { info := Lean.Parser.nonReservedSymbolInfo sym includeIdent, fn := Lean.Parser.nonReservedSymbolFn sym }

source

def Lean.Parser.strAux (sym : String) (errorMsg : String) (j : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.strAux sym errorMsg j = (fun parse => parse j) (Lean.Parser.strAux.parse sym errorMsg)

source

partial def Lean.Parser.strAux.parse (sym : String) (errorMsg : String) (j : String.Pos) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) :

Lean.Parser.ParserState

source

def Lean.Parser.checkTailWs (prev : Lean.Syntax) :

Bool

Equations

Lean.Parser.checkTailWs prev = match Lean.Syntax.getTailInfo prev with | Lean.SourceInfo.original x x_1 trailing x_2 => decide (trailing.stopPos > trailing.startPos) | x => false

source

def Lean.Parser.checkWsBeforeFn (errorMsg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkWsBeforeFn errorMsg c s = let prev := Array.back s.stxStack; if Lean.Parser.checkTailWs prev = true then s else Lean.Parser.ParserState.mkError s errorMsg

source

def Lean.Parser.checkWsBefore (errorMsg : optParam String "space before") :

Lean.Parser.Parser

Equations

Lean.Parser.checkWsBefore errorMsg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkWsBeforeFn errorMsg }

source

def Lean.Parser.checkTailLinebreak (prev : Lean.Syntax) :

Bool

Equations

Lean.Parser.checkTailLinebreak prev = match Lean.Syntax.getTailInfo prev with | Lean.SourceInfo.original x x_1 trailing x_2 => Substring.contains trailing (Char.ofNat 10) | x => false

source

def Lean.Parser.checkLinebreakBeforeFn (errorMsg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkLinebreakBeforeFn errorMsg c s = let prev := Array.back s.stxStack; if Lean.Parser.checkTailLinebreak prev = true then s else Lean.Parser.ParserState.mkError s errorMsg

source

def Lean.Parser.checkLinebreakBefore (errorMsg : optParam String "line break") :

Lean.Parser.Parser

Equations

Lean.Parser.checkLinebreakBefore errorMsg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkLinebreakBeforeFn errorMsg }

source

def Lean.Parser.checkNoWsBeforeFn (errorMsg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkNoWsBeforeFn errorMsg c s = let prev := Lean.Parser.pickNonNone s.stxStack; if Lean.Parser.checkTailNoWs prev = true then s else Lean.Parser.ParserState.mkError s errorMsg

source

def Lean.Parser.checkNoWsBefore (errorMsg : optParam String "no space before") :

Lean.Parser.Parser

Equations

Lean.Parser.checkNoWsBefore errorMsg = { info := Lean.Parser.epsilonInfo, fn := Lean.Parser.checkNoWsBeforeFn errorMsg }

source

def Lean.Parser.unicodeSymbolFnAux (sym : String) (asciiSym : String) (expected : List String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.unicodeSymbolFnAux sym asciiSym expected = Lean.Parser.satisfySymbolFn (fun s => s == sym || s == asciiSym) expected

source

def Lean.Parser.unicodeSymbolInfo (sym : String) (asciiSym : String) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.unicodeSymbolInfo sym asciiSym = { collectTokens := fun tks => sym :: asciiSym :: tks, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.tokens [sym, asciiSym] }

source

@[inline]

def Lean.Parser.unicodeSymbolFn (sym : String) (asciiSym : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.unicodeSymbolFn sym asciiSym = Lean.Parser.unicodeSymbolFnAux sym asciiSym ["'" ++ sym ++ "', '" ++ asciiSym ++ "'"]

source

@[inline]

def Lean.Parser.unicodeSymbolNoAntiquot (sym : String) (asciiSym : String) :

Lean.Parser.Parser

Equations

Lean.Parser.unicodeSymbolNoAntiquot sym asciiSym = let sym := String.trim sym; let asciiSym := String.trim asciiSym; { info := Lean.Parser.unicodeSymbolInfo sym asciiSym, fn := Lean.Parser.unicodeSymbolFn sym asciiSym }

source

def Lean.Parser.mkAtomicInfo (k : String) :

Lean.Parser.ParserInfo

Equations

Lean.Parser.mkAtomicInfo k = { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.tokens [k] }

source

def Lean.Parser.numLitFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.numLitFn c s = let initStackSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := Lean.Parser.tokenFn ["numeral"] c s; if (!Lean.Parser.ParserState.hasError s && !Lean.Syntax.isOfKind (Array.back s.stxStack) Lean.numLitKind) = true then Lean.Parser.ParserState.mkErrorAt s "numeral" iniPos (some initStackSz) else s

source

@[inline]

def Lean.Parser.numLitNoAntiquot :

Lean.Parser.Parser

Equations

Lean.Parser.numLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "numLit", fn := Lean.Parser.numLitFn }

source

def Lean.Parser.scientificLitFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.scientificLitFn c s = let initStackSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := Lean.Parser.tokenFn ["scientific number"] c s; if (!Lean.Parser.ParserState.hasError s && !Lean.Syntax.isOfKind (Array.back s.stxStack) Lean.scientificLitKind) = true then Lean.Parser.ParserState.mkErrorAt s "scientific number" iniPos (some initStackSz) else s

source

@[inline]

def Lean.Parser.scientificLitNoAntiquot :

Lean.Parser.Parser

Equations

Lean.Parser.scientificLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "scientificLit", fn := Lean.Parser.scientificLitFn }

source

def Lean.Parser.strLitFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.strLitFn c s = let initStackSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := Lean.Parser.tokenFn ["string literal"] c s; if (!Lean.Parser.ParserState.hasError s && !Lean.Syntax.isOfKind (Array.back s.stxStack) Lean.strLitKind) = true then Lean.Parser.ParserState.mkErrorAt s "string literal" iniPos (some initStackSz) else s

source

@[inline]

def Lean.Parser.strLitNoAntiquot :

Lean.Parser.Parser

Equations

Lean.Parser.strLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "strLit", fn := Lean.Parser.strLitFn }

source

def Lean.Parser.charLitFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.charLitFn c s = let initStackSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := Lean.Parser.tokenFn ["char literal"] c s; if (!Lean.Parser.ParserState.hasError s && !Lean.Syntax.isOfKind (Array.back s.stxStack) Lean.charLitKind) = true then Lean.Parser.ParserState.mkErrorAt s "character literal" iniPos (some initStackSz) else s

source

@[inline]

def Lean.Parser.charLitNoAntiquot :

Lean.Parser.Parser

Equations

Lean.Parser.charLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "charLit", fn := Lean.Parser.charLitFn }

source

def Lean.Parser.nameLitFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.nameLitFn c s = let initStackSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := Lean.Parser.tokenFn ["Name literal"] c s; if (!Lean.Parser.ParserState.hasError s && !Lean.Syntax.isOfKind (Array.back s.stxStack) Lean.nameLitKind) = true then Lean.Parser.ParserState.mkErrorAt s "Name literal" iniPos (some initStackSz) else s

source

@[inline]

def Lean.Parser.nameLitNoAntiquot :

Lean.Parser.Parser

Equations

Lean.Parser.nameLitNoAntiquot = { info := Lean.Parser.mkAtomicInfo "nameLit", fn := Lean.Parser.nameLitFn }

source

def Lean.Parser.identFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.identFn c s = let initStackSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := Lean.Parser.tokenFn ["identifier"] c s; if (!Lean.Parser.ParserState.hasError s && !Lean.Syntax.isIdent (Array.back s.stxStack)) = true then Lean.Parser.ParserState.mkErrorAt s "identifier" iniPos (some initStackSz) else s

source

@[inline]

def Lean.Parser.identNoAntiquot :

Lean.Parser.Parser

Equations

Lean.Parser.identNoAntiquot = { info := Lean.Parser.mkAtomicInfo "ident", fn := Lean.Parser.identFn }

source

@[inline]

def Lean.Parser.rawIdentNoAntiquot :

Lean.Parser.Parser

Equations

Lean.Parser.rawIdentNoAntiquot = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.rawIdentFn }

source

def Lean.Parser.identEqFn (id : Lean.Name) :

Lean.Parser.ParserFn

Equations

Lean.Parser.identEqFn id c s = let initStackSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := Lean.Parser.tokenFn ["identifier"] c s; if Lean.Parser.ParserState.hasError s = true then s else match Array.back s.stxStack with | Lean.Syntax.ident x x_1 val x_2 => if (val != id) = true then Lean.Parser.ParserState.mkErrorAt s ("expected identifier '" ++ toString id ++ "'") iniPos (some initStackSz) else s | x => Lean.Parser.ParserState.mkErrorAt s "identifier" iniPos (some initStackSz)

source

@[inline]

def Lean.Parser.identEq (id : Lean.Name) :

Lean.Parser.Parser

Equations

Lean.Parser.identEq id = { info := Lean.Parser.mkAtomicInfo "ident", fn := Lean.Parser.identEqFn id }

source

def Lean.Parser.ParserState.keepTop (s : Array Lean.Syntax) (startStackSize : Nat) :

Array Lean.Syntax

Equations

Lean.Parser.ParserState.keepTop s startStackSize = let node := Array.back s; Array.push (Array.shrink s startStackSize) node

source

def Lean.Parser.ParserState.keepNewError (s : Lean.Parser.ParserState) (oldStackSize : Nat) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.keepNewError s oldStackSize = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := err } => { stxStack := Lean.Parser.ParserState.keepTop stack oldStackSize, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := err }

source

def Lean.Parser.ParserState.keepPrevError (s : Lean.Parser.ParserState) (oldStackSize : Nat) (oldStopPos : String.Pos) (oldError : Option Lean.Parser.Error) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.keepPrevError s oldStackSize oldStopPos oldError = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := x, cache := cache, errorMsg := x_1 } => { stxStack := Array.shrink stack oldStackSize, lhsPrec := lhsPrec, pos := oldStopPos, cache := cache, errorMsg := oldError }

source

def Lean.Parser.ParserState.mergeErrors (s : Lean.Parser.ParserState) (oldStackSize : Nat) (oldError : Lean.Parser.Error) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.mergeErrors s oldStackSize oldError = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some err } => if (oldError == err) = true then s else { stxStack := Array.shrink stack oldStackSize, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := some (Lean.Parser.Error.merge oldError err) } | other => other

source

def Lean.Parser.ParserState.keepLatest (s : Lean.Parser.ParserState) (startStackSize : Nat) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.keepLatest s startStackSize = match s with | { stxStack := stack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := x } => { stxStack := Lean.Parser.ParserState.keepTop stack startStackSize, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := none }

source

def Lean.Parser.ParserState.replaceLongest (s : Lean.Parser.ParserState) (startStackSize : Nat) :

Lean.Parser.ParserState

Equations

Lean.Parser.ParserState.replaceLongest s startStackSize = Lean.Parser.ParserState.keepLatest s startStackSize

source

def Lean.Parser.invalidLongestMatchParser (s : Lean.Parser.ParserState) :

Lean.Parser.ParserState

Equations

Lean.Parser.invalidLongestMatchParser s = Lean.Parser.ParserState.mkError s "longestMatch parsers must generate exactly one Syntax node"

source

def Lean.Parser.runLongestMatchParser (left? : Option Lean.Syntax) (startLhsPrec : Nat) (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.runLongestMatchParser left? startLhsPrec p c s = Id.run (let s := { stxStack := s.stxStack, lhsPrec := if Option.isSome left? = true then startLhsPrec else Lean.Parser.maxPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg }; let startSize := Lean.Parser.ParserState.stackSize s; let _do_jp := fun s y => let s := p c s; if (Lean.Parser.ParserState.stackSize s == startSize + 1) = true then s else if Lean.Parser.ParserState.hasError s = true then Lean.Parser.ParserState.pushSyntax (Lean.Parser.ParserState.shrinkStack s startSize) Lean.Syntax.missing else Lean.Parser.invalidLongestMatchParser s; match left? with | some left => let s := Lean.Parser.ParserState.pushSyntax s left; do let y ← pure PUnit.unit _do_jp s y | x => do let y ← pure PUnit.unit _do_jp s y)

source

def Lean.Parser.longestMatchStep (left? : Option Lean.Syntax) (startSize : Nat) (startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (prio : Nat) (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState × Nat

Equations

Lean.Parser.longestMatchStep left? startSize startLhsPrec startPos prevPrio prio p c s = let prevErrorMsg := s.errorMsg; let prevStopPos := s.pos; let prevSize := Lean.Parser.ParserState.stackSize s; let prevLhsPrec := s.lhsPrec; let s := Lean.Parser.ParserState.restore s prevSize startPos; let s := Lean.Parser.runLongestMatchParser left? startLhsPrec p c s; match prevErrorMsg, s.errorMsg with | none, none => if (decide (s.pos > prevStopPos) || s.pos == prevStopPos && decide (prio > prevPrio)) = true then (Lean.Parser.ParserState.replaceLongest s startSize, prio) else if (decide (s.pos < prevStopPos) || s.pos == prevStopPos && decide (prio < prevPrio)) = true then (let src := Lean.Parser.ParserState.restore s prevSize prevStopPos; { stxStack := src.stxStack, lhsPrec := prevLhsPrec, pos := src.pos, cache := src.cache, errorMsg := src.errorMsg }, prevPrio) else ({ stxStack := s.stxStack, lhsPrec := Nat.min s.lhsPrec prevLhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg }, prio) | none, some x => (let src := Lean.Parser.ParserState.restore s prevSize prevStopPos; { stxStack := src.stxStack, lhsPrec := prevLhsPrec, pos := src.pos, cache := src.cache, errorMsg := src.errorMsg }, prevPrio) | some oldError, some x => if (decide (s.pos > prevStopPos) || s.pos == prevStopPos && decide (prio > prevPrio)) = true then (Lean.Parser.ParserState.keepNewError s startSize, prio) else if (decide (s.pos < prevStopPos) || s.pos == prevStopPos && decide (prio < prevPrio)) = true then (Lean.Parser.ParserState.keepPrevError s prevSize prevStopPos prevErrorMsg, prevPrio) else (Lean.Parser.ParserState.mergeErrors s prevSize oldError, prio) | some x, none => let successNode := Array.back s.stxStack; let s := Lean.Parser.ParserState.shrinkStack s startSize; (Lean.Parser.ParserState.pushSyntax s successNode, prio)

source

def Lean.Parser.longestMatchMkResult (startSize : Nat) (s : Lean.Parser.ParserState) :

Lean.Parser.ParserState

Equations

Lean.Parser.longestMatchMkResult startSize s = if Lean.Parser.ParserState.stackSize s > startSize + 1 then Lean.Parser.ParserState.mkNode s Lean.choiceKind startSize else s

source

def Lean.Parser.longestMatchFnAux (left? : Option Lean.Syntax) (startSize : Nat) (startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (ps : List (Lean.Parser.Parser × Nat)) :

Lean.Parser.ParserFn

Equations

Lean.Parser.longestMatchFnAux left? startSize startLhsPrec startPos prevPrio ps = (fun parse => parse prevPrio ps) (Lean.Parser.longestMatchFnAux.parse left? startSize startLhsPrec startPos)

source

def Lean.Parser.longestMatchFnAux.parse (left? : Option Lean.Syntax) (startSize : Nat) (startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (ps : List (Lean.Parser.Parser × Nat)) :

Lean.Parser.ParserFn

Equations

Lean.Parser.longestMatchFnAux.parse left? startSize startLhsPrec startPos prevPrio [] = fun x s => Lean.Parser.longestMatchMkResult startSize s
Lean.Parser.longestMatchFnAux.parse left? startSize startLhsPrec startPos prevPrio (p :: ps_2) x x_1 = Lean.Parser.longestMatchFnAux.parse left? startSize startLhsPrec startPos (Lean.Parser.longestMatchStep left? startSize startLhsPrec startPos prevPrio p.snd p.fst.fn x x_1).2 ps_2 x (Lean.Parser.longestMatchStep left? startSize startLhsPrec startPos prevPrio p.snd p.fst.fn x x_1).1

source

def Lean.Parser.longestMatchFn (left? : Option Lean.Syntax) :

List (Lean.Parser.Parser × Nat) → Lean.Parser.ParserFn

Equations

Lean.Parser.longestMatchFn left? x = match x with | [] => fun x s => Lean.Parser.ParserState.mkError s "longestMatch: empty list" | [p] => fun c s => Lean.Parser.runLongestMatchParser left? s.lhsPrec p.fst.fn c s | p :: ps => fun c s => let startSize := Lean.Parser.ParserState.stackSize s; let startLhsPrec := s.lhsPrec; let startPos := s.pos; let s := Lean.Parser.runLongestMatchParser left? s.lhsPrec p.fst.fn c s; Lean.Parser.longestMatchFnAux left? startSize startLhsPrec startPos p.snd ps c s

source

def Lean.Parser.anyOfFn :

List Lean.Parser.Parser → Lean.Parser.ParserFn

Equations

Lean.Parser.anyOfFn [] x x = Lean.Parser.ParserState.mkError x "anyOf: empty list"
Lean.Parser.anyOfFn [p] x x = Lean.Parser.Parser.fn p x x
Lean.Parser.anyOfFn (p :: ps) x x = Lean.Parser.orelseFn p.fn (Lean.Parser.anyOfFn ps) x x

source

@[inline]

def Lean.Parser.checkColGeFn (errorMsg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkColGeFn errorMsg c s = match c.savedPos? with | none => s | some savedPos => let savedPos := Lean.FileMap.toPosition c.toInputContext.fileMap savedPos; let pos := Lean.FileMap.toPosition c.toInputContext.fileMap s.pos; if pos.column ≥ savedPos.column then s else Lean.Parser.ParserState.mkError s errorMsg

source

@[inline]

def Lean.Parser.checkColGe (errorMsg : optParam String "checkColGe") :

Lean.Parser.Parser

Equations

Lean.Parser.checkColGe errorMsg = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.checkColGeFn errorMsg }

source

@[inline]

def Lean.Parser.checkColGtFn (errorMsg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkColGtFn errorMsg c s = match c.savedPos? with | none => s | some savedPos => let savedPos := Lean.FileMap.toPosition c.toInputContext.fileMap savedPos; let pos := Lean.FileMap.toPosition c.toInputContext.fileMap s.pos; if pos.column > savedPos.column then s else Lean.Parser.ParserState.mkError s errorMsg

source

@[inline]

def Lean.Parser.checkColGt (errorMsg : optParam String "checkColGt") :

Lean.Parser.Parser

Equations

Lean.Parser.checkColGt errorMsg = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.checkColGtFn errorMsg }

source

@[inline]

def Lean.Parser.checkLineEqFn (errorMsg : String) :

Lean.Parser.ParserFn

Equations

Lean.Parser.checkLineEqFn errorMsg c s = match c.savedPos? with | none => s | some savedPos => let savedPos := Lean.FileMap.toPosition c.toInputContext.fileMap savedPos; let pos := Lean.FileMap.toPosition c.toInputContext.fileMap s.pos; if (pos.line == savedPos.line) = true then s else Lean.Parser.ParserState.mkError s errorMsg

source

@[inline]

def Lean.Parser.checkLineEq (errorMsg : optParam String "checkLineEq") :

Lean.Parser.Parser

Equations

Lean.Parser.checkLineEq errorMsg = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.checkLineEqFn errorMsg }

source

@[inline]

def Lean.Parser.withPosition (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withPosition p = { info := p.info, fn := fun c s => Lean.Parser.Parser.fn p { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := c.prec, tokens := c.tokens, quotDepth := c.quotDepth, suppressInsideQuot := c.suppressInsideQuot, savedPos? := some s.pos, forbiddenTk? := c.forbiddenTk? } s }

source

@[inline]

def Lean.Parser.withoutPosition (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withoutPosition p = { info := p.info, fn := fun c s => let pos := Lean.FileMap.toPosition c.toInputContext.fileMap s.pos; Lean.Parser.Parser.fn p { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := c.prec, tokens := c.tokens, quotDepth := c.quotDepth, suppressInsideQuot := c.suppressInsideQuot, savedPos? := none, forbiddenTk? := c.forbiddenTk? } s }

source

@[inline]

def Lean.Parser.withForbidden (tk : Lean.Parser.Token) (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withForbidden tk p = { info := p.info, fn := fun c s => Lean.Parser.Parser.fn p { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := c.prec, tokens := c.tokens, quotDepth := c.quotDepth, suppressInsideQuot := c.suppressInsideQuot, savedPos? := c.savedPos?, forbiddenTk? := some tk } s }

source

@[inline]

def Lean.Parser.withoutForbidden (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withoutForbidden p = { info := p.info, fn := fun c s => Lean.Parser.Parser.fn p { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := c.prec, tokens := c.tokens, quotDepth := c.quotDepth, suppressInsideQuot := c.suppressInsideQuot, savedPos? := c.savedPos?, forbiddenTk? := none } s }

source

def Lean.Parser.eoiFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.eoiFn c s = let i := s.pos; if String.atEnd c.toInputContext.input i = true then s else Lean.Parser.ParserState.mkError s "expected end of file"

source

@[inline]

def Lean.Parser.eoi :

Lean.Parser.Parser

Equations

Lean.Parser.eoi = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.eoiFn }

source

noncomputable def Lean.Parser.TokenMap (α : Type) :

Type

Equations

Lean.Parser.TokenMap α = Std.RBMap Lean.Name (List α) Lean.Name.quickCmp

source

def Lean.Parser.TokenMap.insert {α : Type} (map : Lean.Parser.TokenMap α) (k : Lean.Name) (v : α) :

Lean.Parser.TokenMap α

Equations

Lean.Parser.TokenMap.insert map k v = match Std.RBMap.find? map k with | none => Std.RBMap.insert map k [v] | some vs => Std.RBMap.insert map k (v :: vs)

source

instance Lean.Parser.TokenMap.instInhabitedTokenMap {α : Type} :

Inhabited (Lean.Parser.TokenMap α)

Equations

Lean.Parser.TokenMap.instInhabitedTokenMap = { default := Std.RBMap.empty }

source

instance Lean.Parser.TokenMap.instEmptyCollectionTokenMap {α : Type} :

EmptyCollection (Lean.Parser.TokenMap α)

Equations

Lean.Parser.TokenMap.instEmptyCollectionTokenMap = { emptyCollection := Std.RBMap.empty }

source

structure Lean.Parser.PrattParsingTables :

Type

leadingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × Nat)
leadingParsers : List (Lean.Parser.Parser × Nat)
trailingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × Nat)
trailingParsers : List (Lean.Parser.Parser × Nat)

source

instance Lean.Parser.instInhabitedPrattParsingTables :

Inhabited Lean.Parser.PrattParsingTables

Equations

Lean.Parser.instInhabitedPrattParsingTables = { default := { leadingTable := ∅, leadingParsers := [], trailingTable := ∅, trailingParsers := [] } }

source

inductive Lean.Parser.LeadingIdentBehavior :

Type

default: Lean.Parser.LeadingIdentBehavior
symbol: Lean.Parser.LeadingIdentBehavior
both: Lean.Parser.LeadingIdentBehavior

source

instance Lean.Parser.instBEqLeadingIdentBehavior :

BEq Lean.Parser.LeadingIdentBehavior

Equations

Lean.Parser.instBEqLeadingIdentBehavior = { beq := [anonymous] }

source

instance Lean.Parser.instReprLeadingIdentBehavior :

Repr Lean.Parser.LeadingIdentBehavior

Equations

Lean.Parser.instReprLeadingIdentBehavior = { reprPrec := [anonymous] }

source

instance Lean.Parser.instInhabitedLeadingIdentBehavior :

Inhabited Lean.Parser.LeadingIdentBehavior

Equations

Lean.Parser.instInhabitedLeadingIdentBehavior = { default := Lean.Parser.LeadingIdentBehavior.default }

source

structure Lean.Parser.ParserCategory :

Type

tables : Lean.Parser.PrattParsingTables
behavior : Lean.Parser.LeadingIdentBehavior

source

instance Lean.Parser.instInhabitedParserCategory :

Inhabited Lean.Parser.ParserCategory

Equations

Lean.Parser.instInhabitedParserCategory = { default := { tables := default, behavior := default } }

source

@[inline]

abbrev Lean.Parser.ParserCategories :

Type

Equations

Lean.Parser.ParserCategories = Std.PersistentHashMap Lean.Name Lean.Parser.ParserCategory

source

def Lean.Parser.indexed {α : Type} (map : Lean.Parser.TokenMap α) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) (behavior : Lean.Parser.LeadingIdentBehavior) :

Lean.Parser.ParserState × List α

Equations

Lean.Parser.indexed map c s behavior = let x := Lean.Parser.peekToken c s; match x with | (s, stx) => let find := fun n => match Std.RBMap.find? map n with | some as => (s, as) | x => (s, []); match stx with | Except.ok (Lean.Syntax.atom x sym) => find (Lean.Name.mkSimple sym) | Except.ok (Lean.Syntax.ident x x_1 val x_2) => match behavior with | Lean.Parser.LeadingIdentBehavior.default => find Lean.identKind | Lean.Parser.LeadingIdentBehavior.symbol => match Std.RBMap.find? map val with | some as => (s, as) | none => find Lean.identKind | Lean.Parser.LeadingIdentBehavior.both => match Std.RBMap.find? map val with | some as => match Std.RBMap.find? map Lean.identKind with | some as' => (s, as ++ as') | x => (s, as) | none => find Lean.identKind | Except.ok (Lean.Syntax.node x k x_1) => find k | Except.ok x => (s, []) | Except.error s' => (s', [])

source

@[inline]

abbrev Lean.Parser.CategoryParserFn :

Type

Equations

Lean.Parser.CategoryParserFn = (Lean.Name → Lean.Parser.ParserFn)

source

constant Lean.Parser.categoryParserFnRef :

IO.Ref Lean.Parser.CategoryParserFn

source

constant Lean.Parser.categoryParserFnExtension :

Lean.EnvExtension Lean.Parser.CategoryParserFn

source

def Lean.Parser.categoryParserFn (catName : Lean.Name) :

Lean.Parser.ParserFn

Equations

Lean.Parser.categoryParserFn catName ctx s = Lean.EnvExtension.getState Lean.Parser.categoryParserFnExtension ctx.toParserModuleContext.env catName ctx s

source

def Lean.Parser.categoryParser (catName : Lean.Name) (prec : Nat) :

Lean.Parser.Parser

Equations

Lean.Parser.categoryParser catName prec = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := fun c s => Lean.Parser.categoryParserFn catName { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := prec, tokens := c.tokens, quotDepth := c.quotDepth, suppressInsideQuot := c.suppressInsideQuot, savedPos? := c.savedPos?, forbiddenTk? := c.forbiddenTk? } s }

source

@[inline]

def Lean.Parser.termParser (prec : optParam Nat 0) :

Lean.Parser.Parser

Equations

Lean.Parser.termParser prec = Lean.Parser.categoryParser `term prec

source

def Lean.Parser.checkNoImmediateColon :

Lean.Parser.Parser

Equations

Lean.Parser.checkNoImmediateColon = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := fun c s => let prev := Array.back s.stxStack; if Lean.Parser.checkTailNoWs prev = true then let input := c.toInputContext.input; let i := s.pos; if String.atEnd input i = true then s else let curr := String.get input i; if (curr == Char.ofNat 58) = true then Lean.Parser.ParserState.mkUnexpectedError s "unexpected ':'" else s else s }

source

def Lean.Parser.setExpectedFn (expected : List String) (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.setExpectedFn expected p c s = match p c s with | s'@h:{ stxStack := x, lhsPrec := x_1, pos := x_2, cache := x_3, errorMsg := some msg } => { stxStack := s'.stxStack, lhsPrec := s'.lhsPrec, pos := s'.pos, cache := s'.cache, errorMsg := some { unexpected := msg.unexpected, expected := [] } } | s' => s'

source

def Lean.Parser.setExpected (expected : List String) (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.setExpected expected p = { info := p.info, fn := Lean.Parser.setExpectedFn expected p.fn }

source

def Lean.Parser.pushNone :

Lean.Parser.Parser

Equations

Lean.Parser.pushNone = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := fun c s => Lean.Parser.ParserState.pushSyntax s Lean.mkNullNode }

source

def Lean.Parser.antiquotNestedExpr :

Lean.Parser.Parser

Equations

Lean.Parser.antiquotNestedExpr = Lean.Parser.node `antiquotNestedExpr (HAndThen.hAndThen (Lean.Parser.symbolNoAntiquot "(") fun x => HAndThen.hAndThen (Lean.Parser.decQuotDepth Lean.Parser.termParser) fun x => Lean.Parser.symbolNoAntiquot ")")

source

def Lean.Parser.antiquotExpr :

Lean.Parser.Parser

Equations

Lean.Parser.antiquotExpr = HOrElse.hOrElse Lean.Parser.identNoAntiquot fun x => Lean.Parser.antiquotNestedExpr

source

@[inline]

def Lean.Parser.tokenWithAntiquotFn (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.tokenWithAntiquotFn p c s = Id.run (let s := p c s; let _do_jp := fun y => let iniSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := Lean.Parser.Parser.fn (HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => HAndThen.hAndThen (Lean.Parser.symbolNoAntiquot "%") fun x => HAndThen.hAndThen (Lean.Parser.symbolNoAntiquot "$") fun x => HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => Lean.Parser.antiquotExpr) c s; let _do_jp := fun y => Lean.Parser.ParserState.mkNode s `token_antiquot (iniSz - 1); if Lean.Parser.ParserState.hasError s = true then pure (Lean.Parser.ParserState.restore s iniSz iniPos) else do let y ← pure PUnit.unit _do_jp y; if (Lean.Parser.ParserState.hasError s || c.quotDepth == 0) = true then pure s else do let y ← pure PUnit.unit _do_jp y)

source

@[inline]

def Lean.Parser.tokenWithAntiquot (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.tokenWithAntiquot p = { info := p.info, fn := Lean.Parser.tokenWithAntiquotFn p.fn }

source

@[inline]

def Lean.Parser.symbol (sym : String) :

Lean.Parser.Parser

Equations

Lean.Parser.symbol sym = Lean.Parser.tokenWithAntiquot (Lean.Parser.symbolNoAntiquot sym)

source

instance Lean.Parser.instCoeStringParser :

Coe String Lean.Parser.Parser

Equations

Lean.Parser.instCoeStringParser = { coe := fun s => Lean.Parser.symbol s }

source

@[inline]

def Lean.Parser.nonReservedSymbol (sym : String) (includeIdent : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.nonReservedSymbol sym includeIdent = Lean.Parser.tokenWithAntiquot (Lean.Parser.nonReservedSymbolNoAntiquot sym includeIdent)

source

@[inline]

def Lean.Parser.unicodeSymbol (sym : String) (asciiSym : String) :

Lean.Parser.Parser

Equations

Lean.Parser.unicodeSymbol sym asciiSym = Lean.Parser.tokenWithAntiquot (Lean.Parser.unicodeSymbolNoAntiquot sym asciiSym)

source

def Lean.Parser.mkAntiquot (name : String) (kind : Option Lean.SyntaxNodeKind) (anonymous : optParam Bool true) :

Lean.Parser.Parser

Equations

Lean.Parser.mkAntiquot name kind anonymous = let kind := Option.getD kind Lean.Name.anonymous ++ `antiquot; let nameP := Lean.Parser.node `antiquotName (HAndThen.hAndThen (Lean.Parser.checkNoWsBefore ("no space before ':" ++ name ++ "'")) fun x => HAndThen.hAndThen (Lean.Parser.symbol ":") fun x => Lean.Parser.nonReservedSymbol name); let nameP := if anonymous = true then HOrElse.hOrElse nameP fun x => HAndThen.hAndThen Lean.Parser.checkNoImmediateColon fun x => Lean.Parser.pushNone else nameP; Lean.Parser.leadingNode kind Lean.Parser.maxPrec (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.setExpected [] (Lean.Parser.symbol "$")) fun x => HAndThen.hAndThen (Lean.Parser.manyNoAntiquot (HAndThen.hAndThen (Lean.Parser.checkNoWsBefore "") fun x => Lean.Parser.symbol "$")) fun x => HAndThen.hAndThen (Lean.Parser.checkNoWsBefore "no space before spliced term") fun x => HAndThen.hAndThen Lean.Parser.antiquotExpr fun x => nameP))

source

def Lean.Parser.tryAnti (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) :

Bool

Equations

Lean.Parser.tryAnti c s = Id.run (let _do_jp := fun y => let x := Lean.Parser.peekToken c s; match x with | (s, stx) => match stx with | Except.ok stx@h:(Lean.Syntax.atom x sym) => sym == "$" | x => false; if (c.quotDepth == 0) = true then pure false else do let y ← pure PUnit.unit _do_jp y)

source

@[inline]

def Lean.Parser.withAntiquotFn (antiquotP : Lean.Parser.ParserFn) (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.withAntiquotFn antiquotP p c s = if Lean.Parser.tryAnti c s = true then Lean.Parser.orelseFn antiquotP p c s else p c s

source

@[inline]

def Lean.Parser.withAntiquot (antiquotP : Lean.Parser.Parser) (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withAntiquot antiquotP p = { info := Lean.Parser.orelseInfo antiquotP.info p.info, fn := Lean.Parser.withAntiquotFn antiquotP.fn p.fn }

source

def Lean.Parser.withoutInfo (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withoutInfo p = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := p.fn }

source

def Lean.Parser.mkAntiquotSplice (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) (suffix : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.mkAntiquotSplice kind p suffix = let kind := kind ++ `antiquot_scope; Lean.Parser.leadingNode kind Lean.Parser.maxPrec (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.setExpected [] (Lean.Parser.symbol "$")) fun x => HAndThen.hAndThen (Lean.Parser.manyNoAntiquot (HAndThen.hAndThen (Lean.Parser.checkNoWsBefore "") fun x => Lean.Parser.symbol "$")) fun x => HAndThen.hAndThen (Lean.Parser.checkNoWsBefore "no space before spliced term") fun x => HAndThen.hAndThen (Lean.Parser.symbol "[") fun x => HAndThen.hAndThen (Lean.Parser.node Lean.nullKind p) fun x => HAndThen.hAndThen (Lean.Parser.symbol "]") fun x => suffix))

source

@[inline]

def Lean.Parser.withAntiquotSuffixSpliceFn (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.ParserFn) (suffix : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.withAntiquotSuffixSpliceFn kind p suffix c s = Id.run (let s := p c s; let _do_jp := fun y => let iniSz := Lean.Parser.ParserState.stackSize s; let iniPos := s.pos; let s := suffix c s; let _do_jp := fun y => Lean.Parser.ParserState.mkNode s (kind ++ `antiquot_suffix_splice) (Array.size s.stxStack - 2); if Lean.Parser.ParserState.hasError s = true then pure (Lean.Parser.ParserState.restore s iniSz iniPos) else do let y ← pure PUnit.unit _do_jp y; if (Lean.Parser.ParserState.hasError s || c.quotDepth == 0 || !Lean.Syntax.isAntiquot (Array.back s.stxStack)) = true then pure s else do let y ← pure PUnit.unit _do_jp y)

source

@[inline]

def Lean.Parser.withAntiquotSuffixSplice (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) (suffix : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withAntiquotSuffixSplice kind p suffix = { info := Lean.Parser.andthenInfo p.info suffix.info, fn := Lean.Parser.withAntiquotSuffixSpliceFn kind p.fn suffix.fn }

source

def Lean.Parser.withAntiquotSpliceAndSuffix (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) (suffix : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withAntiquotSpliceAndSuffix kind p suffix = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquotSplice kind (Lean.Parser.withoutInfo p) suffix) (Lean.Parser.withAntiquotSuffixSplice kind p suffix)

source

def Lean.Parser.nodeWithAntiquot (name : String) (kind : Lean.SyntaxNodeKind) (p : Lean.Parser.Parser) (anonymous : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.nodeWithAntiquot name kind p anonymous = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot name (some kind) anonymous) (Lean.Parser.node kind p)

source

def Lean.Parser.sepByElemParser (p : Lean.Parser.Parser) (sep : String) :

Lean.Parser.Parser

Equations

Lean.Parser.sepByElemParser p sep = Lean.Parser.withAntiquotSpliceAndSuffix `sepBy p (Lean.Parser.symbol (String.trim sep ++ "*"))

source

def Lean.Parser.sepBy (p : Lean.Parser.Parser) (sep : String) (psep : optParam Lean.Parser.Parser (Lean.Parser.symbol sep)) (allowTrailingSep : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.sepBy p sep psep allowTrailingSep = Lean.Parser.sepByNoAntiquot (Lean.Parser.sepByElemParser p sep) psep allowTrailingSep

source

def Lean.Parser.sepBy1 (p : Lean.Parser.Parser) (sep : String) (psep : optParam Lean.Parser.Parser (Lean.Parser.symbol sep)) (allowTrailingSep : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.sepBy1 p sep psep allowTrailingSep = Lean.Parser.sepBy1NoAntiquot (Lean.Parser.sepByElemParser p sep) psep allowTrailingSep

source

def Lean.Parser.categoryParserOfStackFn (offset : Nat) :

Lean.Parser.ParserFn

Equations

Lean.Parser.categoryParserOfStackFn offset ctx s = let stack := s.stxStack; if Array.size stack < offset + 1 then Lean.Parser.ParserState.mkUnexpectedError s "failed to determine parser category using syntax stack, stack is too small" else match Array.get! stack (Array.size stack - offset - 1) with | Lean.Syntax.ident x x_1 catName x_2 => Lean.Parser.categoryParserFn catName ctx s | x => Lean.Parser.ParserState.mkUnexpectedError s "failed to determine parser category using syntax stack, the specified element on the stack is not an identifier"

source

def Lean.Parser.categoryParserOfStack (offset : Nat) (prec : optParam Nat 0) :

Lean.Parser.Parser

Equations

Lean.Parser.categoryParserOfStack offset prec = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := fun c s => Lean.Parser.categoryParserOfStackFn offset { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := prec, tokens := c.tokens, quotDepth := c.quotDepth, suppressInsideQuot := c.suppressInsideQuot, savedPos? := c.savedPos?, forbiddenTk? := c.forbiddenTk? } s }