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

feat(frontends/lean): remove 'context' command

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-22 11:32:02 -07:00
parent 53653c3526
commit 91f21c007a
15 changed files with 41 additions and 79 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/emacs/lean-syntax.el
View file

@ -12,7 +12,7 @@
"hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
"hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises"
"print" "theorem" "example" "abbreviation"
"context" "open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
"open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
"alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
"calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
"infix" "infixl" "infixr" "notation" "eval" "check" "coercion" "end"

12
src/frontends/lean/builtin_cmds.cpp
View file

@ -252,15 +252,6 @@ environment section_cmd(parser & p) {
return push_scope(p.env(), p.ios(), scope_kind::Section, n);
}
environment context_cmd(parser & p) {
name n;
if (p.curr_is_identifier())
n = p.check_atomic_id_next("invalid context, atomic identifier expected");
bool save_options = true;
p.push_local_scope(save_options);
return push_scope(p.env(), p.ios(), scope_kind::Context, n);
}
environment namespace_cmd(parser & p) {
auto pos = p.pos();
name n = p.check_atomic_id_next("invalid namespace declaration, atomic identifier expected");
@ -274,7 +265,7 @@ static environment redeclare_aliases(environment env, parser & p,
list<pair<name, level>> old_level_entries,
list<pair<name, expr>> old_entries) {
environment const & old_env = p.env();
if (!in_context(old_env) && !in_section(old_env))
if (!in_section(old_env))
return env;
list<pair<name, expr>> new_entries = p.get_local_entries();
buffer<pair<name, expr>> to_redeclare;
@ -695,7 +686,6 @@ void init_cmd_table(cmd_table & r) {
add_cmd(r, cmd_info("exit", "exit", exit_cmd));
add_cmd(r, cmd_info("print", "print a string", print_cmd));
add_cmd(r, cmd_info("section", "open a new section", section_cmd));
add_cmd(r, cmd_info("context", "open a new context", context_cmd));
add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd));
add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd));
add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd));

15
src/frontends/lean/decl_cmds.cpp
View file

