From ca632cca13614f8943e7a9f652439713f12eb7fb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Oct 2014 10:58:15 -0700 Subject: [PATCH] feat(frontends/lean): add 'universe variable' command We can declare variables anywhere. So, we must also be able do declare "universe" variables anywhere. Here is a minimal example that requires this feature ``` -- We want A and B to be in the same universe universe variable l variable A : Type.{l} variable B : Type.{l} definition tst := A = B ``` The following doesn't work because A and B are in different universes ``` variable A : Type variable B : Type definition tst := A = B ``` The following works, but tst is not universe polymorphic, since l is one *fixed* global universe ``` universe l variable A : Type.{l} variable B : Type.{l} definition tst := A = B ``` --- src/frontends/lean/decl_cmds.cpp | 34 ++++++++++++++++++-------- src/frontends/lean/inductive_cmd.cpp | 2 +- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 +++ src/frontends/lean/tokens.h | 1 + src/frontends/lean/util.cpp | 4 +-- src/frontends/lean/util.h | 6 +++-- tests/lean/univ_vars.lean | 28 +++++++++++++++++++++ tests/lean/univ_vars.lean.expected.out | 5 ++++ 9 files changed, 70 insertions(+), 16 deletions(-) create mode 100644 tests/lean/univ_vars.lean create mode 100644 tests/lean/univ_vars.lean.expected.out diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index e3198da26..25760be47 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -24,8 +24,8 @@ Author: Leonardo de Moura #include "frontends/lean/tokens.h" namespace lean { -static environment declare_universe(parser & p, environment env, name const & n) { - if (in_section_or_context(env)) { +static environment declare_universe(parser & p, environment env, name const & n, bool local) { + if (in_section_or_context(env) || local) { p.add_local_level(n, mk_param_univ(n)); } else { name const & ns = get_namespace(env); @@ -37,23 +37,37 @@ static environment declare_universe(parser & p, environment env, name const & n) return env; } -environment universe_cmd(parser & p) { - name n = p.check_id_next("invalid 'universe' command, identifier expected"); - return declare_universe(p, p.env(), n); -} - -environment universes_cmd(parser & p) { +static environment universes_cmd_core(parser & p, bool local) { if (!p.curr_is_identifier()) throw parser_error("invalid 'universes' command, identifier expected", p.pos()); environment env = p.env(); while (p.curr_is_identifier()) { name n = p.get_name_val(); p.next(); - env = declare_universe(p, env, n); + env = declare_universe(p, env, n, local); } return env; } +static environment universe_cmd(parser & p) { + if (p.curr_is_token(get_variables_tk())) { + p.next(); + return universes_cmd_core(p, true); + } else { + bool local = false; + if (p.curr_is_token(get_variable_tk())) { + p.next(); + local = true; + } + name n = p.check_id_next("invalid 'universe' command, identifier expected"); + return declare_universe(p, p.env(), n, local); + } +} + +static environment universes_cmd(parser & p) { + return universes_cmd_core(p, false); +} + bool parse_univ_params(parser & p, buffer & ps) { if (p.curr_is_token(get_llevel_curly_tk())) { p.next(); @@ -383,7 +397,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo value = Fun_as_is(section_value_ps, value, p); update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p); ls = to_list(ls_buffer.begin(), ls_buffer.end()); - levels section_ls = collect_section_nonvar_levels(p, ls); + levels section_ls = collect_local_nonvar_levels(p, ls); remove_section_variables(p, section_ps); if (!section_ps.empty()) { expr ref = mk_section_local_ref(real_n, section_ls, section_ps); diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 753b381a5..5879d91f3 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -608,7 +608,7 @@ struct inductive_cmd_fn { buffer section_params_only(section_params); remove_section_variables(m_p, section_params_only); // Create aliases/local refs - levels section_levels = collect_section_nonvar_levels(m_p, ls); + levels section_levels = collect_local_nonvar_levels(m_p, ls); for (auto & d : decls) { name d_name = inductive_decl_name(d); name d_short_name(d_name.get_string()); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 8c6fda414..6d208770d 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -75,7 +75,7 @@ void init_token_table(token_table & t) { {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, - {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, + {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0}, {nullptr, 0}}; char const * commands[] = diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 0acdeb32d..c3281a584 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -65,6 +65,7 @@ static name * g_definition = nullptr; static name * g_theorem = nullptr; static name * g_axiom = nullptr; static name * g_variable = nullptr; +static name * g_variables = nullptr; static name * g_opaque = nullptr; static name * g_instance = nullptr; static name * g_priority = nullptr; @@ -148,6 +149,7 @@ void initialize_tokens() { g_opaque = new name("opaque"); g_axiom = new name("axiom"); g_variable = new name("variable"); + g_variables = new name("variables"); g_instance = new name("[instance]"); g_priority = new name("[priority"); g_coercion = new name("[coercion]"); @@ -193,6 +195,7 @@ void finalize_tokens() { delete g_theorem; delete g_opaque; delete g_axiom; + delete g_variables; delete g_variable; delete g_instance; delete g_priority; @@ -312,6 +315,7 @@ name const & get_definition_tk() { return *g_definition; } name const & get_theorem_tk() { return *g_theorem; } name const & get_axiom_tk() { return *g_axiom; } name const & get_variable_tk() { return *g_variable; } +name const & get_variables_tk() { return *g_variables; } name const & get_opaque_tk() { return *g_opaque; } name const & get_instance_tk() { return *g_instance; } name const & get_priority_tk() { return *g_priority; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 104c07492..ed462d347 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -67,6 +67,7 @@ name const & get_definition_tk(); name const & get_theorem_tk(); name const & get_axiom_tk(); name const & get_variable_tk(); +name const & get_variables_tk(); name const & get_opaque_tk(); name const & get_instance_tk(); name const & get_priority_tk(); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index a97263c13..31efd87ae 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -60,8 +60,8 @@ void sort_section_params(expr_struct_set const & locals, parser const & p, buffe }); } -// Return the levels in \c ls that are defined in the section -levels collect_section_nonvar_levels(parser & p, level_param_names const & ls) { +// Return the local levels in \c ls that are not associated with variables +levels collect_local_nonvar_levels(parser & p, level_param_names const & ls) { buffer section_ls_buffer; for (name const & l : ls) { if (p.get_local_level_index(l) && !p.is_local_level_variable(l)) diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 6634d8ac0..9269b3a23 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -22,8 +22,10 @@ void check_atomic(name const & n); void check_in_section_or_context(parser const & p); bool is_root_namespace(name const & n); name remove_root_prefix(name const & n); -/** \brief Return the levels in \c ls that are defined in the section, but are not tagged as variables. */ -levels collect_section_nonvar_levels(parser & p, level_param_names const & ls); +/** \brief Return the local levels in \c ls that are not tagged as variables. + A local level is tagged as variable if it associated with a variable. +*/ +levels collect_local_nonvar_levels(parser & p, level_param_names const & ls); /** \brief Collect local (section) constants occurring in type and value, sort them, and store in section_ps */ void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer & section_ps); /** \brief Copy the local parameters to \c section_ps, then sort \c section_ps (using the order in which they were declared). */ diff --git a/tests/lean/univ_vars.lean b/tests/lean/univ_vars.lean new file mode 100644 index 000000000..a2924cb9a --- /dev/null +++ b/tests/lean/univ_vars.lean @@ -0,0 +1,28 @@ +import logic +set_option pp.universes true + +universe u +variable A : Type.{u} + +definition id1 (a : A) : A := a +check @id1 + +variable B : Type + +definition id2 (a : B) : B := a +check @id2 + +universe variable k +variable C : Type.{k} + +definition id3 (a : C) := a + +check @id3 + +universe variables l m +variable A₁ : Type.{l} +variable A₂ : Type.{l} +definition foo (a₁ : A₁) (a₂ : A₂) := a₁ == a₂ +check @foo + +check Type.{m} diff --git a/tests/lean/univ_vars.lean.expected.out b/tests/lean/univ_vars.lean.expected.out new file mode 100644 index 000000000..a25e57362 --- /dev/null +++ b/tests/lean/univ_vars.lean.expected.out @@ -0,0 +1,5 @@ +id1 : Π (A : Type.{u}), A → A +id2.{l_2} : Π (B : Type.{l_2}), B → B +id3.{k} : Π (C : Type.{k}), C → C +foo.{l} : Π (A₁ A₂ : Type.{l}), A₁ → A₂ → Prop +Type.{m} : Type.{succ m}