myreen
myreen
In CakeML strings are immutable vectors of characters. At present they are always represented at runtime as a pointer to an immutable byte array. For example, the string "hello" is...
Currently, we have two compiler configs. The original one: https://github.com/CakeML/cakeml/blob/8f782f6b8ebd26b0c84d781bc1922f3b66149d7b/compiler/backend/backendScript.sml#L24-L38 And the version adapted for `Eval`: https://github.com/CakeML/cakeml/blob/8f782f6b8ebd26b0c84d781bc1922f3b66149d7b/compiler/backend/backendScript.sml#L634-L648 The original is called `config` and the new version is called `inc_config`. The...
That CakeML translator is the oldest part of the CakeML project and has grown organically with the project. There are a number of features we would like added or improved:...
LabLang is an assembly style IL at the bottom of the CakeML compiler. It represents the program as a list of functions which in turn are lists of assembly instructions....
Several people have contacted us asking to have the CakeML semantics in provers other than HOL4. There is an [AFP entry](https://devel.isa-afp.org/entries/CakeML.html) with the CakeML semantics ported to Isabelle/HOL via Lem....
At present, CakeML’s source code has two word sizes: 8 and 64. This issue is about supporting any word size as if it is primitive type, ie by writing word7...
Currently, [mlstringTheory](https://github.com/CakeML/cakeml/blob/master/basis/pure/mlstringScript.sml#L13) defines a function `implode` as follows. val implode_def = Define` implode = strlit` which is exactly the same as the (only) constructor `strlit` for the `mlstring` type, which...
The CakeML compiler currently lacks a lambda lifting optimisation. Such an optimisation pass could be beneficial because it makes functions closed (not have free variables) which allows optimisations such as...
This issue records our intent to add thunks to the CakeML semantics so that [the PureCake compiler](https://github.com/CakeML/pure) can generate thunks that CakeML's GC can be optimised for. The plan is...
This issue is about adding [tail-recursion modulo cons (TMC)](https://dl.acm.org/doi/10.1145/3571233) as a new optimisation to the CakeML compiler. The idea is to automatically transform non-tail-recursive functions such as fun append []...