@ -37,7 +37,7 @@ Author: Leonardo de Moura
namespace lean {
static environment declare_universe(parser & p, environment env, name const & n, bool local) {
if (in_context(env) || local) {
if (local) {
p.add_local_level(n, mk_param_univ(n), local);
} else {
name const & ns = get_namespace(env);
@ -125,7 +125,7 @@ static environment declare_var(parser & p, environment env,
if (_bi) bi = *_bi;
if (k == variable_kind::Parameter || k == variable_kind::Variable) {
if (k == variable_kind::Parameter) {
check_in_context_or_section(p);
check_in_section(p);
check_parameter_type(p, n, type, pos);
}
if (p.get_local(n))
@ -172,13 +172,13 @@ optional<binder_info> parse_binder_info(parser & p, variable_kind k) {
}
static void check_variable_kind(parser & p, variable_kind k) {
if (in_context(p.env()) || in_section(p.env())) {
if (in_section(p.env())) {
if (k == variable_kind::Axiom || k == variable_kind::Constant)
throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections/contexts",
throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections",
p.pos());
} else if (!in_section(p.env()) && !in_context(p.env()) && k == variable_kind::Parameter) {
} else if (!in_section(p.env()) && k == variable_kind::Parameter) {
throw parser_error("invalid declaration, 'parameter/hypothesis/conjecture' "
"can only be used in contexts and sections", p.pos());
"can only be used in sections", p.pos());
}
}
@ -374,10 +374,7 @@ struct decl_attributes {
m_is_instance = true;
p.next();
} else if (p.curr_is_token(get_coercion_tk())) {
auto pos = p.pos();
p.next();
if (in_context(p.env()) && m_persistent)
throw parser_error("invalid '[coercion]' attribute, (non local) coercions cannot be defined in contexts", pos);
m_is_coercion = true;
} else if (p.curr_is_token(get_reducible_tk())) {
if (m_is_irreducible || m_is_semireducible || m_is_quasireducible)

14
src/frontends/lean/notation_cmd.cpp
View file

@ -627,7 +627,7 @@ struct notation_modifiers {
static environment notation_cmd_core(parser & p, bool overload, bool reserve, bool persistent) {
notation_modifiers mods;
mods.parse(p);
flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !persistent);
flet<bool> set_allow_local(g_allow_local, !persistent);
environment env = p.env();
buffer<token_entry> new_tokens;
auto ne = parse_notation_core(p, overload, reserve, new_tokens, mods.m_parse_only);
@ -640,7 +640,7 @@ static environment notation_cmd_core(parser & p, bool overload, bool reserve, bo
static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool reserve, bool persistent) {
notation_modifiers mods;
mods.parse(p);
flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !persistent);
flet<bool> set_allow_local(g_allow_local, !persistent);
auto nt = parse_mixfix_notation(p, k, overload, reserve, mods.m_parse_only);
environment env = p.env();
if (nt.second)
@ -650,35 +650,35 @@ static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool res
}
static environment notation_cmd(parser & p) {
bool overload = !in_context(p.env());
bool overload = true;
bool reserve = false;
bool persistent = true;
return notation_cmd_core(p, overload, reserve, persistent);
}
static environment infixl_cmd(parser & p) {
bool overload = !in_context(p.env());
bool overload = true;
bool reserve = false;
bool persistent = true;
return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent);
}
static environment infixr_cmd(parser & p) {
bool overload = !in_context(p.env());
bool overload = true;
bool reserve = false;
bool persistent = true;
return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve, persistent);
}
static environment postfix_cmd(parser & p) {
bool overload = !in_context(p.env());
bool overload = true;
bool reserve = false;
bool persistent = true;
return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve, persistent);
}
static environment prefix_cmd(parser & p) {
bool overload = !in_context(p.env());
bool overload = true;
bool reserve = false;
bool persistent = true;
return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve, persistent);

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

@ -457,7 +457,7 @@ void parser::push_local_scope(bool save_options) {
void parser::pop_local_scope() {
if (!m_local_level_decls.has_scopes()) {
throw parser_error("invalid 'end', there is no open namespace/section/context", pos());
throw parser_error("invalid 'end', there is no open namespace/section", pos());
}
m_local_level_decls.pop();
m_local_decls.pop();
@ -1116,7 +1116,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
if (auto it1 = m_local_decls.find(id)) {
if (ls && m_undef_id_behavior != undef_id_behavior::AssumeConstant)
throw parser_error("invalid use of explicit universe parameter, identifier is a variable, "
"parameter or a constant bound to parameters in a section/context", p);
"parameter or a constant bound to parameters in a section", p);
auto r = copy_with_new_pos(*it1, p);
save_type_info(r);
save_identifier_info(p, id);
@ -1189,7 +1189,7 @@ name parser::check_constant_next(char const * msg) {
name id = check_id_next(msg);
expr e = id_to_expr(id, p);
if ((in_section(m_env) || in_context(m_env)) && is_as_atomic(e)) {
if (in_section(m_env) && is_as_atomic(e)) {
e = get_app_fn(get_as_atomic_arg(e));
if (is_explicit(e))
e = get_explicit_arg(e);

2
src/frontends/lean/token_table.cpp
View file

@ -96,7 +96,7 @@ void init_token_table(token_table & t) {
"evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-f]", "[unfold-c", "print",
"end", "namespace", "section", "prelude", "help",
"import", "inductive", "record", "structure", "module", "universe", "universes", "local",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
"exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
"add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
"multiple_instances", "find_decl", "attribute", "persistent",

11
src/frontends/lean/util.cpp
View file

@ -60,14 +60,9 @@ void check_atomic(name const & n) {
throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic");
}
void check_in_context(parser const & p) {
if (!in_context(p.env()))
throw exception(sstream() << "invalid command, it must be used in a (local) context");
}
void check_in_context_or_section(parser const & p) {
if (!in_context(p.env()) && !in_section(p.env()))
throw exception(sstream() << "invalid command, it must be used in a (local) context or section");
void check_in_section(parser const & p) {
if (!in_section(p.env()))
throw exception(sstream() << "invalid command, it must be used in a section");
}
bool is_root_namespace(name const & n) {

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

@ -27,8 +27,7 @@ void check_command_period_or_eof(parser const & p);
/** \brief Throw and error if the current token is not a command, nor an open binder, nor a '.', nor an end-of-file. */
void check_command_period_open_binder_or_eof(parser const & p);
void check_atomic(name const & n);
void check_in_context(parser const & p);
void check_in_context_or_section(parser const & p);
void check_in_section(parser const & p);
bool is_root_namespace(name const & n);
name remove_root_prefix(name const & n);
/** \brief Return the local levels in \c ls that are not tagged as variables.

14
src/library/aliases.cpp
View file

@ -25,12 +25,12 @@ static environment update(environment const & env, aliases_ext const & ext);
struct aliases_ext : public environment_extension {
struct state {
bool m_in_context;
bool m_in_section;
name_map<list<name>> m_aliases;
name_map<name> m_inv_aliases;
name_map<name> m_level_aliases;
name_map<name> m_inv_level_aliases;
state():m_in_context(false) {}
state():m_in_section(false) {}
void add_expr_alias(name const & a, name const & e, bool overwrite) {
auto it = m_aliases.find(a);
@ -63,7 +63,7 @@ struct aliases_ext : public environment_extension {
} else {
state s = head(scopes);
s.add_expr_alias(a, e, overwrite);
if (s.m_in_context) {
if (s.m_in_section) {
return cons(s, add_expr_alias_rec_core(tail(scopes), a, e, overwrite));
} else {
return cons(s, tail(scopes));
@ -72,15 +72,15 @@ struct aliases_ext : public environment_extension {
}
void add_expr_alias_rec(name const & a, name const & e, bool overwrite = false) {
if (m_state.m_in_context) {
if (m_state.m_in_section) {
m_scopes = add_expr_alias_rec_core(m_scopes, a, e, overwrite);
}
add_expr_alias(a, e, overwrite);
}
void push(bool in_context) {
void push(bool in_section) {
m_scopes = cons(m_state, m_scopes);
m_state.m_in_context = in_context;
m_state.m_in_section = in_section;
}
void pop() {
@ -106,7 +106,7 @@ struct aliases_ext : public environment_extension {
aliases_ext ext = get_extension(env);
ext.push(k != scope_kind::Namespace);
environment new_env = update(env, ext);
if (!::lean::in_context(new_env) && !::lean::in_section(new_env))
if (!::lean::in_section(new_env))
new_env = add_aliases(new_env, get_namespace(new_env), name());
return new_env;
}

24
src/library/scoped_ext.cpp
View file

@ -50,18 +50,9 @@ list<name> const & get_namespaces(environment const & env) {
return get_extension(env).m_namespaces;
}
bool in_section_or_context(environment const & env) {
scope_mng_ext const & ext = get_extension(env);
return !is_nil(ext.m_scope_kinds) && head(ext.m_scope_kinds) != scope_kind::Namespace;
}
bool in_context(environment const & env) {
scope_mng_ext const & ext = get_extension(env);
return !is_nil(ext.m_scope_kinds) && head(ext.m_scope_kinds) == scope_kind::Context;
}
bool in_section(environment const & env) {
return in_section_or_context(env) && !in_context(env);
scope_mng_ext const & ext = get_extension(env);
return !is_nil(ext.m_scope_kinds) && head(ext.m_scope_kinds) == scope_kind::Section;
}
void get_metaclasses(buffer<name> & r) {
@ -143,10 +134,8 @@ environment add_namespace(environment const & env, name const & ns) {
}
environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n) {
if (k == scope_kind::Namespace && in_section_or_context(env))
throw exception("invalid namespace declaration, a namespace cannot be declared inside a section or context");
if (k == scope_kind::Section && in_context(env))
throw exception("invalid section declaration, a section cannot be declared inside a context");
if (k == scope_kind::Namespace && in_section(env))
throw exception("invalid namespace declaration, a namespace cannot be declared inside a section");
name new_n = get_namespace(env);
if (k == scope_kind::Namespace)
new_n = new_n + n;
@ -200,7 +189,7 @@ environment pop_scope_core(environment const & env, io_state const & ios) {
environment pop_scope(environment const & env, io_state const & ios, name const & n) {
scope_mng_ext ext = get_extension(env);
if (is_nil(ext.m_namespaces))
throw exception("invalid end of scope, there are no open namespaces/sections/contexts");
throw exception("invalid end of scope, there are no open namespaces/sections");
if (n != head(ext.m_headers))
throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '"
<< head(ext.m_headers) << "', and ends with '" << n << "'");
@ -227,7 +216,7 @@ static int using_namespace_objects(lua_State * L) {
static int push_scope(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 1)
return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Context));
return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Section));
else if (nargs == 2)
return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Namespace, to_name_ext(L, 2)));
scope_kind k = static_cast<scope_kind>(lua_tonumber(L, 3));
@ -253,7 +242,6 @@ void open_scoped_ext(lua_State * L) {
lua_newtable(L);
SET_ENUM("Namespace", scope_kind::Namespace);
SET_ENUM("Section", scope_kind::Section);
SET_ENUM("Context", scope_kind::Context);
lua_setglobal(L, "scope_kind");
}

5
src/library/scoped_ext.h
View file

@ -16,7 +16,7 @@ Author: Leonardo de Moura
#include "library/fingerprint.h"
namespace lean {
enum class scope_kind { Namespace, Section, Context };
enum class scope_kind { Namespace, Section };
typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &);
typedef environment (*export_namespace_fn)(environment const &, io_state const &, name const &);
typedef environment (*push_scope_fn)(environment const &, io_state const &, scope_kind);
@ -56,7 +56,6 @@ environment add_namespace(environment const & env, name const & ns);
name const & get_namespace(environment const & env);
list<name> const & get_namespaces(environment const & env);
bool in_context(environment const & env);
bool in_section(environment const & env);
/** \brief Check if \c n may be a reference to a namespace, if it is return it.
@ -234,7 +233,7 @@ public:
if (auto h = get_fingerprint(e)) {
env = update_fingerprint(env, *h);
}
if (in_context(env) || !persistent) {
if (!persistent) {
return update(env, get(env)._add_tmp_entry(env, ios, e));
} else {
name n = get_namespace(env);

2
tests/lean/bad_end.lean.expected.out
View file

@ -1 +1 @@
bad_end.lean:1:4: error: invalid 'end', there is no open namespace/section/context
bad_end.lean:1:4: error: invalid 'end', there is no open namespace/section

2
tests/lean/sec3.lean.expected.out
View file

@ -1 +1 @@
sec3.lean:5:8: error: invalid use of explicit universe parameter, identifier is a variable, parameter or a constant bound to parameters in a section/context
sec3.lean:5:8: error: invalid use of explicit universe parameter, identifier is a variable, parameter or a constant bound to parameters in a section

2
tests/lean/t3.lean.expected.out
View file

@ -5,7 +5,7 @@ Type
t3.lean:9:16: error: unknown universe 'v'
Type
t3.lean:14:16: error: unknown universe 'z'
t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section or context
t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section
Type
Type
Type

6
tests/lua/scope.lua
View file

@ -66,9 +66,3 @@ for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. to
assert(get_num_coercions(env) == 6)
print("---------")
env = pop_scope(env)
assert(get_num_coercions(env) == 3)
env = pop_scope(env, "tst")
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
assert(get_num_coercions(env) == 1)
env = push_scope(env, "tst")
assert(get_num_coercions(env) == 3)