ddc-code 0.3.1.1 → 0.3.2.1
raw patch · 12 files changed
+188/−188 lines, 12 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- LICENSE +1/−1
- ddc-code.cabal +1/−2
- lite/base/Data/Container/List.dcl +17/−17
- lite/base/Data/Numeric/Bool.dcl +25/−24
- lite/base/Data/Numeric/Int.dcl +18/−18
- lite/base/Data/Numeric/Nat.dcl +26/−26
- lite/base/Math/Integer.dcl +6/−6
- salt/primitive/Vector.dcs +10/−10
- salt/primitive32/Int.dcs +11/−11
- salt/primitive64/Int.dcs +11/−11
- salt/runtime32/Object.dcs +31/−31
- salt/runtime64/Object.dcs +31/−31
LICENSE view
@@ -1,7 +1,7 @@ -------------------------------------------------------------------------------- The Disciplined Disciple Compiler License (MIT style) -Copyrite (K) 2007-2012 The Disciplined Disciple Compiler Strike Force+Copyrite (K) 2007-2013 The Disciplined Disciple Compiler Strike Force All rights reversed. Permission is hereby granted, free of charge, to any person obtaining a copy
ddc-code.cabal view
@@ -1,5 +1,5 @@ Name: ddc-code-Version: 0.3.1.1+Version: 0.3.2.1 License: MIT License-file: LICENSE Author: The Disciplined Disciple Compiler Strike Force@@ -9,7 +9,6 @@ Stability: experimental Category: Compilers/Interpreters Homepage: http://disciple.ouroborus.net-Bug-reports: disciple@ouroborus.net Synopsis: Disciplined Disciple Compiler base libraries. Description: Disciplined Disciple Compiler base libraries.
lite/base/Data/Container/List.dcl view
@@ -1,19 +1,19 @@ module List imports addNat - :: [r1 r2 r3 : %].- Nat r1 -(!0 | Use r3)>+ :: [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 : %].- Nat r1 -(!0 | Use r3)>+ :: [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 : %]. Nat# -> Ptr# r String#- putStrLn :: [r : %]. Ptr# r String# -> Void#+ showInt :: [r : Region]. Nat# -> Ptr# r String#+ putStrLn :: [r : Region]. Ptr# r String# -> Void# with letrec @@ -21,7 +21,7 @@ -- Constructors --------------------------------------------------------------- -- | Construct a list containing a single element. singleton - [r : %] [a : *]+ [r : Region] [a : Data] (x : a) { Alloc r | Use r } : List r a = Cons [r] [a] x (Nil [r] [a] ())@@ -29,8 +29,8 @@ -- | Construct a list containing copies of some value. replicate- [r1 r2 : %] [a : *]- (n : Nat r1) { !0 | Use r1 + Use r2 }+ [r1 r2 : Region] [a : Data]+ (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@@ -45,8 +45,8 @@ -- | Construct a range of Nat values enumFromTo- [r1 r2 : %]- (n : Nat r2) { !0 | Use r1 + Use r2 }+ [r1 r2 : Region]+ (n : Nat r2) { Pure | Use r1 + Use r2 } (max : Nat r2) { Read r2 + Alloc r1 + Alloc r2 | Use r1 + Use r2 } : List r1 (Nat r2) = case n of@@ -62,7 +62,7 @@ -- | O(n^2) reverse the elements in a list.-reverse [r1 r2 : %] [a : *]+reverse [r1 r2 : Region] [a : Data] (xx : List r1 a) { Read r1 + Read r2 + Alloc r2 | Use r1 + Use r2 } : List r2 a = case xx of@@ -74,8 +74,8 @@ -- | Append two lists.-append [r1 r2 : %] [a : *]- (xx : List r1 a) { !0 | Use r1 + Use r2 }+append [r1 r2 : Region] [a : Data]+ (xx : List r1 a) { Pure | Use r1 + Use r2 } (yy : List r2 a) { Read r1 + Alloc r2 | Use r1 + Use r2 + DeepUse a } : List r2 a = case xx of@@ -88,13 +88,13 @@ ------------------------------------------------------------------------------- -- | Take the length of a list.-length [r1 r2 : %] [a : *]+length [r1 r2 : Region] [a : Data] (xx : List r1 a) { Read r1 + Read r2 + Alloc r2 | Use r1 + Use r2 } : Nat r2 = length2 [:r1 r2 a:] (N# [r2] 0#) xx -length2 [r1 r2 : %] [a : *]- (acc : Nat r2) { !0 | Use r1 + Use r2 }+length2 [r1 r2 : Region] [a : Data]+ (acc : Nat r2) { Pure | Use r1 + Use r2 } (xx : List r1 a) { Read r1 + Read r2 + Alloc r2 | Use r1 + Use r2} : Nat r2
lite/base/Data/Numeric/Bool.dcl view
@@ -1,41 +1,41 @@ module Bool exports boxBool- :: [r : %].+ :: [r : Region]. Bool# -(Alloc r | Use r)> Bool r unboxBool- :: [r : %].- Bool r -(Read r | $0)>+ :: [r : Region].+ Bool r -(Read r | Empty)> Bool# addBool- :: [r1 r2 r3 : %].- Bool r1 -(!0 | Use r3)>+ :: [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 : %].- Bool r1 -(!0 | Use r3)>+ :: [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 : %].+ :: [r1 r2 : Region]. Bool r1 -(Read r1 + Alloc r2 | Use r1 + Use r2)> Bool r2 and - :: [r1 r2 r3 : %].- Bool r1 -(!0 | Use r1 + Use r2)>+ :: [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 : %].- Bool r1 -(!0 | Use r1 + Use r2)>+ :: [r1 r2 r3 : Region].+ Bool r1 -(Pure | Use r1 + Use r2)> Bool r2 -(Read r1 + Alloc r2 | Use r1 + Use r2)> Bool r2 @@ -43,23 +43,24 @@ -- | Box a boolean.-boxBool [r : %] +boxBool [r : Region] (i : Bool#) { Alloc r | Use r } : Bool r = B# [r] i -- | Unbox a boolean.-unboxBool [r : %]- (x : Bool r) { Read r | $0 } +unboxBool + [r : Region]+ (x : Bool r) { Read r | Empty } : Bool# = case x of B# i -> i -- | Add two booleans.-addBool [r1 r2 r3 : %] - (x : Bool r1) { !0 | Use r3 } +addBool [r1 r2 r3 : Region] + (x : Bool r1) { Pure | Use r3 } (y : Bool r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 } : Bool r3 = case x of { B# i1 @@ -68,8 +69,8 @@ -- | Multiply two naturals.-mulBool [r1 r2 r3 : %] - (x : Bool r1) { !0 | Use r3 } +mulBool [r1 r2 r3 : Region] + (x : Bool r1) { Pure | Use r3 } (y : Bool r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 } : Bool r3 = case x of { B# i1 @@ -78,7 +79,7 @@ -- | Boolean negation.-not [r1 r2 : %]+not [r1 r2 : Region] (x : Bool r1) {Read r1 + Alloc r2 | Use r1 + Use r2} : Bool r2 = case unboxBool [r1] x of@@ -87,8 +88,8 @@ -- | Right biased short-circuiting and.-and [r1 r2 r3 : %]- (x : Bool r1) {!0 | Use r1 + Use r2 }+and [r1 r2 r3 : Region]+ (x : Bool r1) { Pure | Use r1 + Use r2 } (y : Bool r2) { Read r1 + Alloc r2 | Use r1 + Use r2 } : Bool r2 = case unboxBool [r1] x of @@ -97,8 +98,8 @@ -- | Right biased short-circuiting or.-or [r1 r2 r3 : %]- (x : Bool r1) {!0 | Use r1 + Use r2 }+or [r1 r2 r3 : Region]+ (x : Bool r1) { Pure | Use r1 + Use r2 } (y : Bool r2) { Read r1 + Alloc r2 | Use r1 + Use r2 } : Bool r2 = case unboxBool [r1] x of
lite/base/Data/Numeric/Int.dcl view
@@ -1,30 +1,30 @@ module Int exports boxInt - :: [r : %].+ :: [r : Region]. Int# -(Alloc r | Use r)> Int r unboxInt - :: [r : %].- Int r -(Read r | $0)>+ :: [r : Region].+ Int r -(Read r | Empty)> Int# addInt - :: [r1 r2 r3 : %].- Int r1 -(!0 | Use r3)>+ :: [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 : %].- Int r1 -(!0 | Use r3)>+ :: [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 : %].- Int r1 -(!0 | Use r3)>+ :: [r1 r2 r3 : Region].+ Int r1 -(Pure | Use r3)> Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> Int r3 @@ -32,23 +32,23 @@ -- | Box an integer.-boxInt [r : %] +boxInt [r : Region] (i : Int#) { Alloc r | Use r } : Int r = I# [r] i -- | Unbox an integer.-unboxInt [r : %]- (x : Int r) { Read r | $0 } +unboxInt [r : Region]+ (x : Int r) { Read r | Empty } : Int# = case x of I# i -> i -- | Add two integers.-addInt [r1 r2 r3 : %] - (x : Int r1) { !0 | Use r3 } +addInt [r1 r2 r3 : Region] + (x : Int r1) { Pure | Use r3 } (y : Int r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 } : Int r3 = case x of { I# i1 @@ -57,8 +57,8 @@ -- | Subtract the second integer from the first.-subInt [r1 r2 r3 : %] - (x : Int r1) { !0 | Use r3 } +subInt [r1 r2 r3 : Region] + (x : Int r1) { Pure | Use r3 } (y : Int r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 } : Int r3 = case x of { I# i1 @@ -67,8 +67,8 @@ -- | Multiply two integers.-mulInt [r1 r2 r3 : %] - (x : Int r1) { !0 | Use r3 } +mulInt [r1 r2 r3 : Region] + (x : Int r1) { Pure | Use r3 } (y : Int r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 } : Int r3 = case x of { I# i1
lite/base/Data/Numeric/Nat.dcl view
@@ -1,42 +1,42 @@ module Nat exports boxNat- :: [r : %].+ :: [r : Region]. Nat# -(Alloc r | Use r)> Nat r unboxNat - :: [r : %].- Nat r -(Read r | $0)>+ :: [r : Region].+ Nat r -(Read r | Empty)> Nat# addNat - :: [r1 r2 r3 : %].- Nat r1 -(!0 | Use r3)>+ :: [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 : %].- Nat r1 -(!0 | Use r3)>+ :: [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 : %].- Nat r1 -(!0 | Use r3)>+ :: [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 : %].- Nat r1 -(!0 | Use r3)>+ :: [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 : %].- Nat r1 -(!0 | Use r3)>+ :: [r1 r2 r3 : Region].+ Nat r1 -(Pure | Use r3)> Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> Bool r3 @@ -44,54 +44,54 @@ -- | Box an natural.-boxNat [r : %] +boxNat [r : Region] (i : Nat#) { Alloc r | Use r } : Nat r = N# [r] i -- | Unbox an natural.-unboxNat [r : %]- (x : Nat r) { Read r | $0 } +unboxNat [r : Region]+ (x : Nat r) { Read r | Empty } : Nat# = case x of { N# n -> n } -- | Add two naturals.-addNat [r1 r2 r3 : %] - (x : Nat r1) { !0 | Use r3 } +addNat [r1 r2 r3 : Region] + (x : Nat r1) { Pure | Use r3 } (y : Nat r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 } : Nat r3 = case x of { N# i1 -> case y of { N# i2 -> N# [r3] (add# [Nat#] i1 i2) } } -- | Subtract the second natural from the first.-subNat [r1 r2 r3 : %]- (x : Nat r1) { !0 | Use r3 } +subNat [r1 r2 r3 : Region]+ (x : Nat r1) { Pure | Use r3 } (y : Nat r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 } : Nat r3 = case x of { N# i1 -> case y of { N# i2 -> N# [r3] (sub# [Nat#] i1 i2) } } -- | Multiply two naturals.-mulNat [r1 r2 r3 : %] - (x : Nat r1) { !0 | Use r3 } +mulNat [r1 r2 r3 : Region] + (x : Nat r1) { Pure | Use r3 } (y : Nat r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 } : Nat r3 = case x of { N# i1 -> case y of { N# i2 -> N# [r3] (mul# [Nat#] i1 i2) } } -- | Equality on naturals.-eqNat [r1 r2 r3 : %]- (x : Nat r1) { !0 | Use r3 }+eqNat [r1 r2 r3 : Region]+ (x : Nat r1) { Pure | Use r3 } (y : Nat r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3} : Bool r3 = case x of { N# n1 -> case y of { N# n2 -> B# [r3] (eq# [Nat#] n1 n2) } } -- | Negated Equality on naturals.-neqNat [r1 r2 r3 : %]- (x : Nat r1) { !0 | Use r3 }+neqNat [r1 r2 r3 : Region]+ (x : Nat r1) { Pure | Use r3 } (y : Nat r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3} : Bool r3 = case x of { N# n1 -> case y of { N# n2 -> B# [r3] (neq# [Nat#] n1 n2) } }
lite/base/Math/Integer.dcl view
@@ -1,20 +1,20 @@ module Integer imports {- subInt :: [r1 r2 r3 : %]- . Int r1 -(!0 | Use r3)> + subInt :: [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 : %]- . Int r1 -(!0 | Use r3)> + mulInt :: [r1 r2 r3 : Region]+ . Int r1 -(Pure | Use r3)> Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> Int r3; } with letrec -fac [r : %] - (acc : Int r) {!0 | Use r}+fac [r : Region] + (acc : Int r) {Pure | Use r} (n : Int r) {Read r + Alloc r | Use r} : Int r = case n of { I# i ->
salt/primitive/Vector.dcs view
@@ -2,8 +2,8 @@ -- | Vectors are arrays of unboxed values. module Vector imports {- allocRaw :: [r : %]. Tag# -> Nat# -> Ptr# r Obj;- payloadOfRaw :: [r : %]. Ptr# r Obj -> Addr#;+ allocRaw :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj;+ payloadOfRaw :: [r : Region]. Ptr# r Obj -> Addr#; } with letrec @@ -16,7 +16,7 @@ -- uint8_t payload[] -- } Vector8 ---allocVector8 [r : %] (length : Nat#) : Ptr# r Obj+allocVector8 [r : Region] (length : Nat#) : Ptr# r Obj = do -- total size of object payload. bytes = add# [Nat#] (bytesNat# V#) length@@ -34,13 +34,13 @@ -- Projections ---------------------------------------------------------------- -- | Get the length of a vector.-lengthVector8 [r : %] (obj : Ptr# r Obj) : Nat#+lengthVector8 [r : Region] (obj : Ptr# r Obj) : Nat# = do payload = payloadOfRaw [r] obj read# [Nat#] payload 0# -- | Unsafely read a byte from a vector.-indexVector8 [r : %] (obj : Ptr# r Obj) (index : Nat#) : Word8#+indexVector8 [r : Region] (obj : Ptr# r Obj) (index : Nat#) : Word8# = do payload = payloadOfRaw [r] obj offset = add# [Nat#] (bytesNat# V#) index read# [Word8#] payload offset @@ -49,7 +49,7 @@ -- Update --------------------------------------------------------------------- -- | Unsafely write a byte into a vector. updateVector8 - [r : %]+ [r : Region] (obj : Ptr# r Obj) (index : Nat#) (val : Word8#) : Void#@@ -61,7 +61,7 @@ -- Fill ----------------------------------------------------------------------- -- | Fill a vector with the given value. fillVector8 - [r : %]+ [r : Region] (obj : Ptr# r Obj) (val : Word8#) : Void# = do payload = payloadOfRaw [r] obj@@ -74,7 +74,7 @@ -- | Fill a range of bytes with the given value. fillPtr8 - [r : %] + [r : Region] (cur : Ptr# r Word8#) (top : Ptr# r Word8#) (val : Word8#) : Void#@@ -92,7 +92,7 @@ -- Copy ----------------------------------------------------------------------- -- | Copy a vector into a fresh buffer. copyVector8 - [r1 r2 : %]+ [r1 r2 : Region] (vec1 : Ptr# r1 Obj) : Ptr# r2 Obj = do @@ -112,7 +112,7 @@ copyPtr8- [r1 r2 : %]+ [r1 r2 : Region] (offset : Nat#) (length : Nat#) (src : Ptr# r1 Word8#)
salt/primitive32/Int.dcs view
@@ -2,37 +2,37 @@ -- | Int primitives for 32-bit machines. module Int exports- boxInt :: [r : %]. Int# -> Ptr# r Obj- unboxInt :: [r : %]. Ptr# r Obj -> Int#- addInt :: [r1 r2 r3 : %]. Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj- subInt :: [r1 r2 r3 : %]. Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj- mulInt :: [r1 r2 r3 : %]. Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj+ 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 : %]. Tag# -> Nat# -> Ptr# r Obj+ allocRawSmall :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj with letrec -boxInt [r : %] (x : Int#) : Ptr# r Obj+boxInt [r : Region] (x : Int#) : Ptr# r Obj = do obj = allocRawSmall [r] TAG0# 4# addr = takePtr# [r] [Obj] obj write# [Int#] addr 4# x obj -unboxInt [r : %] (obj : Ptr# r Obj) : Int#+unboxInt [r : Region] (obj : Ptr# r Obj) : Int# = do addr = takePtr# [r] [Obj] obj read# [Int#] addr 4# -addInt [r1 r2 r3 : %] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj+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 : %] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj+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 : %] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj+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))
salt/primitive64/Int.dcs view
@@ -2,38 +2,38 @@ -- | Int primitives for 64-bit machines. module Int exports- boxInt :: [r : %]. Int# -> Ptr# r Obj- unboxInt :: [r : %]. Ptr# r Obj -> Int#- addInt :: [r1 r2 r3 : %]. Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj- subInt :: [r1 r2 r3 : %]. Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj- mulInt :: [r1 r2 r3 : %]. Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj+ 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 : %]. Tag# -> Nat# -> Ptr# r Obj+ allocRawSmall :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj with letrec -boxInt [r : %] (x : Int#) : Ptr# r Obj+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 : %] (obj : Ptr# r Obj) : Int#+unboxInt [r : Region] (obj : Ptr# r Obj) : Int# = do addr = takePtr# [r] [Obj] obj read# [Int#] addr 4# -addInt [r1 r2 r3 : %] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj+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 : %] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj+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 : %] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj+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))
salt/runtime32/Object.dcs view
@@ -28,7 +28,7 @@ -- 0 1 0 1 a 0 0 1 -- SuspIndir -- -- size -- a 0 1 1 -- DataRawSmall -- --- * GC Forwarding / Broken-Heart pointers.+-- Data GC Forwarding / Broken-Heart pointers. -- During garbage collection, after the GC copies an object to the -- "to-space" its header in the "from-space" is overwritten with a pointer -- to where the "to-space" version of the object is.@@ -39,12 +39,12 @@ -- For all other values of the format field, we ensure the lowest two bits -- are not 00. -- --- * Anchor flag+-- Data Anchor flag -- If bit 3 in the format field is set then the GC is not permitted to move -- the object. This is useful when the object has been allocated by malloc -- and exists outside the DDC runtime's garbage collected heap. -- --- * Data{Boxed, Mixed, Raw, RawSmall}+-- Data Data{Boxed, Mixed, Raw, RawSmall} -- There are four data object formats: -- DataBoxed: A boxed object containing pointers to more heap objects. -- DataMixed: Some heap pointers, and some raw data.@@ -67,26 +67,26 @@ -- module Object exports- getTag :: [r : %]. Ptr# r Obj -> Tag#+ getTag :: [r : Region]. Ptr# r Obj -> Tag# - allocBoxed :: [r : %]. Tag# -> Nat# -> Ptr# r Obj- getFieldOfBoxed :: [r : %]. [a : *]. Ptr# r Obj -> Nat# -> a- setFieldOfBoxed :: [r : %]. [a : *]. 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 : %]. Tag# -> Nat# -> Nat# -> Ptr# r Obj- fieldOfMixed :: [r : %]. Ptr# r Obj -> Nat# -> Ptr# r Obj- payloadOfMixed :: [r : %]. 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 : %]. Tag# -> Nat# -> Ptr# r Obj- payloadOfRaw :: [r : %]. 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 : %]. Tag# -> Nat# -> Ptr# r Obj- payloadOfRawSmall :: [r : %]. 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 : %] (obj : Ptr# r Obj) : Tag#+getTag [r : Region] (obj : Ptr# r Obj) : Tag# = do ptr = castPtr# [r] [Word32#] [Obj] obj header = peek# [r] [Word32#] ptr 0#@@ -102,11 +102,11 @@ -- { uint32_t tagFormat; // Constructor tag and format field. -- uint32_t arity; // Arity of the data constructor. -- // (The number of pointers in the payload)--- Obj* payload[]; +-- ObjData payload[]; -- } DataBoxed; -- allocBoxed - [r : %]+ [r : Region] (tag : Tag#) (arity : Nat#) : Ptr# r Obj = do -- multiply arity by 4 bytes-per-pointer to get size of payload.@@ -118,7 +118,7 @@ False# -> fail# [Ptr# r Obj] allocBoxed_ok- [r : %]+ [r : Region] (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj@@ -136,7 +136,7 @@ ---- | Get one of the pointers from a boxed data object. getFieldOfBoxed - [r1 : %] [a : *] + [r1 : Region] [a : Data] (obj : Ptr# r1 Obj) (index : Nat#) : a = read# [a] (takePtr# [r1] [Obj] obj)@@ -145,7 +145,7 @@ -- | Set one of the pointers from a boxed data object. setFieldOfBoxed - [r1 : %] [a : *]+ [r1 : Region] [a : Data] (obj : Ptr# r1 Obj) (index : Nat#) (val : a) : Void#@@ -163,11 +163,11 @@ -- uint32_t padding; // Padding to ensure payload is 8 byte aligned. -- uint32_t size; // Size of the whole object, in bytes. -- uint32_t ptrCount; // Number of pointers at the start of the payload.--- Obj* payload[]; // Contains ptrCount pointers, then raw data.+-- ObjData payload[]; // Contains ptrCount pointers, then raw data. -- } DataMixed; -- allocMixed- [r : %]+ [r : Region] (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) : Ptr# r Obj = do bytesPtrs = shl# [Nat#] arity 2#@@ -177,7 +177,7 @@ False# -> fail# [Ptr# r Obj] allocMixed_ok - [r : %]+ [r : Region] (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj@@ -198,14 +198,14 @@ -- | Get one of the pointers from a mixed data object.-fieldOfMixed [r : %] (obj : Ptr# r Obj) (index : Nat#) : Ptr# r Obj+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 -- | Get the address of the raw data payload from a mixed object.-payloadOfMixed [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+payloadOfMixed [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 16# @@ -221,7 +221,7 @@ -- } DataRaw; -- allocRaw- [r : %]+ [r : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj = do bytesObj = add# [Nat#] 8# bytesPayload@@ -230,7 +230,7 @@ False# -> fail# [Ptr# r Obj] allocRaw_ok - [r : %] + [r : Region] (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj@@ -247,7 +247,7 @@ -- | Get the payload data from a raw object.-payloadOfRaw [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+payloadOfRaw [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 8# @@ -262,7 +262,7 @@ -- } DataRawSmall; -- allocRawSmall - [r : %] + [r : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj = do bytesObj = add# [Nat#] 4# bytesPayload@@ -271,7 +271,7 @@ False# -> fail# [Ptr# r Obj] allocRawSmall_ok- [r : %] + [r : Region] (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj@@ -289,5 +289,5 @@ -- | Get the payload data from a raw small object.-payloadOfRawSmall [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+payloadOfRawSmall [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 4#
salt/runtime64/Object.dcs view
@@ -28,7 +28,7 @@ -- 0 1 0 1 a 0 0 1 -- SuspIndir -- -- size -- a 0 1 1 -- DataRawSmall -- --- * GC Forwarding / Broken-Heart pointers.+-- Data GC Forwarding / Broken-Heart pointers. -- During garbage collection, after the GC copies an object to the -- "to-space" its header in the "from-space" is overwritten with a pointer -- to where the "to-space" version of the object is.@@ -39,12 +39,12 @@ -- For all other values of the format field, we ensure the lowest two bits -- are not 00. -- --- * Anchor flag+-- Data Anchor flag -- If bit 3 in the format field is set then the GC is not permitted to move -- the object. This is useful when the object has been allocated by malloc -- and exists outside the DDC runtime's garbage collected heap. -- --- * Data{Boxed, Mixed, Raw, RawSmall}+-- Data Data{Boxed, Mixed, Raw, RawSmall} -- There are four data object formats: -- DataBoxed: A boxed object containing pointers to more heap objects. -- DataMixed: Some heap pointers, and some raw data.@@ -67,26 +67,26 @@ -- module Object exports- getTag :: [r : %]. Ptr# r Obj -> Tag#+ getTag :: [r : Region]. Ptr# r Obj -> Tag# - allocBoxed :: [r : %]. Tag# -> Nat# -> Ptr# r Obj- getFieldOfBoxed :: [r : %]. [a : *]. Ptr# r Obj -> Nat# -> a- setFieldOfBoxed :: [r : %]. [a : *]. 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 : %]. Tag# -> Nat# -> Nat# -> Ptr# r Obj- fieldOfMixed :: [r : %]. Ptr# r Obj -> Nat# -> Ptr# r Obj- payloadOfMixed :: [r : %]. 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 : %]. Tag# -> Nat# -> Ptr# r Obj- payloadOfRaw :: [r : %]. 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 : %]. Tag# -> Nat# -> Ptr# r Obj- payloadOfRawSmall :: [r : %]. 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 : %] (obj : Ptr# r Obj) : Tag#+getTag [r : Region] (obj : Ptr# r Obj) : Tag# = do ptr = castPtr# [r] [Word32#] [Obj] obj header = peek# [r] [Word32#] ptr 0#@@ -106,11 +106,11 @@ -- { uint32_t tagFormat; // Constructor tag and format field. -- uint32_t arity; // Arity of the data constructor. -- // (The number of pointers in the payload)--- Obj* payload[]; +-- ObjData payload[]; -- } DataBoxed; -- allocBoxed- [r : %]+ [r : Region] (tag : Tag#) (arity : Nat#) : Ptr# r Obj = do -- Multiple arity by 8 bytes-per-pointer to get size of payload.@@ -124,7 +124,7 @@ False# -> fail# [Ptr# r Obj] allocBoxed_ok- [r : %]+ [r : Region] (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj@@ -143,7 +143,7 @@ ---- | Get one of the pointers from a boxed data object. getFieldOfBoxed - [r1 : %] [a : *]+ [r1 : Region] [a : Data] (obj : Ptr# r1 Obj) (index : Nat#) : a = read# [a] (takePtr# [r1] [Obj] obj)@@ -153,7 +153,7 @@ -- | Set one of the pointers from a boxed data object. setFieldOfBoxed - [r1 : %] [a : *] + [r1 : Region] [a : Data] (obj : Ptr# r1 Obj) (index : Nat#) (val : a) : Void#@@ -174,11 +174,11 @@ -- { uint32_t tagFormat; -- uint32_t ptrCount; // Number of pointers at the start of the payload. -- uint64_t size; // Size of the whole object, in bytes.--- Obj* payload[]; // Contains ptrCount pointers, then raw data.+-- ObjData payload[]; // Contains ptrCount pointers, then raw data. -- } DataMixed; -- allocMixed - [r : %]+ [r : Region] (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) : Ptr# r Obj = do bytesPtrs = shl# [Nat#] arity 3#@@ -192,7 +192,7 @@ False# -> fail# [Ptr# r Obj] allocMixed_ok- [r : %]+ [r : Region] (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj@@ -212,7 +212,7 @@ -- | Get one of the pointers from a mixed data object.-fieldOfMixed [r : %] (obj : Ptr# r Obj) (index : Nat#) : Ptr# r Obj+fieldOfMixed [r : Region] (obj : Ptr# r Obj) (index : Nat#) : Ptr# r Obj = do offset = add# [Nat#] 16# (shl# [Nat#] index (size2# [Addr#]))@@ -221,7 +221,7 @@ -- | Get the address of the raw data payload from a mixed object.-payloadOfMixed [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+payloadOfMixed [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 16# @@ -239,7 +239,7 @@ -- } DataRaw; -- allocRaw- [r : %] + [r : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj = do bytesObj = add# [Nat#] (size# [Word32#])@@ -251,7 +251,7 @@ False# -> fail# [Ptr# r Obj] allocRaw_ok- [r : %]+ [r : Region] (tag : Tag#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj@@ -268,7 +268,7 @@ -- | Get the payload data from a raw object.-payloadOfRaw [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+payloadOfRaw [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 8# @@ -285,7 +285,7 @@ -- } DataRawSmall; -- allocRawSmall- [r : %]+ [r : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj = do bytesObj = add# [Nat#] 4# bytesPayload@@ -294,7 +294,7 @@ False# -> fail# [Ptr# r Obj] allocRawSmall_ok- [r : %]+ [r : Region] (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj@@ -312,6 +312,6 @@ -- | Get the payload data from a raw small object.-payloadOfRawSmall [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+payloadOfRawSmall [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 4#