TDF Specification

token_value: TOKEN
token_args:  BITSTREAM param_sorts(token_value)
             → ACCESS

The token is applied to the arguments encoded in the BITSTREAM token_args to give an ACCESS.

The notation param_sorts(token_value) is intended to mean the following. The token definition or token declaration for token_value gives the SORTs of its arguments in the SORTNAME component. The BITSTREAM in token_args consists of these SORTs in the given order. If no token declaration or definition exists in the CAPSULE, the BITSTREAM cannot be read.

control: EXP INTEGER(v)
e1:      BITSTREAM ACCESS
e2:      BITSTREAM ACCESS
         → ACCESS

control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.

a1: ACCESS
a2: ACCESS
    → ACCESS

A construction qualified with add_accesses has both ACCESS properties a1 and a2. This operation is associative and commutative.

→ ACCESS

Only a variable (not an identity) may be qualified with constant. A variable qualified with constant will retain its initialising value unchanged throughout its lifetime.

→ ACCESS

An object must also have this property if it is to have a defined value when a long_jump returns to the procedure declaring the object.

→ ACCESS

This property refers to a POINTER, p. It says that, within the lifetime of the declaration being qualified, there are no contents, contents_with_mode or move_some source accesses to any pointer not derived from p which overlap with any of the contents, contents_with_mode, assign, assign_with_mode or move_some accesses to pointers derived from p.

The POINTER being described is that obtained by applying obtain_tag to the TAG of the declaration. If the declaration is an identity, the SHAPE of the TAG will be a POINTER.

→ ACCESS

This property refers to a POINTER, p. It says that, within the lifetime of the declaration being qualified, there are no assign, assign_with_mode or move_some destination accesses to any pointer not derived from p which overlap with any of the contents, contents_with_mode, assign, assign_with_mode or move_some accesses to pointers derived from p.

The POINTER being described is that obtained by applying obtain_tag to the TAG of the declaration. If the declaration is an identity, the SHAPE of the TAG will be a POINTER.

→ ACCESS

An object qualified by out_par will be an output parameter in a make_general_proc construct. This will indicate that the final value of the parameter is required in postlude part of an apply_general_proc of this procedure.

→ ACCESS

This property refers to a global object. It says that the object will be included in the final program, whether or not all possible accesses to that object are optimised away; for example by inlining all possible uses of procedure object.

→ ACCESS

Indicates that an object with this property is frequently used. This can be taken as a recommendation to place it in a register.

→ ACCESS

An object qualified as having standard_access has normal (i.e. no special) access properties.

→ ACCESS

An object qualified as having used_as_volatile will be used in a move_some, contents_with_mode or an assign_with_mode construct with TRANSFER_MODE volatile.

→ ACCESS

An object qualified as visible may be accessed when the procedure in which it is declared is not the current procedure. A TAG must have this property if it is to be used by env_offset.

token_value: TOKEN
token_args:  BITSTREAM param_sorts(token_value)
             → AL_TAG

The token is applied to the arguments encoded in the BITSTREAM token_args to give an AL_TAG.

If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.

al_tagno: TDFINT
          → AL_TAG

make_al_tag constructs an AL_TAG identified by al_tagno.

t: TDFINT
a: ALIGNMENT
   → AL_TAGDEF

The AL_TAG identified by t is defined to stand for the ALIGNMENT a. All the AL_TAGDEFs in a CAPSULE must be considered together as a set of simultaneous equations defining ALIGNMENT values for the AL_TAGs. No order is imposed on the definitions.

In any particular CAPSULE the set of equations may be incomplete, but a CAPSULE which is being translated into code will have a set of equations which defines all the AL_TAGs which it uses.

The result of the evaluation of the control argument of any x_cond construction (e.g alignment_cond) used in a shall be independent of any AL_TAGs used in the control. Simultaneous equations defining ALIGNMENTs can then always be solved.

See Section 6.13.3, “Circular types in languages” Circular types in languages.

no_labels: TDFINT
tds:       SLIST(AL_TAGDEF)
           → AL_TAGDEF_PROPS

no_labels is the number of local LABELs used in tds. tds is a list of AL_TAGDEFs which define the bindings for al_tags.

token_value: TOKEN
token_args:  BITSTREAM param_sorts(token_value)
             → ALIGNMENT

The token is applied to the arguments encoded in the BITSTREAM token_args to give an ALIGNMENT.

If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.

control: EXP INTEGER(v)
e1:      BITSTREAM ALIGNMENT
e2:      BITSTREAM ALIGNMENT
         → ALIGNMENT

control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.

sha: SHAPE
     → ALIGNMENT

The alignment construct is defined as follows:

→ ALIGNMENT

Delivers the ALIGNMENT of POINTERs produced from local_alloc.

var: BOOL
     → ALIGNMENT

If var is true the ALIGNMENT is that of callee parameters qualified by the PROCPROPS var_callees. If var is false, the ALIGNMENT is that of callee parameters not qualified by PROCPROPS var_callees.

Delivers the base ALIGNMENT of OFFSETs from a frame-pointer to a CALLEE parameter. Values of such OFFSETs can only be produced by env_offset applied to CALLEE parameters, or offset arithmetic operations applied to existing OFFSETs.

var: BOOL
     → ALIGNMENT

If var is true the ALIGNMENT is that of caller parameters qualified by the PROCPROPS var_callers. If var is false, the ALIGNMENT is that of caller parameters not qualified by PROCPROPS var_callers.

