From bdff53fdf5d0c2c972af294ee6188ce6e37f2681 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 1 Oct 2020 09:55:39 +0200 Subject: [PATCH] feat: use ppLine --- src/Lean/Parser/Command.lean | 20 ++++++++++---------- src/Lean/Parser/Module.lean | 4 ++-- src/Lean/Parser/Term.lean | 4 ++-- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index e9cdecb741..53c8d00384 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -24,18 +24,18 @@ def commentBody : Parser := @[combinatorParenthesizer commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken @[combinatorFormatter commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous -def docComment := parser! "/--" >> commentBody +def docComment := parser! "/--" >> commentBody >> ppLine def «private» := parser! "private " def «protected» := parser! "protected " def visibility := «private» <|> «protected» def «noncomputable» := parser! "noncomputable " def «unsafe» := parser! "unsafe " def «partial» := parser! "partial " -def declModifiers := parser! optional docComment >> optional Term.«attributes» >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial» +def declModifiers (inline : Bool) := parser! optional docComment >> optional (Term.«attributes» >> if inline then skip else ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial» def declId := parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}") def declSig := parser! many Term.bracketedBinder >> Term.typeSpec def optDeclSig := parser! many Term.bracketedBinder >> Term.optType -def declValSimple := parser! " := " >> termParser +def declValSimple := parser! " :=\n" >> termParser def declValEqns := parser! Term.matchAlts false def declVal := declValSimple <|> declValEqns def «abbrev» := parser! "abbrev " >> declId >> optDeclSig >> declVal @@ -46,20 +46,20 @@ def «instance» := parser! "instance " >> optional declId >> declSig >> d def «axiom» := parser! "axiom " >> declId >> declSig def «example» := parser! "example " >> declSig >> declVal def inferMod := parser! try ("{" >> "}") -def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig +def ctor := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many ctor def classInductive := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor -def structExplicitBinder := parser! try (declModifiers >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")" -def structImplicitBinder := parser! try (declModifiers >> "{") >> many1 ident >> optional inferMod >> declSig >> "}" -def structInstBinder := parser! try (declModifiers >> "[") >> many1 ident >> optional inferMod >> declSig >> "]" -def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder) -def structCtor := parser! try (declModifiers >> ident >> optional inferMod >> " :: ") +def structExplicitBinder := parser! try (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")" +def structImplicitBinder := parser! try (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}" +def structInstBinder := parser! try (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]" +def structFields := parser! many (ppLine >> (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)) +def structCtor := parser! try (declModifiers true >> ident >> optional inferMod >> " :: ") def structureTk := parser! "structure " def classTk := parser! "class " def «extends» := parser! " extends " >> sepBy1 termParser ", " def «structure» := parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields @[builtinCommandParser] def declaration := parser! -declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure») +declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure») @[builtinCommandParser] def «section» := parser! "section " >> optional ident @[builtinCommandParser] def «namespace» := parser! "namespace " >> ident diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index 792460dc71..7724d2e848 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -12,13 +12,13 @@ namespace Parser namespace Module def «prelude» := parser! "prelude" def «import» := parser! "import " >> optional "runtime" >> ident -def header := parser! optional «prelude» >> many «import» +def header := parser! optional («prelude» >> ppLine) >> many («import» >> ppLine) >> ppLine /-- Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition for it in order to auto-generate helpers such as the pretty printer. -/ @[runParserAttributeHooks] -def module := parser! header >> many commandParser +def module := parser! header >> many (commandParser >> ppLine >> ppLine) def updateTokens (c : ParserContext) : ParserContext := { c with diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index cf92c461c7..d1819026ed 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -129,8 +129,8 @@ nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $ def matchAlts (optionalFirstBar := true) : Parser := parser! withPosition $ - (if optionalFirstBar then optional "| " else "| ") >> - sepBy1 matchAlt (checkColGe "alternatives must be indented" >> "|") + ppLine >> (if optionalFirstBar then optional "| " else "| ") >> + sepBy1 matchAlt (ppLine >> checkColGe "alternatives must be indented" >> "|") def matchDiscr := parser! optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser