**5.1**- ACCESS-
**5.1.1**- access_apply_token**5.1.2**- access_cond**5.1.3**- add_accesses**5.1.4**- constant**5.1.5**- long_jump_access**5.1.6**- no_other_read**5.1.7**- no_other_write**5.1.8**- out_par**5.1.9**- preserve**5.1.10**- register**5.1.11**- standard_access**5.1.12**- used_as_volatile**5.1.13**- visible

**5.2**- AL_TAG-
**5.2.1**- al_tag_apply_token**5.2.2**- make_al_tag

**5.3**- AL_TAGDEF-
**5.3.1**- make_al_tagdef

**5.4**- AL_TAGDEF_PROPS-
**5.4.1**- make_al_tagdefs

**5.5**- ALIGNMENT-
**5.5.1**- alignment_apply_token**5.5.2**- alignment_cond**5.5.3**- alignment**5.5.4**- alloca_alignment**5.5.5**- callees_alignment**5.5.6**- callers_alignment**5.5.7**- code_alignment**5.5.8**- locals_alignment**5.5.9**- obtain_al_tag**5.5.10**- parameter_alignment**5.5.11**- unite_alignments**5.5.12**- var_param_alignment

**5.6**- BITFIELD_VARIETY-
**5.6.1**- bfvar_apply_token**5.6.2**- bfvar_cond**5.6.3**- bfvar_bits

**5.7**- BITSTREAM-
**5.8**- BOOL-
**5.8.1**- bool_apply_token**5.8.2**- bool_cond**5.8.3**- false**5.8.4**- true

**5.9**- BYTESTREAM-
**5.10**- CALLEES-
**5.10.1**- make_callee_list**5.10.2**- make_dynamic_callees**5.10.3**- same_callees

**5.11**- CAPSULE-
**5.11.1**- make_capsule

**5.12**- CAPSULE_LINK-
**5.12.1**- make_capsule_link

**5.13**- CASELIM-
**5.13.1**- make_caselim

**5.14**- ERROR_CODE-
**5.14.1**- nil_access**5.14.2**- overflow**5.14.3**- stack_overflow

**5.15**- ERROR_TREATMENT-
**5.15.1**- errt_apply_token**5.15.2**- errt_cond**5.15.3**- continue**5.15.4**- error_jump**5.15.5**- trap**5.15.6**- wrap**5.15.7**- impossible

**5.16**- EXP-
**5.16.1**- exp_apply_token**5.16.2**- exp_cond**5.16.3**- abs**5.16.4**- add_to_ptr**5.16.5**- and**5.16.6**- apply_proc**5.16.7**- apply_general_proc**5.16.8**- assign**5.16.9**- assign_with_mode**5.16.10**- bitfield_assign**5.16.11**- bitfield_assign_with_mode**5.16.12**- bitfield_contents**5.16.13**- bitfield_contents_with_mode**5.16.14**- case**5.16.15**- change_bitfield_to_int**5.16.16**- change_floating_variety**5.16.17**- change_variety**5.16.18**- change_int_to_bitfield**5.16.19**- complex_conjugate**5.16.20**- component**5.16.21**- concat_nof**5.16.22**- conditional**5.16.23**- contents**5.16.24**- contents_with_mode**5.16.25**- current_env**5.16.26**- div0**5.16.27**- div1**5.16.28**- div2**5.16.29**- env_offset**5.16.30**- env_size**5.16.31**- fail_installer**5.16.32**- float_int**5.16.33**- floating_abs**5.16.34**- floating_div**5.16.35**- floating_minus**5.16.36**- floating_maximum**5.16.37**- floating_minimum**5.16.38**- floating_mult**5.16.39**- floating_negate**5.16.40**- floating_plus**5.16.41**- floating_power**5.16.42**- floating_test**5.16.43**- goto**5.16.44**- goto_local_lv**5.16.45**- identify**5.16.46**- ignorable**5.16.47**- imaginary_part**5.16.48**- initial_value**5.16.49**- integer_test**5.16.50**- labelled**5.16.51**- last_local**5.16.52**- local_alloc**5.16.53**- local_alloc_check**5.16.54**- local_free**5.16.55**- local_free_all**5.16.56**- long_jump**5.16.57**- make_complex**5.16.58**- make_compound**5.16.59**- make_floating**5.16.60**- make_general_proc**5.16.61**- make_int**5.16.62**- make_local_lv**5.16.63**- make_nof**5.16.64**- make_nof_int**5.16.65**- make_null_local_lv**5.16.66**- make_null_proc**5.16.67**- make_null_ptr**5.16.68**- make_proc**5.16.69**- make_stack_limit**5.16.70**- make_top**5.16.71**- make_value**5.16.72**- maximum**5.16.73**- minimum**5.16.74**- minus**5.16.75**- move_some**5.16.76**- mult**5.16.77**- n_copies**5.16.78**- negate**5.16.79**- not**5.16.80**- obtain_tag**5.16.81**- offset_add**5.16.82**- offset_div**5.16.83**- offset_div_by_int**5.16.84**- offset_max**5.16.85**- offset_mult**5.16.86**- offset_negate**5.16.87**- offset_pad**5.16.88**- offset_subtract**5.16.89**- offset_test**5.16.90**- offset_zero**5.16.91**- or**5.16.92**- plus**5.16.93**- pointer_test**5.16.94**- power**5.16.95**- proc_test**5.16.96**- profile**5.16.97**- real_part**5.16.98**- rem0**5.16.99**- rem1**5.16.100**- rem2**5.16.101**- repeat**5.16.102**- return**5.16.103**- return_to_label**5.16.104**- round_with_mode**5.16.105**- rotate_left**5.16.106**- rotate_right**5.16.107**- sequence**5.16.108**- set_stack_limit**5.16.109**- shape_offset**5.16.110**- shift_left**5.16.111**- shift_right**5.16.112**- subtract_ptrs**5.16.113**- tail_call**5.16.114**- untidy_return**5.16.115**- variable**5.16.116**- xor

**5.17**- EXTERNAL-
**5.17.1**- string_extern**5.17.2**- unique_extern**5.17.3**- chain_extern

**5.18**- EXTERN_LINK-
**5.18.1**- make_extern_link

**5.19**- FLOATING_VARIETY-
**5.19.1**- flvar_apply_token**5.19.2**- flvar_cond**5.19.3**- flvar_parms**5.19.4**- complex_parms**5.19.5**- float_of_complex**5.19.6**- complex_of_float

**5.20**- GROUP-
**5.20.1**- make_group

**5.21**- LABEL-
**5.21.1**- label_apply_token**5.21.2**- make_label

**5.22**- LINK-
**5.22.1**- make_link

**5.23**- LINKEXTERN-
**5.23.1**- make_linkextern

**5.24**- LINKS-
**5.24.1**- make_links

**5.25**- NAT-
**5.25.1**- nat_apply_token**5.25.2**- nat_cond**5.25.3**- computed_nat**5.25.4**- error_val**5.25.5**- make_nat

**5.26**- NTEST-
**5.26.1**- ntest_apply_token**5.26.2**- ntest_cond**5.26.3**- equal**5.26.4**- greater_than**5.26.5**- greater_than_or_equal**5.26.6**- less_than**5.26.7**- less_than_or_equal**5.26.8**- not_equal**5.26.9**- not_greater_than**5.26.10**- not_greater_than_or_equal**5.26.11**- not_less_than**5.26.12**- not_less_than_or_equal**5.26.13**- less_than_or_greater_than**5.26.14**- not_less_than_and_not_greater_than**5.26.15**- comparable**5.26.16**- not_comparable

**5.27**- OTAGEXP-
**5.27.1**- make_otagexp

**5.28**- PROCPROPS-
**5.28.1**- procprops_apply_token**5.28.2**- procprops_cond**5.28.3**- add_procprops**5.28.4**- check_stack**5.28.5**- inline**5.28.6**- no_long_jump_dest**5.28.7**- untidy**5.28.8**- var_callees**5.28.9**- var_callers

**5.29**- PROPS-
**5.30**- ROUNDING_MODE-
**5.30.1**- rounding_mode_apply_token**5.30.2**- rounding_mode_cond**5.30.3**- round_as_state**5.30.4**- to_nearest**5.30.5**- toward_larger**5.30.6**- toward_smaller**5.30.7**- toward_zero

**5.31**- SHAPE-
**5.31.1**- shape_apply_token**5.31.2**- shape_cond**5.31.3**- bitfield**5.31.4**- bottom**5.31.5**- compound**5.31.6**- floating**5.31.7**- integer**5.31.8**- nof**5.31.9**- offset**5.31.10**- pointer**5.31.11**- proc**5.31.12**- top

**5.32**- SIGNED_NAT-
**5.32.1**- signed_nat_apply_token**5.32.2**- signed_nat_cond**5.32.3**- computed_signed_nat**5.32.4**- make_signed_nat**5.32.5**- snat_from_nat

**5.33**- SORTNAME-
**5.33.1**- access**5.33.2**- al_tag**5.33.3**- alignment_sort**5.33.4**- bitfield_variety**5.33.5**- bool**5.33.6**- error_treatment**5.33.7**- exp**5.33.8**- floating_variety**5.33.9**- foreign_sort**5.33.10**- label**5.33.11**- nat**5.33.12**- ntest**5.33.13**- procprops**5.33.14**- rounding_mode**5.33.15**- shape**5.33.16**- signed_nat**5.33.17**- string**5.33.18**- tag**5.33.19**- transfer_mode**5.33.20**- token**5.33.21**- variety

**5.34**- STRING-
**5.34.1**- string_apply_token**5.34.2**- string_cond**5.34.3**- concat_string**5.34.4**- make_string

**5.35**- TAG-
**5.35.1**- tag_apply_token**5.35.2**- make_tag

**5.36**- TAGACC-
**5.36.1**- make_tagacc

**5.37**- TAGDEC-
**5.37.1**- make_id_tagdec**5.37.2**- make_var_tagdec**5.37.3**- common_tagdec

**5.38**- TAGDEC_PROPS-
**5.38.1**- make_tagdecs

**5.39**- TAGDEF-
**5.39.1**- make_id_tagdef**5.39.2**- make_var_tagdef**5.39.3**- common_tagdef

**5.40**- TAGDEF_PROPS-
**5.40.1**- make_tagdefs

**5.41**- TAGSHACC-
**5.41.1**- make_tagshacc

**5.42**- TDFBOOL-
**5.43**- TDFIDENT-
**5.44**- TDFINT-
**5.45**- TDFSTRING-
**5.46**- TOKDEC-
**5.46.1**- make_tokdec

**5.47**- TOKDEC_PROPS-
**5.47.1**- make_tokdecs

**5.48**- TOKDEF-
**5.48.1**- make_tokdef

**5.49**- TOKDEF_PROPS-
**5.49.1**- make_tokdefs

**5.50**- TOKEN-
**5.50.1**- token_apply_token**5.50.2**- make_tok**5.50.3**- use_tokdef

**5.51**- TOKEN_DEFN-
**5.51.1**- token_definition

**5.52**- TOKFORMALS-
**5.52.1**- make_tokformals

**5.53**- TRANSFER_MODE-
**5.53.1**- transfer_mode_apply_token**5.53.2**- transfer_mode_cond**5.53.3**- add_modes**5.53.4**- overlap**5.53.5**- standard_transfer_mode**5.53.6**- trap_on_nil**5.53.7**- volatile**5.53.8**- complete

