5. Specification of TDF constructs
- 5.1. Access
- 5.2. AL_TAG
- 5.3. AL_TAGDEF
- 5.4. AL_TAGDEF_PROPS
- 5.5. ALIGNMENT
- 5.6. BITFIELD_VARIETY
- 5.7. BITSTREAM
- 5.8. BOOL
- 5.9. BYTESTREAM
- 5.10. CALLEES
- 5.11. CAPSULE
- 5.12. CAPSULE_LINK
- 5.13. CASELIM
- 5.14. ERROR_code
- 5.15. ERROR_TREATMENT
- 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.18. EXTERN_LINK
- 5.19. FLOATING_VARIETY
- 5.20. GROUP
- 5.21. LABEL
- 5.22. LINK
- 5.23. LINKEXTERN
- 5.24. LINKS
- 5.25. NAT
- 5.26. NTEST
- 5.26.1. ntest_apply
- 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.28. PROCPROPS
- 5.29. PROPS
- 5.30. ROUNDING_MODE
- 5.31. SHAPE
- 5.32. SIGNED_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.35. TAG
- 5.36. TAGACC
- 5.37. TAGDEC
- 5.38. TAGDEC_PROPS
- 5.39. TAGDEF
- 5.40. TAGDEF_PROPS
- 5.41. TAGSHACC
- 5.42. TDFBOOL
- 5.43. TDFIDENT
- 5.44. TDFINT
- 5.45. TDFSTRING
- 5.46. TOKDEC
- 5.47. TOKDEC_PROPS
- 5.48. TOKDEF
- 5.49. TOKDEF_PROPS
- 5.50. TOKEN
- 5.51. TOKEN_DEFN
- 5.52. TOKFORMALS
- 5.53. TRANSFER_MODE
- 5.54. UNIQUE
- 5.55. UNIT
- 5.56. VARIETY
- 5.57. VERSION_PROPS
- 5.58. VERSION
5.1. Access
| Number of encoding bits | 4 |
| Is coding extendable | yes |
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.
5.1.1. access_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> ACCESS
The token is applied to the arguments encoded in the BITSTREAM token_args to give an ACCESS.
The notation param_sorts(token_value) is intended to mean the following. The token definition or token declaration for token_value gives the SORTs of its arguments in the SORTNAME component. The BITSTREAM in token_args consists of these SORTs in the given order. If no token declaration or definition exists in the CAPSULE, the BITSTREAM cannot be read.
5.1.2. access_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM ACCESS e2: BITSTREAM ACCESS -> ACCESS
control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.1.3. add_access
| Encoding number | 3 |
a1: ACCESS a2: ACCESS -> ACCESS
A construction qualified with add_accesses has both ACCESS properties a1 and a2. This operation is associative and commutative.
5.1.4. constant
| Encoding number | 4 |
-> ACCESS
Only a variable (not an identity) may be qualified with constant. A variable qualified with constant will retain its initialising value unchanged throughout its lifetime.
5.1.5. long_jump_access
| Encoding number | 5 |
-> ACCESS
An object must also have this property if it is to have a defined value when a long_jump returns to the procedure declaring the object.
5.1.6. no_other_read
| Encoding number | 6 |
-> ACCESS
This property refers to a POINTER, p. It says that, within the lifetime of the declaration being qualified, there are no contents, contents_with_mode or move_some source accesses to any pointer not derived from p which overlap with any of the contents, contents_with_mode, assign, assign_with_mode or move_some accesses to pointers derived from p.
The POINTER being described is that obtained by applying obtain_tag to the TAG of the declaration. If the declaration is an identity, the SHAPE of the TAG will be a POINTER.
5.1.7. no_other_write
| Encoding number | 7 |
-> ACCESS
This property refers to a POINTER, p. It says that, within the lifetime of the declaration being qualified, there are no assign, assign_with_mode or move_some destination accesses to any pointer not derived from p which overlap with any of the contents, contents_with_mode, assign, assign_with_mode or move_some accesses to pointers derived from p.
The POINTER being described is that obtained by applying obtain_tag to the TAG of the declaration. If the declaration is an identity, the SHAPE of the TAG will be a POINTER.
5.1.8. out_par
| Encoding number | 8 |
-> ACCESS
An object qualified by out_par will be an output parameter in a make_general_proc construct. This will indicate that the final value of the parameter is required in postlude part of an apply_general_proc of this procedure.
5.1.9. preserve
| Encoding number | 9 |
-> ACCESS
This property refers to a global object. It says that the object will be included in the final program, whether or not all possible accesses to that object are optimised away; for example by inlining all possible uses of procedure object.
5.1.10. register
| Encoding number | 10 |
-> ACCESS
Indicates that an object with this property is frequently used. This can be taken as a recommendation to place it in a register.
5.1.11. standard_access
| Encoding number | 11 |
-> ACCESS
An object qualified as having standard_access has normal (i.e. no special) access properties.
5.1.12. used_as_volatile
| Encoding number | 12 |
-> ACCESS
An object qualified as having used_as_volatile will be used in a move_some, contents_with_mode or an assign_with_mode construct with TRANSFER_MODE volatile.
5.1.13. visible
| Encoding number | 13 |
-> ACCESS
An object qualified as visible may be accessed when the procedure in which it is declared is not the current procedure. A TAG must have this property if it is to be used by env_offset.
5.2. AL_TAG
| Number of encoding bits | 1 |
| Is coding extendable | yes |
| Linkable entity identification | alignment |
AL_TAGs name ALIGNMENTs. 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}.
5.2.1. al_tag_apply_token
| Encoding number | 2 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> AL_TAG
The token is applied to the arguments encoded in the BITSTREAM token_args to give an AL_TAG.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.2.2. make_al_tag
| Encoding number | 1 |
al_tagno: TDFINT -> AL_TAG
make_al_tag constructs an AL_TAG identified by al_tagno.
5.3. AL_TAGDEF
| Number of encoding bits | 1 |
| Is coding extendable | yes |
An AL_TAGDEF gives the definition of an AL_TAG for incorporation into a AL_TAGDEF_PROPS.
5.3.1. make_al_tagdef
| Encoding number | 1 |
t: TDFINT a: ALIGNMENT -> AL_TAGDEF
The AL_TAG identified by t is defined to stand for the ALIGNMENT a. All the AL_TAGDEFs in a CAPSULE must be considered together as a set of simultaneous equations defining ALIGNMENT values for the AL_TAGs. No order is imposed on the definitions.
In any particular CAPSULE the set of equations may be incomplete, but a CAPSULE which is being translated into code will have a set of equations which defines all the AL_TAGs which it uses.
The result of the evaluation of the control argument of any x_cond construction (e.g alignment_cond) used in a shall be independent of any AL_TAGs used in the control. Simultaneous equations defining ALIGNMENTs can then always be solved.
5.4. AL_TAGDEF_PROPS
| Number of encoding bits | 0 |
| Is coding extendable | no |
| Unit identificaiton | aldef |
5.4.1. make_al_tagdefs
| Encoding number | 0 |
no_labels: TDFINT tds: SLIST(AL_TAGDEF) -> AL_TAGDEF_PROPS
no_labels is the number of local LABELs used in tds. tds is a list of AL_TAGDEFs which define the bindings for al_tags.
5.5. ALIGNMENT
| Number of encoding bits | 4 |
| Is coding extendable | yes |
An ALIGNMENT gives information about the layout of data in memory and hence is a parameter for the POINTER and OFFSET SHAPEs (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 VARIETYs, all FLOATING_VARIETYs and all BITFIELD_VARIETYs. The sets are written here as, for example, {pointer, proc} meaning the set containing pointer and proc.
In addition, there are “special” ALIGNMENTs 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” ALIGNMENTs 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 PROCs and POINTERs. 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, doubles 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 ALIGNMENTs, means that the set b will be a subset of a (or equal to a).
5.5.1. alignment_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> ALIGNMENT
The token is applied to the arguments encoded in the BITSTREAM token_args to give an ALIGNMENT.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.5.2. alignment_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM ALIGNMENT e2: BITSTREAM ALIGNMENT -> ALIGNMENT
control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.5.3. alignment
| Encoding number | 3 |
sha: SHAPE -> ALIGNMENT
The alignment construct is defined as follows:
-
If sha is
PROCthen the resultingALIGNMENTis {proc}. -
If sha is
INTEGER(v) then the resultingALIGNMENTis {v}. -
If sha is
FLOATING(v) then the resultingALIGNMENTis {v}. -
If sha is
BITFIELD(v) then the resultingALIGNMENTis {v}. -
If sha is
TOPthe resultingALIGNMENTis {} - the empty set. -
If sha is
BOTTOMthe resultingALIGNMENTis undefined. -
If sha is
POINTER(x) the resultingALIGNMENTis {pointer}. -
If sha is
OFFSET(x, y) the resultingALIGNMENTis {offset}. -
If sha is
NOF(n, s) the resultingALIGNMENTis alignment(s). -
If sha is
COMPOUND(EXP OFFSET(x, y)) then the resultingALIGNMENTis x.
5.5.4. alloca_allignment
| Encoding number | 4 |
-> ALIGNMENT
Delivers the ALIGNMENT of POINTERs produced from local_alloc.
5.5.5. callees_alignment
| Encoding number | 5 |
var: BOOL -> ALIGNMENT
If var is true the ALIGNMENT is that of callee parameters qualified by the PROCPROPS var_callees. If var is false, the ALIGNMENT is that of callee parameters not qualified by PROCPROPS var_callees.
Delivers the base ALIGNMENT of OFFSETs from a frame-pointer to a CALLEE parameter. Values of such OFFSETs can only be produced by env_offset applied to CALLEE parameters, or offset arithmetic operations applied to existing OFFSETs.
5.5.6. callers_alignment
| Encoding number | 6 |
var: BOOL -> ALIGNMENT
If var is true the ALIGNMENT is that of caller parameters qualified by the PROCPROPS var_callers. If var is false, the ALIGNMENT is that of caller parameters not qualified by PROCPROPS var_callers.
Delivers the base ALIGNMENT of OFFSETs from a frame-pointer to a CALLER parameter. Values of such OFFSETs can only be produced by env_offset applied to CALLER parameters, or offset arithmetic operations applied to existing OFFSETs.
5.5.7. code_alignment
| Encoding number | 7 |
-> ALIGNMENT
Delivers {code}, the ALIGNMENT of the POINTER produced by make_local_lv.
5.5.8. locals_alignment
| Encoding number | 8 |
-> ALIGNMENT
Delivers the base ALIGNMENT of OFFSETs from a frame-pointer to a value defined by variable or identify. Values of such OFFSETs can only be produced by env_offset applied to TAGs so defined, or offset arithmetic operations applied to existing OFFSETs.
5.5.9. obtain_al_tag
| Encoding number | 9 |
at: AL_TAG -> ALIGNMENT
obtain_al_tag produces the ALIGNMENT with which the AL_TAG at is bound.
5.5.10. parameter_alignment
| Encoding number | 10 |
sha: SHAPE -> ALIGNMENT
Delivers the ALIGNMENT of a parameter of a procedure of SHAPE sha.
5.5.11. unite_alignments
| Encoding number | 11 |
a1: ALIGNMENT a2: ALIGNMENT -> ALIGNMENT
unite_alignments produces the alignment at which all the members of the ALIGNMENT sets a1 and a2 can be placed - in other words the ALIGNMENT set which is the union of a1 and a2.
5.5.12. var_param_alignment
| Encoding number | 12 |
-> ALIGNMENT
Delivers the ALIGNMENT used in the var_param argument of make_proc.
5.6. BITFIELD_VARIETY
| Number of encoding bits | 2 |
| Is coding extendable | yes |
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.
5.6.1. bfvar_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> BITFIELD_VARIETY
The token is applied to the arguments encoded in the BITSTREAM token_args to give a BITFIELD_VARIETY.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.6.2. bfvar_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM BITFIELD_VARIETY e2: BITSTREAM BITFIELD_VARIETY -> BITFIELD_VARIETY
control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.6.3. bfvar_bits
| Encoding number | 3 |
issigned: BOOL bits: NAT -> BITFIELD_VARIETY
bfvar_bits constructs a BITFIELD_VARIETY describing a pattern of bits bits. If issigned is true, the pattern is considered to be a twos-complement signed number: otherwise it is considered to be unsigned.
5.7. BITSTREAM
A 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.
5.8. BOOL
| Number of encoding bits | 3 |
| Is coding extendable | yes |
A BOOL is a piece of TDF which can take two values, true or false.
5.8.1. bool_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> BOOL
The token is applied to the arguments encoded in the BITSTREAM token_args to give a BOOL.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.8.2. bool_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM BOOL e2: BITSTREAM BOOL -> BOOL
control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.8.3. false
| Encoding number | 3 |
-> BOOL
false produces a false BOOL.
5.8.4. true
| Encoding number | 4 |
-> BOOL
true produces a true BOOL.
5.9. BYTESTREAM
A BYTESTREAM is analogous to a BITSTREAM, but is encoded to permit fast copying.
See The TDF encoding.
5.10. CALLEES
| Number of encoding bits | 2 |
| Is coding extendable | yes |
This is an auxilliary SORT used in calling procedures by apply_general_proc and tail_call to provide their actual callee parameters.
5.10.1. make_callee_list
| Encoding number | 1 |
args: LIST(EXP) -> CALLEES
The list of EXPs args are evaluated in any interleaved order and the resulting list of values form the actual callee parameters of the call.
5.10.2. make_dynamic_callees
| Encoding number | 2 |
ptr: EXP POINTER(x) sze: EXP OFFSET(x, y) -> CALLEES
The value of size sze pointed at by ptr forms the actual callee parameters of the call.
The CALLEES value is intended to refer to a sequence of zero or more callee parameters. x will include parameter_alignment(s) for each s that is the SHAPE of an intended callee parameter. The value addressed by ptr may be produced in one of two ways. It may be produced as a COMPOUND SHAPE value in the normal sense of a structure, whose successive elements will be used to generate the sequence of callee parameters. In this case, each element in the sequence of SHAPE s must additionally be padded to parameter_alignment(s). Alternatively, ptr may address the callee parameters of an already activated procedure, by referring to the first of the sequence. sze will be equivalent to shape_offset(c) where c is the COMPOUND SHAPE just described.
The call involved (i.e. apply_general_proc or tail_call) must have a var_callees PROCPROPS.
5.10.3. same_callees
| Encoding number | 3 |
-> CALLEES
The callee parameters of the call are the same as those of the current procedure.
5.11. CAPSULE
| Number of encoding bits | 0 |
| Is coding extendable | no |
A CAPSULE is an independent piece of TDF. There is only one construction, make_capsule.
5.11.1. make_capsule
| Encoding number | 0 |
prop_names: SLIST(TDFIDENT) cap_linking: SLIST(CAPSULE_LINK) ext_linkage: SLIST(EXTERN_LINK) groups: SLIST(GROUP) -> CAPSULE
make_capsule brings together UNITs and linking and naming information. See The Overall Structure.
The elements of the list, prop_names, correspond one-to-one with the elements of the list, groups. The element of prop_names is the unit identification of all the UNITs in the corresponding GROUP. See PROPS. A CAPSULE need not contain all the kinds of UNIT.
It is intended that new kinds of PROPS with new unit identifications can be added to the standard in a purely additive fashion, either to form a new standard or for private purposes.
The elements of the list, cap_linking, correspond one-to-one with the elements of the list, ext_linkage. The element of cap_linking gives the linkable entity identification for all the LINKEXTERNs in the element of ext_linkage. It also gives the number of CAPSULE level linkable entities having that identification.
The elements of the list, cap_linking, also correspond one-to-one with the elements of the lists called local_vars in each of the make_unit constructions for the UNITs in groups. The element of local_vars gives the number of UNIT level linkable entities having the identification in the corresponding member of cap_linking.
It is intended that new kinds of linkable entity can be added to the standard in a purely additive fashion, either to form a new standard or for private purposes.
ext_linkage provides a list of lists of LINKEXTERNs. These LINKEXTERNs specify the associations between the names to be used outside the CAPSULE and the linkable entities by which the UNITs make objects available within the CAPSULE.
The list, groups, provides the non-linkage information of the CAPSULE.
5.12. CAPSULE_LINK
| Number of encoding bits | 0 |
| Is coding extendable | no |
An auxiliary SORT which gives the number of linkable entities of a given kind at CAPSULE level. It is used only in make_capsule.
5.12.1. make_capsule_link
| Encoding number | 0 |
sn: TDFIDENT n: TDFINT -> CAPSULE_LINK
n is the number of CAPSULE level linkable entities (numbered from 0 to n-1) of the kind given by sn. sn corresponds to the linkable entity identification.
5.13. CASELIM
| Number of encoding bits | 0 |
| Is coding extendable | no |
An auxiliary SORT which provides lower and upper bounds and the LABEL destination for the case construction.
5.13.1. make_caselim
| Encoding number | 0 |
branch: LABEL lower: SIGNED_NAT upper: SIGNED_NAT -> CASELIM
Makes a triple of destination and limits. The case construction uses a list of CASELIMs. If the control variable of the case lies between lower and upper, control passes to branch.
5.14. ERROR_code
| Number of encoding bits | 2 |
| Is coding extendable | yes |
5.14.1. nil_access
| Encoding number | 1 |
-> ERROR_code
Delivers the ERROR_code arising from an attempt to access a nil pointer in an operation with TRANSFER_MODE trap_on_nil.
5.14.2. overflow
| Encoding number | 2 |
-> ERROR_code
Delivers the ERROR_code arising from a numerical exceptional result in an operation with ERROR_TREATMENT trap(overflow).
5.14.3. stack_overflow
| Encoding number | 3 |
-> ERROR_code
Delivers the ERROR_code arising from a stack overflow in the call of a procedure defined with PROCPROPS check_stack.
5.15. ERROR_TREATMENT
| Number of encoding bits | 3 |
| Is coding extendable | yes |
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.
5.15.1. errt_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> ERROR_TREATMENT
The token is applied to the arguments encoded in the BITSTREAM token_args to give an ERROR_TREATMENT.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.15.2. errt_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM ERROR_TREATMENT e2: BITSTREAM ERROR_TREATMENT -> ERROR_TREATMENT
control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.15.3. continue
| Encoding number | 3 |
-> ERROR_TREATMENT
If an operation with a continue ERROR_TREATMENT causes an error, some value of the correct SHAPE shall be delivered. This value shall have the same properties as is specified in make_value.
5.15.4. error_jump
| Encoding number | 4 |
lab: LABEL -> ERROR_TREATMENT
error_jump produces an ERROR_TREATMENT which requires that control be passed to lab if it is invoked. lab will be in scope.
If a construction has an error_jump ERROR_TREATMENT and the jump is taken, the canonical order specifies only that the jump occurs after evaluating the construction. It is not specified how many further constructions are evaluated.
This rule implies that a further construction is needed to guarantee that errors have been processed. This is not yet included. The effect of nearby procedure calls or exits also needs definition.
5.15.5. trap
| Encoding number | 5 |
trap_list: LIST(ERROR_code) -> ERROR_TREATMENT
The list of ERROR_codeS in trap_list specifies a set of possible exceptional behaviours. If any of these occur in an construction with ERROR_TREATMENT trap, the TDF exception handling is invoked (see section 7.8).
The observations on canonical ordering in error_jump apply equally here.
5.15.6. wrap
| Encoding number | 6 |
-> ERROR_TREATMENT
wrap is an ERROR_TREATMENT which will only be used in constructions with integer operands and delivering EXP INTEGER(v) where either the lower bound of v is zero or the construction is not one of mult, power, div0, div1, div2, rem0, rem1, rem2. The result will be evaluated and any bits in the result lying outside the representing VARIETY will be discarded (see Representing integers
5.15.7. impossible
| Encoding number | 7 |
-> ERROR_TREATMENT
impossible is an ERROR_TREATMENT which means that this error will not occur in the construct concerned.
impossible is possibly a misnomer. If an error occurs the result is undefined.
5.16. EXP
| Number of encoding bits | 7 |
| Is coding extendable | yes |
EXPs are pieces of TDF which are translated into program. EXP is by far the richest SORT. There are few primitive EXPs: most of the constructions take arguments which are a mixture of EXPs and other SORTs. There are constructs delivering EXPs that correspond to the declarations, program structure, procedure calls, assignments, pointer manipulation, arithmetic operations, tests etc. of programming languages.
5.16.1. exp_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> EXP x
The token is applied to the arguments encoded in the BITSTREAM token_args to give an EXP.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.16.2. exp_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM EXP x e2: BITSTREAM EXP y -> EXP (control ? x : y)
control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.16.3. abs
| Encoding number | 3 |
ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) -> EXP INTEGER(v)
The absolute value of the result produced by arg1 is delivered.
If the result cannot be expressed in the VARIETY being used to represent v, an overflow error is caused and is handled in the way specified by ov_err.
5.16.4. add_to_ptr
| Encoding number | 4 |
arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) -> EXP POINTER(z)
arg1 is evaluated, giving p, and arg2 is evaluated and the results are added to produce the answer. The result is derived from the pointer delivered by arg1. The intention is to produce a POINTER displaced from the argument POINTER by the given amount.
x will include y.
arg1 may deliver a null POINTER. In this case the result is derived from a null POINTER which counts as an original POINTER. Further OFFSETs may be added to the result, but the only other useful operation on the result of adding a number of OFFSETs to a null POINTER is to subtract_ptrs a null POINTER from it.
The result will be less than or equal (in the sense of pointer_test) to the result of applying add_to_ptr to the original pointer from which p is derived and the size of the space allocated for the original pointer.
In the simple representation of POINTER arithmetic (see 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.
5.16.5. and
| Encoding number | 5 |
arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
The arguments are evaluated producing integer values of the same VARIETY, v. The result is the bitwise and of the two values in the representing VARIETY. The result is delivered with the same SHAPE as the arguments.
5.16.6. apply_proc
| Encoding number | 6 |
result_shape: SHAPE p: EXP PROC params: LIST(EXP) var_param: OPTION(EXP) -> EXP result_shape
p, params and var_param (if present) are evaluated in any interleaved order. The procedure, p, is applied to the parameters. The result of the procedure call, which will have result_shape, is delivered as the result of the construction.
The canonical order of evaluation is as if the definition were in-lined. That is, the actual parameters are evaluated interleaved in any order and used to initialise variables which are identified by the formal parameters during the evaluation of the procedure body. When this is complete the body is evaluated. So apply_proc is evaluated like a variable construction, and obeys similar rules for order of evaluation.
If p delivers a null procedure the effect is undefined.
var_param is intended to communicate parameters which vary in SHAPE from call to call. Access to these parameters during the procedure is performed by using OFFSET arithmetic. Note that it is necessary to place these values on var_param_alignment because of the definition of make_proc.
The optional var_param should not be confused with variable argument lists in the C (<stdarg.h> or <varargs.h>) sense, which are communicated by extending the params list. This is discussed further in section 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.
5.16.7. apply_general_proc
| Encoding number | 7 |
result_shape: SHAPE prcprops: OPTION(PROCPROPS) p: EXP PROC callers_intro: LIST(OTAGEXP) callee_pars: CALLEES postlude: EXP TOP -> EXP result_shape
p, callers_intro and callee_pars are evaluated in any order. The procedure, p, is applied to the parameters. The result of the procedure call, which will have result_shape, is delivered as the result of the construction.
If p delivers a null procedure the effect is undefined.
Any TAG introduced by an OTAGEXP in callers_intro is available in postlude which will be evaluated after the application.
postlude will not contain any local_allocs or calls of procedures with untidy returns. If prcprops include untidy, postlude will be make_top.
The canonical order of evaluation is as if the definition of p were inlined in a manner dependent on prcprops.
If none of the PROCPROPS var_callers, var_callees and check_stack are present the inlining is as follows, supposing that P is the body of the definition of p:
Let Ri be the value of the EXP of the ith OTAGEXP in callers_intro and Ti be its TAG (if it is present). Let Ei be the ith value in callee_pars. Let ri be the ith formal caller parameter TAG of p. Let ei be the ith formal callee parameter TAG of p.
Each Ri is used to initialise a variable which is identified by ri; there will be exactly as many Ri as ri.The scope of these variable definitions is a sequence consisting of three components - the identification of a TAG res with the result of a binding of P, followed by a binding of postlude, followed by an obtain_tag of res giving the result of the inlined procedure call.
The binding of P consists of using each Ei to initialise a variable identified with ei; there will be exactly as many Ei as ei. The scope of these variable definitions is P modified so that the first return or untidy_return encountered in P gives the result of the binding. If it ends with a return, any space generated by local_allocs within the binding is freed (in the sense of local_free) at this point. If it ends with untidy_return, no freeing will take place.
The binding of postlude consists of identifying each Ti (if present) with the contents of the variable identified by ri. The scope of these identifications is postlude.
If the PROCPROPS var_callers is present, the inlining process is modified by: A compound variable is constructed initialised to Ri in order; the alignment and padding of each individual Ri will be given by an exact application of parameter_alignment on the SHAPE of Ri. Each ri is then identified with a pointer to the copy of Ri within the compound variable; there will be at least as many Ri as ri. The evaluation then continues as above with the scope of these identifications being the sequence.
If the PROCPROPS var_callees is present, the inlining process is modified by: The binding of P is done by generating (as if by local_alloc) a pointer to space for a compound value constructed from each Ei in order (just as for var_callers). Each ei is identified with a pointer to the copy of Ei within the generated space; there will be at least as many ei as Ei. P is evaluated within the scope of these identifications as before. Note that the generation of space for these callee parameters is a local_alloc with the binding of P, and hence will not be freed if P ends with an untidy_return.
5.16.8. assign
| Encoding number | 8 |
arg1: EXP POINTER(x) arg2: EXP y -> EXP TOP
The value produced by arg2 will be put in the space indicated by arg1.
x will include alignment(y).
y will not be a BITFIELD.
If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.
If the value delivered by arg1 is a null pointer the effect is undefined.
See 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.
5.16.9. assign_with_mode
| Encoding number | 9 |
md: TRANSFER_MODE arg1: EXP POINTER(x) arg2: EXP y -> EXP TOP
The value produced by arg2 will be put in the space indicated by arg1. The assignment will be carried out as specified by the TRANSFER_MODE (q.v.).
If md consists of standard_transfer_mode only, then assign_with_mode is the same as assign.
x will include alignment(y).
y will not be a BITFIELD.
If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.
If the value delivered by arg1 is a null pointer the effect is undefined.
See Overlapping and >Incomplete assignment.
5.16.10. bitfield_assign
| Encoding number | 10 |
arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) arg3: EXP BITFIELD(v) -> EXP TOP
The value delivered by arg3 is assigned at a displacement given by arg2 from the pointer delivered by arg1.
x will include y and z will include v.
arg2, BITFIELD(v) will be variety-enclosed (see section 7.24).
5.16.11. bitfield_assign_with_mode
| Encoding number | 11 |
md: TRANSFER_MODE arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) arg3: EXP BITFIELD(v) -> EXP TOP
The value delivered by arg3 is assigned at a displacement given by arg2 from the pointer delivered by arg1.The assignment will be carried out as specified by the TRANSFER_MODE (q.v.).
If md consists of standard_transfer_mode only, then bitfield_assign_with_mode is the same as bitfield_assign.
arg2, BITFIELD(v) will be variety-enclosed.(see section 7.24).
5.16.12. bitfield_contents
| Encoding number | 12 |
v: BITFIELD_VARIETY arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) -> EXP BITFIELD(v)
The bitfield of BITFIELD_VARIETY v, located at the displacement delivered by arg2 from the pointer delivered by arg1 is extracted and delivered.
x will include y and z will include v.
arg2, BITFIELD(v) will be variety_enclosed (see section 7.24).
5.16.13. bitfield_contents_with_mode
| Encoding number | 13 |
md: TRANSFER_MODE v: BITFIELD_VARIETY arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) -> EXP BITFIELD(v)
The bitfield of BITFIELD_VARIETY v, located at the displacement delivered by arg2 from the pointer delivered by arg1 is extracted and delivered.The operation will be carried out as specified by the TRANSFER_MODE (q.v.).
If md consists of standard_transfer_mode only, then bitfield_contents_with_mode is the same as bitfield_contents.
x will include y and z will include v.
arg2, BITFIELD(v) will be variety_enclosed (see section 7.24).
5.16.14. case
| Encoding number | 14 |
exhaustive: BOOL control: EXP INTEGER(v) branches: LIST(CASELIM) -> EXP (exhaustive ? BOTTOM : TOP)
control is evaluated to produce an integer value, c. Then c is tested to see if it lies inclusively between lower and upper, for each element of branches. If this tests succeeds, control passes to the label branch belonging to that CASELIM (see section 5.13). If c lies between no pair, the construct delivers a value of SHAPE TOP. The order in which the comparisons are made is undefined.
The sets of SIGNED_NATs in branches will be disjoint.
If exhaustive is true the value delivered by control will lie between one of the lower/upper pairs.
5.16.15. change_bitfield_to_int
| Encoding number | 15 |
v: VARIETY arg1: EXP BITFIELD(bv) -> EXP INTEGER(v)
arg1 is evaluated and converted to a INTEGER(v).
If arg1 exceed the bounds of v, the effect is undefined.
5.16.16. change_floating_variety
| Encoding number | 16 |
flpt_err: ERROR_TREATMENT r: FLOATING_VARIETY arg1: EXP FLOATING(f) -> EXP FLOATING(r)
arg1 is evaluated and will produce floating point value, fp. The value fp is delivered, changed to the representation of the FLOATING_VARIETY r.
Either r and f will both real or both complex.
If there is a floating point error it is handled by flpt_err.
5.16.17. change_variety
| Encoding number | 17 |
ov_err: ERROR_TREATMENT r: VARIETY arg1: EXP INTEGER(v) -> EXP INTEGER(r)
arg1 is evaluated and will produce an integer value, a. The value a is delivered, changed to the representation of the VARIETY r.
If a is not contained in the VARIETY being used to represent r, an overflow occurs and is handled according to ov_err.
5.16.18. change_int_to_bitfield
| Encoding number | 18 |
bv: BITFIELD_VARIETY arg1: EXP INTEGER(v) -> EXP BITFIELD(bv)
arg1 is evaluated and converted to a BITFIELD(bv).
If arg1 exceed the bounds of bv, the effect is undefined.
5.16.19. complex_conjugate
| Encoding number | 19 |
c: EXP FLOATING(cv) -> EXP FLOATING(cv)
Delivers the complex conjugate of c.
cv will be a complex floating variety.
5.16.20. component
| Encoding number | 20 |
sha: SHAPE arg1: EXP COMPOUND(EXP OFFSET(x, y)) arg2: EXP OFFSET(x, alignment(sha)) -> EXP sha
arg1 is evaluated to produce a COMPOUND value. The component of this value at the OFFSET given by arg2 is delivered. This will have SHAPE sha.
arg2 will be a constant and non-negative (see Constant evaluation).
If sha is a BITFIELD then arg2, sha will be variety_enclosed (see section 7.24).
5.16.21. concat_nof
| Encoding number | 21 |
arg1: EXP NOF(n, s) arg2: EXP NOF(m, s) -> EXP NOF(n+m, s)
arg1 and arg2 are evaluated and their results concatenated. In the result the components derived from arg1 will have lower indices than those derived from arg2.
5.16.22. conditional
| Encoding number | 22 |
altlab_intro: LABEL first: EXP x alt: EXP z -> EXP (x LUB z)
first is evaluated. If first produces a result, f, this value is delivered as the result of the whole construct, and alt is not evaluated.
If goto(altlab_intro) or any other jump (including long_jump) to altlab_intro is obeyed during the evaluation of first, then the evaluation of first will stop, alt will be evaluated and its result delivered as the result of the construction.
The lifetime of altlab_intro is the evaluation of first. altlab_intro will not be used within alt.
The actual order of evaluation of the constituents shall be indistinguishable in all observable effects (apart from time) from evaluating all the obeyed parts of first before any obeyed part of alt. Note that this specifically includes any defined error handling.
For LUB see Least Upper Bound.
5.16.23. contents
| Encoding number | 23 |
s: SHAPE arg1: EXP POINTER(x) -> EXP s
A value of SHAPE s will be extracted from the start of the space indicated by the pointer, and this is delivered.
x will include alignment(s).
s will not be a BITFIELD.
If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.
If the value delivered by arg1 is a null pointer the effect is undefined.
The constraint “x will include alignment(s)” ensures in the simple memory model that no change is needed to the POINTER.
5.16.24. contents_with_mode
| Encoding number | 24 |
md: TRANSFER_MODE s: SHAPE arg1: EXP POINTER(x) -> EXP s
A value of SHAPE s will be extracted from the start of the space indicated by the pointer, and this is delivered. The operation will be carried out as specified by the TRANSFER_MODE (q.v.).
If md consists of standard_transfer_mode only, then contents_with_mode is the same as contents.
x will include alignment(s).
s will not be a BITFIELD.
If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.
If the value delivered by arg1 is a null pointer the effect is undefined.
5.16.25. current_env
| Encoding number | 25 |
-> EXP POINTER(fa)
A value of SHAPE POINTER(fa) is created and delivered. It gives access to the variables, identities and parameters in the current procedure activation which are declared as having ACCESS visible.
If the immediately enclosing procedure is defined by make_general_proc, then fa is the set union of local_alignment and the alignments of the kinds of parameters defined. That is to say, if there are caller parameters, then the alignment includes callers_alignment(x) where x is true if and only if the PROCPROPS var_callers is present; if there are callee parameters, the alignment includes callees_alignment(x) where x is true if and only if the PROCPROPS var_callees is present.
If the immediately enclosing procedure is defined by make_proc, then fa = { locals_alignment, callers_alignment(false) }.
If an OFFSET produced by env_offset is added to a POINTER produced by current_env from an activation of the procedure which contains the declaration of the TAG used by env_offset, then the result is an original POINTER, notwithstanding the normal rules for add_to_ptr (see Original pointers).
If an OFFSET produced by env_offset is added to such a pointer from an inappropriate procedure the effect is undefined.
5.16.26. div0
| Encoding number | 26 |
div_by_0_err: ERROR_TREATMENT ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. Either the value a D1 b or the value a D2 b is delivered as the result of the construct, with the same SHAPE as the arguments. Different occurrences of div0 in the same capsule can use D1 or D2 independently.
If b is zero a div_by_zero error occurs and is handled by div_by_0_err.
If b is not zero and the result cannot be expressed in the VARIETY being used to represent v an overflow occurs and is handled by ov_err.
Producers may assume that shifting and div0 by a constant which is a power of two yield equally good code.
See Division and modulus for the definitions of D1, D2, M1 and M2.
5.16.27. div1
| Encoding number | 27 |
div_by_0_err: ERROR_TREATMENT ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The value a D1 b is delivered as the result of the construct, with the same SHAPE as the arguments.
If b is zero a div_by_zero error occurs and is handled by div_by_0_err.
If b is not zero and the result cannot be expressed in the VARIETY being used to represent v an overflow occurs and is handled by ov_err.
Producers may assume that shifting and div1 by a constant which is a power of two yield equally good code.
See Division and modulus for the definitions of D1, D2, M1 and M2.
5.16.28. div2
| Encoding number | 28 |
div_by_0_err: ERROR_TREATMENT ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The value a D2 b is delivered as the result of the construct, with the same SHAPE as the arguments.
If b is zero a div_by_zero error occurs and is handled by div_by_0_err.
If b is not zero and the result cannot be expressed in the VARIETY being used to represent v an overflow occurs and is handled by ov_err.
Producers may assume that shifting and div2 by a constant which is a power of two yield equally good code if the lower bound of v is zero.
See Division and modulus for the definitions of D1, D2, M1 and M2.
5.16.29. env_offset
| Encoding number | 29 |
fa: ALIGNMENT y: ALIGNMENT t: TAG x -> EXP OFFSET(fa, y)
t will be the tag of a variable, identify or procedure parameter with the visible property within a procedure defined by make_general_proc or make_proc.
If it is defined in a make_general_proc, let P be its associated PROCPROPS; otherwise let P be the PROCPROPS {locals_alignment, caller_alignment(false)}.
If t is the TAG of a variable or identify, fa will contain locals_alignment; if it is a caller parameter fa will contain a caller_alignment(b) where b is true if and only if P contains var_callers ; if it is a callee parameter fa will contain a callee_alignment(b) where b is true if and only if P contains var_callees.
If t is the TAG of a variable or parameter, the result is the OFFSET of its position, within any procedure environment which derives from the procedure containing the declaration of the variable or parameter, relative to its environment pointer. In this case x will be POINTER(y).
If t is the TAG of an identify, the result will be an OFFSET of space which holds the value. This pointer will not be used to alter the value. In this case y will be alignment(x).
See section 7.10.
5.16.30. env_size
| Encoding number | 30 |
proctag: TAG PROC
-> EXP OFFSET(locals_alignment, {}) Delivers an OFFSET of a space sufficient to contain all the variables and identifications, explicit or implicit in the procedure identified by proctag. This will not include the space required for any local_allocs or procedure calls within the procedure.
proctag will be defined in the current CAPSULE by a TAGDEF identification of a make_proc or a make_general_proc.
5.16.31. fail_installer
| Encoding number | 31 |
message: STRING(k, n) -> EXP BOTTOM
Any attempt to use this operation to produce code will result in a failure of the installation process. message will give information about the reason for this failure which should be passed to the installation manager.
5.16.32. float_int
| Encoding number | 32 |
flpt_err: ERROR_TREATMENT f: FLOATING_VARIETY arg1: EXP INTEGER(v) -> EXP FLOATING(f)
arg1 is evaluated to produce an integer value, which is converted to the representation of f and delivered.
If f is complex the real part of the result will be derived from arg1 and the imaginary part will be zero.
If there is a floating point error it is handled by flpt_err. See Floating point errors.
5.16.33. floating_abs
| Encoding number | 33 |
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) -> EXP FLOATING(f)
arg1 is evaluated and will produce a floating point value, a, of the FLOATING_VARIETY, f. The absolute value of a is delivered as the result of the construct, with the same SHAPE as the argument.
Though floating_abs cannot produce an overflow it can give an invalid operand exception which is handled by flpt_err.
f will not be complex.
See also Floating point accuracy.
5.16.34. floating_div
| Encoding number | 34 |
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP FLOATING(f)
arg1 and arg2 are evaluated and will produce floating point values, a and b, of the same FLOATING_VARIETY, f. The value a/b is delivered as the result of the construct, with the same SHAPE as the arguments.
If there is a floating point error it is handled by flpt_err. See Floating point errors.
See also Floating point accuracy.
5.16.35. floating_minus
| Encoding number | 35 |
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP FLOATING(f)
arg1 and arg2 are evaluated and will produce floating point values, a and b, of the same FLOATING_VARIETY, f. The value a-b is delivered as the result of the construct, with the same SHAPE as the arguments.
If there is a floating point error it is handled by flpt_err. See Floating point errors.
See also Floating point accuracy.
5.16.36. floating_maximum
| Encoding number | 36 |
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP FLOATING(f)
The maximum of the values delivered by arg1 and arg2 is the result. f will not be complex.
If arg1 and arg2 are incomparable, flpt_err will be invoked.
See also Floating point accuracy.
5.16.37. floating_minimum
| Encoding number | 37 |
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP FLOATING(f)
The minimum of the values delivered by arg1 and arg2 is the result. f will not be complex.
If arg1 and arg2 are incomparable, flpt_err will be invoked.
See also Floating point accuracy.
5.16.38. floating_mult
| Encoding number | 38 |
flpt_err: ERROR_TREATMENT arg1: LIST(EXP) -> EXP FLOATING(f)
The arguments, arg1, are evaluated producing floating point values all of the same FLOATING_VARIETY, f. These values are multiplied in any order and the result of this multiplication is delivered as the result of the construct, with the same SHAPE as the arguments.
If there is a floating point error it is handled by flpt_err. See 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.
5.16.39. floating_negate
| Encoding number | 39 |
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) -> EXP FLOATING(f)
arg1 is evaluated and will produce a floating point value, a, of the FLOATING_VARIETY, f. The value -a is delivered as the result of the construct, with the same SHAPE as the argument.
Though floating_negate cannot produce an overflow it can give an invalid operand exception which is handled by flpt_err.
See also Floating point accuracy.
5.16.40. floating_plus
| Encoding number | 40 |
flpt_err: ERROR_TREATMENT arg1: LIST(EXP) -> EXP FLOATING(f)
The arguments, arg1, are evaluated producing floating point values, all of the same FLOATING_VARIETY, f. These values are added in any order and the result of this addition is delivered as the result of the construct, with the same SHAPE as the arguments.
If there is a floating point error it is handled by flpt_err. See 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.
5.16.41. floating_power
| Encoding number | 41 |
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) arg2: EXP INTEGER(v) -> EXP FLOATING(f)
The result of arg1 is raised to the power given by arg2.
If there is a floating point error it is handled by flpt_err. See Floating point errors.
See also Floating point accuracy.
5.16.42. floating_test
| Encoding number | 42 |
prob: OPTION(NAT) flpt_err: ERROR_TREATMENT nt: NTEST dest: LABEL arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP TOP
arg1 and arg2 are evaluated and will produce floating point values, a and b, of the same FLOATING_VARIETY, f. These values are compared using nt.
If f is complex then nt will be equal or not_equal.
If a nt b, this construction yields TOP. Otherwise control passes to dest.
If prob is present, prob/100 gives the probability that control will continue to the next construct (ie. not pass to dest). If prob is absent this probability is unknown.
If there is a floating point error it is handled by flpt_err. See Floating point errors.
See also Floating point accuracy.
5.16.43. goto
| Encoding number | 43 |
dest: LABEL -> EXP BOTTOM
Control passes to the EXP labelled dest. This construct will only be used where dest is in scope.
5.16.44. goto_local_lv
| Encoding number | 44 |
arg1: EXP POINTER({code})
-> EXP BOTTOM arg1 is evaluated. The label from which the value delivered by arg1 was created will be within its lifetime and this construction will be obeyed in the same activation of the same procedure as the creation of the POINTER({code}) by make_local_lv. Control passes to this activation of this LABEL.
If arg1 delivers a null POINTER the effect is undefined.
5.16.45. identify
| Encoding number | 45 |
opt_access: OPTION(ACCESS) name_intro: TAG x definition: EXP x body: EXP y -> EXP y
definition is evaluated to produce a value, v. Then body is evaluated. During this evaluation, v is bound to name_intro. This means that inside body an evaluation of obtain_tag(name_intro) will produce the value, v.
The value delivered by identify is that produced by body.
The TAG given for name_intro will not be reused within the current UNIT. No rules for the hiding of one TAG by another are given: this will not happen. The lifetime of name_intro is the evaluation of body.
If opt_access contains visible, it means that the value must not be aliased while the procedure containing this declaration is not the current procedure. Hence if there are any copies of this value they will need to be refreshed when the procedure is returned to. The easiest implementation when opt_access is visible may be to keep the value in memory, but this is not a necessary requirement.
The order in which the constituents of definition and body are evaluated shall be indistinguishable in all observable effects (apart from time) from completely evaluating definition before starting body. See the note about order in sequence.
5.16.46. ignorable
| Encoding number | 46 |
arg1: EXP x -> EXP x
If the result of this construction is discarded, arg1 need not be evaluated, though evaluation is permitted. If the result is used it is the result of arg1.
5.16.47. imaginary_part
| Encoding number | 47 |
arg1: EXP c -> EXP FLOATING (float_of_complex(c))
c will be complex. Delivers the imaginary part of the value produced by arg1.
5.16.48. initial_value
| Encoding number | 48 |
init: EXP s -> EXP s
Any tag used as an argument of an obtain_tag in init will be global or defined within init.
All labels used in init will be defined within init.
init will be evaluated once only before any procedure application, other than those involved in this or other initial_value constructions, but after all load-time constant initialisations of TAGDEFs. The result of this evaluation is the value of the construction.
The order of evaluation of the different initial_values in a program is undefined.
See section 7.29.
5.16.49. integer_test
| Encoding number | 49 |
prob: OPTION(NAT) nt: NTEST dest: LABEL arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP TOP
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. These values are compared using nt.
If a nt b, this construction yields TOP. Otherwise control passes to dest.
If prob is present, prob/100 gives the probability that control will continue to the next construct (ie. not pass to dest). If prob is absent this probability is unknown.
5.16.50. labelled
| Encoding number | 50 |
labs_intro: LIST(LABEL) starter: EXP x places: LIST(EXP) -> EXP w
The lists labs_intro and places shall have the same number of elements.
To evaluate the construction starter is evaluated. If its evaluation runs to completion producing a value, then this is delivered as the result of the whole construction. If a goto one of the LABELs in labs_intro or any other jump to one of these LABELs is evaluated, then the evaluation of starter stops and the corresponding element of places is evaluated. In the canonical ordering all the operations which are evaluated from starter are completed before any from an element of places is started. If the evaluation of the member of places produces a result this is the result of the construction.
If a jump to any of the labs_intro is obeyed then evaluation continues similarly. Such jumping may continue indefinitely, but if any places terminates, then the value it produces is the value delivered by the construction.
The SHAPE w is the LUB of x and all the places. See Least Upper Bound.
The actual order of evaluation of the constituents shall be indistinguishable in all observable effects (apart from time) from that described above. Note that this specifically includes any defined error handling.
The lifetime of each of the LABELs in labs_intro, is the evaluation of starter and all the elements of places.
5.16.51. last_local
| Encoding number | 51 |
x: EXP OFFSET(y, z) -> EXP POINTER(alloca_alignment)
If the last use of local_alloc in the current activation of the current procedure was after the last use of local_free or local_free_all, then the value returned is the last POINTER allocated with local_alloc.
If the last use of local_free in the current activation of the current procedure was after the last use of local_alloc, then the result is the POINTER last allocated which is still active.
The ALIGNMENT, alloca_alignment, includes the set union of all the ALIGNMENTs which can be produced by alignment from any SHAPE. See Special alignments.
5.16.52. local_alloc
| Encoding number | 52 |
arg1: EXP OFFSET(x, y) -> EXP POINTER(alloca_alignment)
The arg1 expression is evaluated and space is allocated sufficient to hold a value of the given size. The result is an original pointer to this space.
x will not consist entirely of bitfield alignments.
The initial contents of the space are not specified.
This allocation is as if on the stack of the current procedure, and the lifetime of the pointer ends when the current activation of the current procedure ends with a return, return_to_label or tail_call or if there is a long jump out of the activation. Any use of the pointer thereafter is undefined. Note the specific exclusion of the procedure ending with untidy_return; in this case the calling procedure becomes the current activation.
The uses of local_alloc within the procedure are ordered dynamically as they occur, and this order affects the meaning of local_free and last_local.
arg1 may be a zero OFFSET. In this case suppose the result is p. Then a subsequent use, in the same activation of the procedure, of
local_free(offset_zero(alloca_alignment), p)
will return the alloca stack to the state it was in immediately before the use of local_alloc.
Note that if a procedure which uses local_alloc is inlined, it may be necessary to use local_free to get the correct semantics.
See also section 7.12.
5.16.53. local_alloc_check
| Encoding number | 53 |
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.
5.16.54. local_free
| Encoding number | 54 |
a: EXP OFFSET(x, y) p: EXP POINTER(alloca_alignment) -> EXP TOP
The POINTER, p, will be an original pointer to space allocated by local_alloc within the current call of the current procedure. It and all spaces allocated after it by local_alloc will no longer be used. This POINTER will have been created by local_alloc with the value of its arg1 equal to the value of a.
Any subsequent use of pointers to the spaces no longer used will be undefined.
5.16.55. local_free_all
| Encoding number | 55 |
-> EXP TOP
Every space allocated by local_alloc within the current call of the current procedure will no longer be used.
Any use of a pointer to space allocated before this operation within the current call of the current procedure is undefined.
Note that if a procedure which uses local_free_all is inlined, it may be necessary to use local_free to get the correct semantics.
5.16.56. long_jump
| Encoding number | 56 |
arg1: EXP POINTER(fa)
arg2: EXP POINTER({code})
-> EXP BOTTOM arg1 will be a pointer produced by an application of curent_env in a currently active procedure.
The frame produced by arg1 is reinstated as the current procedure. This frame will still be active. Evaluation recommences at the label given by arg2. This operation will only be used during the lifetime of that label.
Only TAGs declared to have long_jump_access will be defined at the re-entry.
If arg2 delivers a null POINTER({code}) the effect is undefined.
5.16.57. make_complex
| Encoding number | 57 |
c: FLOATING_VARIETY arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP FLOATING(c)
c will be complex and derived from the same parameters as f.
Delivers a complex number with arg1 delivering the real part and arg2 the imaginary.
5.16.58. make_compound
| Encoding number | 58 |
arg1: EXP OFFSET(base, y) arg2: LIST(EXP) -> EXP COMPOUND(arg1)
Let the ith component (i starts at one) of arg2 be x[i]. The list may be empty.
The components x[2 * k] are values which are to be placed at OFFSETs given by x[2 * k - 1]. These OFFSETs will be constants and non-negative.
The OFFSET x[2 * k - 1] will have the SHAPE OFFSET(zk, alignment(shape(x[2 * k]))), where shape gives the SHAPE of the component and base includes zk.
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 OFFSETs are equal and the values have the same SHAPE. If they coincide the corresponding values x[2 * k] will have VARIETY SHAPEs 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).
5.16.59. make_floating
| Encoding number | 59 |
f: FLOATING_VARIETY rm: ROUNDING_MODE negative: BOOL mantissa: STRING(k, n) base: NAT exponent: SIGNED_NAT -> EXP FLOATING(f)
f will not be complex.
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*( baseexponent) 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.
5.16.60. make_general_proc
| Encoding number | 60 |
result_shape: SHAPE prcprops: OPTION(PROCPROPS) caller_intro: LIST(TAGSHACC) callee_intro: LIST(TAGSHACC) body: EXP BOTTOM -> EXP PROC
Evaluation of make_general_proc delivers a PROC. When this procedure is applied to parameters using apply_general_proc, space is allocated to hold the actual values of the parameters caller_intro and callee_intro. The values produced by the actual parameters are used to initialise these spaces. Then body is evaluated. During this evaluation the TAGs in caller_intro and callee_intro are bound to original POINTERs to these spaces. The lifetime of these TAGs is the evaluation of body.
The SHAPE of body will be BOTTOM. caller_intro and callee_intro may be empty.
The TAGs introduced in the parameters will not be reused within the current UNIT.
The SHAPEs in the parameters specify the SHAPE of the corresponding TAGs.
The OPTION(ACCESS) (in params_intro) specifies the ACCESS properties of the corresponding parameter, just as for a variable declaration.
In body the only TAGs 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 TAGs 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 TAGs 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.
5.16.61. make_int
| Encoding number | 61 |
v: VARIETY value: SIGNED_NAT -> EXP INTEGER(v)
An integer value is delivered of which the value is given by value, and the VARIETY by v. The SIGNED_NAT value will lie between the bounds of v.
5.16.62. make_local_lv
| Encoding number | 62 |
lab: LABEL
-> EXP POINTER({code}) A POINTER({code}) lv is created and delivered. It can be used as an argument to goto_local_lv or long_jump. If and when one of these is evaluated with lv as an argument, control will pass to lab.
5.16.63. make_nof
| Encoding number | 63 |
arg1: LIST(EXP) -> EXP NOF(n, s)
Creates an array of n values of SHAPE s, containing the given values produced by evaluating the members of arg1 in the same order as they occur in the list.
n will not be zero.
5.16.64. make_nof_int
| Encoding number | 64 |
v: VARIETY str: STRING(k, n) -> EXP NOF(n, INTEGER(v))
An NOF INTEGER is delivered. The conversions are carried out as if the elements of str were INTEGER(var_limits(0, 2k-1)). n may be zero.
5.16.65. make_null_local_lv
| Encoding number | 65 |
-> EXP POINTER({code}) Makes a null POINTER({code}) which can be detected by pointer_test. The effect of goto_local_lv or long_jump applied to this value is undefined.
All null POINTER({code}) are equal to each other and unequal to any other POINTERs.
5.16.66. make_null_proc
| Encoding number | 66 |
-> EXP PROC
A null PROC is created and delivered. The null PROC may be tested for by using proc_test. The effect of using it as the first argument of apply_proc is undefined.
All null PROC are equal to each other and unequal to any other PROC.
5.16.67. make_null_ptr
| Encoding number | 67 |
a: ALIGNMENT -> EXP POINTER(a)
A null POINTER(a) is created and delivered. The null POINTER may be tested for by pointer_test.
a will not include code.
All null POINTER(x) are equal to each other and unequal to any other POINTER(x).
5.16.68. make_proc
| Encoding number | 68 |
result_shape: SHAPE params_intro: LIST(TAGSHACC) var_intro: OPTION(TAGACC) body: EXP BOTTOM -> EXP PROC
Evaluation of make_proc delivers a PROC. When this procedure is applied to parameters using apply_proc, space is allocated to hold the actual values of the parameters params_intro and var_intro (if present). The values produced by the actual parameters are used to initialise these spaces. Then body is evaluated. During this evaluation the TAGs in params_intro and var_intro are bound to original POINTERs to these spaces. The lifetime of these TAGs is the evaluation of body.
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 ALIGNMENTs 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 TAGs introduced in the parameters will not be reused within the current UNIT.
The SHAPEs in the parameters specify the SHAPE of the corresponding TAGs.
The OPTION(ACCESS) (in params_intro) specifies the ACCESS properties of the corresponding parameter, just as for a variable declaration.
In body the only TAGs 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 TAGs 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 TAGs 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.
5.16.69. make_stack_limit
| Encoding number | 116 |
stack_base: EXP POINTER(fa) frame_size: EXP OFFSET(locals_alignment, x) alloc_size: EXP OFFSET(alloca_alignment, y) -> EXP POINTER(fb)
This creates a POINTER suitable for use with set_stack_limit.
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 isperformed:
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.
5.16.70. make_top
| Encoding number | 69 |
-> EXP TOP
make_top delivers a value of SHAPE TOP (i.e. void).
5.16.71. make_value
| Encoding number | 70 |
s: SHAPE -> EXP s
This EXP creates some value with the representation of the SHAPE s. This value will have the correct size, but its representation is not specified. It can be assigned, be the result of a contents, a parameter or result of a procedure, or the result of any construction (like sequence) which delivers the value delivered by an internal EXP. But if it is used for arithmetic or as a POINTER for taking contents or add_to_ptr etc. the effect is undefined.
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.
5.16.72. maximum
| Encoding number | 71 |
arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
The arguments will be evaluated and the maximum of the values delivered is the result.
5.16.73. minimum
| Encoding number | 72 |
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.
5.16.74. minus
| Encoding number | 73 |
ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The difference a-b is delivered as the result of the construct, with the same 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.
5.16.75. move_some
| Encoding number | 74 |
md: TRANSFER_MODE arg1: EXP POINTER(x) arg2: EXP POINTER(y) arg3: EXP OFFSET(z, t) -> EXP TOP
The arguments are evaluated to produce p1, p2, and sz respectively. A quantity of data measured by sz in the space indicated by p1 is moved to the space indicated by p2. The operation will be carried out as specified by the 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.
5.16.76. mult
| Encoding number | 75 |
ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The product a*b is delivered as the result of the construct, with the same 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.
5.16.77. n_copies
| Encoding number | 76 |
n: NAT arg1: EXP x -> EXP NOF(n, x)
arg1 is evaluated and an NOF value is delivered which contains n copies of this value. n can be zero or one or greater.
Producers are encouraged to use n_copies to initialise arrays of known size.
5.16.78. negate
| Encoding number | 78 |
ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 is evaluated and will produce an integer value, a. The value -a is delivered as the result of the construct, with the same SHAPE as the argument.
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.
5.16.79. not
| Encoding number | 78 |
arg1: EXP INTEGER(v) -> EXP INTEGER(v)
The argument is evaluated producing an integer value, of VARIETY, v. The result is the bitwise not of this value in the representing VARIETY. The result is delivered as the result of the construct, with the same SHAPE as the arguments.
5.16.80. obtain_tag
| Encoding number | 79 |
t: TAG x -> EXP x
The value with which the TAG t is bound is delivered. The SHAPE of the result is the SHAPE of the value with which the TAG is bound.
5.16.81. offset_add
| Encoding number | 80 |
arg1: EXP OFFSET(x, y) arg2: EXP OFFSET(z, t) -> EXP OFFSET(x, t)
The two arguments deliver OFFSETs. The result is the sum of these OFFSETs, 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.
5.16.82. offset_div
| Encoding number | 81 |
v: VARIETY arg1: EXP OFFSET(x, x) arg2: EXP OFFSET(x, x) -> EXP INTEGER(v)
The two arguments deliver OFFSETs, a and b. The result is a/b, as an INTEGER of VARIETY, v. Division is interpreted in the same sense (with respect to remainder) as in div0.
The value produced by arg2 will be non-zero.
5.16.83. offset_div_by_int
| Encoding number | 82 |
arg1: EXP OFFSET(x, x) arg2: EXP INTEGER(v) -> EXP OFFSET(x, x)
The result is the OFFSET produced by arg1 divided by arg2, as an OFFSET(x, x).
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
5.16.84. offset_max
| Encoding number | 83 |
arg1: EXP OFFSET(x, y) arg2: EXP OFFSET(z, y) -> EXP OFFSET(unite_alignments(x, z), y)
The two arguments deliver OFFSETs. The result is the maximum of these OFFSETs, 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.
5.16.85. offset_mult
| Encoding number | 84 |
arg1: EXP OFFSET(x, x) arg2: EXP INTEGER(v) -> EXP OFFSET(x, x)
The first argument gives an OFFSET, off, and the second an integer, n. The result is the product of these, as an offset.
The result shall be equal to offset_adding off n times to offset_zero(x).
5.16.86. offset_negate
| Encoding number | 85 |
arg1: EXP OFFSET(x, x) -> EXP OFFSET(x, x)
The inverse of the argument is delivered.
In the simple memory model this can be represented by negate.
5.16.87. offset_pad
| Encoding number | 86 |
a: ALIGNMENT arg1: EXP OFFSET(z, t) -> EXP OFFSET(unite_alignments(z, a), a)
arg1 is evaluated giving off. The next greater or equal OFFSET at which a value of ALIGNMENT a can be placed is delivered. That is, there shall not exist an OFFSET of the same SHAPE as the result which is greater than or equal to off and less than the result, in the sense of offset_test.
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.
5.16.88. offset_subtract
| Encoding number | 87 |
arg1: EXP OFFSET(x, y) arg2: EXP OFFSET(x, z) -> EXP OFFSET(z, y)
The two arguments deliver offsets, p and q. The result is p-q, as an offset.
Note that x will include y, x will include z and z will include y, by the constraints on OFFSETs.
offset_subtract and offset_add do not have the conventional relationship because offset_add can lose information, which cannot be regenerated by offset_subtract.
5.16.89. offset_test
| Encoding number | 88 |
prob: OPTION(NAT) nt: NTEST dest: LABEL arg1: EXP OFFSET(x, y) arg2: EXP OFFSET(x, y) -> EXP TOP
arg1 and arg2 are evaluated and will produce offset values, a and b. These values are compared using nt.
If a nt b, this construction yields TOP. Otherwise control passes to dest.
If prob is present, prob/100 gives the probability that control will continue to the next construct (ie. not pass to dest). If prob is absent this probability is unknown.
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.
5.16.90. offset_zero
| Encoding number | 89 |
a: ALIGNMENT -> EXP OFFSET(a, a)
A zero offset of SHAPE OFFSET(a, a).
offset_pad(b, offset_zero(a)) is a zero offset of SHAPE OFFSET(unite_alignments(a, b), b).
5.16.91. or
| Encoding number | 90 |
arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
The arguments are evaluated producing integer values of the same VARIETY, v. The result is the bitwise or of these two integers in the representing VARIETY. The result is delivered as the result of the construct, with the same SHAPE as the arguments.
5.16.92. plus
| Encoding number | 91 |
ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The sum a+b is delivered as the result of the construct, with the same 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.
5.16.93. pointer_test
| Encoding number | 92 |
prob: OPTION(NAT) nt: NTEST dest: LABEL arg1: EXP POINTER(x) arg2: EXP POINTER(x) -> EXP TOP
arg1 and arg2 are evaluated and will produce pointer values, a and b, which will be derived from the same original pointer. These values are compared using nt.
If a nt b, this construction yields TOP. Otherwise control passes to dest.
If prob is present, prob/100 gives the probability that control will continue to the next construct (ie. not pass to dest). If prob is absent this probability is unknown.
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.
5.16.94. power
| Encoding number | 93 |
ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(w) -> EXP INTEGER(v)
arg2 will be non-negative. The result is the result of arg1 raised to the power given by arg2.
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.
5.16.95. proc_test
| Encoding number | 94 |
prob: OPTION(NAT) nt: NTEST dest: LABEL arg1: EXP PROC arg2: EXP PROC -> EXP TOP
arg1 and arg2 are evaluated and will produce PROC values, a and b. These values are compared using nt. The only permitted values of nt are equal and 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.
Two PROCs 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.
5.16.96. profile
| Encoding number | 95 |
uses: NAT -> EXP TOP
The integer uses gives the number of times which this construct is expected to be evaluated.
All uses of profile in the same capsule are to the same scale. They will be mutually consistent.
5.16.97. real_part
| Encoding number | 96 |
arg1: EXP c -> EXP FLOATING (float_of_complex(c))
c will be complex. Delivers the real part of the value produced by arg1.
5.16.98. rem0
| Encoding number | 97 |
div_by_0_err: ERROR_TREATMENT ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The value a M1 b or the value a M2 b is delivered as the result of the construct, with the same SHAPE as the arguments. Different occurrences of rem0 in the same capsule can use M1 or M2 independently.
The following equivalence shall hold:
x = plus(mult(div0(x, y), y), rem0(x, y))
if all the ERROR_TREATMENTs are impossible, and x and y have no side effects.
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.
5.16.99. rem1
| Encoding number | 98 |
div_by_0_err: ERROR_TREATMENT ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The value a M1 b is delivered as the result of the construct, with the same SHAPE as the arguments.
If b is zero a div_by_zero error occurs and is handled by div_by_0_err.
If b is not zero and 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.
5.16.100. rem2
| Encoding number | 99 |
div_by_0_err: ERROR_TREATMENT ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b, of the same VARIETY, v. The value a M2 b is delivered as the result of the construct, with the same SHAPE as the arguments.
If b is zero a div_by_zero error occurs and is handled by
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.
5.16.101. repeat
| Encoding number | 100 |
replab_intro: LABEL start: EXP TOP body: EXP y -> EXP y
start is evaluated. Then body is evaluated.
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.
5.16.102. return
| Encoding number | 101 |
arg1: EXP x -> EXP BOTTOM
arg1 is evaluated to produce a value, v. The evaluation of the immediately enclosing procedure ceases and v is delivered as the result of the procedure.
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.
5.16.103. return_to_label
| Encoding number | 102 |
lab_val: EXP POINTER code_alignment -> EXP BOTTOM
lab_val will be a label value in the calling procedure.
The evaluation of the immediately enclosing procedure ceases and control is passed to the calling procedure at the label given by lab_val.
5.16.104. round_with_mode
| Encoding number | 103 |
flpt_err: ERROR_TREATMENT mode: ROUNDING_MODE r: VARIETY arg1: EXP FLOATING(f) -> EXP INTEGER(r)
arg is evaluated to produce a floating point value, v. This is rounded to an integer of VARIETY, r, using the ROUNDING_MODE, mode. This is the result of the construction.
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.
5.16.105. rotate_left
| Encoding number | 104 |
arg1: EXP INTEGER(v) arg2: EXP INTEGER(w) -> EXP INTEGER(v)
The value delivered by arg1 is rotated left arg2 places.
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.
5.16.106. rotate_right
| Encoding number | 105 |
arg1: EXP INTEGER(v) arg2: EXP INTEGER(w) -> EXP INTEGER(v)
The value delivered by arg1 is rotated right arg2 places.
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.
5.16.107. sequence
| Encoding number | 106 |
statements: LIST(EXP) result: EXP x -> EXP x
The statements are evaluated in the same order as the list, statements, and their results are discarded. Then result is evaluated and its result forms the result of the construction.
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.
5.16.108. set_stack_limit
| Encoding number | 107 |
lim: EXP POINTER({locals_alignment, alloca_alignment})
-> EXP TOP set_stack_limit sets the limits of remaining free stack space to lim. This include both the frame stack limit and the local_alloc stack. Note that, in implementations where the frame stack and local_alloc stack are distinct, this pointer will have a special representation, appropriate to its frame alignment. Thus the pointer should always be generated using make_stack_limit or its equivalent formation.
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.
5.16.109. shape_offset
| Encoding number | 108 |
s: SHAPE
-> EXP OFFSET(alignment(s), {}) This construction delivers the “size” of a value of the given 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.
5.16.110. shift_left
| Encoding number | 109 |
ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(w) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b. The value a shifted left b places is delivered as the result of the construct, with the same SHAPE as a.
b will be non-negative and will be strictly less than the number of bits needed to represent 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.
Producers may assume that shift_left and multiplication by a power of two yield equally efficient code.
5.16.111. shift_right
| Encoding number | 110 |
arg1: EXP INTEGER(v) arg2: EXP INTEGER(w) -> EXP INTEGER(v)
arg1 and arg2 are evaluated and will produce integer values, a and b. The value a shifted right b places is delivered as the result of the construct, with the same SHAPE as arg1.
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.
5.16.112. subtract_ptrs
| Encoding number | 111 |
arg1: EXP POINTER(y) arg2: EXP POINTER(x) -> EXP OFFSET(x, y)
arg1 and arg2 are evaluated to produce pointers p1 and p2, which will be derived from the same original pointer. The result, r, is the OFFSET from p2 to p1. Both arguments will be derived from the same original pointer.
Note that add_to_ptr(p2, r) = p1.
5.16.113. tail_call
| Encoding number | 112 |
prcprops: OPTION(PROCPROPS) p: EXP PROC callee_pars: CALLEES -> EXP BOTTOM
p is called in the sense of apply_general_proc with the caller parameters of the immediately enclosing proc and CALLEES given by callee_pars and PROCPROPS prcprops.
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.
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.
5.16.114. untidy_return
| Encoding number | 113 |
arg1: EXP x -> EXP BOTTOM
arg1 is evaluated to produce a value, v. The evaluation of the immediately enclosing procedure ceases and v is delivered as the result of the procedure, in such a manner as that pointers to any callee parameters or local allocations are valid in the calling procedure.
untidy_return can only occur in a procedure defined by make_general_proc with PROCPROPS including untidy.
5.16.115. variable
| Encoding number | 114 |
opt_access: OPTION(ACCESS) name_intro: TAG POINTER(alignment(x)) init: EXP x body: EXP y -> EXP y
init is evaluated to produce a value, v. Space is allocated to hold a value of SHAPE x and this is initialised with v. Then body is evaluated. During this evaluation, an original POINTER pointing to the allocated space is bound to name_intro. This means that inside body an evaluation of obtain_tag(name_intro) will produce a POINTER to this space. The lifetime of name_intro is the evaluation of body.
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.
5.16.116. xor
| Encoding number | 115 |
arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)
The arguments are evaluated producing integer values of the same VARIETY, v. The result is the bitwise xor of these two integers in the representing VARIETY. The result is delivered as the result of the construct, with the same SHAPE as the arguments.
5.17. EXTERNAL
| Number of encoding bits | 2 |
| Is coding extendable | yes |
An EXTERNAL defines the classes of external name available for connecting the internal names inside a CAPSULE to the world outside the CAPSULE.
5.17.1. string_extern
| Encoding number | 1 |
s: BYTE_ALIGN TDFIDENT(n) -> EXTERNAL
string_extern produces an EXTERNAL identified by the TDFIDENT s.
5.17.2. unique_extern
| Encoding number | 2 |
u: BYTE_ALIGN UNIQUE -> EXTERNAL
unique_extern produces an EXTERNAL identified by the UNIQUE u.
5.17.3. chain_extern
| Encoding number | 3 |
s: BYTE_ALIGN TDFIDENT prev: TDFINT -> EXTERNAL
This construct is redundant and should not be used.
5.18. EXTERN_LINK
| Number of encoding bits | 0 |
| Is coding extendable | no |
An auxiliary SORT providing a list of LINKEXTERN.
5.18.1. make_extern_link
| Encoding number | 0 |
el: SLIST(LINKEXTERN) -> EXTERN_LINK
make_capsule requires a SLIST(EXTERN_LINK) to express the links between the linkable entities and the named (by EXTERNALs) values outside the CAPSULE.
5.19. FLOATING_VARIETY
| Number of encoding bits | 3 |
| Is coding extendable | yes |
These describe kinds of floating point number.
5.19.1. flvar_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> FLOATING_VARIETY
The token is applied to the arguments to give a FLOATING_VARIETY
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.19.2. flvar_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM FLOATING_VARIETY e2: BITSTREAM FLOATING_VARIETY -> FLOATING_VARIETY
The control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.19.3. flvar_parms
| Encoding number | 3 |
base: NAT mantissa_digs: NAT min_exponent: NAT max_exponent: NAT -> FLOATING_VARIETY
base is the base with respect to which the remaining numbers refer. base will be a power of 2.
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_VARIETYs 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 baseq-1 M < baseq -min_exponent N max_exponent
Zero will also be represented exactly in any FLOATING_VARIETY.
5.19.4. complex_parms
| Encoding number | 4 |
base: NAT mantissa_digs: NAT min_exponent: NAT max_exponent: NAT -> FLOATING_VARIETY
A FLOATING_VARIETY described by complex_parms holds a complex number which is likely to be represented by its real and imaginary parts, each of which is as if defined by flvar_parms with the same arguments.
5.19.5. float_of_complex
| Encoding number | 5 |
csh: SHAPE -> FLOATING_VARIETY
csh will be a complex SHAPE.
Delivers the FLOATING_VARIETY required for the real (or imaginary) part of a complex SHAPE csh.
5.19.6. complex_of_float
| Encoding number | 6 |
fsh: SHAPE -> FLOATING_VARIETY
fsh will be a floating SHAPE.
Delivers FLOATING_VARIETY required for a complex number whose real (and imaginary) parts have SHAPE fsh.
5.20. GROUP
| Number of encoding bits | 0 |
| Is coding extendable | no |
A GROUP is a list of UNITs with the same unit identification.
5.20.1. make_group
| Encoding number | 0 |
us: SLIST(UNIT) -> GROUP
make_capsule contains a list of GROUPS. Each member of this list has a different unit identification deduced from the prop_name argument of make_capsule.
5.21. LABEL
| Number of encoding bits | 1 |
| Is coding extendable | yes |
A LABEL marks an EXP in certain constructions, and is used in jump-like constructions to change the control to the labelled construction.
5.21.1. label_apply_token
| Encoding number | 2 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> LABEL x
The token is applied to the arguments to give a LABEL.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.21.2. make_label
| Encoding number | 1 |
labelno: TDFINT -> LABEL
Labels are represented in TDF by integers, but they are not linkable. Hence the definition and all uses of a LABEL occur in the same UNIT.
5.22. LINK
| Number of encoding bits | 0 |
| Is coding extendable | no |
A LINK expresses the connection between two variables of the same SORT.
5.22.1. make_link
| Encoding number | 0 |
unit_name: TDFINT capsule_name: TDFINT -> LINK
A LINK defines a linkable entity declared inside a UNIT as unit_name to correspond to a CAPSULE linkable entity having the same linkable entity identification. The CAPSULE linkable entity is capsule_name.
A LINK is normally constructed by the TDF builder in the course of resolving sharing and name clashes when constructing a composite CAPSULE.
5.23. LINKEXTERN
| Number of encoding bits | 0 |
| Is coding extendable | no |
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.
5.23.1. make_linkextern
| Encoding number | 0 |
internal: TDFINT ext: EXTERNAL -> LINKEXTERN
make_linkextern produces a LINKEXTERN connecting an object identified within a CAPSULE by a TAG, TOKEN, AL_TAG or any linkable entity constructed from internal, with an EXTERNAL, ext. The EXTERNAL is an identifier which linkers and similar programs can use.
5.24. LINKS
| Number of encoding bits | 0 |
| Is coding extendable | no |
5.24.1. make_links
| Encoding number | 0 |
ls: SLIST(LINK) -> LINKS
make_unit uses a 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.
5.25. NAT
| Number of encoding bits | 3 |
| Is coding extendable | yes |
These are non-negative integers of unlimited size.
5.25.1. nat_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> NAT
The token is applied to the arguments to give a NAT.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.25.2. nat_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM NAT e2: BITSTREAM NAT -> NAT
The control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.25.3. computed_nat
| Encoding number | 3 |
arg: EXP INTEGER(v) -> NAT
arg will be an install-time non-negative constant. The result is that constant.
5.25.4. error_val
| Encoding number | 4 |
err: ERROR_code -> NAT
Gives the NAT corresponding to the ERROR_code err. Each distinct ERROR_code will give a different NAT.
5.25.5. make_nat
| Encoding number | 5 |
n: TDFINT -> NAT
n is a non-negative integer of unbounded magnitude.
5.26. NTEST
| Number of encoding bits | 4 |
| Is coding extendable | yes |
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).
5.26.1. ntest_apply
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> NTEST
The token is applied to the arguments to give a NTEST.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.26.2. ntest_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM NTEST e2: BITSTREAM NTEST -> NTEST
The control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.26.3. equal
| Encoding number | 3 |
-> NTEST
Signifies “equal” test.
5.26.4. greater_than
| Encoding number | 4 |
-> NTEST
Signifies “greater than” test.
5.26.5. greater_than_or_equal
| Encoding number | 5 |
-> NTEST
Signifies “greater than or equal” test.
5.26.6. less_than
| Encoding number | 6 |
-> NTEST
Signifies “less than” test.
5.26.7. less_than_or_equal
| Encoding number | 7 |
-> NTEST
Signifies “less than or equal” test.
5.26.8. not_equal
| Encoding number | 8 |
-> NTEST
Signifies “not equal” test.
5.26.9. not_greater_than
| Encoding number | 9 |
-> NTEST
Signifies “not greater than” test.
5.26.10. not_greater_than_or_equal
| Encoding number | 10 |
-> NTEST
Signifies “not (greater than or equal)” test.
5.26.11. not_less_than
| Encoding number | 11 |
-> NTEST
Signifies “not less than” test.
5.26.12. not_less_than_or_equal
| Encoding number | 12 |
-> NTEST
Signifies “not (less than or equal)” test.
5.26.13. less_than_or_greater_than
| Encoding number | 13 |
-> NTEST
Signifies “less than or greater than” test.
5.26.14. not_less_than_and_not_greater_than
| Encoding number | 14 |
-> NTEST
Signifies “not less than and not greater than” test.
5.26.15. comparable
| Encoding number | 15 |
-> NTEST
Signifies “comparable” test.
With all operands SHAPEs except FLOATING, this comparison is always true.
5.26.16. not_comparable
| Encoding number | 16 |
-> NTEST
Signifies “not comparable” test.
With all operands SHAPEs except FLOATING, this comparison is always false.
5.27. OTAGEXP
| Number of encoding bits | 0 |
| Is coding extendable | no |
This is a auxilliary SORT used in apply_general_proc.
5.27.1. make_otagexp
| Encoding number | 0 |
tgopt: OPTION(TAG x) e: EXP x -> OTAGEXP
e is evaluated and its value is the actual caller parameter. If tgopt is present, the TAG will be bound to the final value of caller parameter in the postlude part of the apply_general_proc.
5.28. PROCPROPS
| Number of encoding bits | 4 |
| Is coding extendable | yes |
PROCPROPS is a set of properties ascribed to procedure definitions and calls.
5.28.1. procprops_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> PROCPROPS
The token is applied to the arguments to give a PROCPROPS.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters in the order specified.
5.28.2. procprops_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM PROCPROPS e2: BITSTREAM PROCPROPS -> PROCPROPS
The control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.28.3. add_procprops
| Encoding number | 3 |
arg1: PROCPROPS arg2: PROCPROPS -> PROCPROPS
Delivers the join of arg1 and arg2.
5.28.4. check_stack
| Encoding number | 4 |
-> PROCPROPS
The procedure body is required to check for stack overflow.
5.28.5. inline
| Encoding number | 5 |
-> PROCPROPS
The procedure body is a good candidate for inlining at its application.
5.28.6. no_long_jump_dest
| Encoding number | 6 |
-> PROCPROPS
The procedure body will contain no label which is the destination of a long_jump.
5.28.7. untidy
| Encoding number | 7 |
-> PROCPROPS
The procedure body may be exited using an untidy_return.
5.28.8. var_callees
| Encoding number | 8 |
-> PROCPROPS
Applications of the procedure may have different numbers of actual callee parameters.
5.28.9. var_callers
| Encoding number | 9 |
-> PROCPROPS
Applications of the procedure may have different numbers of actual caller parameters.
5.29. PROPS
A 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_TAGs standing forALIGNMENTs; -
declarations of
TAGs standing forEXPs; -
definitions of the
EXPs for whichTAGsstand; -
declarations of
TOKENs standing for pieces of TDF program; -
definitions of the pieces of TDF program for which
TOKENs 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 UNITs is identified by a unit identification - a TDFIDENT. All the UNITs in that GROUP are of the same kind.
In addition there is a tld UNIT, see The TDF encoding.
5.30. ROUNDING_MODE
| Number of encoding bits | 3 |
| Is coding extendable | yes |
ROUNDING_MODE specifies the way rounding is to be performed in floating point arithmetic.
5.30.1. rounding_mode_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> ROUNDING_MODE
The token is applied to the arguments to give a ROUNDING_MODE.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.30.2. rounding_mode_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM ROUNDING_MODE e2: BITSTREAM ROUNDING_MODE -> ROUNDING_MODE
The control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.30.3. round_as_state
| Encoding number | 3 |
-> ROUNDING_MODE
Round as specified by the current state of the machine.
5.30.4. to_nearest
| Encoding number | 4 |
-> ROUNDING_MODE
Signifies rounding to nearest. The effect when the number lies half-way is not specified.
5.30.5. toward_larger
| Encoding number | 5 |
-> ROUNDING_MODE
Signifies rounding toward next largest.
5.30.6. toward_smaller
| Encoding number | 6 |
-> ROUNDING_MODE
Signifies rounding toward next smallest.
5.30.7. toward_zero
| Encoding number | 7 |
-> ROUNDING_MODE
Signifies rounding toward zero.
5.31. SHAPE
| Number of encoding bits | 4 |
| Is coding extendable | yes |
SHAPEs express symbolic size and representation information about run time values.
SHAPEs are constructed from primitive SHAPEs which describe values such as procedures and integers, and recursively from compound construction in terms of other SHAPEs.
5.31.1. shape_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> SHAPE
The token is applied to the arguments to give a SHAPE.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.31.2. shape_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM SHAPE e2: BITSTREAM SHAPE -> SHAPE
The control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.31.3. bitfield
| Encoding number | 3 |
bf_var: BITFIELD_VARIETY -> SHAPE
A BITFIELD is used to represent a pattern of bits which will be packed, provided that the variety_enclosed constraints are not violated. (see See section 7.24)
A BITFIELD_VARIETY specifies the number of bits and whether they are considered to be signed.
There are very few operations on BITFIELDs, which have to be converted to INTEGERs before arithmetic can be performed on them.
An installer may place a limit on the number of bits it implements. See Permitted limits.
5.31.4. bottom
| Encoding number | 4 |
-> SHAPE
BOTTOM is the SHAPE which describes a piece of program which does not evaluate to any result. Examples include goto and return.
If BOTTOM is a parameter to any other SHAPE constructor, the result is BOTTOM.
5.31.5. compound
| Encoding number | 5 |
sz: EXP OFFSET(x, y) -> SHAPE
The SHAPE constructor COMPOUND describes cartesian products and unions.
The alignments x and y will be alignment(sx) and alignment(sy) for some SHAPEs 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.
5.31.6. floating
| Encoding number | 6 |
fv: FLOATING_VARIETY -> SHAPE
Most of the floating point arithmetic operations, floating_plus, floating_minus etc., are defined to work in the same way on different kinds of floating point number. If these operations have more than one argument the arguments have to be of the same kind, and the result is of the same kind.
See Representing floating point.
An installer may limit the FLOATING_VARIETYs it can represent. A statement of any such limits shall be part of the specification of an installer. See Representing floating point.
5.31.7. integer
| Encoding number | 7 |
var: VARIETY -> SHAPE
The different kinds of INTEGER are distinguished by having different VARIETYs. A fundamental VARIETY (not a TOKEN or conditional) is represented by two SIGNED_NATs, 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 VARIETYs of the two arguments must be identical. An example illustrates this. A piece of TDF which attempted to add two values whose SHAPEs were:
INTEGER(0, 60000) and INTEGER(0, 30000)
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 two INTEGERs are going to be represented in the same way in all machines is to stipulate that their VARIETYs 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.
5.31.8. nof
| Encoding number | 8 |
n: NAT s: SHAPE -> SHAPE
The NOF constructor describes the SHAPE of a value consisting of an array of n values of the same SHAPE, s.
5.31.9. offset
| Encoding number | 9 |
arg1: ALIGNMENT arg2: ALIGNMENT -> SHAPE
The SHAPE constructor OFFSET describes values which represent the differences between POINTERs, 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 POINTERs 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_VARIETYs.
The set arg1 will include the set arg2.
See Memory Model.
5.31.10. pointer
| Encoding number | 10 |
arg: ALIGNMENT -> SHAPE
A 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_VARIETYs. See Memory Model.
5.31.11. proc
| Encoding number | 11 |
-> SHAPE
PROC is the SHAPE which describes pieces of program.
5.31.12. top
| Encoding number | 12 |
-> SHAPE
TOP is the SHAPE which describes pieces of program which return no useful value. assign is an example: it performs an assignment, but does not deliver any useful value.
5.32. SIGNED_NAT
| Number of encoding bits | 3 |
| Is coding extendable | yes |
These are positive or negative integers of unbounded size.
5.32.1. signed_nat_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> SIGNED_NAT
The token is applied to the arguments to give a SIGNED_NAT.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.32.2. signed_nat_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM SIGNED_NAT e2: BITSTREAM SIGNED_NAT -> SIGNED_NAT
The control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.32.3. computed_signed_nat
| Encoding number | 3 |
arg: EXP INTEGER(v) -> SIGNED_NAT
arg will be an install-time constant. The result is that constant.
5.32.4. make_signed_nat
| Encoding number | 4 |
neg: TDFBOOL n: TDFINT -> SIGNED_NAT
n is a non-negative integer of unbounded magnitude. The result is negative if and only if neg is true.
5.32.5. snat_from_nat
| Encoding number | 5 |
neg: BOOL n: NAT -> SIGNED_NAT
The result is negated if and only if neg is true.
5.33. SORTNAME
| Number of encoding bits | 5 |
| Is coding extendable | yes |
These are the names of the SORTs which can be parameters of TOKEN definitions.
5.33.1. access
| Encoding number | 1 |
-> SORTNAME
5.33.2. al_tag
| Encoding number | 2 |
-> SORTNAME
5.33.3. alignment_sort
| Encoding number | 3 |
-> SORTNAME
5.33.4. bitfield_variety
| Encoding number | 4 |
-> SORTNAME
5.33.5. bool
| Encoding number | 5 |
-> SORTNAME
5.33.6. error_treatment
| Encoding number | 6 |
-> SORTNAME
5.33.7. exp
| Encoding number | 7 |
-> SORTNAME
5.33.8. floating_variety
| Encoding number | 8 |
-> SORTNAME
5.33.9. foreign_sort
| Encoding number | 9 |
foreign_name: STRING(k, n) -> SORTNAME
This SORT enables unanticipated kinds of information to be placed in TDF.
5.33.10. label
| Encoding number | 10 |
-> SORTNAME
5.33.11. nat
| Encoding number | 11 |
-> SORTNAME
5.33.12. ntest
| Encoding number | 12 |
-> SORTNAME
5.33.13. procprops
| Encoding number | 13 |
-> SORTNAME
5.33.14. rounding_mode
| Encoding number | 14 |
-> SORTNAME
5.33.15. shape
| Encoding number | 15 |
-> SORTNAME
5.33.16. signed_nat
| Encoding number | 16 |
-> SORTNAME
5.33.17. string
| Encoding number | 17 |
-> SORTNAME
5.33.18. tag
| Encoding number | 18 |
-> SORTNAME
The SORT of TAG.
5.33.19. transfer_mode
| Encoding number | 19 |
-> SORTNAME
5.33.20. token
| Encoding number | 20 |
result: SORTNAME params: LIST(SORTNAME) -> SORTNAME
The SORTNAME of a TOKEN. Note that it can have tokens as parameters, but not as result.
5.33.21. variety
| Encoding number | 21 |
-> SORTNAME
5.34. STRING
| Number of encoding bits | 3 |
| Is coding extendable | yes |
5.34.1. string_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> STRING(k, n)
The token is applied to the arguments to give a STRING
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.34.2. string_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM STRING e2: BITSTREAM STRING -> STRING(k, n)
The control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.34.3. concat_string
| Encoding number | 3 |
arg1: STRING(k, n) arg2: STRING(k, m) -> STRING(k, n+m)
Gives a STRING which is the concatenation of arg1 with arg2.
5.34.4. make_string
| Encoding number | 4 |
arg: TDFSTRING(k, n) -> STRING(k, n)
Delivers the STRING identical to the arg.
5.35. TAG
| Number of encoding bits | 1 |
| Is coding extendable | yes |
| Linkable entity identification | tag |
These are used to name values and variables in the run time program.
5.35.1. tag_apply_token
| Encoding number | 2 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> TAG x
The token is applied to the arguments to give a TAG.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.35.2. make_tag
| Encoding number | 1 |
tagno: TDFINT -> TAG x
make_tag produces a TAG identified by tagno.
5.36. TAGACC
| Number of encoding bits | 0 |
| Is coding extendable | no |
Constructs a pair of a TAG and an OPTION(ACCESS) for use in make_proc.
5.36.1. make_tagacc
| Encoding number | 0 |
tg: TAG POINTER var_param_alignment acc: OPTION(ACCESS) -> TAGACC
Constructs the pair for make_proc.
5.37. TAGDEC
| Number of encoding bits | 2 |
| Is coding extendable | yes |
A TAGDEC declares a TAG for incorporation into a TAGDEC_PROPS.
5.37.1. make_id_tagdec
| Encoding number | 1 |
t_intro: TDFINT acc: OPTION(ACCESS) signature: OPTION(STRING) x: SHAPE -> TAGDEC
A TAGDEC announcing that the TAG t_intro identifies an EXP of SHAPE x is constructed.
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.
5.37.2. make_var_tagdec
| Encoding number | 2 |
t_intro: TDFINT acc: OPTION(ACCESS) signature: OPTION(STRING) x: SHAPE -> TAGDEC
A TAGDEC announcing that the TAG t_intro identifies an EXP of SHAPE POINTER(alignment (x)) is constructed.
acc specifies the ACCESS properties of the TAG.
If there is a make_var_tagdec for a TAG then all other make_var_tagdecs for the same TAG will specify SHAPEs with identical ALIGNMENT and there will be no make_id_tagdec or common_tagdec for the TAG.
If two make_var_tagdecs 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.
5.37.3. common_tagdec
| Encoding number | 3 |
t_intro: TDFINT acc: OPTION(ACCESS) signature: OPTION(STRING) x: SHAPE -> TAGDEC
A TAGDEC announcing that the TAG t_intro identifies an EXP of SHAPE POINTER(alignment (x)) is constructed.
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 SHAPEs will have a maximum. The maximum of two SHAPEs, 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) andCOMPOUND(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) andNOF(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.
If two common_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.
5.38. TAGDEC_PROPS
| Number of encoding bits | 0 |
| Is coding extendable | no |
| Unit identification | tagdec |
5.38.1. make_tagdecs
| Encoding number | 0 |
no_labels: TDFINT tds: SLIST(TAGDEC) -> TAGDEC_PROPS
no_labels is the number of local LABELs used in tds. tds is a list of TAGDECs which declare the SHAPEs associated with TAGs.
5.39. TAGDEF
| Number of encoding bits | 2 |
| Is coding extendable | yes |
A value of SORT TAGDEF gives the definition of a TAG for incorporation into a TAGDEF_PROPS.
5.39.1. make_id_tagdef
| Encoding number | 1 |
t: TDFINT signature: OPTION(STRING) e: EXP x -> TAGDEF
make_id_tagdef produces a TAGDEF defining the TAG x constructed from the TDFINT, t. This TAG is defined to stand for the value delivered by e.
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.
5.39.2. make_var_tagdef
| Encoding number | 2 |
t: TDFINT opt_access: OPTION(ACCESS) signature: OPTION(STRING) e: EXP x -> TAGDEF
make_var_tagdef produces a TAGDEF defining the TAG POINTER(alignment(x)) constructed from the TDFINT, t. This TAG stands for a variable which is initialised with the value delivered by e. The 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.
5.39.3. common_tagdef
| Encoding number | 3 |
t: TDFINT opt_access: OPTION(ACCESS) signature: OPTION(STRING) e: EXP x -> TAGDEF
common_tagdef produces a TAGDEF defining the TAG POINTER(alignment(x)) constructed from the TDFINT, t. This TAG stands for a variable which is initialised with the value delivered by e. The 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 EXPs, 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) andCOMPOUND(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) andNOF(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.
5.40. TAGDEF_PROPS
| Number of encoding bits | 0 |
| Is coding extendable | no |
| Unit identification | tagdef |
5.40.1. make_tagdefs
| Encoding number | 0 |
no_labels: TDFINT tds: SLIST(TAGDEF) -> TAGDEF_PROPS
no_labels is the number of local LABELs used in tds. tds is a list of TAGDEFs which give the EXPs which are the definitions of values associated with TAGs.
5.41. TAGSHACC
| Number of encoding bits | 0 |
| Is coding extendable | no |
5.41.1. make_tagshacc
| Encoding number | 0 |
sha: SHAPE opt_access: OPTION(ACCESS) tg_intro: TAG -> TAGSHACC
This is an auxiliary construction to make the elements of params_intro in make_proc.
5.42. TDFBOOL
A TDFBOOL is the TDF encoding of a boolean. See Fundamental encoding.
5.43. TDFIDENT
A TDFIDENT(k, n) encodes a sequence of n unsigned integers of size k bits. k will be a multiple of 8. See Fundamental encoding.
This construction will not be used inside a BITSTREAM.
5.44. TDFINT
A TDFINT is the TDF encoding of an unbounded unsigned integer constant. See Fundamental encoding.
5.45. TDFSTRING
A TDFSTRING(k, n) encodes a sequence of n unsigned integers of size k bits. See Fundamental encoding.
5.46. TOKDEC
| Number of encoding bits | 1 |
| Is coding extendable | yes |
A TOKDEC declares a TOKEN for incorporation into a UNIT.
5.46.1. make_tokdec
| Encoding number | 1 |
tok: TDFINT signature: OPTION(STRING) s: SORTNAME -> TOKDEC
The sort of the token tok is declared to be s. Note that s will always be a token SORT, with a list of parameter SORTs (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.
5.47. TOKDEC_PROPS
| Number of encoding bits | 0 |
| Is coding extendable | no |
| Unit identification | tokdec |
5.47.1. make_tokdecs
| Encoding number | 0 |
tds: SLIST(TOKDEC) -> TOKDEC_PROPS
tds is a list of TOKDECs which gives the sorts associated with TOKENs.
5.48. TOKDEF
| Number of encoding bits | 1 |
| Is coding extendable | yes |
tds is a list of TOKDECs which gives the sorts associated with TOKENs.
5.48.1. make_tokdef
| Encoding number | 1 |
tok: TDFINT signature: OPTION(STRING) def: BITSTREAM TOKEN_DEFN -> TOKDEF
A TOKDEF is constructed which defines the TOKEN tok to stand for the fragment of TDF, body, which may be of any SORT with a SORTNAME, except for token. The SORT of the result, result_sort, is given by the first component of the 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 TOKENs within body.
5.49. TOKDEF_PROPS
| Number of encoding bits | 0 |
| Is coding extendable | no |
| Unit identification | tokdef |
5.49.1. make_tokdefs
| Encoding number | 0 |
no_labels: TDFINT tds: SLIST(TOKDEF) -> TOKDEF_PROPS
no_labels is the number of local LABELs used in tds. tds is a list of TOKDEFs which gives the definitions associated with TOKENs.
5.50. TOKEN
| Number of encoding bits | 2 |
| Is coding extendable | yes |
| Linkable entity identification | token |
These are used to stand for functions evaluated at installation time. They are represented by TDFINTs.
5.50.1. token_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> TOKEN
The token is applied to the arguments to give a TOKEN.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.50.2. make_tok
| Encoding number | 2 |
tokno: TDFINT -> TOKEN
make_tok constructs a TOKEN identified by tokno.
5.50.3. use_tokdef
| Encoding number | 3 |
tdef: BITSTREAM TOKEN_DEFN -> TOKEN
tdef is used to supply the definition, as in make_tokdef. Note that TOKENs are only used in x_apply_token constructions.
5.51. TOKEN_DEFN
| Number of encoding bits | 1 |
| Is coding extendable | yes |
An auxiliary SORT used in make_tokdef and use_tokdef.
5.51.1. token_definition
| Encoding number | 1 |
result_sort: SORTNAME tok_params: LIST(TOKFORMALS) body: result_sort -> TOKEN_DEFN
Makes a token definition. result_sort is the SORT of body. tok_params is a list of formal TOKENs and their SORTs. body is the definition, which can use the formal TOKENs defined in tok_params.
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 SORTs. During this expansion all token applications in the actual parameters are expanded.
Second, the definition is copied, making fresh TAGs and LABELs where these are introduced in identify, variable, labelled, conditional, make_proc, make_general_proc and repeat constructions. Any other TAGs or LABELs 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 (TOKENs, TAGs, LABELs, AL_TAGs etc.) “in scope” at the site of the TOKEN_DEFN.
Thus, in a make_tokdef, the context consists of the set of TOKENs 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 LABELs and the only TAGs 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 TAGs or LABELs 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.
5.52. TOKFORMALS
| Number of encoding bits | 0 |
| Is coding extendable | no |
5.52.1. make_tokformals
| Encoding number | 0 |
sn: SORTNAME tk: TDFINT -> TOKFORMALS
An auxiliary construction to make up the elements of the lists in token_definition.
5.53. TRANSFER_MODE
| Number of encoding bits | 3 |
| Is coding extendable | yes |
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.
5.53.1. transfer_mode_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> TRANSFER_MODE
The token is applied to the arguments encoded in the BITSTREAM token_args to give a 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 SORTs of its arguments in the SORTNAME component. The BITSTREAM in token_args consists of these SORTs in the given order. If no token declaration or definition exists in the CAPSULE, the BITSTREAM cannot be read.
5.53.2. transfer_mode_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM TRANSFER_MODE e2: BITSTREAM TRANSFER_MODE -> TRANSFER_MODE
control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.53.3. add_modes
| Encoding number | 3 |
md1: TRANSFER_MODE md2: TRANSFER_MODE -> TRANSFER_MODE
A construction qualified by add_modes has both TRANSFER_MODES md1 and md2. If md1 is standard_transfer_mode then the result is md2 and symmetrically. This operation is associative and commutative.
5.53.4. overlap
| Encoding number | 4 |
-> TRANSFER_MODE
If overlap is used to qualify a move_some or an assign_with_mode for which arg2 is a contents or contents_with_mode, then the source and destination might overlap. The transfer shall be made as if the data were copied from the source to an independent place and thence to the destination.
See Overlapping.
5.53.5. standard_transfer_mode
| Encoding number | 5 |
-> TRANSFER_MODE
This TRANSFER_MODE implies no special properties.
5.53.6. trap_on_nil
| Encoding number | 6 |
-> TRANSFER_MODE
If trap_on_nil is used to qualify a contents_with_mode operation with a nil pointer argument, or an assign_with_mode whose arg1 is a nil pointer, or a move_some with either argument a nil pointer, the TDF exception nil_access is raised.
5.53.7. volatile
| Encoding number | 7 |
-> TRANSFER_MODE
If volatile is used to qualify a construction it shall not be optimised away.
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.
5.53.8. complete
| Encoding number | 8 |
-> TRANSFER_MODE
A transfer qualified with complete shall leave the destination unchanged if the evaluation of the value transferred is left with a jump.
5.54. UNIQUE
| Number of encoding bits | 0 |
| Is coding extendable | no |
These are used to provide world-wide unique names for TOKENs and TAGs.
This implies a registry for allocating UNIQUE values.
5.54.1. make_unique
| Encoding number | 0 |
text: SLIST(TDFIDENT) -> UNIQUE
Two UNIQUE values are equal if and only if they were constructed with equal arguments.
5.55. UNIT
| Number of encoding bits | 0 |
| Is coding extendable | no |
A UNIT gathers together a PROPS and LINKs 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.
5.55.1. make_unit
| Encoding number | 0 |
local_vars: SLIST(TDFINT) lks: SLIST(LINKS) properties: BYTESTREAM PROPS -> UNIT
local_vars gives the number of linkable entities of each kind. These numbers correspond (in the same order) to the variable sorts in cap_linking in make_capsule. The linkable entities will be represented by TDFINTs in the range 0 to the corresponding nl-1.
lks gives the LINKs 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.
5.56. VARIETY
| Number of encoding bits | 2 |
| Is coding extendable | yes |
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.
5.56.1. var_apply_token
| Encoding number | 1 |
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> VARIETY
The token is applied to the arguments to give a VARIETY.
If there is a definition for token_value in the CAPSULE then token_args is a BITSTREAM encoding of the SORTs of its parameters, in the order specified.
5.56.2. var_cond
| Encoding number | 2 |
control: EXP INTEGER(v) e1: BITSTREAM VARIETY e2: BITSTREAM VARIETY -> VARIETY
The control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
5.56.3. var_limits
| Encoding number | 3 |
lower_bound: SIGNED_NAT upper_bound: SIGNED_NAT -> VARIETY
lower_bound is the lower limit (inclusive) of the range of values which shall be representable in the resulting VARIETY, and upper_bound is the upper limit (inclusive).
5.56.4. var_width
| Encoding number | 4 |
signed_width: BOOL width: NAT -> VARIETY
If signed_width is true then this construction is equivalent to var_limits(-2width-1, 2width-1-1). If signed_width is false then this construction is var_limits (0, 2width-1).
5.57. VERSION_PROPS
| Number of encoding bits | 0 |
| Is coding extendable | no |
| Unit identification | versions |
This UNIT gives information about version numbers and user information.
5.57.1. make_versions
| Encoding number | 0 |
version_info: SLIST(VERSION) -> VERSION_PROPS
Contains version information.
5.58. VERSION
| Number of encoding bits | 1 |
| Is coding extendable | yes |
5.58.1. make_version
| Encoding number | 1 |
major_version: TDFINT minor_version: TDFINT -> VERSION
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.
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.
5.58.2. user_info
| Encoding number | 2 |
information: STRING(k, n) -> VERSION
This is (usually character) information included in the TDF for labelling purposes.
information will be produced by make_string.