Delivers the base ALIGNMENT of OFFSETs from a frame-pointer to a CALLER parameter. Values of such OFFSETs can only be produced by env_offset applied to CALLER parameters, or offset arithmetic operations applied to existing OFFSETs.

→ ALIGNMENT

Delivers {code}, the ALIGNMENT of the POINTER produced by make_local_lv.

→ ALIGNMENT

Delivers the base ALIGNMENT of OFFSETs from a frame-pointer to a value defined by variable or identify. Values of such OFFSETs can only be produced by env_offset applied to TAGs so defined, or offset arithmetic operations applied to existing OFFSETs.

at: AL_TAG
    → ALIGNMENT

obtain_al_tag produces the ALIGNMENT with which the AL_TAG at is bound.

sha: SHAPE
     → ALIGNMENT

Delivers the ALIGNMENT of a parameter of a procedure of SHAPE sha.

a1: ALIGNMENT
a2: ALIGNMENT
    → ALIGNMENT

unite_alignments produces the alignment at which all the members of the ALIGNMENT sets a1 and a2 can be placed - in other words the ALIGNMENT set which is the union of a1 and a2.

→ ALIGNMENT

Delivers the ALIGNMENT used in the var_param argument of make_proc.

token_value: TOKEN
token_args:  BITSTREAM param_sorts(token_value)
             → BITFIELD_VARIETY

The token is applied to the arguments encoded in the BITSTREAM token_args to give a BITFIELD_VARIETY.

If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.

control: EXP INTEGER(v)
e1:      BITSTREAM BITFIELD_VARIETY
e2:      BITSTREAM BITFIELD_VARIETY
         → BITFIELD_VARIETY

control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.

issigned: BOOL
bits:     NAT
          → BITFIELD_VARIETY

bfvar_bits constructs a BITFIELD_VARIETY describing a pattern of bits bits. If issigned is true, the pattern is considered to be a twos-complement signed number: otherwise it is considered to be unsigned.

token_value: TOKEN
token_args:  BITSTREAM param_sorts(token_value)
             → BOOL

The token is applied to the arguments encoded in the BITSTREAM token_args to give a BOOL.

If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.

control: EXP INTEGER(v)
e1:      BITSTREAM BOOL
e2:      BITSTREAM BOOL
         → BOOL

control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.

→ BOOL

false produces a false BOOL.

→ BOOL

true produces a true BOOL.

args: LIST(EXP)
      → CALLEES

The list of EXPs args are evaluated in any interleaved order and the resulting list of values form the actual callee parameters of the call.

ptr: EXP POINTER(x)
sze: EXP OFFSET(x, y)
     → CALLEES

The value of size sze pointed at by ptr forms the actual callee parameters of the call.

The CALLEES value is intended to refer to a sequence of zero or more callee parameters. x will include parameter_alignment(s) for each s that is the SHAPE of an intended callee parameter. The value addressed by ptr may be produced in one of two ways. It may be produced as a COMPOUND SHAPE value in the normal sense of a structure, whose successive elements will be used to generate the sequence of callee parameters. In this case, each element in the sequence of SHAPE s must additionally be padded to parameter_alignment(s). Alternatively, ptr may address the callee parameters of an already activated procedure, by referring to the first of the sequence. sze will be equivalent to shape_offset(c) where c is the COMPOUND SHAPE just described.

The call involved (i.e. apply_general_proc or tail_call) must have a var_callees PROCPROPS.

→ CALLEES

The callee parameters of the call are the same as those of the current procedure.

prop_names:  SLIST(TDFIDENT)
cap_linking: SLIST(CAPSULE_LINK)
ext_linkage: SLIST(EXTERN_LINK)
groups:      SLIST(GROUP)
             → CAPSULE

make_capsule brings together UNITs and linking and naming information. See Section 1.1, “The Overall Structure” The Overall Structure.

The elements of the list, prop_names, correspond one-to-one with the elements of the list, groups. The element of prop_names is the unit identification of all the UNITs in the corresponding GROUP. See Section 4.29, “PROPS” PROPS. A CAPSULE need not contain all the kinds of UNIT.

It is intended that new kinds of PROPS with new unit identifications can be added to the standard in a purely additive fashion, either to form a new standard or for private purposes.

The elements of the list, cap_linking, correspond one-to-one with the elements of the list, ext_linkage. The element of cap_linking gives the linkable entity identification for all the LINKEXTERNs in the element of ext_linkage. It also gives the number of CAPSULE level linkable entities having that identification.

The elements of the list, cap_linking, also correspond one-to-one with the elements of the lists called local_vars in each of the make_unit constructions for the UNITs in groups. The element of local_vars gives the number of UNIT level linkable entities having the identification in the corresponding member of cap_linking.

It is intended that new kinds of linkable entity can be added to the standard in a purely additive fashion, either to form a new standard or for private purposes.

ext_linkage provides a list of lists of LINKEXTERNs. These LINKEXTERNs specify the associations between the names to be used outside the CAPSULE and the linkable entities by which the UNITs make objects available within the CAPSULE.

The list, groups, provides the non-linkage information of the CAPSULE.

sn: TDFIDENT
n:  TDFINT
    → CAPSULE_LINK

n is the number of CAPSULE level linkable entities (numbered from 0 to n-1) of the kind given by sn. sn corresponds to the linkable entity identification.

branch: LABEL
lower:  SIGNED_NAT
upper:  SIGNED_NAT
        → CASELIM

Makes a triple of destination and limits. The case construction uses a list of CASELIMs. If the control variable of the case lies between lower and upper, control passes to branch.

