diff --git a/src/Lean/Util/Profile.lean b/src/Lean/Util/Profile.lean index d92d18fe5f..7b2c3314dc 100644 --- a/src/Lean/Util/Profile.lean +++ b/src/Lean/Util/Profile.lean @@ -9,9 +9,19 @@ import Lean.Data.Position namespace Lean /-- Print and accumulate run time of `act` when Option `profiler` is set to `true`. -/ -@[extern 5 "lean_lean_profileit"] -constant profileit {α : Type} (category : @& String) (pos : @& Position) (act : IO α) : IO α := act -def profileitPure {α : Type} (category : String) (pos : Position) (fn : Unit → α) : IO α := -profileit category pos $ IO.lazyPure fn +@[extern "lean_profileit"] +def profileit {α : Type} (category : @& String) (pos : @& Position) (fn : Unit → α) : α := fn () + +unsafe def profileitIOUnsafe {ε α : Type} (category : String) (pos : Position) (act : EIO ε α) : EIO ε α := + match profileit category pos fun _ => unsafeEIO act with + | Except.ok a => pure a + | Except.error e => throw e + +@[implementedBy profileitIOUnsafe] +def profileitIO {ε α : Type} (category : String) (pos : Position) (act : EIO ε α) : EIO ε α := act + +-- impossible to infer `ε` +def profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) (EIO ε) m m] {α : Type} (category : @& String) (pos : @& Position) (act : m α) : m α := + monadMap (fun {β} => @profileitIO ε β category pos) act end Lean diff --git a/src/library/time_task.cpp b/src/library/time_task.cpp index 782f33561a..cf2e944352 100644 --- a/src/library/time_task.cpp +++ b/src/library/time_task.cpp @@ -64,13 +64,13 @@ time_task::~time_task() { } } -/* profileit {α : Type} (category : string) (pos : position) (act : io α) : io α */ -extern "C" obj_res lean_lean_profileit(obj_arg, b_obj_arg category, b_obj_arg pos, obj_arg fn, obj_arg w) { +/* profileit {α : Type} (category : String) (pos : Position) (fn : Unit → α) : α */ +extern "C" obj_res lean_profileit(b_obj_arg category, b_obj_arg pos, obj_arg fn) { time_task t(string_to_std(category), - message_builder(environment(), get_global_ios(), get_pos_info_provider()->get_file_name(), + message_builder(environment(), get_global_ios(), "foo", pos_info(nat(cnstr_get(pos, 0), true).get_small_value(), nat(cnstr_get(pos, 1), true).get_small_value()), message_severity::INFORMATION)); - return apply_1(fn, w); + return apply_1(fn, box(0)); } }