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

feat(frontends/lean): add 'coercion' command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-26 08:08:39 -07:00
parent 06f9e7bfdd
commit 52ff29a6f7
3 changed files with 22 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h"
#include "library/aliases.h"
#include "library/locals.h"
#include "library/coercion.h"
#include "frontends/lean/util.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/calc.h"
@ -33,6 +34,7 @@ static name g_declarations("declarations");
static name g_decls("decls");
static name g_hiding("hiding");
static name g_renaming("renaming");
static name g_colon(":");
environment print_cmd(parser & p) {
if (p.curr() == scanner::token_kind::String) {
@ -206,6 +208,23 @@ environment using_cmd(parser & p) {
return env;
}
environment coercion_cmd(parser & p) {
auto pos = p.pos();
expr f = p.parse_expr();
if (!is_constant(f))
throw parser_error("invalid 'coercion' command, constant expected", pos);
if (p.curr_is_token(g_colon)) {
p.next();
pos = p.pos();
expr C = p.parse_expr();
if (!is_constant(C))
throw parser_error("invalid 'coercion' command, constant expected", pos);
return add_coercion(p.env(), const_name(f), const_name(C), p.ios());
} else {
return add_coercion(p.env(), const_name(f), p.ios());
}
}
cmd_table init_cmd_table() {
cmd_table r;
add_cmd(r, cmd_info("using", "create aliases for declarations, and use objects defined in other namespaces", using_cmd));
@ -216,6 +235,7 @@ cmd_table init_cmd_table() {
add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd));
add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd));
add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd));
add_cmd(r, cmd_info("coercion", "add a new coercion", coercion_cmd));
add_cmd(r, cmd_info("#setline", "modify the current line number, it only affects error/report messages", set_line_cmd));
register_decl_cmds(r);
register_inductive_cmd(r);

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

@ -62,7 +62,7 @@ token_table init_token_table() {
{"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", 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", "coercion",
"variables", "[private]", "[inline]", "[fact]", "abbreviation",
"evaluate", "check", "print", "end", "namespace", "section", "import",
"abbreviation", "inductive", "record", "structure", "module", "universe",

2
src/library/coercion.h
View file

@ -36,7 +36,7 @@ namespace lean {
\remark \c ios is used to report warning messages.
*/
environment add_coercion(environment const & env, name & f, io_state const & ios);
environment add_coercion(environment const & env, name const & f, io_state const & ios);
environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios);
bool is_coercion(environment const & env, name const & f);
bool is_coercion(environment const & env, expr const & f);