diff --git a/library/init/util.lean b/library/init/util.lean index 321530d52f..3dd26fd267 100644 --- a/library/init/util.lean +++ b/library/init/util.lean @@ -23,3 +23,6 @@ f () @[extern c inline "#4"] unsafe def unsafeCast {α : Type u} {β : Type v} [Inhabited β] (a : α) : β := default _ + +@[effectful, extern c inline "lean_panic_fn(#3)"] +constant panic {α : Type u} [Inhabited α] (msg : String) : α := default _ diff --git a/src/runtime/lean.h b/src/runtime/lean.h index 0777f2e452..5129c64b27 100644 --- a/src/runtime/lean.h +++ b/src/runtime/lean.h @@ -246,6 +246,7 @@ __attribute__((noreturn)) void lean_panic(char const * msg); __attribute__((noreturn)) void lean_panic_out_of_memory(); __attribute__((noreturn)) void lean_panic_unreachable(); __attribute__((noreturn)) void lean_panic_rc_overflow(); +lean_object * lean_panic_fn(lean_object * msg); static inline size_t lean_align(size_t v, size_t a) { return (v / a)*a + a * (v % a != 0); diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index f09e70432d..d5a9bcf228 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -38,6 +38,10 @@ extern "C" void lean_panic_rc_overflow() { lean_panic("reference counter overflowed"); } +extern "C" object * lean_panic_fn(object * msg) { + lean_panic(lean_string_cstr(msg)); +} + extern "C" size_t lean_object_byte_size(lean_object * o) { if (lean_is_mt(o) || lean_is_st(o) || lean_is_persistent(o)) { /* Recall that multi-threaded, single-threaded and persistent objects are stored in the heap.