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

chore(frontends/lean/parser): minor cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-08 08:26:39 -07:00
parent fcdd527897
commit 5b9bd279af
2 changed files with 24 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/frontends/lean/parser.cpp
View file

@ -126,7 +126,8 @@ void parser::cache_definition(name const & n, expr const & pre_type, expr const
m_cache->add(m_env, n, pre_type, pre_value, ls, type, value); m_cache->add(m_env, n, pre_type, pre_value, ls, type, value);
} }
optional<std::tuple<level_param_names, expr, expr>> parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value) { auto parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value)
-> optional<std::tuple<level_param_names, expr, expr>> {
if (m_cache) if (m_cache)
return m_cache->find(m_env, n, pre_type, pre_value); return m_cache->find(m_env, n, pre_type, pre_value);
else else
@ -596,7 +597,8 @@ elaborator_context parser::mk_elaborator_context(environment const & env, pos_in
return elaborator_context(env, m_ios, m_local_level_decls, &pp, m_info_manager, true); return elaborator_context(env, m_ios, m_local_level_decls, &pp, m_info_manager, true);
} }
elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp) { elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls,
pos_info_provider const & pp) {
return elaborator_context(env, m_ios, lls, &pp, m_info_manager, true); return elaborator_context(env, m_ios, lls, &pp, m_info_manager, true);
} }
@ -632,8 +634,9 @@ std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env
return r; return r;
} }
std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v, auto parser::elaborate_definition(name const & n, expr const & t, expr const & v,
bool is_opaque) { bool is_opaque)
-> std::tuple<expr, expr, level_param_names> {
parser_pos_provider pp = get_pos_provider(); parser_pos_provider pp = get_pos_provider();
elaborator_context eenv = mk_elaborator_context(pp); elaborator_context eenv = mk_elaborator_context(pp);
auto r = ::lean::elaborate(eenv, n, t, v, is_opaque); auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
@ -641,8 +644,9 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name cons
return r; return r;
} }
std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, local_level_decls const & lls, auto parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
name const & n, expr const & t, expr const & v, bool is_opaque) { name const & n, expr const & t, expr const & v, bool is_opaque)
-> std::tuple<expr, expr, level_param_names> {
parser_pos_provider pp = get_pos_provider(); parser_pos_provider pp = get_pos_provider();
elaborator_context eenv = mk_elaborator_context(env, lls, pp); elaborator_context eenv = mk_elaborator_context(env, lls, pp);
auto r = ::lean::elaborate(eenv, n, t, v, is_opaque); auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
@ -923,7 +927,8 @@ expr parser::parse_notation(parse_table t, expr * left) {
scoped_set_parser scope(L, *this); scoped_set_parser scope(L, *this);
lua_getglobal(L, a.get_lua_fn().c_str()); lua_getglobal(L, a.get_lua_fn().c_str());
if (!lua_isfunction(L, -1)) if (!lua_isfunction(L, -1))
throw parser_error(sstream() << "failed to use notation implemented in Lua, Lua state does not contain function '" throw parser_error(sstream() << "failed to use notation implemented in Lua, "
<< "Lua state does not contain function '"
<< a.get_lua_fn() << "'", p); << a.get_lua_fn() << "'", p);
lua_pushinteger(L, p.first); lua_pushinteger(L, p.first);
lua_pushinteger(L, p.second); lua_pushinteger(L, p.second);
@ -1360,7 +1365,8 @@ bool parser::curr_is_command_like() const {
} }
} }
void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v) { void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls,
expr const & t, expr const & v) {
m_theorem_queue.add(env, n, ls, get_local_level_decls(), t, v); m_theorem_queue.add(env, n, ls, get_local_level_decls(), t, v);
} }

14
src/frontends/lean/parser.h
View file

