TDF Guide

The context of usage will always determine when and how an integer is to be interpreted as a name in a particular name-space. For example, a TAG in a UNIT is constructed by make_tag applied to a TDFINT which will be interpreted as a name from that UNIT's "tag" name-space. An integer representing a name in the CAPSULE name-space would be found in a LINKEXTERN of the external_linkage parameter of make_capsule.

external_linkage: SLIST(EXTERN_LINK)

Each EXTERN_LINK is itself formed from an SLIST of LINKEXTERNs given by make_extern_link . The order of the EXTERN_LINKs determines which name-space one is dealing with; they are in the same order as given by the capsule_linkage parameter. Thus, with the capsule_linkage given above, the first EXTERN_LINK would deal with the "tag" name-space; Each of its component LINKEXTERNs constructed by make_linkextern would be identifying a tag number with some name external to the CAPSULE; for example one might be:

make_linkextern (4, string_extern("printf"))

This would mean: identify the CAPSULE's "tag" 4 with an name called "printf", external to the module. The name "printf" would be used to linkage external to the CAPSULE; any name required outside the CAPSULE would have to be linked like this.

This name "printf", of course, does not necessarily mean the C procedure in the system library. This depends both on the system context in which the CAPSULE is translated and also the meaning of the CAPSULE "tag" name 4 given by the component UNITs of the CAPSULE in the groups parameter of make_capsule:

groups: SLIST(GROUP)

Each GROUP in the groups SLIST will be formed by sets of UNITs of the same kind. Once again, there are a potentially unlimited number of kinds of UNITs but core-TDF only uses those named "tld","al_tagdefs", "tagdecs", "tagdefs", "tokdecs" and "tokdefs" ^[2] These names will appear (in the same order as in groups) in the prop_names parameter of make_capsule, one for each kind of UNIT appearing in the CAPSULE:

prop_names: SLIST(TDFIDENT)

Thus if:

prop_names = ("tagdecs", "tagdefs")

then, the first element of groups would contain only "tagdecs" UNITs and and the second would contain only "tagdefs" UNITs. A "tagdecs" UNIT contains things rather like a set of global identifier declarations in C, while a "tagdefs" UNIT is like a set of global definitions of identifiers.

Now we come to the construction of UNITs using make_unit, as in the diagram below

Figure 2.2. make_quit Diagram

First we give the limits of the various name-spaces local to the UNIT in the local_vars parameter:

local_vars: SLIST(TDFINT)

Just in the same way as with external_linkage, the numbers in local_vars correspond (in the same order) to the spaces indicated in capsule_linking in Section 2.1, “make_capsule and name-spaces” . With our example,the first element of local_vars gives the number of "tag" names local to the UNIT, the second gives the number of "token" names local to the UNIT etc. These will include all the names used in the body of the UNIT. Each declaration of a TAG, for example, will use a new number from the "tag" name-space; there is no hiding or reuse of names within a UNIT.

Connections between the CAPSULE name-spaces and the UNIT name-spaces are made by LINKs in the lks parameter of make_unit:

lks: SLIST(LINKS)

Once again, lks is effectively indexed by the kind of name-space a. Each LINKS is an SLIST of LINKs each of which which establish an identity between names in the CAPSULE name-space and names in the UNIT name-space. Thus if the first element of lks contains:

make_link(42, 4)

then, the UNIT "tag" 42 is identical to the CAPSULE "tag" 4.

Note that names from the CAPSULE name-space only arise in two places, LINKs and LINK_EXTERNs. Every other use of names are derived from some UNIT name-space.

Only names introduced by AL_TAGDEFS, TAGDEFS, TAGDECs, TOKDECs and TOKDEFs can be used in other UNITs (and then, only via the lks parameters of the UNITs involved). You can regard them as being similar to C global declarations. Token definitions include their declarations implicitly; however this is not true of tags. This means that any CAPSULE which uses or defines a tag across UNITs must include a TAGDEC for that tag in its "tagdecs" UNITs. A TAGDEC is constructed using either make_id_tagdec , make_var_tagdec or common_tagdec, all with the same form:

t_intro:   TDFINT
acc:       OPTION(ACCESS)
signature: OPTION(STRING)
x:         SHAPE
           → TAGDEC

