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

refactor(frontends/lean/builtin_cmds): explicit token initialization

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-22 19:22:53 -07:00
parent 531046626a
commit 4437a65d0b
3 changed files with 89 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -27,37 +27,18 @@ Author: Leonardo de Moura
#include "frontends/lean/decl_cmds.h" #include "frontends/lean/decl_cmds.h"
#include "frontends/lean/class.h" #include "frontends/lean/class.h"
#include "frontends/lean/tactic_hint.h" #include "frontends/lean/tactic_hint.h"
#include "frontends/lean/tokens.h"
namespace lean { namespace lean {
static name g_raw("raw");
static name g_true("true");
static name g_false("false");
static name g_options("options");
static name g_lparen("(");
static name g_rparen(")");
static name g_arrow("->");
static name g_lbracket("[");
static name g_rbracket("]");
static name g_declarations("declarations");
static name g_decls("decls");
static name g_hiding("hiding");
static name g_exposing("exposing");
static name g_renaming("renaming");
static name g_as("as");
static name g_colon(":");
static name g_on("[on]");
static name g_off("[off]");
static name g_none("[none]");
environment print_cmd(parser & p) { environment print_cmd(parser & p) {
if (p.curr() == scanner::token_kind::String) { if (p.curr() == scanner::token_kind::String) {
p.regular_stream() << p.get_str_val() << endl; p.regular_stream() << p.get_str_val() << endl;
p.next(); p.next();
} else if (p.curr_is_token_or_id(g_raw)) { } else if (p.curr_is_token_or_id(get_raw_tk())) {
p.next(); p.next();
expr e = p.parse_expr(); expr e = p.parse_expr();
p.regular_stream() << e << endl; p.regular_stream() << e << endl;
} else if (p.curr_is_token_or_id(g_options)) { } else if (p.curr_is_token_or_id(get_options_tk())) {
p.next(); p.next();
p.regular_stream() << p.ios().get_options() << endl; p.regular_stream() << p.ios().get_options() << endl;
} else { } else {
@ -140,9 +121,9 @@ environment set_option_cmd(parser & p) {
} }
option_kind k = decl_it->second.kind(); option_kind k = decl_it->second.kind();
if (k == BoolOption) { if (k == BoolOption) {
if (p.curr_is_token_or_id(g_true)) if (p.curr_is_token_or_id(get_true_tk()))
p.set_option(id, true); p.set_option(id, true);
else if (p.curr_is_token_or_id(g_false)) else if (p.curr_is_token_or_id(get_false_tk()))
p.set_option(id, false); p.set_option(id, false);
else else
throw parser_error("invalid Boolean option value, 'true' or 'false' expected", p.pos()); throw parser_error("invalid Boolean option value, 'true' or 'false' expected", p.pos());
@ -164,7 +145,7 @@ environment set_option_cmd(parser & p) {
} }
static name parse_class(parser & p) { static name parse_class(parser & p) {
if (p.curr_is_token(g_lbracket)) { if (p.curr_is_token(get_lbracket_tk())) {
p.next(); p.next();
name n; name n;
if (p.curr_is_identifier()) if (p.curr_is_identifier())
@ -174,7 +155,7 @@ static name parse_class(parser & p) {
else else
throw parser_error("invalid 'open' command, identifier or symbol expected", p.pos()); throw parser_error("invalid 'open' command, identifier or symbol expected", p.pos());
p.next(); p.next();
p.check_token_next(g_rbracket, "invalid 'open' command, ']' expected"); p.check_token_next(get_rbracket_tk(), "invalid 'open' command, ']' expected");
return n; return n;
} else { } else {
return name(); return name();
@ -209,7 +190,7 @@ environment open_export_cmd(parser & p, bool open) {
environment env = p.env(); environment env = p.env();
while (true) { while (true) {
name cls = parse_class(p); name cls = parse_class(p);
bool decls = cls.is_anonymous() || cls == g_decls || cls == g_declarations; bool decls = cls.is_anonymous() || cls == get_decls_tk() || cls == get_declarations_tk();
auto pos = p.pos(); auto pos = p.pos();
name ns = p.check_id_next("invalid 'open/export' command, identifier expected"); name ns = p.check_id_next("invalid 'open/export' command, identifier expected");
optional<name> real_ns = to_valid_namespace_name(env, ns); optional<name> real_ns = to_valid_namespace_name(env, ns);
@ -217,7 +198,7 @@ environment open_export_cmd(parser & p, bool open) {
throw parser_error(sstream() << "invalid namespace name '" << ns << "'", pos); throw parser_error(sstream() << "invalid namespace name '" << ns << "'", pos);
ns = *real_ns; ns = *real_ns;
name as; name as;
if (p.curr_is_token_or_id(g_as)) { if (p.curr_is_token_or_id(get_as_tk())) {
p.next(); p.next();
as = p.check_id_next("invalid 'open/export' command, identifier expected"); as = p.check_id_next("invalid 'open/export' command, identifier expected");
} }
@ -229,14 +210,14 @@ environment open_export_cmd(parser & p, bool open) {
// Remark: we currently to not allow renaming and hiding of universe levels // Remark: we currently to not allow renaming and hiding of universe levels
buffer<name> exceptions; buffer<name> exceptions;
bool found_explicit = false; bool found_explicit = false;
while (p.curr_is_token(g_lparen)) { while (p.curr_is_token(get_lparen_tk())) {
p.next(); p.next();
if (p.curr_is_token_or_id(g_renaming)) { if (p.curr_is_token_or_id(get_renaming_tk())) {
p.next(); p.next();
while (p.curr_is_identifier()) { while (p.curr_is_identifier()) {
name from_id = p.get_name_val(); name from_id = p.get_name_val();
p.next(); p.next();
p.check_token_next(g_arrow, "invalid 'open/export' command renaming, '->' expected"); p.check_token_next(get_arrow_tk(), "invalid 'open/export' command renaming, '->' expected");
name to_id = p.check_id_next("invalid 'open/export' command renaming, identifier expected"); name to_id = p.check_id_next("invalid 'open/export' command renaming, identifier expected");
check_identifier(p, env, ns, from_id); check_identifier(p, env, ns, from_id);
exceptions.push_back(from_id); exceptions.push_back(from_id);
@ -245,7 +226,7 @@ environment open_export_cmd(parser & p, bool open) {
else else
env = add_abbrev(p, env, as+to_id, ns+from_id); env = add_abbrev(p, env, as+to_id, ns+from_id);
} }
} else if (p.curr_is_token_or_id(g_hiding)) { } else if (p.curr_is_token_or_id(get_hiding_tk())) {
p.next(); p.next();
while (p.curr_is_identifier()) { while (p.curr_is_identifier()) {
name id = p.get_name_val(); name id = p.get_name_val();
@ -269,7 +250,7 @@ environment open_export_cmd(parser & p, bool open) {
} }
if (found_explicit && !exceptions.empty()) if (found_explicit && !exceptions.empty())
throw parser_error("invalid 'open/export' command option, mixing explicit and implicit 'open/export' options", p.pos()); throw parser_error("invalid 'open/export' command option, mixing explicit and implicit 'open/export' options", p.pos());
p.check_token_next(g_rparen, "invalid 'open/export' command option, ')' expected"); p.check_token_next(get_rparen_tk(), "invalid 'open/export' command option, ')' expected");
} }
if (!found_explicit) { if (!found_explicit) {
if (open) { if (open) {
@ -289,7 +270,7 @@ environment open_export_cmd(parser & p, bool open) {
} }
} }
} }
if (!p.curr_is_token(g_lbracket) && !p.curr_is_identifier()) if (!p.curr_is_token(get_lbracket_tk()) && !p.curr_is_identifier())
break; break;
} }
return env; return env;
@ -301,7 +282,7 @@ environment coercion_cmd(parser & p) {
bool persistent = false; bool persistent = false;
parse_persistent(p, persistent); parse_persistent(p, persistent);
name f = p.check_constant_next("invalid 'coercion' command, constant expected"); name f = p.check_constant_next("invalid 'coercion' command, constant expected");
if (p.curr_is_token(g_colon)) { if (p.curr_is_token(get_colon_tk())) {
p.next(); p.next();
name C = p.check_constant_next("invalid 'coercion' command, constant expected"); name C = p.check_constant_next("invalid 'coercion' command, constant expected");
return add_coercion(p.env(), f, C, p.ios(), persistent); return add_coercion(p.env(), f, C, p.ios(), persistent);
@ -313,13 +294,13 @@ environment coercion_cmd(parser & p) {
static void parse_reducible_modifiers(parser & p, reducible_status & status, bool & persistent) { static void parse_reducible_modifiers(parser & p, reducible_status & status, bool & persistent) {
while (true) { while (true) {
if (parse_persistent(p, persistent)) { if (parse_persistent(p, persistent)) {
} else if (p.curr_is_token_or_id(g_on)) { } else if (p.curr_is_token_or_id(get_on_tk())) {
p.next(); p.next();
status = reducible_status::On; status = reducible_status::On;
} else if (p.curr_is_token_or_id(g_off)) { } else if (p.curr_is_token_or_id(get_off_tk())) {
p.next(); p.next();
status = reducible_status::Off; status = reducible_status::Off;
} else if (p.curr_is_token_or_id(g_none)) { } else if (p.curr_is_token_or_id(get_none_tk())) {
p.next(); p.next();
status = reducible_status::None; status = reducible_status::None;
} else { } else {

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

@ -31,6 +31,20 @@ static name * g_assume = nullptr;
static name * g_take = nullptr; static name * g_take = nullptr;
static name * g_fun = nullptr; static name * g_fun = nullptr;
static name * g_ellipsis = nullptr; static name * g_ellipsis = nullptr;
static name * g_raw = nullptr;
static name * g_true = nullptr;
static name * g_false = nullptr;
static name * g_options = nullptr;
static name * g_arrow = nullptr;
static name * g_declarations = nullptr;
static name * g_decls = nullptr;
static name * g_hiding = nullptr;
static name * g_exposing = nullptr;
static name * g_renaming = nullptr;
static name * g_as = nullptr;
static name * g_on = nullptr;
static name * g_off = nullptr;
static name * g_none = nullptr;
void initialize_tokens() { void initialize_tokens() {
g_period = new name("."); g_period = new name(".");
@ -57,9 +71,37 @@ void initialize_tokens() {
g_take = new name("take"); g_take = new name("take");
g_fun = new name("fun"); g_fun = new name("fun");
g_ellipsis = new name("..."); g_ellipsis = new name("...");
g_raw = new name("raw");
g_true = new name("true");
g_false = new name("false");
g_options = new name("options");
g_arrow = new name("->");
g_declarations = new name("declarations");
g_decls = new name("decls");
g_hiding = new name("hiding");
g_exposing = new name("exposing");
g_renaming = new name("renaming");
g_as = new name("as");
g_on = new name("[on]");
g_off = new name("[off]");
g_none = new name("[none]");
} }
void finalize_tokens() { void finalize_tokens() {
delete g_raw;
delete g_true;
delete g_false;
delete g_options;
delete g_arrow;
delete g_declarations;
delete g_decls;
delete g_hiding;
delete g_exposing;
delete g_renaming;
delete g_as;
delete g_on;
delete g_off;
delete g_none;
delete g_ellipsis; delete g_ellipsis;
delete g_fun; delete g_fun;
delete g_take; delete g_take;
@ -110,4 +152,18 @@ name const & get_assume_tk() { return *g_assume; }
name const & get_take_tk() { return *g_take; } name const & get_take_tk() { return *g_take; }
name const & get_fun_tk() { return *g_fun; } name const & get_fun_tk() { return *g_fun; }
name const & get_ellipsis_tk() { return *g_ellipsis; } name const & get_ellipsis_tk() { return *g_ellipsis; }
name const & get_raw_tk() { return *g_raw; }
name const & get_true_tk() { return *g_true; }
name const & get_false_tk() { return *g_false; }
name const & get_options_tk() { return *g_options; }
name const & get_arrow_tk() { return *g_arrow; }
name const & get_declarations_tk() { return *g_declarations; }
name const & get_decls_tk() { return *g_decls; }
name const & get_hiding_tk() { return *g_hiding; }
name const & get_exposing_tk() { return *g_exposing; }
name const & get_renaming_tk() { return *g_renaming; }
name const & get_as_tk() { return *g_as; }
name const & get_on_tk() { return *g_on; }
name const & get_off_tk() { return *g_off; }
name const & get_none_tk() { return *g_none; }
} }

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

@ -33,4 +33,18 @@ name const & get_assume_tk();
name const & get_take_tk(); name const & get_take_tk();
name const & get_fun_tk(); name const & get_fun_tk();
name const & get_ellipsis_tk(); name const & get_ellipsis_tk();
name const & get_raw_tk();
name const & get_true_tk();
name const & get_false_tk();
name const & get_options_tk();
name const & get_arrow_tk();
name const & get_declarations_tk();
name const & get_decls_tk();
name const & get_hiding_tk();
name const & get_exposing_tk();
name const & get_renaming_tk();
name const & get_as_tk();
name const & get_on_tk();
name const & get_off_tk();
name const & get_none_tk();
} }