max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: IO API for retrieving monotonic time

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-01-20 15:45:41 -05:00 • committed by Sebastian Ullrich
parent 8addea6e74
commit d5ba10a316
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/runtime/io.cpp
View file

@ -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();