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

feat(frontends/lean): add '@' explicit notation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 12:50:47 -07:00
parent 905209df1c
commit f2b41312fb
3 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/builtin_exprs.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/ */
#include "kernel/abstract.h" #include "kernel/abstract.h"
#include "library/placeholder.h" #include "library/placeholder.h"
#include "library/explicit.h"
#include "frontends/lean/builtin_exprs.h" #include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/token_table.h" #include "frontends/lean/token_table.h"
#include "frontends/lean/calc.h" #include "frontends/lean/calc.h"
@ -264,6 +265,11 @@ static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_inf
return p.parse_scoped_expr(0, nullptr, env); return p.parse_scoped_expr(0, nullptr, env);
} }
static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
expr e = p.parse_expr(get_max_prec());
return p.save_pos(mk_explicit(e), pos);
}
parse_table init_nud_table() { parse_table init_nud_table() {
action Expr(mk_expr_action()); action Expr(mk_expr_action());
action Skip(mk_skip_action()); action Skip(mk_skip_action());
@ -281,6 +287,7 @@ parse_table init_nud_table() {
r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0); r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0);
r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0); r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0); r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
return r; return r;
} }

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

@ -13,6 +13,7 @@ static unsigned g_arrow_prec = 25;
static unsigned g_max_prec = std::numeric_limits<unsigned>::max(); static unsigned g_max_prec = std::numeric_limits<unsigned>::max();
static unsigned g_plus_prec = 65; static unsigned g_plus_prec = 65;
static unsigned g_cup_prec = 60; static unsigned g_cup_prec = 60;
unsigned get_max_prec() { return g_max_prec; }
unsigned get_arrow_prec() { return g_arrow_prec; } unsigned get_arrow_prec() { return g_arrow_prec; }
token_table add_command_token(token_table const & s, char const * token) { token_table add_command_token(token_table const & s, char const * token) {
return insert(s, token, token_info(token)); return insert(s, token, token_info(token));
@ -58,7 +59,7 @@ token_table init_token_table() {
{"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
{"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0}, {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0},
{"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
{"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", 0},
{"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
char const * commands[] = {"theorem", "axiom", "variable", "definition", char const * commands[] = {"theorem", "axiom", "variable", "definition",

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

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "util/lua.h" #include "util/lua.h"
namespace lean { namespace lean {
unsigned get_max_prec();
unsigned get_arrow_prec(); unsigned get_arrow_prec();
class token_info { class token_info {
bool m_command; bool m_command;