From 5bd86754afe09cf031da3c7ab23141e104c6051d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Jun 2014 17:51:00 -0700 Subject: [PATCH] feat(frontends/lean/builtin_cmds): change notation for marking implicit/cast parameter in sections Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 68 +++++++++++++++--------------- src/frontends/lean/token_table.cpp | 7 +-- tests/lean/run/t11.lean | 6 +-- tests/lean/t4.lean | 2 +- tests/lean/t6.lean | 3 +- tests/lean/t7.lean | 2 +- 6 files changed, 43 insertions(+), 45 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 3b950b098..9b15e9c51 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -16,7 +16,10 @@ Author: Leonardo de Moura namespace lean { static name g_llevel_curly(".{"); +static name g_lcurly("{"); static name g_rcurly("}"); +static name g_lbracket("["); +static name g_rbracket("]"); static name g_colon(":"); static name g_assign(":="); static name g_private("[private]"); @@ -38,6 +41,28 @@ environment universe_cmd(parser & p) { return env; } +binder_info parse_open_binder_info(parser & p) { + if (p.curr_is_token(g_lcurly)) { + check_in_section(p); + p.next(); + return mk_implicit_binder_info(); + } else if (p.curr_is_token(g_lbracket)) { + check_in_section(p); + p.next(); + return mk_cast_binder_info(); + } else { + return binder_info(); + } +} + +void parse_close_binder_info(parser & p, binder_info const & bi) { + if (bi.is_implicit()) { + p.check_token_next(g_rcurly, "invalid declaration, '}' expected"); + } else if (bi.is_cast()) { + p.check_token_next(g_rbracket, "invalid declaration, ']' expected"); + } +} + bool parse_univ_params(parser & p, buffer & ps) { if (p.curr_is_token(g_llevel_curly)) { p.next(); @@ -83,8 +108,9 @@ static environment declare_var(parser & p, environment env, } } -environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) { +environment variable_cmd_core(parser & p, bool is_axiom) { auto pos = p.pos(); + binder_info bi = parse_open_binder_info(p); name n = p.check_id_next("invalid declaration, identifier expected"); check_atomic(n); buffer ls_buffer; @@ -106,6 +132,7 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) p.next(); type = p.parse_expr(); } + parse_close_binder_info(p, bi); level_param_names ls; if (in_section(p.env())) { ls = to_level_param_names(collect_univ_params(type)); @@ -117,22 +144,10 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) return declare_var(p, p.env(), n, ls, type, is_axiom, bi, pos); } environment variable_cmd(parser & p) { - return variable_cmd_core(p, false, binder_info()); + return variable_cmd_core(p, false); } environment axiom_cmd(parser & p) { - return variable_cmd_core(p, true, binder_info()); -} -environment implicit_variable_cmd(parser & p) { - check_in_section(p); - return variable_cmd_core(p, false, mk_implicit_binder_info()); -} -environment implicit_axiom_cmd(parser & p) { - check_in_section(p); - return variable_cmd_core(p, true, mk_implicit_binder_info()); -} -environment cast_variable_cmd(parser & p) { - check_in_section(p); - return variable_cmd_core(p, false, mk_cast_binder_info()); + return variable_cmd_core(p, true); } // Sort local_names by order of occurrence in the section, and copy the associated parameters to section_ps @@ -264,9 +279,10 @@ environment theorem_cmd(parser & p) { return definition_cmd_core(p, true, true); } -static environment variables_cmd_core(parser & p, bool is_axiom, binder_info const & bi) { +static environment variables_cmd(parser & p) { auto pos = p.pos(); buffer ids; + binder_info bi = parse_open_binder_info(p); while (!p.curr_is_token(g_colon)) { name id = p.check_id_next("invalid parameters declaration, identifier expected"); check_atomic(id); @@ -278,37 +294,23 @@ static environment variables_cmd_core(parser & p, bool is_axiom, binder_info con scope1.emplace(p); parser::param_universe_scope scope2(p); expr type = p.parse_expr(); + parse_close_binder_info(p, bi); level_param_names ls = to_level_param_names(collect_univ_params(type)); type = p.elaborate(type, ls); environment env = p.env(); for (auto id : ids) - env = declare_var(p, env, id, ls, type, is_axiom, bi, pos); + env = declare_var(p, env, id, ls, type, true, bi, pos); return env; } -environment variables_cmd(parser & p) { - return variables_cmd_core(p, false, binder_info()); -} -environment implicit_variables_cmd(parser & p) { - check_in_section(p); - return variables_cmd_core(p, false, mk_implicit_binder_info()); -} -environment cast_variables_cmd(parser & p) { - check_in_section(p); - return variables_cmd_core(p, false, mk_cast_binder_info()); -} + void register_decl_cmds(cmd_table & r) { add_cmd(r, cmd_info("universe", "declare a global universe level", universe_cmd)); add_cmd(r, cmd_info("variable", "declare a new parameter", variable_cmd)); - add_cmd(r, cmd_info("{variable}", "declare a new implict parameter", implicit_variable_cmd)); - add_cmd(r, cmd_info("[variable]", "declare a new cast parameter", cast_variable_cmd)); add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd)); - add_cmd(r, cmd_info("{axiom}", "declare a new implicit axiom", implicit_axiom_cmd)); add_cmd(r, cmd_info("definition", "add new definition", definition_cmd)); add_cmd(r, cmd_info("abbreviation", "add new abbreviation (aka transparent definition)", abbreviation_cmd)); add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd)); add_cmd(r, cmd_info("variables", "declare new parameters", variables_cmd)); - add_cmd(r, cmd_info("{variables}", "declare new implict parameters", implicit_variables_cmd)); - add_cmd(r, cmd_info("[variables]", "declare new cast parameters", cast_variables_cmd)); } } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 92b42d349..d3e13022e 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -61,8 +61,8 @@ token_table init_token_table() { {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; - char const * commands[] = {"theorem", "axiom", "variable", "definition", "{axiom}", "{variable}", "[variable]", - "variables", "{variables}", "[variables]", "[private]", "[inline]", "[fact]", "abbreviation", + char const * commands[] = {"theorem", "axiom", "variable", "definition", + "variables", "[private]", "[inline]", "[fact]", "abbreviation", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "notation", "exit", "set_option", @@ -75,9 +75,6 @@ token_table init_token_table() { std::pair cmd_aliases[] = {{"parameter", "variable"}, {"parameters", "variables"}, {"lemma", "theorem"}, {"hypothesis", "axiom"}, {"conjecture", "axiom"}, {"corollary", "theorem"}, - {"{parameter}", "{variable}"}, {"{parameters}", "{variables}"}, - {"[parameter]", "[variable]"}, {"[parameters]", "[variables]"}, - {"{hypothesis}", "{axiom}"}, {"{conjecture}", "{axiom}"}, {nullptr, nullptr}}; auto it = builtin; diff --git a/tests/lean/run/t11.lean b/tests/lean/run/t11.lean index 17a59fd37..bd5350f8a 100644 --- a/tests/lean/run/t11.lean +++ b/tests/lean/run/t11.lean @@ -3,9 +3,9 @@ parameters a b c : A parameter f : A → A → A check f a b section - parameters A B : Type - {parameters} C D : Type - [parameters] e d : A + parameters A B : Type + parameters {C D : Type} + parameters [e d : A] check A check B definition g (a : A) (b : B) (c : C) : A := e diff --git a/tests/lean/t4.lean b/tests/lean/t4.lean index f51ddecc8..9118bf0de 100644 --- a/tests/lean/t4.lean +++ b/tests/lean/t4.lean @@ -17,7 +17,7 @@ section variable A : Type variable B : Bool hypothesis H : B - {parameter} C : Type + parameter {C : Type} check B -> B check A → A check C diff --git a/tests/lean/t6.lean b/tests/lean/t6.lean index 049a48229..40bb5b2f9 100644 --- a/tests/lean/t6.lean +++ b/tests/lean/t6.lean @@ -1,6 +1,6 @@ definition Bool : Type.{1} := Type.{0} section - {parameter} A : Type -- Mark A as implicit parameter + parameter {A : Type} -- Mark A as implicit parameter parameter R : A → A → Bool definition id (a : A) : A := a definition refl : Bool := forall (a : A), R a a @@ -9,4 +9,3 @@ end check id.{2} check refl.{1} check symm.{1} - diff --git a/tests/lean/t7.lean b/tests/lean/t7.lean index 480650c2a..3a440c6de 100644 --- a/tests/lean/t7.lean +++ b/tests/lean/t7.lean @@ -1,7 +1,7 @@ definition Bool : Type.{1} := Type.{0} variable and : Bool → Bool → Bool section - {parameter} A : Type -- Mark A as implicit parameter + parameter {A : Type} -- Mark A as implicit parameter parameter R : A → A → Bool parameter B : Type definition id (a : A) : A := a