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

feat(frontends/lean): parse argument of unary tactis with rbp=0, tokens may have a different precedence in expression and tactic modes

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-28 13:43:05 -07:00
parent 4283111198
commit 1be72f1faa
12 changed files with 164 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
src/frontends/lean/notation_cmd.cpp
View file

@ -96,6 +96,28 @@ void check_not_forbidden(char const * tk) {
}
}
static optional<unsigned> get_precedence(environment const & env, char const * tk, bool is_expr) {
if (is_expr)
return get_expr_precedence(get_token_table(env), tk);
else
return get_tactic_precedence(get_token_table(env), tk);
}
static optional<unsigned> get_precedence(environment const & env, char const * tk, notation_entry_group grp) {
return get_precedence(env, tk, grp != notation_entry_group::Tactic);
}
static token_entry mk_token_entry(std::string const & tk, unsigned prec, bool is_expr) {
if (is_expr)
return mk_expr_token_entry(tk, prec);
else
return mk_tactic_token_entry(tk, prec);
}
static token_entry mk_token_entry(std::string const & tk, unsigned prec, notation_entry_group grp) {
return mk_token_entry(tk, prec, grp != notation_entry_group::Tactic);
}
static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, bool parse_only)
-> pair<notation_entry, optional<token_entry>> {
std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
@ -107,7 +129,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
optional<parse_table> reserved_pt;
optional<action> reserved_action;
if (grp != notation_entry_group::Reserve) {
if (grp == notation_entry_group::Main) {
if (k == mixfix_kind::prefix) {
if (auto at = get_reserved_nud_table(p.env()).find(tks)) {
reserved_pt = at->second;
@ -134,18 +156,20 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
if (!prec) {
if (reserved_action && k == mixfix_kind::prefix && reserved_action->kind() == notation::action_kind::Expr) {
lean_assert(grp == notation_entry_group::Main);
prec = reserved_action->rbp();
} else if (reserved_action && k == mixfix_kind::infixr && reserved_action->kind() == notation::action_kind::Expr) {
lean_assert(grp == notation_entry_group::Main);
prec = reserved_action->rbp();
} else {
prec = get_precedence(get_token_table(env), tk.c_str());
prec = get_precedence(env, tk.c_str(), grp);
if (prec && k == mixfix_kind::infixr)
prec = *prec - 1;
}
} else {
auto old_prec = get_precedence(get_token_table(env), tk.c_str());
auto old_prec = get_precedence(env, tk.c_str(), grp);
if (!old_prec || (k != mixfix_kind::prefix && old_prec != prec))
new_token = token_entry(tk.c_str(), *prec);
new_token = mk_token_entry(tk.c_str(), *prec, grp);
if (k == mixfix_kind::infixr)
prec = *prec - 1;
}
@ -231,7 +255,7 @@ static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool over
return nt.first;
}
static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens, bool & used_default) {
static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens, bool & used_default, notation_entry_group grp) {
used_default = false;
if (p.curr_is_quoted_symbol()) {
environment const & env = p.env();
@ -243,11 +267,11 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
if (p.curr_is_token(get_colon_tk())) {
p.next();
unsigned prec = parse_precedence(p);
auto old_prec = get_precedence(get_token_table(env), tkcs);
auto old_prec = get_precedence(env, tkcs, grp);
if (!old_prec || prec != *old_prec)
new_tokens.push_back(token_entry(tkcs, prec));
} else if (!get_precedence(get_token_table(env), tkcs)) {
new_tokens.push_back(token_entry(tkcs, LEAN_DEFAULT_PRECEDENCE));
new_tokens.push_back(mk_token_entry(tkcs, prec, grp));
} else if (!get_precedence(env, tkcs, grp)) {
new_tokens.push_back(mk_token_entry(tkcs, LEAN_DEFAULT_PRECEDENCE, grp));
used_default = true;
}
return tk;
@ -261,9 +285,9 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
}
}
static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens) {
static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens, notation_entry_group grp) {
bool dummy;
return parse_quoted_symbol_or_token(p, new_tokens, dummy);
return parse_quoted_symbol_or_token(p, new_tokens, dummy, grp);
}
static expr parse_notation_expr(parser & p, buffer<expr> const & locals) {
@ -293,7 +317,7 @@ static unsigned get_precedence(environment const & env, buffer<token_entry> cons
if (e.m_token == token_str)
return e.m_prec;
}
auto prec = get_precedence(get_token_table(env), token_str.c_str());
auto prec = get_expr_precedence(get_token_table(env), token_str.c_str());
if (prec)
return *prec;
else
@ -301,7 +325,7 @@ static unsigned get_precedence(environment const & env, buffer<token_entry> cons
}
static action parse_action(parser & p, name const & prev_token, unsigned default_prec,
buffer<expr> & locals, buffer<token_entry> & new_tokens) {
buffer<expr> & locals, buffer<token_entry> & new_tokens, notation_entry_group grp) {
if (p.curr_is_token(get_colon_tk())) {
p.next();
if (p.curr_is_numeral() || p.curr_is_token_or_id(get_max_tk())) {
@ -323,7 +347,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
bool is_fold_right = p.curr_is_token_or_id(get_foldr_tk());
p.next();
auto prec = parse_optional_precedence(p);
name sep = parse_quoted_symbol_or_token(p, new_tokens);
name sep = parse_quoted_symbol_or_token(p, new_tokens, grp);
expr rec;
{
parser::local_scope scope(p);
@ -341,7 +365,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
ini = parse_notation_expr(p, locals);
optional<name> terminator;
if (!p.curr_is_token(get_rparen_tk()))
terminator = parse_quoted_symbol_or_token(p, new_tokens);
terminator = parse_quoted_symbol_or_token(p, new_tokens, grp);
p.check_token_next(get_rparen_tk(), "invalid fold notation argument, ')' expected");
return mk_exprs_action(sep, rec, ini, terminator, is_fold_right, prec ? *prec : 0);
} else if (p.curr_is_token_or_id(get_scoped_tk())) {
@ -446,7 +470,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
bool used_default = false;
while ((grp != notation_entry_group::Reserve && !p.curr_is_token(get_assign_tk())) ||
(grp == notation_entry_group::Reserve && !p.curr_is_command() && !p.curr_is_eof())) {
name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default);
name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default, grp);
if (auto at = find_next(reserved_pt, tk)) {
action const & a = at->first;
reserved_pt = at->second;
@ -499,7 +523,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
unsigned default_prec = get_default_prec(pt, tk);
name n = p.get_name_val();
p.next();
action a = parse_action(p, tk, default_prec, locals, new_tokens);
action a = parse_action(p, tk, default_prec, locals, new_tokens, grp);
expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant
expr l = mk_local(n, local_type);
p.add_local(l);
@ -606,7 +630,7 @@ static environment add_user_token(environment const & env, token_entry const & e
static environment add_user_token(environment const & env, char const * val, unsigned prec) {
check_token(val);
return add_token(env, val, prec);
return add_expr_token(env, val, prec);
}
struct notation_modifiers {

2
src/frontends/lean/parse_table.cpp
View file

@ -488,7 +488,7 @@ void display(io_state_stream & out, unsigned num, transition const * ts, list<ex
if (i > 0) out << " ";
out << "`" << ts[i].get_token() << "`";
if (tt) {
if (auto prec = get_precedence(*tt, ts[i].get_token().to_string().c_str())) {
if (auto prec = get_expr_precedence(*tt, ts[i].get_token().to_string().c_str())) {
out << ":" << *prec;
}
}

20
src/frontends/lean/parser.cpp
View file

@ -1282,10 +1282,13 @@ expr parser::parse_led(expr left) {
}
}
unsigned parser::curr_lbp() const {
unsigned parser::curr_lbp_core(bool as_tactic) const {
switch (curr()) {
case scanner::token_kind::Keyword:
return get_token_info().precedence();
if (as_tactic)
return get_token_info().tactic_precedence();
else
return get_token_info().expr_precedence();
case scanner::token_kind::CommandKeyword: case scanner::token_kind::Eof:
case scanner::token_kind::ScriptBlock: case scanner::token_kind::QuotedSymbol:
return 0;
@ -1298,7 +1301,7 @@ unsigned parser::curr_lbp() const {
expr parser::parse_expr(unsigned rbp) {
expr left = parse_nud();
while (rbp < curr_lbp()) {
while (rbp < curr_expr_lbp()) {
left = parse_led(left);
}
return left;
@ -1314,7 +1317,7 @@ pair<optional<name>, expr> parser::parse_id_tk_expr(name const & tk, unsigned rb
return mk_pair(optional<name>(id), parse_expr(rbp));
} else {
expr left = id_to_expr(id, id_pos);
while (rbp < curr_lbp()) {
while (rbp < curr_expr_lbp()) {
left = parse_led(left);
}
return mk_pair(optional<name>(), left);
@ -1449,6 +1452,7 @@ expr parser::parse_tactic_nud() {
if (optional<expr> tac_type = is_tactic_command(id)) {
next();
expr type = *tac_type;
bool unary = get_arity(type) == 1;
expr r = save_pos(mk_constant(id), id_pos);
while (is_pi(type)) {
expr d = binding_domain(type);
@ -1459,13 +1463,15 @@ expr parser::parse_tactic_nud() {
} else if (is_tactic_opt_expr_list_type(d)) {
r = mk_app(r, parse_tactic_opt_expr_list(), id_pos);
} else if (is_tactic_identifier_type(d)) {
r = mk_app(r, mk_local(check_id_next("invalid tactic, identifier expected"), mk_expr_placeholder()), id_pos);
r = mk_app(r, mk_local(check_id_next("invalid tactic, identifier expected"),
mk_expr_placeholder()), id_pos);
} else if (is_tactic_identifier_list_type(d)) {
r = mk_app(r, parse_tactic_id_list(), id_pos);
} else if (is_tactic_opt_identifier_list_type(d)) {
r = mk_app(r, parse_tactic_opt_id_list(), id_pos);
} else {
r = mk_app(r, parse_expr(get_max_prec()), id_pos);
unsigned prec = unary ? 1 : get_max_prec();
r = mk_app(r, parse_expr(prec), id_pos);
}
type = binding_body(type);
}
@ -1490,7 +1496,7 @@ expr parser::parse_tactic_led(expr left) {
expr parser::parse_tactic(unsigned rbp) {
expr left = parse_tactic_nud();
while (rbp < curr_lbp()) {
while (rbp < curr_tactic_lbp()) {
left = parse_tactic_led(left);
}
return left;

4
src/frontends/lean/parser.h
View file

@ -182,7 +182,9 @@ class parser {
void parse_command();
void parse_script(bool as_expr = false);
bool parse_commands();
unsigned curr_lbp() const;
unsigned curr_lbp_core(bool as_tactic) const;
unsigned curr_expr_lbp() const { return curr_lbp_core(false); }
unsigned curr_tactic_lbp() const { return curr_lbp_core(true); }
expr parse_notation_core(parse_table t, expr * left, bool as_tactic);
expr parse_expr_or_tactic(unsigned rbp, bool as_tactic) {
return as_tactic ? parse_tactic(rbp) : parse_expr(rbp);

16
src/frontends/lean/parser_config.cpp
View file

@ -83,7 +83,10 @@ struct token_config {
static std::string * g_key;
static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
if (e.m_expr)
s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec);
else
s.m_table = add_tactic_token(s.m_table, e.m_token.c_str(), e.m_prec);
}
static name const & get_class_name() {
return *g_class_name;
@ -92,12 +95,13 @@ struct token_config {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << e.m_token.c_str() << e.m_prec;
s << e.m_expr << e.m_token.c_str() << e.m_prec;
}
static entry read_entry(deserializer & d) {
bool is_expr = d.read_bool();
std::string tk = d.read_string();
unsigned prec = d.read_unsigned();
return entry(tk, prec);
return entry(is_expr, tk, prec);
}
static optional<unsigned> get_fingerprint(entry const &) {
return optional<unsigned>();
@ -113,8 +117,12 @@ environment add_token(environment const & env, token_entry const & e, bool persi
return token_ext::add_entry(env, get_dummy_ios(), e, persistent);
}
environment add_token(environment const & env, char const * val, unsigned prec) {
return add_token(env, token_entry(val, prec));
environment add_expr_token(environment const & env, char const * val, unsigned prec) {
return add_token(env, token_entry(true, val, prec));
}
environment add_tactic_token(environment const & env, char const * val, unsigned prec) {
return add_token(env, token_entry(false, val, prec));
}
token_table const & get_token_table(environment const & env) {

9
src/frontends/lean/parser_config.h
View file

@ -13,10 +13,13 @@ Author: Leonardo de Moura
namespace lean {
struct token_entry {
bool m_expr; // true if it precedence for an expression token
std::string m_token;
unsigned m_prec;
token_entry(std::string const & tk, unsigned prec):m_token(tk), m_prec(prec) {}
token_entry(bool e, std::string const & tk, unsigned prec):m_expr(e), m_token(tk), m_prec(prec) {}
};
inline token_entry mk_expr_token_entry(std::string const & tk, unsigned prec) { return token_entry(true, tk, prec); }
inline token_entry mk_tactic_token_entry(std::string const & tk, unsigned prec) { return token_entry(false, tk, prec); }
enum class notation_entry_kind { NuD, LeD, Numeral };
enum class notation_entry_group { Main, Reserve, Tactic };
@ -62,7 +65,9 @@ notation_entry replace(notation_entry const & e, std::function<expr(expr const &
environment add_token(environment const & env, token_entry const & e, bool persistent = true);
environment add_notation(environment const & env, notation_entry const & e, bool persistent = true);
environment add_token(environment const & env, char const * val, unsigned prec);
environment add_expr_token(environment const & env, char const * val, unsigned prec);
environment add_tactic_token(environment const & env, char const * val, unsigned prec);
environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,
bool overload = true, notation_entry_group g = notation_entry_group::Main, bool parse_only = false);
environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,

4
src/frontends/lean/pp.cpp
View file

@ -845,10 +845,10 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
static unsigned get_some_precedence(token_table const & t, name const & tk) {
if (tk.is_atomic() && tk.is_string()) {
if (auto p = get_precedence(t, tk.get_string()))
if (auto p = get_expr_precedence(t, tk.get_string()))
return *p;
} else {
if (auto p = get_precedence(t, tk.to_string().c_str()))
if (auto p = get_expr_precedence(t, tk.to_string().c_str()))
return *p;
}
return 0;

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

@ -20,6 +20,20 @@ unsigned get_max_prec() { return g_max_prec; }
unsigned get_Max_prec() { return g_Max_prec; }
unsigned get_arrow_prec() { return g_arrow_prec; }
unsigned get_decreasing_prec() { return g_decreasing_prec; }
static token_table update(token_table const & s, char const * token, char const * val,
optional<unsigned> expr_prec, optional<unsigned> tac_prec) {
lean_assert(expr_prec || tac_prec);
token_info info(token, val, 0, 0);
if (token_info const * old_info = find(s, token)) {
info = info.update_expr_precedence(old_info->expr_precedence());
info = info.update_tactic_precedence(old_info->tactic_precedence());
}
if (expr_prec)
info = info.update_expr_precedence(*expr_prec);
if (tac_prec)
info = info.update_tactic_precedence(*tac_prec);
return insert(s, token, info);
}
token_table add_command_token(token_table const & s, char const * token) {
return insert(s, token, token_info(token));
}
@ -27,10 +41,16 @@ token_table add_command_token(token_table const & s, char const * token, char co
return insert(s, token, token_info(token, val));
}
token_table add_token(token_table const & s, char const * token, unsigned prec) {
return insert(s, token, token_info(token, prec));
return update(s, token, token, optional<unsigned>(prec), optional<unsigned>());
}
token_table add_token(token_table const & s, char const * token, char const * val, unsigned prec) {
return insert(s, token, token_info(token, val, prec));
return update(s, token, val, optional<unsigned>(prec), optional<unsigned>());
}
token_table add_tactic_token(token_table const & s, char const * token, unsigned prec) {
return update(s, token, token, optional<unsigned>(), optional<unsigned>(prec));
}
token_table add_tactic_token(token_table const & s, char const * token, char const * val, unsigned prec) {
return update(s, token, val, optional<unsigned>(), optional<unsigned>(prec));
}
token_table const * find(token_table const & s, char c) {
return s.find(c);
@ -38,9 +58,13 @@ token_table const * find(token_table const & s, char c) {
token_info const * value_of(token_table const & s) {
return s.value();
}
optional<unsigned> get_precedence(token_table const & s, char const * token) {
optional<unsigned> get_expr_precedence(token_table const & s, char const * token) {
auto it = find(s, token);
return it ? optional<unsigned>(it->precedence()) : optional<unsigned>();
return it ? optional<unsigned>(it->expr_precedence()) : optional<unsigned>();
}
optional<unsigned> get_tactic_precedence(token_table const & s, char const * token) {
auto it = find(s, token);
return it ? optional<unsigned>(it->tactic_precedence()) : optional<unsigned>();
}
bool is_token(token_table const & s, char const * token) {
return static_cast<bool>(find(s, token));
@ -53,16 +77,6 @@ void for_each(token_table const & s, std::function<void(char const *, token_info
fn(str.data(), info);
});
}
void display(std::ostream & out, token_table const & s) {
for_each(s, [&](char const * token, token_info const & info) {
out << "`" << token << "`:" << info.precedence();
if (info.is_command())
out << " [command]";
if (info.value() != info.token())
out << " " << info.value();
out << "\n";
});
}
static char const * g_lambda_unicode = "\u03BB";
static char const * g_pi_unicode = "\u03A0";
@ -79,7 +93,7 @@ void init_token_table(token_table & t) {
{"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
{"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
{"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {";", 1},
{"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0},
{".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {"fold", 0}, {"unfold", 0},
{":=", 0}, {"--", 0}, {"#", 0},
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
@ -197,7 +211,7 @@ static int value_of(lua_State * L) {
if (it) {
push_boolean(L, it->is_command());
push_name(L, it->value());
push_integer(L, it->precedence());
push_integer(L, it->expr_precedence());
return 3;
} else {
push_nil(L);
@ -212,7 +226,7 @@ static int for_each(lua_State * L) {
lua_pushstring(L, k);
lua_pushboolean(L, info.is_command());
push_name(L, info.value());
lua_pushinteger(L, info.precedence());
lua_pushinteger(L, info.expr_precedence());
pcall(L, 4, 0, 0);
});
return 0;

31
src/frontends/lean/token_table.h
View file

@ -26,21 +26,30 @@ class token_info {
bool m_command;
name m_token;
name m_value;
unsigned m_precedence;
unsigned m_expr_precedence;
unsigned m_tactic_precedence;
token_info(bool c, name const & t, name const & v, unsigned ep, unsigned tp):
m_command(c), m_token(t), m_value(v), m_expr_precedence(ep), m_tactic_precedence(tp) {}
public:
token_info():m_command(true) {}
token_info(char const * val):
m_command(true), m_token(val), m_value(val), m_precedence(LEAN_DEFAULT_PRECEDENCE) {}
m_command(true), m_token(val), m_value(val), m_expr_precedence(0), m_tactic_precedence(0) {}
token_info(char const * token, char const * val):
m_command(true), m_token(token), m_value(val), m_precedence(LEAN_DEFAULT_PRECEDENCE) {}
token_info(char const * val, unsigned prec):
m_command(false), m_token(val), m_value(val), m_precedence(prec) {}
token_info(char const * token, char const * val, unsigned prec):
m_command(false), m_token(token), m_value(val), m_precedence(prec) {}
m_command(true), m_token(token), m_value(val), m_expr_precedence(0), m_tactic_precedence(0) {}
token_info(char const * token, char const * val, unsigned prec, unsigned tac_prec):
m_command(false), m_token(token), m_value(val),
m_expr_precedence(prec), m_tactic_precedence(tac_prec) {}
bool is_command() const { return m_command; }
name const & token() const { return m_token; }
name const & value() const { return m_value; }
unsigned precedence() const { return m_precedence; }
unsigned expr_precedence() const { return m_expr_precedence; }
unsigned tactic_precedence() const { return m_tactic_precedence; }
token_info update_expr_precedence(unsigned prec) const {
return token_info(m_command, m_token, m_value, prec, m_tactic_precedence);
}
token_info update_tactic_precedence(unsigned prec) const {
return token_info(m_command, m_token, m_value, m_expr_precedence, prec);
}
};
typedef ctrie<token_info> token_table;
@ -50,10 +59,12 @@ token_table add_command_token(token_table const & s, char const * token);
token_table add_command_token(token_table const & s, char const * token, char const * val);
token_table add_token(token_table const & s, char const * token, unsigned prec = LEAN_DEFAULT_PRECEDENCE);
token_table add_token(token_table const & s, char const * token, char const * val, unsigned prec = LEAN_DEFAULT_PRECEDENCE);
token_table add_tactic_token(token_table const & s, char const * token, unsigned prec = LEAN_DEFAULT_PRECEDENCE);
token_table add_tactic_token(token_table const & s, char const * token, char const * val, unsigned prec = LEAN_DEFAULT_PRECEDENCE);
void for_each(token_table const & s, std::function<void(char const *, token_info const&)> const & fn);
void display(std::ostream & out, token_table const & s);
token_table const * find(token_table const & s, char c);
optional<unsigned> get_precedence(token_table const & s, char const * token);
optional<unsigned> get_expr_precedence(token_table const & s, char const * token);
optional<unsigned> get_tactic_precedence(token_table const & s, char const * token);
bool is_token(token_table const & s, char const * token);
token_info const * value_of(token_table const & s);
void open_token_table(lua_State * L);

14
src/tests/frontends/lean/scanner.cpp
View file

@ -99,13 +99,13 @@ static void check_keyword(char const * str, name const & expected, environment c
static void tst1() {
environment env;
token_table s = get_token_table(env);
env = add_token(env, "+", 0);
env = add_token(env, "=", 0);
env = add_expr_token(env, "+", 0);
env = add_expr_token(env, "=", 0);
scan_success("a..a");
check("a..a", {tk::Identifier, tk::Keyword, tk::Keyword, tk::Identifier});
check("Type.{0}", {tk::Keyword, tk::Keyword, tk::Numeral, tk::Keyword});
env = add_token(env, "ab+cde", 0);
env = add_token(env, "+cd", 0);
env = add_expr_token(env, "ab+cde", 0);
env = add_expr_token(env, "+cd", 0);
scan_success("ab+cd", env);
check("ab+cd", {tk::Identifier, tk::Keyword}, env);
scan_success("ab+cde", env);
@ -139,9 +139,9 @@ static void tst2() {
scan_error("***");
environment env;
token_table s = mk_default_token_table();
env = add_token(env, "***", 0);
env = add_expr_token(env, "***", 0);
check_keyword("***", "***", env);
env = add_token(env, "+", 0);
env = add_expr_token(env, "+", 0);
check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
check("-- testing", {});
check("/- testing -/", {});
@ -152,7 +152,7 @@ static void tst2() {
check("int -> int", {tk::Identifier, tk::Keyword, tk::Identifier});
check("int->int", {tk::Identifier, tk::Keyword, tk::Identifier});
check_keyword("->", "->");
env = add_token(env, "-+->", 0);
env = add_expr_token(env, "-+->", 0);
check("Int -+-> Int", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
check("x := 10", {tk::Identifier, tk::Keyword, tk::Numeral});
check("{x}", {tk::Keyword, tk::Identifier, tk::Keyword});

2
tests/lean/run/tactic20.lean
View file

@ -1,8 +1,6 @@
import logic
open tactic
infixl `;`:15 := tactic.and_then
definition assump := eassumption
theorem tst {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c

22
tests/lean/run/tactic31.lean Normal file
View file

@ -0,0 +1,22 @@
import data.nat
example (a b c : Prop) : a → b → c → a ∧ b ∧ c :=
begin
intro Ha, intro Hb, intro Hc,
apply and.intro Ha,
apply and.intro Hb Hc
end
example (a b c : Prop) : a → b → c → a ∧ b ∧ c :=
by intro Ha; intro Hb; intro Hc; apply and.intro Ha; apply and.intro Hb Hc
open nat
example (a b c : nat) : a = b → b = 0 + c → a = c + 0:=
begin
intro ab, intro bc,
change a = c,
rewrite zero_add at bc,
rewrite -bc,
exact ab
end