chore: helpers for parser debugging

This commit is contained in:
Sebastian Ullrich 2021-04-04 23:44:10 +02:00
parent 9f708ece44
commit e5be9e7dd4
3 changed files with 17 additions and 0 deletions

View file

@ -327,6 +327,19 @@ structure Parser where
abbrev TrailingParser := Parser
def dbgTraceStateFn (label : String) (p : ParserFn) : ParserFn :=
fun c s =>
let sz := s.stxStack.size
let s' := p c s
dbg_trace "{label}
pos: {s'.pos}
err: {s'.errorMsg}
out: {s'.stxStack.extract sz s'.stxStack.size}" s'
def dbgTraceState (label : String) (p : Parser) : Parser where
fn := dbgTraceStateFn label p.fn
info := p.info
@[noinline] def epsilonInfo : ParserInfo :=
{ firstTokens := FirstTokens.epsilon }

View file

@ -450,6 +450,8 @@ def interpolatedStr.formatter (p : Formatter) : Formatter := do
| some str => push str *> goLeft
| none => p
@[combinatorFormatter Lean.Parser.dbgTraceState] def dbgTraceState.formatter (label : String) (p : Formatter) : Formatter := p
@[combinatorFormatter ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Formatter) : Formatter :=
if c then t else e

View file

@ -494,6 +494,8 @@ def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do
else
p
@[combinatorParenthesizer Lean.Parser.dbgTraceState] def dbgTraceState.parenthesizer (label : String) (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Parenthesizer) : Parenthesizer :=
if c then t else e