feat(library/vm,library/init): add builtin timeit primitive for profiling

library/init/default.lean

@@ -8,4 +8,4 @@ import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
-import init.monad init.fin init.list init.char init.string init.to_string
+import init.monad init.fin init.list init.char init.string init.to_string init.timeit

library/init/timeit.lean

@@ -0,0 +1,9 @@
+-- Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+prelude
+import init.string
+
+/- This function has a native implementation that tracks time. -/
+definition timeit {A : Type} (s : string) (f : unit → A) : A :=
+f unit.star

src/library/compiler/inliner.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/trace.h"
 #include "library/normalize.h"
+#include "library/vm/vm.h"
 #include "library/compiler/util.h"
 #include "library/compiler/compiler_step_visitor.h"
 
@@ -146,6 +147,8 @@ class inline_simple_definitions_fn : public compiler_step_visitor {
         if (!is_constant(fn))
             return default_visit_app(e);
         name const & n  = const_name(fn);
+        if (is_vm_builtin_function(n))
+            return default_visit_app(e);
         if (is_cases_on_recursor(env(), n) || is_nonrecursive_recursor(n))
             return visit_cases_on_app(e);
         unsigned nargs  = get_app_num_args(e);

src/library/constants.cpp

@@ -299,6 +299,7 @@ name const * g_tactic_trace = nullptr;
 name const * g_tactic_try_for = nullptr;
 name const * g_tactic_using_expr = nullptr;
 name const * g_tactic_whnf = nullptr;
+name const * g_timeit = nullptr;
 name const * g_to_string = nullptr;
 name const * g_trans_rel_left = nullptr;
 name const * g_trans_rel_right = nullptr;
@@ -611,6 +612,7 @@ void initialize_constants() {
     g_tactic_try_for = new name{"tactic", "try_for"};
     g_tactic_using_expr = new name{"tactic", "using_expr"};
     g_tactic_whnf = new name{"tactic", "whnf"};
+    g_timeit = new name{"timeit"};
     g_to_string = new name{"to_string"};
     g_trans_rel_left = new name{"trans_rel_left"};
     g_trans_rel_right = new name{"trans_rel_right"};
@@ -924,6 +926,7 @@ void finalize_constants() {
     delete g_tactic_try_for;
     delete g_tactic_using_expr;
     delete g_tactic_whnf;
+    delete g_timeit;
     delete g_to_string;
     delete g_trans_rel_left;
     delete g_trans_rel_right;
@@ -1236,6 +1239,7 @@ name const & get_tactic_trace_name() { return *g_tactic_trace; }
 name const & get_tactic_try_for_name() { return *g_tactic_try_for; }
 name const & get_tactic_using_expr_name() { return *g_tactic_using_expr; }
 name const & get_tactic_whnf_name() { return *g_tactic_whnf; }
+name const & get_timeit_name() { return *g_timeit; }
 name const & get_to_string_name() { return *g_to_string; }
 name const & get_trans_rel_left_name() { return *g_trans_rel_left; }
 name const & get_trans_rel_right_name() { return *g_trans_rel_right; }

src/library/constants.h

@@ -301,6 +301,7 @@ name const & get_tactic_trace_name();
 name const & get_tactic_try_for_name();
 name const & get_tactic_using_expr_name();
 name const & get_tactic_whnf_name();
+name const & get_timeit_name();
 name const & get_to_string_name();
 name const & get_trans_rel_left_name();
 name const & get_trans_rel_right_name();

src/library/constants.txt

@@ -294,6 +294,7 @@ tactic.trace
 tactic.try_for
 tactic.using_expr
 tactic.whnf
+timeit
 to_string
 trans_rel_left
 trans_rel_right

src/library/vm/CMakeLists.txt

@@ -1 +1 @@
-add_library(vm OBJECT vm.cpp vm_nat.cpp vm_string.cpp vm_io.cpp optimize.cpp init_module.cpp)
+add_library(vm OBJECT vm.cpp vm_nat.cpp vm_string.cpp vm_io.cpp vm_aux.cpp optimize.cpp init_module.cpp)

src/library/vm/init_module.cpp

@@ -7,17 +7,20 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_io.h"
+#include "library/vm/vm_aux.h"
 
 namespace lean {
 void initialize_vm_core_module() {
     initialize_vm_core();
     initialize_vm_nat();
     initialize_vm_io();
+    initialize_vm_aux();
 }
 void finalize_vm_core_module() {
+    finalize_vm_aux();
+    finalize_vm_io();
     finalize_vm_nat();
     finalize_vm_core();
-    finalize_vm_io();
 }
 
 void initialize_vm_module() {

src/library/vm/vm_aux.cpp

@@ -0,0 +1,30 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <iostream>
+#include "util/timeit.h"
+#include "library/constants.h"
+#include "library/vm/vm.h"
+#include "library/vm/vm_string.h"
+
+namespace lean {
+static void vm_timeit(vm_state & s) {
+    vm_obj const & msg  = s.get(-2);
+    vm_obj const & fn   = s.get(-3);
+    std::string msg_str = to_string(msg);
+    timeit timer(std::cout, msg_str.c_str());
+    s.push(mk_vm_unit());
+    s.push(fn);
+    s.apply();
+}
+
+void initialize_vm_aux() {
+    declare_vm_builtin(get_timeit_name(), 3, vm_timeit);
+}
+
+void finalize_vm_aux() {
+}
+}

src/library/vm/vm_aux.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+void initialize_vm_aux();
+void finalize_vm_aux();
+}