Here the tagname is given by t_intro; the SHAPE x will defined the space and alignment required for the tag (this is analogous to the type in a C declaration). The acc field will define certain properties of the tag not implicit in its SHAPE; I shall return to the kinds of properties envisaged in discussing local declarations in Section 4.3, “Defining and using locals” .

Most program will appear in the "tagdefs" UNITs - they will include the definitions of the procedures of the program which in turn will include local definitions of tags for the locals of the procedures.

The standard TDF linker allows one to link CAPSULEs together using the name identifications given in the LINKEXTERNs, perhaps hiding some of them in the final CAPSULE. It does this just by generating a new CAPSULE name-space, grouping together component UNITs of the same kind and replacing their lks parameters with values derived from the new CAPSULE name-space without changing the UNITs' name-spaces or their props parameters. The operation of grouping together UNITs is effectively assumed to be associative, commutative and idempotent e.g. if the same tag is declared in two capsules it is assumed to be the same thing . It also means that there is no implied order of evaluation of UNITs or of their component TAGDEFs

Different languages have different conventions for deciding how programs are actually run. For example, C requires the presence of a suitably defined "main" procedure; this is usually enforced by requiring the system ld utility to bind the name "main" along with the definitions of any library values required. Otherwise, the C conventions are met by standard TDF linking. Other languages have more stringent requirements. For example, C++ requires dynamic initialisation of globals, using initial_value. As the only runnable code in TDF is in procedures, C++ would probably require an additional linking phase to construct a "main" procedure which calls the initialisation procedures of each CAPSULE involved if the system linker did not provide suitable C++ linking.

The signature arguments of TAGDEFs and TAGDECs are designed to allow a measure of cross-UNIT checking when linking independently compiled CAPSULEs. Suppose that we have a tag, t, used in one CAPSULE and defined in another; the first CAPSULE would have to have a TAGDEC for t whose TAGDEF is in the second. The signature STRING of both could be arranged to represent the language-specific type of t as understood at compilation-time. Clearly, when the CAPSULEs are linked the types must be identical and hence their STRING representation must be the same - a translator will reject any attempt to link definitions and declarations of the same object with different signatures.

Similar considerations apply to TOKDEFs and TOKDECs; the "type" of a TOKEN may not have any familiar analogue in most HLLs, but the principle remains the same.

The SORT STRING is used in various constructs other than declarations and definitions. It is a first-class SORT with string_apply_token and string_cond. A primitive STRING is constructed from a TDFSTRING(k,n) which is an encoding of n integers,each of k bits, using make_string:

arg: TDFSTRING(k, n)
     → STRING(k, n)

STRINGs may be concatenated using concat_string:

arg1: STRING(k, n)
arg2: STRING(k,m)
      → STRING(k, n+m)

Being able to compose strings, including token applications etc, means that late-binding is possible in signature checking in definitions and declarations. This late-binding means that the representation of platform-dependent HLL types need only be fully expanded at install-time and hence the types could be expressed in their representational form on the specific platform.

Two of the SHAPE constructions are rather specialised; these are TOP and BOTTOM. The result of any expression with a TOP shape will always be discarded; examples are those produced by assign and integer_test . A BOTTOM SHAPE is produced by an expression which will leave the current flow of control e.g. goto . The significance of these SHAPEs only really impinges on the computation of the shapes of constructs which have alternative expressions as results. For example, the result of conditional is the result of one of its component expressions. In this case, the SHAPE of the result is described as the LUB of the SHAPEs of the components. This simply means that if one of the component SHAPEs is TOP then the resulting SHAPE is TOP; if one is BOTTOM then the resulting SHAPE is the SHAPE of the other; otherwise both component SHAPEs must be equal and is the resulting SHAPE. Since this operation is associative, commutative and idempotent, we can speak quite unambiguously of the LUB of several SHAPEs.

Integer values in TDF have shape INTEGER(v) where v is of SORT VARIETY. The constructor for this SHAPE is integer with a VARIETY parameter. The basic constructor for VARIETY is var_limits which has a pair of signed natural numbers as parameters giving the limits of possible values that the integer can attain. The SHAPE required for a 32 bit signed integer would be:

integer(var_limits(-231, 231-1))

