From bd23f5d63dbfb464f39b670ddfef7bf9f070a423 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 May 2016 16:15:44 -0700 Subject: [PATCH] feat(frontends/lean/builtin_cmd): improve vm_eval command --- src/frontends/lean/builtin_cmds.cpp | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 6ad2626010..fa309f5cb7 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -665,11 +665,22 @@ static environment compile_cmd(parser & p) { } static environment vm_eval_cmd(parser & p) { - name n = p.check_constant_next("invalid vm_eval command, constant expected"); - vm_state s(p.env()); + auto pos = p.pos(); + expr e; level_param_names ls; + std::tie(e, ls) = parse_local_expr(p); + if (has_local(e) || has_metavar(e)) + throw parser_error("invalid vm_eval command, argument must be a closed expression", pos); + type_checker tc(p.env()); + expr type = tc.infer(e); + environment new_env = p.env(); + name main("_main"); + auto cd = check(new_env, mk_definition(new_env, main, ls, type, e)); + new_env = new_env.add(cd); + new_env = vm_compile(p.env(), new_env.get(main)); + vm_state s(new_env); { timeit timer(p.ios().get_diagnostic_stream(), "vm_eval time"); - s.invoke_fn(n); + s.invoke_fn(main); } vm_obj r = s.get(0); display(p.ios().get_regular_stream(), r);