wiki:Language/Core/Tetra

Disciple Core Tetra

Disciple Core Tetra uses effect indexed computation types to represent effects.

Example code is at https://github.com/DDCSF/ddc/tree/master/demo/Tetra

Primitive Data Types

NameKindDescription
Void# :: Data Has no associated values
Bool# :: Data Unboxed booleans
Nat# :: Data Positive natural numbers
Int# :: Data Integers
WordN# :: Data N in [8, 16, 32, 64]
FloatN# :: Data N in [32, 64]
Addr# :: Data Raw store addresses
Ptr# :: Region ~> Data ~> Data Pointers to well-formed data
Tag# :: Data Data constructor tags
String# :: Data C style null-terminated strings (phantom)

Primitive Literals

TypeFormatNotes
Bool# True#, False#
Nat# 0 1 2 3 ...
Int# -2i# -1i# 0i# 1i# 2i# ...
WordN# 0wN# 1wN# 2wN# ... N in [8, 16, 32, 64]

Primitive Arithmetic Operators

Each of the primitive numeric operators can be instantiated for any of the primitive unboxed numeric types. This is Nat#, Int#, and WordN#.

NameTypeDescription
neg# :: [a : Data].a -> a Negation
add# :: [a : Data].a -> a -> a Addition
sub# :: [a : Data].a -> a -> a Subtraction
mul# :: [a : Data].a -> a -> a Multiplication
div# :: [a : Data].a -> a -> a Division
mod# :: [a : Data].a -> a -> a Modulus
rem# :: [a : Data].a -> a -> a Remainder
eq# :: [a : Data].a -> a -> Bool# Equality
neq# :: [a : Data].a -> a -> Bool# Negated Equality
gt# :: [a : Data].a -> a -> Bool# Greater-Than
ge# :: [a : Data].a -> a -> Bool# Greater-than-Equal
lt# :: [a : Data].a -> a -> Bool# Less-Than
le# :: [a : Data].a -> a -> Bool# Less-than-Equal
and# :: Bool# -> Bool# -> Bool# Boolean And
or# :: Bool# -> Bool# -> Bool# Boolean Or
shl# :: [a : Data].a -> a -> a Shift Left
shr# :: [a : Data].a -> a -> a Shift Right (*)
band# :: [a : Data].a -> a -> a Bitwise And
bor# :: [a : Data].a -> a -> a Bitwise Or
bxor# :: [a : Data].a -> a -> a Bitwise eXclusive Or

Primitive Numeric Casting Operators

NameType
promote# [a b : Data]. b -> a
truncate# [a b : Data]. b -> a

The promotion and truncation operators cast between numeric types.

promote# can be instantiated for any pair of numeric types such that no precision is lost in the result. For example, Word8# can be promoted to Word32# but not vis-versa. Whether promotion between types whose width depends on the platform is valid is platform dependent. For example, promotion from Word32# to Nat# is only valid on platforms when the size of Nat# is at least 32 bits.

truncate# performs an integer cast that may lose precision. For example Word32# can be truncated to Word8#. Only the least significant bits are preserved.

Invalid uses of promote# and truncate# will yield a static error at code generation time.

Primitive Store Operators

NameType
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) Unit
Last modified 3 years ago Last modified on Mar 8, 2014, 7:27:23 AM