ddc-code 0.3.2.1 → 0.4.1.1

raw patch · 14 files changed

+219/−259 lines, 14 filesdep ~base

Dependency ranges changed: base

Files

• LICENSE +1/−15
• ddc-code.cabal +2/−2
• lite/base/Data/Container/List.dcl +6/−6
• lite/base/Data/Numeric/Bool.dcl +8/−11
• lite/base/Data/Numeric/Int.dcl +6/−6
• lite/base/Data/Numeric/Nat.dcl +8/−8
• lite/base/Math/Integer.dcl +5/−6
• salt/primitive/Vector.dcs +4/−4
• salt/primitive32/Int.dcs +16/−17
• salt/primitive64/Int.dcs +16/−17
• salt/runtime32/Object.dcs +65/−78
• salt/runtime64/Object.dcs +73/−82
• sea/primitive/Primitive.c +2/−0
• sea/primitive/Primitive.h +7/−7

@@ -1,7 +1,7 @@ -------------------------------------------------------------------------------- The Disciplined Disciple Compiler License (MIT style) -Copyrite (K) 2007-2013 The Disciplined Disciple Compiler Strike Force+Copyrite (K) 2007-2014 The Disciplined Disciple Compiler Strike Force All rights reversed.  Permission is hereby granted, free of charge, to any person obtaining a copy@@ -13,18 +13,4 @@  The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.----------------------------------------------------------------------------------Under Australian law copyright is free and automatic.-By contributing to DDC authors grant all rights they have regarding their-contributions to the other members of the Disciplined Disciple Compiler Strike-Force, past, present and future, as well as placing their contributions under-the above license.--Use "darcs show authors" to get a list of Strike Force members.- ---------------------------------------------------------------------------------Redistributions of libraries in ./external are governed by their own licenses:--  - TinyPTC   GNU Lesser General Public License-  

@@ -1,5 +1,5 @@ Name:           ddc-code-Version:        0.3.2.1+Version:        0.4.1.1 License:        MIT License-file:   LICENSE Author:         The Disciplined Disciple Compiler Strike Force@@ -33,7 +33,7 @@  Library   build-depends:-        base            == 4.6.*,+        base            >= 4.6  &&  < 4.8,         filepath        == 1.3.*    exposed-modules:

@@ -1,19 +1,19 @@ module List-imports +import foreign c value  addNat -  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Nat r1 -(Pure | Use r3)>         Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Nat r3   subNat -  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Nat r1 -(Pure | Use r3)>         Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Nat r3 - showInt   :: [r : Region]. Nat# -> Ptr# r String#- putStrLn  :: [r : Region]. Ptr# r String# -> Void#+ showInt   : [r : Region]. Nat# -> Ptr# r String#+ putStrLn  : [r : Region]. Ptr# r String# -> Void#  with letrec @@ -33,7 +33,7 @@         (n : Nat r1)            { Pure | Use r1 + Use r2 }         (x : a)                 { Read r1 + Read r2 + Alloc r2 | Use r1 + Use r2}         : List r2 a- = letregion r3 in+ = private r3 in    case n of         N# n2             -> case eq# [Nat#] n2 0# of

@@ -1,40 +1,37 @@ module Bool-exports+export foreign c value  boxBool-  ::    [r : Region].+  :     [r : Region].         Bool# -(Alloc r | Use r)>         Bool r   unboxBool-  ::    [r : Region].+  :     [r : Region].         Bool r -(Read r | Empty)>         Bool#   addBool-  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Bool r1 -(Pure | Use r3)>         Bool r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Bool r3   mulBool-  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Bool r1 -(Pure | Use r3)>         Bool r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Bool r3 - not    -  ::    [r1 r2 : Region].+ not :  [r1 r2 : Region].         Bool r1 -(Read r1 + Alloc r2 | Use r1 + Use r2)>         Bool r2 - and    -  ::    [r1 r2 r3 : Region].+ and :  [r1 r2 r3 : Region].         Bool r1 -(Pure | Use r1 + Use r2)>         Bool r2 -(Read r1 + Alloc r2 | Use r1 + Use r2)>         Bool r2 - or-  ::    [r1 r2 r3 : Region].+ or  :  [r1 r2 r3 : Region].         Bool r1 -(Pure | Use r1 + Use r2)>         Bool r2 -(Read r1 + Alloc r2 | Use r1 + Use r2)>         Bool r2

