From f2231ebbc081dec1527925df693b2470c3d2c2a3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2020 09:37:36 -0800 Subject: [PATCH] feat: improve `macro` command parser --- src/Init/Lean/Parser/Parser.lean | 27 +++++++++++++++++++++++++++ src/Init/Lean/Parser/Syntax.lean | 30 +++++++++++++++++++----------- src/Init/Lean/Parser/Term.lean | 7 +++++-- tests/lean/run/newfrontend1.lean | 7 +++++++ 4 files changed, 58 insertions(+), 13 deletions(-) diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index be83a8c547..f74ba9ad5c 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1083,6 +1083,20 @@ fun _ c s => @[inline] def rawIdentNoAntiquot {k : ParserKind} : Parser k := { fn := fun _ => rawIdentFn } +def identEqFn {k : ParserKind} (id : Name) : ParserFn k := +fun _ c s => + let iniPos := s.pos; + let s := tokenFn c s; + if s.hasError then + s.mkErrorAt "identifier" iniPos + else match s.stxStack.back with + | Syntax.ident _ _ val _ => if val != id then s.mkErrorAt ("expected identifier '" ++ toString id ++ "'") iniPos else s + | _ => s.mkErrorAt "identifier" iniPos + +@[inline] def identEq {k : ParserKind} (id : Name) : Parser k := +{ fn := identEqFn id, + info := mkAtomicInfo "ident" } + def quotedSymbolFn {k : ParserKind} : ParserFn k := nodeFn `quotedSymbol (andthenFn (andthenFn (chFn '`') (rawFn (fun _ => takeUntilFn (fun c => c == '`')))) (chFn '`' true)) @@ -1365,6 +1379,19 @@ fun rbp ctx s => categoryParserFnExtension.getState ctx.env catName rbp ctx s def categoryParser {k} (catName : Name) (rbp : Nat) : Parser k := { fn := fun _ => categoryParserFn catName rbp } +def categoryParserOfStackFn (offset : Nat) : ParserFn leading := +fun rbp ctx s => + let stack := s.stxStack; + if stack.size < offset + 1 then + s.mkUnexpectedError ("failed to determine parser category using syntax stack, stack is too small") + else + match stack.get! (stack.size - offset - 1) with + | Syntax.ident _ _ catName _ => categoryParserFn catName rbp ctx s + | _ => s.mkUnexpectedError ("failed to determine parser category using syntax stack, the specified element on the stack is not an identifier") + +def categoryParserOfStack {k} (offset : Nat) (rbp : Nat := 0) : Parser k := +{ fn := fun _ => categoryParserOfStackFn offset rbp } + def mkBuiltinTokenTable : IO (IO.Ref TokenTable) := IO.mkRef {} @[init mkBuiltinTokenTable] constant builtinTokenTable : IO.Ref TokenTable := arbitrary _ diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean index 824f8f870e..80546545e1 100644 --- a/src/Init/Lean/Parser/Syntax.lean +++ b/src/Init/Lean/Parser/Syntax.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude import Init.Lean.Parser.Command +import Init.Lean.Parser.Tactic namespace Lean namespace Parser @@ -16,13 +17,15 @@ registerBuiltinParserAttribute `builtinSyntaxParser `syntax leadingIdentAsSymbol @[inline] def syntaxParser {k : ParserKind} (rbp : Nat := 0) : Parser k := categoryParser `syntax rbp -namespace Syntax def maxPrec := parser! nonReservedSymbol "max" true def precedenceLit : Parser := numLit <|> maxPrec def «precedence» := parser! ":" >> precedenceLit +def optPrecedence := optional (try «precedence») + +namespace Syntax @[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")" -@[builtinSyntaxParser] def cat := parser! ident >> optional (try «precedence») -@[builtinSyntaxParser] def atom := parser! strLit >> optional (try «precedence») +@[builtinSyntaxParser] def cat := parser! ident >> optPrecedence +@[builtinSyntaxParser] def atom := parser! strLit >> optPrecedence @[builtinSyntaxParser] def num := parser! nonReservedSymbol "num" @[builtinSyntaxParser] def str := parser! nonReservedSymbol "str" @[builtinSyntaxParser] def char := parser! nonReservedSymbol "char" @@ -41,7 +44,7 @@ end Syntax namespace Command -def quotedSymbolPrec := parser! quotedSymbol >> optional Syntax.precedence +def quotedSymbolPrec := parser! quotedSymbol >> optPrecedence def «prefix» := parser! "prefix" def «infix» := parser! "infix" def «infixl» := parser! "infixl" @@ -51,17 +54,22 @@ def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «p -- TODO delete reserve @[builtinCommandParser] def «reserve» := parser! "reserve " >> mixfixKind >> quotedSymbolPrec def mixfixSymbol := quotedSymbolPrec <|> unquotedSymbol -@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> mixfixSymbol >> unicodeSymbol "⇒" "=>" >> termParser -def strLitPrec := parser! strLit >> optional Syntax.precedence -def identPrec := parser! ident >> optional Syntax.precedence +@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> mixfixSymbol >> darrow >> termParser +def strLitPrec := parser! strLit >> optPrecedence +def identPrec := parser! ident >> optPrecedence -@[builtinCommandParser] def «notation» := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> unicodeSymbol "⇒" "=>" >> termParser +@[builtinCommandParser] def «notation» := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> darrow >> termParser @[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> many1Indent Term.matchAlt "'match' alternatives must be indented" @[builtinCommandParser] def «syntax» := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident @[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident -def macroArgSimple := parser! ident >> ":" >> ident >> optional Syntax.precedence -def macroArg := try (strLitPrec <|> macroArgSimple) -@[builtinCommandParser] def «macro» := parser! "macro " >> (strLitPrec <|> identPrec) >> many macroArg >> " : " >> ident >> unicodeSymbol "⇒" "=>" >> termParser +def macroArgSimple := parser! ident >> ":" >> ident >> optPrecedence +def macroArg := try strLitPrec <|> try macroArgSimple +def macroHead := try strLitPrec <|> try identPrec +def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")" +def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")" +def macroTailDefault : Parser := try (" : " >> ident) >> darrow >> "`(" >> categoryParserOfStack 2 >> ")" +def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault +@[builtinCommandParser] def «macro» := parser! "macro " >> macroHead >> many macroArg >> macroTail end Command diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 2b2c4c2ced..f1e129c481 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -9,6 +9,9 @@ import Init.Lean.Parser.Level namespace Lean namespace Parser + +def darrow : Parser := unicodeSymbol "⇒" "=>" + namespace Term /- Helper functions for defining simple parsers -/ @@ -53,7 +56,7 @@ def haveAssign := parser! " := " >> termParser @[builtinTermParser] def «have» := parser! "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser @[builtinTermParser] def «suffices» := parser! "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser @[builtinTermParser] def «show» := parser! "show " >> termParser >> fromTerm -@[builtinTermParser] def «fun» := parser! unicodeSymbol "λ" "fun" >> many1 (termParser appPrec) >> unicodeSymbol "⇒" "=>" >> termParser +@[builtinTermParser] def «fun» := parser! unicodeSymbol "λ" "fun" >> many1 (termParser appPrec) >> darrow >> termParser def structInstField := parser! ident >> " := " >> termParser def structInstSource := parser! ".." >> optional termParser @[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (ident >> " . ")) >> sepBy (structInstField <|> structInstSource) ", " true >> "}" @@ -75,7 +78,7 @@ def bracktedBinder (requireType := false) := explicitBinder requireType <|> impl @[builtinTermParser] def depArrow := parser! bracktedBinder true >> unicodeSymbolCheckPrec " → " " -> " 25 >> termParser def simpleBinder := parser! many1 binderIdent @[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracktedBinder) >> ", " >> termParser -def matchAlt := parser! " | " >> sepBy1 termParser ", " >> unicodeSymbol "⇒" "=>" >> termParser +def matchAlt := parser! " | " >> sepBy1 termParser ", " >> darrow >> termParser @[builtinTermParser] def «match» := parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> many1Indent matchAlt "'match' alternatives must be indented" @[builtinTermParser] def «nomatch» := parser! "nomatch " >> termParser @[builtinTermParser] def «parser!» := parser! "parser! " >> termParser diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index f6cdb0d4ad..69d98ebc33 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -62,3 +62,10 @@ begin intro2; assumption end + +-- set_option trace.Elab true +-- set_option syntaxMaxDepth 100 + +-- macro intro3 : tactic => `(intro; intro) +-- macro check2 x: term : command => `(#check $x #check $x) +-- macro foo x: term ", " y: term : term => `($x + $y + $x)