In 64-bit machines, the max small nat value should now be (2^63 - 1), and on 32-bit
machines (2^32 - 1).
The main motivation for this modification are the array indexing
operations. With the new representation, if a Nat index is not small,
then it must not be a valid index. This was not true in 64-bit
machines. Example: an array of size 2^33 would fit in memory, and but
an index `i` > 2^32 - 1 would not be a small nat value.
`whnf_core(e)` uses `whnf` to reduce the major premise of recursors and
projections, and `whnf` unfolds arbitrary definitions.
This commit adds a new option (`cheap`) to `whnf_core`. When
`whnf_core(e, true)` is used, the type checker will not unfolding
definitions when reducing the major premises.
`uint32` is a definition, and `type_checker::whnf` unfolds it.
To preserve the information at `erase_irrelevant`, we use a custom
`whnf_type` method that stops reduction as soon as a builtin runtime
type is found.
`proj_sname` is not just for enabling better pretty printing. It is
necessary in the compiler when type information is lost, and we can't
infer the type of a `proj`-term argument (field `proj_expr`).
Before this commit, given a term `let x : t := v in b`, `infer_type`
would return `let x : t := v in T` where `T` is the type of `b` in
the local context extended with declaration `x : t := v`.
This is correct, but it produces unnecessarily large terms
in the new compiler stack which makes a heavy use of let-expressions.
We noticed the problem when the size of some .olean files were 100x
bigger. For example, `repr.olean` increased from 136Kb to
13Mb after we started saving the `._cstage1` (code after after
simplification) in the `.olean` files.
The new implementation relies on the fact that `T` seldom depends on
`x`. So, in most cases, the result is just `T` instead of `let x : t := v in T`
After this change, the new .olean files are at most 56% bigger than
.olean files not containing `._cstate1` code. This seems reasonable
since most of our .olean files only contain code and we are storing a
copy of each function.
@kha The new lcnf format keeps exposing problems :)
