myreen
commented
7 years ago At aa308d1 (1) and (2) are complete. I think (3) shouldn't be done because it's better if the compiler automatically turn any w2n (n2w ..) into w2w internally, in case the user provided w2n (n2w ..) input. The final bullet-point (4) should be an issue of its own.
From a discussion with Magnus.
The encoders would potentially be more efficient if we had better primitive support for w2w operations (between word8, word64). This is a list of things that could be done:
1) Currently, all instances of w2w get manually translated, see e.g. https://github.com/CakeML/cakeml/blob/master/compiler/bootstrap/translation/x64/x64ProgScript.sml#L249 One could generalize https://github.com/CakeML/cakeml/blob/master/translator/ml_translatorScript.sml#L1000 so that all of the w2ws are automatically translated. For word8 -> word64 (and vice versa), this could be done (for now) using n2w (w2n w) i.e. w2w_def
2) Add new primitives to the compiler backend that do efficient WordFromWord operations (e.g.. This would detect instances of n2w(w2n w) and convert them back into w2w operations
3) (Optionally) propagate this up to the source level, so we can immediately use the w2w operations.
4) Add more word sizes to the source. In particular, word63s and below can be unboxed. This would likely help with the encoders because everything above word8 gets translated as boxed word64s.