2.4.1 Integer Literals

The general form of an integer literal is:

[-][baser]digits

where base is radix of the subsequent digits expressed in decimal form. Legal bases are 2, 8, 10, and 16. In the absence of a base prefix, the digits are interpreted as base ten. The digits are selected from the characters

0 1 2 3 4 5 6 7 8 9 a b c d e f

with the customary hexadecimal valuations. The letters may appear in either lowercase or uppercase. It is an error for a digit to be present whose value as a digit is greater than or equal to the specified base.

Integer literals of a particular fixed-precision type may be written by using a type qualifier. The expression:

564 : uint32

specifies an unsigned 32 bit quantity whose value is 564. It is a compile-time error to qualify an integer literal with a type that is incapable of representing the literal's value. In the absence of explicit qualification, the type assigned to an integer literal will be some subset of:

int8  int16  int32  int64
uint8 uint16 uint32 uint64
word

Any concrete type that cannot represent the literal value will be omitted from the set of types assigned.¹

2.4.2 Floating Point Literals

The general form of a floating point literal is:

[-][baser]digits.digits[^exponent]

where base defines the decimal encoded radix of the digits and exponent is an integer literal, possibly including an initial minus sign and a radix specification for the exponent part. Digits are selected as for integer literals, above. Note that the decimal point is not optional, and must have digits on both sides. Thus, 0.0 is a valid floating point literal, but 0. and .0 are not.

As with integer literals, floating point literals of an explicitly stated representation type may be written using a type qualifier. The expression:

0.0 : float

specifies a 32-bit (single precision) IEEE floating point quantity whose value is zero. As with integer literals, it is a compile-time error to specify a value cannot be represented within the representable range of the qualifying type.² In the absence of explicit qualification, the type of a floating point literal is some subset of:

float double quad

Any concrete type whose representable range cannot express the literal value will be omitted from the assigned set.

Conversion of a floating point literal to internal representation follows the customary IEEE floating point rounding rules when the specified literal cannot be exactly represented.³

2.4.3 Character Literals

BitC uses the Unicode character set as defined in version 4.1.0 of the Unicode standard [13]. Characters are 32 bits wide. Character literals can be expressed in two ways.

A character literal may be written as

#\printable-character

Where printable-character is any character specified in the Unicode 4.1.0 standard except those with general categories "Cc" (control codes) "Cf" (format controls), "Cs" (surrogates), "Cn" (unassigned), or "Z" (separators). That is, any printable character, excluding spaces. Notwithstanding the listed Unicode categories, the characters ``{'' (U+007B, left curly brace) and ``}'' (U+007D, right curly brace) are excluded for use in character literal escaping. Notwithstanding the previously listed Unicode categories, the following characters are considered printable characters as well:

