From dde4a46fe396af30c98e65ac9eacaad06ebb6a28 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Jun 2016 16:32:20 -0700
Subject: [PATCH] feat(library/vm): add 'trace'

---
 library/init/default.lean     | 4 ++--
 src/library/vm/vm_aux.cpp     | 9 ++++++++-
 tests/lean/run/trace_tst.lean | 3 +++
 3 files changed, 13 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/trace_tst.lean

diff --git a/library/init/default.lean b/library/init/default.lean
index 3bda9a79ba..cf3d0d07dd 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -8,7 +8,7 @@ import init.datatypes init.reserved_notation init.logic
 import init.relation init.nat 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 init.timeit
-import init.unsigned init.ordering
+import init.monad init.fin init.list init.char init.string init.to_string
+import init.timeit init.trace init.unsigned init.ordering
 import init.meta
 import init.wf init.wf_k
diff --git a/src/library/vm/vm_aux.cpp b/src/library/vm/vm_aux.cpp
index 6b8f0abeb2..270d3489f6 100644
--- a/src/library/vm/vm_aux.cpp
+++ b/src/library/vm/vm_aux.cpp
@@ -7,18 +7,25 @@ Author: Leonardo de Moura
 #include <string>
 #include <iostream>
 #include "util/timeit.h"
+#include "library/trace.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_string.h"
 
 namespace lean {
 vm_obj vm_timeit(vm_obj const &, vm_obj const & s, vm_obj const & fn) {
     std::string msg = to_string(s);
-    timeit timer(std::cout, msg.c_str());
+    timeit timer(tout().get_stream(), msg.c_str());
+    return invoke(fn, mk_vm_unit());
+}
+
+vm_obj vm_trace(vm_obj const &, vm_obj const & s, vm_obj const & fn) {
+    tout() << to_string(s) << "\n";
     return invoke(fn, mk_vm_unit());
 }
 
 void initialize_vm_aux() {
     DECLARE_VM_BUILTIN("timeit", vm_timeit);
+    DECLARE_VM_BUILTIN("trace",  vm_trace);
 }
 
 void finalize_vm_aux() {
diff --git a/tests/lean/run/trace_tst.lean b/tests/lean/run/trace_tst.lean
new file mode 100644
index 0000000000..3e4fa17ec6
--- /dev/null
+++ b/tests/lean/run/trace_tst.lean
@@ -0,0 +1,3 @@
+open nat
+
+vm_eval trace "step1" (λ u, trace "hello" (λ u, succ 3))