From 8dacd97801d496d38f50736f474cdfd7c7099f3a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Aug 2013 16:03:45 -0700 Subject: [PATCH] Remove obsolete commands. --- examples/ex12.lean | 60 ++++++++++++++++++++++++ src/frontends/lean/lean_parser.cpp | 46 ++---------------- src/shell/CMakeLists.txt | 1 + src/tests/frontends/lean/lean_parser.cpp | 2 +- 4 files changed, 65 insertions(+), 44 deletions(-) create mode 100644 examples/ex12.lean diff --git a/examples/ex12.lean b/examples/ex12.lean new file mode 100644 index 0000000000..1a17cea84a --- /dev/null +++ b/examples/ex12.lean @@ -0,0 +1,60 @@ + + +Set lean::parser::verbose false. +Notation 10 if _ then _ : implies. +Show Environment 1. +Show if true then false. +Variable a : Bool. +Show if true then if a then false. +Set lean::pp::notation false. +Show if true then if a then false. +Variable A : Type. +Variable f : A -> A -> A -> Bool. +Notation 100 _ |- _ ; _ : f. +Show Environment 1. +Variable c : A. +Variable d : A. +Variable e : A. +Show c |- d ; e. +Set lean::pp::notation true. +Show c |- d ; e. +Variable fact : A -> A. +Notation 20 _ ! : fact. +Show a! !. +Set lean::pp::notation false. +Show a! !. +Set lean::pp::notation true. +Variable g : A -> A -> A. +Notation 30 [ _ ; _ ] : g +Show [c;d]. +Show [c ; [d;e] ]. +Set lean::pp::notation false. +Show [c ; [d;e] ]. +Set lean::pp::notation true. +Variable h : A -> A -> A. +Notation 40 _ << _ end : h. +Show Environment 1. +Show d << e end. +Show [c ; d << e end ]. +Set lean::pp::notation false. +Show [c ; d << e end ]. +Set lean::pp::notation true. +Variable r : A -> A -> A. +Infixl 30 ++ : r. +Variable s : A -> A -> A. +Infixl 40 ** : s. +Show c ** d ++ e ** c. +Variable p1 : Bool. +Variable p2 : Bool. +Variable p3 : Bool. +Show p1 || p2 && p3. +Set lean::pp::notation false. +Show c ** d ++ e ** c. +Show p1 || p2 && p3. +Set lean::pp::notation true. +Show c = d || d = c. +Show not p1 || p2. +Show p1 && p3 || p2 && p3. +Set lean::pp::notation false. +Show not p1 || p2. +Show p1 && p3 || p2 && p3. diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 07682ded3f..51849971a1 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -66,23 +66,17 @@ static name g_check_kwd("Check"); static name g_infix_kwd("Infix"); static name g_infixl_kwd("Infixl"); static name g_infixr_kwd("Infixr"); -static name g_prefix_kwd("Prefix"); -static name g_postfix_kwd("Postfix"); -static name g_mixfixl_kwd("Mixfixl"); -static name g_mixfixr_kwd("Mixfixr"); -static name g_mixfixc_kwd("Mixfixc"); +static name g_notation_kwd("Notation"); static name g_echo_kwd("Echo"); static name g_set_kwd("Set"); static name g_options_kwd("Options"); static name g_env_kwd("Environment"); static name g_import_kwd("Import"); static name g_help_kwd("Help"); -static name g_notation_kwd("Notation"); /** \brief Table/List with all builtin command keywords */ static list g_command_keywords = {g_definition_kwd, g_variable_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd, - g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_prefix_kwd, - g_postfix_kwd, g_mixfixl_kwd, g_mixfixr_kwd, g_mixfixc_kwd, g_echo_kwd, - g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_notation_kwd}; + g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd, + g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd}; // ========================================== // ========================================== @@ -1188,8 +1182,6 @@ class parser::imp { name name_id = check_identifier_next("invalid operator definition, identifier expected"); expr d = mk_constant(name_id); switch (fx) { - case fixity::Prefix: m_frontend.add_prefix(op_id, prec, d); break; - case fixity::Postfix: m_frontend.add_postfix(op_id, prec, d); break; case fixity::Infix: m_frontend.add_infix(op_id, prec, d); break; case fixity::Infixl: m_frontend.add_infixl(op_id, prec, d); break; case fixity::Infixr: m_frontend.add_infixr(op_id, prec, d); break; @@ -1197,33 +1189,6 @@ class parser::imp { } } - /** - \brief Parse mixfix/mixfixl/mixfixr user operator definition. - These definitions have the form: - - - fixity [NUM] ID ID+ ':' ID - */ - void parse_mixfix_op(fixity fx) { - next(); - unsigned prec = parse_precedence(); - buffer parts; - parts.push_back(parse_op_id()); - parts.push_back(parse_op_id()); - while (!curr_is_colon()) { - parts.push_back(parse_op_id()); - } - lean_assert(curr_is_colon()); - next(); - name name_id = check_identifier_next("invalid operator definition, identifier expected"); - expr d = mk_constant(name_id); - switch (fx) { - case fixity::Mixfixl: m_frontend.add_mixfixl(parts.size(), parts.data(), prec, d); break; - case fixity::Mixfixr: m_frontend.add_mixfixr(parts.size(), parts.data(), prec, d); break; - case fixity::Mixfixc: m_frontend.add_mixfixc(parts.size(), parts.data(), prec, d); break; - default: lean_unreachable(); break; - } - } - /** \brief Parse notation declaration unified format @@ -1421,11 +1386,6 @@ class parser::imp { else if (cmd_id == g_infix_kwd) parse_op(fixity::Infix); else if (cmd_id == g_infixl_kwd) parse_op(fixity::Infixl); else if (cmd_id == g_infixr_kwd) parse_op(fixity::Infixr); - else if (cmd_id == g_prefix_kwd) parse_op(fixity::Prefix); - else if (cmd_id == g_postfix_kwd) parse_op(fixity::Postfix); - else if (cmd_id == g_mixfixl_kwd) parse_mixfix_op(fixity::Mixfixl); - else if (cmd_id == g_mixfixr_kwd) parse_mixfix_op(fixity::Mixfixr); - else if (cmd_id == g_mixfixc_kwd) parse_mixfix_op(fixity::Mixfixc); else if (cmd_id == g_notation_kwd) parse_notation_decl(); else if (cmd_id == g_echo_kwd) parse_echo(); else if (cmd_id == g_set_kwd) parse_set(); diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index f884eb0024..d1e0f73026 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -13,3 +13,4 @@ add_test(lean8 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ add_test(lean9 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex9.lean") add_test(lean10 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex10.lean") add_test(lean11 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex11.lean") +add_test(lean12 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex12.lean") diff --git a/src/tests/frontends/lean/lean_parser.cpp b/src/tests/frontends/lean/lean_parser.cpp index 3aa4ac5231..97eb9a921e 100644 --- a/src/tests/frontends/lean/lean_parser.cpp +++ b/src/tests/frontends/lean/lean_parser.cpp @@ -33,7 +33,7 @@ static void tst1() { parse(fe, "Eval true && true"); parse(fe, "Show true && false Eval true && false"); parse(fe, "Infixl 35 & : and Show true & false & false Eval true & false"); - parse(fe, "Mixfixc 100 if then fi : implies Show if true then false fi"); + parse(fe, "Notation 100 if _ then _ fi : implies Show if true then false fi"); parse(fe, "Show Pi (A : Type), A -> A"); parse(fe, "Check Pi (A : Type), A -> A"); }