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

Fix bug in parser.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-18 15:23:01 -07:00
parent afd62ced87
commit 4d5b65fe87
2 changed files with 27 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
examples/ex5.lean Normal file
View file

@ -0,0 +1,8 @@
Show fun x : Bool, (fun x : Bool, x).
Show let x := true,
y := true
in (let z := x /\ y,
f := (fun x y : Bool, x /\ y <=>
y /\ x <=>
x \/ y \/ y)
in (f x y) \/ z)

25
src/frontend/parser.cpp
View file

@ -55,6 +55,7 @@ struct parser_fn {
bool m_use_exceptions; bool m_use_exceptions;
bool m_found_errors; bool m_found_errors;
local_decls m_local_decls; local_decls m_local_decls;
unsigned m_num_local_decls;
builtins m_builtins; builtins m_builtins;
/** \brief Exception used to track parsing erros, it does not leak outside of this class. */ /** \brief Exception used to track parsing erros, it does not leak outside of this class. */
@ -62,6 +63,14 @@ struct parser_fn {
parser_error(char const * msg):exception(msg) {} parser_error(char const * msg):exception(msg) {}
}; };
struct mk_scope {
parser_fn & m_fn;
local_decls::mk_scope m_scope;
unsigned m_old_num_local_decls;
mk_scope(parser_fn & fn):m_fn(fn), m_scope(fn.m_local_decls), m_old_num_local_decls(fn.m_num_local_decls) {}
~mk_scope() { m_fn.m_num_local_decls = m_old_num_local_decls; }
};
void scan() { m_curr = m_scanner.scan(); } void scan() { m_curr = m_scanner.scan(); }
scanner::token curr() const { return m_curr; } scanner::token curr() const { return m_curr; }
void next() { if (m_curr != scanner::token::Eof) scan(); } void next() { if (m_curr != scanner::token::Eof) scan(); }
@ -112,6 +121,7 @@ struct parser_fn {
m_err(err), m_err(err),
m_use_exceptions(use_exceptions) { m_use_exceptions(use_exceptions) {
m_found_errors = false; m_found_errors = false;
m_num_local_decls = 0;
m_scanner.set_command_keywords(g_command_keywords); m_scanner.set_command_keywords(g_command_keywords);
init_builtins(); init_builtins();
scan(); scan();
@ -226,7 +236,7 @@ struct parser_fn {
next(); next();
auto it = m_local_decls.find(id); auto it = m_local_decls.find(id);
if (it != m_local_decls.end()) { if (it != m_local_decls.end()) {
return mk_var(m_local_decls.size() - it->second - 1); return mk_var(m_num_local_decls - it->second - 1);
} else { } else {
operator_info op = m_frontend.find_nud(id); operator_info op = m_frontend.find_nud(id);
if (op) { if (op) {
@ -247,7 +257,7 @@ struct parser_fn {
next(); next();
auto it = m_local_decls.find(id); auto it = m_local_decls.find(id);
if (it != m_local_decls.end()) { if (it != m_local_decls.end()) {
return mk_app(left, mk_var(m_local_decls.size() - it->second - 1)); return mk_app(left, mk_var(m_num_local_decls - it->second - 1));
} else { } else {
operator_info op = m_frontend.find_led(id); operator_info op = m_frontend.find_led(id);
if (op) { if (op) {
@ -285,7 +295,10 @@ struct parser_fn {
} }
void register_binding(name const & n) { void register_binding(name const & n) {
m_local_decls.insert(n, m_local_decls.size()); unsigned lvl = m_num_local_decls;
m_local_decls.insert(n, lvl);
m_num_local_decls++;
lean_assert(m_local_decls.find(n)->second == lvl);
} }
void parse_simple_bindings(buffer<std::pair<name, expr>> & result) { void parse_simple_bindings(buffer<std::pair<name, expr>> & result) {
@ -335,7 +348,7 @@ struct parser_fn {
expr parse_abstraction(bool is_lambda) { expr parse_abstraction(bool is_lambda) {
next(); next();
local_decls::mk_scope scope(m_local_decls); mk_scope scope(*this);
buffer<std::pair<name, expr>> bindings; buffer<std::pair<name, expr>> bindings;
parse_bindings(bindings); parse_bindings(bindings);
check_comma_next("invalid abstraction, ',' expected"); check_comma_next("invalid abstraction, ',' expected");
@ -353,7 +366,7 @@ struct parser_fn {
expr parse_let() { expr parse_let() {
next(); next();
local_decls::mk_scope scope(m_local_decls); mk_scope scope(*this);
buffer<std::pair<name, expr>> bindings; buffer<std::pair<name, expr>> bindings;
while (true) { while (true) {
name id = check_identifier_next("invalid let expression, identifier expected"); name id = check_identifier_next("invalid let expression, identifier expected");
@ -472,7 +485,7 @@ struct parser_fn {
check_assign_next("invalid definition, ':=' expected"); check_assign_next("invalid definition, ':=' expected");
val = elaborate(parse_expr()); val = elaborate(parse_expr());
} else { } else {
local_decls::mk_scope scope(m_local_decls); mk_scope scope(*this);
buffer<std::pair<name, expr>> bindings; buffer<std::pair<name, expr>> bindings;
parse_bindings(bindings); parse_bindings(bindings);
check_colon_next("invalid definition, ':' expected"); check_colon_next("invalid definition, ':' expected");