→ ERROR_CODE

Delivers the ERROR_CODE arising from an attempt to access a nil pointer in an operation with TRANSFER_MODE trap_on_nil.

→ ERROR_CODE

Delivers the ERROR_CODE arising from a numerical exceptional result in an operation with ERROR_TREATMENT trap(overflow).

→ ERROR_CODE

Delivers the ERROR_CODE arising from a stack overflow in the call of a procedure defined with PROCPROPS check_stack.

token_value: TOKEN
token_args:  BITSTREAM param_sorts(token_value)
             → ERROR_TREATMENT

The token is applied to the arguments encoded in the BITSTREAM token_args to give an ERROR_TREATMENT.

If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.

control: EXP INTEGER(v)
e1:      BITSTREAM ERROR_TREATMENT
e2:      BITSTREAM ERROR_TREATMENT
         → ERROR_TREATMENT

control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.

→ ERROR_TREATMENT

If an operation with a continue ERROR_TREATMENT causes an error, some value of the correct SHAPE shall be delivered. This value shall have the same properties as is specified in make_value.

lab: LABEL
     → ERROR_TREATMENT

error_jump produces an ERROR_TREATMENT which requires that control be passed to lab if it is invoked. lab will be in scope.

If a construction has an error_jump ERROR_TREATMENT and the jump is taken, the canonical order specifies only that the jump occurs after evaluating the construction. It is not specified how many further constructions are evaluated.

This rule implies that a further construction is needed to guarantee that errors have been processed. This is not yet included. The effect of nearby procedure calls or exits also needs definition.

trap_list: LIST(ERROR_CODE)
           → ERROR_TREATMENT

The list of ERROR_CODES in trap_list specifies a set of possible exceptional behaviours. If any of these occur in an construction with ERROR_TREATMENT trap, the TDF exception handling is invoked (see Section 6.8, “Exceptions and jumps” section 7.8).

The observations on canonical ordering in error_jump apply equally here.

→ ERROR_TREATMENT

wrap is an ERROR_TREATMENT which will only be used in constructions with integer operands and delivering EXP INTEGER(v) where either the lower bound of v is zero or the construction is not one of mult, power, div0, div1, div2, rem0, rem1, rem2. The result will be evaluated and any bits in the result lying outside the representing VARIETY will be discarded (see Section 6.18, “Representing integers” Representing integers).

→ ERROR_TREATMENT

impossible is an ERROR_TREATMENT which means that this error will not occur in the construct concerned.

impossible is possibly a misnomer. If an error occurs the result is undefined.

token_value: TOKEN
token_args:  BITSTREAM param_sorts(token_value)
             → EXP x

The token is applied to the arguments encoded in the BITSTREAM token_args to give an EXP.

If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.

control: EXP INTEGER(v)
e1:      BITSTREAM EXP x
e2:      BITSTREAM EXP y
         → EXP (control ? x : y)

control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.

ov_err: ERROR_TREATMENT
arg1:   EXP INTEGER(v)
        → EXP INTEGER(v)

The absolute value of the result produced by arg1 is delivered.

If the result cannot be expressed in the VARIETY being used to represent v, an overflow error is caused and is handled in the way specified by ov_err.

arg1: EXP POINTER(x)
arg2: EXP OFFSET(y, z)
      → EXP POINTER(z)

arg1 is evaluated, giving p, and arg2 is evaluated and the results are added to produce the answer. The result is derived from the pointer delivered by arg1. The intention is to produce a POINTER displaced from the argument POINTER by the given amount.

x will include y.

arg1 may deliver a null POINTER. In this case the result is derived from a null POINTER which counts as an original POINTER. Further OFFSETs may be added to the result, but the only other useful operation on the result of adding a number of OFFSETs to a null POINTER is to subtract_ptrs a null POINTER from it.

The result will be less than or equal (in the sense of pointer_test) to the result of applying add_to_ptr to the original pointer from which p is derived and the size of the space allocated for the original pointer.

In the simple representation of POINTER arithmetic (see Section 6.13, “Memory Model” Memory Model) add_to_ptr is represented by addition. The constraint "x includes y" ensures that no padding has to be inserted in this case.

arg1: EXP INTEGER(v)
arg2: EXP INTEGER(v)
      → EXP INTEGER(v)

The arguments are evaluated producing integer values of the same VARIETY, v. The result is the bitwise and of the two values in the representing VARIETY. The result is delivered with the same SHAPE as the arguments.

See Section 6.18, “Representing integers” Representing integers.

result_shape: SHAPE
p:            EXP PROC
params:       LIST(EXP)
var_param:    OPTION(EXP)
              → EXP result_shape

p, params and var_param (if present) are evaluated in any interleaved order. The procedure, p, is applied to the parameters. The result of the procedure call, which will have result_shape, is delivered as the result of the construction.

The canonical order of evaluation is as if the definition were in-lined. That is, the actual parameters are evaluated interleaved in any order and used to initialise variables which are identified by the formal parameters during the evaluation of the procedure body. When this is complete the body is evaluated. So apply_proc is evaluated like a variable construction, and obeys similar rules for order of evaluation.

If p delivers a null procedure the effect is undefined.

var_param is intended to communicate parameters which vary in SHAPE from call to call. Access to these parameters during the procedure is performed by using OFFSET arithmetic. Note that it is necessary to place these values on var_param_alignment because of the definition of make_proc.