**5.54**- UNIQUE-
**5.54.1**- make_unique

**5.55**- UNIT-
**5.55.1**- make_unit

**5.56**- VARIETY-
**5.56.1**- var_apply_token**5.56.2**- var_cond**5.56.3**- var_limits**5.56.4**- var_width

**5.57**- VERSION_PROPS-
**5.57.1**- make_versions

**5.58**- VERSION-
**5.58.1**- make_version**5.58.2**- user_info

An `ACCESS`

describes properties a variable or identity
may have which may constrain or describe the ways in which the variable
or identity is used.

Each construction which needs an `ACCESS`

uses it in the
form `OPTION`

(`ACCESS`

). If the option is absent
the variable or identity has no special properties.

An `ACCESS`

acts like a set of the values *constant*,
*long_jump_access*, *no_other_read*, *no_other_write*,
*register*, *out_par*, *used_as_volatile*, and
*visible*. *standard_access* acts like the empty set.
*add_accesses* is the set union operation.

The token is applied to the arguments encoded in thetoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> ACCESS

`BITSTREAM`

`ACCESS`

.
The notation *param_sorts(token_value)* is intended to mean the
following. The token definition or token declaration for
*token_value* gives the `SORT`

s of its arguments in
the
`SORTNAME`

component. The `BITSTREAM`

in
*token_args* consists of these `SORT`

s 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 ACCESSe2: BITSTREAM ACCESS -> ACCESS

A construction qualified witha1: ACCESSa2: ACCESS -> ACCESS

`ACCESS`

properties

-> ACCESSOnly a variable (not an identity) may be qualified with

-> ACCESSAn object must also have this property if it is to have a defined value when a

-> ACCESSThis property refers to a

`POINTER`

,
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`

.

-> ACCESSThis property refers to a

`POINTER`

,
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`

.

-> ACCESSAn object qualified by

-> ACCESSThis 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.

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

-> ACCESSAn object qualified as having

-> ACCESSAn object qualified as having

`TRANSFER_MODE`

-> ACCESSAn object qualified as

`TAG`

must have this property if it is to be used by

`AL_TAG`

s name `ALIGNMENT`

s. They are used so
that circular definitions can be written in TDF. However, because
of the definition of alignments, intrinsic circularities cannot occur.

*For example, the following equation has a circular form*
*x = alignment(pointer(alignment(x))) and it or a similar equation
might occur in TDF. But since
**alignment*(*pointer*(*x*)) is {*pointer*},
this reduces to *x* = {*pointer*}.

The token is applied to the arguments encoded in thetoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> AL_TAG

`BITSTREAM`

`AL_TAG`

.
If there is a definition for *token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

al_tagno: TDFINT -> AL_TAG

`AL_TAG`

identified by

An `AL_TAGDEF`

gives the definition of an `AL_TAG`

for incorporation into a `AL_TAGDEF_PROPS`

.

Thet: TDFINTa: ALIGNMENT -> AL_TAGDEF

`AL_TAG`

identified by `ALIGNMENT`

`AL_TAGDEF`

s
in a `CAPSULE`

must be considered together as a set of
simultaneous equations defining `ALIGNMENT`

values for
the `AL_TAG`

s. 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_TAG`

s 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_TAG`

s used in the
*control*. Simultaneous equations defining `ALIGNMENT`

s
can then always be solved.

See Circular types in languages.

no_labels: TDFINTtds: SLIST(AL_TAGDEF) -> AL_TAGDEF_PROPS

`LABEL`

s used in
`AL_TAGDEF`

s which
define the bindings for

An `ALIGNMENT`

gives information about the layout of data
in memory and hence is a parameter for the `POINTER`

and
`OFFSET SHAPE`

s (see Memory Model).
This information consists of a set of elements.

The possible values of the elements in such a set are *proc*,
*code*, *pointer*, *offset*, all `VARIETY`

s,
all `FLOATING_VARIETY`

s and all
`BITFIELD_VARIETY`

s. The sets are written here as, for
example, {*pointer*, *proc*} meaning the set containing
*pointer* and *proc*.

In addition, there are "special" `ALIGNMENT`

s
*alloca_alignment*, *callers_alignment*,
*callees_alignment*, *locals_alignment* and
*var_param_alignment*. Each of these are considered to be sets
which include all of the "ordinary" `ALIGNMENT`

s
above.

There is a function, *alignment*, which can be applied to a
`SHAPE`

to give an `ALIGNMENT`

(see the definition
below). The interpretation of a `POINTER`

to an
`ALIGNMENT`

, *a*, is that it can serve as a
`POINTER`

to any `SHAPE`

, *s*, such that
*alignment*(*s*) is a subset of the set *a*.

So given a `POINTER`

({*proc*, *pointer*}) it
is permitted to assign a `PROC`

or a `POINTER`

to it, or indeed a compound containing only `PROC`

s and
`POINTER`

s. This permission is valid only in respect of
the space being of the right kind; it may or may not be big enough
for the data.

The most usual use for `ALIGNMENT`

is to ensure that addresses
of *int* values are aligned on 4-byte boundaries, *float*
values are aligned on 4-byte boundaries, *double*s on 8-bit boundaries
etc. and whatever may be implied by the definitions of the machines
and languages involved.

In the specification the phrase "*a* will include *b*"
where *a* and *b* are `ALIGNMENT`

s, means that
the set *b* will be a subset of *a* (or equal to *a*).

The token is applied to the arguments encoded in thetoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> ALIGNMENT

`BITSTREAM`

`ALIGNMENT`

.
If there is a definition for *token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

control: EXP INTEGER(v)e1: BITSTREAM ALIGNMENTe2: BITSTREAM ALIGNMENT -> ALIGNMENT

Thesha: SHAPE -> ALIGNMENT

- If
*sha*is`PROC`

then the resulting`ALIGNMENT`

is {*proc*}. - If
*sha*is`INTEGER`

(*v*) then the resulting`ALIGNMENT`

is {*v*}. - If
*sha*is`FLOATING`

(*v*) then the resulting`ALIGNMENT`

is {*v*}. - If
*sha*is`BITFIELD`

(*v*) then the resulting`ALIGNMENT`

is {*v*}. - If
*sha*is`TOP`

the resulting`ALIGNMENT`

is {} - the empty set. - If
*sha*is`BOTTOM`

the resulting`ALIGNMENT`

is undefined. - If
*sha*is`POINTER`

(*x*) the resulting`ALIGNMENT`

is {*pointer*}. - If
*sha*is`OFFSET`

(*x*,*y*) the resulting`ALIGNMENT`

is {*offset*}. - If
*sha*is`NOF`

(*n*,*s*) the resulting`ALIGNMENT`

is*alignment*(*s*). - If
*sha*is`COMPOUND`

(`EXP OFFSET`

(*x*,*y*)) then the resulting`ALIGNMENT`

is*x*.

-> ALIGNMENTDelivers the

`ALIGNMENT`

of `POINTER`

s produced
from

Ifvar: BOOL -> ALIGNMENT

`ALIGNMENT`

is that of
callee parameters qualified by the `PROCPROPS`

`ALIGNMENT`

is that of callee parameters not qualified
by
`PROCPROPS`

Delivers the `base ALIGNMENT`

of `OFFSET`

s from
a frame-pointer to a `CALLEE`

parameter. Values of such
`OFFSET`

s can only be produced by *env_offset* applied
to `CALLEE`

parameters, or offset arithmetic operations
applied to existing `OFFSET`

s.

Ifvar: BOOL -> ALIGNMENT

`ALIGNMENT`

is that of
caller parameters qualified by the `PROCPROPS`

`ALIGNMENT`

is that of caller parameters not qualified
by
`PROCPROPS`

Delivers the `base ALIGNMENT`

of `OFFSET`

s from
a frame-pointer to a `CALLER`

parameter. Values of such
`OFFSET`

s can only be produced by *env_offset* applied
to `CALLER`

parameters, or offset arithmetic operations
applied to existing `OFFSET`

s.

