From a65c43c0dbd254d4fd27ecd84f51da4058d40981 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Jun 2014 17:30:35 -0700 Subject: [PATCH] feat(frontends/lean/builtin_cmds): add definition command family Signed-off-by: Leonardo de Moura --- src/emacs/lean-mode.el | 2 +- src/frontends/lean/builtin_cmds.cpp | 122 +++++++++++++++++++++++++++ src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/parser.cpp | 15 +++- src/frontends/lean/parser.h | 3 + src/frontends/lean/token_table.cpp | 45 +++++----- src/library/private.cpp | 9 -- src/library/private.h | 13 --- tests/lean/t5.lean | 14 +++ tests/lean/t5.lean.expected.out | 5 ++ tests/lean/t6.lean | 11 +++ tests/lean/t6.lean.expected.out | 3 + tests/lean/t7.lean | 19 +++++ tests/lean/t7.lean.expected.out | 5 ++ tests/lua/prv.lua | 6 -- 15 files changed, 222 insertions(+), 52 deletions(-) create mode 100644 tests/lean/t5.lean create mode 100644 tests/lean/t5.lean.expected.out create mode 100644 tests/lean/t6.lean create mode 100644 tests/lean/t6.lean.expected.out create mode 100644 tests/lean/t7.lean create mode 100644 tests/lean/t7.lean.expected.out diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index c4500875c..4cbb11a5b 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -31,7 +31,7 @@ ("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face) ("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face) ("\\_<\\(\\b.*_tac\\|Cond\\|OrElse\\|T\\(?:hen\\|ry\\)\\|When\\|apply\\|b\\(?:ack\\|eta\\)\\|done\\|exact\\)\\_>" . 'font-lock-constant-face) - ("\\_<\\(universe\\|theorem\\|axiom\\|definition\\|variable\\|builtin\\)\\_>[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-function-name-face)) + ("\\_<\\(universe\\|theorem\\|axiom\\|definition\\|variable\\|parameter\\)\\_>}?[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-function-name-face)) ("variables[ \t]\\([^:]*\\)" (1 'font-lock-function-name-face)) ("\\(set_opaque\\|set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face)) ("\\_<_\\_>" . 'font-lock-preprocessor-face) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index eb2d1f1dd..2be5db557 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" #include "library/scoped_ext.h" #include "library/aliases.h" +#include "library/private.h" #include "library/locals.h" #include "frontends/lean/parser.h" @@ -18,6 +19,9 @@ static name g_raw("raw"); static name g_llevel_curly(".{"); static name g_rcurly("}"); static name g_colon(":"); +static name g_assign(":="); +static name g_private("[private]"); +static name g_inline("[inline]"); static void check_atomic(name const & n) { if (!n.is_atomic()) @@ -138,6 +142,121 @@ environment cast_variable_cmd(parser & p) { return variable_cmd_core(p, false, mk_cast_binder_info()); } +// Collect local (section) constants occurring in type and value, sort them, and store in section_ps +static void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer & section_ps) { + name_set ls = collect_locals(type, collect_locals(value)); + ls.for_each([&](name const & n) { + section_ps.push_back(*p.get_local(n)); + }); + std::sort(section_ps.begin(), section_ps.end(), [&](parameter const & p1, parameter const & p2) { + return *p.get_local_index(mlocal_name(p1.m_local)) < *p.get_local_index(mlocal_name(p2.m_local)); + }); +} + +static void parse_modifiers(parser & p, bool & is_private, bool & is_opaque) { + while (true) { + if (p.curr_is_token(g_private)) { + is_private = true; + p.next(); + } else if (p.curr_is_token(g_inline)) { + is_opaque = false; + p.next(); + } else { + break; + } + } +} + +// Wrap \c e with the "explicit macro", the idea is to inform the elaborator +// preprocessor, that we do not need create metavariables for implicit arguments +static expr mark_explicit(expr const & e) { + // TODO(Leo) + return e; +} + +environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) { + bool is_private = false; + parse_modifiers(p, is_private, is_opaque); + if (is_theorem && !is_opaque) + throw exception("invalid theorem declaration, theorems cannot be transparent"); + name n = p.check_id_next("invalid declaration, identifier expected"); + check_atomic(n); + environment env = p.env(); + name real_n; // real name for this declaration + if (is_private) { + auto env_n = add_private_name(env, n, optional(hash(p.pos().first, p.pos().second))); + env = env_n.first; + real_n = env_n.second; + } else { + name const & ns = get_namespace(env); + real_n = ns + n; + } + buffer ls_buffer; + expr type, value; + level_param_names ls; + { + parser::local_scope scope(p); + parse_univ_params(p, ls_buffer); + p.set_type_use_placeholder(false); + buffer ps; + if (!p.curr_is_token(g_colon)) + p.parse_binders(ps); + p.check_token_next(g_colon, "invalid declaration, ':' expected"); + type = p.parse_scoped_expr(ps); + p.check_token_next(g_assign, "invalid declaration, ':=' expected"); + p.set_type_use_placeholder(true); + value = p.parse_scoped_expr(ps); + type = p.pi_abstract(ps, type); + value = p.lambda_abstract(ps, value); + update_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p); + ls = to_list(ls_buffer.begin(), ls_buffer.end()); + } + if (in_section(env)) { + buffer section_ps; + collect_section_locals(type, value, p, section_ps); + type = p.pi_abstract(section_ps, type); + value = p.lambda_abstract(section_ps, value); + buffer section_ls_buffer; + for (name const & l : ls) { + if (p.get_local_level_index(l)) + section_ls_buffer.push_back(mk_param_univ(l)); + else + break; + } + levels section_ls = to_list(section_ls_buffer.begin(), section_ls_buffer.end()); + buffer section_args; + for (auto const & p : section_ps) + section_args.push_back(p.m_local); + expr ref = mk_app(mark_explicit(mk_constant(real_n, section_ls)), section_args); + p.add_local_expr(n, ref); + } else { + if (real_n != n) + env = add_alias(env, n, mk_constant(real_n)); + } + if (is_theorem) { + // TODO(Leo): delay theorems + auto type_value = p.elaborate(type, value, ls); + type = type_value.first; + value = type_value.second; + env = env.add(check(env, mk_theorem(real_n, ls, type, value))); + } else { + auto type_value = p.elaborate(type, value, ls); + type = type_value.first; + value = type_value.second; + env = env.add(check(env, mk_definition(env, real_n, ls, type, value, is_opaque))); + } + return env; +} +environment definition_cmd(parser & p) { + return definition_cmd_core(p, false, true); +} +environment abbreviation_cmd(parser & p) { + return definition_cmd_core(p, false, false); +} +environment theorem_cmd(parser & p) { + return definition_cmd_core(p, true, true); +} + environment print_cmd(parser & p) { if (p.curr() == scanner::token_kind::String) { p.regular_stream() << p.get_str_val() << "\n"; @@ -190,6 +309,9 @@ cmd_table init_cmd_table() { add_cmd(r, cmd_info("[variable]", "declare a new cast parameter", cast_variable_cmd)); add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd)); add_cmd(r, cmd_info("{axiom}", "declare a new implicit axiom", implicit_axiom_cmd)); + add_cmd(r, cmd_info("definition", "add new definition", definition_cmd)); + add_cmd(r, cmd_info("abbreviation", "add new abbreviation (aka transparent definition)", abbreviation_cmd)); + add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd)); add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd)); return r; } diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index e93da92cd..d194c963d 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -40,7 +40,7 @@ parse_table init_nud_table() { parse_table init_led_table() { parse_table r(false); - r.add({transition("->", mk_expr_action(get_arrow_prec() + 1))}, mk_arrow(Var(0), Var(2))); + r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(Var(0), Var(2))); return r; } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 70e75602e..031fa305a 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -246,6 +246,14 @@ optional parser::get_local_index(name const & n) const { return optional(); } +optional parser::get_local(name const & n) const { + auto it = m_local_decls.find(n); + if (it != m_local_decls.end()) + return optional(it->second.first); + else + return optional(); +} + /** \brief Parse a sequence of identifiers ID*. Store the result in \c result. */ void parser::parse_names(buffer> & result) { while (curr_is_identifier()) { @@ -401,6 +409,10 @@ expr parser::elaborate(expr const & e, level_param_names const &) { return e; } +std::pair parser::elaborate(expr const & t, expr const & v, level_param_names const &) { + return mk_pair(t, v); +} + /** \brief Parse ID ':' expr, where the expression represents the type of the identifier. */ parameter parser::parse_binder_core(binder_info const & bi) { auto p = pos(); @@ -621,9 +633,6 @@ expr parser::parse_id() { // globals if (m_env.find(id)) r = save_pos(mk_constant(id, ls), p); - // private globals - else if (auto prv_id = user_to_hidden_name(m_env, id)) - r = save_pos(mk_constant(*prv_id, ls), p); // aliases auto as = get_alias_exprs(m_env, id); if (!is_nil(as)) { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 356d9b568..444d7f5a1 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -195,6 +195,8 @@ public: optional get_local_level_index(name const & n) const; /** \brief Position of the local declaration named \c n in the sequence of local decls. */ optional get_local_index(name const & n) const; + /** \brief Return the local parameter named \c n */ + optional get_local(name const & n) const; /** \brief Specify how the method mk_Type behaves. When set_type_use_placeholder(true), then it returns 'Type.{_}', where '_' is placeholder that instructs the Lean elaborator to @@ -210,6 +212,7 @@ public: expr mk_Type(); expr elaborate(expr const & e, level_param_names const &); + std::pair elaborate(expr const & t, expr const & v, level_param_names const &); /** parse all commands in the input stream */ bool operator()() { return parse_commands(); } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index e837550be..7c41c8828 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -4,11 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include #include "frontends/lean/token_table.h" namespace lean { static unsigned g_arrow_prec = 25; +static unsigned g_max_prec = std::numeric_limits::max(); +static unsigned g_plus_prec = 65; +static unsigned g_cup_prec = 75; unsigned get_arrow_prec() { return g_arrow_prec; } token_table add_command_token(token_table const & s, char const * token) { return insert(s, token, token_info(token)); @@ -45,12 +49,16 @@ static char const * g_cup = "\u2294"; token_table init_token_table() { token_table t; - char const * builtin[] = {"fun", "Pi", "let", "in", "have", "show", "by", "from", "(", ")", "{", "}", "[", "]", - ".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--", - "proof", "qed", "private", "raw", "Bool", "+", g_cup, nullptr}; + std::pair builtin[] = + {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0}, + {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, + {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, + {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, + {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"raw", 0}, {"Bool", g_max_prec}, + {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "definition", "{axiom}", "{variable}", "[variable]", - "variables", "{variables}", "[variables]", + "variables", "{variables}", "[variables]", "[private]", "[inline]", "abbreviation", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "structure", "module", "universe", nullptr}; @@ -68,29 +76,28 @@ token_table init_token_table() { {nullptr, nullptr}}; auto it = builtin; - while (*it) { - t = add_token(t, *it); + while (it->first) { + t = add_token(t, it->first, it->second); it++; } - t = add_token(t, "->", get_arrow_prec()); - it = commands; - while (*it) { - t = add_command_token(t, *it); - ++it; + auto it2 = commands; + while (*it2) { + t = add_command_token(t, *it2); + ++it2; } - auto it2 = aliases; - while (it2->first) { - t = add_token(t, it2->first, it2->second); - it2++; + auto it3 = aliases; + while (it3->first) { + t = add_token(t, it3->first, it3->second); + it3++; } t = add_token(t, g_arrow_unicode, "->", get_arrow_prec()); - it2 = cmd_aliases; - while (it2->first) { - t = add_command_token(t, it2->first, it2->second); - ++it2; + auto it4 = cmd_aliases; + while (it4->first) { + t = add_command_token(t, it4->first, it4->second); + ++it4; } return t; } diff --git a/src/library/private.cpp b/src/library/private.cpp index fe35f3bde..109eeeb7d 100644 --- a/src/library/private.cpp +++ b/src/library/private.cpp @@ -14,7 +14,6 @@ Author: Leonardo de Moura namespace lean { struct private_ext : public environment_extension { unsigned m_counter; - rb_map m_map; // map: user-name -> hidden-name rb_map m_inv_map; // map: hidden-name -> user-name private_ext():m_counter(0) {} }; @@ -47,7 +46,6 @@ std::pair add_private_name(environment const & env, name cons if (extra_hash) h = hash(h, *extra_hash); name r = name(g_private, h) + n; - ext.m_map.insert(n, r); ext.m_inv_map.insert(r, n); ext.m_counter++; environment new_env = update(env, ext); @@ -76,11 +74,6 @@ optional hidden_to_user_name(environment const & env, name const & n) { return it ? optional(*it) : optional(); } -optional user_to_hidden_name(environment const & env, name const & n) { - auto it = get_extension(env).m_map.find(n); - return it ? optional(*it) : optional(); -} - static int add_private_name(lua_State * L) { int nargs = lua_gettop(L); optional h; @@ -93,11 +86,9 @@ static int add_private_name(lua_State * L) { } static int hidden_to_user_name(lua_State * L) { return push_optional_name(L, hidden_to_user_name(to_environment(L, 1), to_name_ext(L, 2))); } -static int user_to_hidden_name(lua_State * L) { return push_optional_name(L, user_to_hidden_name(to_environment(L, 1), to_name_ext(L, 2))); } void open_private(lua_State * L) { SET_GLOBAL_FUN(add_private_name, "add_private_name"); SET_GLOBAL_FUN(hidden_to_user_name, "hidden_to_user_name"); - SET_GLOBAL_FUN(user_to_hidden_name, "user_to_hidden_name"); } } diff --git a/src/library/private.h b/src/library/private.h index 0f2749e9a..ae47f4e4e 100644 --- a/src/library/private.h +++ b/src/library/private.h @@ -31,18 +31,5 @@ std::pair add_private_name(environment const & env, name cons */ optional hidden_to_user_name(environment const & env, name const & n); -/** - \brief Return the hidden name associated with the user name \c n. - - \remark The "user name" is the argument provided to \c add_private_name, and "hidden name" is the name returned - by \c add_private_name. - - \remark The mapping user -> hidden name is *not* stored in .olean files. - In this way, users don't have "access" to the names. - - \see add_private_name -*/ -optional user_to_hidden_name(environment const & env, name const & n); - void open_private(lua_State * L); } diff --git a/tests/lean/t5.lean b/tests/lean/t5.lean new file mode 100644 index 000000000..d9e58a712 --- /dev/null +++ b/tests/lean/t5.lean @@ -0,0 +1,14 @@ +variable N : Type.{1} +variable f : N → N +variable a : N +definition g (a : N) : N := f a +check g +namespace foo + definition h : N := f a + check h + definition [private] q : N := f a + check q +end +check foo.h +check q -- Error q is now hidden + diff --git a/tests/lean/t5.lean.expected.out b/tests/lean/t5.lean.expected.out new file mode 100644 index 000000000..41a6910fd --- /dev/null +++ b/tests/lean/t5.lean.expected.out @@ -0,0 +1,5 @@ +g : N -> N +foo.h : N +private.3156207665.q : N +foo.h : N +t5.lean:13:6: error: unknown identifier 'q' diff --git a/tests/lean/t6.lean b/tests/lean/t6.lean new file mode 100644 index 000000000..15608e865 --- /dev/null +++ b/tests/lean/t6.lean @@ -0,0 +1,11 @@ +section + {parameter} A : Type -- Mark A as implicit parameter + parameter R : A → A → Bool + definition id (a : A) : A := a + definition refl : Bool := forall (a : A), R a a + definition symm : Bool := forall (a b : A), R a b -> R b a +end +check id.{2} +check refl.{1} +check symm.{1} + diff --git a/tests/lean/t6.lean.expected.out b/tests/lean/t6.lean.expected.out new file mode 100644 index 000000000..9c892a20b --- /dev/null +++ b/tests/lean/t6.lean.expected.out @@ -0,0 +1,3 @@ +id.{2} : Pi {A : Type.{2}} (a : A), A +refl.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool +symm.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool diff --git a/tests/lean/t7.lean b/tests/lean/t7.lean new file mode 100644 index 000000000..e9020e835 --- /dev/null +++ b/tests/lean/t7.lean @@ -0,0 +1,19 @@ +variable and : Bool → Bool → Bool +section + {parameter} A : Type -- Mark A as implicit parameter + parameter R : A → A → Bool + parameter B : Type + definition id (a : A) : A := a + definition [private] refl : Bool := ∀ (a : A), R a a + definition symm : Bool := ∀ (a b : A), R a b → R b a + definition trans : Bool := ∀ (a b c : A), R a b → R b c → R a c + definition equivalence : Bool := and (and refl symm) trans +end +check id.{2} +check trans.{1} +check symm.{1} +check equivalence.{1} +(* +local env = get_env() +print(env:find("equivalence"):value()) +*) diff --git a/tests/lean/t7.lean.expected.out b/tests/lean/t7.lean.expected.out new file mode 100644 index 000000000..a7a9b68f5 --- /dev/null +++ b/tests/lean/t7.lean.expected.out @@ -0,0 +1,5 @@ +id.{2} : Pi {A : Type.{2}} (a : A), A +trans.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool +symm.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool +equivalence.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool +fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.2020036202.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R)) diff --git a/tests/lua/prv.lua b/tests/lua/prv.lua index b298b002b..a68a7e792 100644 --- a/tests/lua/prv.lua +++ b/tests/lua/prv.lua @@ -12,9 +12,6 @@ assert(hidden_to_user_name(env, n1)) assert(hidden_to_user_name(env, n1) == name("foo")) assert(hidden_to_user_name(env, n2) == name("foo")) assert(hidden_to_user_name(env, n3) == name("foo", "bla")) -print(user_to_hidden_name(env, "foo")) -assert(user_to_hidden_name(env, "foo") == n2) -assert(user_to_hidden_name(env, {"foo", "bla"}) == n3) env:export("prv_mod.olean") @@ -22,10 +19,7 @@ local env2 = import_modules("prv_mod") assert(hidden_to_user_name(env2, n1) == name("foo")) assert(hidden_to_user_name(env2, n2) == name("foo")) assert(hidden_to_user_name(env2, n3) == name("foo", "bla")) -assert(not user_to_hidden_name(env2, "foo")) -assert(not user_to_hidden_name(env2, {"foo", "bla"})) env2, n4 = add_private_name(env2, "foo") print(n4) assert(n1 ~= n4) assert(not hidden_to_user_name(env, n4)) -assert(user_to_hidden_name(env2, "foo") == n4)