diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 4e53536ecd..877bba95c5 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1709,6 +1709,8 @@ inductive ParserDescr where | cat (catName : Name) (rbp : Nat) | parser (declName : Name) | nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : ParserDescr) + | sepBy (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false) + | sepBy1 (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false) instance : Inhabited ParserDescr where default := ParserDescr.symbol "" diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 9aa0aa96d9..d9fc00a185 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -74,8 +74,8 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax | _ => throwErrorAt stx "too many antiquotations in antiquotation scope; don't be greedy" let arr ← if k == `sepBy then - let Syntax.atom _ sep ← (getAntiquotScopeSuffix arg)[0] | unreachable! - `(mkSepArray $arr (mkAtom $(Syntax.mkStrLit sep))) + let Syntax.atom _ sep ← getAntiquotScopeSuffix arg | unreachable! + `(mkSepArray $arr (mkAtom $(Syntax.mkStrLit (sep.dropRight 1)))) else arr let arr ← bindLets arr `(Array.appendCore $args $arr) diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 0eb6107de7..7abc1021e9 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -96,17 +96,13 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := withRef s let sep := stx[3] let psep ← if stx[4].isNone then `(ParserDescr.symbol $sep) else toParserDescrAux stx[4][1] let allowTrailingSep := !stx[5].isNone - --`(ParserDescr.sepBy $p $sep $psep $(quote allowTrailingSep)) - let sepBy := if allowTrailingSep then `sepByT else `sepBy - `(ParserDescr.binary $(quote sepBy) $p $psep) + `(ParserDescr.sepBy $p $sep $psep $(quote allowTrailingSep)) else if kind == `Lean.Parser.Syntax.sepBy1 then let p ← withNestedParser $ toParserDescrAux stx[1] let sep := stx[3] let psep ← if stx[4].isNone then `(ParserDescr.symbol $sep) else toParserDescrAux stx[4][1] let allowTrailingSep := !stx[5].isNone - --`(ParserDescr.sepBy1 $p $sep $psep $(quote allowTrailingSep)) - let sepBy := if allowTrailingSep then `sepBy1T else `sepBy1 - `(ParserDescr.binary $(quote sepBy) $p $psep) + `(ParserDescr.sepBy1 $p $sep $psep $(quote allowTrailingSep)) else if kind == `Lean.Parser.Syntax.cat then let cat := stx[0].getId.eraseMacroScopes let prec? : Option Nat := expandOptPrecedence stx[1] diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index 7e0e1bc2df..fdc04a5414 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -33,12 +33,8 @@ builtin_initialize registerAlias "optional" optional registerAlias "withPosition" withPosition registerAlias "interpolatedStr" interpolatedStr - registerAlias "sepBy" sepBy - registerAlias "sepBy1" sepBy1 registerAlias "orelse" orelse registerAlias "andthen" andthen - registerAlias "sepByT" (sepBy (allowTrailingSep := true)) - registerAlias "sepBy1T" (sepBy1 (allowTrailingSep := true)) end Parser @@ -58,6 +54,23 @@ def mkAntiquot.parenthesizer (name : String) (kind : Option SyntaxNodeKind) (ano @[builtinParenthesizer charLit] def charLit.parenthesizer : Parenthesizer := Parser.Term.char.parenthesizer @[builtinParenthesizer strLit] def strLit.parenthesizer : Parenthesizer := Parser.Term.str.parenthesizer +open Lean.Parser + +@[export lean_pretty_printer_parenthesizer_interpret_parser_descr] +unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer + | ParserDescr.const n => getConstAlias parenthesizerAliasesRef n + | ParserDescr.unary n d => return (← getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d) + | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) + | ParserDescr.node k prec d => return leadingNode.parenthesizer k prec (← interpretParserDescr d) + | ParserDescr.nodeWithAntiquot _ k d => return node.parenthesizer k (← interpretParserDescr d) + | ParserDescr.sepBy p sep psep trail => return sepBy.parenthesizer (← interpretParserDescr p) sep (← interpretParserDescr psep) trail + | ParserDescr.sepBy1 p sep psep trail => return sepBy1.parenthesizer (← interpretParserDescr p) sep (← interpretParserDescr psep) trail + | ParserDescr.trailingNode k prec d => return trailingNode.parenthesizer k prec (← interpretParserDescr d) + | ParserDescr.symbol tk => return symbol.parenthesizer tk + | ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol.parenthesizer tk includeIdent + | ParserDescr.parser constName => combinatorParenthesizerAttribute.runDeclFor constName + | ParserDescr.cat catName prec => return categoryParser.parenthesizer catName prec + end Parenthesizer namespace Formatter @@ -72,6 +85,23 @@ def mkAntiquot.formatter (name : String) (kind : Option SyntaxNodeKind) (anonymo @[builtinFormatter charLit] def charLit.formatter : Formatter := Parser.Term.char.formatter @[builtinFormatter strLit] def strLit.formatter : Formatter := Parser.Term.str.formatter +open Lean.Parser + +@[export lean_pretty_printer_formatter_interpret_parser_descr] +unsafe def interpretParserDescr : ParserDescr → CoreM Formatter + | ParserDescr.const n => getConstAlias formatterAliasesRef n + | ParserDescr.unary n d => return (← getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d) + | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) + | ParserDescr.node k prec d => return node.formatter k (← interpretParserDescr d) + | ParserDescr.nodeWithAntiquot _ k d => return node.formatter k (← interpretParserDescr d) + | ParserDescr.sepBy p sep psep trail => return sepBy.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail + | ParserDescr.sepBy1 p sep psep trail => return sepBy1.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail + | ParserDescr.trailingNode k prec d => return trailingNode.formatter k prec (← interpretParserDescr d) + | ParserDescr.symbol tk => return symbol.formatter tk + | ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol.formatter tk + | ParserDescr.parser constName => combinatorFormatterAttribute.runDeclFor constName + | ParserDescr.cat catName prec => return categoryParser.formatter catName + end Formatter end PrettyPrinter end Lean diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index fdcc8a2d63..fac543b363 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1643,6 +1643,15 @@ def nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : Parser) (anony /- End of Antiquotations -/ /- ===================== -/ +def sepByElemParser (p : Parser) (sep : String) : Parser := + withAntiquot (mkAntiquotScope `sepBy p (symbol (sep.trim ++ "*"))) p + +def sepBy (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser := + sepByNoAntiquot (sepByElemParser p sep) psep allowTrailingSep + +def sepBy1 (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser := + sepBy1NoAntiquot (sepByElemParser p sep) psep allowTrailingSep + def categoryParserOfStackFn (offset : Nat) : ParserFn := fun ctx s => let stack := s.stxStack if stack.size < offset + 1 then diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index a24e4f1a56..ff924431cc 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -77,9 +77,7 @@ def elseIf := atomic (group (withPosition (" else " >> checkLineEq >> " if "))) @[builtinDoElemParser] def doUnless := parser! "unless " >> withForbidden "do" termParser >> "do " >> doSeq @[builtinDoElemParser] def doFor := parser! "for " >> termParser >> " in " >> withForbidden "do" termParser >> "do " >> doSeq -/- `match`-expression where the right-hand-side of alternatives is a `doSeq` instead of a `term` -/ -def doMatchAlt : Parser := parser! sepBy1 termParser ", " >> darrow >> doSeq -def doMatchAlts : Parser := parser! withPosition $ (optional "| ") >> sepBy1 doMatchAlt (checkColGe "alternatives must be indented" >> "| ") +def doMatchAlts := matchAlts (rhsParser := doSeq) @[builtinDoElemParser] def doMatch := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts def doCatch := parser! atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 00a46de11c..df7e35fcbe 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -275,6 +275,8 @@ partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias parserAliasesRef n) (← visit d₁) (← visit d₂) | ParserDescr.node k prec d => return leadingNode k prec (← visit d) | ParserDescr.nodeWithAntiquot n k d => return nodeWithAntiquot n k (← visit d) (anonymous := true) + | ParserDescr.sepBy p sep psep trail => return sepBy (← visit p) sep (← visit psep) trail + | ParserDescr.sepBy1 p sep psep trail => return sepBy1 (← visit p) sep (← visit psep) trail | ParserDescr.trailingNode k prec d => return trailingNode k prec (← visit d) | ParserDescr.symbol tk => return symbol tk | ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol tk includeIdent diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index d68163acd7..d64983f86d 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -14,7 +14,7 @@ namespace Parser -- synthesize pretty printers for parsers declared prior to `Lean.PrettyPrinter` -- (because `Parser.Extension` depends on them) attribute [runBuiltinParserAttributeHooks] - leadingNode termParser commandParser mkAntiquot nodeWithAntiquot + leadingNode termParser commandParser mkAntiquot nodeWithAntiquot sepBy sepBy1 @[runBuiltinParserAttributeHooks] def optional (p : Parser) : Parser := optionalNoAntiquot (withAntiquot (mkAntiquotScope `optional p (symbol "?")) p) @@ -25,16 +25,6 @@ attribute [runBuiltinParserAttributeHooks] @[runBuiltinParserAttributeHooks] def many1 (p : Parser) : Parser := many1NoAntiquot (withAntiquot (mkAntiquotScope `many p (symbol "*")) p) --- all the separators you could ever want -@[runBuiltinParserAttributeHooks] def sepByScopeSuffixes : Parser := -parser! (symbol "," <|> symbol ";" <|> symbol "|") >> symbol "*" - -@[runBuiltinParserAttributeHooks] def sepBy (p psep : Parser) (allowTrailingSep : Bool := false) : Parser := - sepByNoAntiquot (withAntiquot (mkAntiquotScope `sepBy p sepByScopeSuffixes) p) psep allowTrailingSep - -@[runBuiltinParserAttributeHooks] def sepBy1 (p psep : Parser) (allowTrailingSep : Bool := false) : Parser := - sepBy1NoAntiquot (withAntiquot (mkAntiquotScope `sepBy p sepByScopeSuffixes) p) psep allowTrailingSep - @[runBuiltinParserAttributeHooks] def ident : Parser := withAntiquot (mkAntiquot "ident" identKind) identNoAntiquot @@ -136,10 +126,6 @@ builtin_initialize registerAlias "many" many.parenthesizer registerAlias "many1" many1.parenthesizer registerAlias "optional" optional.parenthesizer - registerAlias "sepBy" sepBy.parenthesizer - registerAlias "sepBy1" sepBy1.parenthesizer - registerAlias "sepByT" sepBy.parenthesizer - registerAlias "sepBy1T" sepBy1.parenthesizer open PrettyPrinter.Formatter (registerAlias) in builtin_initialize @@ -152,9 +138,5 @@ builtin_initialize registerAlias "many" many.formatter registerAlias "many1" many1.formatter registerAlias "optional" optional.formatter - registerAlias "sepBy" sepBy.formatter - registerAlias "sepBy1" sepBy1.formatter - registerAlias "sepByT" sepBy.formatter - registerAlias "sepBy1T" sepBy1.formatter end Lean diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 941dd23037..eb399f641f 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -27,7 +27,7 @@ def tacticSeq := /- Raw sequence for quotation and grouping -/ def seq1 := - node `Lean.Parser.Tactic.seq1 $ sepBy1 tacticParser ";\n" true + node `Lean.Parser.Tactic.seq1 $ sepBy1 tacticParser ";\n" (allowTrailingSep := true) end Tactic @@ -109,14 +109,14 @@ def simpleBinder := parser! many1 binderIdent >> optType @[builtinTermParser] def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser -def matchAlt : Parser := +def matchAlt (rhsParser : Parser := termParser) : Parser := nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $ - sepBy1 termParser ", " >> darrow >> termParser + sepBy1 termParser ", " >> darrow >> rhsParser -def matchAlts (optionalFirstBar := true) : Parser := +def matchAlts (rhsParser : Parser := termParser) (optionalFirstBar := true) : Parser := parser! ppDedent $ withPosition $ ppLine >> (if optionalFirstBar then optional "| " else group "| ") >> - sepBy1 (ppIndent matchAlt) (ppLine >> checkColGe "alternatives must be indented" >> "| ") + sepBy1 (ppIndent <| matchAlt rhsParser) "|" (ppLine >> checkColGe "alternatives must be indented" >> "| ") def matchDiscr := parser! optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser @@ -128,7 +128,7 @@ def funSimpleBinder := atomic (lookahead (many1 binderIdent >> " : ")) >> simp def funBinder : Parser := funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec -- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser) -@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts false) +@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts (optionalFirstBar := false)) def optExprPrecedence := optional (atomic ":" >> termParser maxPrec) @[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser @@ -142,7 +142,7 @@ def simpleBinderWithoutType := node `Lean.Parser.Term.simpleBinder (many1 binder def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType def letIdDecl := node `Lean.Parser.Term.letIdDecl $ atomic (letIdLhs >> " := ") >> termParser def letPatDecl := node `Lean.Parser.Term.letPatDecl $ atomic (termParser >> pushNone >> optType >> " := ") >> termParser -def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts false +def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts (optionalFirstBar := false) -- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl` def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl)) @[builtinTermParser] def «let» := parser!:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser @@ -163,7 +163,7 @@ def «letrec» := parser!:leadPrec withPosition (group ("let " >> nonReservedSym @[runBuiltinParserAttributeHooks] def whereDecls := parser! "where " >> many1Indent (group (optional «attributes» >> letDecl >> optional ";")) @[runBuiltinParserAttributeHooks] -def matchAltsWhereDecls := parser! matchAlts false >> optional whereDecls +def matchAltsWhereDecls := parser! matchAlts (optionalFirstBar := false) >> optional whereDecls @[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser maxPrec @[builtinTermParser] def nativeDecide := parser! "nativeDecide!" diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 6e1c483c5e..0c9c881836 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -121,6 +121,8 @@ def compileEmbeddedParsers : ParserDescr → MetaM Unit | ParserDescr.parser constName => discard $ compileParserExpr ctx (mkConst constName) (force := false) | ParserDescr.node _ _ d => compileEmbeddedParsers d | ParserDescr.nodeWithAntiquot _ _ d => compileEmbeddedParsers d + | ParserDescr.sepBy p _ psep _ => compileEmbeddedParsers p *> compileEmbeddedParsers psep + | ParserDescr.sepBy1 p _ psep _ => compileEmbeddedParsers p *> compileEmbeddedParsers psep | ParserDescr.trailingNode _ _ d => compileEmbeddedParsers d | ParserDescr.symbol _ => pure () | ParserDescr.nonReservedSymbol _ _ => pure () diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 24d7efd012..5930ade29c 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -456,19 +456,6 @@ builtin_initialize registerAlias "orelse" orelse.formatter registerAlias "andthen" andthen.formatter -@[export lean_pretty_printer_formatter_interpret_parser_descr] -unsafe def interpretParserDescr : ParserDescr → CoreM Formatter - | ParserDescr.const n => getConstAlias formatterAliasesRef n - | ParserDescr.unary n d => return (← getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d) - | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) - | ParserDescr.node k prec d => return node.formatter k (← interpretParserDescr d) - | ParserDescr.nodeWithAntiquot _ k d => return node.formatter k (← interpretParserDescr d) - | ParserDescr.trailingNode k prec d => return trailingNode.formatter k prec (← interpretParserDescr d) - | ParserDescr.symbol tk => return symbol.formatter tk - | ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol.formatter tk - | ParserDescr.parser constName => combinatorFormatterAttribute.runDeclFor constName - | ParserDescr.cat catName prec => return categoryParser.formatter catName - end Formatter open Formatter diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index cc35299cc3..f76c9d40a4 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -511,19 +511,6 @@ builtin_initialize registerAlias "orelse" orelse.parenthesizer registerAlias "andthen" andthen.parenthesizer -@[export lean_pretty_printer_parenthesizer_interpret_parser_descr] -unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer - | ParserDescr.const n => getConstAlias parenthesizerAliasesRef n - | ParserDescr.unary n d => return (← getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d) - | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) - | ParserDescr.node k prec d => return leadingNode.parenthesizer k prec (← interpretParserDescr d) - | ParserDescr.nodeWithAntiquot _ k d => return node.parenthesizer k (← interpretParserDescr d) - | ParserDescr.trailingNode k prec d => return trailingNode.parenthesizer k prec (← interpretParserDescr d) - | ParserDescr.symbol tk => return symbol.parenthesizer tk - | ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol.parenthesizer tk includeIdent - | ParserDescr.parser constName => combinatorParenthesizerAttribute.runDeclFor constName - | ParserDescr.cat catName prec => return categoryParser.parenthesizer catName prec - end Parenthesizer open Parenthesizer