@@ -1,29 +1,29 @@ module Int -exports+export foreign c value  boxInt  -  ::    [r : Region].+  :     [r : Region].         Int# -(Alloc r | Use r)>         Int r   unboxInt -  ::    [r : Region].+  :     [r : Region].         Int r -(Read r | Empty)>         Int#   addInt -  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Int r1 -(Pure | Use r3)>         Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Int r3   subInt -  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Int r1 -(Pure | Use r3)>         Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Int r3   mulInt -  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Int r1 -(Pure | Use r3)>         Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Int r3

@@ -1,41 +1,41 @@ module Nat -exports+export foreign c value  boxNat-  ::    [r : Region].+  :     [r : Region].         Nat# -(Alloc r | Use r)>         Nat r   unboxNat -  ::    [r : Region].+  :     [r : Region].         Nat r -(Read r | Empty)>         Nat#   addNat -  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Nat r1 -(Pure | Use r3)>         Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Nat r3   subNat -  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Nat r1 -(Pure | Use r3)>         Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Nat r3   mulNat-  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Nat r1 -(Pure | Use r3)>         Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Nat r3   eqNat -  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Nat r1 -(Pure | Use r3)>         Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Bool r3   neqNat -  ::    [r1 r2 r3 : Region].+  :     [r1 r2 r3 : Region].         Nat r1 -(Pure | Use r3)>         Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>         Bool r3

@@ -1,16 +1,15 @@  module Integer -imports {-        subInt  :: [r1 r2 r3 : Region]+import foreign c value+        subInt  : [r1 r2 r3 : Region]                 . Int r1 -(Pure | Use r3)>                    Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> -                  Int r3;+                  Int r3 -        mulInt  :: [r1 r2 r3 : Region]+        mulInt  : [r1 r2 r3 : Region]                 . Int r1 -(Pure | Use r3)>                    Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> -                  Int r3;-}+                  Int r3 with letrec  fac    [r : Region] 

