Print memory representation for a structure type?

Stream: lean4

[Geoffrey Irving]

Is there an analogue of trace.compiler.ir.result for the memory representation of a structure? E.g., if I do

@[unbox] structure Floating where
  n : UInt64
  s : UInt64

is there a way to print out what actually happened, to see that the type is 16 bytes?

[Sebastian Ullrich]

No but https://lean-lang.org/lean4/doc/dev/ffi.html has a mostly complete description

[Sebastian Ullrich]

[unbox] is not implemented yet

[Geoffrey Irving]

Oh no!

[Geoffrey Irving]

Is there a tracking issue? https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+unbox doesn’t show anything.

[Sebastian Ullrich]

I don't think so, it will be part of the compiler rewrite

[Geoffrey Irving]

Does unboxing work for a single field structure?

[Geoffrey Irving]

https://github.com/girving/ray/blob/182ad3693a29ac55d0df12175d28b9a2b8d6b671/Ray/Approx/Int64.lean#L15

[Geoffrey Irving]

/-- 64-bit two's complement integers -/
@[unbox] structure Int64 where
  n : UInt64
  deriving DecidableEq, BEq

[Henrik Böving]

It will unbox on its own without the attribute