diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean index c8093afbd3..fa61abb191 100644 --- a/library/init/lean/parser/combinators.lean +++ b/library/init/lean/parser/combinators.lean @@ -19,7 +19,7 @@ variables {α : Type} {m : Type → Type} local notation `parser` := m syntax variables [monad m] [monad_except (parsec.message syntax) m] [monad_parsec syntax m] [alternative m] -def node' (k : option syntax_node_kind) (rs : list parser) : parser := +def node (k : syntax_node_kind) (rs : list parser) : parser := do args ← rs.mfoldl (λ (p : list syntax) r, do args ← pure p, -- on error, append partial syntax tree to previous successful parses and rethrow @@ -30,10 +30,9 @@ do args ← rs.mfoldl (λ (p : list syntax) r, do ) [], pure $ syntax.node ⟨k, args.reverse⟩ -@[reducible] def seq : list parser → parser := node' none -@[reducible] def node (k : syntax_node_kind) : list parser → parser := node' (some k) +@[reducible] def seq : list parser → parser := node no_kind -instance node'.tokens (k) (rs : list parser) [parser.has_tokens rs] : parser.has_tokens (node' k rs) := +instance node.tokens (k) (rs : list parser) [parser.has_tokens rs] : parser.has_tokens (node k rs) := ⟨tokens rs⟩ instance node.view (k) (rs : list parser) [i : has_view α k] : parser.has_view α (node k rs) := diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean index dac3ae8538..27bebebf05 100644 --- a/library/init/lean/parser/syntax.lean +++ b/library/init/lean/parser/syntax.lean @@ -31,6 +31,8 @@ structure syntax_node_kind := (name : name) @[pattern] def choice : syntax_node_kind := ⟨`lean.parser.choice⟩ +-- TODO(Sebastian): replace `option syntax_kind` using this special kind +@[pattern] def no_kind : syntax_node_kind := ⟨`lean.parser.no_kind⟩ /- Parsers create `syntax_node`'s with the following property: @@ -83,8 +85,8 @@ with to_format : syntax → format | (node {kind := none, args := args, ..}) := sbracket $ join_sep (to_format_lst args) line | stx@(node {kind := some kind, args := args, ..}) := - if kind.name = `lean.parser.ident - then to_fmt "`" ++ ident_to_format stx + if kind.name = `lean.parser.no_kind then sbracket $ join_sep (to_format_lst args) line + else if kind.name = `lean.parser.ident then to_fmt "`" ++ ident_to_format stx else let shorter_name := kind.name.replace_prefix `lean.parser name.anonymous in paren $ join_sep (to_fmt shorter_name :: to_format_lst args) line | missing := ""