(vl-print-nat x) is an optimized version of vl-print for
We make a few optimizations.
- We identify numeric literals (like 5) at compile time and turn them into
strings, so they can be printed at runtime without any coercion.
- Numbers don't have to be encoded, so there's no need to consider whether
we're in HTML mode.
- We essentially use str::revappend-nat-to-dec-chars instead of calling natstr or
similar. This does the minimum amount of consing and doesn't build a
- We manually inline the executable definition of str::revappend-nat-to-dec-chars to
avoid doing the loop.
- Optimized base-10 natural number printing into ps.