From 9ef4d44a865aff75b48992630ea8967bbfe5c559 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 20 Jul 2014 00:23:55 +0100 Subject: [PATCH] chore(frontends/lean): add 'replace' auxiliary funcs Signed-off-by: Leonardo de Moura --- src/frontends/lean/parse_table.cpp | 17 +++++++++++++++++ src/frontends/lean/parse_table.h | 6 ++++++ src/frontends/lean/parser_config.cpp | 8 ++++++++ src/frontends/lean/parser_config.h | 3 +++ 4 files changed, 34 insertions(+) diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index 93c8e0d2b..040018ad7 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -189,6 +189,23 @@ action mk_scoped_expr_action(expr const & rec, unsigned rb, bool lambda) { action mk_ext_action(parse_fn const & fn) { return action(new ext_action_cell(fn)); } action mk_ext_lua_action(char const * fn) { return action(new ext_lua_action_cell(fn)); } +action replace(action const & a, std::function const & f) { + switch (a.kind()) { + case action_kind::Skip: case action_kind::Binder: case action_kind::Binders: + case action_kind::Ext: case action_kind::LuaExt: case action_kind::Expr: + return a; + case action_kind::Exprs: + return mk_exprs_action(a.get_sep(), f(a.get_rec()), f(a.get_initial()), a.is_fold_right(), a.rbp()); + case action_kind::ScopedExpr: + return mk_scoped_expr_action(f(a.get_rec()), a.rbp(), a.use_lambda_abstraction()); + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +transition replace(transition const & t, std::function const & f) { + return transition(t.get_token(), replace(t.get_action(), f)); +} + struct parse_table::cell { bool m_nud; list m_accept; diff --git a/src/frontends/lean/parse_table.h b/src/frontends/lean/parse_table.h index 44618f9ab..15b7b642a 100644 --- a/src/frontends/lean/parse_table.h +++ b/src/frontends/lean/parse_table.h @@ -89,6 +89,9 @@ action mk_scoped_expr_action(expr const & rec, unsigned rbp = 0, bool lambda = t action mk_ext_action(parse_fn const & fn); action mk_ext_lua_action(char const * lua_fn); +/** \brief Apply \c f to expressions embedded in the given action */ +action replace(action const & a, std::function const & f); + class transition { name m_token; action m_action; @@ -99,6 +102,9 @@ public: action const & get_action() const { return m_action; } }; +/** \brief Apply \c f to expressions embedded in the given transition */ +transition replace(transition const & t, std::function const & f); + /** \brief Parse table "transition rules" for implementing a Pratt's parser. The table supports "left factoring" in the methods \c add and \c merge. diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 463c3d29b..882eaeda7 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/sstream.h" +#include "util/list_fn.h" #include "library/scoped_ext.h" #include "library/kernel_serializer.h" #include "frontends/lean/parser_config.h" @@ -17,6 +18,13 @@ using notation::transition; using notation::action; using notation::action_kind; +notation_entry replace(notation_entry const & e, std::function const & f) { + return notation_entry(e.m_is_nud, + map(e.m_transitions, [&](transition const & t) { return notation::replace(t, f); }), + f(e.m_expr), + e.m_overload); +} + struct token_state { token_table m_table; token_state() { m_table = mk_default_token_table(); } diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h index 76b221a18..7aaf25bce 100644 --- a/src/frontends/lean/parser_config.h +++ b/src/frontends/lean/parser_config.h @@ -29,6 +29,9 @@ struct notation_entry { m_is_nud(is_nud), m_transitions(ts), m_expr(e), m_overload(overload) {} }; +/** \brief Apply \c f to expressions embedded in the notation entry */ +notation_entry replace(notation_entry const & e, std::function const & f); + environment add_token(environment const & env, token_entry const & e); environment add_notation(environment const & env, notation_entry const & e);