From 2de3d4091080b94b53a79e262b39005e82a1afbf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Aug 2016 16:45:32 -0700
Subject: [PATCH] feat(frontends/lean/definition_cmds): invoke compiler

---
 src/frontends/lean/definition_cmds.cpp | 30 +++++++++++++++++++++++---
 tests/lean/run/def3.lean               | 13 +++++++++++
 2 files changed, 40 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/def3.lean

diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 89eb7db0d3..34446fd4fc 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -16,8 +16,10 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 #include "library/noncomputable.h"
 #include "library/module.h"
+#include "library/flycheck.h"
 #include "library/error_handling.h"
 #include "library/equations_compiler/equations.h"
+#include "library/compiler/vm_compiler.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/elaborator.h"
@@ -187,10 +189,14 @@ static expr_pair elaborate_definition_core(elaborator & elab, def_cmd_kind kind,
     }
 }
 
+static void display_pos(std::ostream & out, parser const & p, pos_info const & pos) {
+    display_pos(out, p.get_stream_name().c_str(), pos.first, pos.second);
+}
+
 static expr_pair elaborate_definition(parser & p, elaborator & elab, def_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) {
     if (p.profiling()) {
         std::ostringstream msg;
-        display_pos(msg, p.get_stream_name().c_str(), pos.first, pos.second);
+        display_pos(msg, p, pos);
         msg << " elaboration time for " << local_pp_name(fn);
         timeit timer(p.ios().get_diagnostic_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD);
         return elaborate_definition_core(elab, kind, fn, val);
@@ -230,7 +236,7 @@ static pair<environment, name> mk_real_name(environment const & env, name const
 static certified_declaration check(parser & p, environment const & env, name const & c_name, declaration const & d, pos_info const & pos) {
     if (p.profiling()) {
         std::ostringstream msg;
-        display_pos(msg, p.get_stream_name().c_str(), pos.first, pos.second);
+        display_pos(msg, p, pos);
         msg << " type checking time for " << c_name;
         timeit timer(p.ios().get_diagnostic_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD);
         return ::lean::check(env, d);
@@ -257,6 +263,23 @@ static void check_noncomputable(parser & p, environment const & env, name const
     }
 }
 
+static environment compile_decl(parser & p, environment const & env, def_cmd_kind kind, bool is_noncomputable,
+                                name const & c_name, name const & c_real_name, pos_info const & pos) {
+    if (is_noncomputable || kind == Theorem || is_vm_builtin_function(c_real_name))
+        return env;
+    try {
+        declaration d = env.get(c_real_name);
+        return vm_compile(env, d);
+    } catch (exception & ext) {
+        flycheck_warning wrn(p.ios());
+        auto & out = p.ios().get_regular_stream();
+        display_pos(out, p, pos);
+        out << "failed to generate bytecode for '" << c_name << "'" << std::endl;
+        out << ext.what() << std::endl;
+        return env;
+    }
+}
+
 static environment declare_definition(parser & p, def_cmd_kind kind, buffer<name> const & lp_names, name const & c_name,
                                       expr const & type, expr const & val, bool is_private, bool is_protected, bool is_noncomputable,
                                       decl_attributes attrs, pos_info const & pos) {
@@ -285,7 +308,8 @@ static environment declare_definition(parser & p, def_cmd_kind kind, buffer<name
         new_env = add_abbreviation(new_env, c_real_name, attrs.is_parsing_only(), persistent);
     }
 
-    return attrs.apply(new_env, p.ios(), c_real_name);
+    new_env = attrs.apply(new_env, p.ios(), c_real_name);
+    return compile_decl(p, new_env, kind, is_noncomputable, c_name, c_real_name, pos);
 }
 
 environment xdefinition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, bool is_protected, bool is_noncomputable,
diff --git a/tests/lean/run/def3.lean b/tests/lean/run/def3.lean
new file mode 100644
index 0000000000..a31a3d74e6
--- /dev/null
+++ b/tests/lean/run/def3.lean
@@ -0,0 +1,13 @@
+set_option new_elaborator true
+
+definition f (a b : nat) : nat :=
+nat.cases_on a
+  (a + b + a + a + b)
+  (λ a', a + a + b)
+
+definition g (a b : nat) :=
+f (f a b) a
+
+set_option trace.compiler true
+
+vm_eval g (g (f 2 3) 2) 3