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

fix(frontends/lean/token_table): static initialization problem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-11 10:56:04 -07:00
parent 3dc26666b9
commit 8fcc25d55a
1 changed files with 49 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -40,56 +40,61 @@ static char const * g_pi_unicode = "\u03A0";
static char const * g_forall_unicode = "\u2200"; static char const * g_forall_unicode = "\u2200";
static char const * g_arrow_unicode = "\u2192"; static char const * g_arrow_unicode = "\u2192";
// Auxiliary class for creating the initial token set token_table init_token_table() {
class init_token_table_fn { token_table t;
public: char const * builtin[] = {"fun", "Pi", "let", "in", "have", "show", "by", "from", "(", ")", "{", "}",
token_table m_token_table; ".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--", "->",
init_token_table_fn() { "proof", "qed", "private", nullptr};
char const * builtin[] = {"fun", "Pi", "let", "in", "have", "show", "by", "from", "(", ")", "{", "}",
".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--", "->",
"proof", "qed", "private", nullptr};
char const * commands[] = {"theorem", "axiom", "variable", "definition", "evaluate", "check", char const * commands[] = {"theorem", "axiom", "variable", "definition", "evaluate", "check",
"print", "variables", "end", "namespace", "section", "import", "print", "variables", "end", "namespace", "section", "import",
"abbreviation", "inductive", "record", "structure", "module", nullptr}; "abbreviation", "inductive", "record", "structure", "module", nullptr};
std::pair<char const *, char const *> aliases[] = std::pair<char const *, char const *> aliases[] =
{{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
{g_arrow_unicode, "->"}, {nullptr, nullptr}}; {g_arrow_unicode, "->"}, {nullptr, nullptr}};
std::pair<char const *, char const *> cmd_aliases[] = std::pair<char const *, char const *> cmd_aliases[] =
{{"parameter", "variable"}, {"parameters", "variables"}, {"lemma", "theorem"}, {{"parameter", "variable"}, {"parameters", "variables"}, {"lemma", "theorem"},
{"hypothesis", "axiom"}, {"conjecture", "axiom"}, {"corollary", "theorem"}, {"hypothesis", "axiom"}, {"conjecture", "axiom"}, {"corollary", "theorem"},
{nullptr, nullptr}}; {nullptr, nullptr}};
auto it = builtin; auto it = builtin;
while (*it) { while (*it) {
m_token_table = add_token(m_token_table, *it); t = add_token(t, *it);
it++; it++;
}
it = commands;
while (*it) {
m_token_table = add_command_token(m_token_table, *it);
++it;
}
auto it2 = aliases;
while (it2->first) {
m_token_table = add_token(m_token_table, it2->first, it2->second);
it2++;
}
it2 = cmd_aliases;
while (it2->first) {
m_token_table = add_command_token(m_token_table, it2->first, it2->second);
++it2;
}
} }
};
static init_token_table_fn g_init; it = commands;
while (*it) {
t = add_command_token(t, *it);
++it;
}
auto it2 = aliases;
while (it2->first) {
t = add_token(t, it2->first, it2->second);
it2++;
}
it2 = cmd_aliases;
while (it2->first) {
t = add_command_token(t, it2->first, it2->second);
++it2;
}
return t;
}
token_table mk_default_token_table() {
static optional<token_table> r;
if (!r)
r = init_token_table();
return *r;
}
static token_table g_init(mk_default_token_table());
token_table mk_token_table() { return token_table(); } token_table mk_token_table() { return token_table(); }
token_table mk_default_token_table() { return g_init.m_token_table; }
DECL_UDATA(token_table) DECL_UDATA(token_table)
static int mk_token_table(lua_State * L) { return push_token_table(L, mk_token_table()); } static int mk_token_table(lua_State * L) { return push_token_table(L, mk_token_table()); }