max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf(library/init/lean/parser/combinators): make node semireducible

Browse source
This commit is contained in:
Sebastian Ullrich 2018-10-30 15:43:31 +01:00
parent 0d7ea62f9a
commit 74bd182bc8
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/init/lean/parser/combinators.lean
View file

@ -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) :=

6
library/init/lean/parser/syntax.lean
View file

@ -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 := "<missing>"