The optional var_param should not be confused with variable argument lists in the C (<stdarg.h> or <varargs.h>) sense, which are communicated by extending the params list. This is discussed further in Section 6.9, “Procedures” section 7.9. If the number of arguments in the params list differs from the number of elements in the params_intro of the corresponding make_proc, then var_param must not be present.

All calls to the same procedure will yield results of the same SHAPE.

For notes on the intended implementation of procedures see Section 6.9, “Procedures” section 7.9.

result_shape:  SHAPE
prcprops:      OPTION(PROCPROPS)
p:             EXP PROC
callers_intro: LIST(OTAGEXP)
callee_pars:   CALLEES
postlude:      EXP TOP
               → EXP result_shape

p, callers_intro and callee_pars are evaluated in any order. The procedure, p, is applied to the parameters. The result of the procedure call, which will have result_shape, is delivered as the result of the construction.

If p delivers a null procedure the effect is undefined.

Any TAG introduced by an OTAGEXP in callers_intro is available in postlude which will be evaluated after the application.

postlude will not contain any local_allocs or calls of procedures with untidy returns. If prcprops include untidy, postlude will be make_top.

The canonical order of evaluation is as if the definition of p were inlined in a manner dependent on prcprops.

If none of the PROCPROPS var_callers, var_callees and check_stack are present the inlining is as follows, supposing that P is the body of the definition of p:

Let Ri be the value of the EXP of the ith OTAGEXP in callers_intro and Ti be its TAG (if it is present). Let Ei be the ith value in callee_pars.

Let ri be the ith formal caller parameter TAG of p.

Let ei be the ith formal callee parameter TAG of p.

Each Ri is used to initialise a variable which is identified by ri; there will be exactly as many Ri as ri.The scope of these variable definitions is a sequence consisting of three components - the identification of a TAG res with the result of a binding of P, followed by a binding of postlude, followed by an obtain_tag of res giving the result of the inlined procedure call.

The binding of P consists of using each Ei to initialise a variable identified with ei; there will be exactly as many Ei as ei. The scope of these variable definitions is P modified so that the first return or untidy_return encountered in P gives the result of the binding. If it ends with a return, any space generated by local_allocs within the binding is freed (in the sense of local_free) at this point. If it ends with untidy_return, no freeing will take place.

The binding of postlude consists of identifying each Ti (if present) with the contents of the variable identified by ri. The scope of these identifications is postlude.

If the PROCPROPS var_callers is present, the inlining process is modified by:

A compound variable is constructed initialised to Ri in order; the alignment and padding of each individual Ri will be given by an exact application of parameter_alignment on the SHAPE of Ri. Each ri is then identified with a pointer to the copy of Ri within the compound variable; there will be at least as many Ri as ri. The evaluation then continues as above with the scope of these identifications being the sequence.

If the PROCPROPS var_callees is present, the inlining process is modified by:

The binding of P is done by generating (as if by local_alloc) a pointer to space for a compound value constructed from each Ei in order (just as for var_callers). Each ei is identified with a pointer to the copy of Ei within the generated space; there will be at least as many ei as Ei. P is evaluated within the scope of these identifications as before. Note that the generation of space for these callee parameters is a local_alloc with the binding of P, and hence will not be freed if P ends with an untidy_return.

arg1: EXP POINTER(x)
arg2: EXP y
      → EXP TOP

The value produced by arg2 will be put in the space indicated by arg1.

x will include alignment(y).

y will not be a BITFIELD.

If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.

If the value delivered by arg1 is a null pointer the effect is undefined.

See Section 6.16, “Overlapping” Overlapping and Section 6.17, “Incomplete assignment” Incomplete assignment.

The constraint "x will include alignment(y)" ensures in the simple memory model that no change is needed to the POINTER.

md:   TRANSFER_MODE
arg1: EXP POINTER(x)
arg2: EXP y
      → EXP TOP

The value produced by arg2 will be put in the space indicated by arg1. The assignment will be carried out as specified by the TRANSFER_MODE (q.v.).

If md consists of standard_transfer_mode only, then assign_with_mode is the same as assign.

x will include alignment(y).

y will not be a BITFIELD.

If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.

If the value delivered by arg1 is a null pointer the effect is undefined.

See Section 6.16, “Overlapping” Overlapping and Section 6.17, “Incomplete assignment” Incomplete assignment.

arg1: EXP POINTER(x)
arg2: EXP OFFSET(y, z)
arg3: EXP BITFIELD(v)
      → EXP TOP

The value delivered by arg3 is assigned at a displacement given by arg2 from the pointer delivered by arg1.

x will include y and z will include v.

arg2, BITFIELD(v) will be variety-enclosed (see Section 6.24, “Representing bitfields” section 7.24).

md:   TRANSFER_MODE
arg1: EXP POINTER(x)
arg2: EXP OFFSET(y, z)
arg3: EXP BITFIELD(v)
      → EXP TOP

The value delivered by arg3 is assigned at a displacement given by arg2 from the pointer delivered by arg1.The assignment will be carried out as specified by the TRANSFER_MODE (q.v.).

If md consists of standard_transfer_mode only, then bitfield_assign_with_mode is the same as bitfield_assign.

x will include y and z will include v.

arg2, BITFIELD(v) will be variety-enclosed.(see Section 6.24, “Representing bitfields” section 7.24).

v:    BITFIELD_VARIETY
arg1: EXP POINTER(x)
arg2: EXP OFFSET(y, z)
      → EXP BITFIELD(v)

The bitfield of BITFIELD_VARIETY v, located at the displacement delivered by arg2 from the pointer delivered by arg1 is extracted and delivered.

