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

refactor(frontends/lean/notation_cmd): add register_notation_cmds procedure

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-17 13:39:44 -07:00
parent f6dc6e6504
commit 037cfcf622
3 changed files with 18 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -511,13 +511,8 @@ cmd_table init_cmd_table() {
add_cmd(r, cmd_info("abbreviation", "add new abbreviation (aka transparent definition)", abbreviation_cmd));
add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd));
add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd));
add_cmd(r, cmd_info("precedence", "set token left binding power", precedence_cmd));
add_cmd(r, cmd_info("infixl", "declare a new infix (left) notation", infixl_cmd));
add_cmd(r, cmd_info("infix", "declare a new infix (left) notation", infixl_cmd));
add_cmd(r, cmd_info("infixr", "declare a new infix (right) notation", infixr_cmd));
add_cmd(r, cmd_info("postfix", "declare a new postfix notation", postfix_cmd));
add_cmd(r, cmd_info("notation", "declare a new notation", notation_cmd));
add_cmd(r, cmd_info("#setline", "modify the current line number, it only affects error/report messages", set_line_cmd));
register_notation_cmds(r);
register_calc_cmds(r);
return r;
}

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

@ -297,4 +297,18 @@ notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & n
throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'postfix' or 'notation' expected", p.pos());
}
}
environment notation_cmd(parser & p) { return notation_cmd_core(p, true); }
environment infixl_cmd(parser & p) { return infixl_cmd_core(p, true); }
environment infixr_cmd(parser & p) { return infixr_cmd_core(p, true); }
environment postfix_cmd(parser & p) { return postfix_cmd_core(p, true); }
void register_notation_cmds(cmd_table & r) {
add_cmd(r, cmd_info("precedence", "set token left binding power", precedence_cmd));
add_cmd(r, cmd_info("infixl", "declare a new infix (left) notation", infixl_cmd));
add_cmd(r, cmd_info("infix", "declare a new infix (left) notation", infixl_cmd));
add_cmd(r, cmd_info("infixr", "declare a new infix (right) notation", infixr_cmd));
add_cmd(r, cmd_info("postfix", "declare a new postfix notation", postfix_cmd));
add_cmd(r, cmd_info("notation", "declare a new notation", notation_cmd));
}
}

7
src/frontends/lean/notation_cmd.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include "kernel/environment.h"
#include "frontends/lean/parser_config.h"
#include "frontends/lean/cmd_table.h"
namespace lean {
class parser;
@ -15,13 +16,11 @@ environment notation_cmd_core(parser & p, bool overload);
environment infixl_cmd_core(parser & p, bool overload);
environment infixr_cmd_core(parser & p, bool overload);
environment postfix_cmd_core(parser & p, bool overload);
inline environment notation_cmd(parser & p) { return notation_cmd_core(p, true); }
inline environment infixl_cmd(parser & p) { return infixl_cmd_core(p, true); }
inline environment infixr_cmd(parser & p) { return infixr_cmd_core(p, true); }
inline environment postfix_cmd(parser & p) { return postfix_cmd_core(p, true); }
/** \brief Return true iff the current token is a notation declaration */
bool curr_is_notation_decl(parser & p);
/** \brief Parse a notation declaration, throws an error if the current token is not a "notation declaration". */
notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & new_tokens);
void register_notation_cmds(cmd_table & r);
}