From 491028df257459ab9521802ab49fc6d2df71423c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2019 20:31:41 -0800 Subject: [PATCH] feat: add `compileParserDescr` --- src/Init/Lean/Parser/Command.lean | 2 +- src/Init/Lean/Parser/Level.lean | 2 +- src/Init/Lean/Parser/Parser.lean | 66 +++++++++++++++++++++++-------- src/Init/LeanExt.lean | 28 +++++++------ 4 files changed, 67 insertions(+), 31 deletions(-) diff --git a/src/Init/Lean/Parser/Command.lean b/src/Init/Lean/Parser/Command.lean index daa211096d..772561efc0 100644 --- a/src/Init/Lean/Parser/Command.lean +++ b/src/Init/Lean/Parser/Command.lean @@ -22,7 +22,7 @@ registerParserAttribute `commandParser "command" "command parser" (some builtinC constant commandParserAttribute : ParserAttribute := arbitrary _ @[inline] def commandParser {k : ParserKind} (rbp : Nat := 0) : Parser k := -{ fn := fun _ => commandParserAttribute.runParser rbp } +{ fn := fun _ => commandParserAttribute.runParserFn rbp } namespace Command def commentBody : Parser := diff --git a/src/Init/Lean/Parser/Level.lean b/src/Init/Lean/Parser/Level.lean index be51d670d7..39aac71647 100644 --- a/src/Init/Lean/Parser/Level.lean +++ b/src/Init/Lean/Parser/Level.lean @@ -22,7 +22,7 @@ registerParserAttribute `levelParser "level" "universe level parser" (some built constant levelParserAttribute : ParserAttribute := arbitrary _ @[inline] def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k := -{ fn := fun _ => levelParserAttribute.runParser rbp } +{ fn := fun _ => levelParserAttribute.runParserFn rbp } namespace Level diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 24432e1c80..034934425b 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1394,6 +1394,9 @@ else def mkBuiltinParsingTablesRef : IO (IO.Ref ParsingTables) := IO.mkRef {} +@[init mkBuiltinParsingTablesRef] +constant builtinTermParsingTable : IO.Ref ParsingTables := arbitrary _ + private def updateTokens (info : ParserInfo) (declName : Name) : IO Unit := do tokens ← builtinTokenTable.swap {}; match info.updateTokens tokens with @@ -1484,7 +1487,46 @@ structure ParserAttribute := (ext : PersistentEnvExtension ParserAttributeEntry ParsingTables) (kind : String) -instance ParserAttribute.inhabited : Inhabited ParserAttribute := ⟨{ attr := arbitrary _, ext := arbitrary _, kind := "" }⟩ +namespace ParserAttribute + +instance : Inhabited ParserAttribute := ⟨{ attr := arbitrary _, ext := arbitrary _, kind := "" }⟩ + +def runParserFn (attr : ParserAttribute) : ParserFn leading := +fun a c s => + let tables : ParsingTables := attr.ext.getState c.env; + prattParser attr.kind tables a c s + +def mkParser (attr : ParserAttribute) (rbp : Nat) : Parser leading := +{ fn := fun _ => attr.runParserFn rbp } + +end ParserAttribute + +abbrev ParserAttributeTable := HashMap Name ParserAttribute + +def mkParserAttributeTable : IO (IO.Ref ParserAttributeTable) := +IO.mkRef {} + +@[init mkParserAttributeTable] +constant parserAttributeTable : IO.Ref ParserAttributeTable := arbitrary _ + +def compileParserDescr (table : ParserAttributeTable) : forall {k : ParserKind}, ParserDescr k → Except String (Parser k) +| _, ParserDescr.andthen d₁ d₂ => andthen <$> compileParserDescr d₁ <*> compileParserDescr d₂ +| _, ParserDescr.orelse d₁ d₂ => orelse <$> compileParserDescr d₁ <*> compileParserDescr d₂ +| _, ParserDescr.optional d => optional <$> compileParserDescr d +| _, ParserDescr.lookahead d => lookahead <$> compileParserDescr d +| _, ParserDescr.try d => try <$> compileParserDescr d +| _, ParserDescr.many d => many <$> compileParserDescr d +| _, ParserDescr.many1 d => many1 <$> compileParserDescr d +| _, ParserDescr.sepBy d₁ d₂ => sepBy <$> compileParserDescr d₁ <*> compileParserDescr d₂ +| _, ParserDescr.sepBy1 d₁ d₂ => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂ +| _, ParserDescr.node k d => node k <$> compileParserDescr d +| _, ParserDescr.symbol tk lbp => pure $ symbol tk lbp +| _, ParserDescr.unicodeSymbol tk₁ tk₂ lbp => pure $ unicodeSymbol tk₁ tk₂ lbp +| ParserKind.leading, ParserDescr.parser n rbp => + match table.find? n with + | some attr => pure $ attr.mkParser rbp + | none => throw ("unknow parser kind '" ++ toString n ++ "'") +| ParserKind.trailing, ParserDescr.pushLeading => pure $ pushLeading /- This is just the basic skeleton where we create an @@ -1493,10 +1535,12 @@ a builtin parser attribute. The current implementation just uses the bultin parser. We still need to: -- Add a ParserDescr type, and write an interpreter for it. - Add support for scoped parser extensions. -/ def registerParserAttribute (attrName : Name) (kind : String) (descr : String) (builtinTable : Option (IO.Ref ParsingTables) := none) : IO ParserAttribute := do +let kindSym := mkNameSimple kind; +attrTable ← parserAttributeTable.get; +when (attrTable.contains kindSym) $ throw (IO.userError ("parser attribute '" ++ kind ++ "' has already been defined")); ext : PersistentEnvExtension ParserAttributeEntry ParsingTables ← registerPersistentEnvExtension { name := attrName, addImportedFn := fun es => do @@ -1514,22 +1558,12 @@ let attrImpl : AttributeImpl := { descr := descr, add := fun env decl args persistent => pure env -- TODO }; -pure { ext := ext, attr := attrImpl, kind := kind } - -namespace ParserAttribute - -def runParser (attr : ParserAttribute) : ParserFn leading := -fun a c s => - let tables : ParsingTables := attr.ext.getState c.env; - prattParser attr.kind tables a c s - -end ParserAttribute +let attr : ParserAttribute := { ext := ext, attr := attrImpl, kind := kind }; +parserAttributeTable.modify $ fun table => table.insert kindSym attr; +pure attr -- declare `termParser` here since it is used everywhere via antiquotations -@[init mkBuiltinParsingTablesRef] -constant builtinTermParsingTable : IO.Ref ParsingTables := arbitrary _ - @[init] def regBuiltinTermParserAttr : IO Unit := registerBuiltinParserAttribute `builtinTermParser `Lean.Parser.builtinTermParsingTable @@ -1540,7 +1574,7 @@ registerParserAttribute `termParser "term" "term parser" (some builtinTermParsin constant termParserAttribute : ParserAttribute := arbitrary _ @[inline] def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k := -{ fn := fun _ => termParserAttribute.runParser rbp } +{ fn := fun _ => termParserAttribute.runParserFn rbp } def dollarSymbol {k : ParserKind} : Parser k := symbol "$" 1 diff --git a/src/Init/LeanExt.lean b/src/Init/LeanExt.lean index 15e118d72e..8b202643c1 100644 --- a/src/Init/LeanExt.lean +++ b/src/Init/LeanExt.lean @@ -29,18 +29,20 @@ inductive ParserKind /- Small DSL for describing parsers. We implement an interpreter for it at `Parser.lean` -/ -inductive ParserDescr (kind : ParserKind := ParserKind.leading) -| andthen : ParserDescr → ParserDescr → ParserDescr -| orelse : ParserDescr → ParserDescr → ParserDescr -| optional : ParserDescr → ParserDescr -| lookahead : ParserDescr → ParserDescr -| try : ParserDescr → ParserDescr -| many : ParserDescr → ParserDescr -| many1 : ParserDescr → ParserDescr -| sepBy : ParserDescr → ParserDescr → ParserDescr -| sepBy1 : ParserDescr → ParserDescr → ParserDescr -| symbol : String → Nat → ParserDescr -| unicodeSymbol : String → String → Nat → ParserDescr -| parser : Name → ParserDescr +inductive ParserDescr : ParserKind → Type +| andthen {k : ParserKind} : ParserDescr k → ParserDescr k → ParserDescr k +| orelse {k : ParserKind} : ParserDescr k → ParserDescr k → ParserDescr k +| optional {k : ParserKind} : ParserDescr k → ParserDescr k +| lookahead {k : ParserKind} : ParserDescr k → ParserDescr k +| try {k : ParserKind} : ParserDescr k → ParserDescr k +| many {k : ParserKind} : ParserDescr k → ParserDescr k +| many1 {k : ParserKind} : ParserDescr k → ParserDescr k +| sepBy {k : ParserKind} : ParserDescr k → ParserDescr k → ParserDescr k +| sepBy1 {k : ParserKind} : ParserDescr k → ParserDescr k → ParserDescr k +| node {k : ParserKind} : Name → ParserDescr k → ParserDescr k +| symbol {k : ParserKind} : String → Nat → ParserDescr k +| unicodeSymbol {k : ParserKind} : String → String → Nat → ParserDescr k +| pushLeading : ParserDescr ParserKind.trailing +| parser : Name → Nat → ParserDescr ParserKind.leading end Lean