feat(frontends/lean/builtin_cmds): add simple 'print' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-11 11:52:58 -07:00
parent 7fd502993b
commit 1972a09021
4 changed files with 27 additions and 1 deletions

View file

@ -4,11 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include "library/io_state_stream.h"
#include "frontends/lean/parser.h" #include "frontends/lean/parser.h"
namespace lean { namespace lean {
environment print_cmd(parser & p) {
if (p.curr() == scanner::token_kind::String) {
regular(p.env(), p.ios()) << p.get_str_val() << "\n";
p.next();
} else {
throw parser_error("invalid print command", p.pos());
}
return p.env();
}
cmd_table init_cmd_table() {
cmd_table r;
add_cmd(r, cmd_info("print", "print a string", print_cmd));
return r;
}
cmd_table get_builtin_cmds() { cmd_table get_builtin_cmds() {
return cmd_table(); static optional<cmd_table> r;
if (!r)
r = init_cmd_table();
return *r;
} }
} }

View file

@ -35,4 +35,6 @@ typedef cmd_info_tmpl<tactic_command_fn> tactic_cmd_info;
typedef rb_map<name, cmd_info, name_quick_cmp> cmd_table; typedef rb_map<name, cmd_info, name_quick_cmp> cmd_table;
typedef rb_map<name, tactic_cmd_info, name_quick_cmp> tactic_cmd_table; typedef rb_map<name, tactic_cmd_info, name_quick_cmp> tactic_cmd_table;
inline void add_cmd(cmd_table & t, cmd_info const & cmd) { t.insert(cmd.get_name(), cmd); }
} }

2
tests/lean/t2.lean Normal file
View file

@ -0,0 +1,2 @@
print "hello world"
print "testing"

View file

@ -0,0 +1,2 @@
hello world
testing