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

feat(frontends/lean): add local notation support

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-15 11:30:52 -07:00
parent 9931033554
commit 28047a33ae
5 changed files with 79 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -89,16 +89,22 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi)
name n = p.check_id_next("invalid declaration, identifier expected");
check_atomic(n);
buffer<name> ls_buffer;
buffer<parameter> ps;
if (p.curr_is_token(g_llevel_curly) && in_section(p.env()))
throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
local_scope_if_not_section scope(p);
parse_univ_params(p, ls_buffer);
p.set_type_use_placeholder(false);
if (!p.curr_is_token(g_colon))
p.parse_binders(ps);
p.check_token_next(g_colon, "invalid declaration, ':' expected");
expr type = p.parse_scoped_expr(ps);
expr type;
if (!p.curr_is_token(g_colon)) {
buffer<parameter> ps;
auto lenv = p.parse_binders(ps);
p.check_token_next(g_colon, "invalid declaration, ':' expected");
type = p.parse_scoped_expr(ps, lenv);
type = p.pi_abstract(ps, type);
} else {
p.next();
type = p.parse_expr();
}
level_param_names ls;
if (in_section(p.env())) {
ls = to_level_param_names(collect_univ_params(type));
@ -106,7 +112,6 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi)
update_parameters(ls_buffer, collect_univ_params(type), p);
ls = to_list(ls_buffer.begin(), ls_buffer.end());
}
type = p.pi_abstract(ps, type);
type = p.elaborate(type, ls);
if (in_section(p.env())) {
p.add_local_expr(n, mk_local(n, n, type), bi);
@ -199,16 +204,23 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
parser::local_scope scope(p);
parse_univ_params(p, ls_buffer);
p.set_type_use_placeholder(false);
buffer<parameter> 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);
if (!p.curr_is_token(g_colon)) {
buffer<parameter> ps;
auto lenv = p.parse_binders(ps);
p.check_token_next(g_colon, "invalid declaration, ':' expected");
type = p.parse_scoped_expr(ps, lenv);
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
p.set_type_use_placeholder(true);
value = p.parse_scoped_expr(ps, lenv);
type = p.pi_abstract(ps, type);
value = p.lambda_abstract(ps, value);
} else {
p.next();
type = p.parse_expr();
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
p.set_type_use_placeholder(true);
value = p.parse_expr();
}
update_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
ls = to_list(ls_buffer.begin(), ls_buffer.end());
}

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

@ -23,6 +23,7 @@ Author: Leonardo de Moura
#include "library/deep_copy.h"
#include "library/error_handling/error_handling.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/notation_cmd.h"
#ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
#define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
@ -316,6 +317,11 @@ static name g_add("+");
static name g_max("max");
static name g_imax("imax");
static name g_cup("\u2294");
static name g_infix("infix");
static name g_infixl("infixl");
static name g_infixr("infixr");
static name g_postfix("postfix");
static name g_notation("postfix");
static unsigned g_level_add_prec = 10;
static unsigned g_level_cup_prec = 5;
@ -524,7 +530,21 @@ void parser::parse_binders_core(buffer<parameter> & r) {
parse_binder_block(r, binder_info());
} else if (curr_is_token(g_lparen)) {
next();
parse_binder_block(r, binder_info());
if (curr_is_token(g_infix) || curr_is_token(g_infixl)) {
next();
m_env = infixl_cmd(*this);
} else if (curr_is_token(g_infixr)) {
next();
m_env = infixr_cmd(*this);
} else if (curr_is_token(g_postfix)) {
next();
m_env = postfix_cmd(*this);
} else if (curr_is_token(g_notation)) {
next();
m_env = notation_cmd(*this);
} else {
parse_binder_block(r, binder_info());
}
check_token_next(g_rparen, "invalid binder, ')' expected");
} else if (curr_is_token(g_lcurly)) {
next();
@ -540,12 +560,14 @@ void parser::parse_binders_core(buffer<parameter> & r) {
parse_binders_core(r);
}
void parser::parse_binders(buffer<parameter> & r) {
local_environment parser::parse_binders(buffer<parameter> & r) {
flet<environment> save(m_env, m_env); // save environment
local_expr_decls::mk_scope scope(m_local_decls);
unsigned old_sz = r.size();
parse_binders_core(r);
if (old_sz == r.size())
throw parser_error("invalid binder, '(', '{', '[' or identifier expected", pos());
return local_environment(m_env);
}
expr parser::parse_notation(parse_table t, expr * left) {
@ -553,6 +575,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
auto p = pos();
buffer<expr> args;
buffer<parameter> ps;
local_environment lenv(m_env);
if (left)
args.push_back(*left);
while (true) {
@ -601,10 +624,10 @@ expr parser::parse_notation(parse_table t, expr * left) {
ps.push_back(parse_binder());
break;
case notation::action_kind::Binders:
parse_binders(ps);
lenv = parse_binders(ps);
break;
case notation::action_kind::ScopedExpr: {
expr r = parse_scoped_expr(ps, a.rbp());
expr r = parse_scoped_expr(ps, lenv, a.rbp());
if (is_var(a.get_rec(), 0)) {
r = abstract(ps, r, a.use_lambda_abstraction());
} else {
@ -753,7 +776,8 @@ expr parser::parse_expr(unsigned rbp) {
return left;
}
expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp) {
expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, local_environment const & lenv, unsigned rbp) {
flet<environment> let(m_env, lenv.m_env);
if (num_params == 0) {
return parse_expr(rbp);
} else {

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

@ -43,6 +43,11 @@ struct parser_error : public exception {
struct interrupt_parser {};
typedef local_decls<parameter> local_expr_decls;
typedef local_decls<level> local_level_decls;
class local_environment {
friend parser;
environment m_env;
local_environment(environment const & env):m_env(env) {}
};
class parser {
environment m_env;
@ -183,10 +188,16 @@ public:
level parse_level(unsigned rbp = 0);
parameter parse_binder();
void parse_binders(buffer<parameter> & r);
local_environment parse_binders(buffer<parameter> & r);
expr parse_expr(unsigned rbp = 0);
expr parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp = 0);
expr parse_scoped_expr(unsigned num_params, parameter const * ps, local_environment const & lenv, unsigned rbp = 0);
expr parse_scoped_expr(buffer<parameter> & ps, local_environment const & lenv, unsigned rbp = 0) {
return parse_scoped_expr(ps.size(), ps.data(), lenv, rbp);
}
expr parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp = 0) {
return parse_scoped_expr(num_params, ps, local_environment(m_env), rbp);
}
expr parse_scoped_expr(buffer<parameter> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda = true);
expr abstract(buffer<parameter> const & ps, expr const & e, bool lambda = true) { return abstract(ps.size(), ps.data(), e, lambda); }

7
tests/lean/t12.lean Normal file
View file

@ -0,0 +1,7 @@
precedence `+` : 65
precedence `*` : 75
variable N : Type.{1}
check λ (f : N -> N -> N) (g : N → N → N) (infix + := f) (infix * := g) (x y : N), x+x*y
variable f : N → N → N
variable a : N
check a+a -- + notation is not available anymore

2
tests/lean/t12.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
fun (f : N -> N -> N) (g : N -> N -> N) (x : N) (y : N), (f x (g x y)) : (N -> N -> N) -> (N -> N -> N) -> N -> N -> N
t12.lean:7:7: error: invalid expression