wiki:Language/Core/Salt

Disciple Core Salt

Disciple Core Salt is an intermediate representation used when converting to C or LLVM code. It supports only those features that map directly onto C or LLVM. It does not support higher order functions, partial application, general application or nested functions. These features must be translated out when converting higher level programs to Core Salt.

All expressions are assumed to be impure, and can refer to arbitrary data in the context.

Core Salt includes only unboxed primitive types. Operations on boxed values are expanded to primitive operations when converting from higher level languages.

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

Primitive Type Constructors

NameKindDescription
Obj Data Phantom type to represent a heap object
Void# Data Has a place-holder constructor V#
Bool# Data Unboxed booleans
Nat# Data Positive natural numbers
Int# Data Integers
Tag# Data Data constructor tags
WordN# Data N in [8, 16, 32, 64]
Addr# Data Raw store addresses
Ptr# Region ~> Data ~> Data Pointers to well-formed data
String# Region ~> Data C style null-terminated strings
  • The Obj type is used in conjunction with a pointer type, that is Ptr# r Obj. Such a pointer can only be created with the makePtr# operator, as there are no data constructors for Obj.

Primitive Literals

TypeFormat Notes
Void# V# cannot be demanded
Bool# True#, False#
Nat# 0# 1# 2# 3# ...
Int# -2i# -1i# 0i# 1i# 2i# ...
Tag# TAG0# TAG1# ...
WordN# 0w8# 1wN# 2wN# ... N in [8, 16, 32, 64]
  • The V# constructor is a place holder for a missing value. V# can be used as the argument for any function accepting a parameter of type V#, but demanding its value with a case expression is a static type error.

Arithmetic and Logic Operators

The primitive numeric operators are polytypic, and can be instantiated for any of the primitive unboxed numeric types. Nat#, Int#, Tag# 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
rem# [a : Data].a -> a -> a Remainder
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
eq# [a : Data].a -> a -> Bool# Equality
neq# [a : Data].a -> a -> Bool# Negated Equality
gt# [a : Data].a -> a -> Bool# Greater-Than
lt# [a : Data].a -> a -> Bool# Less-Than
le# [a : Data].a -> a -> Bool# Less-than-Equal
ge# [a : Data].a -> a -> Bool# Greater-than-Equal
and# Bool# -> Bool# -> Bool# Boolean And
or# Bool# -> Bool# -> Bool# Boolean Or

Type Casts

NameType
promote# [a b : *]. b -> a
truncate# [a b : *]. 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 loses precision. For example Word32# can be truncated to Word8#. In all cases only the least significant bits are preserved.

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

Tail Calls

NameType
tailcall1# [a b : Data].(a -> b) -> a -> b
tailcall2# [a b c : Data].(a -> b -> c) -> a -> b -> c
tailcall3# [a b c d : Data].(a -> b -> c -> d) -> a -> b -> c -> d
... ...

The tailcallN# family of operators instruct the code generator to perform a tail call rather than a regular function call. There is no limit to the arity of the call. The tailcallN# operator must be used in tail call position, otherwise it will yield a static error at code generation time.

Control Operators

NameType
fail# [a : Data]. a
return# [a : Data]. a -> a

fail# aborts the program, ungracefully. This is used for internal runtime system errors or when the heap is known to be corrupted. The current implementation calls the abort() C library function.

return# returns from the enclosing function with the given value.

Store Operators

These operators allow raw access to the store. They are used to construct and destruct heap objects, as well as data in foreign memory.

IMPORTANT: All values of type Ptr# r Obj must point to well formed heap objects across calls to check#, recover# and alloc#. If not, then undefined. The intention is for heap objects to be constructed with the read# and write# operators, and only when they are completely formed should they be cast to a Ptr# r Obj. This ensures the runtime system can use values of type Ptr# r Obj as roots for the graph of live heap data.

NameTypeDescription
size# [a : Data]. Nat# Size in bytes of a primitive type.
size2# [a : Data]. Nat# Log2 of the size in bytes of a primitive type.
create# Nat# -> Void# Initialise the heap of the given size in bytes.
check# Nat# -> Bool# Check whether this many bytes is available on the heap.
recover# Nat# -> Void# Recover at least this many bytes in the heap.
alloc# Nat# -> Addr# Allocate space on the heap.
read# [a : Data].Addr# -> Nat# -> a Read from an address plus an offset in bytes.
write# [a : Data].Addr# -> Nat# -> a -> Void# Write to an address plus an offset in bytes.
plusAddr# Addr# -> Nat# -> Addr# Add an offset in bytes to an address.
minusAddr# Addr# -> Nat# -> Addr# Subtract an offset in bytes from an address.
peek# [r : Region].[a : Data].Ptr# r a -> Nat# -> a Read from a pointer plus an offset in bytes.
poke# [r : Region].[a : Data].Ptr# r a -> Nat# -> a Write to pointer plus an offset in bytes.
plusPtr# [r : Region].[a : Data].Ptr# r a -> Nat# -> Ptr# r a Add an offset in bytes to a pointer.
minusPtr# [r : Region].[a : Data].Ptr# r a -> Nat# -> Ptr# r a Subtract an offset in bytes from a pointer.
makePtr# [r : Region].[a : Data].Addr# -> Ptr# r a Convert an address to a pointer.
takePtr# [r : Region].[a : Data].Ptr# r a -> Addr# Convert a pointer to an address.
castPtr# [r : Region].[a b : Data].Ptr# r b -> Ptr# r a Cast a pointer to a different type.

size# and size2# work for primitive types whose width in bits is divisible by 8. Appling them to others like Void# or Bool# will yield a static error at code generation time.

create# creates the heap and must be called before any uses of the alloc# operator. It is passed the desired size of the heap in bytes. Calling create# multiple times in the same program is undefined.

check# checks that at least the given number of bytes are currently available on the heap. This operator should be used before alloc# to ensure enough space is available.

recover# recovers at least the given number of bytes of free space in the heap. Once completed, a subsequent call to check# with the same number of bytes is guaranteed to return True#. (not yet implemented).

alloc# allocates the given number of bytes on the heap. There must be enough space available, else undefined.

read# and write# read and write a value of primitive type to a raw store address plus an offset in bytes. The effective address must be in-bounds and owned by the current process, else undefined.

peek# and poke# are similar to read# and write#, except the former work on values of the Ptr# type instead of the Addr# type.

makePtr# converts a raw store address to a pointer. This should only be done when the pointer points to a well formed object, and the current process can access the space. Pointers to Obj must only be created when they point to well formed heap objects, else undefined.

takePtr# takes the raw address of a pointer.

castPtr# casts a pointer to one of a different type. Pointers to Obj must only be created when they point to well formed heap objects, else undefined.

Last modified 3 years ago Last modified on Mar 8, 2014, 7:28:05 AM