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

feat: add new kind of parser category

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-20 20:06:04 -08:00
parent c89972b6e2
commit 4ff001fa04
2 changed files with 104 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Elab/Syntax.lean
View file

@ -140,7 +140,7 @@ fun stx => do
let catName := stx.getIdAt 1;
let attrName := catName.appendAfter "Parser";
env ← getEnv;
env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
env ← liftIO stx $ Parser.registerPrattParserCategory env attrName catName;
setEnv env
def mkFreshKind (catName : Name) : CommandElabM Name := do

163
src/Init/Lean/Parser/Parser.lean
View file

@ -1250,31 +1250,48 @@ instance {α : Type} : HasEmptyc (TokenMap α) := ⟨RBMap.empty⟩
end TokenMap
structure ParsingTables :=
structure PrattParsingTables :=
(leadingTable : TokenMap Parser := {})
(trailingTable : TokenMap TrailingParser := {})
(trailingParsers : List TrailingParser := []) -- for supporting parsers such as function application
instance ParsingTables.inhabited : Inhabited ParsingTables := ⟨{}⟩
instance PrattParsingTables.inhabited : Inhabited PrattParsingTables := ⟨{}⟩
/-
Each parser category has its own Pratt's parsing tables.
/--
Each parser category is implemented using Pratt's parser or a sequence of parsers (`simple` constructor).
The system comes equipped with the following categories: `level`, `term`, `tactic`, and `command`.
Users and plugins may define extra categories.
The field `leadingIdentAsSymbol` specifies how the parsing table lookup function behaves for identifiers.
The function `prattParser` uses two tables `leadingTable` and `trailingTable`. They map tokens to
parsers. If `leadingIdentAsSymbol == false` and the leading token is an identifier, then `prattParser`
just executes the parsers associated with the auxiliary token "ident".
If `leadingIdentAsSymbol == true` and the leading token is an identifier `<foo>`, then `prattParser`
combines the parsers associated with the token `<foo>` with the parsers associated with the auxiliary token "ident".
We use this feature and the `nonReservedSymbol` parser to implement the `tactic` parsers.
We use this approach to avoid creating a reserved symbol for each builtin tactic (e.g., `apply`, `assumption`, etc.).
That is, users may still use these symbols as identifiers (e.g., naming a function).
-/
structure ParserCategory :=
(tables : ParsingTables)
(leadingIdentAsSymbol : Bool := false)
We current support two kinds of parser categories.
- `pratt` which is ideal for implementing big categories and supports left-recursion,
but each parser is left recursive or starts with an atom.
A parser `syntax term "<=" ident "<" term : index` is not allowed here because
it doesn't start with atom nor with the `index` catagory.
The field `leadingIdentAsSymbol` specifies how the parsing table
lookup function behaves for identifiers. The function
`prattParser` uses two tables `leadingTable` and
`trailingTable`. They map tokens to parsers. If
`leadingIdentAsSymbol == false` and the leading token is an
identifier, then `prattParser` just executes the parsers
associated with the auxiliary token "ident". If
`leadingIdentAsSymbol == true` and the leading token is an
identifier `<foo>`, then `prattParser` combines the parsers
associated with the token `<foo>` with the parsers associated
with the auxiliary token "ident". We use this feature and the
`nonReservedSymbol` parser to implement the `tactic` parsers. We
use this approach to avoid creating a reserved symbol for each
builtin tactic (e.g., `apply`, `assumption`, etc.). That is,
users may still use these symbols as identifiers (e.g., naming a
function).
- `simple` which is ideal for small categories which are not left recursive.
This kind of category is implemented using the longestMatch combinator. -/
inductive ParserCategory
| pratt (tables : PrattParsingTables) (leadingIdentAsSymbol : Bool) : ParserCategory
| simple (parsers : List Parser) : ParserCategory
instance ParserCategory.inhabited : Inhabited ParserCategory := ⟨ParserCategory.simple []⟩
abbrev ParserCategories := PersistentHashMap Name ParserCategory
@ -1319,7 +1336,7 @@ private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
if s.stackSize == iniSz + 1 then s
else s.mkNode nullKind iniSz -- throw error instead?
def leadingParser (kind : Name) (tables : ParsingTables) (leadingIdentAsSymbol : Bool) : ParserFn leading :=
def leadingParser (kind : Name) (tables : PrattParsingTables) (leadingIdentAsSymbol : Bool) : ParserFn leading :=
fun a c s =>
let iniSz := s.stackSize;
let (s, ps) := indexed tables.leadingTable c s leadingIdentAsSymbol;
@ -1329,11 +1346,11 @@ fun a c s =>
let s := longestMatchFn ps a c s;
mkResult s iniSz
def trailingLoopStep (tables : ParsingTables) (ps : List (Parser trailing)) : ParserFn trailing :=
def trailingLoopStep (tables : PrattParsingTables) (ps : List (Parser trailing)) : ParserFn trailing :=
fun left c s =>
orelseFn (longestMatchFn ps) (anyOfFn tables.trailingParsers) left c s
partial def trailingLoop (tables : ParsingTables) (rbp : Nat) (c : ParserContext) : Syntax → ParserState → ParserState
partial def trailingLoop (tables : PrattParsingTables) (rbp : Nat) (c : ParserContext) : Syntax → ParserState → ParserState
| left, s =>
let (s, lbp) := currLbp left c s;
if rbp ≥ lbp then s.pushSyntax left
@ -1352,7 +1369,7 @@ partial def trailingLoop (tables : ParsingTables) (rbp : Nat) (c : ParserContext
let s := s.popSyntax;
trailingLoop left s
def prattParser (kind : Name) (tables : ParsingTables) (leadingIdentAsSymbol : Bool) : ParserFn leading :=
def prattParser (kind : Name) (tables : PrattParsingTables) (leadingIdentAsSymbol : Bool) : ParserFn leading :=
fun rbp c s =>
let s := leadingParser kind tables leadingIdentAsSymbol rbp c s;
if s.hasError then s
@ -1407,28 +1424,31 @@ def mkBuiltinParserCategories : IO (IO.Ref ParserCategories) := IO.mkRef {}
private def throwParserCategoryAlreadyDefined {α} (catName : Name) : ExceptT String Id α :=
throw ("parser category '" ++ toString catName ++ "' has already been defined")
private def addParserCategoryCore (categories : ParserCategories) (catName : Name) (leadingIdentAsSymbol : Bool) : Except String ParserCategories :=
private def addParserCategoryCore (categories : ParserCategories) (catName : Name) (initial : ParserCategory) : Except String ParserCategories :=
if categories.contains catName then
throwParserCategoryAlreadyDefined catName
else
pure $ categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol }
pure $ categories.insert catName initial
/-- All builtin parser categories are Pratt's parsers -/
private def addBuiltinParserCategory (catName : Name) (leadingIdentAsSymbol : Bool) : IO Unit := do
categories ← builtinParserCategoriesRef.get;
categories ← IO.ofExcept $ addParserCategoryCore categories catName leadingIdentAsSymbol;
categories ← IO.ofExcept $ addParserCategoryCore categories catName $ ParserCategory.pratt {} leadingIdentAsSymbol;
builtinParserCategoriesRef.set categories
inductive ParserExtensionOleanEntry
| token (val : TokenConfig) : ParserExtensionOleanEntry
| kind (val : SyntaxNodeKind) : ParserExtensionOleanEntry
| category (catName : Name) (leadingIdentAsSymbol : Bool)
| parser (catName : Name) (declName : Name) : ParserExtensionOleanEntry
| token (val : TokenConfig) : ParserExtensionOleanEntry
| kind (val : SyntaxNodeKind) : ParserExtensionOleanEntry
| prattCategory (catName : Name) (leadingIdentAsSymbol : Bool)
| simpleCategory (catName : Name)
| parser (catName : Name) (declName : Name) : ParserExtensionOleanEntry
inductive ParserExtensionEntry
| token (val : TokenConfig) : ParserExtensionEntry
| kind (val : SyntaxNodeKind) : ParserExtensionEntry
| category (catName : Name) (leadingIdentAsSymbol : Bool)
| parser (catName : Name) (declName : Name) (k : ParserKind) (p : Parser k) : ParserExtensionEntry
| token (val : TokenConfig) : ParserExtensionEntry
| kind (val : SyntaxNodeKind) : ParserExtensionEntry
| prattCategory (catName : Name) (leadingIdentAsSymbol : Bool)
| simpleCategory (catName : Name)
| parser (catName : Name) (declName : Name) (k : ParserKind) (p : Parser k) : ParserExtensionEntry
structure ParserExtensionState :=
(tokens : TokenTable := {})
@ -1468,22 +1488,25 @@ def throwUnknownParserCategory {α} (catName : Name) : ExceptT String Id α :=
throw ("unknown parser category '" ++ toString catName ++ "'")
def addLeadingParser (categories : ParserCategories) (catName : Name) (parserName : Name) (p : Parser) : Except String ParserCategories :=
let addTokens (tks : List TokenConfig) : Except String ParserCategories :=
match categories.find? catName with
| none => throwUnknownParserCategory catName
| some cat =>
match categories.find? catName with
| none =>
throwUnknownParserCategory catName
| some (ParserCategory.simple parsers) =>
pure $ categories.insert catName (ParserCategory.simple (p::parsers))
| some (ParserCategory.pratt tables i) =>
let addTokens (tks : List TokenConfig) : Except String ParserCategories :=
let tks := tks.map $ fun tk => mkNameSimple tk.val;
let tables := tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) cat.tables;
pure $ categories.insert catName { tables := tables, .. cat };
match p.info.firstTokens with
| FirstTokens.tokens tks => addTokens tks
| FirstTokens.optTokens tks => addTokens tks
| _ => throw ("invalid parser '" ++ toString parserName ++ "', initial token is not statically known")
let tables := tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) tables;
pure $ categories.insert catName (ParserCategory.pratt tables i);
match p.info.firstTokens with
| FirstTokens.tokens tks => addTokens tks
| FirstTokens.optTokens tks => addTokens tks
| _ => throw ("invalid parser '" ++ toString parserName ++ "', initial token is not statically known")
private def addTrailingParserAux (tables : ParsingTables) (p : TrailingParser) : ParsingTables :=
let addTokens (tks : List TokenConfig) : ParsingTables :=
private def addTrailingParserAux (tables : PrattParsingTables) (p : TrailingParser) : PrattParsingTables :=
let addTokens (tks : List TokenConfig) : PrattParsingTables :=
let tks := tks.map $ fun tk => mkNameSimple tk.val;
tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { trailingTable := tables.trailingTable.insert tk p, .. tables }) tables;
tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { trailingTable := tables.trailingTable.insert tk p, .. tables }) tables;
match p.info.firstTokens with
| FirstTokens.tokens tks => addTokens tks
| FirstTokens.optTokens tks => addTokens tks
@ -1491,8 +1514,9 @@ match p.info.firstTokens with
def addTrailingParser (categories : ParserCategories) (catName : Name) (p : TrailingParser) : Except String ParserCategories :=
match categories.find? catName with
| none => throwUnknownParserCategory catName
| some cat => pure $ categories.insert catName { tables := addTrailingParserAux cat.tables p, .. cat }
| none => throwUnknownParserCategory catName
| some (ParserCategory.simple _) => throw ("parser category '" ++ toString catName ++ "' does not support trailing parsers")
| some (ParserCategory.pratt tables i) => pure $ categories.insert catName $ ParserCategory.pratt (addTrailingParserAux tables p) i
def addParser {k} (categories : ParserCategories) (catName : Name) (declName : Name) (p : Parser k) : Except String ParserCategories :=
match k, p with
@ -1530,10 +1554,14 @@ match e with
| _ => unreachable!
| ParserExtensionEntry.kind k =>
{ kinds := s.kinds.insert k, newEntries := ParserExtensionOleanEntry.kind k :: s.newEntries, .. s }
| ParserExtensionEntry.category catName leadingIdentAsSymbol =>
| ParserExtensionEntry.prattCategory catName leadingIdentAsSymbol =>
if s.categories.contains catName then s
else { categories := s.categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol },
newEntries := ParserExtensionOleanEntry.category catName leadingIdentAsSymbol :: s.newEntries, .. s }
else { categories := s.categories.insert catName (ParserCategory.pratt {} leadingIdentAsSymbol),
newEntries := ParserExtensionOleanEntry.prattCategory catName leadingIdentAsSymbol :: s.newEntries, .. s }
| ParserExtensionEntry.simpleCategory catName =>
if s.categories.contains catName then s
else { categories := s.categories.insert catName (ParserCategory.simple []),
newEntries := ParserExtensionOleanEntry.simpleCategory catName :: s.newEntries, .. s }
| ParserExtensionEntry.parser catName declName _ parser =>
match addParser s.categories catName declName parser with
| Except.ok categories => { categories := categories, newEntries := ParserExtensionOleanEntry.parser catName declName :: s.newEntries, .. s }
@ -1601,8 +1629,11 @@ es.foldlM
pure { tokens := tokens, .. s }
| ParserExtensionOleanEntry.kind k =>
pure { kinds := s.kinds.insert k, .. s }
| ParserExtensionOleanEntry.category catName leadingIdentAsSymbol => do
categories ← IO.ofExcept (addParserCategoryCore s.categories catName leadingIdentAsSymbol);
| ParserExtensionOleanEntry.prattCategory catName leadingIdentAsSymbol => do
categories ← IO.ofExcept (addParserCategoryCore s.categories catName (ParserCategory.pratt {} leadingIdentAsSymbol));
pure { categories := categories, .. s }
| ParserExtensionOleanEntry.simpleCategory catName => do
categories ← IO.ofExcept (addParserCategoryCore s.categories catName (ParserCategory.simple []));
pure { categories := categories, .. s }
| ParserExtensionOleanEntry.parser catName declName =>
match mkParserOfConstant env s.categories declName with
@ -1642,18 +1673,25 @@ let env := parserExtension.setState env { nextKindIdx := idx+1, .. s };
def isParserCategory (env : Environment) (catName : Name) : Bool :=
(parserExtension.getState env).categories.contains catName
def addParserCategory (env : Environment) (catName : Name) (leadingIdentAsSymbol : Bool) : Except String Environment := do
def addPrattParserCategory (env : Environment) (catName : Name) (leadingIdentAsSymbol : Bool) : Except String Environment := do
if isParserCategory env catName then
throwParserCategoryAlreadyDefined catName
else
pure $ parserExtension.addEntry env $ ParserExtensionEntry.category catName leadingIdentAsSymbol
pure $ parserExtension.addEntry env $ ParserExtensionEntry.prattCategory catName leadingIdentAsSymbol
def addSimpleParserCategory (env : Environment) (catName : Name) : Except String Environment := do
if isParserCategory env catName then
throwParserCategoryAlreadyDefined catName
else
pure $ parserExtension.addEntry env $ ParserExtensionEntry.simpleCategory catName
def categoryParserFnImpl (catName : Name) : ParserFn leading :=
fun rbp ctx s =>
let categories := (parserExtension.getState ctx.env).categories;
match categories.find? catName with
| some cat => prattParser catName cat.tables cat.leadingIdentAsSymbol rbp ctx s
| none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
| some (ParserCategory.pratt tables leadingIdentAsSymbol) => prattParser catName tables leadingIdentAsSymbol rbp ctx s
| some (ParserCategory.simple parsers) => longestMatchFn parsers rbp ctx s
| none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
@[init] def setCategoryParserFnRef : IO Unit :=
categoryParserFnRef.set categoryParserFnImpl
@ -1694,15 +1732,16 @@ def mkParserState (input : String) : ParserState :=
def runParserCategory (env : Environment) (catName : Name) (input : String) (fileName := "<input>") : Except String Syntax :=
let categories := (parserExtension.getState env).categories;
match categories.find? catName with
| some cat =>
| some (ParserCategory.pratt tables leadingIdentAsSymbol) =>
let c := mkParserContext env (mkInputContext input fileName);
let s := mkParserState input;
let s := whitespace c s;
let s := prattParser catName cat.tables cat.leadingIdentAsSymbol (0 : Nat) c s;
let s := prattParser catName tables leadingIdentAsSymbol (0 : Nat) c s;
if s.hasError then
Except.error (s.toErrorMsg c)
else
Except.ok s.stxStack.back
| some _ => throw "runParserCategory does not support simple parsers yet"
| none => throwUnknownParserCategory catName
def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) (declName : Name) : IO Environment :=
@ -1786,8 +1825,12 @@ registerAttributeImplBuilder `parserAttr $ fun args =>
| [DataValue.ofName attrName, DataValue.ofName catName] => pure $ mkParserAttributeImpl attrName catName
| _ => throw ("invalid parser attribute implementation builder arguments")
def registerParserCategory (env : Environment) (attrName : Name) (catName : Name) (leadingIdentAsSymbol := false) : IO Environment := do
env ← IO.ofExcept $ addParserCategory env catName leadingIdentAsSymbol;
def registerPrattParserCategory (env : Environment) (attrName : Name) (catName : Name) (leadingIdentAsSymbol := false) : IO Environment := do
env ← IO.ofExcept $ addPrattParserCategory env catName leadingIdentAsSymbol;
registerAttributeOfBuilder env `parserAttr [DataValue.ofName attrName, DataValue.ofName catName]
def registerSimpleParserCategory (env : Environment) (attrName : Name) (catName : Name) : IO Environment := do
env ← IO.ofExcept $ addSimpleParserCategory env catName;
registerAttributeOfBuilder env `parserAttr [DataValue.ofName attrName, DataValue.ofName catName]
-- declare `termParser` here since it is used everywhere via antiquotations