@@ -1,10 +1,10 @@  -- | Vectors are arrays of unboxed values. module Vector-imports {-        allocRaw     :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj;-        payloadOfRaw :: [r : Region]. Ptr# r Obj -> Addr#;-} +import value+        allocRaw     : [r : Region]. Tag# -> Nat# -> Ptr# r Obj+        payloadOfRaw : [r : Region]. Ptr# r Obj -> Addr#+ with letrec  

@@ -1,38 +1,37 @@  -- | Int primitives for 32-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+module  Int+export value +        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 +import value         allocRawSmall :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj  with letrec - boxInt [r : Region] (x : Int#) : Ptr# r Obj- = do   obj     = allocRawSmall [r] TAG0# 4#-        addr    = takePtr# [r] [Obj] obj-        write#  [Int#] addr 4# x+ = do   obj     = allocRawSmall TAG0# 4#+        addr    = takePtr# obj+        write# addr 4# x         obj   unboxInt [r : Region] (obj : Ptr# r Obj) : Int#- = do   addr    = takePtr# [r] [Obj] obj-        read#   [Int#] addr 4#+ = do   addr    = takePtr# obj+        read#  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))+ = boxInt (add# (unboxInt x) (unboxInt 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))+ = boxInt (sub# (unboxInt x) (unboxInt 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))+ = boxInt (mul# (unboxInt x) (unboxInt y))

@@ -1,39 +1,38 @@  -- | 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+module  Int+export value+        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+import value         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+ = do   obj     = allocRawSmall TAG0# 8#+        addr    = takePtr# obj+        write# addr 4# x         obj   unboxInt [r : Region] (obj : Ptr# r Obj) : Int#- = do   addr    = takePtr# [r] [Obj] obj-        read#   [Int#] addr 4#+ = do   addr    = takePtr# obj+        read#  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))+ = boxInt (add# (unboxInt x) (unboxInt 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))+ = boxInt (sub# (unboxInt x) (unboxInt 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))+ = boxInt (mul# (unboxInt x) (unboxInt y)) 

@@ -65,33 +65,33 @@ --   that can load them typically suffer a penalty, so it is good to align heap --   objects anyway. ---module Object -exports-        getTag            :: [r : Region]. Ptr# r Obj -> Tag#+module  Object +export value+        getTag            : [r : Region]. Ptr# r Obj -> Tag# -        allocBoxed        :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj-        getFieldOfBoxed   :: [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a-        setFieldOfBoxed   :: [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a -> Void#+        allocBoxed        : [r : Region]. Tag# -> Nat# -> Ptr# r Obj+        getFieldOfBoxed   : [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a+        setFieldOfBoxed   : [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a -> Void# -        allocMixed        :: [r : Region]. Tag# -> Nat# -> Nat# -> Ptr# r Obj-        fieldOfMixed      :: [r : Region]. Ptr# r Obj -> Nat# -> Ptr# r Obj-        payloadOfMixed    :: [r : Region]. Ptr# r Obj -> Ptr# r Word8#+        allocMixed        : [r : Region]. Tag# -> Nat# -> Nat# -> Ptr# r Obj+        fieldOfMixed      : [r : Region]. Ptr# r Obj -> Nat# -> Ptr# r Obj+        payloadOfMixed    : [r : Region]. Ptr# r Obj -> Ptr# r Word8# -        allocRaw          :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj-        payloadOfRaw      :: [r : Region]. Ptr# r Obj -> Ptr# r Word8#+        allocRaw          : [r : Region]. Tag# -> Nat# -> Ptr# r Obj+        payloadOfRaw      : [r : Region]. Ptr# r Obj -> Ptr# r Word8# -        allocRawSmall     :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj-        payloadOfRawSmall :: [r : Region]. Ptr# r Obj -> Ptr# r Word8#+        allocRawSmall     : [r : Region]. Tag# -> Nat# -> Ptr# r Obj+        payloadOfRawSmall : [r : Region]. Ptr# r Obj -> Ptr# r Word8#  with letrec  -- | Get the constructor tag of an object. getTag [r : Region] (obj : Ptr# r Obj) : Tag#  = do   -        ptr             = castPtr# [r] [Word32#] [Obj] obj-        header          = peek# [r] [Word32#] ptr 0#-        tag32           = shr#  [Word32#] header 8w32#-        promote# [Tag#] [Word32#] tag32+        ptr             = castPtr# obj+        header          = peek# ptr 0#+        tag32           = shr#  header 8w32#+        promote# tag32    -- Boxed ----------------------------------------------------------------------@@ -106,52 +106,45 @@ --   } DataBoxed; --     allocBoxed -        [r : Region]-        (tag : Tag#) (arity : Nat#) : Ptr# r Obj+        [r : Region] (tag : Tag#) (arity : Nat#) : Ptr# r Obj  = do            -- multiply arity by 4 bytes-per-pointer to get size of payload.-        bytesPayload    = shl# [Nat#] arity (size2# [Ptr# r Obj])+        bytesPayload    = shl# arity (size2# [Ptr# r Obj])         -        bytesObj        = add# [Nat#] 8# bytesPayload+        bytesObj        = add# 8# bytesPayload         case check# bytesObj of-         True#  -> allocBoxed_ok [r] tag arity bytesObj-         False# -> fail# [Ptr# r Obj]+         True#  -> allocBoxed_ok tag arity bytesObj+         False# -> fail#  allocBoxed_ok-        [r : Region]-        (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj+        [r : Region] (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj  = do            addr            = alloc# bytesObj -        tag32           = promote# [Word32#] [Tag#] tag+        tag32           = promote# tag         format          = 0b00100001w32#-        header          = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format+        header          = bor# (shl# tag32 8w32#) format         write# [Word32#] addr 0# header -        arity32         = promote# [Word32#] [Nat#] arity+        arity32         = promote# arity         write# [Word32#] addr 4# arity32 -        makePtr# [r] [Obj] addr+        makePtr# addr   ---- | Get one of the pointers from a boxed data object. getFieldOfBoxed -        [r1 : Region] [a : Data] -        (obj : Ptr# r1 Obj) (index : Nat#) -        : a- =      read# [a]  (takePtr# [r1] [Obj] obj)-                   (add# [Nat#] 8# (shl# [Nat#] index 2#))+        [r1 : Region] [a : Data] (obj : Ptr# r1 Obj) (index : Nat#) : a+ =      read# [a]  (takePtr# obj)+                   (add# 8# (shl# index 2#))   -- | Set one of the pointers from a boxed data object. setFieldOfBoxed          [r1 : Region] [a : Data]-        (obj : Ptr# r1 Obj) (index : Nat#) -        (val : a) -        : Void#- =      write# [a] (takePtr# [r1] [Obj] obj)-                   (add# [Nat#] 8# (shl# [Nat#] index 2#))-                   val+        (obj : Ptr# r1 Obj) (index : Nat#) (val : a) : Void#+ =      write# (takePtr# obj)+               (add# 8# (shl# index 2#)) val   -- Mixed ----------------------------------------------------------------------@@ -167,14 +160,13 @@ --   } DataMixed; -- allocMixed-        [r : Region]-        (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) : Ptr# r Obj+        [r : Region] (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) : Ptr# r Obj  = do   -        bytesPtrs       = shl# [Nat#] arity 2#-        bytesObj        = add# [Nat#] 16# (add# [Nat#] bytesPtrs bytesRaw)+        bytesPtrs       = shl# arity 2#+        bytesObj        = add# 16# (add# bytesPtrs bytesRaw)         case check# bytesObj of-         True#  -> allocMixed_ok [r] tag arity bytesRaw bytesObj-         False# -> fail# [Ptr# r Obj]+         True#  -> allocMixed_ok tag arity bytesRaw bytesObj+         False# -> fail#  allocMixed_ok          [r : Region]@@ -182,16 +174,16 @@  = do         addr            = alloc# bytesObj -        tag32           = promote# [Word32#] [Tag#] tag+        tag32           = promote# tag         format          = 0b01000001w32#-        header          = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format+        header          = bor# (shl# tag32 8w32#) format         write# [Word32#] addr 0# header         write# [Word32#] addr 4# 0w32# -        bytesObj32      = promote# [Word32#] [Nat#] bytesObj+        bytesObj32      = promote# bytesObj         write# [Word32#] addr 8# bytesObj32 -        arity32         = promote# [Word32#] [Nat#] arity+        arity32         = promote# arity         write# [Word32#] addr 12# arity32          makePtr# [r] [Obj] addr@@ -200,13 +192,13 @@ -- | Get one of the pointers from a mixed data object. fieldOfMixed [r : Region] (obj : Ptr# r Obj) (index : Nat#) : Ptr# r Obj  = do   -        offset          = add# [Nat#] 16# (shl# [Nat#] index 2#)-        plusPtr# [r] [Obj] obj offset+        offset  = add# 16# (shl# index 2#)+        plusPtr# obj offset         -- | Get the address of the raw data payload from a mixed object. payloadOfMixed [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8#- =      plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 16#+ =      plusPtr# (castPtr# obj) 16#   -- Raw ------------------------------------------------------------------------@@ -220,35 +212,32 @@ --           uint8_t   payload[];    // Raw data that does not contain heap pointers. --   } DataRaw; ---allocRaw-        [r : Region]-        (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj+allocRaw [r : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj  = do   -        bytesObj        = add# [Nat#] 8# bytesPayload+        bytesObj        = add# 8# bytesPayload         case check# bytesObj of          True#  -> allocRaw_ok [r] tag bytesPayload bytesObj-         False# -> fail# [Ptr# r Obj]+         False# -> fail#  allocRaw_ok -        [r : Region] -        (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj+         [r : Region] (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj  = do         addr            = alloc# bytesObj -        tag32           = promote# [Word32#] [Tag#] tag+        tag32           = promote# tag         format          = 0b00110001w32#-        header          = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format+        header          = bor# (shl# tag32 8w32#) format         write# [Word32#] addr 0# header -        bytesObj32      = promote# [Word32#] [Nat#] bytesObj+        bytesObj32      = promote# bytesObj         write# [Word32#] addr 4# bytesObj32 -        makePtr# [r] [Obj] addr+        makePtr# addr   -- | Get the payload data from a raw object. payloadOfRaw [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8#- =      plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 8#+ =      plusPtr# (castPtr# obj) 8#   -- RawSmall -------------------------------------------------------------------@@ -262,13 +251,12 @@ --   } DataRawSmall; -- allocRawSmall -        [r : Region] -        (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj+        [r : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj  = do   -        bytesObj        = add# [Nat#] 4# bytesPayload+        bytesObj        = add# 4# bytesPayload         case check# bytesObj of-         True#  -> allocRawSmall_ok [r] tag bytesPayload bytesObj-         False# -> fail# [Ptr# r Obj]+         True#  -> allocRawSmall_ok tag bytesPayload bytesObj+         False# -> fail#  allocRawSmall_ok         [r : Region] @@ -276,18 +264,17 @@  = do         addr            = alloc# bytesObj -        tag32           = promote#  [Word32#] [Tag#] tag-        bytesPayload32  = truncate# [Word32#] [Nat#] bytesPayload-        wordsPayload32  = shr# [Word32#] bytesPayload32 2w32#+        tag32           = promote#  tag+        bytesPayload32  = truncate# bytesPayload+        wordsPayload32  = shr# bytesPayload32 2w32#         format          = 0b0011w32#-        header          =  bor# [Word32#] (shl# [Word32#] tag32          8w32#) -                          (bor# [Word32#] (shl# [Word32#] wordsPayload32 4w32#) -                                                          format)+        header          =  bor# (shl# tag32          8w32#) +                          (bor# (shl# wordsPayload32 4w32#) format)         write# [Word32#] addr 0# header -        makePtr# [r] [Obj] addr+        makePtr# addr   -- | Get the payload data from a raw small object. payloadOfRawSmall [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8#- =      plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 4#+ =      plusPtr# (castPtr# obj) 4#

@@ -65,33 +65,33 @@ --   that can load them typically suffer a penalty, so it is good to align heap --   objects anyway. ---module Object -exports-        getTag            :: [r : Region]. Ptr# r Obj -> Tag#+module  Object +export value+        getTag            : [r : Region]. Ptr# r Obj -> Tag# -        allocBoxed        :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj-        getFieldOfBoxed   :: [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a-        setFieldOfBoxed   :: [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a -> Void#+        allocBoxed        : [r : Region]. Tag# -> Nat# -> Ptr# r Obj+        getFieldOfBoxed   : [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a+        setFieldOfBoxed   : [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a -> Void# -        allocMixed        :: [r : Region]. Tag# -> Nat# -> Nat# -> Ptr# r Obj-        fieldOfMixed      :: [r : Region]. Ptr# r Obj -> Nat# -> Ptr# r Obj-        payloadOfMixed    :: [r : Region]. Ptr# r Obj -> Ptr# r Word8#+        allocMixed        : [r : Region]. Tag# -> Nat# -> Nat# -> Ptr# r Obj+        fieldOfMixed      : [r : Region]. Ptr# r Obj -> Nat# -> Ptr# r Obj+        payloadOfMixed    : [r : Region]. Ptr# r Obj -> Ptr# r Word8# -        allocRaw          :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj-        payloadOfRaw      :: [r : Region]. Ptr# r Obj -> Ptr# r Word8#+        allocRaw          : [r : Region]. Tag# -> Nat# -> Ptr# r Obj+        payloadOfRaw      : [r : Region]. Ptr# r Obj -> Ptr# r Word8# -        allocRawSmall     :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj-        payloadOfRawSmall :: [r : Region]. Ptr# r Obj -> Ptr# r Word8#+        allocRawSmall     : [r : Region]. Tag# -> Nat# -> Ptr# r Obj+        payloadOfRawSmall : [r : Region]. Ptr# r Obj -> Ptr# r Word8#  with letrec  -- | Get the constructor tag of an object. getTag [r : Region] (obj : Ptr# r Obj) : Tag#  = do   -        ptr             = castPtr# [r] [Word32#] [Obj] obj-        header          = peek# [r] [Word32#] ptr 0#-        tag32           = shr#  [Word32#] header 8w32#-        promote# [Tag#] [Word32#] tag32+        ptr             = castPtr# obj+        header          = peek# ptr 0#+        tag32           = shr#  header 8w32#+        promote# tag32    -- Boxed ----------------------------------------------------------------------@@ -114,14 +114,13 @@         (tag : Tag#) (arity : Nat#) : Ptr# r Obj  = do            -- Multiple arity by 8 bytes-per-pointer to get size of payload.-        bytesPayload    = shl# [Nat#] arity (size2# [Addr#])-        bytesObj        = add# [Nat#] (size# [Word32#])-                         (add# [Nat#] (size# [Word32#])-                                       bytesPayload)+        bytesPayload    = shl# arity (size2# [Addr#])+        bytesObj        = add# (size# [Word32#])+                         (add# (size# [Word32#]) bytesPayload)          case check# bytesObj of-         True#  -> allocBoxed_ok [r] tag arity bytesObj-         False# -> fail# [Ptr# r Obj]+         True#  -> allocBoxed_ok tag arity bytesObj+         False# -> fail#  allocBoxed_ok         [r : Region]@@ -131,14 +130,14 @@          tag32           = promote# [Word32#] [Tag#] tag         format          = 0b00100001w32#-        header          = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format-        write# [Word32#] addr 0# header+        header          = bor# (shl# tag32 8w32#) format+        write# addr 0# header          -- Truncate arity to 32-bits.         arity32         = truncate# [Word32#] [Nat#] arity-        write# [Word32#] addr 4# arity32+        write# addr 4# arity32 -        makePtr# [r] [Obj] addr+        makePtr# addr   ---- | Get one of the pointers from a boxed data object.@@ -146,21 +145,17 @@         [r1 : Region] [a : Data]         (obj : Ptr# r1 Obj) (index : Nat#)          : a- =      read# [a]  (takePtr# [r1] [Obj] obj)-                   (add# [Nat#] 8#-                                (shl# [Nat#] index (size2# [Addr#])))+ =      read#  (takePtr# obj)+               (add# 8# (shl# index (size2# [Addr#])))   -- | Set one of the pointers from a boxed data object. setFieldOfBoxed          [r1 : Region] [a : Data] -        (obj : Ptr# r1 Obj) (index : Nat#)-        (val : a) -        : Void#- =      write# [a] (takePtr# [r1] [Obj] obj)-                   (add# [Nat#] 8# -                                (shl# [Nat#] index (size2# [Addr#])))-                   val+        (obj : Ptr# r1 Obj) (index : Nat#) (val : a) : Void#+ =      write# (takePtr# obj)+               (add# 8# (shl# index (size2# [Addr#])))+               val   -- Mixed ----------------------------------------------------------------------@@ -181,11 +176,11 @@         [r : Region]         (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) : Ptr# r Obj  = do   -        bytesPtrs       = shl# [Nat#] arity 3#-        bytesObj        = add# [Nat#] (size# [Word32#])-                         (add# [Nat#] (size# [Word32#])-                         (add# [Nat#] (size# [Word64#])-                         (add# [Nat#] bytesPtrs bytesRaw)))+        bytesPtrs       = shl# arity 3#+        bytesObj        = add# (size# [Word32#])+                         (add# (size# [Word32#])+                         (add# (size# [Word64#])+                         (add# bytesPtrs bytesRaw)))          case check# bytesObj of          True#  -> allocMixed_ok [r] tag arity bytesObj@@ -197,32 +192,32 @@  = do         addr            = alloc# bytesObj -        tag32           = promote# [Word32#] [Tag#] tag+        tag32           = promote# tag         format          = 0b01000001w32#-        header          = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format-        write# [Word32#] addr 0# header+        header          = bor# (shl# tag32 8w32#) format+        write# addr 0# header          arity32         = truncate# [Word32#] [Nat#] arity-        write# [Word32#] addr 4# arity32+        write# addr 4# arity32          bytesObj32      = promote#  [Word64#] [Nat#] bytesObj-        write# [Word64#] addr 8# bytesObj32+        write# addr 8# bytesObj32 -        makePtr# [r] [Obj] addr+        makePtr# addr   -- | Get one of the pointers from a mixed data object. fieldOfMixed [r : Region] (obj : Ptr# r Obj) (index : Nat#) : Ptr# r Obj  = do   -        offset          = add# [Nat#] 16# -                         (shl# [Nat#] index (size2# [Addr#]))+        offset          = add# 16# +                         (shl# index (size2# [Addr#])) -        plusPtr# [r] [Obj] obj offset+        plusPtr# obj offset         -- | Get the address of the raw data payload from a mixed object. payloadOfMixed [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8#- =      plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 16#+ =      plusPtr# (castPtr# obj) 16#   -- Raw ------------------------------------------------------------------------@@ -239,37 +234,34 @@ --   } DataRaw; -- allocRaw-        [r : Region] -        (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj+        [r : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj  = do   -        bytesObj        = add# [Nat#] (size# [Word32#])-                         (add# [Nat#] (size# [Word32#])-                                      bytesPayload)+        bytesObj        = add# (size# [Word32#])+                         (add# (size# [Word32#]) bytesPayload)          case check# bytesObj of-         True#  -> allocRaw_ok [r] tag bytesObj-         False# -> fail# [Ptr# r Obj]+         True#  -> allocRaw_ok tag bytesObj+         False# -> fail#  -allocRaw_ok-        [r : Region]-        (tag : Tag#) (bytesObj : Nat#) : Ptr# r Obj+allocRaw_ok +        [r : Region] (tag : Tag#) (bytesObj : Nat#) : Ptr# r Obj  = do         addr            = alloc# bytesObj -        tag32           = promote# [Word32#] [Tag#] tag+        tag32           = promote# tag         format          = 0b00110001w32#-        header          = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format-        write# [Word32#] addr 0# header+        header          = bor# (shl# tag32 8w32#) format+        write# addr 0# header          bytesObj32      = truncate# [Word32#] [Nat#] bytesObj-        write# [Word32#] addr 4# bytesObj32+        write# addr 4# bytesObj32 -        makePtr# [r] [Obj] addr+        makePtr# addr   -- | Get the payload data from a raw object. payloadOfRaw [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8#- =      plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 8#+ =      plusPtr# (castPtr# obj) 8#   -- RawSmall -------------------------------------------------------------------@@ -285,33 +277,32 @@ --   } DataRawSmall; -- allocRawSmall-        [r : Region]+        [r : Region]          (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj  = do   -        bytesObj        = add# [Nat#] 4# bytesPayload+        bytesObj        = add# 4# bytesPayload         case check# bytesObj of-         True#   -> allocRawSmall_ok [r] tag bytesPayload bytesObj-         False#  -> fail# [Ptr# r Obj]+         True#   -> allocRawSmall_ok tag bytesPayload bytesObj+         False#  -> fail#  allocRawSmall_ok-        [r : Region]+        [r : Region]          (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj  = do            addr            = alloc# bytesObj -        tag32           = promote#  [Word32#] [Tag#] tag-        bytesPayload32  = truncate# [Word32#] [Nat#] bytesPayload-        wordsPayload32  = shr# [Word32#] bytesPayload32 2w32#+        tag32           = promote#  tag+        bytesPayload32  = truncate# bytesPayload+        wordsPayload32  = shr#  bytesPayload32 2w32#         format          = 0b0011w32#-        header          =  bor# [Word32#] (shl# [Word32#] tag32          8w32#) -                          (bor# [Word32#] (shl# [Word32#] wordsPayload32 4w32#) -                                                          format)-        write# [Word32#] addr 0# header+        header          =  bor# (shl# tag32          8w32#) +                          (bor# (shl# wordsPayload32 4w32#) format)+        write# addr 0# header -        makePtr# [r] [Obj] addr+        makePtr# addr   -- | Get the payload data from a raw small object. payloadOfRawSmall [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8#- =      plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 4#+ =      plusPtr# (castPtr# obj) 4# 

@@ -6,6 +6,7 @@   // Show an integer.+// This leaks the space for the string, but nevermind until we get a GC. string_t* showInt (int i) {       string_t* str = malloc(32);         snprintf(str, 32, "%d", i);@@ -14,6 +15,7 @@   // Show a natural number.+// This leaks the space for the string, but nevermind until we get a GC. string_t* showNat (nat_t i) {       string_t* str = malloc(32);         snprintf(str, 32, "%u", (unsigned int)i);

@@ -17,16 +17,16 @@   // Store Primops ---------------------------------------------------------------extern addr_t _DDC_Runtime_heapTop;-extern addr_t _DDC_Runtime_heapMax;+extern addr_t _DDC__heapTop;+extern addr_t _DDC__heapMax;   // Create the initial store. static inline void    _CREATE (nat_t bytes) {-        _DDC_Runtime_heapTop    = malloc (bytes);-        _DDC_Runtime_heapMax    = _DDC_Runtime_heapTop + bytes;        +        _DDC__heapTop   = malloc (bytes);+        _DDC__heapMax   = _DDC__heapTop + bytes;         }  @@ -34,8 +34,8 @@ static inline  addr_t _ALLOC (nat_t bytes)  {       -        addr_t obj              = _DDC_Runtime_heapTop;-        _DDC_Runtime_heapTop    = _DDC_Runtime_heapTop + bytes;+        addr_t obj      = _DDC__heapTop;+        _DDC__heapTop   = _DDC__heapTop + bytes;         return obj; }        @@ -45,7 +45,7 @@ static inline bool_t  _CHECK (nat_t bytes) {-        return (_DDC_Runtime_heapTop + bytes < _DDC_Runtime_heapMax);+        return (_DDC__heapTop + bytes < _DDC__heapMax); }