|
|
|---|
|
|
|
|---|
System utilities with some enhanced features.
Some built-in system utilities are not guard-verified; some are guard-verified but have weak guards, and also weak (or non-existent) return type theorems. Some system utilities in the Std/system library are similar in this respect (intentionally so, as they are meant to complement the built-in ones). Strengthening the guards and return type theorems of these utilities may require stronger world invariants, and thus quite a bit of work. Nonetheless, these utilities are adequate, in their current form, for code where proving properties of the code itself is not a focus (e.g. program-mode code).
For code where proving at least some type-like properties
(particularly verifying guards and return types) is instead desired,
the Std/system library provides ``enhanced'' versions
of some of the aforementioned system utilities (built-in or not).
These variants may have stronger guards,
and often have stronger return type theorems:
the latter are made possible via run-time checks
that are expected to never fail.
Because of the run-time checks,
these variants are slower than the corresponding utilities
with weaker guards and weaker (or no) return type theorems.
These enhanced variants are named
like the corresponding utilities,
but with a
Besides the run-time checks for the return type theorems, some of these enhanced variants include additional run-time checks on their arguments. Making those checks part of the guards would make these utilities harder to use in practice, because it would be difficult to discharge their stronger guard obligations given the customary guards for the surrounding code. For instance, the customary pseudo-termp guard does not ensure that function symbols in terms satisfy function-symbolp: so, if some enhanced utilities operating on named functions were to require the function symbol to satisfy function-symbolp, the pseudo-termp guard would have to be replaced with something stronger. Instead, these enhanced utilities operating on named functions can check that function-symbolp at run time, helping to detect programming errors.