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

fix(library/init/lean/parser/parser): use eraseDups when registering builting parsers

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-22 18:19:47 -07:00
parent 8b0730ef7d
commit c40cba66fb
1 changed files with 12 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
library/init/lean/parser/parser.lean
View file

@ -1420,25 +1420,26 @@ do tables ← tablesRef.get;
tablesRef.reset;
updateTokens p.info declName;
updateSyntaxNodeKinds p.info;
let addTokens (tks : List TokenConfig) : IO Unit :=
let tks := tks.map $ fun tk => mkSimpleName tk.val;
tablesRef.set $ tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) tables;
match p.info.firstTokens with
| FirstTokens.tokens tks =>
let tables := tks.foldl (fun (tables : ParsingTables) tk => { leadingTable := tables.leadingTable.insert (mkSimpleName tk.val) p, .. tables }) tables;
tablesRef.set tables
| _ =>
throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', initial token is not statically known"))
| FirstTokens.tokens tks => addTokens tks
| FirstTokens.optTokens tks => addTokens tks
| _ => throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', initial token is not statically known"))
def addBuiltinTrailingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : TrailingParser) : IO Unit :=
do tables ← tablesRef.get;
tablesRef.reset;
updateTokens p.info declName;
updateSyntaxNodeKinds p.info;
let addTokens (tks : List TokenConfig) : IO Unit :=
let tks := tks.map $ fun tk => mkSimpleName tk.val;
tablesRef.set $ tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { trailingTable := tables.trailingTable.insert tk p, .. tables }) tables;
match p.info.firstTokens with
| FirstTokens.tokens tks =>
let tables := tks.foldl (fun (tables : ParsingTables) tk => { trailingTable := tables.trailingTable.insert (mkSimpleName tk.val) p, .. tables }) tables;
tablesRef.set tables
| _ =>
let tables := { trailingParsers := p :: tables.trailingParsers, .. tables };
tablesRef.set tables
| FirstTokens.tokens tks => addTokens tks
| FirstTokens.optTokens tks => addTokens tks
| _ => tablesRef.set { trailingParsers := p :: tables.trailingParsers, .. tables }
def declareBuiltinParser (env : Environment) (addFnName : Name) (refDeclName : Name) (declName : Name) : IO Environment :=
let name := `_regBuiltinParser ++ declName;