-- | Int primitives for 64-bit machines. module Int exports boxInt :: [r : Region]. Int# -> Ptr# r Obj unboxInt :: [r : Region]. Ptr# r Obj -> Int# addInt :: [r1 r2 r3 : Region]. Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj subInt :: [r1 r2 r3 : Region]. Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj mulInt :: [r1 r2 r3 : Region]. Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj imports allocRawSmall :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj with letrec boxInt [r : Region] (x : Int#) : Ptr# r Obj = do obj = allocRawSmall [r] TAG0# 8# addr = takePtr# [r] [Obj] obj write# [Int#] addr 4# x obj unboxInt [r : Region] (obj : Ptr# r Obj) : Int# = do addr = takePtr# [r] [Obj] obj read# [Int#] addr 4# addInt [r1 r2 r3 : Region] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj = boxInt [r3] (add# [Int#] (unboxInt [r1] x) (unboxInt [r2] y)) subInt [r1 r2 r3 : Region] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj = boxInt [r3] (sub# [Int#] (unboxInt [r1] x) (unboxInt [r2] y)) mulInt [r1 r2 r3 : Region] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj = boxInt [r3] (mul# [Int#] (unboxInt [r1] x) (unboxInt [r2] y))