@ -212,7 +212,8 @@ public:
void cache_definition(name const & n, expr const & pre_type, expr const & pre_value, void cache_definition(name const & n, expr const & pre_type, expr const & pre_value,
level_param_names const & ls, expr const & type, expr const & value); level_param_names const & ls, expr const & type, expr const & value);
/** \brief Try to find an elaborated definition for (n, pre_type, pre_value) in the cache */ /** \brief Try to find an elaborated definition for (n, pre_type, pre_value) in the cache */
optional<std::tuple<level_param_names, expr, expr>> find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value); optional<std::tuple<level_param_names, expr, expr>>
find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value);
void erase_cached_definition(name const & n) { if (m_cache) m_cache->erase(n); } void erase_cached_definition(name const & n) { if (m_cache) m_cache->erase(n); }
bool are_info_lines_valid(unsigned start_line, unsigned end_line) const; bool are_info_lines_valid(unsigned start_line, unsigned end_line) const;
@ -279,9 +280,11 @@ public:
bool curr_is_token(name const & tk) const; bool curr_is_token(name const & tk) const;
/** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */ /** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */
void check_token_next(name const & tk, char const * msg); void check_token_next(name const & tk, char const * msg);
/** \brief Check if the current token is an identifier, if it is return it and move to next token, otherwise throw an exception. */ /** \brief Check if the current token is an identifier, if it is return it and move to next token,
otherwise throw an exception. */
name check_id_next(char const * msg); name check_id_next(char const * msg);
/** \brief Check if the current token is an atomic identifier, if it is, return it and move to next token, otherwise throw an exception. */ /** \brief Check if the current token is an atomic identifier, if it is, return it and move to next token,
otherwise throw an exception. */
name check_atomic_id_next(char const * msg); name check_atomic_id_next(char const * msg);
/** \brief Check if the current token is a constant, if it is, return it and move to next token, otherwise throw an exception. */ /** \brief Check if the current token is a constant, if it is, return it and move to next token, otherwise throw an exception. */
name check_constant_next(char const * msg); name check_constant_next(char const * msg);
@ -343,6 +346,8 @@ public:
unsigned get_local_index(expr const & e) const { return get_local_index(local_pp_name(e)); } unsigned get_local_index(expr const & e) const { return get_local_index(local_pp_name(e)); }
/** \brief Return the local parameter named \c n */ /** \brief Return the local parameter named \c n */
expr const * get_local(name const & n) const { return m_local_decls.find(n); } expr const * get_local(name const & n) const { return m_local_decls.find(n); }
/** \brief Return local declarations as a list of local constants. */
list<expr> locals_to_context() const;
/** /**
\brief By default, when the parser finds a unknown identifier, it signs an error. \brief By default, when the parser finds a unknown identifier, it signs an error.
@ -355,7 +360,8 @@ public:
/** \brief Elaborate \c e, and tolerate metavariables in the result. */ /** \brief Elaborate \c e, and tolerate metavariables in the result. */
std::tuple<expr, level_param_names> elaborate_relaxed(expr const & e, list<expr> const & ctx = list<expr>()); std::tuple<expr, level_param_names> elaborate_relaxed(expr const & e, list<expr> const & ctx = list<expr>());
/** \brief Elaborate \c e, and ensure it is a type. */ /** \brief Elaborate \c e, and ensure it is a type. */
std::tuple<expr, level_param_names> elaborate_type(expr const & e, list<expr> const & ctx = list<expr>(), bool clear_pre_info = true); std::tuple<expr, level_param_names> elaborate_type(expr const & e, list<expr> const & ctx = list<expr>(),
bool clear_pre_info = true);
/** \brief Elaborate \c e in the given environment. */ /** \brief Elaborate \c e in the given environment. */
std::tuple<expr, level_param_names> elaborate_at(environment const & env, expr const & e); std::tuple<expr, level_param_names> elaborate_at(environment const & env, expr const & e);
/** \brief Elaborate \c e (making sure the result does not have metavariables). */ /** \brief Elaborate \c e (making sure the result does not have metavariables). */