From c6e7ea8fd50d8a5dc889abb8715efeda13f4f907 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Jun 2020 14:02:06 -0700 Subject: [PATCH] feat: add `ParserDescr.parser` constructor for embedding parser definitions into parser descriptions --- src/Init/LeanInit.lean | 1 + src/Lean/Parser/Parser.lean | 62 ++++++++++++++++++------------ tests/lean/run/termParserAttr.lean | 13 +++++++ 3 files changed, 51 insertions(+), 25 deletions(-) diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index 76fdc08b97..d466672dfa 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -156,6 +156,7 @@ inductive ParserDescr | nameLit : ParserDescr | ident : ParserDescr | cat : Name → Nat → ParserDescr +| parser : Name → ParserDescr instance ParserDescr.inhabited : Inhabited ParserDescr := ⟨ParserDescr.symbol ""⟩ abbrev TrailingParserDescr := ParserDescr diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index 323d0090c0..fb30da75d0 100644 --- a/src/Lean/Parser/Parser.lean +++ b/src/Lean/Parser/Parser.lean @@ -1753,7 +1753,38 @@ match e with | Except.ok categories => { s with categories := categories, newEntries := ParserExtensionOleanEntry.parser catName declName :: s.newEntries } | _ => unreachable! -def compileParserDescr (categories : ParserCategories) : ParserDescr → Except String (Parser) +unsafe def mkParserOfConstantUnsafe + (env : Environment) (categories : ParserCategories) (constName : Name) + (compileParserDescr : ParserDescr → Except String Parser) + : Except String (Bool × Parser) := +match env.find? constName with +| none => throw ("unknow constant '" ++ toString constName ++ "'") +| some info => + match info.type with + | Expr.const `Lean.Parser.TrailingParser _ _ => do + p ← env.evalConst Parser constName; + pure ⟨false, p⟩ + | Expr.const `Lean.Parser.Parser _ _ => do + p ← env.evalConst Parser constName; + pure ⟨true, p⟩ + | Expr.const `Lean.ParserDescr _ _ => do + d ← env.evalConst ParserDescr constName; + p ← compileParserDescr d; + pure ⟨true, p⟩ + | Expr.const `Lean.TrailingParserDescr _ _ => do + d ← env.evalConst TrailingParserDescr constName; + p ← compileParserDescr d; + pure ⟨false, p⟩ + | _ => throw ("unexpected parser type at '" ++ toString constName ++ "' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected") + +@[implementedBy mkParserOfConstantUnsafe] +constant mkParserOfConstantAux + (env : Environment) (categories : ParserCategories) (constName : Name) + (compileParserDescr : ParserDescr → Except String Parser) + : Except String (Bool × Parser) := +arbitrary _ + +partial def compileParserDescr (env : Environment) (categories : ParserCategories) : ParserDescr → Except String Parser | ParserDescr.andthen d₁ d₂ => andthen <$> compileParserDescr d₁ <*> compileParserDescr d₂ | ParserDescr.orelse d₁ d₂ => orelse <$> compileParserDescr d₁ <*> compileParserDescr d₂ | ParserDescr.optional d => optional <$> compileParserDescr d @@ -1772,35 +1803,16 @@ def compileParserDescr (categories : ParserCategories) : ParserDescr → Except | ParserDescr.nameLit => pure $ nameLit | ParserDescr.ident => pure $ ident | ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol tk includeIdent +| ParserDescr.parser constName => do + (_, p) ← mkParserOfConstantAux env categories constName compileParserDescr; + pure p | ParserDescr.cat catName prec => match categories.find? catName with | some _ => pure $ categoryParser catName prec | none => throwUnknownParserCategory catName -unsafe def mkParserOfConstantUnsafe (env : Environment) (categories : ParserCategories) (constName : Name) : Except String (Bool × Parser) := -match env.find? constName with -| none => throw ("unknow constant '" ++ toString constName ++ "'") -| some info => - match info.type with - | Expr.const `Lean.Parser.TrailingParser _ _ => do - p ← env.evalConst Parser constName; - pure ⟨false, p⟩ - | Expr.const `Lean.Parser.Parser _ _ => do - p ← env.evalConst Parser constName; - pure ⟨true, p⟩ - | Expr.const `Lean.ParserDescr _ _ => do - d ← env.evalConst ParserDescr constName; - p ← compileParserDescr categories d; - pure ⟨true, p⟩ - | Expr.const `Lean.TrailingParserDescr _ _ => do - d ← env.evalConst TrailingParserDescr constName; - p ← compileParserDescr categories d; - pure ⟨false, p⟩ - | _ => throw ("unexpected parser type at '" ++ toString constName ++ "' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected") - -@[implementedBy mkParserOfConstantUnsafe] -constant mkParserOfConstant (env : Environment) (categories : ParserCategories) (constName : Name) : Except String (Bool × Parser) := -arbitrary _ +def mkParserOfConstant (env : Environment) (categories : ParserCategories) (constName : Name) : Except String (Bool × Parser) := +mkParserOfConstantAux env categories constName (compileParserDescr env categories) private def ParserExtension.addImported (env : Environment) (es : Array (Array ParserExtensionOleanEntry)) : IO ParserExtensionState := do s ← ParserExtension.mkInitial; diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean index f223804f06..a2f720163e 100644 --- a/tests/lean/run/termParserAttr.lean +++ b/tests/lean/run/termParserAttr.lean @@ -15,6 +15,8 @@ open Lean.Parser @[termParser] def tst := parser! "(|" >> termParser >> optional (symbol ", " >> termParser) >> "|)" +def tst2 : Parser := symbol "(||" >> termParser >> symbol "||)" + @[termParser] def boo : ParserDescr := ParserDescr.node `boo 10 (ParserDescr.andthen @@ -23,6 +25,9 @@ ParserDescr.node `boo 10 (ParserDescr.cat `term 0) (ParserDescr.symbol "|]"))) +@[termParser] def boo2 : ParserDescr := +ParserDescr.node `boo2 10 (ParserDescr.parser `tst2) + open Lean.Elab.Term @[termElab tst] def elabTst : TermElab := @@ -34,8 +39,16 @@ adaptExpander $ fun stx => match_syntax stx with fun stx expected? => elabTerm (stx.getArg 1) expected? +@[termElab boo2] def elabBool2 : TermElab := +adaptExpander $ fun stx => match_syntax stx with + | `((|| $e ||)) => `($e + 1) + | _ => throwUnsupportedSyntax + #eval run "#check [| @id.{1} Nat |]" #eval run "#check (| id 1 |)" +#eval run "#check (|| id 1 ||)" + + -- #eval run "#check (| id 1, id 1 |)" -- it will fail @[termElab tst] def elabTst2 : TermElab :=