x will include y and z will include v.

arg2, BITFIELD(v) will be variety_enclosed (see Section 6.24, “Representing bitfields” section 7.24).

md:   TRANSFER_MODE
v:    BITFIELD_VARIETY
arg1: EXP POINTER(x)
arg2: EXP OFFSET(y, z)
      → EXP BITFIELD(v)

The bitfield of BITFIELD_VARIETY v, located at the displacement delivered by arg2 from the pointer delivered by arg1 is extracted and delivered.The operation will be carried out as specified by the TRANSFER_MODE (q.v.).

If md consists of standard_transfer_mode only, then bitfield_contents_with_mode is the same as bitfield_contents.

x will include y and z will include v.

arg2, BITFIELD(v) will be variety_enclosed (see Section 6.24, “Representing bitfields” section 7.24).

exhaustive: BOOL
control:    EXP INTEGER(v)
branches:   LIST(CASELIM)
            → EXP (exhaustive ? BOTTOM : TOP)

control is evaluated to produce an integer value, c. Then c is tested to see if it lies inclusively between lower and upper, for each element of branches. If this tests succeeds, control passes to the label branch belonging to that CASELIM (see Section 4.13, “CASELIM” section 5.13). If c lies between no pair, the construct delivers a value of SHAPE TOP. The order in which the comparisons are made is undefined.

The sets of SIGNED_NATs in branches will be disjoint.

If exhaustive is true the value delivered by control will lie between one of the lower/upper pairs.

v:    VARIETY
arg1: EXP BITFIELD(bv)
      → EXP INTEGER(v)

arg1 is evaluated and converted to a INTEGER(v).

If arg1 exceed the bounds of v, the effect is undefined.

flpt_err: ERROR_TREATMENT
r:        FLOATING_VARIETY
arg1:     EXP FLOATING(f)
          → EXP FLOATING(r)

arg1 is evaluated and will produce floating point value, fp. The value fp is delivered, changed to the representation of the FLOATING_VARIETY r.

Either r and f will both real or both complex.

If there is a floating point error it is handled by flpt_err.

See Section 6.21, “Floating point errors” Floating point errors.

ov_err: ERROR_TREATMENT
r:      VARIETY
arg1:   EXP INTEGER(v)
        → EXP INTEGER(r)

arg1 is evaluated and will produce an integer value, a. The value a is delivered, changed to the representation of the VARIETY r.

If a is not contained in the VARIETY being used to represent r, an overflow occurs and is handled according to ov_err.

bv:   BITFIELD_VARIETY
arg1: EXP INTEGER(v)
      → EXP BITFIELD(bv)

arg1 is evaluated and converted to a BITFIELD(bv).

If arg1 exceed the bounds of bv, the effect is undefined.

c: EXP FLOATING(cv)
   → EXP FLOATING(cv)

Delivers the complex conjugate of c.

cv will be a complex floating variety.

sha:  SHAPE
arg1: EXP COMPOUND(EXP OFFSET(x, y))
arg2: EXP OFFSET(x, alignment(sha))
      → EXP sha

arg1 is evaluated to produce a COMPOUND value. The component of this value at the OFFSET given by arg2 is delivered. This will have SHAPE sha.

arg2 will be a constant and non-negative (see Section 6.3, “Constant evaluation” Constant evaluation).

If sha is a BITFIELD then arg2, sha will be variety_enclosed (see Section 6.24, “Representing bitfields” section 7.24).

arg1: EXP NOF(n, s)
arg2: EXP NOF(m, s)
      → EXP NOF(n+m, s)

arg1 and arg2 are evaluated and their results concatenated. In the result the components derived from arg1 will have lower indices than those derived from arg2.

altlab_intro: LABEL
first:        EXP x
alt:          EXP z
              → EXP (x LUB z)

first is evaluated. If first produces a result, f, this value is delivered as the result of the whole construct, and alt is not evaluated.

If goto(altlab_intro) or any other jump (including long_jump) to altlab_intro is obeyed during the evaluation of first, then the evaluation of first will stop, alt will be evaluated and its result delivered as the result of the construction.

The lifetime of altlab_intro is the evaluation of first. altlab_intro will not be used within alt.

The actual order of evaluation of the constituents shall be indistinguishable in all observable effects (apart from time) from evaluating all the obeyed parts of first before any obeyed part of alt. Note that this specifically includes any defined error handling.

For LUB see Section 6.26, “Least Upper Bound” Least Upper Bound.

s:    SHAPE
arg1: EXP POINTER(x)
      → EXP s

A value of SHAPE s will be extracted from the start of the space indicated by the pointer, and this is delivered.

x will include alignment(s).

s will not be a BITFIELD.

If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.

If the value delivered by arg1 is a null pointer the effect is undefined.

The constraint "x will include alignment(s)" ensures in the simple memory model that no change is needed to the POINTER.

md:   TRANSFER_MODE
s:    SHAPE
arg1: EXP POINTER(x)
      → EXP s

A value of SHAPE s will be extracted from the start of the space indicated by the pointer, and this is delivered. The operation will be carried out as specified by the TRANSFER_MODE (q.v.).

If md consists of standard_transfer_mode only, then contents_with_mode is the same as contents.

x will include alignment(s).

s will not be a BITFIELD.

If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.

If the value delivered by arg1 is a null pointer the effect is undefined.

→ EXP POINTER(fa)

