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

Remove obsolete commands.

Browse source
This commit is contained in:
Leonardo de Moura 2013-08-27 16:03:45 -07:00
parent a9c6088d11
commit 8dacd97801
4 changed files with 65 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
examples/ex12.lean Normal file
View file

@ -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.

46
src/frontends/lean/lean_parser.cpp
View file

@ -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<name> 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<name> 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();

1
src/shell/CMakeLists.txt
View file

@ -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")

2
src/tests/frontends/lean/lean_parser.cpp
View file

@ -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");
}