Zulip Chat Archive

Stream: lean4

Topic: UInt* structure codegen


Mac (Jul 04 2021 at 18:51):

Currently, wrapping a primitive type like UInt32 in a structure makes it boxed:

structure AddressSpace where
  index : UInt32

@[extern "foo"]
constant foo (addrSpace : AddressSpace) : IO PUnit
-- passes address space as an `lean_object*`

@[extern "bar"]
constant bar (addrSpace : UInt32) : IO PUnit
-- passes address space as an `uint32`

This poses a problem for examples like the above where, for type safety reasons, wrapping a primitive type in a singleton structure is desirable.

Would it be feasible for such wrappers to also be special-cased by the code generator?

Sebastian Ullrich (Jul 04 2021 at 19:44):

Oh... this is already the case, but, what I can only assume is an oversight, only in the case of parameterized structures

Mac (Jul 04 2021 at 21:08):

lol! Well then, should I submit an issue about it?

Sebastian Ullrich (Jul 05 2021 at 06:20):

https://github.com/leanprover/lean4/pull/556

Mac (Jul 05 2021 at 21:28):

I discovered another place where unbox-ness is not preserved. Though, this may be intended:

constant Address : Type := USize
-- Address is a `lean_object*` instead of a `usize`

Would it be feasible for such opaque definitions to also preserve unbox-ness?


Last updated: Dec 20 2023 at 11:08 UTC