From b9d08ff28c0792a48fa9922e46e45c05703a5b9e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Jul 2014 14:53:06 -0700 Subject: [PATCH] feat(frontends/lean/builtin_cmds): allow many namespaces in the same 'using' command Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 84 +++++++++++++++-------------- tests/lean/run/class1.lean | 3 +- tests/lean/run/class2.lean | 3 +- tests/lean/run/class3.lean | 3 +- tests/lean/run/class5.lean | 3 +- 5 files changed, 48 insertions(+), 48 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 5cf604320..b1025a9e2 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -170,52 +170,56 @@ static void check_identifier(parser & p, environment const & env, name const & n // using [class] id (id ...) (renaming id->id id->id) (hiding id ... id) environment using_cmd(parser & p) { environment env = p.env(); - name cls = parse_class(p); - bool decls = cls.is_anonymous() || cls == g_decls || cls == g_declarations; - name ns = p.check_id_next("invalid 'using' command, identifier expected"); - env = using_namespace(env, p.ios(), ns, cls); - if (decls) { - // Remark: we currently to not allow renaming and hiding of universe levels - buffer exceptions; - bool found_explicit = false; - while (p.curr_is_token(g_lparen)) { - p.next(); - if (p.curr_is_token_or_id(g_renaming)) { + while (true) { + name cls = parse_class(p); + bool decls = cls.is_anonymous() || cls == g_decls || cls == g_declarations; + name ns = p.check_id_next("invalid 'using' command, identifier expected"); + env = using_namespace(env, p.ios(), ns, cls); + if (decls) { + // Remark: we currently to not allow renaming and hiding of universe levels + buffer exceptions; + bool found_explicit = false; + while (p.curr_is_token(g_lparen)) { p.next(); - while (p.curr_is_identifier()) { - name from_id = p.get_name_val(); + if (p.curr_is_token_or_id(g_renaming)) { p.next(); - p.check_token_next(g_arrow, "invalid 'using' command renaming, '->' expected"); - name to_id = p.check_id_next("invalid 'using' command renaming, identifier expected"); - check_identifier(p, env, ns, from_id); - exceptions.push_back(from_id); - env = add_alias(env, to_id, mk_constant(ns+from_id)); - } - } else if (p.curr_is_token_or_id(g_hiding)) { - p.next(); - while (p.curr_is_identifier()) { - name id = p.get_name_val(); + while (p.curr_is_identifier()) { + name from_id = p.get_name_val(); + p.next(); + p.check_token_next(g_arrow, "invalid 'using' command renaming, '->' expected"); + name to_id = p.check_id_next("invalid 'using' command renaming, identifier expected"); + check_identifier(p, env, ns, from_id); + exceptions.push_back(from_id); + env = add_alias(env, to_id, mk_constant(ns+from_id)); + } + } else if (p.curr_is_token_or_id(g_hiding)) { p.next(); - check_identifier(p, env, ns, id); - exceptions.push_back(id); + while (p.curr_is_identifier()) { + name id = p.get_name_val(); + p.next(); + check_identifier(p, env, ns, id); + exceptions.push_back(id); + } + } else if (p.curr_is_identifier()) { + found_explicit = true; + while (p.curr_is_identifier()) { + name id = p.get_name_val(); + p.next(); + check_identifier(p, env, ns, id); + env = add_alias(env, id, mk_constant(ns+id)); + } + } else { + throw parser_error("invalid 'using' command option, identifier, 'hiding' or 'renaming' expected", p.pos()); } - } else if (p.curr_is_identifier()) { - found_explicit = true; - while (p.curr_is_identifier()) { - name id = p.get_name_val(); - p.next(); - check_identifier(p, env, ns, id); - env = add_alias(env, id, mk_constant(ns+id)); - } - } else { - throw parser_error("invalid 'using' command option, identifier, 'hiding' or 'renaming' expected", p.pos()); + if (found_explicit && !exceptions.empty()) + throw parser_error("invalid 'using' command option, mixing explicit and implicit 'using' options", p.pos()); + p.check_token_next(g_rparen, "invalid 'using' command option, ')' expected"); } - if (found_explicit && !exceptions.empty()) - throw parser_error("invalid 'using' command option, mixing explicit and implicit 'using' options", p.pos()); - p.check_token_next(g_rparen, "invalid 'using' command option, ')' expected"); + if (!found_explicit) + env = add_aliases(env, ns, name(), exceptions.size(), exceptions.data()); } - if (!found_explicit) - env = add_aliases(env, ns, name(), exceptions.size(), exceptions.data()); + if (!p.curr_is_token(g_lbracket) && !p.curr_is_identifier()) + break; } return env; } diff --git a/tests/lean/run/class1.lean b/tests/lean/run/class1.lean index 3d1eacb71..dd72065b7 100644 --- a/tests/lean/run/class1.lean +++ b/tests/lean/run/class1.lean @@ -1,6 +1,5 @@ import standard -using num -using pair +using num pair definition H : inhabited (Bool × num × (num → num)) := _ diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean index 53945b678..cc06516cb 100644 --- a/tests/lean/run/class2.lean +++ b/tests/lean/run/class2.lean @@ -1,6 +1,5 @@ import standard -using num -using pair +using num pair theorem H {A B : Type} (H1 : inhabited A) : inhabited (Bool × A × (B → num)) := _ diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean index 767ddb9ae..2ffc19b93 100644 --- a/tests/lean/run/class3.lean +++ b/tests/lean/run/class3.lean @@ -1,6 +1,5 @@ import standard -using num -using pair +using num pair section parameter {A : Type} diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean index 17ddf5f2b..c382bd38e 100644 --- a/tests/lean/run/class5.lean +++ b/tests/lean/run/class5.lean @@ -25,8 +25,7 @@ namespace nat end section - using algebra - using nat + using algebra nat variables a b c : nat check a * b * c end