9 Checked Bodies
The bodies of functions with refinements can use many but not all features of Shplait. A body is a sequence of (zero or more) local defs followed by one result expression, and it may contain:
integer, Boolean, symbol, and character literals, and identifiers;
calls to this module’s functions and constructors;
calls to functions defined inside the function, and to functions passed to it as arguments; the checker knows only the type of the result, not its value;
the builtins max, min, add1, sub1, is_even, is_odd, the list, string, and array measures, and cons, which the checker models exactly;
options, pairs, and characters (Options, Pairs, and Characters);
make_array, Array, string_append, substring, append, reverse, map, filter, and rest, whose results’ lengths the checker knows (for filter, only that the length is at most the input’s);
any other Shplait builtin, and array indexing and assignment; the checker knows only the type of the result, not its value;
error, unreachable, and assert (error, unreachable, and assert).
For instance, there is no abs; write max(n, -n). A local def may not shadow a parameter or an earlier local.
A builtin such as first(l) may be called, but nothing is known about its value. Builtins check their own arguments only when the program runs: string_get(s, i) with an i out of range is a run-time error, not a compile-time one. To have such a precondition checked, write a function that states it, like safe_get above, and call that.