michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(frontends/lean): add 'replace' auxiliary funcs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-20 00:23:55 +01:00
parent 5e8c128b00
commit 9ef4d44a86
4 changed files with 34 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/frontends/lean/parse_table.cpp
View file

@ -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<expr(expr const &)> 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<expr(expr const &)> const & f) {
return transition(t.get_token(), replace(t.get_action(), f));
}
struct parse_table::cell {
bool m_nud;
list<expr> m_accept;

6
src/frontends/lean/parse_table.h
View file

@ -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<expr(expr const &)> 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<expr(expr const &)> 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.

8
src/frontends/lean/parser_config.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <string>
#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<expr(expr const &)> 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(); }

3
src/frontends/lean/parser_config.h
View file

@ -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<expr(expr const &)> const & f);
environment add_token(environment const & env, token_entry const & e);
environment add_notation(environment const & env, notation_entry const & e);