diff --git a/ddc-code.cabal b/ddc-code.cabal --- a/ddc-code.cabal +++ b/ddc-code.cabal @@ -1,5 +1,5 @@ Name: ddc-code -Version: 0.4.1.3 +Version: 0.4.2.1 License: MIT License-file: LICENSE Author: The Disciplined Disciple Compiler Strike Force @@ -15,26 +15,39 @@ 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/debug/Trace.dcs + salt/runtime64/primitive/Array.dcs + salt/runtime64/primitive/Ref.dcs + salt/runtime64/primitive/Text.dcs + salt/runtime64/Apply.dcs salt/runtime64/Object.dcs sea/primitive/Primitive.c sea/primitive/Primitive.h - sea/runtime/Runtime.h + sea/runtime/Runtime.h + tetra/base/Data/Numeric/Bool.ds + tetra/base/Data/Numeric/Nat.ds + tetra/base/Data/Array.ds + tetra/base/Data/Function.ds + tetra/base/Data/List.ds + tetra/base/Data/Maybe.ds + tetra/base/Data/Ref.ds + tetra/base/Data/Stream.ds + tetra/base/Data/Text.ds + tetra/base/Data/Tuple.ds + + tetra/base/Math/Combinations.ds + + tetra/base/System/IO/Console.ds + + Library build-depends: - base >= 4.6 && < 4.8, - filepath == 1.3.* + base >= 4.6 && < 4.9, + filepath >= 1.3 && < 1.5 exposed-modules: DDC.Code.Config diff --git a/lite/base/Data/Container/List.dcl b/lite/base/Data/Container/List.dcl deleted file mode 100644 --- a/lite/base/Data/Container/List.dcl +++ /dev/null @@ -1,108 +0,0 @@ -module List -import foreign c value - addNat - : [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]. - 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# - -with letrec - - --- Constructors --------------------------------------------------------------- --- | Construct a list containing a single element. -singleton - [r : Region] [a : Data] - (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 : 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 - = private 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 : 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 - 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 : Region] [a : Data] - (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 : 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 - Nil - -> yy - - Cons x xs - -> Cons [r2] [a] x (append [:r1 r2 a:] xs yy) - - -------------------------------------------------------------------------------- --- | Take the length of a list. -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 : 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 - = case xx of - Nil -> acc - - Cons x xs - -> length2 [:r1 r2 a:] - (addNat [:r2 r2 r2:] acc (N# [r2] 1#)) - xs - diff --git a/lite/base/Data/Numeric/Bool.dcl b/lite/base/Data/Numeric/Bool.dcl deleted file mode 100644 --- a/lite/base/Data/Numeric/Bool.dcl +++ /dev/null @@ -1,104 +0,0 @@ -module Bool -export foreign c value - boxBool - : [r : Region]. - Bool# -(Alloc r | Use r)> - Bool r - - unboxBool - : [r : Region]. - Bool r -(Read r | Empty)> - Bool# - - addBool - : [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]. - Bool r1 -(Pure | Use r3)> - Bool r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> - Bool r3 - - not : [r1 r2 : Region]. - Bool r1 -(Read r1 + Alloc r2 | Use r1 + Use r2)> - Bool r2 - - 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]. - Bool r1 -(Pure | Use r1 + Use r2)> - Bool r2 -(Read r1 + Alloc r2 | Use r1 + Use r2)> - Bool r2 - -with letrec - - --- | Box a boolean. -boxBool [r : Region] - (i : Bool#) { Alloc r | Use r } - : Bool r - = B# [r] i - - --- | Unbox a boolean. -unboxBool - [r : Region] - (x : Bool r) { Read r | Empty } - : Bool# - = case x of - B# i -> i - - --- | Add two booleans. -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 - -> case y of { B# i2 - -> B# [r3] (add# [Bool#] i1 i2) } } - - --- | Multiply two naturals. -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 - -> case y of { B# i2 - -> B# [r3] (mul# [Bool#] i1 i2) } } - - --- | Boolean negation. -not [r1 r2 : Region] - (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 : 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 - False# -> B# [r2] False# - True# -> y - - --- | Right biased short-circuiting or. -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 - True# -> B# [r2] True# - False# -> y diff --git a/lite/base/Data/Numeric/Int.dcl b/lite/base/Data/Numeric/Int.dcl deleted file mode 100644 --- a/lite/base/Data/Numeric/Int.dcl +++ /dev/null @@ -1,77 +0,0 @@ -module Int -export foreign c value - boxInt - : [r : Region]. - Int# -(Alloc r | Use r)> - Int r - - unboxInt - : [r : Region]. - Int r -(Read r | Empty)> - Int# - - addInt - : [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]. - Int r1 -(Pure | Use r3)> - Int r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> - Int 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 - - --- | Box an integer. -boxInt [r : Region] - (i : Int#) { Alloc r | Use r } - : Int r - = I# [r] i - - --- | Unbox an integer. -unboxInt [r : Region] - (x : Int r) { Read r | Empty } - : Int# - = case x of - I# i -> i - - --- | Add two integers. -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 - -> case y of { I# i2 - -> I# [r3] (add# [Int#] i1 i2) } } - - --- | Subtract the second integer from the first. -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 - -> case y of { I# i2 - -> I# [r3] (sub# [Int#] i1 i2) } } - - --- | Multiply two integers. -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 - -> case y of { I# i2 - -> I# [r3] (mul# [Int#] i1 i2) } } - diff --git a/lite/base/Data/Numeric/Nat.dcl b/lite/base/Data/Numeric/Nat.dcl deleted file mode 100644 --- a/lite/base/Data/Numeric/Nat.dcl +++ /dev/null @@ -1,98 +0,0 @@ -module Nat -export foreign c value - boxNat - : [r : Region]. - Nat# -(Alloc r | Use r)> - Nat r - - unboxNat - : [r : Region]. - Nat r -(Read r | Empty)> - Nat# - - addNat - : [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]. - Nat r1 -(Pure | Use r3)> - Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> - Nat r3 - - mulNat - : [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]. - Nat r1 -(Pure | Use r3)> - Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> - Bool r3 - - neqNat - : [r1 r2 r3 : Region]. - Nat r1 -(Pure | Use r3)> - Nat r2 -(Read r1 + Read r2 + Alloc r3 | Use r1 + Use r3)> - Bool r3 - -with letrec - - --- | Box an natural. -boxNat [r : Region] - (i : Nat#) { Alloc r | Use r } - : Nat r - = N# [r] i - - --- | Unbox an natural. -unboxNat [r : Region] - (x : Nat r) { Read r | Empty } - : Nat# - = case x of { N# n -> n } - - --- | Add two naturals. -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 : 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 : 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 : 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 : 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) } } - diff --git a/lite/base/Math/Integer.dcl b/lite/base/Math/Integer.dcl deleted file mode 100644 --- a/lite/base/Math/Integer.dcl +++ /dev/null @@ -1,26 +0,0 @@ - -module Integer -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 - - 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 : Region] - (acc : Int r) {Pure | 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#)); - }; - } diff --git a/salt/primitive/Vector.dcs b/salt/primitive/Vector.dcs deleted file mode 100644 --- a/salt/primitive/Vector.dcs +++ /dev/null @@ -1,131 +0,0 @@ - --- | Vectors are arrays of unboxed values. -module Vector -import value - allocRaw : [r : Region]. Tag# -> Nat# -> Ptr# r Obj - payloadOfRaw : [r : Region]. 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 : Region] (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 : Region] (obj : Ptr# r Obj) : Nat# - = do payload = payloadOfRaw [r] obj - read# [Nat#] payload 0# - - --- | Unsafely read a byte from a vector. -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 - - --- Update --------------------------------------------------------------------- --- | Unsafely write a byte into a vector. -updateVector8 - [r : Region] - (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 : Region] - (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 : Region] - (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 : Region] - (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 : Region] - (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 - diff --git a/salt/primitive32/Int.dcs b/salt/primitive32/Int.dcs deleted file mode 100644 --- a/salt/primitive32/Int.dcs +++ /dev/null @@ -1,37 +0,0 @@ - --- | Int primitives for 32-bit machines. -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 - -import value - allocRawSmall :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj - -with letrec - -boxInt [r : Region] (x : Int#) : Ptr# r Obj - = do obj = allocRawSmall TAG0# 4# - addr = takePtr# obj - write# addr 4# x - obj - - -unboxInt [r : Region] (obj : Ptr# r Obj) : Int# - = do addr = takePtr# obj - read# addr 4# - - -addInt [r1 r2 r3 : Region] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj - = boxInt (add# (unboxInt x) (unboxInt y)) - - -subInt [r1 r2 r3 : Region] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj - = boxInt (sub# (unboxInt x) (unboxInt y)) - - -mulInt [r1 r2 r3 : Region] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj - = boxInt (mul# (unboxInt x) (unboxInt y)) diff --git a/salt/primitive64/Int.dcs b/salt/primitive64/Int.dcs deleted file mode 100644 --- a/salt/primitive64/Int.dcs +++ /dev/null @@ -1,38 +0,0 @@ - --- | Int primitives for 64-bit machines. -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 - -import value - allocRawSmall :: [r : Region]. Tag# -> Nat# -> Ptr# r Obj - -with letrec - -boxInt [r : Region] (x : Int#) : Ptr# r Obj - = do obj = allocRawSmall TAG0# 8# - addr = takePtr# obj - write# addr 4# x - obj - - -unboxInt [r : Region] (obj : Ptr# r Obj) : Int# - = do addr = takePtr# obj - read# addr 4# - - -addInt [r1 r2 r3 : Region] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj - = boxInt (add# (unboxInt x) (unboxInt y)) - - -subInt [r1 r2 r3 : Region] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj - = boxInt (sub# (unboxInt x) (unboxInt y)) - - -mulInt [r1 r2 r3 : Region] (x : Ptr# r1 Obj) (y : Ptr# r2 Obj) : Ptr# r3 Obj - = boxInt (mul# (unboxInt x) (unboxInt y)) - diff --git a/salt/runtime64/Apply.dcs b/salt/runtime64/Apply.dcs new file mode 100644 --- /dev/null +++ b/salt/runtime64/Apply.dcs @@ -0,0 +1,466 @@ + + -- Thunk application. +module Runtime.Apply + +export value + runThunk : [r1 r2 : Region]. Ptr# r1 Obj -> Ptr# r2 Obj + + apply0 : [r0 r1 : Region] + . Ptr# r0 Obj -> Ptr# r1 Obj + + apply1 : [r0 r1 r2 : Region] + . Ptr# r0 Obj -> Ptr# r1 Obj -> Ptr# r2 Obj + + apply2 : [r0 r1 r2 r3 : Region] + . Ptr# r0 Obj -> Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj + + apply3 : [r0 r1 r2 r3 r4 : Region] + . Ptr# r0 Obj -> Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj + -> Ptr# r4 Obj + + apply4 : [r0 r1 r2 r3 r4 r5 : Region] + . Ptr# r0 Obj -> Ptr# r1 Obj -> Ptr# r2 Obj -> Ptr# r3 Obj + -> Ptr# r4 Obj -> Ptr# r5 Obj + +import value + allocThunk : [r1 : Region]. Addr# -> Nat# -> Nat# -> Nat# -> Nat# -> Ptr# r1 Obj + copyThunk : [r1 r2 : Region]. Ptr# r1 Obj -> Ptr# r2 Obj -> Nat# -> Nat# -> Ptr# r2 Obj + extendThunk : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj + + funThunk : [r1 : Region]. Ptr# r1 Obj -> Addr# + paramsThunk : [r1 : Region]. Ptr# r1 Obj -> Nat# + boxesThunk : [r1 : Region]. Ptr# r1 Obj -> Nat# + argsThunk : [r1 : Region]. Ptr# r1 Obj -> Nat# + runsThunk : [r1 : Region]. Ptr# r1 Obj -> Nat# + + setThunk : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Nat# -> Ptr# r2 Obj -> Void# + getThunk : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj + +with letrec + + +------------------------------------------------------------------------------- +-- | Run a thunk. +-- If this is the last run the evaluate it, +-- otherwise increment the run count. +-- +runThunk + [r1 r2 : Region] + (src : Ptr# r1 Obj) : Ptr# r2 Obj + = do + boxes = boxesThunk src + case boxes of + + -- The thunk is not boxed, + -- so running it would be a type error. + 0# -> fail# + + -- We don't know what region the result is going to be allocated + -- into, so need to assign it to rT. + 1# -> eval0 src + + _ -> do + fun = funThunk src + params = paramsThunk src + args = argsThunk src + runs' = add# (runsThunk src) 1# + + dst = allocThunk [r2] fun params boxes args runs' + copyThunk src dst 0# args + + +------------------------------------------------------------------------------- +-- The apply family of functions work out how call the function in a thunk. +-- Some arguments come from in the thunk itself, while some can be provided +-- directly to the evaluators. +-- +-- The hard limits are: +-- - The maximum arity for the function in a thunk is 12. +-- See the comment on applyZ. +-- - The maximum number of directly applied arguments is 4, +-- because we only have apply0 - apply4. +-- +-- The choice of where to set the limit is a balance between being able to +-- enumerate all possible calling conventions, and polluting the instruction +-- cache with code for too many evaluators. +-- + +----------------------------------------------------------- 0 +-- | Apply (evaluate) a thunk, given no more arguments. +apply0 [r0 r1 : Region] + (t : Ptr# r0 Obj) : Ptr# r1 Obj + = do + p = paramsThunk t + a = argsThunk t + b = boxesThunk t + r = runsThunk t + case mul# (eq# a p) (eq# b r) of + True# -> eval0 t + False# -> makePtr# (takePtr# t) + + +-- | Evaluate a saturated thunk, give no more arguments. +eval0 [r0 r1 : Region] + (t : Ptr# r0 Obj) : Ptr# r1 Obj + = do + f = funThunk t + p = paramsThunk t + a = argsThunk t + case p of + 0# -> callP0 f + + 1# -> callP1 f (getThunk t 0#) + + 2# -> callP2 f (getThunk t 0#) (getThunk t 1#) + + 3# -> callP3 f (getThunk t 0#) (getThunk t 1#) + (getThunk t 2#) + + 4# -> callP4 f (getThunk t 0#) (getThunk t 1#) + (getThunk t 2#) (getThunk t 3#) + + _ -> evalZ t f p (getThunk t (sub# a 4#)) + (getThunk t (sub# a 3#)) + (getThunk t (sub# a 2#)) + (getThunk t (sub# a 1#)) + + +----------------------------------------------------------- 1 +-- | Apply a thunk to one more argument. +apply1 [r0 r1 r2 : Region] + (t : Ptr# r0 Obj) (arg1 : Ptr# r1 Obj) + : Ptr# r2 Obj + = do + p = paramsThunk t + a = argsThunk t + b = boxesThunk t + r = runsThunk t + + case mul# (eq# (add# a 1#) p) (eq# b r) of { + True# -> + eval1 t arg1; + + False# -> + do t' = extendThunk t 1# + setThunk t' a 0# arg1 + t' + } + +-- | Evaluate a saturated thunk, given one more argument. +eval1 [r0 r1 r2 : Region] + (t : Ptr# r0 Obj) (arg1 : Ptr# r1 Obj) + : Ptr# r2 Obj + = do + f = funThunk t + p = paramsThunk t + a = argsThunk t + case p of + 0# -> apply1 (callP0 f) arg1 + + 1# -> callP1 f arg1 + + 2# -> callP2 f (getThunk t 0#) arg1 + + 3# -> callP3 f (getThunk t 0#) (getThunk t 1#) + arg1 + + 4# -> callP4 f (getThunk t 0#) (getThunk t 1#) + (getThunk t 2#) arg1 + + _ -> evalZ t f p (getThunk t (sub# a 3#)) + (getThunk t (sub# a 2#)) + (getThunk t (sub# a 1#)) + arg1 + + +----------------------------------------------------------- 2 +apply2 [r0 r1 r2 r3 : Region] + (t : Ptr# r0 Obj) + (arg1 : Ptr# r1 Obj) (arg2 : Ptr# r2 Obj) + : Ptr# r3 Obj + = do + p = paramsThunk t + a = argsThunk t + b = boxesThunk t + r = runsThunk t + + case eq# (add# a 1#) p of { True# -> + apply1 (eval1 t arg1) arg2; + + False# -> + case mul# (eq# (add# a 2#) p) (eq# b r) of { True# -> + eval2 t arg1 arg2; + + False# -> + do t' = extendThunk t 2# + setThunk t' a 0# arg1 + setThunk t' a 1# arg2 + t' + }} + + +-- | Evaluate a saturated thunk, given two more arguments. +eval2 [r0 r1 r2 r3 : Region] + (t : Ptr# r0 Obj) + (arg1 : Ptr# r1 Obj) (arg2 : Ptr# r2 Obj) + : Ptr# r3 Obj + = do + f = funThunk t + p = paramsThunk t + a = argsThunk t + case p of + 0# -> apply2 (callP0 f) arg1 arg2 + + 1# -> apply1 (callP1 f arg1) arg2 + + 2# -> callP2 f arg1 arg2 + + 3# -> callP3 f (getThunk t 0#) + arg1 arg2 + + 4# -> callP4 f (getThunk t 0#) (getThunk t 1#) + arg1 arg2 + + _ -> evalZ t f p (getThunk t (sub# a 2#)) + (getThunk t (sub# a 1#)) + arg1 arg2 + + +----------------------------------------------------------- 3 +-- | Apply a thunk to three more arguments. +apply3 [r0 r1 r2 r3 r4 : Region] + (t : Ptr# r0 Obj) + (arg1 : Ptr# r1 Obj) (arg2 : Ptr# r2 Obj) + (arg3 : Ptr# r3 Obj) + : Ptr# r4 Obj + = do + p = paramsThunk t + a = argsThunk t + b = boxesThunk t + r = runsThunk t + + case eq# (add# a 2#) p of { True# -> + apply1 (eval2 t arg1 arg2) arg3; + + False# -> + case eq# (add# a 1#) p of { True# -> + apply2 (eval1 t arg1) arg2 arg3; + + False# -> + case mul# (eq# (add# a 3#) p) (eq# b r) of { True# -> + eval3 t arg1 arg2 arg3; + + False# -> + do t' = extendThunk t 3# + setThunk t' a 0# arg1 + setThunk t' a 1# arg2 + setThunk t' a 2# arg3 + t' + }}} + + +-- | Evaluate a saturated thunk, given three more arguments. +eval3 [r0 r1 r2 r3 r4 : Region] + (t : Ptr# r0 Obj) + (arg1 : Ptr# r1 Obj) (arg2 : Ptr# r2 Obj) + (arg3 : Ptr# r3 Obj) + : Ptr# r4 Obj + = do + f = funThunk t + p = paramsThunk t + a = argsThunk t + case p of + 0# -> apply3 (callP0 f) arg1 arg2 arg3 + + 1# -> apply2 (callP1 f arg1) arg2 arg3 + + 2# -> apply1 (callP2 f arg1 arg2) arg3 + + 3# -> callP3 f arg1 arg2 arg3 + + 4# -> callP4 f (getThunk t 0#) + arg1 arg2 arg3 + + _ -> evalZ t f p (getThunk t (sub# a 1#)) + arg1 arg2 arg3 + + +----------------------------------------------------------- 4 +-- | Apply a thunk to four more arguments. +apply4 [r0 r1 r2 r3 r4 r5 : Region] + (t : Ptr# r0 Obj) + (arg1 : Ptr# r1 Obj) (arg2 : Ptr# r2 Obj) + (arg3 : Ptr# r3 Obj) (arg4 : Ptr# r4 Obj) + : Ptr# r5 Obj + = do + p = paramsThunk t + a = argsThunk t + b = boxesThunk t + r = runsThunk t + + case eq# (add# a 3#) p of { True# -> + apply1 (eval3 t arg1 arg2 arg3) arg4; + + False# -> + case eq# (add# a 2#) p of { True# -> + apply2 (eval2 t arg1 arg2) arg3 arg4; + + False# -> + case eq# (add# a 1#) p of { True# -> + apply3 (eval1 t arg1) arg2 arg3 arg4; + + False# -> + case mul# (eq# (add# a 4#) p) (eq# b r) of { True# -> + eval4 t arg1 arg2 arg3 arg4; + + False# -> + do t' = extendThunk t 4# + setThunk t' a 0# arg1 + setThunk t' a 1# arg2 + setThunk t' a 2# arg3 + setThunk t' a 3# arg4 + t' + }}}} + + +-- | Evaluate a saturated thunk, given four more arguments. +eval4 [r0 r1 r2 r3 r4 r5 : Region] + (t : Ptr# r0 Obj) + (arg1 : Ptr# r1 Obj) (arg2 : Ptr# r2 Obj) + (arg3 : Ptr# r3 Obj) (arg4 : Ptr# r4 Obj) + : Ptr# r5 Obj + = do + f = funThunk t + p = paramsThunk t + case p of + 0# -> apply4 (callP0 f) arg1 arg2 arg3 arg4 + + 1# -> apply3 (callP1 f arg1) arg2 arg3 arg4 + + 2# -> apply2 (callP2 f arg1 arg2) arg3 arg4 + + 3# -> apply1 (callP3 f arg1 arg2 arg3) arg4 + + 4# -> callP4 f arg1 arg2 arg3 arg4 + + _ -> evalZ t f p arg1 arg2 arg3 arg4 + + +----------------------------------------------------------- Z +-- Evaluate a saturated thunk, given its last 4 arguments. +-- We read the first (n-4) arguments directly from the thunk. +-- +-- In the object code, this function serves to enumerate the function calling +-- conventions for functions of 4-12 parameters. The fact that it stops at 12 +-- places a hard limit on the arity of the core programs that we're prepared +-- to compile. Supers higher than this arity need to be transformed to take +-- some of their arguments from a tuple instead of as direct parameters. +-- +-- In terms of the generated object program, we don't want to add more +-- alternatives here anyway because the underlying machine is unlikely to have +-- good calling convention when the object function has > 12 arguments. It +-- isn't useful for the 'arity' here to be more than the number of general +-- purpose registers we're likely to have in the machine. +-- +-- Note that some registers will also be needed for the stack pointer etc. +-- If the machine has 16 general purpose registers, then setting the maximum +-- arity here to 12 is probably enough. +-- +evalZ [r0 r1 r2 r3 r4 r5 : Region] + (t : Ptr# r0 Obj) (fun : Addr#) (arity : Nat#) + (argL3 : Ptr# r1 Obj) (argL2 : Ptr# r2 Obj) + (argL1 : Ptr# r3 Obj) (argL0 : Ptr# r4 Obj) + : Ptr# r5 Obj + + = do argA3 = takePtr# argL3 + argA2 = takePtr# argL2 + argA1 = takePtr# argL1 + argA0 = takePtr# argL0 + + case arity of + 4# -> makePtr# (call4# fun + argA3 argA2 argA1 argA0) + + 5# -> makePtr# (call5# fun + (getThunkA t 0#) + argA3 argA2 argA1 argA0) + + 6# -> makePtr# (call6# fun + (getThunkA t 0#) (getThunkA t 1#) + argA3 argA2 argA1 argA0) + + 7# -> makePtr# (call7# fun + (getThunkA t 0#) (getThunkA t 1#) + (getThunkA t 2#) + argA3 argA2 argA1 argA0) + + 8# -> makePtr# (call8# fun + (getThunkA t 0#) (getThunkA t 1#) + (getThunkA t 2#) (getThunkA t 3#) + argA3 argA2 argA1 argA0) + + 9# -> makePtr# (call9# fun + (getThunkA t 0#) (getThunkA t 1#) + (getThunkA t 2#) (getThunkA t 3#) + (getThunkA t 4#) + argA3 argA2 argA1 argA0) + + 10# -> makePtr# (call10# fun + (getThunkA t 0#) (getThunkA t 1#) + (getThunkA t 2#) (getThunkA t 3#) + (getThunkA t 4#) (getThunkA t 5#) + argA3 argA2 argA1 argA0) + + 11# -> makePtr# (call11# fun + (getThunkA t 0#) (getThunkA t 1#) + (getThunkA t 2#) (getThunkA t 3#) + (getThunkA t 4#) (getThunkA t 5#) + (getThunkA t 6#) + argA3 argA2 argA1 argA0) + + 12# -> makePtr# (call12# fun + (getThunkA t 0#) (getThunkA t 1#) + (getThunkA t 2#) (getThunkA t 3#) + (getThunkA t 4#) (getThunkA t 5#) + (getThunkA t 6#) (getThunkA t 7#) + argA3 argA2 argA1 argA0) + + _ -> fail# + + +callP0 [r1 : Region] + (f : Addr#) : Ptr# r1 Obj + = makePtr# (call0# f) + +callP1 [r1 r2 : Region] + (f : Addr#) + (a1 : Ptr# r1 Obj) + : Ptr# r2 Obj + = makePtr# (call1# f (takePtr# a1)) + +callP2 [r1 r2 r3 : Region] + (f : Addr#) + (a1 : Ptr# r1 Obj) (a2 : Ptr# r2 Obj) + : Ptr# r3 Obj + = makePtr# (call2# f (takePtr# a1) (takePtr# a2)) + +callP3 [r1 r2 r3 r4 : Region] + (f : Addr#) + (a1 : Ptr# r1 Obj) (a2 : Ptr# r2 Obj) (a3 : Ptr# r3 Obj) + : Ptr# r4 Obj + = makePtr# (call3# f (takePtr# a1) (takePtr# a2) (takePtr# a3)) + +callP4 [r1 r2 r3 r4 r5 : Region] + (f : Addr#) + (a1 : Ptr# r1 Obj) (a2 : Ptr# r2 Obj) (a3 : Ptr# r3 Obj) (a4 : Ptr# r4 Obj) + : Ptr# r5 Obj + = makePtr# (call4# f (takePtr# a1) (takePtr# a2) (takePtr# a3) (takePtr# a4)) + + +-- | Like `getThunk`, but convert the result to a raw address. +getThunkA + [r1 : Region] + (obj : Ptr# r1 Obj) (index : Nat#) : Addr# + = read# (takePtr# obj) + (add# 16# (shl# index (size2# [Addr#]))) + diff --git a/salt/runtime64/Object.dcs b/salt/runtime64/Object.dcs --- a/salt/runtime64/Object.dcs +++ b/salt/runtime64/Object.dcs @@ -65,28 +65,49 @@ -- that can load them typically suffer a penalty, so it is good to align heap -- objects anyway. -- -module Object +module Runtime.Object export value - getTag : [r : Region]. Ptr# r Obj -> Tag# + -- Get the tag of an object. + 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# + -- Thunk initialization. + allocThunk : [r1: Region]. Addr# -> Nat# -> Nat# -> Nat# -> Nat# -> Ptr# r1 Obj + copyThunk : [r1 r2: Region]. Ptr# r1 Obj -> Ptr# r2 Obj -> Nat# -> Nat# -> Ptr# r2 Obj + extendThunk : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj - 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# + funThunk : [r1: Region]. Ptr# r1 Obj -> Addr# + paramsThunk : [r1: Region]. Ptr# r1 Obj -> Nat# + boxesThunk : [r1: Region]. Ptr# r1 Obj -> Nat# + argsThunk : [r1: Region]. Ptr# r1 Obj -> Nat# + runsThunk : [r1: Region]. Ptr# r1 Obj -> Nat# - allocRaw : [r : Region]. Tag# -> Nat# -> Ptr# r Obj - payloadOfRaw : [r : Region]. Ptr# r Obj -> Ptr# r Word8# + setThunk : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Nat# -> Ptr# r2 Obj -> Void# + getThunk : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj - allocRawSmall : [r : Region]. Tag# -> Nat# -> Ptr# r Obj - payloadOfRawSmall : [r : Region]. Ptr# r Obj -> Ptr# r Word8# + -- Objects with just pointers to boxed things. + allocBoxed : [r1: Region]. Tag# -> Nat# -> Ptr# r1 Obj + getBoxed : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj + setBoxed : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj -> Void# + -- Object with mixed pointers and raw, non-pointer data. + allocMixed : [r1: Region]. Tag# -> Nat# -> Nat# -> Ptr# r1 Obj + getMixed : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj + payloadMixed : [r1: Region]. Ptr# r1 Obj -> Ptr# r1 Word8# + + -- Objects containing raw non-pointer data. + allocRaw : [r1: Region]. Tag# -> Nat# -> Ptr# r1 Obj + payloadRaw : [r1: Region]. Ptr# r1 Obj -> Ptr# r1 Word8# + payloadSizeRaw : [r1: Region]. Ptr# r1 Obj -> Nat# + + -- Objects with small, raw non-pointer data. + allocSmall : [r1: Region]. Tag# -> Nat# -> Ptr# r1 Obj + payloadSmall : [r1: Region]. Ptr# r1 Obj -> Ptr# r1 Word8# + + with letrec -- | Get the constructor tag of an object. -getTag [r : Region] (obj : Ptr# r Obj) : Tag# +getTag [r: Region] (obj: Ptr# r Obj): Tag# = do ptr = castPtr# obj header = peek# ptr 0# @@ -94,6 +115,190 @@ promote# tag32 +-- Thunk ---------------------------------------------------------------------- +-- | Allocate a Thunk +-- The payload contains a code pointer to the top-level supercombinator, +-- along with pointers to any available arguments. The actual pointer values +-- for the arguments are undefined. +-- +-- Note that unlike the GHC runtime we don't use a separate PAP +-- (Partial Application) object type to store partially applied arguments. +-- To perform a partial application we just create a new Thunk, copy the old +-- arguments into it, and write the extra partially applied arguments into the +-- new thunk. This is done to keep the implementation complexity down, and we +-- haven't performed any concrete performance comparisons between the two +-- approaches. +-- +-- For the GHC approach see: +-- How to make a fast curry, push/enter vs eval apply. +-- Simon Marlow and Simon Peyton Jones. +-- Journal of Functional Programming, 2006. +-- +-- A thunk wraps a top-level super of the following form: +-- f = /\a1 .. /\an. \x1 .. \xn. box .. box. body +-- +-- The type parameters a1 .. an are not represented at runtime. +-- +-- The value parameters x1 .. xn are counted in the boxes field. +-- We need to collect this many applied arguments in the thunk before +-- we can call the super. +-- +-- The boxes box .. box are counted in the boxes field of the thunk. +-- We need to run the thunk this many times before calling the super. +-- the expression 'box body' is equivalent to (\(_ : Void#). body), +-- and running it eliminates the outer lambda. +-- +-- typedef struct +-- { uint32_t tagFormat; // Constructor tag and format field. +-- uint8_t params; // Value parameters of super. +-- uint8_t boxes; // Number of runs required. +-- uint8_t args; // Available arguments. +-- uint8_t runs; // Number of times we've been run so far. +-- Fun* fun; // Function pointer. +-- Obj* payload[]; // Pointers to available arguments. +-- } Thunk; +-- +allocThunk [r: Region] (fun: Addr#) + (params: Nat#) (boxes: Nat#) + (args: Nat#) (runs: Nat#) + : Ptr# r Obj + = do + -- The payload needs to be big enough to store pointers to the + -- current available args. + bytesPayload = shl# args (size2# [Addr#]) + + bytesObj = add# (size# [Word32#]) -- tagFormat word. + (add# (size# [Word32#]) -- params/boxes/args/runs. + (add# (size# [Word64#]) -- function pointer. + bytesPayload)) -- function args. + + case check# bytesObj of + True# -> allocThunk_ok fun params boxes args runs bytesObj + False# -> fail# + +allocThunk_ok [r: Region] (fun: Addr#) + (params: Nat#) (boxes: Nat#) + (args: Nat#) (runs: Nat#) + (bytesObj: Nat#) + : Ptr# r Obj + = do + addr = alloc# bytesObj + + -- The tag of thunks is set to all 1 bits to make them easy to identify. + tag32 = 0xffffff00w32# + format = 0b00010001w32# + header = bor# tag32 format + write# addr 0# header + + -- Truncate params to 8-bits and write to object. + params8 = truncate# [Word8#] [Nat#] params + write# addr 4# params8 + + -- Truncate boxes to 8-bits and write to object. + boxes8 = truncate# [Word8#] [Nat#] boxes + write# addr 5# boxes8 + + -- Truncate args count to 8-bits and write to object. + args8 = truncate# [Word8#] [Nat#] args + write# addr 6# args8 + + -- Truncate runs count to 8-bits and write to object. + runs8 = truncate# [Word8#] [Nat#] runs + write# addr 7# runs8 + + -- Write the function pointer. + write# addr 8# fun + + makePtr# addr + + +-- | Copy the available arguments from one thunk to another. +copyThunk + [rSrc rDst: Region] + (src: Ptr# rSrc Obj) (dst: Ptr# rDst Obj) + (index: Nat#) (len: Nat#) + : Ptr# rDst Obj + = case ge# index len of + True# -> dst + False# + -> do ptr = getThunk src index + setThunk dst 0# index ptr + copyThunk src dst (add# index 1#) len + + +-- | Copy a thunk while extending the number of available argument slots. +-- This is used when implementing both the curryN# and applyN# core primops. +extendThunk + [rSrc rDst: Region] + (src: Ptr# rSrc Obj) (more: Nat#) + : Ptr# rDst Obj + = do + -- Function pointer and arity of that function. + fun = funThunk src + params = paramsThunk src + boxes = boxesThunk src + + -- Available arguments in source and destination. + args = argsThunk src + args' = add# args more + + -- Number of times the thunk has been run + runs = runsThunk src + + -- Allocate a new thunk with the orignal function and arity. + dst = allocThunk [rDst] (funThunk src) params boxes args' runs + + -- Copy argument pointers from the source into the new thunk. + copyThunk src dst 0# args + + +-- | Get the function pointer from a thunk. +funThunk [r: Region] (obj: Ptr# r Obj): Addr# + = read# [Addr#] (takePtr# obj) 8# + + +-- | Get the arity of the function in a thunk. +paramsThunk [r: Region] (obj: Ptr# r Obj): Nat# + = promote# (read# [Word8#] (takePtr# obj) 4#) + + +-- | Get the count of available arguments in a thunk. +boxesThunk [r: Region] (obj: Ptr# r Obj): Nat# + = promote# (read# [Word8#] (takePtr# obj) 5#) + + +-- | Get the count of available arguments in a thunk. +argsThunk [r: Region] (obj: Ptr# r Obj): Nat# + = promote# (read# [Word8#] (takePtr# obj) 6#) + + +-- | Get the count of available arguments in a thunk. +runsThunk [r: Region] (obj: Ptr# r Obj): Nat# + = promote# (read# [Word8#] (takePtr# obj) 7#) + + +-- | Set one of the pointers in a thunk. +-- The value is just a plain Addr# because we don't know what region the +-- original pointer in the Thunk was pointing to. Also, when setting these +-- pointers for the first time the pointer values in the thunk are undefined. +-- This takes a 'base' and 'offset' parameter separately to allow for easier +-- code generation. +setThunk + [r1 r2: Region] + (obj: Ptr# r1 Obj) (base: Nat#) (offset: Nat#) (val: Ptr# r2 Obj): Void# + = write# (takePtr# obj) + (add# 16# (shl# (add# base offset) (size2# [Addr#]))) + (takePtr# val) + + +-- | Get one of the arguments from a thunk. +getThunk + [r1 r2: Region] + (obj: Ptr# r1 Obj) (index: Nat#): Ptr# r2 Obj + = read# (takePtr# obj) + (add# 16# (shl# index (size2# [Addr#]))) + + -- Boxed ---------------------------------------------------------------------- -- | Allocate a Boxed Data Object. -- The payload contains pointers to other heap objects. @@ -106,12 +311,12 @@ -- { uint32_t tagFormat; // Constructor tag and format field. -- uint32_t arity; // Arity of the data constructor. -- // (The number of pointers in the payload) --- ObjData payload[]; +-- ObjData payload[]; -- } DataBoxed; -- allocBoxed - [r : Region] - (tag : Tag#) (arity : Nat#) : Ptr# r Obj + [r: Region] + (tag: Tag#) (arity: Nat#): Ptr# r Obj = do -- Multiple arity by 8 bytes-per-pointer to get size of payload. bytesPayload = shl# arity (size2# [Addr#]) @@ -123,8 +328,8 @@ 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 @@ -141,18 +346,18 @@ ---- | Get one of the pointers from a boxed data object. -getFieldOfBoxed - [r1 : Region] [a : Data] - (obj : Ptr# r1 Obj) (index : Nat#) - : a +getBoxed + [r1 r2: Region] + (obj: Ptr# r1 Obj) (index: Nat#) + : Ptr# r2 Obj = 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# +setBoxed + [r1 r2: Region] + (obj: Ptr# r1 Obj) (index: Nat#) (val: Ptr# r2 Obj): Void# = write# (takePtr# obj) (add# 8# (shl# index (size2# [Addr#]))) val @@ -166,15 +371,16 @@ -- 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. --- ObjData payload[]; // Contains ptrCount pointers, then raw data. +-- { 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. +-- ObjData payload[]; // Contains ptrCount pointers, then raw data. -- } 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# arity 3# bytesObj = add# (size# [Word32#]) @@ -187,8 +393,9 @@ False# -> fail# [Ptr# r Obj] allocMixed_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 @@ -207,16 +414,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# 16# - (shl# index (size2# [Addr#])) +getMixed [r1 r2: Region] (obj: Ptr# r1 Obj) (index: Nat#): Ptr# r2 Obj + = read# (takePtr# obj) + (add# 16# (shl# index (size2# [Addr#]))) - 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# +payloadMixed [r: Region] (obj: Ptr# r Obj): Ptr# r Word8# = plusPtr# (castPtr# obj) 16# @@ -228,13 +432,13 @@ -- 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. +-- { 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 : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj + [r: Region] (tag: Tag#) (bytesPayload: Nat#): Ptr# r Obj = do bytesObj = add# (size# [Word32#]) (add# (size# [Word32#]) bytesPayload) @@ -244,7 +448,7 @@ False# -> fail# allocRaw_ok - [r : Region] (tag : Tag#) (bytesObj : Nat#) : Ptr# r Obj + [r: Region] (tag: Tag#) (bytesObj: Nat#): Ptr# r Obj = do addr = alloc# bytesObj @@ -260,34 +464,39 @@ -- | Get the payload data from a raw object. -payloadOfRaw [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# +payloadRaw [r: Region] (obj: Ptr# r Obj): Ptr# r Word8# = plusPtr# (castPtr# obj) 8# +-- | Get the size of the payload of a raw object, in bytes. +payloadSizeRaw [r: Region] (obj: Ptr# r Obj): Nat# + = promote# (read# [Word32#] (takePtr# obj) 4#) + + -- RawSmall ------------------------------------------------------------------- -- | A Small Raw object. --- The object size is encoded as part of format field. +-- 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. +-- The payload size must be no greater than 16 words, else undefined. -- -- typedef struct --- { uint32_t tagFormat; // Constructor tag and format field. --- uint8_t payload[]; // Raw data that does not contain heap pointers. +-- { uint32_t tagFormat; // Constructor tag and format field. +-- uint8_t payload[]; // Raw data that does not contain heap pointers. -- } DataRawSmall; -- -allocRawSmall - [r : Region] - (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj +allocSmall + [r: Region] + (tag: Tag#) (bytesPayload: Nat#): Ptr# r Obj = do bytesObj = add# 4# bytesPayload case check# bytesObj of - True# -> allocRawSmall_ok tag bytesPayload bytesObj + True# -> allocSmall_ok tag bytesPayload bytesObj False# -> fail# -allocRawSmall_ok - [r : Region] - (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj +allocSmall_ok + [r: Region] + (tag: Tag#) (bytesPayload: Nat#) (bytesObj: Nat#): Ptr# r Obj = do addr = alloc# bytesObj @@ -303,6 +512,6 @@ -- | Get the payload data from a raw small object. -payloadOfRawSmall [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# +payloadSmall [r: Region] (obj: Ptr# r Obj): Ptr# r Word8# = plusPtr# (castPtr# obj) 4# diff --git a/salt/runtime64/debug/Trace.dcs b/salt/runtime64/debug/Trace.dcs new file mode 100644 --- /dev/null +++ b/salt/runtime64/debug/Trace.dcs @@ -0,0 +1,235 @@ + +-- | Dumping of the runtime object graph. +module Dump + +export value + traceObj : [r : Region]. Bool# -> Ptr# r Obj -> Nat# + +import value + -- Primitives imported from C-land. + primPutString : TextLit# -> Void# + primShowAddr : Addr# -> TextLit# + primShowNat : Nat# -> TextLit# + primShowWord32 : Word32# -> TextLit# + + -- Generic objects. + getTag : [r : Region]. Ptr# r Obj -> Tag# + + -- Thunk objects. + paramsThunk : [r: Region]. Ptr# r Obj -> Nat# + boxesThunk : [r: Region]. Ptr# r Obj -> Nat# + argsThunk : [r: Region]. Ptr# r Obj -> Nat# + runsThunk : [r: Region]. Ptr# r Obj -> Nat# + funThunk : [r: Region]. Ptr# r Obj -> Addr# + getThunk : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj + + -- Boxed objects. + allocBoxed : [r1 : Region]. Tag# -> Nat# -> Ptr# r1 Obj + getBoxed : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj + setBoxed : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj -> Void# + +with letrec + + +------------------------------------------------------------------------------- +-- | Dump an object to stdout. +traceObj [r: Region] (trace: Bool#) (obj: Ptr# r Obj): Nat# + = do + ptr = castPtr# obj + header = peek# ptr 0# + + -- Get the object format, masking out the anchor flag. + wFormat = band# header 0b11110111w32# + nFormat = promote# wFormat + + case nFormat of + -- Thunk format. + 0b00010001w32# -> traceThunk trace obj + + -- Boxed object format. + 0b00100001w32# -> traceBoxed trace obj + + -- Raw format. + -- Payload contains raw unboxed data. + 0b00110001w32# -> traceRaw obj + + -- Small format, with the size in the top nibble. + -- Payload contains raw unboxed data. + _ -> do + wFormatLow = band# wFormat 0b00001111w32# + wFormatHigh = shr# 4w32# (band# wFormat 0b11110000w32#) + + case wFormatLow of + 0b0011w32# + -> traceSmall obj + + -- Some format that we don't handle yet, + -- or the header is trashed. + _ -> do primPutString "Unknown\n" + 0# + + +------------------------------------------------------------------------------- +-- | Print a thunk object to stdout. +traceThunk [r: Region] (trace: Bool#) (obj: Ptr# r Obj): Nat# + = do + ptr = castPtr# obj + header = peek# ptr 0# + format = band# header 0x0fw32# + tag = shr# header 8w32# + + primPutString "Thunk\n" + fieldAddr "{ ptr = " (takePtr# obj) + fieldWord32 " format = " format + fieldWord32 " tag = " tag + fieldNat " params = " (paramsThunk obj) + fieldNat " boxes = " (boxesThunk obj) + fieldNat " args = " (argsThunk obj) + fieldNat " runs = " (runsThunk obj) + fieldAddr " fun = " (funThunk obj) + traceThunkPtrs obj 0# + primPutString "}\n" + + case trace of + True# -> traceThunkPtrss obj 0# + False# -> 0# + + +-- | Print pointers in a thunk object, which point to more objects. +traceThunkPtrs [r: Region] (obj: Ptr# r Obj) (i: Nat#) : Nat# + = do args = argsThunk obj + case eq# args i of + True# + -> 0# + + False# + -> do addr = takePtr# (getThunk obj i) + primPutString " arg " + primPutString (primShowNat i) + primPutString " = " + primPutString (primShowAddr addr) + primPutString ";\n" + traceThunkPtrs obj (add# i 1#) + + +-- | Trace out the objects that this one refers to. +traceThunkPtrss [r: Region] (obj: Ptr# r Obj) (i: Nat#) : Nat# + = do args = argsThunk obj + case eq# args i of + True# + -> 0# + + False# + -> do traceObj True# (getThunk obj i) + traceThunkPtrss obj (add# i 1#) + + +------------------------------------------------------------------------------- +-- | Print a Boxed object to stdout. +traceBoxed [r: Region] (trace: Bool#) (obj: Ptr# r Obj): Nat# + = do + ptr = castPtr# obj + header = peek# ptr 0# + format = band# header 0x0fw32# + tag = shr# header 8w32# + arity = peek# ptr 4# + + primPutString "Boxed\n" + fieldAddr "{ ptr = " (takePtr# obj) + fieldWord32 " format = " format + fieldWord32 " tag = " tag + fieldNat " arity = " (promote# arity) + traceBoxedPtrs obj (promote# arity) 0# + primPutString "}\n" + + case trace of + True# -> traceBoxedPtrss obj (promote# arity) 0# + False# -> 0# + + +-- | Print pointers in a boxed object, which point to more objects. +traceBoxedPtrs [r: Region] (obj: Ptr# r Obj) (n: Nat#) (i: Nat#) : Nat# + = case eq# n i of + True# + -> 0# + + False# + -> do addr = takePtr# (getBoxed obj i) + + primPutString " arg " + primPutString (primShowNat i) + primPutString " = " + primPutString (primShowAddr addr) + primPutString ";\n" + traceBoxedPtrs obj n (add# i 1#) + + +-- | Trace out the objects that this one refers to. +traceBoxedPtrss [r: Region] (obj: Ptr# r Obj) (n: Nat#) (i: Nat#) : Nat# + = case eq# n i of + True# + -> 0# + + False# + -> do traceObj True# (getBoxed obj i) + traceBoxedPtrss obj n (add# i 1#) + + +------------------------------------------------------------------------------- +-- | Print a Raw object to stdout. +traceRaw [r: Region] (obj: Ptr# r Obj): Nat# + = do + ptr = castPtr# obj + header = peek# ptr 0# + format = band# header 0x0fw32# + tag = shr# header 8w32# + size = peek# ptr 4# + + primPutString "Raw\n" + fieldAddr "{ ptr = " (takePtr# obj) + fieldWord32 " format = " format + fieldWord32 " tag = " tag + fieldWord32 " size = " size + primPutString "}\n" + 0# + + +------------------------------------------------------------------------------- +-- | Print a Small object to stdout. +traceSmall [r: Region] (obj: Ptr# r Obj): Nat# + = do + ptr = castPtr# obj + header = peek# ptr 0# + format = band# header 0x0fw32# + size = shr# 4w32# (band# header 0xf0w32#) + + primPutString "Small\n" + fieldAddr "{ ptr = " (takePtr# obj) + fieldWord32 " format = " format + fieldWord32 " size = " size + primPutString "}\n" + 0# + + +------------------------------------------------------------------------------- +-- | Print an Addr# field to stdout. +fieldAddr (name: TextLit#) (val: Addr#): Void# + = do primPutString name + primPutString (primShowAddr val) + primPutString ";\n" + + +-- | Print a Nat# field to stdout. +fieldNat (name: TextLit#) (val: Nat#): Void# + = do primPutString name + primPutString (primShowNat val) + primPutString ";\n" + + +-- | Print a Word32# field to stdout. +fieldWord32 (name: TextLit#) (val: Word32#): Void# + = do primPutString name + primPutString (primShowWord32 val) + primPutString ";\n" + + diff --git a/salt/runtime64/primitive/Array.dcs b/salt/runtime64/primitive/Array.dcs new file mode 100644 --- /dev/null +++ b/salt/runtime64/primitive/Array.dcs @@ -0,0 +1,69 @@ + +-- | Arrays of pointers to boxed values. +module Runtime.Prim.Array +export value + allocArray : [r1 r2 : Region]. Nat# -> Ptr# r1 Obj -> Ptr# r2 Obj + writeArray : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj -> Ptr# r1 Obj + readArray : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj + fillArray : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Nat# -> Ptr# r2 Obj -> Ptr# r1 Obj + +import value + allocBoxed : [r1 : Region]. Tag# -> Nat# -> Ptr# r1 Obj + setBoxed : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj -> Void# + +with letrec + + +-- | Allocate an array of boxed values, consisting of the same element +-- for all positions. +allocArray + [r1 r2: Region] + (len: Nat#) (val: Ptr# r1 Obj): Ptr# r2 Obj + = do arr = allocBoxed [r2] (truncate# 0#) len + fillArray arr 0# len val + arr + + +-- | Write an element into an array. +writeArray + [r1 r2: Region] + (obj: Ptr# r1 Obj) (ix: Nat#) (val: Ptr# r2 Obj): Ptr# r1 Obj + = do + -- Get address of the first byte after the end of the array. + len = promote# (peek# [r1] [Word32#] (castPtr# obj) 4#) + top = add# 8# (shl# len (size2# [Addr#])) + + -- Bounded poke. + -- If the requested address is past the end of the array then abort. + off = add# 8# (shl# ix (size2# [Addr#])) + _ = pokeBounded# (castPtr# obj) off top val + obj + + +-- | Read an element from an array. +readArray + [r1 r2: Region] + (obj: Ptr# r1 Obj) (ix: Nat#): Ptr# r2 Obj + = do + -- Get address of the first byte after the end of the array. + len = promote# (peek# [r1] [Word32#] (castPtr# obj) 4#) + top = add# 8# (shl# len (size2# [Addr#])) + + -- Bounded peek. + -- If the requested address is past the end of the array then abort. + off = add# 8# (shl# ix (size2# [Addr#])) + result = peekBounded# (castPtr# obj) off top + result + + +-- | Fill all elements of an array with the same value. +fillArray + [r1 r2: Region] + (arr: Ptr# r1 Obj) (start end: Nat#) (val: Ptr# r2 Obj): Ptr# r1 Obj + + = case ge# start end of + True# -> arr + False# -> do + setBoxed arr start val + fillArray arr (add# start 1#) end val + diff --git a/salt/runtime64/primitive/Ref.dcs b/salt/runtime64/primitive/Ref.dcs new file mode 100644 --- /dev/null +++ b/salt/runtime64/primitive/Ref.dcs @@ -0,0 +1,34 @@ + +-- | References to boxed values. +module Runtime.Prim.Ref +export value + allocRef : [r1 r2 : Region]. Ptr# r1 Obj -> Ptr# r2 Obj + readRef : [r1 r2 : Region]. Ptr# r1 Obj -> Ptr# r2 Obj + writeRef_ : [r1 r2 : Region]. Ptr# r1 Obj -> Ptr# r2 Obj -> Void# + +import value + allocBoxed : [r1 : Region]. Tag# -> Nat# -> Ptr# r1 Obj + getBoxed : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj + setBoxed : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj -> Void# + +with letrec + + +-- | Allocate a new reference to some boxed value. +allocRef [r1 r2: Region] (val: Ptr# r1 Obj): Ptr# r2 Obj + = do ref = allocBoxed [r2] (truncate# 0#) 1# + setBoxed ref 0# val + ref + +-- | Read the value from a reference. +readRef [r1 r2: Region] (ref: Ptr# r1 Obj): Ptr# r2 Obj + = getBoxed ref 0# + + +-- | Write a value into reference. +writeRef_ [r1 r2: Region] (ref: Ptr# r1 Obj) (val: Ptr# r2 Obj): Void# + = setBoxed ref 0# val + + + + diff --git a/salt/runtime64/primitive/Text.dcs b/salt/runtime64/primitive/Text.dcs new file mode 100644 --- /dev/null +++ b/salt/runtime64/primitive/Text.dcs @@ -0,0 +1,72 @@ + +module Runtime.Prim.Text +export value + makeTextLit : [r1: Region]. Addr# -> Ptr# r1 Obj + takeTextLit : [r1: Region]. Ptr# r1 Obj -> Addr# + sizeOfTextLit : [r1: Region]. Ptr# r1 Obj -> Nat# + indexTextLit : [r1: Region]. Ptr# r1 Obj -> Nat# -> Word8# + +import value + -- Objects with raw, non-pointer data. + allocRaw : [r1: Region]. Tag# -> Nat# -> Ptr# r1 Obj + payloadRaw : [r1: Region]. Ptr# r1 Obj -> Ptr# r1 Word8# + payloadSizeRaw : [r1: Region]. Ptr# r1 Obj -> Nat# + +with letrec + + +-- | Make a boxed text literal from a pointer to a null terminated +-- sequence of bytes. +-- +-- We first take the length of the string for bounds checks during +-- indexing and store the pointer and length together in the object. +-- +-- typedef struct +-- { uint32_t tagFormat; // Constructor tag and format field. +-- uint32_t size // Size of this boxed object in bytes. +-- uint32_t length; // Length of the string literal in bytes. +-- uint8_t* ptr; // Pointer to null terminated string data. +-- } TextLit; +-- +makeTextLit [r1: Region] (addrString: Addr#): Ptr# r1 Obj + = do + len = sizeOfString 0# addrString + obj = allocRaw (truncate# 0#) (add# 4# (size# [Addr#])) + payload = takePtr# (payloadRaw obj) + write# [Word32#] payload 0# (truncate# len) + write# [Addr#] payload 4# addrString + obj + + +-- | Take the pointer from a text literal. +takeTextLit [r1: Region] (obj: Ptr# r1 Obj): Addr# + = do + payload = takePtr# (payloadRaw obj) + read# [Addr#] payload 4# + + +-- | Get the size of a text literal, in bytes. +sizeOfTextLit [r1: Region] (obj: Ptr# r1 Obj): Nat# + = do + payload = takePtr# (payloadRaw obj) + promote# (read# [Word32#] payload 0#) + + +-- | Get a single byte of a text literal. +indexTextLit [r1: Region] (obj: Ptr# r1 Obj) (ix: Nat#): Word8# + = do + charPtr = takeTextLit obj + size = sizeOfTextLit obj + + char = peekBounded# (makePtr# charPtr) ix size + char + + +-- | Get the size of a null-terminated array of characters, in bytes. +sizeOfString (i: Nat#) (str: Addr#): Nat# + = do + x = promote# (read# [Word8#] str i) + case x of + 0# -> i + _ -> sizeOfString (add# i 1#) str + diff --git a/sea/primitive/Primitive.c b/sea/primitive/Primitive.c --- a/sea/primitive/Primitive.c +++ b/sea/primitive/Primitive.c @@ -5,33 +5,83 @@ #include "Runtime.h" +// Abort the program due to an inexhaustive case match. +// +// When desugaring guards, if the compiler cannot determine that +// the guards are exhaustive then a call to this function is +// inserted as a default case. +// +Obj* primErrorDefault(string_t* source, uint32_t line) +{ + fprintf ( stderr + , "\nDDC runtime error: inexhaustive case match.\n at: %s:%d\n" + , source, line); + exit(1); + + return 0; +} + +// Show a pointer. +string_t* primShowAddr (void* ptr) +{ string_t* str = malloc(32); + snprintf(str, 32, "%p", ptr); + return str; +} + + // Show an integer. // This leaks the space for the string, but nevermind until we get a GC. -string_t* showInt (int i) +string_t* primShowInt (int i) { string_t* str = malloc(32); snprintf(str, 32, "%d", i); return str; } - // 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* primShowNat (nat_t i) { string_t* str = malloc(32); snprintf(str, 32, "%u", (unsigned int)i); return str; } +// Show a Word64. +string_t* primShowWord64 (uint64_t w) +{ string_t* str = malloc(11); + snprintf(str, 10, "%#08llx", w); + return str; +} -// Print a string to stdout. -void putStr (string_t* str) -{ fputs(str, stdout); +// Show a Word32. +string_t* primShowWord32 (uint32_t w) +{ string_t* str = malloc(7); + snprintf(str, 6, "%#04x", w); + return str; } +// Show a Word16. +string_t* primShowWord16 (uint16_t w) +{ string_t* str = malloc(5); + snprintf(str, 4, "%#02x", w); + return str; +} -// Print a string to stdout, with a newline. -void putStrLn (string_t* str) -{ fputs(str, stdout); - fputs("\n", stdout); +// Show a Word8. +string_t* primShowWord8 (uint8_t w) +{ string_t* str = malloc(4); + snprintf(str, 3, "%#01x", w); + return str; } + +// Print a C string to stdout. +void primPutString (string_t* str) +{ fputs(str, stdout); +} + + +// Print a text vector to stdout. +void primPutVector (Obj* obj) +{ string_t* str = (string_t*) _payloadRaw(obj); + fputs(str, stdout); +} diff --git a/sea/primitive/Primitive.h b/sea/primitive/Primitive.h --- a/sea/primitive/Primitive.h +++ b/sea/primitive/Primitive.h @@ -113,8 +113,7 @@ // 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); +extern string_t* primShowInt (int i); +extern string_t* primShowNat (nat_t i); +extern void primPutString (string_t* str); diff --git a/sea/runtime/Runtime.h b/sea/runtime/Runtime.h --- a/sea/runtime/Runtime.h +++ b/sea/runtime/Runtime.h @@ -177,6 +177,7 @@ } DataMixed; +// ---------------------------------------------------------------------------- // A Raw Data Object. // A raw data object does not contain heap pointers that need to be traced // by the garbage collector. @@ -185,6 +186,11 @@ uint32_t size; // Size of the whole object, in bytes. uint8_t payload[]; // Raw data that does not contain heap pointers. } DataRaw; + +static inline uint8_t* _payloadRaw(Obj* obj) +{ + return ((uint8_t*)obj) + 8; +} // A Small Raw object. diff --git a/tetra/base/Data/Array.ds b/tetra/base/Data/Array.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/Array.ds @@ -0,0 +1,12 @@ + +module Data.Array +export { allocArray; readArray; writeArray } + +import foreign boxed type + Array : Region ~> Data ~> Data + +import foreign c value + allocArray : [r: Region]. [a: Data]. Nat# -> a -> S (Alloc r) (Array r a) + readArray : [r: Region]. [a: Data]. Array r a -> Nat# -> S (Read r) a + writeArray : [r: Region]. [a: Data]. Array r a -> Nat# -> a -> S (Write r) Void# + diff --git a/tetra/base/Data/Function.ds b/tetra/base/Data/Function.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/Function.ds @@ -0,0 +1,22 @@ + +module Data.Function +export { id; apply; compose } +where + + +-- | Identity function. +id (x: a): a + = x + + +-- | Apply a function to its argument. +-- The operator '$' is desugared to applications of this function. +apply [a b: Data] (f: a -> b) (x: a): b + = f x + + +-- | Compose two functions. +-- The operator '∘' is desugared to applications of this function. +compose [a b c: Data] (f: b -> c) (g: a -> b): a -> c + = λx : a. f (g x) + diff --git a/tetra/base/Data/List.ds b/tetra/base/Data/List.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/List.ds @@ -0,0 +1,250 @@ + +module Data.List +export { singleton; replicate + ; enumFromTo + ; append + ; length + ; head + ; tail; tail1 + ; last; index + ; reverse + ; map; mapS + ; forS + ; zipWith; zipWithS + ; foldl; foldlS; sum; prod + ; foldr; foldrS + ; scanl + ; filter; filterS + ; any } +import Data.Numeric.Nat +where + +-- | Standard Cons-lists. +data List (a: Data) where + Nil : List a + Cons : a -> List a -> List a + + +-- Constructors --------------------------------------------------------------- +-- | Construct a list containing a single element. +singleton (x: a): List a + = Cons x Nil + + +-- | Construct a list of the given length where all elements are' +-- the same value. +replicate (n: Nat#) (x: a): List a + | n == 0 = Nil + | otherwise = Cons x (replicate (n - 1) x) + + +-- | Construct a range of values. +enumFromTo (start: Nat#) (end: Nat#): List Nat# + | start >= end = singleton start + | otherwise = Cons start (enumFromTo (start + 1) end) + + +-- | Append two lists. +append (xx yy: List a): List a + = case xx of + Nil -> yy + Cons x xs -> Cons x (append xs yy) + + +-- Projections ---------------------------------------------------------------- +-- | Take the length of a list. +length (xx: List a): Nat# + = case xx of + Nil -> 0 + Cons x xs -> 1 + length xs + + +-- | Take the head of a list, if there is one. +head (def: a) (xx: List a): a + = case xx of + Nil -> def + Cons x xs -> x + + +-- | Take the tail of a list, if there is one. +tail (def: List a) (xx: List a): List a + = case xx of + Nil -> def + Cons x xs -> xs + + +-- | Like `tail`, but if there is only one element then keep it. +tail1 (def: a) (xx: List a): List a + = case xx of + Nil -> singleton def + Cons x xs + -> case xs of + Nil -> singleton x + _ -> xs + + +-- | Take the last element of a list, if there is one. +last (def: a) (xx: List a): a + = case xx of + Nil -> def + Cons x xs + -> case xs of + Nil -> x + Cons y ys -> last def xs + + +index (def: a) (n: Nat#) (xx: List a): a + = case xx of + Nil -> def + Cons x xs + -> case n of + 0 -> x + _ -> index def (n - 1) xs + + +-- Transforms ----------------------------------------------------------------- +-- | Reverse the elements of a list. +-- This is a naive O(n^2) version for testing purposes. +reverse (xx: List a): List a + = case xx of + Nil -> Nil + Cons x xs -> append (reverse xs) (singleton x) + + +-- Maps ----------------------------------------------------------------------- +-- | Apply a worker function to every element of a list, yielding a new list. +map (f: a -> b) (xx: List a): List b + = case xx of + Nil -> Nil + Cons x xs -> Cons (f x) (map f xs) + + +-- | Apply a stateful worker function to every element of a list, +-- yielding a new list. +-- The worker is applied to the source elements left-to-right. +mapS (f: a -> S e b) (xx: List a): S e (List b) + = case xx of + Nil -> Nil + Cons x xs -> Cons (f x) (mapS f xs) + + +-- | Apply a function to all elements of a list, yielding nothing. +forS (xx: List a) (f: a -> S e Unit): S e Unit + = case xx of + Nil -> () + Cons x xs + -> do f x + forS xs f + + +-- Zips ----------------------------------------------------------------------- +zipWith (f: a -> b -> c) + (xx: List a) (yy: List b): List c + = case xx of + Nil -> Nil + Cons x xs + -> case yy of + Cons y ys + -> Cons (f x y) (zipWith f xs ys) + + Nil -> Nil + + +zipWithS (f: a -> b -> S e c) + (xx: List a) (yy: List b): S e (List c) + = case xx of + Nil -> Nil + Cons x xs + -> case yy of + Cons y ys + -> Cons (f x y) (zipWithS f xs ys) + + Nil -> Nil + + +-- Folds ---------------------------------------------------------------------- +-- | Reduce a list with a binary function and zero value, +-- from left to right. +foldl (f: b -> a -> b) (z: b) (xx: List a): b + = case xx of + Nil -> z + Cons x xs -> foldl f (f z x) xs + + +-- | Reduce a list with a stateful binary function and zero value, +-- from left to right. +foldlS (f: b -> a -> S e b) (z: b) (xx: List a): S e b + = case xx of + Nil -> z + Cons x xs -> foldlS f (f z x) xs + + +-- | Reduce a list with a binary function and zero value, +-- from right to left. +foldr (f: a -> b -> b) (z: b) (xx: List a): b + = case xx of + Nil -> z + Cons x xs -> f x (foldr f z xs) + + +-- | Reduce a list with a stateful binary function and zero value, +-- from right to left. +foldrS (f: a -> b -> S e b) (z: b) (xx: List a): S e b + = case xx of + Nil -> z + Cons x xs -> f x (foldrS f z xs) + + +-- | Take the sum of a list of Nats. +sum (xs: List Nat#): Nat# + = foldl (+) 0 xs + + +-- | Take the product of a list of Nats. +prod (xs: List Nat#): Nat# + = foldl (*) 1 xs + + +-- Scans ---------------------------------------------------------------------- +scanl (f: b -> a -> b) (acc: b) (xx: List a): List b + = case xx of + Nil + -> Cons acc Nil + + Cons x xs + -> let acc' = f acc x + in Cons acc (scanl f acc' xs) + + +-- Filters -------------------------------------------------------------------- +-- | Keep only those elements that match the given predicate. +filter (p: a -> Bool#) (xx: List a): List a + = case xx of + Nil -> Nil + Cons x xs + -> if p x + then Cons x (filter p xs) + else filter p xs + + +-- | Keep only those elements that match the given stateful predicate. +-- The predicate is applied to the list elements from left to right. +filterS (p: a -> S e Bool#) (xx: List a): S e (List a) + = case xx of + Nil -> Nil + Cons x xs + -> if p x + then Cons x (filterS p xs) + else filterS p xs + + +-- | Check if any of the members of the list match the given predicate. +any (p: a -> Bool#) (xx: List a): Bool# + = case xx of + Nil + -> False + + Cons x xs + | p x -> True + | otherwise -> any p xs + diff --git a/tetra/base/Data/Maybe.ds b/tetra/base/Data/Maybe.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/Maybe.ds @@ -0,0 +1,38 @@ + +module Data.Maybe +export { isNothing; isJust; fromMaybe } +where + + +-- | A `Maybe` may contain a value, or not. +data Maybe (a: Data) where + Nothing : Maybe a + Just : a -> Maybe a + + +-- | Check if the given value is a `Nothing`. +isNothing (m: Maybe a): Bool# + = case m of + Nothing -> True + Just x -> False + + +-- | Check if the given value is a `Just`. +isJust (m: Maybe a): Bool# + = case m of + Nothing -> False + Just x -> True + + +-- | Take the value from a `Just`, or return a default value. +fromMaybe (def: a) (m: Maybe a): a + = case m of + Nothing -> def + Just x -> x + + +-- | Apply a function to the value in a `Just`, or return a default value. +maybe (def: b) (f: a -> b) (m: Maybe a): b + = case m of + Nothing -> def + Just x -> f x diff --git a/tetra/base/Data/Numeric/Bool.ds b/tetra/base/Data/Numeric/Bool.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/Numeric/Bool.ds @@ -0,0 +1,24 @@ + +module Data.Numeric.Bool +export { not; and; or } +where + + +-- | Boolean NOT. +not (x: Bool#): Bool# + = if x then False + else True + + +-- | Boolean AND. +and (x y: Bool#): Bool# + = if x then y + else False + + +-- | Boolean OR. +or (x y: Bool#): Bool# + = if x then True + else y + + diff --git a/tetra/base/Data/Numeric/Nat.ds b/tetra/base/Data/Numeric/Nat.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/Numeric/Nat.ds @@ -0,0 +1,43 @@ + +module Data.Numeric.Nat +export { add; sub; mul; div; rem + ; eq; neq; lt; le; gt; ge + ; shl; shr; band; bor; bxor + ; divMod } +import Data.Tuple +where + +------------------------------------------------------------------------------- +-- Names used by the Source Tetra desugarer to implement infix operators. +add x y = add# [Nat#] x y + +sub x y + = if x == 0 + then 0 + else sub# [Nat#] x y + +mul x y = mul# [Nat#] x y +div x y = div# [Nat#] x y +rem x y = rem# [Nat#] x y + +eq x y = eq# [Nat#] x y +neq x y = neq# [Nat#] x y +lt x y = lt# [Nat#] x y +le x y = le# [Nat#] x y +gt x y = gt# [Nat#] x y +ge x y = ge# [Nat#] x y + + +------------------------------------------------------------------------------- +-- Aliases for other arithmetic functions +shl x y = shl# [Nat#] x y +shr x y = shr# [Nat#] x y +band x y = band# [Nat#] x y +bor x y = bor# [Nat#] x y +bxor x y = bxor# [Nat#] x y + + +divMod (n m: Nat#): Tup2 Nat# Nat# + = T2 (div n m) (rem n m) + + diff --git a/tetra/base/Data/Ref.ds b/tetra/base/Data/Ref.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/Ref.ds @@ -0,0 +1,19 @@ + +module Data.Ref +export { allocRef; readRef; writeRef } + +import foreign boxed type + Ref : Region ~> Data ~> Data + +import foreign c value + allocRef : [r: Region]. [a: Data]. a -> S (Alloc r) (Ref r a) + readRef : [r: Region]. [a: Data]. Ref r a -> S (Read r) a + writeRef_ : [r: Region]. [a: Data]. Ref r a -> a -> S (Write r) Void# + +where + + +-- | Wrap up the primitive writeRef to return a unit result. +writeRef (ref: Ref r a) (x: a): S (Write r) Unit + = do writeRef_ ref x + () diff --git a/tetra/base/Data/Stream.ds b/tetra/base/Data/Stream.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/Stream.ds @@ -0,0 +1,221 @@ + +module Data.Stream +export { streamOfList; listOfStream + ; sgenerate; senumFrom; srepeat; scons + ; smap; smapacc + ; sfold; sany + ; stake; stakeWhile; sfilter } +import Data.Numeric.Nat +import Data.List +import Data.Maybe +import Data.Tuple +import Data.Array +import Data.Numeric.Bool +import Data.Function +where + + +-- | Unbounded streams, +-- wraps a function that produces elements on demand. +data Stream (s a: Data) where + MkStream : (s -> Step s a) -> s -> Stream s a + +data Step (s a: Data) where + Yield : a -> s -> Step s a + Skip : s -> Step s a + Done : Step s a + + +-- Conversions ------------------------------------------------------------------------------------ +-- | Convert a list to a stream. +streamOfList (xx: List a): Stream (List a) a + = let step (s1: List a) + = case s1 of + Nil -> Done + Cons x xs -> Yield x xs + in MkStream step xx + + +-- | Convert a stream to a list. +listOfStream (ss: Stream s a): List a + = case ss of + MkStream f s0 + -> case f s0 of + Yield x s1 -> Cons x (listOfStream (MkStream f s1)) + Skip s1 -> listOfStream (MkStream f s1) + Done -> Nil + + +-- | Load the given number of elements from a stream and write them +-- into a freshly allocated array. +arrayOfStream + [r1: Region] + (n: Nat#) -- ^ Length of result array. + (d: a) -- ^ Default element value. + (ss: Stream s a) -- ^ Stream to evaluate. + : S (Alloc r1) (Array r1 a) + = extend r1 using r2 with { Write r2; Alloc r2 } in + do + -- Allocate an array of the given maximum size. + arr = allocArray [r2] n d + + -- Unstream elements into the array. + unstreamToArray ss arr 0 + + -- Return the completed array. + arr + + +-- | Unstream all available elements into the given array. +unstreamToArray + [r: Region] + (ss: Stream s a) (arr: Array r a) (ix: Nat#) + : S (Write r) Unit + = case ss of + MkStream f s0 + -> case f s0 of + Yield x s1 + -> do writeArray arr ix x + unstreamToArray (MkStream f s1) arr (ix + 1) + + Skip s1 + -> unstreamToArray (MkStream f s1) arr ix + + Done + -> () + + +-- Constructors ----------------------------------------------------------------------------------- +-- | Generate a stream, given a starting value and a stepper function. +sgenerate (x: s) (step: s -> Tup2 s a): Stream s a + = let step' sA + = case step sA of + T2 s' x -> Yield x s' + in MkStream step' x + +senumFrom (x: Nat#): Stream Nat# Nat# + = sgenerate x (λs: Nat#. T2 (s + 1) s) + + +-- | Create a stream that returns copies of the same value. +srepeat (x: a): Stream a a + = sgenerate x (λs: a. T2 s s) + + +-- | Cons an element to the front of a stream. +scons (x: a) (ss: Stream s a): Stream (Tup2 s Bool#) a + = case ss of + MkStream stepA sA0 + -> let stepA2 q + = case q of + T2 sA1 b + -> case b of + True -> Yield x (T2 sA1 False) + False -> case stepA sA1 of + Yield y sA2 -> Yield y (T2 sA2 False) + Skip sA2 -> Skip (T2 sA2 False) + Done -> Done + in MkStream stepA2 (T2 sA0 True) + + +-- Maps ------------------------------------------------------------------------------------------- +-- | Apply a function to every element of a stream. +smap (f: a -> b) (ss: Stream s a): Stream s b + = case ss of + MkStream stepA sA0 + -> let stepB q + = case stepA q of + Yield x sA1 -> Yield (f x) sA1 + Skip sA2 -> Skip sA2 + Done -> Done + in MkStream stepB sA0 + + +-- Scans ------------------------------------------------------------------------------------------ +-- | Like `smap`, but keep a running accumulator as we walk along the stream. +smapacc (f: a -> b -> Tup2 a c) (z: a) + (ss: Stream s b): Stream (Tup2 s a) c + = case ss of + MkStream fB sB0 + -> let stepC q + = case q of + T2 sB1 xA1 + -> case fB sB1 of + Yield xB1 sB2 + -> case f xA1 xB1 of + T2 xA2 xC2 + -> Yield xC2 (T2 sB2 xA2) + Skip sB2 -> Skip (T2 sB2 xA1) + Done -> Done + in MkStream stepC (T2 sB0 z) + + +-- Folds ------------------------------------------------------------------------------------------ +-- | Fold all the elements from a stream. +sfold (f: a -> b -> a) (acc: a) (ss: Stream s b): a + = case ss of + MkStream step s0 + -> sconsume f acc step s0 + + +sconsume (f: a -> b -> a) (acc: a) + (step: s -> Step s b) (state: s) : a + = case step state of + Yield x s' -> sconsume f (f acc x) step s' + Skip s' -> sconsume f acc step s' + Done -> acc + + +-- | Check if any of the elements of this stream are true, +-- demanding only the prefix of non-true elements from the stream. +sany [s: Data] (ss: Stream s Bool#): Bool# + = sfold or False $ stakeWhile id ss + + +-- Projections ------------------------------------------------------------------------------------ +-- | Take the given number of elements from a stream. +stake (n: Nat#) (ss: Stream s a): Stream (Tup2 s Nat#) a + = case ss of + MkStream fA sA0 + -> let stepB q + = case q of + T2 sA ix + | ix >= n -> Done + | otherwise + -> case fA sA of + Yield x sA2 -> Yield x (T2 sA2 (ix + 1)) + Skip sA3 -> Skip (T2 sA3 ix) + Done -> Done + in MkStream stepB (T2 sA0 0) + + +-- | Take elements from a strem while they match the given predicate. +stakeWhile (p: a -> Bool#) (ss: Stream s a): Stream s a + = case ss of + MkStream stepA sA0 + -> let stepB q + = case stepA q of + Yield x sA1 + | p x -> Yield x sA1 + | otherwise -> Done [s] [a] + + Skip sA1 -> Skip sA1 + Done -> Done + + in MkStream stepB sA0 + + +-- | Take elements from a stream that match the given predicate. +sfilter (p: a -> Bool#) (ss: Stream s a): Stream s a + = case ss of + MkStream stepA sA0 + -> let stepB q + = case stepA q of + Yield x sA1 + | p x -> Yield x sA1 + | otherwise -> Skip sA1 + + Skip sA1 -> Skip sA1 + Done -> Done + + in MkStream stepB sA0 diff --git a/tetra/base/Data/Text.ds b/tetra/base/Data/Text.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/Text.ds @@ -0,0 +1,308 @@ + +module Data.Text +export +{ -- * Construction + textLit; textOfVector; vectorOfText; + paste; pastes; + + -- * Projections + sizeOfText; + + -- * Conversions + copyTextToVector; + copyTextLitToVector; + copyTextVecToVector; + + -- * Operators + textOfWord8; + + -- * Showing + showBool; + showNat; showBinaryNat; showDecimalNat; showHexNat; showBaseNat; + digitBinary; digitDecimal; digitHex; +} +import Data.Numeric.Nat +import Data.Numeric.Bool +import Data.Function +import Data.List + + +-- | The TextLit type is define in the runtime system and contains +-- a pointer to the literal utf-8 text data in static memory. +import foreign boxed type + TextLit : Data + + +-- | Runtime functions for dealing with unboxed text literals. +import foreign c value + + -- | Box a text literal. + makeTextLit : TextLit# -> TextLit + + -- | Get the size of a boxed text literal. + sizeOfTextLit : TextLit -> Nat# + + -- | Get a single byte from a boxed text literal. + indexTextLit : TextLit -> Nat# -> Word8# + + +-- | Top level region containing text vectors. +import foreign abstract type + RegionText : Region + + +-- | Capabilities to allocate and read top-level text vectors. +import foreign abstract capability + capTopTextAlloc : Alloc RegionText + capTopTextRead : Read RegionText + +where + + +------------------------------------------------------------------------------- +-- Names used by the Source Tetra desugarer to implement string literals. +textLit (x : TextLit#) : Text + = TextLit (makeTextLit x) + +paste (x y : Text) : Text + = TextApp x y + +pastes (x y : Text) : Text + = x % " " % y + + +------------------------------------------------------------------------------- +data Text where + TextLit : TextLit -> Text + TextVec : Vector# RegionText Word8# -> Text + TextApp : Text -> Text -> Text + + +-- Construction --------------------------------------------------------------- +-- | O(1). Wrap a vector of utf8 data into a text object. +textOfVector (vec: Vector# RegionText Word8#): Text + = TextVec vec + + +-- | Copy a Text object into a flat vector of utf-8 bytes. +vectorOfText [r1: Region] (tt: Text) + : S (Alloc r1) (Vector# r1 Word8#) + = extend r1 using r2 with { Alloc r2; Write r2 } in + do + -- Allocate a vector to hold all the data, + -- including an extra null terminator byte. + vec = vectorAlloc# [r2] [Word8#] (add (sizeOfText tt) 1) + + -- Copy the text data into the vector. + iEnd = copyTextToVector tt vec 0 + + -- Write the null terminator. + vectorWrite# vec iEnd 0w8 + + vec + + +-- | Wrap a single 8-bit character into a text object. +-- +textOfWord8 (w8: Word8#): Text + = TextVec + (extend RegionText using r1 with { Alloc r1; Write r1 } in + do -- Allocate the vector to hold the data, + -- including an extra null terminator byte. + vec = vectorAlloc# [r1] [Word8#] 2 + + -- Write the character. + vectorWrite# vec 0 w8 + + -- Write the null terminator. + vectorWrite# vec 1 0w8 + + vec) + + +-- Projections ---------------------------------------------------------------- +-- | Get the size of the utf8 data in a Text object, in bytes. +-- +-- * This is NOT the same as the length of the text string in characters, +-- as single characters can be encoded using multiple bytes. +-- +sizeOfText (tt: Text): Nat# + = case tt of + TextLit lit + -> sizeOfTextLit lit + + -- The size of a text vector is the vector size minus + -- the null terminator byte. + TextVec vec + -> vectorLength# vec - 1 + + TextApp t1 t2 + -> sizeOfText t1 + sizeOfText t2 + + +-- Conversions ---------------------------------------------------------------- +-- | Copy a text literal to a mutable vector of utf-8 bytes. +copyTextToVector + [r: Region] (tt: Text) (vec: Vector# r Word8#) (i0: Nat#) + : S (Write r) Nat# + = case tt of + TextLit lit + -> copyTextLitToVector lit vec i0 0 (sizeOfTextLit lit) + + TextVec vec2 + -> copyTextVecToVector vec2 vec i0 0 (vectorLength# vec2) + + TextApp t1 t2 + -> do i1 = copyTextToVector t1 vec i0 + i2 = copyTextToVector t2 vec i1 + i2 + + +-- | Copy a text literal to a mutable vector of utf-8 bytes. +copyTextLitToVector + [r: Region] (tt: TextLit) (vec: Vector# r Word8#) + (iDst iSrc nSrc: Nat#) + : S (Write r) Nat# + = case iSrc >= nSrc of + True -> iDst + False + -> do vectorWrite# vec iDst (indexTextLit tt iSrc) + + copyTextLitToVector + tt vec (iDst + 1) (iSrc + 1) nSrc + + +-- | Copy a text source vector to a mutable destination of utf-8 bytes. +copyTextVecToVector + [r1 r2: Region] + (vecSrc: Vector# r1 Word8#) (vecDst: Vector# r2 Word8#) + (iDst iSrc nSrc: Nat#) + : S (Read r1 + Write r2) Nat# + = case iSrc >= nSrc of + True -> iDst + + False -> do + vectorWrite# vecDst iDst (vectorRead# vecSrc iSrc) + + copyTextVecToVector + vecSrc vecDst (iDst + 1) (iSrc + 1) nSrc + + +-- Operators ------------------------------------------------------------------ +-- | If this text is not already in flat form then flatten it. +-- +-- This allocates a new contiguous vector for the text object and +-- allows the program to release space for intermediate append nodes. +-- +flattenText (tt: Text): Text + = case tt of + -- Single text literals are already flat. + TextLit lit -> tt + + -- Single text vectors are already flat. + TextVec vec -> tt + + -- Text has an outer append-node, + -- so flatten the whole thing. + TextApp _ _ -> textOfVector (run vectorOfText [RegionText] tt) + + +-- Showing -------------------------------------------------------------------- +-- | Convert a Bool to a String. +showBool (x : Bool#) : Text + = if x then "True" + else "False" + + +-- | Show a natural number. +showNat (x: Nat#): Text + = showBaseNat 10 digitDecimal 0 "X" x + + +------------------------------------------------------------------------------- +-- | Show a natural number, in binary. +showBinaryNat (x: Nat#): Text + = showBaseNat 2 digitBinary 0 "X" x + +digitBinary (n: Nat#): Text + = case n of + 0 -> "0" + 1 -> "1" + _ -> "X" + + +-- | Show a natural number in decimal. +showDecimalNat (x: Nat#): Text + = showBaseNat 10 digitDecimal 0 "X" x + +digitDecimal (n: Nat#): Text + = case n of + 0 -> "0" + 1 -> "1" + 2 -> "2" + 3 -> "3" + 4 -> "4" + 5 -> "5" + 6 -> "6" + 7 -> "7" + 8 -> "8" + 9 -> "9" + _ -> "X" + + +-- | Show a natural number in hex. +showHexNat (x: Nat#): Text + = showBaseNat 16 digitHex 0 "X" x + +digitHex (n: Nat#): Text + = case n of + 0 -> "0" + 1 -> "1" + 2 -> "2" + 3 -> "3" + 4 -> "4" + 5 -> "5" + 6 -> "6" + 7 -> "7" + 8 -> "8" + 9 -> "9" + 10 -> "a" + 11 -> "b" + 12 -> "c" + 13 -> "d" + 14 -> "e" + 15 -> "f" + _ -> "X" + + +------------------------------------------------------------------------------- +-- | Show a natural number using an arbitrary base encoding. +showBaseNat + (base: Nat#) -- ^ Base of encoding. + (digit: Nat# -> Text) -- ^ Show a digit in this base. + (width: Nat#) -- ^ Width of output, or 0 to not pad. + (pad: Text) -- ^ Character to pad output with. + (x: Nat#) -- ^ Number to print. + : Text + + = do s = showBaseNat' base digit width pad True x + if x < 0 + then "-" % s + else s + +showBaseNat' base digit width pad first x + | and (x == 0) first + = showBaseNat' base digit (width - 1) pad False x + % "0" + + | and (x == 0) (width > 0) + = showBaseNat' base digit (width - 1) pad False x + % pad + + | x == 0 + = "" + + | otherwise + = showBaseNat' base digit (width - 1) pad False (div x base) + % digit (rem x base) + diff --git a/tetra/base/Data/Tuple.ds b/tetra/base/Data/Tuple.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Data/Tuple.ds @@ -0,0 +1,17 @@ + +module Data.Tuple +export {fst; snd} +where + + +data Tup2 (a b: Data) where + T2 : a -> b -> Tup2 a b + + +fst (t: Tup2 a b): a + = case t of + T2 x y -> x + +snd (t: Tup2 a b): b + = case t of + T2 x y -> y diff --git a/tetra/base/Math/Combinations.ds b/tetra/base/Math/Combinations.ds new file mode 100644 --- /dev/null +++ b/tetra/base/Math/Combinations.ds @@ -0,0 +1,42 @@ + +module Math.Combinations +export { factorial + ; choose; chooseMany } +import Data.Numeric.Nat +import Data.List +where + +-- | Compute the factorial of a number. +-- +-- factorial n is the number of possible permutations +-- of a sequence of n things. +-- +factorial (n: Nat#): Nat# + = if n == 0 + then 1 + else n * factorial (n - 1) + + +-- | Compute the number of was of choosing r things from n things. +--- +-- Note that the textbook definition of this is, +-- div (factorial n) ( factorial (n - 1) * factorial r ) +-- but we factor out the (factorial (n - 1)) term beforehand to +-- make it easier to compute. +-- +choose (n r: Nat#): Nat# + = if r > n + then 0 + else div (prodRange n (n - (r - 1))) (factorial r) + +-- | Compute the product of the range [n, n-1 .. m] inclusive. +prodRange (n m: Nat#): Nat# + = if n == m + then n + else n * prodRange (n - 1) m + + +-- | Compute the number of ways of choosing collections of things +-- of sizes rs from n things. +chooseMany (n: Nat#) (rs: List Nat#): Nat# + = div (factorial n) (prod (map factorial rs)) diff --git a/tetra/base/System/IO/Console.ds b/tetra/base/System/IO/Console.ds new file mode 100644 --- /dev/null +++ b/tetra/base/System/IO/Console.ds @@ -0,0 +1,46 @@ + +module System.IO.Console +export { write; writel; writell } +import Data.Text + +import foreign abstract type + Console : Effect + +import foreign c value + primPutString : TextLit# -> S Console Void# + primPutVector : [r: Region]. Vector# r Word8# -> S Console Void# + +import foreign c value + -- Get the unboxed text literal from a boxed text literal. + -- The unboxed version is a pointer to the text data in static memory. + takeTextLit : TextLit -> TextLit# + +where + + +-- | Write text to the console. +write (tt: Text): S Console Unit + = box case tt of + TextLit lit + -> do primPutString (takeTextLit lit) + () + + TextVec vec + -> do primPutVector vec + () + + TextApp t1 t2 + -> do write t1 + write t2 + + +-- | Write text to the console with a trailing newline. +writel (tt: Text): S Console Unit + = do write tt + write "\n" + + +-- | Write text to the console with two trailing newlines. +writell (tt: Text): S Console Unit + = do write tt + write "\n\n"