while an unsigned char is:

integer(var_limits(0, 255))

A translator should represent each integer variety by an object big enough (or bigger) to contain all the possible values with limits of the VARIETY. That being said, I must confess that most current translators do not handle integers of more than the maximum given naturally by the target architecture, but this will be rectified in due course.

The other way of constructing a VARIETY is to specify the number of bits required for its 2s-complemennt representation using var_width:

signed_width: BOOL
width:        NAT
              → VARIETY

Similarly, floating point and complex numbers have shape FLOATING qualified by a FLOATING_VARIETY.

A FLOATING_VARIETY for a real number is constructed using fvar_parms:

base:             NAT
mantissa_digits:  NAT
minimum_exponent: NAT
maximum_exponent: NAT
                  → FLOATING_VARIETY

A FLOATING_VARIETY specifies the base, number of mantissa digits, and maximum and minimum exponent. Once again, it is intended that the translator will choose a representation which will contain all possible values, but in practice only those which are included in IEEE float, double and extended are actually implemented.

Complex numbers have a floating variety constructed by complex_parms which has the the same signature as fvar_parms. The representation of these numbers is likely to be a pair of real numbers each defined as if by fvar_parms with the same arguments. The real and imaginary parts of of a complex number can be extracted using real_part and imaginary_part; these could have been injected ito the complex number using make_complex or any of the complex operations. Many translators will simply transform complex numbers into COMPOUNDs consisting of two floating point numbers, transforming the complex operations into floating point operations on the fields.

A number of contiguous bits have shape BITFIELD, qualified by a BITFIELD_VARIETY (S3.4) which gives the number of bits involved and whether these bits are to be treated as signed or unsigned integers. Current translators put a maximum of 32 or 64 on the number of bits.

The representational SHAPEs of procedure values is given by PROC with constructor proc . I shall return to this in the description of the operations which use it.

The construction of the other four SHAPEs involves either existing SHAPEs or the alignments of existing SHAPEs. These are constructed by compound, nof , offset and pointer. Before describing these, we require a digression into what is meant by alignments and offsets.

The TDF abstraction of an alignment has SORT ALIGNMENT. The constructor, unite_alignments, gives the set-union of its ALIGNMENT parameters; this would correspond to taking a maximum of two real alignments in the translator.

The constructor , alignment, gives the ALIGNMENT of a given SHAPE according to the rules given in the definition. These rules effectively define the primitive ALIGNMENTs as in the ALIGNMENT column of table 3. Those for PROC, all OFFSETs and all POINTERs are constants regardless of any SHAPE qualifiers. Each of the INTERGER VARIETYs, each of the FLOATING VARIETYs and each of the BITFIELD VARIETYs have their own ALIGNMENTs. These ALIGNMENTs will be bound to values apposite to the particular platform at translate-time. The ALIGNMENT of TOP is conventionally taken to be the empty set of ALIGNMENTs (corresponding to the minimum alignment on the platform).

The alignment of a procedure parameter clearly has to include the alignment of its SHAPE; however, most ABIs will mandate a greater alignment for some SHAPEs e.g. the alignment of a byte parameter is usually defined to be on a 32-bit rather than an 8-bit boundary. The constructor, parameter_alignment, gives the ALIGNMENT of a parameter of given SHAPE.

There are several other special ALIGNMENTs.

The alignment of a code address is {code} given by code_alignment; this will be the alignment of a pointer given by make_local_lv giving the value of a label.

The other special ALIGNMENTs are considered to include all of the others, but remain distinct. They are all concerned with offsets and pointers relevant to procedure frames, procedure parameters and local allocations and are collectively known as frame alignments. These frame alignments differ from the normal alignments in that their mapping to a given architecture is rather more than just saying that it describes some n-bit boundary. For example, alloca_alignment describes the alignment of dynamic space produced by local_alloc (roughly the C alloca). Now, an ABI could specify that the alloca space is a stack disjoint from the normal procedure stack; thus manipulations of space at alloca_alignment may involve different code to space generated in other ways.

Similar considerations apply to the other special alignments, callees_alignment(b), callers_alignment(b) and locals_alignment. The first two give the alignments of the bases of the two different parameter spaces in procedures (q.v.) and locals_alignment gives the alignment of the base of locally declared tags within a procedure. The exact interpretation of these depends on how the frame stack is defined in the target ABI, e.g. does the stack grow downwards or upwards?

