Words of any bitwidth in the semantics

[myreen]

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 you get 7-bit words. Similarly word5000 would produce good code for 5000-bit words. Crucially, we could not allow polymorphism over the word lengths. Allowing polymorphism would destroy the performance of primitives.

This is a project that touches the source semantics and many of the intermediate languages in minor ways, but requires some non-trivial changes in the data_to_word phase of the compiler.

This is suitable as part of an Masters thesis project. Contact myreen on the CakeML slack in case you are interested.

[xrchz]

@formrre are you still working on this? If not, maybe remove your assignment?

[formrre]

I am working not on this. I believe this has essentially bit rotten to a point where any attempt to merge master failed. It can potentially be resurrected, but in a very different form