From 6eb852e28f2f224795d9a98fed8c84de0ebb4ca2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Jan 2023 16:01:27 -0800 Subject: [PATCH] fix: fixes #1998 --- src/Lean/Compiler/IR/EmitC.lean | 25 ++++++++++++------- tests/compiler/initUnboxed.lean | 12 +++++++++ tests/compiler/initUnboxed.lean.expected.out | 5 ++++ .../compiler/initUnboxed.lean.no_interpreter | 0 4 files changed, 33 insertions(+), 9 deletions(-) create mode 100644 tests/compiler/initUnboxed.lean create mode 100644 tests/compiler/initUnboxed.lean.expected.out create mode 100644 tests/compiler/initUnboxed.lean.no_interpreter diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index db46c338bd..f67621498b 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -452,14 +452,17 @@ def emitBoxFn (xType : IRType) : M Unit := def emitBox (z : VarId) (x : VarId) (xType : IRType) : M Unit := do emitLhs z; emitBoxFn xType; emit "("; emit x; emitLn ");" -def emitUnbox (z : VarId) (t : IRType) (x : VarId) : M Unit := do - emitLhs z; +def getUnboxOpName (t : IRType) : String := match t with - | IRType.usize => emit "lean_unbox_usize" - | IRType.uint32 => emit "lean_unbox_uint32" - | IRType.uint64 => emit "lean_unbox_uint64" - | IRType.float => emit "lean_unbox_float" - | _ => emit "lean_unbox"; + | IRType.usize => "lean_unbox_usize" + | IRType.uint32 => "lean_unbox_uint32" + | IRType.uint64 => "lean_unbox_uint64" + | IRType.float => "lean_unbox_float" + | _ => "lean_unbox" + +def emitUnbox (z : VarId) (t : IRType) (x : VarId) : M Unit := do + emitLhs z + emit (getUnboxOpName t) emit "("; emit x; emitLn ");" def emitIsShared (z : VarId) (x : VarId) : M Unit := do @@ -706,8 +709,12 @@ def emitDeclInit (d : Decl) : M Unit := do emit "if (builtin) {" emit "res = "; emitCName initFn; emitLn "(lean_io_mk_world());" emitLn "if (lean_io_result_is_error(res)) return res;" - emitCName n; emitLn " = lean_io_result_get_value(res);" - emitMarkPersistent d n + emitCName n + if d.resultType.isScalar then + emitLn (" = " ++ getUnboxOpName d.resultType ++ "(lean_io_result_get_value(res));") + else + emitLn " = lean_io_result_get_value(res);" + emitMarkPersistent d n emitLn "lean_dec_ref(res);" if getBuiltinInitFnNameFor? env d.name |>.isSome then emit "}" diff --git a/tests/compiler/initUnboxed.lean b/tests/compiler/initUnboxed.lean new file mode 100644 index 0000000000..bfa0334058 --- /dev/null +++ b/tests/compiler/initUnboxed.lean @@ -0,0 +1,12 @@ +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 diff --git a/tests/compiler/initUnboxed.lean.expected.out b/tests/compiler/initUnboxed.lean.expected.out new file mode 100644 index 0000000000..b83c46446f --- /dev/null +++ b/tests/compiler/initUnboxed.lean.expected.out @@ -0,0 +1,5 @@ +0 +false +1 +0.500000 +16 diff --git a/tests/compiler/initUnboxed.lean.no_interpreter b/tests/compiler/initUnboxed.lean.no_interpreter new file mode 100644 index 0000000000..e69de29bb2