Module docstring
{"# Debugging helper functions "}
dbgTrace
definition
{α : Type u} (s : String) (f : Unit → α) : α
Informal description
The function `dbgTrace` takes a string `s` and a function `f : Unit → α`, evaluates `f ()` and returns its result of type `α`, while also printing the string `s` for debugging purposes.
dbgTraceVal
definition
{α : Type u} [ToString α] (a : α) : α
Full source
def dbgTraceVal {α : Type u} [ToString α] (a : α) : α :=
dbgTrace (toString a) (fun _ => a)Informal description
The function takes a value `a` of type `α` (with a `ToString` instance for `α`), prints the string representation of `a` for debugging purposes, and returns `a` unchanged.
dbgTraceIfShared
definition
{α : Type u} (s : String) (a : α) : α
Full source
/-- Display the given message if `a` is shared, that is, RC(a) > 1 -/
@[never_extract, extern "lean_dbg_trace_if_shared"]
def dbgTraceIfShared {α : Type u} (s : String) (a : α) : α := aInformal description
Given a string `s` and a value `a` of type `α`, this function displays the message `s` if the reference count of `a` is greater than 1 (indicating that `a` is shared), and then returns `a` unchanged.
dbgStackTrace
definition
{α : Type u} (f : Unit → α) : α
Full source
/-- Print stack trace to stderr before evaluating given closure. Currently supported on Linux only. -/
@[never_extract, extern "lean_dbg_stack_trace"]
def dbgStackTrace {α : Type u} (f : Unit → α) : α := f ()Informal description
The function `dbgStackTrace` evaluates a given closure `f` after printing a stack trace to standard error. This is currently only supported on Linux systems.
dbgSleep
definition
{α : Type u} (ms : UInt32) (f : Unit → α) : α
Informal description
The function `dbgSleep` takes a time duration `ms` in milliseconds and a function `f` from the unit type to a type `α`, and returns the result of applying `f` to the unit value after delaying for `ms` milliseconds.
panicWithPos
definition
{α : Sort u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α
Informal description
Given a type `α` with a default value, a module name `modName`, line and column numbers `line` and `col`, and a message `msg`, this function generates a panic message and raises a panic (exception) with that message, returning a default value of type `α`.
panicWithPosWithDecl
definition
{α : Sort u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α
Informal description
Given a type `α` with a default value, a module name `modName`, a declaration name `declName`, line and column numbers `line` and `col`, and a message `msg`, this function generates a panic message (including the declaration name) and raises a panic (exception) with that message, returning a default value of type `α`.
ptrAddrUnsafe
opaque
{α : Type u} (a : @& α) : USize
Full source
/--
Returns the address at which an object is allocated.
This function is unsafe because it can distinguish between definitionally equal values.
-/
@[extern "lean_ptr_addr"]
unsafe opaque ptrAddrUnsafe {α : Type u} (a : @& α) : USizeInformal description
Given a value `a` of type `α`, the function `ptrAddrUnsafe` returns the memory address (as an unsigned size value) where `a` is allocated. This function is unsafe because it can distinguish between definitionally equal values that may be stored at different memory locations.
isExclusiveUnsafe
opaque
{α : Type u} (a : @& α) : Bool
Full source
/--
Returns `true` if `a` is an exclusive object.
An object is exclusive if it is single-threaded and its reference counter is 1. This function is
unsafe because it can distinguish between definitionally equal values.
-/
@[extern "lean_is_exclusive_obj"]
unsafe opaque isExclusiveUnsafe {α : Type u} (a : @& α) : BoolInformal description
Given a value `a` of type `α`, the function `isExclusiveUnsafe` returns a boolean indicating whether `a` is an exclusive object. An exclusive object is one that is single-threaded and has a reference count of 1. This function is unsafe because it can distinguish between definitionally equal values.
withPtrAddrUnsafe
definition
{α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β
Full source
@[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
k (ptrAddrUnsafe a)Informal description
Given a value `a` of type `α` and a function `k` that maps a memory address (as an unsigned size value) to a value of type `β`, the function `withPtrAddrUnsafe` applies `k` to the memory address of `a`. The additional hypothesis `h` ensures that the result is independent of the specific memory address, as it states that `k` must produce the same output for any two addresses.
ptrEq
definition
(a b : α) : Bool
Full source
/--
Compares two objects for pointer equality.
Two objects are pointer-equal if, at runtime, they are allocated at exactly the same address. This
function is unsafe because it can distinguish between definitionally equal values.
-/
@[inline] unsafe def ptrEq (a b : α) : Bool := ptrAddrUnsafe a == ptrAddrUnsafe bInformal description
The function `ptrEq` checks whether two objects `a` and `b` of type `α` are pointer-equal, meaning they are allocated at the same memory address at runtime. This is determined by comparing their memory addresses obtained via `ptrAddrUnsafe`. Note that this function is unsafe as it can distinguish between definitionally equal values that may be stored at different memory locations.
withPtrEqUnsafe
definition
{α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool
Full source
@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
if ptrEq a b then true else k ()Informal description
The function `withPtrEqUnsafe` takes two elements `a$ and $b$ of type $\alpha$, a continuation function $k$ that returns a boolean when given a unit value, and a proof $h$ that if $a = b$ then $k ()$ evaluates to $\texttt{true}$. The function first checks if $a$ and $b$ are pointer-equal using `ptrEq`, returning $\texttt{true}$ if they are, otherwise it evaluates $k ()$ and returns the resulting boolean.
withPtrEq
definition
{α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool
Informal description
The function `withPtrEq` takes two elements `a` and `b` of type `α`, a continuation function `k` that returns a boolean when given a unit value, and a proof `h` that if `a = b` then `k ()` evaluates to `true`. The function simply applies `k` to the unit value `()` and returns the resulting boolean.
withPtrEqDecEq
definition
{α : Type u} (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b)
Full source
/-- `withPtrEq` for `DecidableEq` -/
@[inline] def withPtrEqDecEq {α : Type u} (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b) :=
let b := withPtrEq a b (fun _ => toBoolUsing (k ())) (toBoolUsing_eq_true (k ()));
match h:b with
| true => isTrue (ofBoolUsing_eq_true h)
| false => isFalse (ofBoolUsing_eq_false h)Informal description
The function `withPtrEqDecEq` takes two elements `a` and `b` of type `α` and a continuation function `k` that returns a decidability proof for the equality `a = b` when given a unit value. It uses pointer equality to optimize the decision process: if `a` and `b` are pointer-equal, it returns a proof that they are equal (`isTrue`), otherwise it evaluates `k ()` to determine decidability.
withPtrAddr
definition
{α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β
Full source
@[implemented_by withPtrAddrUnsafe]
def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0Informal description
Given a value `a` of type `α`, a function `k` from `USize` to `β` that is constant (i.e., `k u₁ = k u₂` for any `u₁, u₂`), the function `withPtrAddr` evaluates `k` at `0` and returns the result.