lean4-htt/tests/compiler/initUnboxed.lean
Siddharth a0a0463451
fix: codegen initUnboxed correctly in LLVM backend (#2015)
Closes #2004.

In porting the bugfix from
6eb852e28f,
I noticed that the LLVM backend was incorrectly generating declaration
initializers (in `callIODeclInitFn`), by assuming the return type of the
initializer is the return type of the declaration. Rather, it must be be
`lean_object`, since the initializer returns an `IO a` value which must be unpacked.

TODO: stop using the `getOrCreateFunction` pattern pervasively.
  perform the `create` at the right location, and the `get`
  at the correct location.
2023-01-07 16:26:53 +01:00

12 lines
309 B
Text

initialize test : UInt64 ← pure 0
initialize testb : Bool ← pure false
initialize testu : USize ← pure 1
initialize testf : Float ← pure 0.5
initialize test32 : UInt32 ← pure 16
def main : IO Unit := do
IO.println test
IO.println testb
IO.println testu
IO.println testf
IO.println test32