! " # $ % & ' ( ) * + , - . / :
{ } ; < = > ? @ [ \ ] ^ _ ` | ~

A character may also be specified by its unicode code point:

#\U+digits

Where digits are hexidecimal.

Certain commonly used non-printing characters have convenience representations as character literals:

#\space
#\linefeed
#\return
#\tab
#\backspace
#\lbrace
#\rbrace

2.4.4 String Literals

BitC strings are written within double quotes, and may contain the previously listed ``printable characters'' excluding backslash (``\''), but including (``{'') and (``}''). They may also contain spaces (U+0020), left curly brace (U+007B) and right curly brace (U+007D).

Within a string, the backslash character (``\'') is interpreted as beginning an encoding of a specially embedded character. The character following the ``\'' is either a single-character embedding or a curly brace character ``{'' identifying the start of a Unicode character embedding. The legal forms and their meanings are:

2.5.1 Definitions and Declarations

The top level forms that introduce programmatic definitions and declarations are:

define    definstance  defrepr
defstruct deftypeclass defunion  
proclaim
use

The define, defunion, defrepr, and defstruct forms support simple recursion. That is, the identifier(s) being defined may be used in their definition. However, the identifier(s) being defined are deemed incomplete until the end of the enclosing defining form. Restrictions on the use of incomplete identifiers are described in the sections on types and value binding.

The proclaim form is used to provide opaque value declarations. The identifier declared by a proclaim form is considered incomplete. If a completing definition is later provided within the same compilation unit, the identifier is considered complete in the balance of the defining compilation unit after the the close of its defining form. An incomplete declaration may be used within a procedure, but may not be used as part of a top-level initializer (see define, Section 5.2).

The use form is used to provide an alternative identifier that is equivalent in all respects to some existing top-level identifier.

All definition forms are expressions that return a value of type unit.

3.4.1 Reference Types

If T is a value type, then

(ref T)

is the type of a reference denoting a heap-allocated instance of T.

Storage Layout    The representation of a ref instance is architecture dependent. It is customarily determined by the size of the machine's integer registers, and aligned at any address that is congruent mod 0 to the integer register size.

3.4.2 Function Types

If t_arg and t_result are types (including type variables), then:

(fn targ tresult)

is the type of a function taking a single argument of type t_arg and returning a value of type t_result.

Function types are considered reference types that denote an object of statically undefined size. The size and alignment of a value of function type is determined by the underlying processor architecture.

3.5.1 Arrays

An array is a value type whose value is a fixed product type T^i>0, all of whose elements are of common type. The type:

(array T i)

describes the type of fixed-length arrays of element type T and length i, where i is an integer literal of type word that is greater than zero.

Storage Layout    The value representation of a k-element array is laid out in memory as the concatenation of k contiguous element cells whose size and alignment are determined by their respective element types. The elements of the array appear at increasing addresses in order from left to right.

3.5.2 Vectors

A vector is a dynamically sized array whose elements are of type T. Vectors are reference types. Because they are dynamically sized, there is no corresponding value type. The type:

(vector T)

describes vectors of element type T.

3.6.1 Structures

The structure declaration defines a named type whose instances are an ordered sequence of named cells. The syntax of a structure declaration is:

(defstruct nm field ...)
(defstruct (nm tv1 ... tvn) field ...)

where each field is one of:

nm:type
(the type nm)
(fill bitfield-type)

All names nm are disjoint identifiers giving the names of the structure fields, and the respective type forms are the types of the respective fields. Given a variable v that is an instance of a structure type having a field named f, the expression v.f unifies with the field f within that structure.

A fill element may be used to support precise specification of alignment. The alignment and storage layout of a fill field follows the alignment and storage layout of its base type, however a fill field has no name or defined value, and cannot be programatically referenced.

An identifier that is bound to a structure type may be used as a procedure to instantiate new values of that structure type. The arguments to this procedure are the initial values of the respective structure fields.

An identifier that is bound to a non-parameterized structure type may be used as a type name. An identifier that is bound to a parameterized structure type may be used in a type constructor application within a type specification. Its arguments are the types over which the newly instantiated structure type should be instantiated. For example, the declarations:

(defstruct ipair a:int32 b:int32)

(defstruct (tree-of 'a):ref
  left : (optional (tree-of 'a))
  right : (optional (tree-of 'a))
  height : int8
  value : 'a)

define (respectively) the type name ipair and the single argument type constructor tree-of.

3.6.2 Unions

The defunion form defines enumerations, discriminated unions, and mixes of these. The type being defined is in-scope within the definition of the type, but is incompletely defined. The syntax of a union declaration is one of:

(defunion nm C1 ... Cn)
(defunion (nm tv1 ... tvn)
  C1 ... Cn)

where each tv_i is a type variable and C_i is a constructor form. A constructor form consists of either a single identifier or a parenthesized identifier followed by a sequence of field or fill declarations (see defstruct). All field names appearing in a defunion, including constructor names, must be disjoint.

An identifier bound to a union constructor having no fields denotes the value of the unique corresponding union instance for that union type.

An identifier bound to a union constructor having associated fields is a procedure that may be used to instantiate new instances of that union type. The arguments to this procedure are the initial values of the union fields associated with that union variant.

An identifier that is bound to a non-parameterized union type is a valid type name. An identifier that is bound to a paramterized union type may be used in a type constructor application within a type specification. Its arguments are the types over which the newly instantiated structure type should be instantiated. For example, the declarations:

(defunion contrived
  (asChar c:char) (asInt i:int32))

(defunion (optional 'a) :val
  none
  (some value:'a))

define (respectively) a reference type holding either a char or an int32, and a value type of optional elements.

The declaration:

(defunion (list 'a):ref
  nil
  (cons car:'a cdr:(list 'a)))

Defines the reference type of homogeneous lists.

(defunion (list 'a):ref
  (declare (tag-type uint8))
  nil
  (cons car:'a cdr:(list 'a)))

3.6.3 Reprs

There are examples of low-level hardware data structures for which the unions and structures that can be specified using defstruct or defunion are insufficiently expressive. One example is the Pentium GDT data structure, which has nested union discriminators, but simultaneously has an overall bit-level layout requirement. Another example is data structures where the representation of the tag must appear at a specific location that is not adjacent to the fields guarded by the tag. The defrepr form is included to permit the expression of these data structures.

The following scheme for defrepr is based on the bit-data representation proposed by Iavor Diatchki, et. al. [11].

Similar to unions and structures, a defrepr delaration takes the following form:

(defrepr name
  (Ctr1 f11:type f21:type ... fn1:type
    (where (= fp1 v11) (= fq1 v21) ...
           (= fm1 vm1))

  (Ctr2 f12:type f22:type ... fn2:type
    (where (= fp2 v12) (= fq2 v22) ... 
           (= fm2 vm2))

  ... )

The following restrictions apply. For all constructors Ctrx, Ctry, Ctrz, ...:

• All fields fpx, fqx...fmx appearing in the when clause of a constructor form Ctrx must be described within the body of Ctrx. That is, {fpx, fqx, ... fmx} ⊆ {f1x, ... fnx}.

• Identically named fields within two different constructor forms must be located at the same bit level offset from the beginning of both the constructor forms. That is, fpx = fpy implies bit-offset(fpx) = bit-offset(fpy).

• Identically named fields within two different constructor must have the same type. That is, fpx = fpy implies type-of(fpx) = type-of(fpy).

• The fields within the when clauses of all constructor forms must uniquely distinguish all constructible values of the union. The compiler will not introduce any more tag bits for a defrepr value.

• Currently, the defrepr form will not accept type arguments over which it can be instantiated. That is, the following definition is not legal.

  (defrepr (name 'a 'b ... ) ... )

• Currently, the discriminating fields fp1, fp2, etc must have a integer/bitfield type, and the discriminator values v11, v12, etc must be an integer literal.

We can envision a larger language construct DEFUNION, which accepts both type arguments and when clauses. The defunion and defrepr are just specializations of this DEFUNION construct. However, currently the language only supports defunion (which does not accept the when clause) and defrepr (which does not accept type arguments).

3.6.4 Value vs. Reference Types

In the absence of other specification, the defstruct, defrepr, and defunion forms declare reference types. The developer may optionally qualify the declaration to make this intention explicit:

(defstruct nm:ref field ...)
(defstruct (nm tv1 ... tvn):ref
  field ...)
(defunion nm:ref C1 ... Cn)
(defunion (nm tv1 ... tvn):ref
  C1 ... Cn)
(defrepr nm:ref (body))
(defrepr (nm tv1 ... tvn):ref (body))

The qualifier ``:ref'' indicates that the type declared (and consequently the type returned by value constructors) is a reference type. The qualifier ``:val'' indicates that the type declared is a value type. The qualifier ``:opaque'' indicates that the type declared is a value type whose internal structure is not accessable outside of the defining interface and the providers of that interface. An importer of an opaque type may declare fields and variables of that type and can copy instances of that type, but can neither apply the type constructors nor make reference to the contents of instances.

Note that if the type declared is a value type, it cannot be instantiated within the body of the declaration because its size is not statically known. That is, it is legal to have a field that is a reference to a value of the type currently being defined, but not a value of that type.

3.6.5 Forward Declarations

The declarations

(defstruct nm [qual] [external])
(defunion nm [qual] [external])
(defrepr nm [qual] [external])
(defstruct (nm tv1 ... tvn) 
          [qual] [external])
(defunion (nm tv1 ... tvn)
          [qual] [external])
(defrepr (nm tv1 ... tvn)
          [qual] [external])

state (respectively) that nm is a structure (respectively union) reference type of the stated arity whose internal structure is not disclosed. If present, the qualifier qual optionally declares the type to be one of ``:ref'', ``:val'', or ``:opaque''. In the absence of qualification, the default is ``:ref''. If present, the external portion consists of the keyword external followed by an optional identifier (see discussion of external identifiers in proclaim).

For example, the following declaration is include in the library bitc.int interface to declare the bignum type:

(defstruct int :val external bitc_int)

The structure of these types may optionally be disclosed later in the same compilation unit by a type definition for nm. If the declaring form appears within an interface, the corresponding type definition may appear in a providing unit of compilation, in which case the type is opaque to importers of the interface.

Note that a forward declaration of a value type is sufficient to declare references to that type, but not instances of that type. A complete definition of the value type is required to be in scope in order to declare fields and variables of value type.

3.6.6 Named Type Conveniences

The following types are defined in the BitC standard prelude.

(defstruct (pair 'a 'b) :val
   fst:'a snd:'b)

(defunion (list 'a) :ref
   nil
   (cons 'a (list 'a)))

Note that pair is a keyword that is specially recognized in binding patterns.

The pair type is supported by a right-associative infix convenience syntax:

(a, b) => (pair a b)
(a, b, c) => (pair a (pair b c))

This convenience syntax may be used in types, binding patterns, and value construction.

4.1.1 Example: Eql

As a first example, consider the equality comparison operations. The type class Eql defines a single element type relation on types 'a: describing whether the type is admissable under equality. Some types — notably function types — cannot be compared for equality. The definition of this type class is written:

(deftypeclass (Eql 'a)
  == : (fn ('a 'a) bool))
  != : (fn ('a 'a) bool))

which states that Eq. is the single element type relation over all types 'a that can be passed as arguments to == and !=.

4.1.2 Qualification: Ord

A type class can also be introduced in qualified form. The syntax for such a type class definition is:

(deftypeclass 
  (forall (constraint ... constraint)
     (nm tv ... tv))
  [tyfn-declarations]
  method-definitions)

where each constraint takes the form:

(tc-name tv ... tv)

where tc-name is a typeclass name. An example of this use is the Ord type class:

(deftypeclass 
  (forall ((Eql 'a)) (Ord 'a))
  < : (fn ('a 'a) 'a))

This type class states that Ord is the single element type relation over all types 'a that can be passed as arguments to <. It also states that the Ord relation is only defined for types that are also members of the Eql relation (that is: types that admit equality comparison).

Note that in the presence of this definition, the procedures >, <=, and >= can be defined as:

(define (> x y)
  (not (or (< x y) (== x y)))
(define (<= x y)
  (or (< x y) (== x y)))
(define (>= x y)
  (or (> x y) (== x y)))

all of which will be inferred to have the type:

(forall ((Ord 'a)) (fn ('a 'a) bool))

This may seem like a very long-winded way of saying that an orderable type is any type that can be passed to the operators < and ==. However, type classes are statements about relations among types. This may become clearer with the following example.

Note that because (Ord 'a) has (Eql 'a), the types:

(forall ((Ord 'a) (Eql 'a))
        (fn ('a 'a) bool))
(forall ((Ord 'a)) (fn ('a 'a) bool))

are equivalent. The second is stylistically preferred for reasons of brevity. It is also more robust: in the (in this example unlikely) event that the definition of Ord should be modified to depend on some other type class in place of Eql the future, the first definition will mistakenly retain an additional, unncessary type dependency, while the second will continue to type check as intended.

Restriction: Qualified type relationships must be acyclic.

4.1.3 Example: tyfn

Need an example of type functions.

5.3.1 let

The let form provides a mechanism for locally binding identifiers to the result of an expression evaluation. Each identifier bound in a let form must appear exactly once among the collection of binding patterns being bound. Evaluation of the initialization expressions occurs in order from e₁ to e_n. The environment in which the expression(s) are evaluated does not contain the identifiers being bound in the current let form.

The syntax of let is:

(let ((bp1 e1)
      ...
      (bpn en))
  ebody-1
  ...
  ebody-n)

One common form of these expressions is the one in which the left hand patterns are simple identifier names, as in:

(let ((x e1)
      ...
      (y e2))
  ; x, y are bound in:
  ebody-1
  ...
  ebody-n)

The value of a let form is the value of the last form executed within the body.

In similar languages, let is often presented as a form derived from lamdba. In BitC, as in other let-polymorphic languages, the value restriction for lambda arguments means that this is not (quite) true.

5.3.2 letrec

The letrec form provides a mechanism for locally binding identifiers to an expression value. Each identifier bound in a letrec form must appear exactly once among the collection of binding patterns being bound. Evaluation of the initialization expressions occurs in order from e₁ to e_n. The environment in which the expression(s) are evaluated contains (via unification) the identifiers being bound in the current letrec form. This allows letrec to bind recursive procedure definitions:

(letrec
  ((odd
     (lambda (x) ; odd
       (cond ((= x 0) #f)
             ((< x 0) (odd (- x)))
             (otherwise
               (not
                 (even (- x 1)))))))
   (even
     (lambda (x) ; even
       (cond ((= x 0) #t)
             ((< x 0) (even (- x)))
             (otherwise
               (not
                 (odd (- x 1))))))))
  body)

The value of a let form is the value of the last form executed within the body.

Within the defining expressions of a letrec form, use of the identifiers being defined is subject to the same restrictions described for define. This ensures that cyclical constant data cannot be introduced.⁷

Any binding pattern appearing in the bp_i position in a letrec must be statically decomposable at compile time. It is not sufficient that the corresponding e_i be of compatible type. This restriction allows the binding patterns to be flattened away by the compiler without internally violating the completeness restriction.⁸

5.3.3 local define

The define form may be used in an expression sequence, provided it is not the last form of the expression sequence. In this context, define is a derived form. The canonical rewriting of the local define form using core language constructs is:

(begin ...
  (define id edef) e2 [...]) =>
(begin ...
  (letrec ((id edef))
    e2 [...]))

This rewrite proceeds left to right. Successive defines are gathered into letrec forms that are progressively more deeply nested. Adjacent define forms are not gathered into a single letrec body.

7.4.1 unit

The expression:

()

denotes the singleton unit value.

7.4.2 make-vector

The expression:

(make-vector elen einit)

creates a new vector whose length is determined by the value of the expression e_len, which must evaluate to a value of type word. The argument e_init must be a function from word to some type T, where the vector created will be of type (vector T). The initializer value for each cell will be obtained by invoking the procedure e_init a total of e_len times, passing as an argument the index of the vector position to be initialized. The procedure e_init should return the desired initializer value for the corresponding position.

For example, the procedure list->vector may be written as:

(import ls bitc.list)
(define (list->vector lst)
  (make-vector
    (length lst)
    (lambda (n)
       (ls.list-nth lst n))))

Care should be taken to ensure that the type returned by the initializer function is mutable if the slots of the vector are intended to be mutable.

7.4.3 array, vector

The expressions:

(array e0 ... en)
(vector e0 ... en)

create a new array (respectively, vector) whose length is determined by number of arguments. The first argument expression becomes the first cell of the created array (respectively, vector), the second becomes the second, and so forth. All expressions must be of like type.

7.4.4 Convenience Syntax

Derived forms

The following are right-associative convenience syntax for types defined in the standard prelude:

(a,b) => (pair a b)
(a,b,c) => (pair a (pair b c))

[]    => nil
[a] => (cons a nil)
[a,b] => (cons a (cons b nil))

7.10.1 array-length, vector-length

If e is an expression of array (respectively: vector) type, then

(array-length e)
(vector-length e)

returns a word whose value is the number of elements in the array.

7.10.2 array-nth, vector-nth

If e is an expression of array (respectively: vector) type, and e_i is an expression with result type word, then:

(array-nth eloc ei)
(vector-nth e ei)

are (respectively) expressions that return the e_i'th element of the array (respectively: vector). If the value e_i is greater than or equal to the length of the array (respectively: vector), then a IndexBoundsError exception is thrown.

array-nth and vector-nth are syntactic forms. The returned value is a location, and can be used as an argument to set!. array-nth requires a location as its argument.

The expression:

e[ei]

is a convenience shorthand for

(vector-nth e ei)

7.11.1 Reference Parameters