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

chore: longestMatchFn parsers must produce exactly one Syntax node

Browse source 
Before this commit, we were handling the following two abnormal cases:

1- `p` did not produce any `Syntax` node. `runLongestMatchParser`
would insert a `Syntax.missing`.

2- `p` produced more than one `Syntax` node on the
stack. `runLongestMatchParser` would combine all of them using a
`nullKind` node.

This feature was never used since we only use `longestMatchFn` to
process leading and trailing parsers. In both case, we create a node.
Moreover, if a bad parser is manually created, I think it is better to
fail than accept using `Syntax.missing` or a `nullKind` node. We would
only be postponing the problem since we don't have elaboration
functions for them.

cc @Kha
This commit is contained in:
Leonardo de Moura 2020-06-11 12:38:55 -07:00
parent 8e4dc5bcf6
commit f0ebf426b7
1 changed files with 11 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1237,11 +1237,15 @@ s.keepLatest startStackSize
end ParserState
def invalidLongestMatchParser (s : ParserState) : ParserState :=
s.mkError "longestMatch parsers must generate exactly one Syntax node"
/--
Auxiliary function used to execute parsers provided to `longestMatchFn`.
Push `left?` into the stack if it is not `none`, and execute `p`.
After executing `p`, remove `left` and combine `p` results.
After executing `p`, remove `left`.
Remark: `p` must produce exactly one syntax node.
Remark: the `left?` is not none when we are processing trailing parsers. -/
@[inline] def runLongestMatchParser (left? : Option Syntax) (p : ParserFn) : ParserFn :=
fun c s =>
@ -1251,37 +1255,24 @@ fun c s =>
let s := p c s;
if s.hasError then s
else
-- stack contains `[..., result_1, ... result_n ]` we must combine the different result nodes
let currSize := s.stackSize;
if currSize == startSize + 1 then
-- `p` created one node
-- stack contains `[..., result ]`
if s.stackSize == startSize + 1 then
s
else
-- `p` created more than one node, we combine them into a single node
let r := Syntax.node nullKind (s.stxStack.extract startSize currSize);
let s := s.shrinkStack startSize;
s.pushSyntax r
invalidLongestMatchParser s
| some left =>
let s := s.pushSyntax left;
let s := p c s;
if s.hasError then s
else
-- stack contains `[..., left, result_1, ... result_n ]` we must remove `left`, and combine the different result nodes
let currSize := s.stackSize;
if currSize == startSize + 1 then
-- `p` did not create any node, then we just remove `left` and add `Syntax.missing`
let s := s.shrinkStack startSize;
s.pushSyntax Syntax.missing
else if currSize == startSize + 2 then
-- stack contains `[..., left, result ]` we must remove `left`
if s.stackSize == startSize + 2 then
-- `p` created one node, then we just remove `left` and keep it
let r := s.stxStack.back;
let s := s.shrinkStack startSize; -- remove `r` and `left`
s.pushSyntax r -- add `r` back
else
-- `p` created more than one node, we combine them into a single node
let r := Syntax.node nullKind (s.stxStack.extract (startSize+1) currSize);
let s := s.shrinkStack startSize;
s.pushSyntax r
invalidLongestMatchParser s
def longestMatchStep (left? : Option Syntax) (startSize : Nat) (startPos : String.Pos) (p : ParserFn) : ParserFn :=
fun c s =>