A value of SHAPE POINTER(fa) is created and delivered. It gives access to the variables, identities and parameters in the current procedure activation which are declared as having ACCESS visible.

If the immediately enclosing procedure is defined by make_general_proc, then fa is the set union of local_alignment and the alignments of the kinds of parameters defined. That is to say, if there are caller parameters, then the alignment includes callers_alignment(x) where x is true if and only if the PROCPROPS var_callers is present; if there are callee parameters, the alignment includes callees_alignment(x) where x is true if and only if the PROCPROPS var_callees is present.

If the immediately enclosing procedure is defined by make_proc, then fa = { locals_alignment, callers_alignment(false) }.

If an OFFSET produced by env_offset is added to a POINTER produced by current_env from an activation of the procedure which contains the declaration of the TAG used by env_offset, then the result is an original POINTER, notwithstanding the normal rules for add_to_ptr (see Section 6.15, “Original pointers” Original pointers).

If an OFFSET produced by env_offset is added to such a pointer from an inappropriate procedure the effect is undefined.

div_by_0_err: ERROR_TREATMENT
ov_err:       ERROR_TREATMENT
arg1:         EXP INTEGER(v)
arg2:         EXP INTEGER(v)
              → EXP INTEGER(v)

arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. Either the value a D1 b or the value a D2 b is delivered as the result of the construct, with the same SHAPE as the arguments. Different occurrences of div0 in the same capsule can use D1 or D2 independently.

If b is zero a div_by_zero error occurs and is handled by div_by_0_err.

If b is not zero and the result cannot be expressed in the VARIETY being used to represent v an overflow occurs and is handled by ov_err.

Producers may assume that shifting and div0 by a constant which is a power of two yield equally good code.

See Section 6.4, “Division and modulus” Division and modulus for the definitions of D1, D2, M1 and M2.

div_by_0_err: ERROR_TREATMENT
ov_err:       ERROR_TREATMENT
arg1:         EXP INTEGER(v)
arg2:         EXP INTEGER(v)
              → EXP INTEGER(v)

arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The value a D1 b is delivered as the result of the construct, with the same SHAPE as the arguments.

If b is zero a div_by_zero error occurs and is handled by div_by_0_err.

If b is not zero and the result cannot be expressed in the VARIETY being used to represent v an overflow occurs and is handled by ov_err.

Producers may assume that shifting and div1 by a constant which is a power of two yield equally good code.

See Section 6.4, “Division and modulus” Division and modulus for the definitions of D1, D2, M1 and M2.

div_by_0_err: ERROR_TREATMENT
ov_err:       ERROR_TREATMENT
arg1:         EXP INTEGER(v)
arg2:         EXP INTEGER(v)
              → EXP INTEGER(v)

arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The value a D2 b is delivered as the result of the construct, with the same SHAPE as the arguments.

If b is zero a div_by_zero error occurs and is handled by div_by_0_err.

If b is not zero and the result cannot be expressed in the VARIETY being used to represent v an overflow occurs and is handled by ov_err.

Producers may assume that shifting and div2 by a constant which is a power of two yield equally good code if the lower bound of v is zero.

See Section 6.4, “Division and modulus” Division and modulus for the definitions of D1, D2, M1 and M2.

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

t will be the tag of a variable, identify or procedure parameter with the visible property within a procedure defined by make_general_proc or make_proc.

If it is defined in a make_general_proc, let P be its associated PROCPROPS; otherwise let P be the PROCPROPS {locals_alignment, caller_alignment(false)}.

If t is the TAG of a variable or identify, fa will contain locals_alignment; if it is a caller parameter fa will contain a caller_alignment(b) where b is true if and only if P contains var_callers ; if it is a callee parameter fa will contain a callee_alignment(b) where b is true if and only if P contains var_callees.

If t is the TAG of a variable or parameter, the result is the OFFSET of its position, within any procedure environment which derives from the procedure containing the declaration of the variable or parameter, relative to its environment pointer. In this case x will be POINTER(y).

If t is the TAG of an identify, the result will be an OFFSET of space which holds the value. This pointer will not be used to alter the value. In this case y will be alignment(x).

See Section 6.10, “Frames” section 7.10.

proctag: TAG PROC
         → EXP OFFSET(locals_alignment, {})

Delivers an OFFSET of a space sufficient to contain all the variables and identifications, explicit or implicit in the procedure identified by proctag. This will not include the space required for any local_allocs or procedure calls within the procedure.

proctag will be defined in the current CAPSULE by a TAGDEF identification of a make_proc or a make_general_proc.

message: STRING(k, n)
         → EXP BOTTOM

Any attempt to use this operation to produce code will result in a failure of the installation process. message will give information about the reason for this failure which should be passed to the installation manager.

flpt_err: ERROR_TREATMENT
f:        FLOATING_VARIETY
arg1:     EXP INTEGER(v)
          → EXP FLOATING(f)

arg1 is evaluated to produce an integer value, which is converted to the representation of f and delivered.

If f is complex the real part of the result will be derived from arg1 and the imaginary part will be zero.

If there is a floating point error it is handled by flpt_err. See Section 6.21, “Floating point errors” Floating point errors.

flpt_err: ERROR_TREATMENT
arg1:     EXP FLOATING(f)
          → EXP FLOATING(f)

arg1 is evaluated and will produce a floating point value, a, of the FLOATING_VARIETY, f. The absolute value of a is delivered as the result of the construct, with the same SHAPE as the argument.

Though floating_abs cannot produce an overflow it can give an invalid operand exception which is handled by flpt_err.

