myreen
myreen
The CakeML source language has arbitrary precision integers as the main integer type. These are implemented dynamically as either smallnums or bignums. A smallnum is used in case the value...
The current version of the CakeML compiler has a bignum library that is generic for all targets and is implemented as part of `data_to_word`. Version 1 of the compiler had...
Currently, entry into a `Handle` is more expensive than it strictly needs to be. See dev mail from 28 September 2016.
I can't seem to find any documentation about command-line arguments for `hol`. `Holmake`'s command-line arguments are well documented, both in the _Description_ and also `Holmake --help`. Are there command-line arguments...
I recently made a PR (https://github.com/CakeML/cakeml/pull/1270) that added `Test` to source `op` datatype. This issue is about doing more of these kinds of rearranging and additions to source `op`. My...
The lack of variable-length shifts has been a blocker for a number of optimisations and improvements. This issue is about adding variable-length shifts to [asm](https://github.com/CakeML/cakeml/blob/master/compiler/encoders/asm/asmScript.sml) and supporting them in all...
CakeML has vectors (immutable) and arrays (mutable). Both have O(1) access and update. This issue is about implementing [persistent arrays](https://en.wikipedia.org/wiki/Persistent_array) in CakeML. If used carefully, persistent arrays have similar performance...
Currently, `Vector.tabluate` is a straightforward translation of the following function from `mlvectorScript.sml`: val tabulate_def = Define` tabulate n f = Vector (GENLIST f n)`; For large `n`, this is a...
We should try to use the translator's brittle "treat `string` as if it is `mlstring`" feature much less. This issue is about replacing all occurrences of `string` in [semantics/astScript.sml](https://github.com/CakeML/cakeml/blob/master/semantics/astScript.sml) with...