From d5ba10a3163a9da41b713d5577f95aef0879ba26 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Wed, 20 Jan 2021 15:45:41 -0500
Subject: [PATCH] feat: IO API for retrieving monotonic time

---
 src/runtime/io.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 8f47fc1c06..be6d560fa0 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -380,6 +380,13 @@ extern "C" obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_arg s, obj_arg
     }
 }
 
+/* monoMsNow : IO Nat */
+extern "C" obj_res lean_io_mono_ms_now(obj_arg /* w */) {
+    auto now = std::chrono::steady_clock::now();
+    auto tm = std::chrono::duration_cast<std::chrono::milliseconds>(now.time_since_epoch());
+    return io_result_mk_ok(usize_to_nat(tm.count()));
+}
+
 /* timeit {α : Type} (msg : @& String) (fn : IO α) : IO α */
 extern "C" obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg w) {
     auto start = std::chrono::steady_clock::now();