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

feat(frontends/lean): parse recursive equations

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-04 16:52:42 -08:00
parent 7a6d674b8e
commit e868ecce36
5 changed files with 60 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -116,7 +116,8 @@
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; modifiers
(,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
"\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[whnf\]" "\[decls\]" "\[strict\]" "\[local\]"))
"\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[wf\]" "\[whnf\]"
"\[decls\]" "\[strict\]" "\[local\]"))
. 'font-lock-doc-face)
(,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
;; tactics

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

@ -18,6 +18,7 @@ Author: Leonardo de Moura
#include "library/explicit.h"
#include "library/reducible.h"
#include "library/coercion.h"
#include "library/definitional/equations.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/util.h"
#include "frontends/lean/class.h"
@ -309,6 +310,50 @@ static void erase_local_binder_info(buffer<expr> & ps) {
p = update_local(p, binder_info());
}
static bool is_curr_with_or_comma(parser & p) {
return p.curr_is_token(get_with_tk()) || p.curr_is_token(get_comma_tk());
}
expr parse_equations(parser & p, name const & n, expr const & type, buffer<expr> & auxs) {
buffer<expr> eqns;
{
parser::local_scope scope1(p);
parser::undef_id_to_local_scope scope2(p);
lean_assert(is_curr_with_or_comma(p));
expr f = mk_local(n, type);
if (p.curr_is_token(get_with_tk())) {
while (p.curr_is_token(get_with_tk())) {
p.next();
name g_name = p.check_id_next("invalid declaration, identifier expected");
p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
expr g_type = p.parse_expr();
expr g = mk_local(g_name, g_type);
auxs.push_back(g);
}
}
p.check_token_next(get_comma_tk(), "invalid declaration, ',' expected");
p.add_local(f);
for (expr const & g : auxs)
p.add_local(g);
while (true) {
expr lhs = p.parse_expr();
p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
expr rhs = p.parse_expr();
eqns.push_back(mk_equation(lhs, rhs));
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
}
if (p.curr_is_token(get_wf_tk())) {
p.next();
expr Hwf = p.parse_expr();
return mk_equations(eqns.size(), eqns.data(), Hwf);
} else {
return mk_equations(eqns.size(), eqns.data());
}
}
// An Lean example is not really a definition, but we use the definition infrastructure to simulate it.
enum def_cmd_kind { Theorem, Definition, Example };
@ -325,6 +370,7 @@ class definition_cmd_fn {
decl_modifiers m_modifiers;
name m_real_name; // real name for this declaration
buffer<name> m_ls_buffer;
buffer<expr> m_aux_decls;
expr m_type;
expr m_value;
level_param_names m_ls;
@ -361,7 +407,9 @@ class definition_cmd_fn {
m_p.next();
auto pos = m_p.pos();
m_type = m_p.parse_expr();
if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
if (is_curr_with_or_comma(m_p)) {
m_value = parse_equations(m_p, m_name, m_type, m_aux_decls);
} else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
check_end_of_theorem(m_p);
m_value = m_p.save_pos(mk_expr_placeholder(), pos);
} else {
@ -377,7 +425,9 @@ class definition_cmd_fn {
if (m_p.curr_is_token(get_colon_tk())) {
m_p.next();
m_type = m_p.parse_scoped_expr(ps, *lenv);
if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
if (is_curr_with_or_comma(m_p)) {
m_value = parse_equations(m_p, m_name, m_type, m_aux_decls);
} else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
check_end_of_theorem(m_p);
m_value = m_p.save_pos(mk_expr_placeholder(), pos);
} else {

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

@ -86,7 +86,7 @@ void init_token_table(token_table & t) {
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[parsing-only]", "reducible", "irreducible",
"evaluate", "check", "eval", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude",
"import", "inductive", "record", "structure", "module", "universe", "universes",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
"exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",

4
src/frontends/lean/tokens.cpp
View file

@ -53,6 +53,7 @@ static name * g_on = nullptr;
static name * g_off = nullptr;
static name * g_none = nullptr;
static name * g_whnf = nullptr;
static name * g_wf = nullptr;
static name * g_strict = nullptr;
static name * g_in = nullptr;
static name * g_assign = nullptr;
@ -146,6 +147,7 @@ void initialize_tokens() {
g_off = new name("[off]");
g_none = new name("[none]");
g_whnf = new name("[whnf]");
g_wf = new name("[wf]");
g_strict = new name("[strict]");
g_in = new name("in");
g_assign = new name(":=");
@ -257,6 +259,7 @@ void finalize_tokens() {
delete g_off;
delete g_none;
delete g_whnf;
delete g_wf;
delete g_strict;
delete g_ellipsis;
delete g_fun;
@ -333,6 +336,7 @@ name const & get_on_tk() { return *g_on; }
name const & get_off_tk() { return *g_off; }
name const & get_none_tk() { return *g_none; }
name const & get_whnf_tk() { return *g_whnf; }
name const & get_wf_tk() { return *g_wf; }
name const & get_strict_tk() { return *g_strict; }
name const & get_in_tk() { return *g_in; }
name const & get_assign_tk() { return *g_assign; }

1
src/frontends/lean/tokens.h
View file

@ -55,6 +55,7 @@ name const & get_on_tk();
name const & get_off_tk();
name const & get_none_tk();
name const & get_whnf_tk();
name const & get_wf_tk();
name const & get_strict_tk();
name const & get_in_tk();
name const & get_assign_tk();