max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: parser error setters

Browse source
This commit is contained in:
Sebastian Ullrich 2023-07-04 08:57:35 +02:00
parent 3aa1cfccea
commit f4fc8b3e15
3 changed files with 20 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Parser/Basic.lean
View file

@ -139,8 +139,7 @@ def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s =>
| none => s
| some pos =>
let pos := if delta then c.input.next pos else pos
match s with
| ⟨stack, lhsPrec, _, cache, _⟩ => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { unexpected := msg }⟩
s.mkUnexpectedErrorAt msg pos
/-- Generate an error at the position saved with the `withPosition` combinator.
If `delta == true`, then it reports at saved position+1.

10
src/Lean/Parser/StrInterpolation.lean
View file

@ -15,9 +15,8 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
let rec parse (startPos : String.Pos) (c : ParserContext) (s : ParserState) : ParserState :=
let i := s.pos
if input.atEnd i then
let s := s.pushSyntax Syntax.missing
let s := s.mkNode interpolatedStrKind stackSize
s.setError "unterminated string literal"
let s := s.mkError "unterminated string literal"
s.mkNode interpolatedStrKind stackSize
else
let curr := input.get i
let s := s.setPos (input.next i)
@ -37,9 +36,8 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
let s := s.setPos (input.next i)
parse i c s
else
let s := s.pushSyntax Syntax.missing
let s := s.mkNode interpolatedStrKind stackSize
s.setError "'}'"
let s := s.mkError "'}'"
s.mkNode interpolatedStrKind stackSize
else
parse startPos c s
let startPos := s.pos

31
src/Lean/Parser/Types.lean
View file

@ -259,34 +259,33 @@ def mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : P
let stack := stack.push newNode
⟨stack, lhsPrec, pos, cache, err⟩
def setError (s : ParserState) (msg : String) : ParserState :=
@[inline]
def setError (s : ParserState) (e : Error) : ParserState :=
match s with
| ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
| ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack, lhsPrec, pos, cache, some e⟩
def mkError (s : ParserState) (msg : String) : ParserState :=
match s with
| ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
s.setError { expected := [msg] } |>.pushSyntax .missing
def mkUnexpectedError (s : ParserState) (msg : String) (expected : List String := []) (pushMissing := true) : ParserState :=
match s with
| ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨if pushMissing then stack.push .missing else stack, lhsPrec, pos, cache, some { unexpected := msg, expected := expected }⟩
let s := s.setError { unexpected := msg, expected }
if pushMissing then s.pushSyntax .missing else s
def mkEOIError (s : ParserState) (expected : List String := []) : ParserState :=
s.mkUnexpectedError "unexpected end of input" expected
def mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState :=
match s, initStackSz? with
| ⟨stack, lhsPrec, _, cache, _⟩, none => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
| ⟨stack, lhsPrec, _, cache, _⟩, some sz => ⟨stack.shrink sz |>.push Syntax.missing, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
def mkErrorsAt (s : ParserState) (ex : List String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState := Id.run do
let mut s := s.setPos pos
if let some sz := initStackSz? then
s := s.shrinkStack sz
s := s.setError { expected := ex }
s.pushSyntax .missing
def mkErrorsAt (s : ParserState) (ex : List String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState :=
match s, initStackSz? with
| ⟨stack, lhsPrec, _, cache, _⟩, none => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { expected := ex }⟩
| ⟨stack, lhsPrec, _, cache, _⟩, some sz => ⟨stack.shrink sz |>.push Syntax.missing, lhsPrec, pos, cache, some { expected := ex }⟩
def mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState :=
s.mkErrorsAt [msg] pos initStackSz?
def mkUnexpectedErrorAt (s : ParserState) (msg : String) (pos : String.Pos) : ParserState :=
match s with
| ⟨stack, lhsPrec, _, cache, _⟩ => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { unexpected := msg }⟩
s.setPos pos |>.mkUnexpectedError msg
end ParserState