Peek and poke

[mshinwell]

These are unsafe, but the idea is for them to be used via a specific library, if I understand correctly.

type ('a : any) t = nativeint#

external read : ('a : any). 'a t -> 'a = "%peek"
  [@@layout_poly]

external write : ('a : any). 'a t -> 'a -> unit = "%poke"
  [@@layout_poly]

cc @ccasin for an initial look (some frontend fixes required in here).

[lpw25]

We should have a mod external bound on the type of write to make it generally save, but IIUC Mark got an error when trying to add it. @goldfirere is that supposed to work yet?

[goldfirere]

Well, it's spelled mod external_, but yes it should work.

[mshinwell]

@TheNumbat maybe you could review this? (I've asked @ccasin if he can fix up the frontend parts.)

[stedolan]

mod external_ alone doesn't make this safe - there's no typechecking here since 'a t = 'b t. I'd prefer to type these as:

external read : ('a : any mod external_). nativeint# -> 'a = "%peek"
  [@@layout_poly]

external write : ('a : any mod external_). nativeint# -> 'a -> unit = "%poke"
  [@@layout_poly]

so at least we're not pretending there's some checking of 'a here.

[lpw25]

I agree that the current signature is not useful. I'd probably slightly prefer to just remove the equality of 'a t to nativeint# though.