The final special alignment is var_param_alignment. This describes the alignment of a special kind of parameter to a procedure which can be of arbitrary length (see Section 4.1.1, “vartag, varparam” .

Alignments can also be named as AL_TAGs using make_al_tagdef. There is no corresponding make_al_tagdec since AL_TAGs are implicitly declared by their constructor, make_al_tag. The main reason for having names for alignments is to allow one to resolve the ALIGNMENTs of recursive data structures. If, for example, we have mutually recursive structures, their ALIGNMENTs are best named and given as a set of equations formed by AL_TAGDEFs. A translator can then solve these equations trivially by substitution; this is easy because the only significant operation is set-union.

Expressions which give sizes or offsets in TDF have an OFFSET SHAPE. These are always described as the difference between two pointers. Since the alignments of the objects pointed to could be different, an OFFSET is qualified by these two ALIGNMENTs. Thus an EXP OFFSET(X,Y) is the difference between an EXP POINTER(X) and an EXP POINTER(Y). In order for the alignment rules to apply, the set X of alignments must include Y. The constructor offset uses two such alignments to make an OFFSET SHAPE. However, many instances of offsets will be produced implicitly by the offset arithmetic, e.g., offset_pad:

a:    ALIGNMENT
arg1: EXP OFFSET(z, t)
      → EXP OFFSET(z ∪ a, a)

This gives the next OFFSET greater or equal to arg1 at which an object of ALIGNMENT a can be placed. It should be noted that the calculation of shapes and alignments are all translate-time activities; only EXPs should produce runnable code. This code, of course, may depend on the shapes and alignments involved; for example, offset_pad might round up arg1 to be a multiple of four bytes if a was an integer ALIGNMENT and z was a character ALIGNMENT. Translators also do extensive constant analysis, so if arg1 was a constant offset, then the round-off would be done at translate-time to produce another constant.

The constructors offset_add , offset_zero and shape_offset are used together with offset_pad to implement (inter alia) selection from structures represented by COMPOUND SHAPEs. Starting from the zero OFFSET given by offset_zero, one can construct an EXP which is the offset of a field by padding and adding offsets until the required field is reached. The value of the field required could then be extracted using component or add_to_ptr. Most producers would define a TOKEN for the EXP OFFSET of each field of a structure or union used in the program simply to reduce the size of the TDF

The SHAPE of a C structure consisting of an char followed by an int would require x to be the set consisting of two INTEGER VARIETYs, one for int and one for char, and sz would probably have been constructed like:

sz = offset_add(offset_pad(int_al, shape_offset(char)), shape_offset(int))

The various rules for the ALIGNMENT qualifiers of the OFFSETs give the required SHAPE; these rules also ensure that offset arithmetic can be implemented simply using integer arithmetic for standard architectures (see Section 12.1, “Model for a 32-bit standard architecture”). Note that the OFFSET computed here is the minimum size for the SHAPE. This would not in general be the same as the difference between successive elements of an array of these structures which would have SHAPE OFFSET(x, x) as produced by offset_pad(x, sz). For examples of the use of OFFSETs to access and create structures, see Chapter 11, TDF expansions of offsets .

In C, all structures have size known at translate-time. This means that OFFSETs for all field selections of structures and unions are translate-time constants; there is never any need to produce code to compute these sizes and offsets. Other languages (notably Ada) do have variable size structures and so sizes and offsets within these structures may have to be computed dynamically. Indexing in C will require the computation of dynamic OFFSETs; this would usually be done by using offset_mult to multiply an offset expression representing the stride by an integer expression giving the index:

arg1: EXP OFFSET(x, x)
arg2: EXP INTEGER(v)
      → EXP OFFSET(x, x)

and using add_to_ptr with a pointer expression giving the base of the array with the resulting OFFSET.

There is an ordering defined on OFFSETs with the same alignment qualifiers, as given by offset_test and offset_max having properties like:

shape_offset(S) ≥ offset_zero(alignment(S))
A ≥ B    iff offset_max(A,B) = A
offset_add(A, B) ≥ A     where B ≥ offset_zero(some compatible alignment)

In most machines, OFFSETs would be represented as single integer values with the OFFSET ordering corresponding to simple integer ordering. The offset_add constructor just translates to simple addition with offset_zero as 0 with similar correspondences for the other offset constructors. You might well ask why TDF does not simply use integers for offsets, instead of introducing the rather complex OFFSET SHAPE. The reasons are two-fold. First, following the OFFSET arithmetic rules concerned with the ALIGNMENT qualifiers will ensure that one never extracts a value from a pointer with the wrong alignment by, for example, applying contents to an add_to_pointer. This frees TDF from having to define the effect of strange operations like forming a float by taking the contents of a pointer to a character which may be mis-aligned with respect to floats - a heavy operation on most processors. The second reason is quite simple; there are machines which cannot represent OFFSETs by a single integer value.

The iAPX-432 is a fairly extreme example of such a machine; it is a "capability" machine which must segregate pointer values and non-pointer values into different spaces. On this machine a value of SHAPE POINTER({pointer, int}) (e.g. a pointer to a structure containing both integers and pointers) could have two components; one referring to the pointers and another to the integers. In general, offsets from this pointer would also have two components, one to pick out any pointer values and the other the integer values. This would obviously be the case if the original POINTER referred to an array of structures containing both pointers and integers; an offset to an element of the array would have SHAPE OFFSET({pointer, int},{pointer , int}); both elements of the offset would have to be used as displacements to the corresponding elements of the pointer to extract the structure element. The OFFSET ordering is now given by the comparison of both displacements. Using this method, one finds that pointers in store to non-pointer alignments are two words in different blocks and pointers to pointer-alignments are four words, two in one block and two in another. This sounds a very unwieldy machine compared to normal machines with linear addressing. However, who knows what similar strange machines will appear in future; the basic conflicts between security, integrity and flexibility that the iAPX-432 sought to resolve are still with us. For more on the modelling of pointers and offsets see Chapter 12, Models of the TDF algebra .

U se of the var_intro OPTION in make_proc and the corresponding varparam in apply_proc allows one to have a parameter of any SHAPE, possibly differing from call to call where the actual SHAPE can be deduced in some way by the body of the make_proc . One supplies an extra actual parameter, varparam, which usually would be a structure grouping some set of values. The body of the procedure can then access these values using the pointer given by the TAG var_intro, using add_to_ptr with some computed offsets to pick out the individual fields.

This is a slightly different method of giving a variable number of parameters to a procedure, rather than simply giving more actuals than formals. The principle difference is in the alignment of the components of varparam; these will be laid out according to the default padding defined by the component shapes. In most ABIs, this padding is usually different to the way parameters are laid out; for example, character parameters are generally padded out to a full word. Thus a sequence of parameters of given shape has a different layout in store to the same sequence of shapes in a structure. If one wished to pass an arbitrary structure to a procedure, one would use the varparam option rather passing the fields individually as extra actual parameters.

Often the result of a procedure, f, is simply given by the call of another (or the same) procedure, g. In appropriate circumstances, the same stack space can be used for the call of g as the call of f. This can be particularly important where heavily recursive routines are involved; some languages even use tail recursion as the preferred method of looping.

One condition for such a tail call to be applicable is knowing that g does not require any pointers to locals of f; this is often implicit in the language involved. Equally important is that the action on the return from f is indistiguishable from the return from g. For example, if it were the callers responsibility to pop the the space for the parameters on return from a call, then the tail call of g would only work if g had the same parameter space as f.

This is the justification for splitting the parameter set of a general proc; it is (at least conceptually) the caller's responsibility for popping the caller-parameters only - the callee-parameters are dealt with by the procedure itself. Hence we can define tail_call which uses the same caller-parameters, but a different set of callee-parameters:

prcprops:      OPTION(PROCPROPS)
p:             EXP PROC
callee_params: CALLEES
               → EXP BOTTOM

The procedure p will be called with the same caller parameters as the current procedure and the new callee_params and return to the call site of the current procedure. Semantically, if S is the return SHAPE of the current procedure, and L is its caller-parameters:

tail_call(P, p, C) = return(apply_general_proc(S, P, p, L, C, make_top()))

However an implementation is expected to conserve stack by using the same space for the call of p as the current procedure.

The presence of var_callees (or var_callers) means that the procedure can be called with more actual callee (or caller) parameters than are indicated in callee_intro (or caller_intro). These extra parameters would be accessed within body using offset calculations with respect to the named parameters. The offsets should be calculated using parameter_alignment to give the packing of the parameter packs.

The presence of untidy means that body may be terminated by an untidy_return. This returns the result of the procedure as in return, but the lifetime of the local space of the procedure is extended (in practice this is performed by not returning the stack to its original value at the call). A procedure containing an untidy_return is a generalisation of a local_alloc(see Section 4.3.4, “local_alloc, local_free_all, last_local”). For example the procedure could do some complicated local allocation (a triangular array, say) and untidily return a pointer to it so that the space is still valid in the calling procedure. The space will remain valid for the lifetime of the calling procedure unless some local_free is called within it, just as if the space had been generated by a local_alloc in the calling procedure.

The presence of inline is just a hint to the translator that the procedure body is a good candidate for inlining at the call.

The presence of check_stack means that the static stack requirements of the procedure will be checked on entry to see that they do not exceed the limits imposed by set_stack_limit; if they are exceeded a TDF exception with ERROR_CODE stack_overflow (see Section 5.3, “Exceptional flow”) will be raised.

Local definitions within the body of a procedure are given by two EXP constructors which permit one to give names to values over a scope given by the definition. Note that this is somewhat different to declarations in standard languages where the declaration is usually embedded in a larger construct which defines the scope of the name; here the scope is explicit in the definition. The reason for this will become more obvious in the discussion of TDF transformations. The simpler constructor is identify:

opt_access: OPTION(ACCESS)
name_intro: TAG x
definition: EXP x
body:       EXP y
            → EXP y

The definition is evaluated and its result is identified with the TAG given by name_intro within its scope body. Hence the use of any obtain_tag(name_intro) within body is equivalent to using this result. Anywhere else, obtain_tag(name_intro) is meaningless, including in other procedures.

The other kind of local definition is variable:

opt_access: OPTION(ACCESS)
name_intro: TAG x
init:       EXP x
body:       EXP y
            → EXP y

Here the init EXP is evaluated and its result serves as an initialisation of space of SHAPE x local to the procedure. The TAG name_intro is then identified with a pointer to that SPACE within body. A use of obtain_tag(name_intro) within body is equivalent to using this pointer and is meaningless outside body or in other procedures. Many variable declarations in programs are uninitialised; in this case, the init argument could be provided by make_value which will produce some value with SHAPE given by its parameter.

The ACCESS SORT given in tag declarations is a way of describing a list of properties to be associated with the tag. They are basically divided into two classes, one which describes global properties of the tag with respect to the model for locals and the other which gives "hints" on how the value will be used. Any of these can be combined using add_access.

The constructor current_env gives a pointer to the current procedure frame of SHAPE POINTER(fa) where fa is depends on how the procedure was defined and will be some set of the special frame ALIGNMENTs. This set will always include locals_alignment - the alignment of any locals defined within the procedure. If the procedure has any caller- parameters, the set will also include callers_alignment(b) where b indicates whether there can be a variable number of them; similarly for callee-parameters.

Offsets from the current_env of a procedure to a tag declared in the procedure are constructed by env_offset:

fa: ALIGNMENT
y:  ALIGNMENT
t:  TAG x
    → EXP OFFSET(fa,y)

The frame ALIGNMENT fa will be the appropriate one for the TAG t; i.e. if t is a local then the fa will be locals_alignment; if t is a caller parameter, fa will be callers_alignment(b); if t is a callee_parameter, fa will be callees_alignment(b). The alignment y will be the alignment of the initialisation of t.

The offset arithmetic operations allow one to access the values of tags non-locally using values derived from current_env and env_offset. They are effectively defined by the following identities:

If TAG t is derived from a variable definition:

add_to_ptr(current_env(), env_offset(locals_alignment, A, t)) = obtain_tag(t)

if TAG t is derived from an identify definition:

contents(S, add_to_ptr(current_env(), env_offset(locals_alignment, A, t))) = obtain_tag(t)

if TAG t is derived from a caller parameter:

add_to_ptr(current_env(), env_offset(callers_alignment(b), A, t)) = obtain_tag(t)

if TAG t is derived from a callee parameter:

add_to_ptr(current_env(), env_offset(callees_alignment(b), A, t)) = obtain_tag(t)

These identities are valid throughout the extent of t, including in inner procedure calls. In other words, one can dynamically create a pointer to the value by composing current_env and env_offset.

The importance of this is that env_offset(t) is a constant OFFSET and can be used anywhere within the enclosing UNIT, in other procedures or as part of constant TAGDEF; remember that the TDFINT underlying t is unique within the UNIT. The result of a current_env could be passed to another procedure (as a parameter, say) and this new procedure could then access a local of the original by using its env_offset. This would be the method one would use to access non-local, non-global identifiers in a language which allowed one to define procedures within procedures such as Pascal or Algol. Of course, given the stack-based model, the value given by current_env becomes meaningless once the procedure in which it is invoked is exited.

The size of stack frame produced by variable and identify definitions is a translate-time constant since the frame is composed of values whose SHAPEs are known. TDF also allows one to produce dynamically sized local objects which are conceptually part of the frame. These are produced by local_alloc:

arg1: EXP OFFSET(x, y)
      → EXP POINTER(alloca_alignment)

The operand arg1 gives the size of the new object required and the result is a pointer to the space for this object "on top of the stack" as part of the frame. The quotation marks indicate that a translator writer might prefer to maintain a dynamic stack as well as static one. There are some disadvantages in putting everything into one stack which may well out-weigh the trouble of maintaining another stack which is relatively infrequently used. If a frame has a known size, then all addressing of locals can be done using a stack-front register; if it is dynamically sized, then another frame-pointer register must be used - some ABIs make this easy but not all. The majority of procedures contain no local_allocs, so their addressing of locals can always be done relative to a stack-front; only the others have to use another register for a frame pointer.

The alignment of pointer result is alloca_alignment which must include all SHAPE alignments.

There are two constructors for releasing space generated by local_alloc. To release all such space generated in the current procedure one does local_free_all(); this reduces the size of the current frame to its static size.

The other constructor is local_free whch is effectively a "pop" to local_alloc's "push":

a: EXP OFFSET(x, y)
p: EXP POINTER(alloca_alignment)
   → EXP TOP

Here p must evaluate to a pointer generated either by local_alloc or last_local . The effect is to free all of the space locally allocated after p. The usual implementation (with a downward growing stack) of this is that p becomes the "top of stack" pointer

The use of a procedure with an untidy_return is just a generalisation of the idea of local_alloc and the space made available by its use can be freed in the same way as normal local allocations. Of course, given that it could be the result of the procedure it can be structured in an arbitrarily complicated way.

To perform a sequential set of operations in TDF, one uses the constructor sequence:

statements: LIST(EXP)
result:     EXP x
            → EXP x

Each of the statements are evaluated in order, throwing away their results. Then, result is evaluated and its result is the result of the sequence.

A translator is free to rearrange the order of evaluation if there is no observable difference other than in time or space. This applies anywhere I say "something is evaluated and then ...". We find this kind of statement in definitions of local variables in Section 4.3, “Defining and using locals” , and in the controlling parts of the conditional constructions below.

For a more precise discussion of allowable reorderings see (S7.14) .

All simple changes of flow of control within a TDF procedure are done by jumps or branches to LABELs, mirroring what actually happens in most computers. There are three constructors which introduce LABELs; the most general is labelled which allows arbitrary jumping between its component EXPs:

placelabs_intro: LIST(LABEL)
starter:         EXP x
places:          LIST(EXP)
                 → EXP w

Each of the EXPs in places is labelled by the corresponding LABEL in placelabs_intro; these LABELs are constructed by make_label applied to a TDFINT uniquely drawn from the LABEL name-space introduced by the enclosing PROPS. The evaluation starts by evaluating starter; if this runs to completion the result of the labelled is the result of starter. If there is some jump to a LABEL in placelabs_intro then control passes to the corresponding EXP in places and so on. If any of these EXPS runs to completion then its result is the result of the labelled; hence the SHAPE of the result, w, is the LUB of the SHAPEs of the component EXPs.