Convenient syntax to destructure newtypes

[Timmmm]

Now that we're using newtype physaddr = physaddr : xlenbits (and virtaddr) in the Sail model, it's a bit awkward not being able to easily access the xlenbits. Currently the solution is a function physaddr_bits() and virtaddr_bits() but it's a bit verbose.

Rust has addr.0 which makes sense because in Rust newtypes are single-entry tuples, but as I understand it in Sail they are single-entry enums, so it doesn't make as much sense to use .0. .something seems reasonable though. Some ideas:

• addr.inner
• addr.val

Or maybe it would be better to change newtype to use a 1-tuple and add .0, .1 syntax?

[Alasdair]

I think the Rust .0, .1, ..., .N syntax is maybe a bit cryptic for people not familiar with it, although I do find it convenient when writing Rust. Something like .inner would probably be fine. OCaml lets you do:

type physaddr = Physaddr of { inner : t }

where a x : physaddr can be unwrapped as x.inner

I don't know if we could make them single element tuples, as single element tuples aren't really a thing in Sail - I suspect internally tuple length is >= 2 is probably assumed in quite a few places as an invariant. The current implementation (single element enum) is a direct copy of Haskell's newtype for a single element.

[bacam]

I think the Rust .0, .1, ..., .N syntax is maybe a bit cryptic for people not familiar with it

That might be one of those bits of Rust inspired by Standard ML, and it's a pretty obscure feature there.

I don't know if we could make them single element tuples, as single element tuples aren't really a thing in Sail - I suspect internally tuple length is >= 2 is probably assumed in quite a few places as an invariant.

It would be a pain because it would need special syntax, although I seem to remember them occurring occasionally in intermediate Sail (maybe in the translation of mappings).