-> ALIGNMENTDelivers {

`ALIGNMENT`

of the
`POINTER`

produced by

-> ALIGNMENTDelivers the

`base ALIGNMENT`

of `OFFSET`

s from
a frame-pointer to a value defined by `OFFSET`

s can only be produced by
`TAG`

s so defined, or offset
arithmetic operations applied to existing `OFFSET`

s.

at: AL_TAG -> ALIGNMENT

`ALIGNMENT`

with which
the `AL_TAG`

Delivers thesha: SHAPE -> ALIGNMENT

`ALIGNMENT`

of a parameter of a procedure
of `SHAPE`

a1: ALIGNMENTa2: ALIGNMENT -> ALIGNMENT

`ALIGNMENT`

sets `ALIGNMENT`

set which is the
union of

-> ALIGNMENTDelivers the

`ALIGNMENT`

used in the

These describe runtime bitfield values. The intention is that these values are usually kept in memory locations which need not be aligned on addressing boundaries.

There is no limit on the size of bitfield values in TDF, but an installer may specify limits. See Representing bitfields and Permitted limits.

The token is applied to the arguments encoded in thetoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> BITFIELD_VARIETY

`BITSTREAM`

`BITFIELD_VARIETY`

.
If there is a definition for *token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

control: EXP INTEGER(v)e1: BITSTREAM BITFIELD_VARIETYe2: BITSTREAM BITFIELD_VARIETY -> BITFIELD_VARIETY

issigned: BOOLbits: NAT -> BITFIELD_VARIETY

`BITFIELD_VARIETY`

describing
a pattern of

`BITSTREAM`

consists of an encoding of any number of
bits. This encoding is such that any program reading TDF can determine
how to skip over it. To read it meaningfully extra knowledge of what
it represents may be needed.
A `BITSTREAM`

is used, for example, to supply parameters
in a `TOKEN`

application. If there is a definition of this
`TOKEN`

available, this will provide the information needed
to decode the bitstream.

See The TDF encoding.

A `BOOL`

is a piece of TDF which can take two values,
*true* or *false*.

The token is applied to the arguments encoded in thetoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> BOOL

`BITSTREAM`

`BOOL`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

control: EXP INTEGER(v)e1: BITSTREAM BOOLe2: BITSTREAM BOOL -> BOOL

-> BOOL

`BOOL`

.

-> BOOL

`BOOL`

.

`BYTESTREAM`

is analogous to a `BITSTREAM`

,
but is encoded to permit fast copying.
See The TDF encoding.

This is an auxilliary `SORT`

used in calling procedures
by
*apply_general_proc* and *tail_call* to provide their actual
callee parameters.

The list ofargs: LIST(EXP) -> CALLEES

`EXP`

s

The value of sizeptr: EXP POINTER(x)sze: EXP OFFSET(x,y) -> CALLEES

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`

.

-> CALLEESThe callee parameters of the call are the same as those of the current procedure.

A `CAPSULE`

is an independent piece of TDF. There is only
one construction, *make_capsule*.

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

`UNIT`

s and linking
and naming information. See 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
`UNIT`

s in the corresponding `GROUP`

. See
`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 `LINKEXTERN`

s 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 `UNIT`

s
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 `LINKEXTERN`

s.
These `LINKEXTERN`

s specify the associations between the
names to be used outside the `CAPSULE`

and the linkable
entities by which the `UNIT`

s make objects available within
the `CAPSULE`

.

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

.

An auxiliary `SORT`

which gives the number of linkable
entities of a given kind at `CAPSULE`

level. It is used
only in *make_capsule*.

sn: TDFIDENTn: TDFINT -> CAPSULE_LINK

`CAPSULE`

level linkable entities
(numbered from 0 to

An auxiliary `SORT`

which provides lower and upper bounds
and the `LABEL`

destination for the *case* construction.

Makes a triple of destination and limits. Thebranch: LABELlower: SIGNED_NATupper: SIGNED_NAT -> CASELIM

`CASELIM`

s. If the control variable of the

-> ERROR_CODEDelivers the

`ERROR_CODE`

arising from an attempt to access
a nil pointer in an operation with `TRANSFER_MODE`

-> ERROR_CODEDelivers the

`ERROR_CODE`

arising from a numerical exceptional
result in an operation with `ERROR_TREATMENT`

-> ERROR_CODEDelivers the

`ERROR_CODE`

arising from a stack overflow
in the call of a procedure defined with `PROCPROPS`

These values describe the way to handle various forms of error which can occur during the evaluation of operations.

*It is expected that additional ERROR_TREATMENTs will
be needed.*

The token is applied to the arguments encoded in thetoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> ERROR_TREATMENT

`BITSTREAM`

`ERROR_TREATMENT`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

control: EXP INTEGER(v)e1: BITSTREAM ERROR_TREATMENTe2: BITSTREAM ERROR_TREATMENT -> ERROR_TREATMENT

-> ERROR_TREATMENTIf an operation with a

`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

lab: LABEL -> ERROR_TREATMENT

`ERROR_TREATMENT`

which requires
that control be passed to
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.*

The list oftrap_list: LIST(ERROR_CODE) -> ERROR_TREATMENT

`ERROR_CODES`

in `ERROR_TREATMENT`

The observations on canonical ordering in *error_jump* apply
equally here.

-> ERROR_TREATMENT

`ERROR_TREATMENT`

which will only be
used in constructions with integer operands and delivering `EXP`

`INTEGER`

(`VARIETY`

will be discarded (see Representing integers).

-> ERROR_TREATMENT

`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.*

`EXP`

s are pieces of TDF which are translated into program.
`EXP`

is by far the richest `SORT`

. There are
few primitive `EXP`

s: most of the constructions take arguments
which are a mixture of `EXP`

s and other `SORT`

s.
There are constructs delivering `EXP`

s that correspond
to the declarations, program structure, procedure calls, assignments,
pointer manipulation, arithmetic operations, tests etc. of programming
languages.

The token is applied to the arguments encoded in thetoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> EXPx

`BITSTREAM`

`EXP`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

control: EXP INTEGER(v)e1: BITSTREAM EXPxe2: BITSTREAM EXPy-> EXP (control?x:y)

The absolute value of the result produced byov_err: ERROR_TREATMENTarg1: EXP INTEGER(v) -> EXP INTEGER(v)

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)

`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 `OFFSET`

s
may be added to the result, but the only other useful operation on
the result of adding a number of `OFFSET`

s 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
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.*

The arguments are evaluated producing integer values of the samearg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `VARIETY`

. The result
is delivered with the same `SHAPE`

as the arguments.

result_shape: SHAPEp: EXP PROCparams: LIST(EXP)var_param: OPTION(EXP) -> EXPresult_shape

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 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 7.9.

result_shape: SHAPEprcprops: OPTION(PROCPROPS)p: EXP PROCcallers_intro: LIST(OTAGEXP)callee_pars: CALLEESpostlude: EXP TOP -> EXPresult_shape

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 R*i* be the value of the `EXP`

of the i*th*
`OTAGEXP`

in *callers_intro* and T*i* be its
`TAG`

(if it is present). Let E*i* be the i*th*
value in *callee_pars*.

Let r*i* be the i*th* formal caller parameter `TAG`

of *p*.

Let e*i* be the i*th* formal callee parameter `TAG`

of *p*.

Each R*i* is used to initialise a variable which is identified
by r*i*; there will be exactly as many R*i* as r*i*.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 E*i* to initialise a
variable identified with e*i*; there will be exactly as many
E*i* as e*i*. 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 T*i*
(if present) with the contents of the variable identified by r*i*.
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 R*i* in order;
the alignment and padding of each individual R*i* will be given
by an exact application of *parameter_alignment* on the
`SHAPE`

of R*i*. Each r*i* is then identified
with a pointer to the copy of R*i* within the compound variable;
there will be at least as many R*i* as r*i*. 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 E*i*
in order (just as for *var_callers*). Each e*i* is identified
with a pointer to the copy of E*i* within the generated space;
there will be at least as many e*i* as E*i*. 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*.

The value produced byarg1: EXP POINTER(x)arg2: EXPy-> EXP TOP

*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 Overlapping and Incomplete assignment.

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

The value produced bymd: TRANSFER_MODEarg1: EXP POINTER(x)arg2: EXPy-> EXP TOP

`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 Overlapping and Incomplete assignment.

The value delivered byarg1: EXP POINTER(x)arg2: EXP OFFSET(y,z)arg3: EXP BITFIELD(v) -> EXP TOP

*x* will include *y* and *z* will include *v*.

*arg2*, `BITFIELD`

(*v*) will be
*variety-enclosed* (see section 7.24).

The value delivered bymd: TRANSFER_MODEarg1: EXP POINTER(x)arg2: EXP OFFSET(y,z)arg3: EXP BITFIELD(v) -> EXP TOP

`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 7.24).

The bitfield ofv: BITFIELD_VARIETYarg1: EXP POINTER(x)arg2: EXP OFFSET(y,z) -> EXP BITFIELD(v)

`BITFIELD_VARIETY`

*x* will include *y* and *z* will include *v*.

*arg2*, `BITFIELD`

(*v*) will be *variety_enclosed*
(see section 7.24).

The bitfield ofmd: TRANSFER_MODEv: BITFIELD_VARIETYarg1: EXP POINTER(x)arg2: EXP OFFSET(y,z) -> EXP BITFIELD(v)

`BITFIELD_VARIETY `

`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 7.24).

exhaustive: BOOLcontrol: EXP INTEGER(v)branches: LIST(CASELIM) -> EXP (exhaustive? BOTTOM : TOP)

`CASELIM`

(see section 5.13). If `SHAPE TOP`

. The order in which the comparisons are made
is undefined.
The sets of `SIGNED_NAT`

s in *branches* will be disjoint.

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

v: VARIETYarg1: EXP BITFIELD(bv) -> EXP INTEGER(v)

`INTEGER`

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

flpt_err: ERROR_TREATMENTr: FLOATING_VARIETYarg1: EXP FLOATING(f) -> EXP FLOATING(r)

`FLOATING_VARIETY`

Either *r* and *f* will both real or both complex.

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

ov_err: ERROR_TREATMENTr: VARIETYarg1: EXP INTEGER(v) -> EXP INTEGER(r)

`VARIETY`

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_VARIETYarg1: EXP INTEGER(v) -> EXP BITFIELD(bv)

`BITFIELD`

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

Delivers the complex conjugate ofc: EXP FLOATING(cv) -> EXP FLOATING(cv)

*cv* will be a complex floating variety.

sha: SHAPEarg1: EXP COMPOUND(EXP OFFSET(x,y))arg2: EXP OFFSET(x,alignment(sha)) -> EXPsha

`COMPOUND`

value.
The component of this value at the `OFFSET`

given by `SHAPE`

*arg2* will be a constant and non-negative (see
Constant evaluation).

If *sha* is a `BITFIELD`

then *arg2*, *sha*
will be *variety_enclosed* (see section
7.24).

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

altlab_intro: LABELfirst: EXPxalt: EXPz-> EXP (xLUBz)

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 Least Upper Bound.

A value ofs: SHAPEarg1: EXP POINTER(x) -> EXPs

`SHAPE`

*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.
*

A value ofmd: TRANSFER_MODEs: SHAPEarg1: EXP POINTER(x) -> EXPs

`SHAPE`

`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 value delivered by *arg1* is a null pointer the effect
is undefined.

-> EXP POINTER(A value offa)

`SHAPE POINTER`

(`ACCESS`

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 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_TREATMENTov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

,
`SHAPE`

as the arguments. Different occurrences of
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 Division and modulus for the definitions of D1, D2, M1 and M2.

div_by_0_err: ERROR_TREATMENTov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `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 Division and modulus for the definitions of D1, D2, M1 and M2.

div_by_0_err: ERROR_TREATMENTov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `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 Division and modulus for the definitions of D1, D2, M1 and M2.

fa: ALIGNMENTy: ALIGNMENTt: TAGx-> EXP OFFSET(fa,y)

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 7.10.

Delivers anproctag: TAG PROC -> EXP OFFSET(locals_alignment, {})

`OFFSET`

of a space sufficient to contain all
the variables and identifications, explicit or implicit in the procedure
identified by
*proctag* will be defined in the current `CAPSULE`

by a
`TAGDEF`

identification of a *make_proc* or a
*make_general_proc*.

Any attempt to use this operation to produce code will result in a failure of the installation process.message: STRING(k, n)-> EXP BOTTOM

flpt_err: ERROR_TREATMENTf: FLOATING_VARIETYarg1: EXP INTEGER(v) -> EXP FLOATING(f)

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 Floating point errors.

flpt_err: ERROR_TREATMENTarg1: EXP FLOATING(f) -> EXP FLOATING(f)

`FLOATING_VARIETY`

, `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 Floating point accuracy.

flpt_err: ERROR_TREATMENTarg1: EXP FLOATING(f)arg2: EXP FLOATING(f) -> EXP FLOATING(f)

`FLOATING_VARIETY`

, `SHAPE`

as the arguments.
If there is a floating point error it is handled by *flpt_err*.
See Floating point errors.

See also Floating point accuracy.

flpt_err: ERROR_TREATMENTarg1: EXP FLOATING(f)arg2: EXP FLOATING(f) -> EXP FLOATING(f)

`FLOATING_VARIETY`

, `SHAPE`

as the arguments.
If there is a floating point error it is handled by *flpt_err*.
See Floating point errors.

See also Floating point accuracy.

The maximum of the values delivered byflpt_err: ERROR_TREATMENTarg1: EXP FLOATING(f)arg2: EXP FLOATING(f) -> EXP FLOATING(f)

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

See also Floating point accuracy.

The minimum of the values delivered byflpt_err: ERROR_TREATMENTarg1: EXP FLOATING(f)arg2: EXP FLOATING(f) -> EXP FLOATING(f)

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

See also Floating point accuracy.

The arguments,flpt_err: ERROR_TREATMENTarg1: LIST(EXP) -> EXP FLOATING(f)

`FLOATING_VARIETY`

, `SHAPE`

as the arguments.
If there is a floating point error it is handled by *flpt_err*.
See Floating point errors.

*Note that separate floating_mult operations cannot in general be
combined, because rounding errors need to be controlled. The reason
for allowing floating_mult 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 Floating point accuracy.

flpt_err: ERROR_TREATMENTarg1: EXP FLOATING(f) -> EXP FLOATING(f)

`FLOATING_VARIETY`