f will not be complex.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

flpt_err: ERROR_TREATMENT
arg1:     EXP FLOATING(f)
arg2:     EXP FLOATING(f)
          → EXP FLOATING(f)

arg1 and arg2 are evaluated and will produce floating point values, a and b, of the same FLOATING_VARIETY, f. The value a/b is delivered as the result of the construct, with the same SHAPE as the arguments.

If there is a floating point error it is handled by flpt_err. See Section 6.21, “Floating point errors” Floating point errors.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

flpt_err: ERROR_TREATMENT
arg1:     EXP FLOATING(f)
arg2:     EXP FLOATING(f)
          → EXP FLOATING(f)

arg1 and arg2 are evaluated and will produce floating point values, a and b, of the same FLOATING_VARIETY, f. The value a-b is delivered as the result of the construct, with the same SHAPE as the arguments.

If there is a floating point error it is handled by flpt_err. See Section 6.21, “Floating point errors” Floating point errors.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

flpt_err: ERROR_TREATMENT
arg1:     EXP FLOATING(f)
arg2:     EXP FLOATING(f)
          → EXP FLOATING(f)

The maximum of the values delivered by arg1 and arg2 is the result. f will not be complex.

If arg1 and arg2 are incomparable, flpt_err will be invoked.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

flpt_err: ERROR_TREATMENT
arg1:     EXP FLOATING(f)
arg2:     EXP FLOATING(f)
          → EXP FLOATING(f)

The minimum of the values delivered by arg1 and arg2 is the result. f will not be complex.

If arg1 and arg2 are incomparable, flpt_err will be invoked.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

flpt_err: ERROR_TREATMENT
arg1:     LIST(EXP)
          → EXP FLOATING(f)

The arguments, arg1, are evaluated producing floating point values all of the same FLOATING_VARIETY, f. These values are multiplied in any order and the result of this multiplication is delivered as the result of the construct, with the same SHAPE as the arguments.

If there is a floating point error it is handled by flpt_err. See Section 6.21, “Floating point errors” Floating point errors.

If arg1 contains one element the result is the value of that element. There will be at least one element in arg1.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

flpt_err: ERROR_TREATMENT
arg1:     EXP FLOATING(f)
          → EXP FLOATING(f)

arg1 is evaluated and will produce a floating point value, a, of the FLOATING_VARIETY, f. The value -a is delivered as the result of the construct, with the same SHAPE as the argument.

Though floating_negate cannot produce an overflow it can give an invalid operand exception which is handled by flpt_err.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

flpt_err: ERROR_TREATMENT
arg1:     LIST(EXP)
          → EXP FLOATING(f)

The arguments, arg1, are evaluated producing floating point values, all of the same FLOATING_VARIETY, f. These values are added in any order and the result of this addition is delivered as the result of the construct, with the same SHAPE as the arguments.

If there is a floating point error it is handled by flpt_err. See Section 6.21, “Floating point errors” Floating point errors.

Note that separate floating_plus operations cannot in general be combined, because rounding errors need to be controlled. The reason for allowing floating_plus to take a variable number of arguments is to make it possible to specify that a number of multiplications can be re-ordered.

If arg1 contains one element the result is the value of that element. There will be at least one element in arg1.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

flpt_err: ERROR_TREATMENT
arg1:     EXP FLOATING(f)
arg2:     EXP INTEGER(v)
          → EXP FLOATING(f)

The result of arg1 is raised to the power given by arg2.

If there is a floating point error it is handled by flpt_err. See Section 6.21, “Floating point errors” Floating point errors.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

prob:     OPTION(NAT)
flpt_err: ERROR_TREATMENT
nt:       NTEST
dest:     LABEL
arg1:     EXP FLOATING(f)
arg2:     EXP FLOATING(f)
          → EXP TOP

arg1 and arg2 are evaluated and will produce floating point values, a and b, of the same FLOATING_VARIETY, f. These values are compared using nt.

If f is complex then nt will be equal or not_equal.

If a nt b, this construction yields TOP. Otherwise control passes to dest.

If prob is present, prob/100 gives the probability that control will continue to the next construct (ie. not pass to dest). If prob is absent this probability is unknown.

If there is a floating point error it is handled by flpt_err. See Section 6.21, “Floating point errors” Floating point errors.

See also Section 6.23, “Floating point accuracy” Floating point accuracy.

dest: LABEL
      → EXP BOTTOM

Control passes to the EXP labelled dest. This construct will only be used where dest is in scope.

arg1: EXP POINTER({code})
      → EXP BOTTOM

arg1 is evaluated. The label from which the value delivered by arg1 was created will be within its lifetime and this construction will be obeyed in the same activation of the same procedure as the creation of the POINTER({code}) by make_local_lv. Control passes to this activation of this LABEL.

If arg1 delivers a null POINTER the effect is undefined.

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

definition is evaluated to produce a value, v. Then body is evaluated. During this evaluation, v is bound to name_intro. This means that inside body an evaluation of obtain_tag(name_intro) will produce the value, v.

The value delivered by identify is that produced by body.

The TAG given for name_intro will not be reused within the current UNIT. No rules for the hiding of one TAG by another are given: this will not happen. The lifetime of name_intro is the evaluation of body.

If opt_access contains visible, it means that the value must not be aliased while the procedure containing this declaration is not the current procedure. Hence if there are any copies of this value they will need to be refreshed when the procedure is returned to. The easiest implementation when opt_access is visible may be to keep the value in memory, but this is not a necessary requirement.

