ddc-code 0.4.1.3 → 0.4.2.1
raw patch · 30 files changed
+2280/−704 lines, 30 filesdep ~basedep ~filepathPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base, filepath
API changes (from Hackage documentation)
Files
- ddc-code.cabal +26/−13
- lite/base/Data/Container/List.dcl +0/−108
- lite/base/Data/Numeric/Bool.dcl +0/−104
- lite/base/Data/Numeric/Int.dcl +0/−77
- lite/base/Data/Numeric/Nat.dcl +0/−98
- lite/base/Math/Integer.dcl +0/−26
- salt/primitive/Vector.dcs +0/−131
- salt/primitive32/Int.dcs +0/−37
- salt/primitive64/Int.dcs +0/−38
- salt/runtime64/Apply.dcs +466/−0
- salt/runtime64/Object.dcs +267/−58
- salt/runtime64/debug/Trace.dcs +235/−0
- salt/runtime64/primitive/Array.dcs +69/−0
- salt/runtime64/primitive/Ref.dcs +34/−0
- salt/runtime64/primitive/Text.dcs +72/−0
- sea/primitive/Primitive.c +60/−10
- sea/primitive/Primitive.h +3/−4
- sea/runtime/Runtime.h +6/−0
- tetra/base/Data/Array.ds +12/−0
- tetra/base/Data/Function.ds +22/−0
- tetra/base/Data/List.ds +250/−0
- tetra/base/Data/Maybe.ds +38/−0
- tetra/base/Data/Numeric/Bool.ds +24/−0
- tetra/base/Data/Numeric/Nat.ds +43/−0
- tetra/base/Data/Ref.ds +19/−0
- tetra/base/Data/Stream.ds +221/−0
- tetra/base/Data/Text.ds +308/−0
- tetra/base/Data/Tuple.ds +17/−0
- tetra/base/Math/Combinations.ds +42/−0
- tetra/base/System/IO/Console.ds +46/−0
ddc-code.cabal view
@@ -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
− lite/base/Data/Container/List.dcl
@@ -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-
− lite/base/Data/Numeric/Bool.dcl
@@ -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
− lite/base/Data/Numeric/Int.dcl
@@ -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) } }-
− lite/base/Data/Numeric/Nat.dcl
@@ -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) } }-
− lite/base/Math/Integer.dcl
@@ -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#));- };- }
− salt/primitive/Vector.dcs
@@ -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-
− salt/primitive32/Int.dcs
@@ -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))
− salt/primitive64/Int.dcs
@@ -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))-
+ salt/runtime64/Apply.dcs view
@@ -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#])))+
salt/runtime64/Object.dcs view
@@ -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#
+ salt/runtime64/debug/Trace.dcs view
@@ -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"++
+ salt/runtime64/primitive/Array.dcs view
@@ -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+
+ salt/runtime64/primitive/Ref.dcs view
@@ -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++++
+ salt/runtime64/primitive/Text.dcs view
@@ -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+
sea/primitive/Primitive.c view
@@ -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);+}
sea/primitive/Primitive.h view
@@ -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);
sea/runtime/Runtime.h view
@@ -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.
+ tetra/base/Data/Array.ds view
@@ -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#+
+ tetra/base/Data/Function.ds view
@@ -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)+
+ tetra/base/Data/List.ds view
@@ -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+
+ tetra/base/Data/Maybe.ds view
@@ -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
+ tetra/base/Data/Numeric/Bool.ds view
@@ -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++
+ tetra/base/Data/Numeric/Nat.ds view
@@ -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)++
+ tetra/base/Data/Ref.ds view
@@ -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+ ()
+ tetra/base/Data/Stream.ds view
@@ -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
+ tetra/base/Data/Text.ds view
@@ -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) +
+ tetra/base/Data/Tuple.ds view
@@ -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
+ tetra/base/Math/Combinations.ds view
@@ -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))
+ tetra/base/System/IO/Console.ds view
@@ -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"