, `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 Floating point accuracy.

The arguments,flpt_err: ERROR_TREATMENTarg1: LIST(EXP) -> EXP FLOATING(f)

`FLOATING_VARIETY`

, `SHAPE`

as
the arguments.
If there is a floating point error it is handled by *flpt_err*.
See 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 Floating point accuracy.

The result offlpt_err: ERROR_TREATMENTarg1: EXP FLOATING(f)arg2: EXP INTEGER(v) -> EXP FLOATING(f)

If there is a floating point error it is handled by *flpt_err*.
See Floating point errors.

See also Floating point accuracy.

prob: OPTION(NAT)flpt_err: ERROR_TREATMENTnt: NTESTdest: LABELarg1: EXP FLOATING(f)arg2: EXP FLOATING(f) -> EXP TOP

`FLOATING_VARIETY`

,
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 Floating point errors.

See also Floating point accuracy.

Control passes to thedest: LABEL -> EXP BOTTOM

`EXP`

labelled

arg1: EXP POINTER({code}) -> EXP BOTTOM

`POINTER(`

`})`

by `LABEL`

.
If *arg1* delivers a null `POINTER`

the effect is
undefined.

opt_access: OPTION(ACCESS)name_intro: TAGxdefinition: EXPxbody: EXPy-> EXPy

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
sequence.

If the result of this construction is discarded,arg1: EXPx-> EXPx

arg1: EXPc-> EXP FLOATING (float_of_complex(c))

Any tag used as an argument of aninit: EXPs-> EXPs

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 7.29.

prob: OPTION(NAT)nt: NTESTdest: LABELarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP TOP

`VARIETY`

,
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.

The listslabs_intro: LIST(LABEL)starter: EXPxplaces: LIST(EXP) -> EXPw

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
`LABEL`

s in *labs_intro* or any other jump to one
of these `LABEL`

s 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 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 `LABEL`

s in *labs_intro*,
is the evaluation of *starter* and all the elements of *places*.

If the last use ofx: EXP OFFSET(y,z) -> EXP POINTER(alloca_alignment)

`POINTER`

allocated with
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 `ALIGNMENT`

s which can be produced
by
*alignment* from any `SHAPE`

. See
Special alignments.

Thearg1: EXP OFFSET(x,y) -> EXP POINTER(alloca_alignment)

*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 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 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*.

Thea: EXP OFFSET(x,y)p: EXP POINTER(alloca_alignment) -> EXP TOP

`POINTER`

, `POINTER`

will have been created
by Any subsequent use of pointers to the spaces no longer used will be undefined.

-> EXP TOPEvery space allocated by

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

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 `TAG`

s declared to have *long_jump_access* will
be defined at the re-entry.

If *arg2* delivers a null
`POINTER(`

{*code*`})`

the effect is undefined.

c: FLOATING_VARIETYarg1: EXP FLOATING(f)arg2: EXP FLOATING(f) -> EXP FLOATING(c)

Delivers a complex number with *arg1* delivering the real part
and *arg2* the imaginary.

Let thearg1: EXP OFFSET(base,y)arg2: LIST(EXP) -> EXP COMPOUND(arg1)

The components *x*[2 * *k*] are values which are to be placed
at `OFFSET`

s given by *x*[2 * *k* - 1]. These
`OFFSET`

s will be constants and non-negative.

The `OFFSET`

*x*[2 * *k* - 1] will have the
`SHAPE`

`OFFSET`

(*z**k*,
*alignment*(*shape*(*x*[2 * *k*]))), where
*shape* gives the `SHAPE`

of the component and
*base* includes *z**k*.

*arg1* will be a constant non-negative `OFFSET`

, see
offset_pad.

The values *x*[2 * *k* - 1] will be such that the components
when in place either do not overlap or exactly coincide, in the sense
that the `OFFSET`

s are equal and the values have the same
`SHAPE`

. If they coincide the corresponding values *x*[2
* *k*] will have `VARIETY SHAPE`

s and will be *ored*
together.

The `SHAPE`

of a *x*[2 * *k*] component can be
`TOP`

. In this case the component is evaluated, but no
value is placed at the corresponding `OFFSET`

.

If *x[2 * k]* is a `BITFIELD`

then *x[2 * k - 1]*,
*shape(x[2 * k])* will be *variety-enclosed* (see
section 7.24).

f: FLOATING_VARIETYrm: ROUNDING_MODEnegative: BOOLmantissa: STRING(k, n)base: NATexponent: SIGNED_NAT -> EXP FLOATING(f)

*mantissa* will be a `STRING`

of 8-bit integers, each
of which is either 46 or is greater than or equal to 48. Those values,
*c*, which lie between 48 and 63 will represent the digit *c*-48.
A decimal point is represented by 46.

The `BOOL`

*negative* determines the sign of the result,
if true the result will be negative, if false, positive.

A floating point number, *mantissa**(*base*^{exponent})
is created and rounded to the representation of *f* as specified
by *rm*. *rm* will not be *round_as_state*. *mantissa*
is read as a sequence of digits to base *base* and may contain
one point symbol.

*base* will be one of the numbers 2, 4, 8, 10, 16. Note that
in base 16 the digit 10 is represented by the character number 58
etc.

The result will lie in *f*.

Evaluation ofresult_shape: SHAPEprcprops: OPTION(PROCPROPS)caller_intro: LIST(TAGSHACC)callee_intro: LIST(TAGSHACC)body: EXP BOTTOM -> EXP PROC

`PROC`

.
When this procedure is applied to parameters using `TAG`

s in `POINTER`

s to these spaces. The lifetime
of these `TAG`

s is the evaluation of
The `SHAPE`

of *body* will be `BOTTOM`

.
*caller_intro* and *callee_intro* may be empty.

The `TAG`

s introduced in the parameters will not be reused
within the current `UNIT`

.

The `SHAPE`

s in the parameters specify the `SHAPE`

of the corresponding `TAG`

s.

The `OPTION(ACCESS)`

(in *params_intro*) specifies
the `ACCESS`

properties of the corresponding parameter,
just as for a variable declaration.

In *body* the only `TAG`

s which may be used as an
argument of *obtain_tag* are those which are declared by
*identify* or *variable* constructions in *body* and
which are in scope, or `TAG`

s which are declared by
*make_id_tagdef*, *make_var_tagdef* or *common_tagdef*
or are in *caller_intro* or *callee_intro*. If a *make_proc*
occurs in *body* its `TAG`

s are not in scope.

The argument of every *return* or *untidy_return* construction
in *body* will have `SHAPE`

*result_shape*. Every
*apply_general_proc* using the procedure will specify the
`SHAPE`

of its result to be *result_shape*.

The presence or absence of each of the `PROCPROPS`

*var_callers*, *var_callees, check_stack* and *untidy*
in
*prcprops* will be reflected in every *apply_general_proc*
or
*tail_call* on this procedure.

The definition of the canonical ordering of the evaluation of
*apply_general_proc* gives the definition of these
`PROCPROPS`

.

If *prcprocs* contains *check_stack*, a TDF exception will
be raised if the static space required for the procedure call (in
the sense of *env_size*) would exceed the limit given by
*set_stack_limit*.

If *prcprops* contains *no_long_jump_dest*, the body of
the procedure will never contain the destination label of a
*long_jump*.

For notes on the intended implementation of procedures see section 7.9.

An integer value is delivered of which the value is given byv: VARIETYvalue: SIGNED_NAT -> EXP INTEGER(v)

`VARIETY`

by `SIGNED_NAT`

Alab: LABEL -> EXP POINTER({code})

`POINTER(`

`})`

Creates an array ofarg1: LIST(EXP) -> EXP NOF(n,s)

`SHAPE`

*n* will not be zero.

Anv: VARIETYstr: STRING(k, n)-> EXP NOF(n, INTEGER(v))

`NOF INTEGER`

is delivered. The conversions are carried
out as if the elements of `INTEGER`

(

-> EXP POINTER({Makes a nullcode})

`POINTER`

({
All null `POINTER`

({*code*}) are equal to each other
and unequal to any other `POINTER`

s.

-> EXP PROCA null

`PROC`

is created and delivered. The null
`PROC`

may be tested for by using
All null `PROC`

are equal to each other and unequal to
any other `PROC`

.

A nulla: ALIGNMENT -> EXP POINTER(a)

`POINTER`

(`POINTER`

may be tested for by
*a* will not include *code*.

All null `POINTER`

(*x*) are equal to each other and
unequal to any other `POINTER`

(*x*).

Evaluation ofresult_shape: SHAPEparams_intro: LIST(TAGSHACC)var_intro: OPTION(TAGACC)body: EXP BOTTOM -> EXP PROC

`PROC`

. When this procedure is applied to parameters using
`TAG`

s in `POINTER`

s to these spaces. The lifetime
of these
`TAG`

s is the evaluation of
If *var_intro* is present, it may be used for one of two purposes,
with different consequences for corresponding uses of *apply_proc*.
See section 7.9. The
`ALIGNMENT`

, *var_param_alignment*, includes the set
union of all the `ALIGNMENT`

s which can be produced by
*alignment* from any `SHAPE`

. Note that *var_intro*
does not contain an `ACCESS`

component and so cannot be
marked *visible*. Hence it is not a possible argument of
*env_offset*. If present, *var_intro* is an original pointer.

The `SHAPE`

of *body* will be `BOTTOM`

.
*params_intro* may be empty.

The `TAG`

s introduced in the parameters will not be reused
within the current `UNIT`

.

The `SHAPE`

s in the parameters specify the `SHAPE`

of the corresponding `TAG`

s.

The `OPTION(ACCESS`

) (in *params_intro*) specifies
the `ACCESS`

properties of the corresponding parameter,
just as for a variable declaration.

In *body* the only `TAG`

s which may be used as an
argument of *obtain_tag* are those which are declared by
*identify* or *variable* constructions in *body* and
which are in scope, or `TAG`

s which are declared by
*make_id_tagdef*, *make_var_tagdef* or *common_tagdef*
or are in *params_intro* or *var_intro*. If a *make_proc*
occurs in *body* its `TAG`

s are not in scope.

The argument of every *return* construction in *body* will
have `SHAPE`

*result_shape*. Every *apply_proc*
using the procedure will specify the `SHAPE`

of it result
to be *result_shape*.

For notes on the intended implementation of procedures see section 7.9.

This creates a POINTER suitable for use withstack_base: EXP POINTER(fa)frame_size: EXP OFFSET(locals_alignment,x)alloc_size: EXP OFFSET(alloca_alignment,y) -> EXP POINTER(fb)

*fa* and *fb* will include *locals_alignment* and,
if
*alloc_size* is not the zero offset, will also contain
*alloca_alignment*.

The result will be the same as if given by:

Assume *stack_base* is the current frame-pointer as given by
*current_env* in a hypothetical procedure P with *env_size*
equal to *frame_size* and which has generated *alloc_size*
by a *local_alloc*. If P then calls Q, the result will be the
same as that of a *current_env* performed immediately in the
body of Q.

If the following construction is performed:

set_stack_limit(make_stack_limit(current_env, F, A))

the frame space and local_alloc space that would be available for
use by this supposed call of Q will not be reused by procedure calls
with *check_stack* or uses of *local_alloc_check* after
the *set_stack_limit*. Any attempt to do so will raise a TDF
exception, *stack_overflow*.

-> EXP TOP

`SHAPE TOP`

(i.e.

Thiss: SHAPE -> EXPs

`EXP`

creates some value with the representation of
the `SHAPE`

`EXP`

. But if it is
used for arithmetic or as a `POINTER`

for taking Installers will usually be able to implement this operation by producing no code.

*Note that a floating point NaN is a possible value for this purpose.*

The `SHAPE`

*s* will not be `BOTTOM`

.

The arguments will be evaluated and the maximum of the values delivered is the result.arg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

The arguments will be evaluated and the minimum of the values delivered is the result.arg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

ov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `SHAPE`

as the arguments.
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*.

The arguments are evaluated to producemd: TRANSFER_MODEarg1: EXP POINTER(x)arg2: EXP POINTER(y)arg3: EXP OFFSET(z,t) -> EXP TOP

`TRANSFER_MODE`

(q.v.).
*x* will include *z* and *y* will include *z*.

*sz* will be a non-negative `OFFSET`

, see
offset_pad.

If the spaces of size *sz* to which *p1* and *p2* point
do not lie entirely within the spaces indicated by the original pointers
from which they are derived, the effect of the operation is undefined.

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

See Overlapping.

ov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `SHAPE`

as the arguments.
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*.

n: NATarg1: EXPx-> EXP NOF(n,x)

`NOF`

value is delivered
which contains
Producers are encouraged to use *n_copies* to initialise arrays
of known size.

ov_err: ERROR_TREATMENTarg1: EXP INTEGER(v) -> EXP INTEGER(v)

`SHAPE`

as the argument.
`VARIETY`

being
used to represent *v*, an overflow error is caused and is handled
in the way specified by *ov_err*.

The argument is evaluated producing an integer value, ofarg1: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `VARIETY`

. The result
is delivered as the result of the construct, with the same
`SHAPE`

as the arguments.

The value with which thet: TAGx-> EXPx

`TAG`

`SHAPE`

of the result is the `SHAPE`

of
the value with which the `TAG`

is bound.

The two arguments deliverarg1: EXP OFFSET(x,y)arg2: EXP OFFSET(z,t) -> EXP OFFSET(x,t)

`OFFSET`

s. The result is the
sum of these `OFFSET`

s, as an `OFFSET`

.
*y* will include *z*.

*The effect of the constraint "y will include z" is that,
in the simple representation of pointer arithmetic, this operation
can be represented by addition. offset_add can lose information, so
that offset_subtract does not have the usual relation with it.*

The two arguments deliverv: VARIETYarg1: EXP OFFSET(x,x)arg2: EXP OFFSET(x,x) -> EXP INTEGER(v)

`OFFSET`

s, `INTEGER`

of `VARIETY`

,
The value produced by *arg2* will be non-zero.

The result is thearg1: EXP OFFSET(x,x)arg2: EXP INTEGER(v) -> EXP OFFSET(x,x)

`OFFSET`

produced by `OFFSET`

(
The value produced by *arg2* will be greater than zero.

The following identity will apply for all A and n:

*offset_mult*(*offset_div_by_int*(A, n), n) = A

The two arguments deliverarg1: EXP OFFSET(x,y)arg2: EXP OFFSET(z,y) -> EXP OFFSET(unite_alignments(x,z),y)

`OFFSET`

s. The result is the
maximum of these `OFFSET`

s, as an `OFFSET`

.
See Comparison of pointers and offsets.

*In the simple memory model this operation is represented by maximum.
The constraint that the second ALIGNMENT parameters are
both y is to permit the representation of OFFSETs in
installers by a simple homomorphism.*

The first argument gives anarg1: EXP OFFSET(x,x)arg2: EXP INTEGER(v) -> EXP OFFSET(x,x)

`OFFSET`

,
The result shall be equal to *offset_adding off n*
times to *offset_zero*(*x*).

The inverse of the argument is delivered.arg1: EXP OFFSET(x,x) -> EXP OFFSET(x,x)

*In the simple memory model this can be represented by negate.*

a: ALIGNMENTarg1: EXP OFFSET(z,t) -> EXP OFFSET(unite_alignments(z,a),a)

`OFFSET`

at which a value of `ALIGNMENT`

`OFFSET`

of the same `SHAPE`

as the result which
is greater than or equal to
*off* will be a non-negative `OFFSET`

, that is it
will be greater than or equal to a zero `OFFSET`

of the
same `SHAPE`

in the sense of *offset_test*.

*In the simple memory model this operation can be represented by
((off + a - 1) / a) * a. In the simple model this is the only operation
which is not represented by a simple corresponding integer operation.*

The two arguments deliver offsets,arg1: EXP OFFSET(x,y)arg2: EXP OFFSET(x,z) -> EXP OFFSET(z,y)

Note that *x* will include *y*, *x* will include *z*
and *z* will include *y*, by the constraints on
`OFFSET`

s.

*offset_subtract and offset_add do not have the conventional relationship
because offset_add can lose information, which cannot be regenerated
by offset_subtract.*

prob: OPTION(NAT)nt: NTESTdest: LABELarg1: EXP OFFSET(x,y)arg2: EXP OFFSET(x,y) -> EXP TOP

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.

*a greater_than_or_equal b* is equivalent to
*offset_max*(*a*, *b*) = *a*, and similarly for
the other comparisons.

*In the simple memory model this can be represented by integer_test.*

A zero offset ofa: ALIGNMENT -> EXP OFFSET(a,a)

`SHAPE OFFSET`

(
*offset_pad*(*b*, *offset_zero*(*a*)) is a zero
offset of `SHAPE OFFSET`

(*unite_alignments*(*a*,
*b*), *b*).

The arguments are evaluated producing integer values of the samearg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `VARIETY`

. The
result is delivered as the result of the construct, with the same
`SHAPE`

as the arguments.

ov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `SHAPE`

as the arguments.
`VARIETY`

being
used to represent *v*, an overflow error is caused and is handled
in the way specified by *ov_err*.

prob: OPTION(NAT)nt: NTESTdest: LABELarg1: EXP POINTER(x)arg2: EXP POINTER(x) -> EXP TOP

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.

The effect of this construction is the same as:

*offset_test*(*prob, nt*, *dest*, *subtract_ptrs*(*arg1
*,
*arg2*), *offset_zero*(*x*))

*In the simple memory model this construction can be represented
by integer_test.*

ov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(w) -> EXP INTEGER(v)

`VARIETY`

being
used to represent *v*, an overflow error is caused and is handled
in the way specified by *ov_err*.

prob: OPTION(NAT)nt: NTESTdest: LABELarg1: EXP PROCarg2: EXP PROC -> EXP TOP

`PROC`

values,
If *a nt b*, this construction yields `TOP`

. Otherwise
control passes to *dest*.

*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.

Two `PROC`

s are equal if they were produced by the same
instantiation of *make_proc* or if they were both made with
*make_null_proc*. Otherwise they are unequal.

The integeruses: NAT -> EXP TOP

All uses of *profile* in the same capsule are to the same scale.
They will be mutually consistent.

arg1: EXPc-> EXP FLOATING (float_of_complex(c))

div_by_0_err: ERROR_TREATMENTov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `SHAPE`

as the arguments. Different occurrences of The following equivalence shall hold:

if all thex = plus(mult(div0(x, y), y), rem0(x, y))

`ERROR_TREATMENT`

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

If *b* is not zero and *div0*(*a*, *b*) cannot
be expressed in the `VARIETY`

being used to represent *v*
an overflow may occur in which case it is handled by *ov_err*.

Producers may assume that suitable masking and *rem0* by a power
of two yield equally good code.

See Division and modulus for the definitions of D1, D2, M1 and M2.

div_by_0_err: ERROR_TREATMENTov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `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 *div1*(*a*, *b*) cannot
be expressed in the `VARIETY`

being used to represent *v*
an overflow may occur, in which case it is handled by *ov_err*.

Producers may assume that suitable masking and *rem1* by a power
of two yield equally good code.

See Division and modulus for the definitions of D1, D2, M1 and M2.

div_by_0_err: ERROR_TREATMENTov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `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 *div2*(*a*, *b*) cannot
be expressed in the `VARIETY`

being used to represent *v*
an overflow may occur, in which case it is handled by *ov_err*.

Producers may assume that suitable masking and *rem2* by a power
of two yield equally good code if the lower bound of *v* is zero.

See Division and modulus for the definitions of D1, D2, M1 and M2.

replab_intro: LABELstart: EXP TOPbody: EXPy-> EXPy

If *body* produces a result, this is the result of the whole
construction. However if *goto* or any other jump to
*replab_intro* is encountered during the evaluation then the
current evaluation stops and *body* is evaluated again. In the
canonical order all evaluated components are completely evaluated
before any of the next iteration of *body*. The lifetime of
*replab_intro* is the evaluation of *body*.

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.

arg1: EXPx-> EXP BOTTOM

Since the *return* construct can never produce a value, the
`SHAPE`

of its result is `BOTTOM`

.

All uses of *return* in the *body* of a *make_proc*
or
*make_general_proc* will have *arg1* with the same
`SHAPE`

.

lab_val: EXP POINTERcode_alignment-> EXP BOTTOM

The evaluation of the immediately enclosing procedure ceases and control
is passed to the calling procedure at the label given by *lab_val*.

flpt_err: ERROR_TREATMENTmode: ROUNDING_MODEr: VARIETYarg1: EXP FLOATING(f) -> EXP INTEGER(r)

`VARIETY`

, `ROUNDING_MODE`

,
If *f* is complex the result is derived from the real part of
*arg1*.

If there is a floating point error it is handled by *flpt_err*.
See Floating point errors.

The value delivered byarg1: EXP INTEGER(v)arg2: EXP INTEGER(w) -> EXP INTEGER(v)

*arg2* will be non-negative and will be strictly less than the
number of bits needed to represent *v*.

The use of this construct assumes knowledge of the representational
variety of *v*.

The value delivered byarg1: EXP INTEGER(v)arg2: EXP INTEGER(w) -> EXP INTEGER(v)

*arg2* will be non-negative and will be strictly less than the
number of bits needed to represent *v*.

The use of this construct assumes knowledge of the representational
variety of *v*.

The statements are evaluated in the same order as the list,statements: LIST(EXP)result: EXPx-> EXPx

A canonical order is one in which all the components of each statement
are completely evaluated before any component of the next statement
is started. A similar constraint applies between the last statement
and the *result*. The actual order in which the statements and
their components are evaluated shall be indistinguishable in all observable
effects (apart from time) from a canonical order.

Note that this specifically includes any defined error handling. However, if in any canonical order the effect of the program is undefined, the actual effect of the sequence is undefined.

Hence constructions with *impossible* error handlers may be performed
before or after those with specified error handlers, if the resulting
order is otherwise acceptable.

lim: EXP POINTER({locals_alignment, alloca_alignment}) -> EXP TOP

Any later *apply_general_proc* with `PROCPROPS`

including
*check_stack* up to the dynamically next *set_stack_limit*
will check that the frame required for the procedure will be within
the frame stack limit. If it is not, normal execution is stopped and
a TDF exception with ERROR_CODE *stack_overflow* is raised.

Any later *local_alloc_check* will check that the locally allocated
space required is within the local_alloc stack limit. If it is not,
normal execution is stopped and a TDF exception with ERROR_CODE
*stack_overflow* is raised.

This construction delivers the "size" of a value of the givens: SHAPE -> EXP OFFSET(alignment(s), {})

`SHAPE`

.
Suppose that a value of `SHAPE`

, *s*, is placed in
a space indicated by a `POINTER`

(*x*), *p*, where
*x* includes *alignment(s*). Suppose that a value of
`SHAPE`

, *t*, where *a* is
*alignment*(*t*) and *x* includes *a*, is placed
at

*add_to_ptr*(*p*, *offset_pad(a, shape_offset*(*s*)))

Then the values shall not overlap. This shall be true for all legal
*s*, *x* and *t*.

ov_err: ERROR_TREATMENTarg1: EXP INTEGER(v)arg2: EXP INTEGER(w) -> EXP INTEGER(v)

`SHAPE`

as
*b* will be non-negative and will be strictly less than the number
of bits needed to represent *v*.

`VARIETY`

being
used to represent *v*, an overflow error is caused and is handled
in the way specified by *ov_err*.

Producers may assume that *shift_left* and multiplication by
a power of two yield equally efficient code.

arg1: EXP INTEGER(v)arg2: EXP INTEGER(w) -> EXP INTEGER(v)

`SHAPE`

as
*b* will be non-negative and will be strictly less than the number
of bits needed to represent *v*.

If the lower bound of *v* is negative, the sign will be propagated.

arg1: EXP POINTER(y)arg2: EXP POINTER(x) -> EXP OFFSET(x,y)

`OFFSET`

from
Note that *add_to_ptr*(*p2*, *r*) = *p1*.

prcprops: OPTION(PROCPROPS)p: EXP PROCcallee_pars: CALLEES -> EXP BOTTOM

`CALLEES`

given by `PROCPROPS`

The result of the call is delivered as the result of the immediately
enclosing proc in the sense of *return*. The `SHAPE`

of the result of *p* will be identical to the `SHAPE`

specified as the result of immediately enclosing procedure.

No pointers to any callee parameters, variables, identifications or
local allocations defined in immediately enclosing procedure will
be accessed either in the body of *p* or after the return.

The presence or absence of each of the `PROCPROPS`

*check_stack* and *untidy*, in *prcprops* will be reflected
in the `PROCPROPS`

of the immediately enclosing procedure.

arg1: EXPx-> EXP BOTTOM

*untidy_return* can only occur in a procedure defined by
*make_general_proc* with `PROCPROPS`

including
*untidy*.

opt_access: OPTION(ACCESS)name_intro: TAG POINTER(alignment(x))init: EXPxbody: EXPy-> EXPy

`SHAPE`

`POINTER`

pointing
to the allocated space is bound to `POINTER`

to this space. The lifetime of
The value delivered by *variable* is that produced by *body*.

If *opt_access* contains *visible*, it means that the contents
of the space may be altered 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 from the variable 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 `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 order in which the constituents of *init* and *body*
are evaluated shall be indistinguishable in all observable effects
(apart from time) from completely evaluating *init* before starting
*body*. See the note about order in
sequence.

When compiling languages which permit uninitialised variable declarations,
*make_value* may be used to provide an initialisation.

The arguments are evaluated producing integer values of the samearg1: EXP INTEGER(v)arg2: EXP INTEGER(v) -> EXP INTEGER(v)

`VARIETY`

, `VARIETY`

. The
result is delivered as the result of the construct, with the same
`SHAPE`

as the arguments.

An `EXTERNAL`

defines the classes of external name available
for connecting the internal names inside a `CAPSULE`

to
the world outside the `CAPSULE`

.

s: BYTE_ALIGN TDFIDENT(n) -> EXTERNAL

`EXTERNAL`

identified
by the `TDFIDENT`

u: BYTE_ALIGN UNIQUE -> EXTERNAL

`EXTERNAL`

identified
by the `UNIQUE`

This construct is redundant and should not be used.s: BYTE_ALIGN TDFIDENTprev: TDFINT -> EXTERNAL

An auxiliary `SORT`

providing a list of `LINKEXTERN`

.

el: SLIST(LINKEXTERN) -> EXTERN_LINK

`SLIST`

(`EXTERN_LINK`

)
to express the links between the linkable entities and the named (by
`EXTERNAL`

s) values outside the `CAPSULE`

.

These describe kinds of floating point number.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> FLOATING_VARIETY

`FLOATING_VARIETY`

*token_value* in the `CAPSULE`

then *token_args*
is a `BITSTREAM`

encoding of the `SORT`

s of
its parameters, in the order specified.

Thecontrol: EXP INTEGER(v)e1: BITSTREAM FLOATING_VARIETYe2: BITSTREAM FLOATING_VARIETY -> FLOATING_VARIETY

base: NATmantissa_digs: NATmin_exponent: NATmax_exponent: NAT -> FLOATING_VARIETY

*mantissa_digs* is the required number of *base* digits,
*q*, such that any number with *q* digits can be rounded
to a floating point number of the variety and back again without any
change to the *q* digits.

*min_exponent* is the negative of the required minimum integer
such that *base* raised to that power can be represented as a
non-zero floating point number in the `FLOATING_VARIETY`

.

*max_exponent* is the required maximum integer such that
*base* raised to that power can be represented in the
`FLOATING_VARIETY`

.

A TDF translator is required to make available a representing
`FLOATING_VARIETY`

such that, if only values within the
given requirements are produced, no overflow error will occur. Where
several such representative `FLOATING_VARIETY`

s exist,
the translator will choose one to minimise space requirements or maximise
the speed of operations.

All numbers of the form xb1 M**base N+1-q* are required to be
represented exactly where M and N are integers such that

*base**q-1* M < *base**q*

-*min_exponent* N *max_exponent*

Zero will also be represented exactly in any `FLOATING_VARIETY`

.

Abase: NATmantissa_digs: NATmin_exponent: NATmax_exponent: NAT -> FLOATING_VARIETY

`FLOATING_VARIETY`

described by

csh: SHAPE -> FLOATING_VARIETY

`SHAPE`

.
Delivers the `FLOATING_VARIETY`

required for the real (or
imaginary) part of a complex `SHAPE`

*csh*.

fsh: SHAPE -> FLOATING_VARIETY

`SHAPE`

.
Delivers `FLOATING_VARIETY`

required for a complex number
whose real (and imaginary) parts have `SHAPE`

*fsh*.

A `GROUP`

is a list of `UNIT`

s with the same
unit identification.

us: SLIST(UNIT) -> GROUP

`GROUPS`

. Each member
of this list has a different unit identification deduced from the

A `LABEL`

marks an `EXP`

in certain constructions,
and is used in jump-like constructions to change the control to the
labelled construction.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> LABELx

`LABEL`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

Labels are represented in TDF by integers, but they are not linkable. Hence the definition and all uses of alabelno: TDFINT -> LABEL

`LABEL`

occur in
the same `UNIT`

.

A `LINK`

expresses the connection between two variables
of the same `SORT`

.

Aunit_name: TDFINTcapsule_name: TDFINT -> LINK

`LINK`

defines a linkable entity declared inside a
`UNIT`

as `CAPSULE`

linkable entity having the same linkable entity
identification. The `CAPSULE`

linkable entity is
A `LINK`

is normally constructed by the TDF builder in
the course of resolving sharing and name clashes when constructing
a composite `CAPSULE`

.

A value of `SORT LINKEXTERN`

expresses the connection between
the name by which an object is known inside a `CAPSULE`

and a name by which it is known outside.

internal: TDFINText: EXTERNAL -> LINKEXTERN

`LINKEXTERN`

connecting
an object identified within a `CAPSULE`

by a `TAG`

,
`TOKEN`

, `AL_TAG`

or any linkable entity constructed
from `EXTERNAL`

, `EXTERNAL`

is an identifier which linkers and similar programs
can use.

ls: SLIST(LINK) -> LINKS

`SLIST`

(`LINKS`

) to
define which linkable entities within a `UNIT`

correspond
to the `CAPSULE`

linkable entities. Each `LINK`

in a `LINKS`

has the same linkable entity identification.

These are non-negative integers of unlimited size.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> NAT

`NAT`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

Thecontrol: EXP INTEGER(v)e1: BITSTREAM NATe2: BITSTREAM NAT -> NAT

arg: EXP INTEGER(v) -> NAT

Gives theerr: ERROR_CODE -> NAT

`NAT`

corresponding to the `ERROR_CODE`

`ERROR_CODE`

will give a different
`NAT`

.

n: TDFINT -> NAT

These describe the comparisons which are possible in the various
*test* constructions. Note that *greater_than* is not necessarily
the same as *not_less_than_or_equal*, since the result need not
be defined (e.g. in IEEE floating point).

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> NTEST

`NTEST`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

Thecontrol: EXP INTEGER(v)e1: BITSTREAM NTESTe2: BITSTREAM NTEST -> NTEST

-> NTESTSignifies "equal" test.

-> NTESTSignifies "greater than" test.

-> NTESTSignifies "greater than or equal" test.

-> NTESTSignifies "less than" test.

-> NTESTSignifies "less than or equal" test.

-> NTESTSignifies "not equal" test.

-> NTESTSignifies "not greater than" test.

-> NTESTSignifies "not (greater than or equal)" test.

-> NTESTSignifies "not less than" test.

-> NTESTSignifies "not (less than or equal)" test.

-> NTESTSignifies "less than or greater than" test.

-> NTESTSignifies "not less than and not greater than" test.

-> NTESTSignifies "comparable" test.

With all operands `SHAPE`

s except `FLOATING`

,
this comparison is always true.

-> NTESTSignifies "not comparable" test.

With all operands `SHAPE`

s except `FLOATING`

,
this comparison is always false.

This is a auxilliary `SORT`

used in *apply_general_proc*.

tgopt: OPTION(TAGx)e: EXPx-> OTAGEXP

`TAG`

will be bound to
the final value of caller parameter in the

`PROCPROPS`

is a set of properties ascribed to procedure
definitions and calls.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> PROCPROPS

`PROCPROPS`

.
If there is a definition for *token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters in the order specified.

Thecontrol: EXP INTEGER(v)e1: BITSTREAM PROCPROPSe2: BITSTREAM PROCPROPS -> PROCPROPS

Delivers the join ofarg1: PROCPROPSarg2: PROCPROPS -> PROCPROPS

-> PROCPROPSThe procedure body is required to check for stack overflow.

-> PROCPROPSThe procedure body is a good candidate for inlining at its application.

-> PROCPROPSThe procedure body will contain no label which is the destination of a long_jump.

-> PROCPROPSThe procedure body may be exited using an

-> PROCPROPSApplications of the procedure may have different numbers of actual callee parameters.

-> PROCPROPSApplications of the procedure may have different numbers of actual caller parameters.

`PROPS`

is an assemblage of program information. This
standard offers various ways of constructing a `PROPS`

- i.e. it defines kinds of information which it is useful to express.
These are:
- definitions of
`AL_TAG`

s standing for`ALIGNMENT`

s; - declarations of
`TAG`

s standing for`EXP`

s; - definitions of the
`EXP`

s for which`TAG`

s stand; - declarations of
`TOKEN`

s standing for pieces of TDF program; - definitions of the pieces of TDF program for which
`TOKEN`

s stand; - linkage and naming information;
- version information

`PROPS`

giving diagnostic information are described in
a separate document.
The standard can be extended by the definition of new kinds of
`PROPS`

information and new `PROPS`

constructs
for expressing them; and private standards can define new kinds of
information and corresponding constructs without disruption to adherents
to the present standard.

Each `GROUP`

of `UNIT`

s is identified by a unit
identification - a `TDFIDENT`

. All the `UNIT`

s
in that `GROUP`

are of the same kind.

In addition there is a *tld* `UNIT`

, see
The TDF encoding.

`ROUNDING_MODE`

specifies the way rounding is to be performed
in floating point arithmetic.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> ROUNDING_MODE

`ROUNDING_MODE`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

Thecontrol: EXP INTEGER(v)e1: BITSTREAM ROUNDING_MODEe2: BITSTREAM ROUNDING_MODE -> ROUNDING_MODE

-> ROUNDING_MODERound as specified by the current state of the machine.

-> ROUNDING_MODESignifies rounding to nearest. The effect when the number lies half-way is not specified.

-> ROUNDING_MODESignifies rounding toward next largest.

-> ROUNDING_MODESignifies rounding toward next smallest.

-> ROUNDING_MODESignifies rounding toward zero.

`SHAPE`

s express symbolic size and representation information
about run time values.

`SHAPE`

s are constructed from primitive `SHAPE`

s
which describe values such as procedures and integers, and recursively
from compound construction in terms of other `SHAPE`

s.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> SHAPE

`SHAPE`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

Thecontrol: EXP INTEGER(v)e1: BITSTREAM SHAPEe2: BITSTREAM SHAPE -> SHAPE

Abf_var: BITFIELD_VARIETY -> SHAPE

`BITFIELD`

is used to represent a pattern of bits which
will be packed, provided that the
A `BITFIELD_VARIETY`

specifies the number of bits and whether
they are considered to be signed.

There are very few operations on `BITFIELD`

s, which have
to be converted to `INTEGER`

s before arithmetic can be
performed on them.

An installer may place a limit on the number of bits it implements. See Permitted limits.

-> SHAPE

`BOTTOM`

is the `SHAPE`

which describes a piece
of program which does not evaluate to any result. Examples include
If `BOTTOM`

is a parameter to any other `SHAPE`

constructor, the result is `BOTTOM`

.

Thesz: EXP OFFSET(x, y) -> SHAPE

`SHAPE`

constructor `COMPOUND`

describes
cartesian products and unions.
The alignments *x* and *y* will be *alignment*(*sx*)
and *alignment*(*sy*) for some `SHAPE`

s *sx*
and *sy*.

*sz* will evaluate to a constant, non-negative `OFFSET`

(see offset_pad). The resulting
`SHAPE`

describes a value whose size is given by *sz*.

Most of the floating point arithmetic operations,fv: FLOATING_VARIETY -> SHAPE

See Representing floating point.

An installer may limit the `FLOATING_VARIETY`

s it can represent.
A statement of any such limits shall be part of the specification
of an installer. See
Representing floating point.

The different kinds ofvar: VARIETY -> SHAPE

`INTEGER`

are distinguished by having
different `VARIETY`

s. A fundamental `VARIETY`

(not a `TOKEN`

or conditional) is represented by two
`SIGNED_NAT`

s, respectively the lower and upper bounds
(inclusive) of the set of values belonging to the `VARIETY`

.
Most architectures require that dyadic integer arithmetic operations
take arguments of the same size, and so TDF does likewise. Because
TDF is completely architecture neutral and makes no assumptions about
word length, this means that the `VARIETY`

s of the two
arguments must be identical. An example illustrates this. A piece
of TDF which attempted to add two values whose `SHAPE`

s
were:

INTEGER(0, 60000)would be undefined. The reason is that without knowledge of the target architecture's word length, it is impossible to guarantee that the two values are going to be represented in the same number of bytes. On a 16-bit machine they probably would, but not on a 15-bit machine. The only way to ensure that twoandINTEGER(0, 30000)

`INTEGER`

s are going to
be represented in the same way in all machines is to stipulate that
their `VARIETY`

s are exactly the same.
When any construct delivering an `INTEGER`

of a given
`VARIETY`

produces a result which is not representable
in the space which an installer has chosen to represent that
`VARIETY`

, an integer overflow occurs. Whether it occurs
in a particular case depends on the target, because the installers'
decisions on representation are inherently target-defined.

A particular installer may limit the ranges of integers that it implements. See Representing integers.

Then: NATs: SHAPE -> SHAPE

`NOF`

constructor describes the `SHAPE`

of a value consisting of an array of `SHAPE`

,

Thearg1: ALIGNMENTarg2: ALIGNMENT -> SHAPE

`SHAPE`

constructor `OFFSET`

describes values
which represent the differences between `POINTER`

s, that
is they measure offsets in memory. It should be emphasised that these
are in general run-time values.
An `OFFSET`

measures the displacement from the value indicated
by a `POINTER`

(*arg1*) to the value indicated by a
`POINTER`

(*arg2*). Such an offset is only defined
if the `POINTER`

s are derived from the same original
`POINTER`

.

An `OFFSET`

may also measure the displacement from a
`POINTER`

to the start of a `BITFIELD_VARIETY`

,
or from the start of one `BITFIELD_VARIETY`

to the start
of another. Hence, unlike the argument of *pointer*, *arg1*
or
*arg2* may consist entirely of `BITFIELD_VARIETY`

s.

The set *arg1* will include the set *arg2*.

See Memory Model.

Aarg: ALIGNMENT -> SHAPE

`POINTER`

is a value which points to space allocated
in a computer's memory. The `POINTER`

constructor takes
an
`ALIGNMENT`

argument. This argument will not consist entirely
of `BITFIELD_VARIETY`

s. See Memory
Model.

-> SHAPE

`PROC`

is the `SHAPE`

which describes pieces
of program.

-> SHAPE

`TOP`

is the `SHAPE`

which describes pieces
of program which return no useful value.

These are positive or negative integers of unbounded size.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> SIGNED_NAT

`SIGNED_NAT`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

Thecontrol: EXP INTEGER(v)e1: BITSTREAM SIGNED_NATe2: BITSTREAM SIGNED_NAT -> SIGNED_NAT

arg: EXP INTEGER(v) -> SIGNED_NAT

neg: TDFBOOLn: TDFINT -> SIGNED_NAT

The result is negated if and only ifneg: BOOLn: NAT -> SIGNED_NAT

These are the names of the `SORT`

s which can be parameters
of `TOKEN`

definitions.

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAMEThe

`SORT`

of `EXP`

.

-> SORTNAME

Thisforeign_name: STRING(k, n)-> SORTNAME

`SORT`

enables unanticipated kinds of information
to be placed in TDF.

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAME

-> SORTNAMEThe

`SORT`

of `TAG`

.

-> SORTNAME

Theresult: SORTNAMEparams: LIST(SORTNAME) -> SORTNAME

`SORTNAME`

of a `TOKEN`

. Note that it can
have tokens as parameters, but not as result.

-> SORTNAME

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> STRING(k, n)

`STRING`

*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

Thecontrol: EXP INTEGER(v)e1: BITSTREAM STRINGe2: BITSTREAM STRING -> STRING(k, n)

Gives aarg1: STRING(k, n)arg2: STRING(k, m)-> STRING(k, n+m)

`STRING`

which is the concatenation of

Delivers thearg: TDFSTRING(k, n)-> STRING(k, n)

`STRING`

identical to the

These are used to name values and variables in the run time program.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> TAGx

`TAG`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

tagno: TDFINT -> TAGx

`TAG`

identified by

Constructs a pair of a `TAG`

and an `OPTION(ACCESS)`

for use in *make_proc*.

Constructs the pair fortg: TAG POINTERvar_param_alignmentacc: OPTION(ACCESS) -> TAGACC

A `TAGDEC`

declares a `TAG`

for incorporation
into a `TAGDEC_PROPS.`

At_intro: TDFINTacc: OPTION(ACCESS)signature: OPTION(STRING)x: SHAPE -> TAGDEC

`TAGDEC`

announcing that the `TAG`

`EXP`

of `SHAPE`

*acc* specifies the `ACCESS`

properties of the
`TAG`

.

If there is a *make_id_tagdec* for a `TAG`

then all
other *make_id_tagdec* for the same `TAG`

will specify
the same `SHAPE`

and there will be no *make_var_tagdec*
or *common_tagdec* for the `TAG`

.

If two *make_id_tagdecs* specify the same tag and both have
*signatures* present, the strings will be identical. Possible
uses of this signature argument are outlined in
section 7.28.

At_intro: TDFINTacc: OPTION(ACCESS)signature: OPTION(STRING)x: SHAPE -> TAGDEC

`TAGDEC`

announcing that the `TAG`

`EXP`

of `SHAPE POINTER`

(
*acc* specifies the `ACCESS`

properties of the
`TAG`

.

If there is a *make_var_tagdec* for a `TAG`

then all
other *make_var_tagdec*s for the same `TAG`

will specify
`SHAPE`

s with identical `ALIGNMENT`

and there
will be no *make_id_tagdec* or *common_tagdec* for the
`TAG`

.

If two *make_var_tagdec*s specify the same tag and both have
*signature* present, the strings will be identical. Possible
uses of this signature argument are outlined in
section 7.28.

At_intro: TDFINTacc: OPTION(ACCESS)signature: OPTION(STRING)x: SHAPE -> TAGDEC

`TAGDEC`

announcing that the `TAG`

`EXP`

of `SHAPE POINTER`

(
*acc* specifies the `ACCESS`

properties of the
`TAG`

.

If there is a *common_tagdec* for a `TAG`

then there
will be no *make_id_tagdec* or *make_var_tagdec* for that
`TAG`

. If there is more than one *common_tagdec* for
a `TAG`

the one having the maximum `SHAPE`

shall
be taken to apply for the `CAPSULE`

. Each pair of such
`SHAPE`

s will have a maximum. The maximum of two
`SHAPE`

s, *a* and *b*, is defined as follows:

- If the
*a*is equal to*b*the maximum is*a*. - If
*a*and*b*are`COMPOUND`

(*x*) and`COMPOUND`

(*y*) respectively and*a*is an initial segment of*b*, then*b*is the maximum. Similarly if*b*is an initial segment of*a*then*a*is the maximum. - If
*a*and*b*are`NOF`

(*n*,*x*) and`NOF`

(*m*,*x*) respectively and*n*is less than or equal to*m*, then*b*is the maximum. Similarly if*m*is less than or equal to*n*then*a*is the maximum. - Otherwise
*a*and*b*have no maximum.

no_labels: TDFINTtds: SLIST(TAGDEC) -> TAGDEC_PROPS

`LABEL`

s used in
`TAGDEC`

s which declare
the `SHAPE`

s associated with `TAG`

s.

A value of `SORT TAGDEF`

gives the definition of a `TAG`

for incorporation into a `TAGDEF_PROPS`

.

t: TDFINTsignature: OPTION(STRING)e: EXPx-> TAGDEF

`TAGDEF`

defining the
`TAG`

`TDFINT`

,
`TAG`

is defined to stand for the value
delivered by
*e* will be a constant which can be evaluated at load_time or
*e* will be some *initial_value*(E) (see section
5.16.48).

*t* will be declared in the `CAPSULE`

using
*make_id_tagdec*. If both the *make_id_tagdec* and
*make_id_tagdef* have *signatures* present, the strings
will be identical.

If *x* is `PROC`

and the `TAG`

represented
by *t* is named externally via a `CAPSULE_LINK`

, e
will be some *make_proc* or *make_general_proc*.

There will not be more than one `TAGDEF`

defining *t*
in a `CAPSULE`

.

t: TDFINTopt_access: OPTION(ACCESS)signature: OPTION(STRING)e: EXPx-> TAGDEF

`TAGDEF`

defining the
`TAG POINTER`

(`TDFINT`

, `TAG`

stands for a
variable which is initialised with the value delivered by `TAG`

is bound to an original pointer which has the
evaluation of the program as its lifetime.
If *opt_access* contains *visible*, the meaning is that
the variable may be used by agents external to the capsule, and so
it must not be optimised away. If it contains constant, the initialising
value will remain in it throughout the program.

*e* will be a constant which can be evaluated at load_time or
*e* will be some *initial_value*(*e1*) (see
section 5.16.48).

*t* will be declared in the `CAPSULE`

using
*make_var_tagdec*. If both the *make_var_tagdec* and
*make_var_tagdef* have *signatures* present, the strings
will be identical.

There will not be more than one `TAGDEF`

defining *t*
in a `CAPSULE`

.

t: TDFINTopt_access: OPTION(ACCESS)signature: OPTION(STRING)e: EXPx-> TAGDEF

`TAGDEF`

defining the
`TAG`

`POINTER`

(`TDFINT`

, `TAG`

stands
for a variable which is initialised with the value delivered by `TAG`

is bound to an original pointer which has the
evaluation of the program as its lifetime.
If *opt_access* contains *visible*, the meaning is that
the variable may be used by agents external to the capsule, and so
it must not be optimised away. If it contains constant, the initialising
value will remain in it throughout the program.

*e* will be a constant evaluable at load_time or *e* will
be some *initial_value*(E) (see section 5.16.48
).

*t* will be declared in the `CAPSULE`

using
*common_tagdec*.If both the *common_tagdec* and

*common_tagdef* have *signatures* present, the strings

will be identical. Let the maximum `SHAPE`

of these (see
common_tagdec) be *s*.

There may be any number of *common_tagdef* definitions for *t*
in a `CAPSULE`

. Of the *e* parameters of these, one
will be a maximum. This maximum definition is chosen as the definition
of *t*. Its value of *e* will have `SHAPE`

*s*.

The maximum of two *common_tagdef* `EXP`

s, *a*
and *b*, is defined as follows:

- If
*a*has the form*make_value*(*s*),*b*is the maximum. - If
*b*has the form*make_value*(*s*),*a*is the maximum. - If
*a*and*b*have`SHAPE COMPOUND`

(*x*) and`COMPOUND`

(*y*) respectively and the value produced by*a*is an initial segment of the value produced by*b*, then*b*is the maximum. Similarly if*b*is an initial segment of*a*then*a*is the maximum. - If
*a*and*b*have`SHAPE NOF`

(*n*,*x*) and`NOF`

(*m*,*x*) respectively and the value produced by*a*is an initial segment of the value produced by*b*, then*b*is the maximum. Similarly if*b*is an initial segment of*a*then*a*is the maximum. - If the value produced by
*a*is equal to the value produced by*b*the maximum is*a*. - Otherwise
*a*and*b*have no maximum.

no_labels: TDFINTtds: SLIST(TAGDEF) -> TAGDEF_PROPS

`LABEL`

s used in
`TAGDEF`

s which give
the `EXP`

s which are the definitions of values associated
with `TAG`

s.

This is an auxiliary construction to make the elements ofsha: SHAPEopt_access: OPTION(ACCESS)tg_intro: TAG -> TAGSHACC

`TDFBOOL`

is the TDF encoding of a boolean. See
Fundamental encoding.

`TDFIDENT`

(
This construction will not be used inside a `BITSTREAM`

.

`TDFINT`

is the TDF encoding of an unbounded unsigned
integer constant. See Fundamental encoding.

`TDFSTRING`

(

A `TOKDEC`

declares a `TOKEN`

for incorporation
into a `UNIT`

.

The sort of the tokentok: TDFINTsignature: OPTION(STRING)s: SORTNAME -> TOKDEC

`SORT`

, with a list of
parameter `SORT`

s (possible empty) and a result
`SORT`

.
If *signature* is present, it will be produced by *make_string*.

If two *make_tokdecs* specify the same token and both have
*signatures* present, the strings will be identical. Possible
uses of this signature argument are outlined in
section 7.28.

tds: SLIST(TOKDEC) -> TOKDEC_PROPS

`TOKDEC`

s which gives the sorts
associated with `TOKEN`

s.

A `TOKDEF`

gives the definition of a `TOKEN`

for incorporation into a `TOKDEF_PROPS`

.

Atok: TDFINTsignature: OPTION(STRING)def: BITSTREAM TOKEN_DEFN -> TOKDEF

`TOKDEF`

is constructed which defines the `TOKEN`

`SORT`

with a `SORTNAME`

, except for
`SORT`

of the result, `BITSTREAM`

. See
token_definition.
If *signature* is present, it will be produced by *make_string*.

*tok* may have been introduced by a *make_tokdec*. If both
the *make_tokdec* and *make_tokdef* have *signatures*
present, the strings will be identical.

At the application of this `TOKEN`

actual pieces of TDF
having `SORT`

*sn*[*i*] are supplied to correspond
to the *tk*[*i*]. The application denotes the piece of TDF
obtained by substituting these actual parameters for the corresponding
`TOKEN`

s within *body*.

no_labels: TDFINTtds: SLIST(TOKDEF) -> TOKDEF_PROPS

`LABEL`

s used in
`TOKDEF`

s which gives
the definitions associated with `TOKEN`

s.

These are used to stand for functions evaluated at installation time.
They are represented by `TDFINT`

s.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> TOKEN

`TOKEN`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

tokno: TDFINT -> TOKEN

`TOKEN`

identified by

tdef: BITSTREAM TOKEN_DEFN -> TOKEN

`TOKEN`

s are only used in

An auxiliary `SORT`

used in *make_tokdef* and
*use_tokdef*.

Makes a token definition.result_sort: SORTNAMEtok_params: LIST(TOKFORMALS)body:result_sort-> TOKEN_DEFN

`SORT`

of body. `TOKEN`

s
and their `SORT`

s. `TOKEN`

s defined in
The effect of applying the definition of a `TOKEN`

is as
if the following sequence was obeyed.

First, the actual parameters (if any) are expanded to produce expressions
of the appropriate `SORT`

s. During this expansion all token
applications in the actual parameters are expanded.

Second, the definition is copied, making fresh `TAG`

s and
`LABEL`

s where these are introduced in *identify*,
*variable*, *labelled*, *conditional*, *make_proc,
make_general_proc* and *repeat* constructions. Any other
`TAG`

s or `LABEL`

s used in *body* will
be provided by the context (see below) of the `TOKEN_DEFN`

or by the expansions of the actual parameters.

Third, the actual parameter expressions are substituted for the formal
parameter tokens in *tok_params* to give the final result.

The context of a `TOKEN_DEFN`

is the set of names (`TOKEN`

s,
`TAG`

s, `LABEL`

s,
`AL_TAG`

s etc.) "in scope" at the site of the
`TOKEN_DEFN`

.

Thus, in a *make_tokdef*, the context consists of the set of
`TOKEN`

s defined in its tokdef `UNIT`

, together
with the set of linkable entities defined by the *make_links*
of that `UNIT`

. Note that this does not include
`LABEL`

s and the only `TAG`

s included are "global"
ones.

In a *use_tokdef*, the context may be wider, since the site of
the
`TOKEN_DEFN`

need not be in a tokdef `UNIT`

;
it may be an actual parameter of a token application. If this happens
to be within an EXP, there may be `TAG`

s or `LABEL`

s
locally within scope; these will be in the context of the
`TOKEN_DEFN`

, together with the global names of the enclosing
UNIT as before.

*Previous versions of the specification limited token definitions
to be non-recursive. There is no intrinsic reason for the limitation
on recursive TOKENs. Since the UNIT structure implies
different namespaces, there is very little implementation advantage
to be gained from retaining the limitation.*

An auxiliary construction to make up the elements of the lists insn: SORTNAMEtk: TDFINT -> TOKFORMALS

A `TRANSFER_MODE`

controls the operation of
*assign_with_mode*, *contents_with_mode* and *move_some*.

A `TRANSFER_MODE`

acts like a set of the values *overlap,
trap_on_nil, complete* and *volatile*. The
`TRANSFER_MODE`

*standard_transfer_mode* acts like
the empty set. *add_modes* acts like set union.

The token is applied to the arguments encoded in thetoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> TRANSFER_MODE

`BITSTREAM`

`TRANSFER_MODE`

.
The notation *param_sorts(token_value)* is intended to mean the
following. The token definition or token declaration for
*token_value* gives the `SORT`

s of its arguments in
the
`SORTNAME`

component. The `BITSTREAM`

in
*token_args* consists of these `SORT`

s 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 TRANSFER_MODEe2: BITSTREAM TRANSFER_MODE -> TRANSFER_MODE

A construction qualified bymd1: TRANSFER_MODEmd2: TRANSFER_MODE -> TRANSFER_MODE

`TRANSFER_MODES`

-> TRANSFER_MODEIf

See Overlapping.

-> TRANSFER_MODEThis

`TRANSFER_MODE`

implies no special properties.

-> TRANSFER_MODEIf

-> TRANSFER_MODEIf

*This is intended to implement ANSI C's volatile construction. In
this use, any volatile identifier should be declared as a TAG
with used_as_volatile ACCESS.*

-> TRANSFER_MODEA transfer qualified with complete shall leave the destination unchanged if the evaluation of the value transferred is left with a jump.

These are used to provide world-wide unique names for `TOKEN`

s
and `TAG`

s.

This implies a registry for allocating `UNIQUE`

values.

Twotext: SLIST(TDFIDENT) -> UNIQUE

`UNIQUE`

values are equal if and only if they were
constructed with equal arguments.

A `UNIT`

gathers together a `PROPS`

and
`LINK`

s which relate the names by which objects are known
inside the `PROPS`

and names by which they are to be known
across the whole of the enclosing `CAPSULE`

.

local_vars: SLIST(TDFINT)lks: SLIST(LINKS)properties: BYTESTREAM PROPS -> UNIT

`TDFINT`

s in the range 0 to the
corresponding
*lks* gives the `LINK`

s for each kind of entity in
the same order as in *local_vars*.

The *properties* will be a `PROPS`

of a form dictated
by the unit identification, see make_capsule.

The length of *lks* will be either 0 or equal to the length of
*cap_linking* in *make_capsule*.

These describe the different kinds of integer which can occur at run
time. The fundamental construction consists of a `SIGNED_NAT`

for the lower bound of the range of possible values, and a
`SIGNED_NAT`

for the upper bound (inclusive at both ends).

There is no limitation on the magnitude of these bounds in TDF, but an installer may specify limits. See Representing integers.

The token is applied to the arguments to give atoken_value: TOKENtoken_args: BITSTREAMparam_sorts(token_value)-> VARIETY

`VARIETY`

.
*token_value* in the `CAPSULE`

then *token_args* is a `BITSTREAM`

encoding of the
`SORT`

s of its parameters, in the order specified.

Thecontrol: EXP INTEGER(v)e1: BITSTREAM VARIETYe2: BITSTREAM VARIETY -> VARIETY

lower_bound: SIGNED_NATupper_bound: SIGNED_NAT -> VARIETY

`VARIETY`

,
and

Ifsigned_width: BOOLwidth: NAT -> VARIETY

This `UNIT`

gives information about version numbers and
user information.

Contains version information.version_info: SLIST(VERSION) -> VERSION_PROPS

The major and minor version numbers of the TDF used. An increase in minor version number means an extension of facilities, an increase in major version number means an incompatible change. TDF with the same major number but a lower minor number than the installer shall install correctly.major_version: TDFINTminor_version: TDFINT -> VERSION

For TDF conforming to this specification the major number will be 4 and the minor number will be 0.

Every `CAPSULE`

will contain at least one *make_version*
construct.

This is (usually character) information included in the TDF for labelling purposes.information: STRING(k, n) -> VERSION

*information* will be produced by *make_string*.

*Part of the TenDRA Web.Crown
Copyright © 1998.*