max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/builtin_cmds): generate better error message when vm_eval result is a function

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-31 19:12:02 -07:00
parent 8bccfc23da
commit a2c1372d45
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -667,9 +667,11 @@ static environment compile_cmd(parser & p) {
static void vm_eval_core(bool is_IO, vm_state & s, name const & main) {
if (is_IO) s.push(mk_vm_simple(0)); // push the "RealWorld" state
vm_decl d = *s.get_decl(main);
if (!is_IO && d.get_arity() > 0)
throw exception("vm_eval result is a function");
s.invoke_fn(main);
if (is_IO) {
vm_decl d = *s.get_decl(main);
if (d.get_arity() == 0) {
/* main returned a closure, it did not process RealWorld yet.
So, we force the execution. */