AST-33: Word{8, 16, 32} <--> {Nat, Int} conversions

[ggreif]

A blueprint for the conversion semantics (Word32 in particular) is written down in https://dfinity.atlassian.net/browse/AST-63. The interpreter is now ready (with the exception of Word64 which is a bit tricky as it may be lossy when converting to Int/Nat in the absence of proper bignums).

I would have preferred to handle the conversions Word* -> {Nat,Int} without the shifts in prelude.ml, as it breaks abstraction, but could not find a suitable method that would do the shifting based on the representation (SubRep) for me. I'd welcome a tip how to funnel the shift amount through the module machinery (if this is possible at all; I honestly doubt it). What I was trying to do is to somehow bake it into MakeWord's to_bits method, but I have failed so far.

Compilation of many Word* arithmetics and bitwise primitives is lacking (test/run/words.as tracks this), I'd tackle this and the trivial refactoring in other PRs.

Below is the laundry list:

• Nat -> Word32 only works up to 2**31-1 in the interpreter (compiler should be fine).
• Nat -> Word32 does not check for proper bignums (in the compiler CG).
• Executing the wasm binary causes an unreachable trap (missing (==) @Word32 codegen).
• Word32 has underlying OCaml Int32, which is signed (thus reading is signed too).
• Write story that iteration protocol should internally use BoxedSmallWord instead of BoxedInt.
• A bunch of refactoring (Wasm.Value, unboxed_zero, unboxed_one, etc.).
• Compilation of Word* arithmetics and bitwise primitives.
• Word64.
• Use awk to obtain a Haskell version of test/run/words.as, and run it, comparing outputs.

Any hints welcome.

[nomeata]

I would prefer the interpreter, as it is our spec, to get things right from the start. The compiler may lag behind.

Maybe the interpreter should just use Value.Int everywhere, and then implement the correct bounds check/wraps in the corresponding operations? This way, we clearly document the desired semantics in the interpreter, without implicitly using whatever semantics int32 has on Ocaml.

[ggreif]

@nomeata For the reference interpreter I'd even prefer nativeint, as it provides all the bit-fiddling ops, that I'll need for Word*.
The implementation needs to assert that nativeint is capable of holding a Word64.

I agree, that the implementation should strive for being the most clean possible. The semantics of the Word{8,16,32,64} types belong into Jira/Confluence. I'll begin with that soon. But should we give @matthewhammer a preview with what we have now (modulo tweaks)?

[nomeata]

nice, printInt can print Nat too

Yes, that works simply by subtyping: Every x:Nat is also an x:Int.

[nomeata]

Looking good!

[ggreif]

Naming is still a bit inconsistent, the small things should be i32, probably.

[nomeata]

Are you reviewing your own code? :-)

[nomeata]

(all comments reasonable, btw)

[nomeata]

Sorry, I missed that this PR changed from Draft to ready. Looks good!

[nomeata]

You write BoxedWord, but the module is still called BoxedInt.

[ggreif]

I'll address this in the follow-up.

[nomeata]

That was actually intentional, to make it clear it’s the “0ths” field after the header. But maybe it’s too confusing.

[ggreif]

Nobody looks at the expansion anyway...