The order in which the constituents of definition and body are evaluated shall be indistinguishable in all observable effects (apart from time) from completely evaluating definition before starting body. See the note about order in Section 4.16.107, “sequence” sequence.

arg1: EXP x
      → EXP x

If the result of this construction is discarded, arg1 need not be evaluated, though evaluation is permitted. If the result is used it is the result of arg1.

arg1: EXP c
      → EXP FLOATING (float_of_complex(c))

c will be complex. Delivers the imaginary part of the value produced by arg1.

init: EXP s
      → EXP s

Any tag used as an argument of an obtain_tag in init will be global or defined within init.

All labels used in init will be defined within init.

init will be evaluated once only before any procedure application, other than those involved in this or other initial_value constructions, but after all load-time constant initialisations of TAGDEFs. The result of this evaluation is the value of the construction.

The order of evaluation of the different initial_values in a program is undefined.

See Section 6.29, “Dynamic initialisation” section 7.29.

prob: OPTION(NAT)
nt:   NTEST
dest: LABEL
arg1: EXP INTEGER(v)
arg2: EXP INTEGER(v)
      → EXP TOP

arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. These values are compared using nt.

If a nt b, this construction yields TOP. Otherwise control passes to dest.

If prob is present, prob/100 gives the probability that control will continue to the next construct (ie. not pass to dest). If prob is absent this probability is unknown.

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

The lists labs_intro and places shall have the same number of elements.

To evaluate the construction starter is evaluated. If its evaluation runs to completion producing a value, then this is delivered as the result of the whole construction. If a goto one of the LABELs in labs_intro or any other jump to one of these LABELs is evaluated, then the evaluation of starter stops and the corresponding element of places is evaluated. In the canonical ordering all the operations which are evaluated from starter are completed before any from an element of places is started. If the evaluation of the member of places produces a result this is the result of the construction.

If a jump to any of the labs_intro is obeyed then evaluation continues similarly. Such jumping may continue indefinitely, but if any places terminates, then the value it produces is the value delivered by the construction.

The SHAPE w is the LUB of x and all the places. See Section 6.26, “Least Upper Bound” Least Upper Bound.

The actual order of evaluation of the constituents shall be indistinguishable in all observable effects (apart from time) from that described above. Note that this specifically includes any defined error handling.

The lifetime of each of the LABELs in labs_intro, is the evaluation of starter and all the elements of places.

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

If the last use of local_alloc in the current activation of the current procedure was after the last use of local_free or local_free_all, then the value returned is the last POINTER allocated with local_alloc.

If the last use of local_free in the current activation of the current procedure was after the last use of local_alloc, then the result is the POINTER last allocated which is still active.

The result POINTER will have been created by local_alloc with the value of its arg1 equal to the value of x.

If the last use of local_free_all in the current activation of the current procedure was after the last use of local_alloc, or if there has been no use of local_alloc in the current activation of the current procedure, then the result is undefined.

The ALIGNMENT, alloca_alignment, includes the set union of all the ALIGNMENTs which can be produced by alignment from any SHAPE. See Section 6.13.4, “Special alignments” Special alignments.

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

The arg1 expression is evaluated and space is allocated sufficient to hold a value of the given size. The result is an original pointer to this space.

x will not consist entirely of bitfield alignments.

The initial contents of the space are not specified.

This allocation is as if on the stack of the current procedure, and the lifetime of the pointer ends when the current activation of the current procedure ends with a return, return_to_label or tail_call or if there is a long jump out of the activation. Any use of the pointer thereafter is undefined. Note the specific exclusion of the procedure ending with untidy_return; in this case the calling procedure becomes the current activation.

The uses of local_alloc within the procedure are ordered dynamically as they occur, and this order affects the meaning of local_free and last_local.

arg1 may be a zero OFFSET. In this case suppose the result is p. Then a subsequent use, in the same activation of the procedure, of

local_free(offset_zero(alloca_alignment), p)

will return the alloca stack to the state it was in immediately before the use of local_alloc.

Note that if a procedure which uses local_alloc is inlined, it may be necessary to use local_free to get the correct semantics.

See also Section 6.12, “Alloca” section 7.12.

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

If the OFFSET arg1 can be accomodated within the limit of the local_alloc stack (see Section 4.16.52, “local_alloc” section 5.16.108), the action is precisely the same as local_alloc.

If not, normal action is stopped and a TDF exception is raised with ERROR_CODE stack_overflow.

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

The POINTER, p, will be an original pointer to space allocated by local_alloc within the current call of the current procedure. It and all spaces allocated after it by local_alloc will no longer be used. This POINTER will have been created by local_alloc with the value of its arg1 equal to the value of a.

Any subsequent use of pointers to the spaces no longer used will be undefined.

→ EXP TOP

Every space allocated by local_alloc within the current call of the current procedure will no longer be used.

Any use of a pointer to space allocated before this operation within the current call of the current procedure is undefined.

Note that if a procedure which uses local_free_all is inlined, it may be necessary to use local_free to get the correct semantics.

arg1: EXP POINTER(fa)
arg2: EXP POINTER({code})
      → EXP BOTTOM

arg1 will be a pointer produced by an application of curent_env in a currently active procedure.

The frame produced by arg1 is reinstated as the current procedure. This frame will still be active. Evaluation recommences at the label given by arg2. This operation will only be used during the lifetime of that label.

Only TAGs declared to have long_jump_access will be defined at the re-entry.

If arg2 delivers a null POINTER({code}) the effect is undefined.