ddc-code (empty) → 0.3.1.1
raw patch · 17 files changed
+1717/−0 lines, 17 filesdep +basedep +filepathsetup-changed
Dependencies added: base, filepath
Files
- DDC/Code/Config.hs +38/−0
- LICENSE +30/−0
- Setup.hs +2/−0
- ddc-code.cabal +47/−0
- lite/base/Data/Container/List.dcl +108/−0
- lite/base/Data/Numeric/Bool.dcl +106/−0
- lite/base/Data/Numeric/Int.dcl +77/−0
- lite/base/Data/Numeric/Nat.dcl +98/−0
- lite/base/Math/Integer.dcl +27/−0
- salt/primitive/Vector.dcs +131/−0
- salt/primitive32/Int.dcs +38/−0
- salt/primitive64/Int.dcs +39/−0
- salt/runtime32/Object.dcs +293/−0
- salt/runtime64/Object.dcs +317/−0
- sea/primitive/Primitive.c +35/−0
- sea/primitive/Primitive.h +120/−0
- sea/runtime/Runtime.h +211/−0
+ DDC/Code/Config.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE CPP #-}+-- | This module is responsible for finding out where the runtime system+-- and base library code is installed.+--+module DDC.Code.Config+ (locateBaseLibrary)+where++-------------------------------------------------------------------------------+-- When the compiler has been installed via 'cabal' install then we don't+-- have the full development source tree. +--+-- In this case the ddc-code.cabal file defines the preprocessesor flag+-- DDC_CABAL_INSTALLED, which tells us we can import the Cabal generated+-- Paths_ddc_code module and ask it where its put our files.+-- +#if defined(DDC_CABAL_INSTALLED)+import System.FilePath+import Paths_ddc_code as Cabal++locateBaseLibrary :: IO FilePath+locateBaseLibrary+ = do -- The rest of the files are in the same directory as the LICENSE+ -- file, so we can just ask for that one and take the directory name.+ licenseName <- Cabal.getDataFileName "LICENSE"+ let basePath = takeDirectory licenseName+ return basePath++-------------------------------------------------------------------------------+-- When the compiler is built from the development source tree via make+-- this code is in "packages/ddc-code", and we need to run 'ddc' from the +-- root of the source tree so it can find this path.+#else+locateBaseLibrary :: IO FilePath+locateBaseLibrary + = return "packages/ddc-code"+#endif+
+ LICENSE view
@@ -0,0 +1,30 @@+--------------------------------------------------------------------------------+The Disciplined Disciple Compiler License (MIT style)++Copyrite (K) 2007-2012 The Disciplined Disciple Compiler Strike Force+All rights reversed.++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++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+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ddc-code.cabal view
@@ -0,0 +1,47 @@+Name: ddc-code+Version: 0.3.1.1+License: MIT+License-file: LICENSE+Author: The Disciplined Disciple Compiler Strike Force+Maintainer: Ben Lippmeier <benl@ouroborus.net>+Build-Type: Simple+Cabal-Version: >=1.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.++data-files:+ LICENSE++ lite/base/Data/Numeric/Bool.dcl+ lite/base/Data/Numeric/Int.dcl+ lite/base/Data/Numeric/Nat.dcl+ lite/base/Math/Integer.dcl+ lite/base/Data/Container/List.dcl++ salt/primitive/Vector.dcs+ salt/primitive32/Int.dcs+ salt/primitive64/Int.dcs+ salt/runtime32/Object.dcs+ salt/runtime64/Object.dcs++ sea/primitive/Primitive.c+ sea/primitive/Primitive.h+ sea/runtime/Runtime.h ++Library+ build-depends:+ base == 4.6.*,+ filepath == 1.3.*++ exposed-modules:+ DDC.Code.Config++ other-modules:+ Paths_ddc_code++ cpp-options:+ -DDDC_CABAL_INSTALLED
+ lite/base/Data/Container/List.dcl view
@@ -0,0 +1,108 @@+module List+imports + addNat + :: [r1 r2 r3 : %].+ Nat r1 -(!0 | 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)>+ 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#++with letrec+++-- Constructors ---------------------------------------------------------------+-- | Construct a list containing a single element.+singleton + [r : %] [a : *]+ (x : a) { Alloc r | Use r }+ : List r a+ = Cons [r] [a] x (Nil [r] [a] ())+++-- | Construct a list containing copies of some value.+replicate+ [r1 r2 : %] [a : *]+ (n : Nat r1) { !0 | Use r1 + Use r2 }+ (x : a) { Read r1 + Read r2 + Alloc r2 | Use r1 + Use r2}+ : List r2 a+ = letregion r3 in+ case n of+ N# n2 + -> case eq# [Nat#] n2 0# of+ True# -> Nil [r2] [a] ()+ False# -> Cons [r2] [a] x + (replicate [:r3 r2 a:]+ (subNat [:r1 r3 r3:] n (N# [r3] 1#))+ x)++-- | Construct a range of Nat values+enumFromTo+ [r1 r2 : %]+ (n : Nat r2) { !0 | Use r1 + Use r2 }+ (max : Nat r2) { Read r2 + Alloc r1 + Alloc r2 | Use r1 + Use r2 }+ : List r1 (Nat r2)+ = case n of+ N# n2+ -> case max of+ N# max2 + -> case ge# [Nat#] n2 max2 of+ True# -> singleton [r1] [Nat r2] n+ False# -> Cons [r1] [Nat r2] n+ (enumFromTo [:r1 r2:]+ (addNat [:r2 r2 r2:] n (N# [r2] 1#))+ max)+++-- | O(n^2) reverse the elements in a list.+reverse [r1 r2 : %] [a : *]+ (xx : List r1 a) { Read r1 + Read r2 + Alloc r2 | Use r1 + Use r2 }+ : List r2 a+ = case xx of+ Nil -> Nil [:r2 a:] ()+ Cons x xs+ -> append [:r2 r2 a:] + (reverse [:r1 r2 a:] xs)+ (singleton [:r2 a:] x)+++-- | Append two lists.+append [r1 r2 : %] [a : *]+ (xx : List r1 a) { !0 | Use r1 + Use r2 }+ (yy : List r2 a) { Read r1 + Alloc r2 | Use r1 + Use r2 + DeepUse a }+ : List r2 a+ = case xx of+ Nil + -> yy++ Cons x xs+ -> Cons [r2] [a] x (append [:r1 r2 a:] xs yy)+++-------------------------------------------------------------------------------+-- | Take the length of a list.+length [r1 r2 : %] [a : *]+ (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 }+ (xx : List r1 a) { Read r1 + Read r2 + Alloc r2 + | Use r1 + Use r2}+ : Nat r2+ = case xx of+ Nil -> acc++ Cons x xs+ -> length2 [:r1 r2 a:]+ (addNat [:r2 r2 r2:] acc (N# [r2] 1#))+ xs+
+ lite/base/Data/Numeric/Bool.dcl view
@@ -0,0 +1,106 @@+module Bool+exports+ boxBool+ :: [r : %].+ Bool# -(Alloc r | Use r)>+ Bool r++ unboxBool+ :: [r : %].+ Bool r -(Read r | $0)>+ Bool#++ addBool+ :: [r1 r2 r3 : %].+ Bool r1 -(!0 | 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)>+ Bool r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>+ Bool r3++ not + :: [r1 r2 : %].+ Bool r1 -(Read r1 + Alloc r2 | Use r1 + Use r2)>+ Bool r2++ and + :: [r1 r2 r3 : %].+ Bool r1 -(!0 | 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)>+ Bool r2 -(Read r1 + Alloc r2 | Use r1 + Use r2)>+ Bool r2++with letrec+++-- | Box a boolean.+boxBool [r : %] + (i : Bool#) { Alloc r | Use r } + : Bool r+ = B# [r] i+++-- | Unbox a boolean.+unboxBool [r : %]+ (x : Bool r) { Read r | $0 } + : Bool#+ = case x of + B# i -> i+++-- | Add two booleans.+addBool [r1 r2 r3 : %] + (x : Bool r1) { !0 | Use r3 } + (y : Bool r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 }+ : Bool r3+ = case x of { B# i1 + -> case y of { B# i2 + -> B# [r3] (add# [Bool#] i1 i2) } }+++-- | Multiply two naturals.+mulBool [r1 r2 r3 : %] + (x : Bool r1) { !0 | Use r3 } + (y : Bool r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 }+ : Bool r3+ = case x of { B# i1 + -> case y of { B# i2 + -> B# [r3] (mul# [Bool#] i1 i2) } }+++-- | Boolean negation.+not [r1 r2 : %]+ (x : Bool r1) {Read r1 + Alloc r2 | Use r1 + Use r2}+ : Bool r2+ = case unboxBool [r1] x of+ False# -> B# [r2] True#+ True# -> B# [r2] False#+++-- | Right biased short-circuiting and.+and [r1 r2 r3 : %]+ (x : Bool r1) {!0 | Use r1 + Use r2 }+ (y : Bool r2) { Read r1 + Alloc r2 | Use r1 + Use r2 }+ : Bool r2+ = case unboxBool [r1] x of + False# -> B# [r2] False#+ True# -> y+++-- | Right biased short-circuiting or.+or [r1 r2 r3 : %]+ (x : Bool r1) {!0 | Use r1 + Use r2 }+ (y : Bool r2) { Read r1 + Alloc r2 | Use r1 + Use r2 }+ : Bool r2+ = case unboxBool [r1] x of + True# -> B# [r2] True#+ False# -> y
+ lite/base/Data/Numeric/Int.dcl view
@@ -0,0 +1,77 @@+module Int +exports+ boxInt + :: [r : %].+ Int# -(Alloc r | Use r)>+ Int r++ unboxInt + :: [r : %].+ Int r -(Read r | $0)>+ Int#++ addInt + :: [r1 r2 r3 : %].+ Int r1 -(!0 | 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)>+ Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>+ Int r3++ mulInt + :: [r1 r2 r3 : %].+ Int r1 -(!0 | Use r3)>+ Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>+ Int r3++with letrec+++-- | Box an integer.+boxInt [r : %] + (i : Int#) { Alloc r | Use r } + : Int r+ = I# [r] i+++-- | Unbox an integer.+unboxInt [r : %]+ (x : Int r) { Read r | $0 } + : Int#+ = case x of + I# i -> i+++-- | Add two integers.+addInt [r1 r2 r3 : %] + (x : Int r1) { !0 | Use r3 } + (y : Int r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 }+ : Int r3+ = case x of { I# i1 + -> case y of { I# i2 + -> I# [r3] (add# [Int#] i1 i2) } }+++-- | Subtract the second integer from the first.+subInt [r1 r2 r3 : %] + (x : Int r1) { !0 | Use r3 } + (y : Int r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 }+ : Int r3+ = case x of { I# i1 + -> case y of { I# i2+ -> I# [r3] (sub# [Int#] i1 i2) } }+++-- | Multiply two integers.+mulInt [r1 r2 r3 : %] + (x : Int r1) { !0 | Use r3 } + (y : Int r2) { Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3 }+ : Int r3+ = case x of { I# i1 + -> case y of { I# i2 + -> I# [r3] (mul# [Int#] i1 i2) } }+
+ lite/base/Data/Numeric/Nat.dcl view
@@ -0,0 +1,98 @@+module Nat +exports+ boxNat+ :: [r : %].+ Nat# -(Alloc r | Use r)>+ Nat r++ unboxNat + :: [r : %].+ Nat r -(Read r | $0)>+ Nat#++ addNat + :: [r1 r2 r3 : %].+ Nat r1 -(!0 | 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)>+ Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>+ Nat r3++ mulNat+ :: [r1 r2 r3 : %].+ Nat r1 -(!0 | 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)>+ Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>+ Bool r3++ neqNat + :: [r1 r2 r3 : %].+ Nat r1 -(!0 | Use r3)>+ Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)>+ Bool r3++with letrec+++-- | Box an natural.+boxNat [r : %] + (i : Nat#) { Alloc r | Use r } + : Nat r+ = N# [r] i+++-- | Unbox an natural.+unboxNat [r : %]+ (x : Nat r) { Read r | $0 } + : Nat#+ = case x of { N# n -> n }+++-- | Add two naturals.+addNat [r1 r2 r3 : %] + (x : Nat r1) { !0 | 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 } + (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 } + (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 }+ (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 }+ (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
@@ -0,0 +1,27 @@++module Integer +imports {+ subInt :: [r1 r2 r3 : %]+ . Int r1 -(!0 | 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)> + Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> + Int r3;+}+with letrec++fac [r : %] + (acc : Int r) {!0 | Use r}+ (n : Int r) {Read r + Alloc r | Use r} : Int r+ = case n of { + I# i -> + case i of {+ 0i# -> acc;+ 1i# -> acc;+ _ -> fac [r] (mulInt [:r r r:] acc n)+ (subInt [:r r r:] n (I# [r] 1i#));+ };+ }
+ salt/primitive/Vector.dcs view
@@ -0,0 +1,131 @@++-- | Vectors are arrays of unboxed values.+module Vector+imports {+ allocRaw :: [r : %]. Tag# -> Nat# -> Ptr# r Obj;+ payloadOfRaw :: [r : %]. Ptr# r Obj -> Addr#;+} +with letrec+++-- Allocation -----------------------------------------------------------------+-- | Alloc a vector of the given length.+-- +-- typedef struct+-- { nat_t length+-- uint8_t payload[] +-- } Vector8+--+allocVector8 [r : %] (length : Nat#) : Ptr# r Obj+ = do + -- total size of object payload.+ bytes = add# [Nat#] (bytesNat# V#) length+ obj = allocRaw [r] TAG0# bytes++ -- write the length field.+ payload = payloadOfRaw [r] obj+ write# [Nat#] payload 0# length++ -- zero fill vector+ fillVector8 [r] obj 0w8#++ obj+++-- Projections ----------------------------------------------------------------+-- | Get the length of a vector.+lengthVector8 [r : %] (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#+ = do payload = payloadOfRaw [r] obj+ offset = add# [Nat#] (bytesNat# V#) index+ read# [Word8#] payload offset +++-- Update ---------------------------------------------------------------------+-- | Unsafely write a byte into a vector.+updateVector8 + [r : %]+ (obj : Ptr# r Obj)+ (index : Nat#) (val : Word8#)+ : Void#+ = do payload = payloadOfRaw [r] obj+ offset = add# [Nat#] (bytesNat# V#) index+ write# [Word8#] payload offset val+++-- Fill -----------------------------------------------------------------------+-- | Fill a vector with the given value.+fillVector8 + [r : %]+ (obj : Ptr# r Obj) (val : Word8#)+ : Void#+ = do payload = payloadOfRaw [r] obj+ length = read# [Nat#] payload 0#++ buf = plusPtr# [r] [Word8#] (makePtr# [r] [Word8#] payload) (bytesNat# V#)+ max = plusPtr# [r] [Word8#] buf length+ fillPtr8 [r] buf max val+++-- | Fill a range of bytes with the given value.+fillPtr8 + [r : %] + (cur : Ptr# r Word8#) + (top : Ptr# r Word8#) (val : Word8#)+ : Void#+ = do + curAddr = takePtr# [r] [Word8#] cur+ topAddr = takePtr# [r] [Word8#] top+ case ge# [Addr#] curAddr topAddr of+ True# -> V#+ False# + -> do poke# [r] [Word8#] cur 0# val+ next = plusPtr# [r] [Word8#] cur 1#+ fillPtr8 [r] next top val+++-- Copy -----------------------------------------------------------------------+-- | Copy a vector into a fresh buffer.+copyVector8 + [r1 r2 : %]+ (vec1 : Ptr# r1 Obj)+ : Ptr# r2 Obj+ = do + len = lengthVector8 [r1] vec1+ vec2 = allocVector8 [r2] len++ src = plusPtr# [r1] [Word8#]+ (makePtr# [r1] [Word8#] (payloadOfRaw [r1] vec1))+ (bytesNat# V#)++ dst = plusPtr# [r2] [Word8#]+ (makePtr# [r2] [Word8#] (payloadOfRaw [r2] vec2))+ (bytesNat# V#)++ copyPtr8 [:r1 r2:] 0# len src dst+ vec2+++copyPtr8+ [r1 r2 : %]+ (offset : Nat#)+ (length : Nat#)+ (src : Ptr# r1 Word8#)+ (dst : Ptr# r2 Word8#)+ : Void#+ = do + case gt# [Nat#] offset length of+ True# -> V#+ False#+ -> do x1 = peek# [r1] [Word8#] src offset+ poke# [r2] [Word8#] dst offset x1+ + copyPtr8 [:r1 r2:] + (add# [Nat#] offset 1#)+ length src dst+
+ salt/primitive32/Int.dcs view
@@ -0,0 +1,38 @@++-- | 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++imports + allocRawSmall :: [r : %]. Tag# -> Nat# -> Ptr# r Obj++with letrec+++boxInt [r : %] (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#+ = 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+ = 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+ = 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+ = boxInt [r3] (mul# [Int#] (unboxInt [r1] x) (unboxInt [r2] y))
+ salt/primitive64/Int.dcs view
@@ -0,0 +1,39 @@++-- | 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++imports+ allocRawSmall :: [r : %]. Tag# -> Nat# -> Ptr# r Obj++with letrec +++boxInt [r : %] (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#+ = 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+ = 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+ = 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+ = boxInt [r3] (mul# [Int#] (unboxInt [r1] x) (unboxInt [r2] y))+
+ salt/runtime32/Object.dcs view
@@ -0,0 +1,293 @@++-- | Primitives for constructing and destructing 32-bit heap objects.+--+-- IMPORTANT: Only one of 'Object64' or 'Object32' is linked into the DDC+-- runtime system. It is also the /only/ module that knows about the layout+-- of heap objects. All access to heap objects must go through the interface+-- provided by this module. +--+-- All 32-bit heap objects start with a 32-bit word containing the constructor +-- tag of the object and a format field in the least-significant byte.+--+-- OBJECT+-- ~~~~~~+-- byte 3 2 1 0 (in MSB order)+-- TAG2 TAG1 TAG0 FORMAT ... +--+--+-- FORMAT field+-- ~~~~~~~~~~~~+-- bit 7 6 5 4 3 2 1 0+-- -- arg --- -- obj ---+-- X X X X X X 0 0 -- Forward / Broken-Heart+-- X X X X a X X X -- Anchor flag+-- 0 0 0 1 a 0 0 1 -- Thunk+-- 0 0 1 0 a 0 0 1 -- DataBoxed+-- 0 0 1 1 a 0 0 1 -- DataRaw+-- 0 1 0 0 a 0 0 1 -- DataMixed+-- 0 1 0 1 a 0 0 1 -- SuspIndir+-- -- size -- a 0 1 1 -- DataRawSmall+-- +-- * 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.+-- +-- We can identify these pointers because their lowest 2 bits are always 00.+-- This is because objects in the heap are always 4-byte aligned.+-- +-- For all other values of the format field, we ensure the lowest two bits+-- are not 00.+-- +-- * 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}+-- There are four data object formats:+-- DataBoxed: A boxed object containing pointers to more heap objects.+-- DataMixed: Some heap pointers, and some raw data.+-- DataRaw: Contains raw data and no pointers.+-- DataRawSmall: Contains raw data where the size is small enough to +-- encode directly in the format field.+-- +-- The -obj- (object mode) portion of the format field can be used to+-- determine if the object is a forwarding pointer, has a fixed value for+-- its format field, or is a DataRS object.+-- +-- Note: 64-bit floats.+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~+-- The various object formats always contain an even number of 32-bit words+-- in the header portion, before the payload. This ensures that the payloads+-- of all heap objects are 8-byte aligned. We do this to support architectures+-- that cannot load misaligned double precision floats (Float64). Architectures+-- that can load them typically suffer a penalty, so it is good to align heap+-- objects anyway.+--+module Object +exports+ getTag :: [r : %]. 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#++ 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#++ allocRaw :: [r : %]. Tag# -> Nat# -> Ptr# r Obj+ payloadOfRaw :: [r : %]. Ptr# r Obj -> Ptr# r Word8#++ allocRawSmall :: [r : %]. Tag# -> Nat# -> Ptr# r Obj+ payloadOfRawSmall :: [r : %]. Ptr# r Obj -> Ptr# r Word8#++with letrec++-- | Get the constructor tag of an object.+getTag [r : %] (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+ ++-- Boxed ----------------------------------------------------------------------+-- | Allocate a Boxed Data Object.+-- The payload contains pointers to other heap objects.+--+-- typedef struct+-- { 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[]; +-- } DataBoxed;+-- +allocBoxed + [r : %]+ (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])+ + bytesObj = add# [Nat#] 8# bytesPayload+ case check# bytesObj of+ True# -> allocBoxed_ok [r] tag arity bytesObj+ False# -> fail# [Ptr# r Obj]++allocBoxed_ok+ [r : %]+ (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj+ = do + addr = alloc# bytesObj++ tag32 = promote# [Word32#] [Tag#] tag+ format = 0b00100001w32#+ header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format+ write# [Word32#] addr 0# header++ arity32 = promote# [Word32#] [Nat#] arity+ write# [Word32#] addr 4# arity32++ makePtr# [r] [Obj] addr+++---- | Get one of the pointers from a boxed data object.+getFieldOfBoxed + [r1 : %] [a : *] + (obj : Ptr# r1 Obj) (index : Nat#) + : a+ = read# [a] (takePtr# [r1] [Obj] obj)+ (add# [Nat#] 8# (shl# [Nat#] index 2#))+++-- | Set one of the pointers from a boxed data object.+setFieldOfBoxed + [r1 : %] [a : *]+ (obj : Ptr# r1 Obj) (index : Nat#) + (val : a) + : Void#+ = write# [a] (takePtr# [r1] [Obj] obj)+ (add# [Nat#] 8# (shl# [Nat#] index 2#))+ val+++-- Mixed ----------------------------------------------------------------------+-- | Allocate a Mixed Data Object.+-- The payload contains some pointers followed by raw data.+--+-- typedef struct +-- { uint32_t tagFormat;+-- 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.+-- } DataMixed;+--+allocMixed+ [r : %]+ (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) : Ptr# r Obj+ = do + bytesPtrs = shl# [Nat#] arity 2#+ bytesObj = add# [Nat#] 16# (add# [Nat#] bytesPtrs bytesRaw)+ case check# bytesObj of+ True# -> allocMixed_ok [r] tag arity bytesRaw bytesObj+ False# -> fail# [Ptr# r Obj]++allocMixed_ok + [r : %]+ (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) (bytesObj : Nat#) : Ptr# r Obj+ = do+ addr = alloc# bytesObj++ tag32 = promote# [Word32#] [Tag#] tag+ format = 0b01000001w32#+ header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format+ write# [Word32#] addr 0# header+ write# [Word32#] addr 4# 0w32#++ bytesObj32 = promote# [Word32#] [Nat#] bytesObj+ write# [Word32#] addr 8# bytesObj32++ arity32 = promote# [Word32#] [Nat#] arity+ write# [Word32#] addr 12# arity32++ makePtr# [r] [Obj] addr+++-- | Get one of the pointers from a mixed data object.+fieldOfMixed [r : %] (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#+ = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 16#+++-- Raw ------------------------------------------------------------------------+-- | A Raw Data Object.+-- A raw data object does not contain heap pointers that need to be traced+-- by the garbage collector.+--+-- typedef struct +-- { uint32_t tagFormat; // Constructor tag and format field.+-- uint32_t size; // Size of the whole object, in bytes.+-- uint8_t payload[]; // Raw data that does not contain heap pointers.+-- } DataRaw;+--+allocRaw+ [r : %]+ (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj+ = do + bytesObj = add# [Nat#] 8# bytesPayload+ case check# bytesObj of+ True# -> allocRaw_ok [r] tag bytesPayload bytesObj+ False# -> fail# [Ptr# r Obj]++allocRaw_ok + [r : %] + (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj+ = do+ addr = alloc# bytesObj++ tag32 = promote# [Word32#] [Tag#] tag+ format = 0b00110001w32#+ header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format+ write# [Word32#] addr 0# header++ bytesObj32 = promote# [Word32#] [Nat#] bytesObj+ write# [Word32#] addr 4# bytesObj32++ makePtr# [r] [Obj] addr+++-- | Get the payload data from a raw object.+payloadOfRaw [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+ = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 8#+++-- RawSmall -------------------------------------------------------------------+-- | A Small Raw object.+-- The object size is encoded as part of format field.+-- This saves us from needing to include a separate arity field.+--+-- typedef struct +-- { uint32_t tagFormat; // Constructor tag and format field.+-- uint8_t payload[]; // Raw data that does not contain heap pointers.+-- } DataRawSmall;+--+allocRawSmall + [r : %] + (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj+ = do + bytesObj = add# [Nat#] 4# bytesPayload+ case check# bytesObj of+ True# -> allocRawSmall_ok [r] tag bytesPayload bytesObj+ False# -> fail# [Ptr# r Obj]++allocRawSmall_ok+ [r : %] + (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#+ format = 0b0011w32#+ header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) + (bor# [Word32#] (shl# [Word32#] wordsPayload32 4w32#) + format)+ write# [Word32#] addr 0# header++ makePtr# [r] [Obj] addr+++-- | Get the payload data from a raw small object.+payloadOfRawSmall [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+ = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 4#
+ salt/runtime64/Object.dcs view
@@ -0,0 +1,317 @@++-- | Primitives for constructing and destructing 64-bit heap objects.+--+-- IMPORTANT: Only one of 'Object64' or 'Object32' is linked into the DDC+-- runtime system. It is also the /only/ module that knows about the layout+-- of heap objects. All access to heap objects must go through the interface+-- provided by this module. +--+-- All 64-bit heap objects start with a 32-bit word containing the constructor+-- tag of the object and a format field in the least-significant byte.+--+-- OBJECT+-- ~~~~~~+-- byte 3 2 1 0 (in MSB order)+-- TAG2 TAG1 TAG0 FORMAT ... +--+--+-- FORMAT field+-- ~~~~~~~~~~~~+-- bit 7 6 5 4 3 2 1 0+-- -- arg --- -- obj ---+-- X X X X X X 0 0 -- Forward / Broken-Heart+-- X X X X a X X X -- Anchor flag+-- 0 0 0 1 a 0 0 1 -- Thunk+-- 0 0 1 0 a 0 0 1 -- DataBoxed+-- 0 0 1 1 a 0 0 1 -- DataRaw+-- 0 1 0 0 a 0 0 1 -- DataMixed+-- 0 1 0 1 a 0 0 1 -- SuspIndir+-- -- size -- a 0 1 1 -- DataRawSmall+-- +-- * 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.+-- +-- We can identify these pointers because their lowest 2 bits are always 00.+-- This is because objects in the heap are always 4-byte aligned.+-- +-- For all other values of the format field, we ensure the lowest two bits+-- are not 00.+-- +-- * 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}+-- There are four data object formats:+-- DataBoxed: A boxed object containing pointers to more heap objects.+-- DataMixed: Some heap pointers, and some raw data.+-- DataRaw: Contains raw data and no pointers.+-- DataRawSmall: Contains raw data where the size is small enough to +-- encode directly in the format field.+-- +-- The -obj- (object mode) portion of the format field can be used to+-- determine if the object is a forwarding pointer, has a fixed value for+-- its format field, or is a DataRS object.+-- +-- Note: 64-bit floats.+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~+-- The various object formats always contain an even number of 32-bit words+-- in the header portion, before the payload. This ensures that the payloads+-- of all heap objects are 8-byte aligned. We do this to support architectures+-- that cannot load misaligned double precision floats (Float64). Architectures+-- that can load them typically suffer a penalty, so it is good to align heap+-- objects anyway.+--+module Object +exports+ getTag :: [r : %]. 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#++ 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#++ allocRaw :: [r : %]. Tag# -> Nat# -> Ptr# r Obj+ payloadOfRaw :: [r : %]. Ptr# r Obj -> Ptr# r Word8#++ allocRawSmall :: [r : %]. Tag# -> Nat# -> Ptr# r Obj+ payloadOfRawSmall :: [r : %]. Ptr# r Obj -> Ptr# r Word8#++with letrec++-- | Get the constructor tag of an object.+getTag [r : %] (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+ ++-- Boxed ----------------------------------------------------------------------+-- | Allocate a Boxed Data Object.+-- The payload contains pointers to other heap objects.+--+-- The arity must be no greater than 2^32, else undefined.+-- This object type is typically used for algebraic data, which won't have+-- more than 2^32 fields.+--+-- typedef struct+-- { 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[]; +-- } DataBoxed;+-- +allocBoxed+ [r : %]+ (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)++ case check# bytesObj of+ True# -> allocBoxed_ok [r] tag arity bytesObj+ False# -> fail# [Ptr# r Obj]++allocBoxed_ok+ [r : %]+ (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj+ = do + addr = alloc# bytesObj++ tag32 = promote# [Word32#] [Tag#] tag+ format = 0b00100001w32#+ header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format+ write# [Word32#] addr 0# header++ -- Truncate arity to 32-bits.+ arity32 = truncate# [Word32#] [Nat#] arity+ write# [Word32#] addr 4# arity32++ makePtr# [r] [Obj] addr+++---- | Get one of the pointers from a boxed data object.+getFieldOfBoxed + [r1 : %] [a : *]+ (obj : Ptr# r1 Obj) (index : Nat#) + : a+ = read# [a] (takePtr# [r1] [Obj] obj)+ (add# [Nat#] 8#+ (shl# [Nat#] index (size2# [Addr#])))+++-- | Set one of the pointers from a boxed data object.+setFieldOfBoxed + [r1 : %] [a : *] + (obj : Ptr# r1 Obj) (index : Nat#)+ (val : a) + : Void#+ = write# [a] (takePtr# [r1] [Obj] obj)+ (add# [Nat#] 8# + (shl# [Nat#] index (size2# [Addr#])))+ val+++-- Mixed ----------------------------------------------------------------------+-- | Allocate a Mixed Data Object.+-- The payload contains some pointers followed by raw data.+--+-- The arity (ptrCount) must be no greater than 2^32, else undefined.+-- The payload can have length up to 2^64.+--+-- typedef struct +-- { 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.+-- } DataMixed;+--+allocMixed + [r : %]+ (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)))++ case check# bytesObj of+ True# -> allocMixed_ok [r] tag arity bytesObj+ False# -> fail# [Ptr# r Obj]++allocMixed_ok+ [r : %]+ (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj+ = do+ addr = alloc# bytesObj++ tag32 = promote# [Word32#] [Tag#] tag+ format = 0b01000001w32#+ header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format+ write# [Word32#] addr 0# header++ arity32 = truncate# [Word32#] [Nat#] arity+ write# [Word32#] addr 4# arity32++ bytesObj32 = promote# [Word64#] [Nat#] bytesObj+ write# [Word64#] addr 8# bytesObj32++ makePtr# [r] [Obj] addr+++-- | Get one of the pointers from a mixed data object.+fieldOfMixed [r : %] (obj : Ptr# r Obj) (index : Nat#) : Ptr# r Obj+ = do + offset = add# [Nat#] 16# + (shl# [Nat#] index (size2# [Addr#]))++ 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#+ = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 16#+++-- Raw ------------------------------------------------------------------------+-- | A Raw Data Object.+-- A raw data object does not contain heap pointers that need to be traced+-- by the garbage collector.+--+-- The payload size must be no greater than (2^32 - 8), else undefined.+-- +-- typedef struct +-- { uint32_t tagFormat; // Constructor tag and format field.+-- uint32_t size; // Size of the whole object, in bytes.+-- uint8_t payload[]; // Raw data that does not contain heap pointers.+-- } DataRaw;+--+allocRaw+ [r : %] + (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj+ = do + bytesObj = add# [Nat#] (size# [Word32#])+ (add# [Nat#] (size# [Word32#])+ bytesPayload)++ case check# bytesObj of+ True# -> allocRaw_ok [r] tag bytesObj+ False# -> fail# [Ptr# r Obj]++allocRaw_ok+ [r : %]+ (tag : Tag#) (bytesObj : Nat#) : Ptr# r Obj+ = do+ addr = alloc# bytesObj++ tag32 = promote# [Word32#] [Tag#] tag+ format = 0b00110001w32#+ header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format+ write# [Word32#] addr 0# header++ bytesObj32 = truncate# [Word32#] [Nat#] bytesObj+ write# [Word32#] addr 4# bytesObj32++ makePtr# [r] [Obj] addr+++-- | Get the payload data from a raw object.+payloadOfRaw [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+ = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 8#+++-- RawSmall -------------------------------------------------------------------+-- | A Small Raw object.+-- The object size is encoded as part of format field.+-- This saves us from needing to include a separate arity field.+--+-- The payload size must be no greater than 16, else undefined. +--+-- typedef struct +-- { uint32_t tagFormat; // Constructor tag and format field.+-- uint8_t payload[]; // Raw data that does not contain heap pointers.+-- } DataRawSmall;+--+allocRawSmall+ [r : %]+ (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj+ = do + bytesObj = add# [Nat#] 4# bytesPayload+ case check# bytesObj of+ True# -> allocRawSmall_ok [r] tag bytesPayload bytesObj+ False# -> fail# [Ptr# r Obj]++allocRawSmall_ok+ [r : %]+ (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#+ format = 0b0011w32#+ header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) + (bor# [Word32#] (shl# [Word32#] wordsPayload32 4w32#) + format)+ write# [Word32#] addr 0# header++ makePtr# [r] [Obj] addr+++-- | Get the payload data from a raw small object.+payloadOfRawSmall [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#+ = plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 4#+
+ sea/primitive/Primitive.c view
@@ -0,0 +1,35 @@++// Primitive operations that sea code uses.+// In future we'll just import these with the FFI.+#include <stdio.h>+#include "Runtime.h"+++// Show an integer.+string_t* showInt (int i)+{ string_t* str = malloc(32);+ snprintf(str, 32, "%d", i);+ return str;+}+++// Show a natural number.+string_t* showNat (nat_t i)+{ string_t* str = malloc(32);+ snprintf(str, 32, "%u", (unsigned int)i);+ return str;+}+++// Print a string to stdout.+void putStr (string_t* str)+{ fputs(str, stdout);+}+++// Print a string to stdout, with a newline.+void putStrLn (string_t* str)+{ fputs(str, stdout);+ fputs("\n", stdout);+}+
+ sea/primitive/Primitive.h view
@@ -0,0 +1,120 @@+// Primitive operations that generated C code uses.+// These should all be static inlined so we can compile programs without+// linking against external code. Operations that need manifest object+// code should be defined somewhere else, and preferably imported+// by the foreign-function interface.+#pragma once+#include <stdio.h>+#include "Runtime.h"++// Error Primops --------------------------------------------------------------+// Fail ungracefully.+// Called when we find an internal runtime error.+static inline +void _FAIL(void)+{ abort();+}+++// Store Primops --------------------------------------------------------------+extern addr_t _DDC_Runtime_heapTop;+extern addr_t _DDC_Runtime_heapMax;+++// Create the initial store.+static inline+void _CREATE (nat_t bytes)+{+ _DDC_Runtime_heapTop = malloc (bytes);+ _DDC_Runtime_heapMax = _DDC_Runtime_heapTop + bytes; +}+++// Allocate some space in the store+static inline +addr_t _ALLOC (nat_t bytes) +{ + addr_t obj = _DDC_Runtime_heapTop;+ _DDC_Runtime_heapTop = _DDC_Runtime_heapTop + bytes;+ return obj;+} +++// Check whether there is enough space on the heap to allocate +// an object of the given size in bytes.+static inline+bool_t _CHECK (nat_t bytes)+{+ return (_DDC_Runtime_heapTop + bytes < _DDC_Runtime_heapMax);+}+++// Get the size of a type.+#define _SIZE(type) \+ sizeof(type)+++// Get the log2 of the size of a type.+#define _SIZE2(type) \+ (sizeof(unsigned int) * 8 - __builtin_clz (sizeof(type)))+++// Read from a field of an Object.+// We use an explicit macro to make it easier to see what is happening in+// the generated code.+#define _READ(type,addr,offset) \+ (*((type *)(addr + offset)))+++// Write to a field of an Object.+// We use an explicit macro to make it easier to see what is happening in+// the generated code.+#define _WRITE(type,addr,offset,val) \+ ((*((type *)(addr + offset))) = val)+++// Add two addresses.+#define _PLUSADDR(addr,offset) \+ (addr + offset)+++// Read from a pointer plus an offset in bytes.+#define _PEEK(type,ptr,offset) \+ (*(type *)(((uint8_t *) ptr) + offset))+++// Write to a pointer plus an offset in bytes.+#define _POKE(type,ptr,offset,val) \+ (*((type *)( ((uint8_t*)ptr) + offset)) = val)+++// Add an offset in bytes to a pointer.+#define _PLUSPTR(type,ptr,offset) \+ ((type *)( ((uint8_t *)ptr) + offset))+++// Subtract an offset in bytes from a pointer.+#define _MINUSPTR(type,ptr,offset) \+ ((type *)( ((uint8_t *)ptr) - offset))+++// Pointer to address conversions.+#define _MAKEPTR(type,addr) \+ ((type *)addr)+++#define _TAKEPTR(type,ptr) \+ ((addr_t)ptr)+++#define _CASTPTR(dstType,srcType,ptr) \+ ((dstType*)ptr)+++// Other primitives -----------------------------------------------------------+// These are defined in C land and linked into the runtime library.+extern string_t* showInt (int i);+extern string_t* showNat (nat_t i);+extern void putStr (string_t* str);+extern void putStrLn (string_t* str);+
+ sea/runtime/Runtime.h view
@@ -0,0 +1,211 @@+#pragma once++// Interface to the DDC runtime.+// This is imported by generated modules and defines the types and macros+// that those modules uses.+//+// Everything should also be static-inlined, so we can run programs without+// needing to link against external code. Primops that are implemented with+// manifest object code should be imported separately.+// +#include <stdint.h>+#include <stdlib.h>+++// -- Types -------------------------------------------------------------------+// Boolean type.+typedef int bool_t;++// An unsigned natural number.+// Used for object sizes and field counts.+// Big enough to represent the number of allocatable bytes.+typedef size_t nat_t;++// Define int_t to make things look consistent.+typedef int int_t;++// Generic address type.+// #ifdef because Cygwin already defines it.+#ifndef __addr_t_defined+typedef uint8_t* addr_t;+#endif++// A constructor tag.+typedef uint32_t tag_t;++// A UTF8 string.+typedef char string_t;+++// -- Object Format -----------------------------------------------------------+//+// Object: TAG2 TAG1 TAG0 FORMAT ... +// byte 3 2 1 0 (in MSB order)+//+// All heap objects start with a 32-bit word containg the tag of the object,+// and a format field in the least-significant byte.+//+// Format Field+// ~~~~~~~~~~~~+//+// bit 7 6 5 4 3 2 1 0+// -- arg --- -- obj ---+// X X X X X X 0 0 -- Forward / Broken-Heart+// X X X X a X X X -- Anchor flag+// 0 0 0 1 a 0 0 1 -- Thunk+// 0 0 1 0 a 0 0 1 -- DataBoxed+// 0 0 1 1 a 0 0 1 -- DataRaw+// 0 1 0 0 a 0 0 1 -- DataMixed+// 0 1 0 1 a 0 0 1 -- SuspIndir+// -- size -- a 0 1 1 -- DataRawSmall+//+// * 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.+//+// We can identify these pointers because their lowest 2 bits are always 00.+// This is because objects in the heap are always 4-byte aligned.+//+// For all other values of the format field, we ensure the lowest two bits+// are not 00.+//+// * 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}+// There are four data object formats:+// DataBoxed: A boxed object containing pointers to more heap objects.+// DataMixed: Some heap pointers, and some raw data.+// DataRaw: Contains raw data and no pointers.+// DataRawSmall: Contains raw data where the size is small enough to +// encode directly in the format field.+//+// The -obj- (object mode) portion of the format field can be used to+// determine if the object is a forwarding pointer, has a fixed value for+// its format field, or is a DataRS object.+//+//+// Note: 64-bit architectures+// ~~~~~~~~~~~~~~~~~~~~~~~~~~~+// The various object formats always contain an even number of 32-bit words+// in the header portion, before the payload. This ensures that the payload+// is 8-byte aligned, which is needed for architecures that cannot load+// misaligned double precision floats (Float64).+++// The object types.+enum _ObjType +{ _ObjTypeUnknown,+ _ObjTypeForward,+ _ObjTypeThunk,+ _ObjTypeDataBoxed,+ _ObjTypeDataRaw,+ _ObjTypeDataMixed,+ _ObjTypeSuspIndir,+ _ObjTypeDataRawSmall+};+++// Whether the object is:+// a forwarding pointer, has a fixed format,+// or is a DataRawSmall object that has its payload size encoded in format+// field as well.+enum _ObjMode+{ _ObjModeForward = 0x00,+ _ObjModeFixed = 0x01,+ _ObjModeDataRawSmall = 0x03+};++// Use this mask to select the object mode portion of the format field.+#define _MaskObjMode 0x03+++// If the object has a fixed format field (ie, has _ObjModeFixed)+// then we can determine the format of the rest of the object by masking+// the format field with the following mask and testing against this enum.+enum _ObjFixed+{ _ObjFixedThunk = 0x11,+ _ObjFixedDataBoxed = 0x21,+ _ObjFixedDataRaw = 0x31,+ _ObjFixedDataMixed = 0x41,+ _ObjFixedSuspIndir = 0x51,+ _ObjFixedMapped = 0x71+};++#define _MaskObjFixed 0xf7+++// Optional flags in the format field.+enum _ObjFlag+{ _ObjFlagAnchored = 0x08+};++#define _MaskObjAnchored (~_ObjFlagAnchored)+++// -- Object Structures -------------------------------------------------------+// Object+// A General Object.+// All objects contain the tag and format field as the first 32-bit word.+// The following is a supertype of the others.+typedef struct +{ uint32_t tagFormat;+} Obj;+++// A Boxed Data Object.+// The payload contains pointers to other heap objects.+typedef struct +{ 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[]; +} DataBoxed;+++// A Mixed Data Object.+// The payload contains some pointers followed by raw data.+typedef struct +{ uint32_t tagFormat;+ 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.+} DataMixed;+++// A Raw Data Object.+// A raw data object does not contain heap pointers that need to be traced+// by the garbage collector.+typedef struct +{ uint32_t tagFormat; // Constructor tag and format field.+ uint32_t size; // Size of the whole object, in bytes.+ uint8_t payload[]; // Raw data that does not contain heap pointers.+} DataRaw;+++// A Small Raw object.+// The object size is encoded as part of format field.+// This saves us from needing to include a separate arity field.+typedef struct +{ uint32_t tagFormat; // Constructor tag and format field.+ uint8_t payload[]; // Raw data that does not contain heap pointers.+} DataRawSmall;+++// -- Object Utils ------------------------------------------------------------+// Get the constructor tag of an object.+static inline +uint32_t _tag (Obj* obj)+{ return obj ->tagFormat >> 8;+} ++// Get the format field of an object.+static inline +uint8_t _format (Obj* obj)+{ return (uint8_t)(obj ->tagFormat & 0x0f);+}+