From 41c0bc87fd22d821032a88e369bd37c78151fc50 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 22 Sep 2018 21:24:38 -0700 Subject: [PATCH] refactor(library/init/lean/parser): make views shallow via `tysyntax` --- library/init/lean/parser/basic.lean | 13 +++++-- library/init/lean/parser/combinators.lean | 45 +++++++++-------------- library/init/lean/parser/command.lean | 29 ++++++++------- library/init/lean/parser/term.lean | 2 +- library/init/lean/parser/token.lean | 14 ++++--- src/frontends/lean/elaborator.cpp | 28 +++++++------- 6 files changed, 67 insertions(+), 64 deletions(-) diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index 24cfdcfa75..e89563dd65 100644 --- a/library/init/lean/parser/basic.lean +++ b/library/init/lean/parser/basic.lean @@ -79,9 +79,16 @@ protected class has_view (r : ρ) (α : out_param Type) := instance has_view.default (r : ρ) : inhabited (parser.has_view r syntax) := ⟨{ view := some, review := id }⟩ -class syntax_node_kind.has_view (k : syntax_node_kind) (α : out_param Type) := -(view : syntax → option α) -(review : α → syntax) +abbreviation tysyntax (α : Type) := syntax + +class tysyntax.is_view (α : Type) := +(view : tysyntax α → option α) +(review : α → tysyntax α) + +export tysyntax.is_view (view review) + +def view_with (α : Type) [tysyntax.is_view α] (stx : syntax) : option α := +view (stx : tysyntax α) def message_of_parsec_message {μ : Type} (cfg : parser_config) (msg : parsec.message μ) : message := -- FIXME: translate position diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean index 9e8415fd6b..cf0c22625b 100644 --- a/library/init/lean/parser/combinators.lean +++ b/library/init/lean/parser/combinators.lean @@ -32,12 +32,12 @@ do (args, _) ← rs.mfoldl (λ (p : list syntax × nat) 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' k +@[reducible] def node (k : syntax_node_kind) (α : Type) : list parser → parser := node' k 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 : syntax_node_kind.has_view k α] : parser.has_view (node k rs) α := +instance node.view (k) (α : Type) (rs : list parser) [i : tysyntax.is_view α] : parser.has_view (node k α rs) α := { view := i.view, review := i.review } private def many1_aux (p : parser) : list syntax → nat → parser @@ -54,12 +54,14 @@ do rem ← remaining, many1_aux r [] (rem+1) instance many1.tokens (r : parser) [parser.has_tokens r] : parser.has_tokens (many1 r) := ⟨tokens r⟩ -instance many1.view (r : parser) [parser.has_view r α] : parser.has_view (many1 r) (list α) := +instance list.is_view : tysyntax.is_view (list (tysyntax α)) := { view := λ stx, match stx with - | syntax.missing := list.ret <$> view r syntax.missing - | syntax.node ⟨none, stxs⟩ := stxs.mmap (view r) + | syntax.node ⟨none, stxs⟩ := pure stxs | _ := failure, - review := λ as, syntax.node ⟨none, as.map (review r)⟩ } + review := λ as, syntax.node ⟨none, as⟩ } + +instance many1.view (r : parser) [parser.has_view r α] : parser.has_view (many1 r) (list (tysyntax α)) := +{..list.is_view} def many (r : parser) : parser := many1 r <|> pure (syntax.node ⟨none, []⟩) @@ -67,7 +69,7 @@ many1 r <|> pure (syntax.node ⟨none, []⟩) instance many.tokens (r : parser) [parser.has_tokens r] : parser.has_tokens (many r) := ⟨tokens r⟩ -instance many.view (r : parser) [has_view r α] : parser.has_view (many r) (list α) := +instance many.view (r : parser) [has_view r α] : parser.has_view (many r) (list (tysyntax α)) := {..many1.view r} private def sep_by_aux (p : m syntax) (sep : parser) (allow_trailing_sep : bool) : bool → list syntax → nat → parser @@ -134,29 +136,18 @@ do r ← optional $ instance optional.tokens (r : parser) [parser.has_tokens r] : parser.has_tokens (optional r) := ⟨tokens r⟩ -inductive optional_view (α : Type) -| some (a : α) : optional_view -| none {} : optional_view -| missing {} : optional_view - -namespace optional_view -instance : functor optional_view := -{ map := λ _ _ f v, match v with - | some a := some (f a) - | none := none - | missing := missing } -end optional_view - -instance optional.view (r : parser) [parser.has_view r α] : parser.has_view (optional r) (optional_view α) := +instance optional.is_view : tysyntax.is_view (option (tysyntax α)) := { view := λ stx, match stx with - | syntax.missing := pure optional_view.missing - | syntax.node ⟨none, []⟩ := pure optional_view.none - | syntax.node ⟨none, [stx]⟩ := optional_view.some <$> view r stx + | syntax.missing := failure + | syntax.node ⟨none, []⟩ := pure none + | syntax.node ⟨none, [stx]⟩ := pure (some stx) | _ := failure, review := λ a, match a with - | optional_view.some a := syntax.node ⟨none, [review r a]⟩ - | optional_view.none := syntax.node ⟨none, []⟩ - | optional_view.missing := syntax.missing } + | some a := syntax.node ⟨none, [a]⟩ + | none := syntax.node ⟨none, []⟩ } + +instance optional.view (r : parser) [parser.has_view r α] : parser.has_view (optional r) (option (tysyntax α)) := +{..optional.is_view} /-- Parse a list `[p1, ..., pn]` of parsers as `p1 <|> ... <|> pn`. Note that there is NO explicit encoding of which parser was chosen; diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index 5302bf6e24..e984456bf7 100644 --- a/library/init/lean/parser/command.lean +++ b/library/init/lean/parser/command.lean @@ -69,26 +69,29 @@ end parser namespace parser namespace «command» -open syntax_node_kind.has_view combinators notation_spec +open combinators notation_spec -- example macro -def mixfix.expand (stx : syntax) : option syntax := -do v ← view mixfix stx, +def mixfix.expand (stx : tysyntax mixfix.view) : option (tysyntax notation.view) := +do v ← view stx, -- TODO: reserved token case - notation_symbol.view.quoted {prec:=prec, ..} ← pure v.symbol, + notation_symbol.view.quoted quoted ← view v.symbol, + quoted ← view quoted, + prec ← view quoted.prec, -- `notation` allows more syntax after `:` than mixfix commands, so we have to do a small conversion let prec_to_action : precedence.view → action.view := - λ prec, {action := action_kind.view.prec prec.prec, ..prec}, - let spec := view.rules $ match v.kind with - | mixfix.kind.view.prefix _ := { - id := optional_view.none, - rules := [{ + λ prec, {action := review $ action_kind.view.prec prec.prec, ..prec}, + k ← view v.kind, + let spec := view.rules $ match k with + | mixfix.kind.view.prefix _ := review { + id := review none, + rules := review [review { symbol := v.symbol, - transition := optional_view.some $ transition.view.arg $ { - id := review ident {part := ident_part.view.default "b", suffix := optional_view.none}, - action := prec_to_action <$> prec}}]} + transition := review $ some $ review $ transition.view.arg $ review { + id := review {part := review $ ident_part.view.default "b", suffix := review none}, + action := review $ do prec ← prec, prec ← view prec, pure $ review $ prec_to_action prec}}]} | _ := sorry, - pure $ review «notation» ⟨"notation", spec, ":=", v.term⟩ + pure $ review ⟨"notation", review spec, ":=", v.term⟩ end «command» end parser diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index fa3c3f36af..9bc3c022ff 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -166,7 +166,7 @@ any_of [ @[derive parser.has_tokens parser.has_view] def sort_app.parser : trailing_term_parser := -do { l ← get_leading, guard (syntax_node_kind.has_view.view sort l).is_some } *> +do { l ← get_leading, guard (view_with sort.view l).is_some } *> node! sort_app [fn: get_leading, arg: monad_lift (level.parser max_prec)] @[derive parser.has_tokens parser.has_view] diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index 06a365873c..1cf86f24f1 100644 --- a/library/init/lean/parser/token.lean +++ b/library/init/lean/parser/token.lean @@ -182,7 +182,8 @@ lift $ try $ do { } "identifier" instance ident.parser.tokens : parser.has_tokens (ident.parser : parser) := default _ -instance ident.parser.view : parser.has_view (ident.parser : parser) syntax := default _ +instance ident.parser.view : parser.has_view (ident.parser : parser) ident.view := +{..ident.view.is_view} /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for parsing local tokens that have not been added to the token table (but may have @@ -197,11 +198,12 @@ lift $ try $ do stx ← token, let sym' := match stx with | syntax.atom ⟨_, sym'⟩ := some sym' - | syntax.node ⟨ident, _⟩ := - (match syntax_node_kind.has_view.view ident stx with - | some {part := ident_part.view.default (syntax.atom ⟨_, sym'⟩), - suffix := optional_view.none} := some sym' - | _ := none) + | syntax.node ⟨ident, _⟩ := do { + id ← view_with ident.view stx, + ident_part.view.default (syntax.atom ⟨_, sym'⟩) ← view id.part | none, + none ← view id.suffix | none, + some sym' + } | _ := none, when (sym' ≠ some sym) $ error "" (dlist.singleton (repr sym)) it, diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c213efcdaf..256a912749 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -3216,7 +3216,7 @@ expr elaborator::visit_node_macro(expr const & e, optional const & expecte if (!expected_type) throw elaborator_exception(e, "node!: expected type must be known"); expr exp = expected_type.value(); - sstream struc, stx_pat, binds, mk_args, view_pat, reviews; + sstream struc, stx_pat, mk_args, view_pat, reviews; unsigned i = 0; struc << "@[pattern] def " << esc_macro.to_string(); struc << " := {syntax_node_kind . name := `" << full_macro.to_string() << "}\n" @@ -3238,19 +3238,18 @@ expr elaborator::visit_node_macro(expr const & e, optional const & expecte if (!inst) throw elaborator_exception(e, sstream() << "Could not infer instance of parser.has_view for '" << r << "'"); - struc << "(«" << fname << "» : " << instantiate_mvars(m) << ")\n"; + struc << "(«" << fname << "» : tysyntax (" << instantiate_mvars(m) << "))\n"; if (i != 0) stx_pat << ", "; stx_pat << "stx" << i; - binds << "a" << i << " <- view (" << pp(r) << " : " << pp(exp) << ") stx" << i << ",\n"; - mk_args << "a" << i << " "; + mk_args << "stx" << i << " "; if (i != 0) view_pat << ", "; view_pat << "a" << i; if (i != 0) reviews << ", "; - reviews << "review (" << pp(r) << " : " << pp(exp) << ") a" << i; + reviews << "a" << i; i++; return mk_as_is(r); }; @@ -3271,10 +3270,9 @@ expr elaborator::visit_node_macro(expr const & e, optional const & expecte mk_lean_list(new_try_args)))); } } - struc << "instance " << macro.to_string() << ".has_view : " << macro.to_string() << ".has_view " << macro.to_string() << ".view :=\n" + struc << "instance " << macro.to_string() << ".view.is_view : tysyntax.is_view " << macro.to_string() << ".view :=\n" << "{ view := fun stx, do {\n" << "syntax.node (syntax_node.mk " << esc_macro.to_string() << " [" << stx_pat.str() << "]) <- pure stx | failure,\n" - << binds.str() << "pure (" << macro.to_string() << ".view.mk " << mk_args.str() << ") },\n" << "review := fun ⟨" << view_pat.str() << "⟩, syntax.node (syntax_node.mk " << esc_macro.to_string() << " [" << reviews.str() << "]) }"; trace_elab_detail(tout() << "expansion of node! macro:\n" << struc.str();); @@ -3286,7 +3284,10 @@ expr elaborator::visit_node_macro(expr const & e, optional const & expecte p.parse_command_like(); m_env = p.env(); m_ctx.set_env(m_env); - return visit(mk_app(mk_const({"lean", "parser", "combinators", "node"}), mk_const(get_namespace(p.env()) + macro), mk_lean_list(new_args)), + return visit(mk_app(mk_const({"lean", "parser", "combinators", "node"}), + mk_const(full_macro), + mk_const(full_macro + "view"), + mk_lean_list(new_args)), expected_type); } @@ -3318,18 +3319,16 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional const & if (!inst) throw elaborator_exception(e, sstream() << "Could not infer instance of parser.has_view for '" << r << "'"); - struc << "| " << fname << " : " << instantiate_mvars(m) << " -> " << macro.to_string() << ".view\n"; + struc << "| " << fname << " : tysyntax (" << instantiate_mvars(m) << ") -> " << macro.to_string() << ".view\n"; - view_cases << "| " << i << " := " << macro.to_string() << ".view." << fname << " <$> view (" << pp(r) - << " : " << pp(exp) << ") stx\n"; + view_cases << "| " << i << " := " << macro.to_string() << ".view." << fname << " stx\n"; review_cases << "| " << macro.to_string() << ".view." << fname << " a := " << "syntax.node (syntax_node.mk (some (syntax_node_kind.mk (name.mk_numeral name.anonymous " << i << "))) " - << "[review (" << pp(r) << " : " << pp(exp) << ") a])\n"; + << "[a])\n"; i++; new_args.push_back(mk_as_is(r)); } - struc << "instance " << macro.to_string() << ".has_view : " << macro.to_string() << ".has_view " - << macro.to_string() << ".view :=\n" + struc << "instance " << macro.to_string() << ".view.is_view : tysyntax.is_view " << macro.to_string() << ".view :=\n" << "{ view := fun stx, do {\n" << "syntax.node (syntax_node.mk " << esc_macro.to_string() << " [syntax.node (syntax_node.mk (some (syntax_node_kind.mk (name.mk_numeral name.anonymous i))) [stx])]) <- pure stx | failure,\n" @@ -3350,6 +3349,7 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional const & m_ctx.set_env(m_env); return visit(mk_app(mk_const({"lean", "parser", "combinators", "node"}), mk_const(full_macro), + mk_const(full_macro + "view"), mk_app(mk_const({"list", "cons"}), mk_app(mk_const({"lean", "parser", "combinators", "choice"}), mk_lean_list(new_args)),