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.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> ACCESSThe token is applied to the arguments encoded in the
BITSTREAM
token_args to give an ACCESS.
The notation param_sorts(token_value) is intended to mean the
following. The token definition or token declaration for
token_value gives the SORTs of its arguments in
the
SORTNAME component. The BITSTREAM in
token_args consists of these SORTs in the given
order. If no token declaration or definition exists in the
CAPSULE, the BITSTREAM cannot be read.
control: EXP INTEGER(v) e1: BITSTREAM ACCESS e2: BITSTREAM ACCESS -> ACCESScontrol is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
a1: ACCESS a2: ACCESS -> ACCESSA construction qualified with add_accesses has both
ACCESS properties a1 and a2. This operation
is associative and commutative.
-> ACCESSOnly a variable (not an identity) may be qualified with constant. A variable qualified with constant will retain its initialising value unchanged throughout its lifetime.
-> ACCESSAn 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.
-> ACCESSThis 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.
-> ACCESSThis 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.
-> ACCESSAn 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.
-> ACCESSThis property refers to a global object. It says that the object will be included in the final program, whether or not all possible accesses to that object are optimised away; for example by inlining all possible uses of procedure object.
-> ACCESSIndicates that an object with this property is frequently used. This can be taken as a recommendation to place it in a register.
-> ACCESSAn object qualified as having standard_access has normal (i.e. no special) access properties.
-> ACCESSAn 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.
-> ACCESSAn 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.
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}.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> AL_TAGThe token is applied to the arguments encoded in the
BITSTREAM
token_args to give an AL_TAG.
If there is a definition for token_value in the CAPSULE
then token_args is a BITSTREAM encoding of the
SORTs of its parameters, in the order specified.
al_tagno: TDFINT -> AL_TAGmake_al_tag constructs an
AL_TAG identified by
al_tagno.
An AL_TAGDEF gives the definition of an AL_TAG
for incorporation into a AL_TAGDEF_PROPS.
t: TDFINT a: ALIGNMENT -> AL_TAGDEFThe
AL_TAG identified by t is defined to stand
for the ALIGNMENT a. All the AL_TAGDEFs
in a CAPSULE must be considered together as a set of
simultaneous equations defining ALIGNMENT values for
the AL_TAGs. No order is imposed on the definitions.
In any particular CAPSULE the set of equations may be
incomplete, but a CAPSULE which is being translated into
code will have a set of equations which defines all the
AL_TAGs which it uses.
The result of the evaluation of the control argument of any
x_cond construction (e.g alignment_cond) used in a
shall be independent of any AL_TAGs used in the
control. Simultaneous equations defining ALIGNMENTs
can then always be solved.
See Circular types in languages.
no_labels: TDFINT tds: SLIST(AL_TAGDEF) -> AL_TAGDEF_PROPSno_labels is the number of local
LABELs used in
tds. tds is a list of AL_TAGDEFs which
define the bindings for al_tags.
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).
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> ALIGNMENTThe token is applied to the arguments encoded in the
BITSTREAM
token_args to give an ALIGNMENT.
If there is a definition for token_value in the CAPSULE
then token_args is a BITSTREAM encoding of the
SORTs of its parameters, in the order specified.
control: EXP INTEGER(v) e1: BITSTREAM ALIGNMENT e2: BITSTREAM ALIGNMENT -> ALIGNMENTcontrol is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
sha: SHAPE -> ALIGNMENTThe alignment construct is defined as follows:
PROC then the resulting
ALIGNMENT is {proc}.
INTEGER(v) then the resulting
ALIGNMENT is {v}.
FLOATING(v) then the resulting
ALIGNMENT is {v}.
BITFIELD(v) then the resulting
ALIGNMENT is {v}.
TOP the resulting ALIGNMENT
is {} - the empty set.
BOTTOM the resulting ALIGNMENT
is undefined.
POINTER(x) the resulting
ALIGNMENT is {pointer}.
OFFSET(x, y) the resulting
ALIGNMENT is {offset}.
NOF(n, s) the resulting
ALIGNMENT is alignment(s).
COMPOUND(EXP OFFSET(x,
y)) then the resulting ALIGNMENT is x.
-> ALIGNMENTDelivers the
ALIGNMENT of POINTERs produced
from local_alloc.
var: BOOL -> ALIGNMENTIf var is true the
ALIGNMENT is that of
callee parameters qualified by the PROCPROPS
var_callees. If var is false, the
ALIGNMENT is that of callee parameters not qualified
by
PROCPROPS var_callees.
Delivers the base ALIGNMENT of OFFSETs from
a frame-pointer to a CALLEE parameter. Values of such
OFFSETs can only be produced by env_offset applied
to CALLEE parameters, or offset arithmetic operations
applied to existing OFFSETs.
var: BOOL -> ALIGNMENTIf 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.
-> ALIGNMENTDelivers {code}, the
ALIGNMENT of the
POINTER produced by make_local_lv.
-> ALIGNMENTDelivers the
base ALIGNMENT of OFFSETs from
a frame-pointer to a value defined by variable or identify.
Values of such OFFSETs can only be produced by
env_offset applied to TAGs so defined, or offset
arithmetic operations applied to existing OFFSETs.
at: AL_TAG -> ALIGNMENTobtain_al_tag produces the
ALIGNMENT with which
the AL_TAG at is bound.
sha: SHAPE -> ALIGNMENTDelivers the
ALIGNMENT of a parameter of a procedure
of SHAPE sha.
a1: ALIGNMENT a2: ALIGNMENT -> ALIGNMENTunite_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.
-> ALIGNMENTDelivers the
ALIGNMENT used in the var_param argument
of make_proc.
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.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> BITFIELD_VARIETYThe token is applied to the arguments encoded in the
BITSTREAM
token_args to give a BITFIELD_VARIETY.
If there is a definition for token_value in the CAPSULE
then token_args is a BITSTREAM encoding of the
SORTs of its parameters, in the order specified.
control: EXP INTEGER(v) e1: BITSTREAM BITFIELD_VARIETY e2: BITSTREAM BITFIELD_VARIETY -> BITFIELD_VARIETYcontrol is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
issigned: BOOL bits: NAT -> BITFIELD_VARIETYbfvar_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.
BITSTREAM consists of an encoding of any number of
bits. This encoding is such that any program reading TDF can determine
how to skip over it. To read it meaningfully extra knowledge of what
it represents may be needed.
A BITSTREAM is used, for example, to supply parameters
in a TOKEN application. If there is a definition of this
TOKEN available, this will provide the information needed
to decode the bitstream.
See The TDF encoding.
A BOOL is a piece of TDF which can take two values,
true or false.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> BOOLThe token is applied to the arguments encoded in the
BITSTREAM
token_args to give a BOOL.
If there is a definition for token_value in the CAPSULE
then token_args is a BITSTREAM encoding of the
SORTs of its parameters, in the order specified.
control: EXP INTEGER(v) e1: BITSTREAM BOOL e2: BITSTREAM BOOL -> BOOLcontrol 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.
-> BOOLfalse produces a false
BOOL.
-> BOOLtrue produces a true
BOOL.
BYTESTREAM is analogous to a BITSTREAM,
but is encoded to permit fast copying.
See The TDF encoding.
This is an auxilliary SORT used in calling procedures
by
apply_general_proc and tail_call to provide their actual
callee parameters.
args: LIST(EXP) -> CALLEESThe list of
EXPs args are evaluated in any interleaved
order and the resulting list of values form the actual callee parameters
of the call.
ptr: EXP POINTER(x) sze: EXP OFFSET(x, y) -> CALLEESThe 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.
-> CALLEESThe callee parameters of the call are the same as those of the current procedure.
A CAPSULE is an independent piece of TDF. There is only
one construction, make_capsule.
prop_names: SLIST(TDFIDENT) cap_linking: SLIST(CAPSULE_LINK) ext_linkage: SLIST(EXTERN_LINK) groups: SLIST(GROUP) -> CAPSULEmake_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.
An auxiliary SORT which gives the number of linkable
entities of a given kind at CAPSULE level. It is used
only in make_capsule.
sn: TDFIDENT n: TDFINT -> CAPSULE_LINKn 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.
An auxiliary SORT which provides lower and upper bounds
and the LABEL destination for the case construction.
branch: LABEL lower: SIGNED_NAT upper: SIGNED_NAT -> CASELIMMakes a triple of destination and limits. The case construction uses a list of
CASELIMs. If the control variable of the
case lies between lower
and upper, control passes to branch.
-> ERROR_CODEDelivers the
ERROR_CODE arising from an attempt to access
a nil pointer in an operation with TRANSFER_MODE
trap_on_nil.
-> ERROR_CODEDelivers the
ERROR_CODE arising from a numerical exceptional
result in an operation with ERROR_TREATMENT
trap(overflow).
-> ERROR_CODEDelivers the
ERROR_CODE arising from a stack overflow
in the call of a procedure defined with PROCPROPS
check_stack.
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.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> ERROR_TREATMENTThe token is applied to the arguments encoded in the
BITSTREAM
token_args to give an ERROR_TREATMENT.
If there is a definition for token_value in the CAPSULE
then token_args is a BITSTREAM encoding of the
SORTs of its parameters, in the order specified.
control: EXP INTEGER(v) e1: BITSTREAM ERROR_TREATMENT e2: BITSTREAM ERROR_TREATMENT -> ERROR_TREATMENTcontrol is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
-> ERROR_TREATMENTIf an operation with a continue
ERROR_TREATMENT
causes an error, some value of the correct SHAPE shall
be delivered. This value shall have the same properties as is specified
in make_value.
lab: LABEL -> ERROR_TREATMENTerror_jump produces an
ERROR_TREATMENT which requires
that control be passed to lab if it is invoked. lab
will be in scope.
If a construction has an error_jump ERROR_TREATMENT
and the jump is taken, the canonical order specifies only that the
jump occurs after evaluating the construction. It is not specified
how many further constructions are evaluated.
This rule implies that a further construction is needed to guarantee that errors have been processed. This is not yet included. The effect of nearby procedure calls or exits also needs definition.
trap_list: LIST(ERROR_CODE) -> ERROR_TREATMENTThe 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.
-> ERROR_TREATMENTwrap 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).
-> ERROR_TREATMENTimpossible 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.
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.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> EXP xThe token is applied to the arguments encoded in the
BITSTREAM
token_args to give an EXP.
If there is a definition for token_value in the CAPSULE
then token_args is a BITSTREAM encoding of the
SORTs of its parameters, in the order specified.
control: EXP INTEGER(v) e1: BITSTREAM EXP x e2: BITSTREAM EXP y -> EXP (control ? x : y)control is evaluated. It will be a constant at install time under the constant evaluation rules. If it is non-zero, e1 is installed at this point and e2 is ignored and never processed. If control is zero then e2 is installed at this point and e1 is ignored and never processed.
ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) -> EXP INTEGER(v)The absolute value of the result produced by arg1 is delivered.
If the result cannot be expressed in the VARIETY being
used to represent v, an overflow error is caused and is handled
in the way specified by ov_err.
arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) -> EXP POINTER(z)arg1 is evaluated, giving p, and arg2 is evaluated and the results are added to produce the answer. The result is derived from the pointer delivered by arg1. The intention is to produce a
POINTER displaced from the argument POINTER
by the given amount.
x will include y.
arg1 may deliver a null POINTER. In this case
the result is derived from a null POINTER which counts
as an original POINTER. Further OFFSETs
may be added to the result, but the only other useful operation on
the result of adding a number of OFFSETs to a null POINTER
is to subtract_ptrs a null POINTER from it.
The result will be less than or equal (in the sense of pointer_test) to the result of applying add_to_ptr to the original pointer from which p is derived and the size of the space allocated for the original pointer.
In the simple representation of POINTER arithmetic
(see
Memory Model) add_to_ptr is represented
by addition. The constraint "x includes y" ensures that
no padding has to be inserted in this case.
arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)The arguments are evaluated producing integer values of the same
VARIETY, v. The result is the bitwise and
of the two values in the representing VARIETY. The result
is delivered with the same SHAPE as the arguments.
result_shape: SHAPE p: EXP PROC params: LIST(EXP) var_param: OPTION(EXP) -> EXP result_shapep, 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.
result_shape: SHAPE prcprops: OPTION(PROCPROPS) p: EXP PROC callers_intro: LIST(OTAGEXP) callee_pars: CALLEES postlude: EXP TOP -> EXP result_shapep, callers_intro and callee_pars are evaluated in any order. The procedure, p, is applied to the parameters. The result of the procedure call, which will have result_shape, is delivered as the result of the construction.
If p delivers a null procedure the effect is undefined.
Any TAG introduced by an OTAGEXP in
callers_intro is available in postlude which will be
evaluated after the application.
postlude will not contain any local_allocs or calls of procedures with untidy returns. If prcprops include untidy, postlude will be make_top.
The canonical order of evaluation is as if the definition of p were inlined in a manner dependent on prcprops.
If none of the PROCPROPS var_callers, var_callees
and check_stack are present the inlining is as follows, supposing
that P is the body of the definition of p:
Let Ri be the value of the EXP of the ith
OTAGEXP in callers_intro and Ti be its
TAG (if it is present). Let Ei be the ith
value in callee_pars.
Let ri be the ith formal caller parameter TAG
of p.
Let ei be the ith formal callee parameter TAG
of p.
Each Ri is used to initialise a variable which is identified
by ri; there will be exactly as many Ri as ri.The
scope of these variable definitions is a sequence consisting of three
components - the identification of a TAG res with
the result of a binding of P, followed by a binding of postlude,
followed by an obtain_tag of res giving the result of
the inlined procedure call.
The binding of P consists of using each Ei to initialise a variable identified with ei; there will be exactly as many Ei as ei. The scope of these variable definitions is P modified so that the first return or untidy_return encountered in P gives the result of the binding. If it ends with a return, any space generated by local_allocs within the binding is freed (in the sense of local_free) at this point. If it ends with untidy_return, no freeing will take place.
The binding of postlude consists of identifying each Ti (if present) with the contents of the variable identified by ri. The scope of these identifications is postlude.
If the PROCPROPS var_callers is present, the inlining
process is modified by:
A compound variable is constructed initialised to Ri in order;
the alignment and padding of each individual Ri will be given
by an exact application of parameter_alignment on the
SHAPE of Ri. Each ri is then identified
with a pointer to the copy of Ri within the compound variable;
there will be at least as many Ri as ri. The evaluation
then continues as above with the scope of these identifications being
the sequence.
If the PROCPROPS var_callees is present, the inlining
process is modified by:
The binding of P is done by generating (as if by local_alloc)
a pointer to space for a compound value constructed from each Ei
in order (just as for var_callers). Each ei is identified
with a pointer to the copy of Ei within the generated space;
there will be at least as many ei as Ei. P is evaluated
within the scope of these identifications as before. Note that the
generation of space for these callee parameters is a local_alloc
with the binding of P, and hence will not be freed if P ends with
an
untidy_return.
arg1: EXP POINTER(x) arg2: EXP y -> EXP TOPThe 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.
md: TRANSFER_MODE arg1: EXP POINTER(x) arg2: EXP y -> EXP TOPThe 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.
arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) arg3: EXP BITFIELD(v) -> EXP TOPThe 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).
md: TRANSFER_MODE arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) arg3: EXP BITFIELD(v) -> EXP TOPThe value delivered by arg3 is assigned at a displacement given by arg2 from the pointer delivered by arg1.The assignment will be carried out as specified by the
TRANSFER_MODE
(q.v.).
If md consists of standard_transfer_mode only, then bitfield_assign_with_mode is the same as bitfield_assign.
x will include y and z will include v.
arg2, BITFIELD(v) will be
variety-enclosed.(see section 7.24).
v: BITFIELD_VARIETY arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) -> EXP BITFIELD(v)The bitfield of
BITFIELD_VARIETY v, located at
the displacement delivered by arg2 from the pointer delivered
by arg1 is extracted and delivered.
x will include y and z will include v.
arg2, BITFIELD(v) will be variety_enclosed
(see section 7.24).
md: TRANSFER_MODE v: BITFIELD_VARIETY arg1: EXP POINTER(x) arg2: EXP OFFSET(y, z) -> EXP BITFIELD(v)The bitfield of
BITFIELD_VARIETY v, located at
the displacement delivered by arg2 from the pointer delivered
by arg1 is extracted and delivered.The operation will be carried
out as specified by the TRANSFER_MODE (q.v.).
If md consists of standard_transfer_mode only, then bitfield_contents_with_mode is the same as bitfield_contents.
x will include y and z will include v.
arg2, BITFIELD(v) will be variety_enclosed
(see section 7.24).
exhaustive: BOOL control: EXP INTEGER(v) branches: LIST(CASELIM) -> EXP (exhaustive ? BOTTOM : TOP)control is evaluated to produce an integer value, c. Then c is tested to see if it lies inclusively between lower and upper, for each element of branches. If this tests succeeds, control passes to the label branch belonging to that
CASELIM (see section 5.13). If c
lies between no pair, the construct delivers a value of
SHAPE TOP. The order in which the comparisons are made
is undefined.
The sets of SIGNED_NATs in branches will be disjoint.
If exhaustive is true the value delivered by control will lie between one of the lower/upper pairs.
v: VARIETY arg1: EXP BITFIELD(bv) -> EXP INTEGER(v)arg1 is evaluated and converted to a
INTEGER(v).
If arg1 exceed the bounds of v, the effect is undefined.
flpt_err: ERROR_TREATMENT r: FLOATING_VARIETY arg1: EXP FLOATING(f) -> EXP FLOATING(r)arg1 is evaluated and will produce floating point value, fp. The value fp is delivered, changed to the representation of the
FLOATING_VARIETY r.
Either r and f will both real or both complex.
If there is a floating point error it is handled by flpt_err.
ov_err: ERROR_TREATMENT r: VARIETY arg1: EXP INTEGER(v) -> EXP INTEGER(r)arg1 is evaluated and will produce an integer value, a. The value a is delivered, changed to the representation of the
VARIETY r.
If a is not contained in the VARIETY being used
to represent r, an overflow occurs and is handled according
to ov_err.
bv: BITFIELD_VARIETY arg1: EXP INTEGER(v) -> EXP BITFIELD(bv)arg1 is evaluated and converted to a
BITFIELD(bv).
If arg1 exceed the bounds of bv, the effect is undefined.
c: EXP FLOATING(cv) -> EXP FLOATING(cv)Delivers the complex conjugate of c.
cv will be a complex floating variety.
sha: SHAPE arg1: EXP COMPOUND(EXP OFFSET(x, y)) arg2: EXP OFFSET(x, alignment(sha)) -> EXP shaarg1 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).
arg1: EXP NOF(n, s) arg2: EXP NOF(m, s) -> EXP NOF(n+m, s)arg1 and arg2 are evaluated and their results concatenated. In the result the components derived from arg1 will have lower indices than those derived from arg2.
altlab_intro: LABEL first: EXP x alt: EXP z -> EXP (x LUB z)first is evaluated. If first produces a result, f, this value is delivered as the result of the whole construct, and alt is not evaluated.
If goto(altlab_intro) or any other jump (including long_jump) to altlab_intro is obeyed during the evaluation of first, then the evaluation of first will stop, alt will be evaluated and its result delivered as the result of the construction.
The lifetime of altlab_intro is the evaluation of first. altlab_intro will not be used within alt.
The actual order of evaluation of the constituents shall be indistinguishable in all observable effects (apart from time) from evaluating all the obeyed parts of first before any obeyed part of alt. Note that this specifically includes any defined error handling.
For LUB see Least Upper Bound.
s: SHAPE arg1: EXP POINTER(x) -> EXP sA value of
SHAPE s will be extracted from the
start of the space indicated by the pointer, and this is delivered.
x will include alignment(s).
s will not be a BITFIELD.
If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.
If the value delivered by arg1 is a null pointer the effect is undefined.
The constraint "x will include alignment(s)" ensures
in the simple memory model that no change is needed to the POINTER.
md: TRANSFER_MODE s: SHAPE arg1: EXP POINTER(x) -> EXP sA value of
SHAPE s will be extracted from the
start of the space indicated by the pointer, and this is delivered.
The operation will be carried out as specified by the
TRANSFER_MODE (q.v.).
If md consists of standard_transfer_mode only, then contents_with_mode is the same as contents.
x will include alignment(s).
s will not be a BITFIELD.
If the space which the pointer indicates does not lie wholly within the space indicated by the original pointer from which it is derived, the effect is undefined.
If the value delivered by arg1 is a null pointer the effect is undefined.
-> EXP POINTER(fa)A value of
SHAPE POINTER(fa) is created and delivered.
It gives access to the variables, identities and parameters in the
current procedure activation which are declared as having
ACCESS visible.
If the immediately enclosing procedure is defined by
make_general_proc, then fa is the set union of
local_alignment and the alignments of the kinds of parameters
defined. That is to say, if there are caller parameters, then the
alignment includes callers_alignment(x) where x
is true if and only if the PROCPROPS var_callers
is present; if there are callee parameters, the alignment includes
callees_alignment(x) where x is true if and only
if the
PROCPROPS var_callees is present.
If the immediately enclosing procedure is defined by make_proc, then fa = { locals_alignment, callers_alignment(false) }.
If an OFFSET produced by env_offset is added to
a
POINTER produced by current_env from an activation
of the procedure which contains the declaration of the TAG
used by env_offset, then the result is an original
POINTER, notwithstanding the normal rules for
add_to_ptr (see Original pointers).
If an OFFSET produced by env_offset is added to
such a pointer from an inappropriate procedure the effect is undefined.
div_by_0_err: ERROR_TREATMENT ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)arg1 and arg2 are evaluated and will produce integer values, a and b, of the same
VARIETY,
v. Either the value a D1 b or the value a
D2 b is delivered as the result of the construct, with the
same
SHAPE as the arguments. Different occurrences of
div0 in the same capsule can use D1 or D2 independently.
If b is zero a div_by_zero error occurs and is handled by div_by_0_err.
If b is not zero and the result cannot be expressed in the
VARIETY being used to represent v an overflow
occurs and is handled by ov_err.
Producers may assume that shifting and div0 by a constant which is a power of two yield equally good code.
See Division and modulus for the definitions of D1, D2, M1 and M2.
div_by_0_err: ERROR_TREATMENT ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)arg1 and arg2 are evaluated and will produce integer values, a and b, of the same
VARIETY, v.
The value a D1 b is delivered as the result of the construct,
with the same SHAPE as the arguments.
If b is zero a div_by_zero error occurs and is handled by div_by_0_err.
If b is not zero and the result cannot be expressed in the
VARIETY being used to represent v an overflow
occurs and is handled by ov_err.
Producers may assume that shifting and div1 by a constant which is a power of two yield equally good code.
See Division and modulus for the definitions of D1, D2, M1 and M2.
div_by_0_err: ERROR_TREATMENT ov_err: ERROR_TREATMENT arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP INTEGER(v)arg1 and arg2 are evaluated and will produce integer values, a and b, of the same
VARIETY, v.
The value a D2 b is delivered as the result of the construct,
with the same SHAPE as the arguments.
If b is zero a div_by_zero error occurs and is handled by div_by_0_err.
If b is not zero and the result cannot be expressed in the
VARIETY being used to represent v an overflow
occurs and is handled by ov_err.
Producers may assume that shifting and div2 by a constant which is a power of two yield equally good code if the lower bound of v is zero.
See Division and modulus for the definitions of D1, D2, M1 and M2.
fa: ALIGNMENT y: ALIGNMENT t: TAG x -> EXP OFFSET(fa, y)t will be the tag of a variable, identify or procedure parameter with the visible property within a procedure defined by make_general_proc or make_proc.
If it is defined in a make_general_proc, let P be its associated
PROCPROPS; otherwise let P be the PROCPROPS
{locals_alignment, caller_alignment(false)}.
If t is the TAG of a variable or identify,
fa
will contain locals_alignment; if it is a caller parameter
fa will contain a caller_alignment(b) where b
is true if and only if P contains var_callers ; if it is
a callee parameter fa will contain a callee_alignment(b)
where b is true if and only if P contains var_callees.
If t is the TAG of a variable or parameter, the
result is the OFFSET of its position, within any procedure
environment which derives from the procedure containing the declaration
of the variable or parameter, relative to its environment pointer.
In this case
x will be POINTER(y).
If t is the TAG
of an identify, the result will be an OFFSET of
space which holds the value. This pointer will not be used to alter
the value. In this case y will be alignment(x).
See section 7.10.
proctag: TAG PROC
-> EXP OFFSET(locals_alignment, {})
Delivers an OFFSET of a space sufficient to contain all
the variables and identifications, explicit or implicit in the procedure
identified by proctag. This will not include the space required
for any local_allocs or procedure calls within the procedure.
proctag will be defined in the current CAPSULE
by a
TAGDEF identification of a make_proc or a
make_general_proc.
message: STRING(k, n) -> EXP BOTTOMAny attempt to use this operation to produce code will result in a failure of the installation process. message will give information about the reason for this failure which should be passed to the installation manager.
flpt_err: ERROR_TREATMENT f: FLOATING_VARIETY arg1: EXP INTEGER(v) -> EXP FLOATING(f)arg1 is evaluated to produce an integer value, which is converted to the representation of f and delivered.
If f is complex the real part of the result will be derived from arg1 and the imaginary part will be zero.
If there is a floating point error it is handled by flpt_err. See Floating point errors.
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) -> EXP FLOATING(f)arg1 is evaluated and will produce a floating point value, a, of the
FLOATING_VARIETY, f. The absolute
value of a is delivered as the result of the construct, with
the same SHAPE as the argument.
Though floating_abs cannot produce an overflow it can give an invalid operand exception which is handled by flpt_err.
f will not be complex.
See also Floating point accuracy.
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP FLOATING(f)arg1 and arg2 are evaluated and will produce floating point values, a and b, of the same
FLOATING_VARIETY, f. The value a/b
is delivered as the result of the construct, with the same
SHAPE as the arguments.
If there is a floating point error it is handled by flpt_err. See Floating point errors.
See also Floating point accuracy.
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP FLOATING(f)arg1 and arg2 are evaluated and will produce floating point values, a and b, of the same
FLOATING_VARIETY, f. The value a-b
is delivered as the result of the construct, with the same
SHAPE as the arguments.
If there is a floating point error it is handled by flpt_err. See Floating point errors.
See also Floating point accuracy.
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP FLOATING(f)The maximum of the values delivered by arg1 and arg2 is the result. f will not be complex.
If arg1 and arg2 are incomparable, flpt_err will be invoked.
See also Floating point accuracy.
flpt_err: ERROR_TREATMENT arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP FLOATING(f)The minimum of the values delivered by arg1 and arg2 is the result. f will not be complex.
If arg1 and arg2 are incomparable, flpt_err will be invoked.
See also Floating point accuracy.
flpt_err: ERROR_TREATMENT arg1: LIST(EXP) -> EXP FLOATING(f)The arguments, arg1, are evaluated producing floating point values all of the same
FLOATING_VARIETY, f. These
values are multiplied in any order and the result of this multiplication
is delivered as the result of the construct, with the same
SHAPE as the arguments.
If there is a floating point error it is handled by flpt_err. See Floating point errors.
Note that separate floating_mult operations cannot in general be combined, because rounding errors need to be controlled. The reason for allowing floating_mult to take a variable number of arguments is to make it possible to specify that a number of multiplications can be re-ordered.
If arg1 contains one element the result is the value of that element. There will be at least one element in arg1.
See also Floating point accuracy.
flpt_err: ERROR_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.
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.
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.
prob: OPTION(NAT) flpt_err: ERROR_TREATMENT nt: NTEST dest: LABEL arg1: EXP FLOATING(f) arg2: EXP FLOATING(f) -> EXP TOParg1 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.
dest: LABEL -> EXP BOTTOMControl passes to the
EXP labelled dest. This
construct will only be used where dest is in scope.
arg1: EXP POINTER({code})
-> EXP BOTTOM
arg1 is evaluated. The label from which the value delivered
by
arg1 was created will be within its lifetime and this construction
will be obeyed in the same activation of the same procedure as the
creation of the POINTER({code})
by make_local_lv. Control passes to this activation of this
LABEL.
If arg1 delivers a null POINTER the effect is
undefined.
opt_access: OPTION(ACCESS) name_intro: TAG x definition: EXP x body: EXP y -> EXP ydefinition 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.
arg1: EXP x -> EXP xIf the result of this construction is discarded, arg1 need not be evaluated, though evaluation is permitted. If the result is used it is the result of arg1.
arg1: EXP c -> EXP FLOATING (float_of_complex(c))c will be complex. Delivers the imaginary part of the value produced by arg1.
init: EXP s -> EXP sAny 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.
prob: OPTION(NAT) nt: NTEST dest: LABEL arg1: EXP INTEGER(v) arg2: EXP INTEGER(v) -> EXP TOParg1 and arg2 are evaluated and will produce integer values, a and b, of the same
VARIETY, v.
These values are compared using nt.
If a nt b, this construction yields TOP. Otherwise
control passes to dest.
If prob is present, prob/100 gives the probability that control will continue to the next construct (ie. not pass to dest). If prob is absent this probability is unknown.
labs_intro: LIST(LABEL) starter: EXP x places: LIST(EXP) -> EXP wThe 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.
x: EXP OFFSET(y, z) -> EXP POINTER(alloca_alignment)If the last use of local_alloc in the current activation of the current procedure was after the last use of local_free or local_free_all, then the value returned is the last
POINTER allocated with local_alloc.
If the last use of local_free in the current activation of
the current procedure was after the last use of local_alloc,
then the result is the POINTER last allocated which is
still active.
The result POINTER will have been created by
local_alloc with the value of its arg1 equal to the
value of x.
If the last use of local_free_all in the current activation of the current procedure was after the last use of local_alloc, or if there has been no use of local_alloc in the current activation of the current procedure, then the result is undefined.
The ALIGNMENT, alloca_alignment, includes the
set union of all the ALIGNMENTs which can be produced
by
alignment from any SHAPE. See
Special alignments.
arg1: EXP OFFSET(x, y) -> EXP POINTER(alloca_alignment)The arg1 expression is evaluated and space is allocated sufficient to hold a value of the given size. The result is an original pointer to this space.
x will not consist entirely of bitfield alignments.
The initial contents of the space are not specified.
This allocation is as if on the stack of the current procedure, and the lifetime of the pointer ends when the current activation of the current procedure ends with a return, return_to_label or tail_call or if there is a long jump out of the activation. Any use of the pointer thereafter is undefined. Note the specific exclusion of the procedure ending with untidy_return; in this case the calling procedure becomes the current activation.
The uses of local_alloc within the procedure are ordered dynamically as they occur, and this order affects the meaning of local_free and last_local.
arg1 may be a zero OFFSET. In this case suppose
the result is p. Then a subsequent use, in the same activation
of the procedure, of
local_free(offset_zero(alloca_alignment), p)
will return the alloca stack to the state it was in immediately before the use of local_alloc.
Note that if a procedure which uses local_alloc is inlined, it may be necessary to use local_free to get the correct semantics.
See also section 7.12.
arg1: EXP OFFSET(x, y) -> EXP POINTER(alloca_alignment)
If the OFFSET arg1 can be accomodated within the
limit of the local_alloc stack (see section 5.16.108),
the action is precisely the same as local_alloc.
If not, normal action is stopped and a TDF exception is raised with ERROR_CODE stack_overflow.
a: EXP OFFSET(x, y) p: EXP POINTER(alloca_alignment) -> EXP TOPThe
POINTER, p, will be an original pointer to
space allocated by local_alloc within the current call of the
current procedure. It and all spaces allocated after it by local_alloc
will no longer be used. This POINTER will have been created
by local_alloc with the value of its arg1 equal to the
value of a.
Any subsequent use of pointers to the spaces no longer used will be undefined.
-> EXP TOPEvery space allocated by local_alloc within the current call of the current procedure will no longer be used.
Any use of a pointer to space allocated before this operation within the current call of the current procedure is undefined.
Note that if a procedure which uses local_free_all is inlined, it may be necessary to use local_free to get the correct semantics.
arg1: EXP POINTER(fa)
arg2: EXP POINTER({code})
-> EXP BOTTOM
arg1 will be a pointer produced by an application of
curent_env in a currently active procedure.
The frame produced by arg1 is reinstated as the current procedure. This frame will still be active. Evaluation recommences at the label given by arg2. This operation will only be used during the lifetime of that label.
Only TAGs declared to have long_jump_access will
be defined at the re-entry.
If arg2 delivers a null
POINTER({code}) the effect is undefined.
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.
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).
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.
result_shape: SHAPE prcprops: OPTION(PROCPROPS) caller_intro: LIST(TAGSHACC) callee_intro: LIST(TAGSHACC) body: EXP BOTTOM -> EXP PROCEvaluation 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.
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.
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.
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.
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.
-> 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.
-> EXP PROCA 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.
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).
result_shape: SHAPE params_intro: LIST(TAGSHACC) var_intro: OPTION(TAGACC) body: EXP BOTTOM -> EXP PROCEvaluation 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.
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 is performed:
set_stack_limit(make_stack_limit(current_env, F, A))
the frame space and local_alloc space that would be available for
use by this supposed call of Q will not be reused by procedure calls
with check_stack or uses of local_alloc_check after
the set_stack_limit. Any attempt to do so will raise a TDF
exception, stack_overflow.
-> EXP TOPmake_top delivers a value of
SHAPE TOP
(i.e. void).
s: SHAPE -> EXP sThis
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.
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.
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.
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.
md: TRANSFER_MODE arg1: EXP POINTER(x) arg2: EXP POINTER(y) arg3: EXP OFFSET(z, t) -> EXP TOPThe 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.
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.
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.
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.
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.
t: TAG x -> EXP xThe 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.
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.
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.
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
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.
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).
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.
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.
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.
prob: OPTION(NAT) nt: NTEST dest: LABEL arg1: EXP OFFSET(x, y) arg2: EXP OFFSET(x, y) -> EXP TOParg1 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.
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).
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.
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.
prob: OPTION(NAT) nt: NTEST dest: LABEL arg1: EXP POINTER(x) arg2: EXP POINTER(x) -> EXP TOParg1 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.
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.
prob: OPTION(NAT) nt: NTEST dest: LABEL arg1: EXP PROC arg2: EXP PROC -> EXP TOParg1 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.
uses: NAT -> EXP TOPThe 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.
arg1: EXP c -> EXP FLOATING (float_of_complex(c))c will be complex. Delivers the real part of the value produced by arg1.
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.
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.
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 div_by_0_err.
If b is not zero and div2(a, b) cannot
be expressed in the VARIETY being used to represent v
an overflow may occur, in which case it is handled by ov_err.
Producers may assume that suitable masking and rem2 by a power of two yield equally good code if the lower bound of v is zero.
See Division and modulus for the definitions of D1, D2, M1 and M2.
replab_intro: LABEL start: EXP TOP body: EXP y -> EXP ystart 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.
arg1: EXP x -> EXP BOTTOMarg1 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.
lab_val: EXP POINTER code_alignment -> EXP BOTTOMlab_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.
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.
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.
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.
statements: LIST(EXP) result: EXP x -> EXP xThe 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.
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.
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.
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.
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.
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.
prcprops: OPTION(PROCPROPS) p: EXP PROC callee_pars: CALLEES -> EXP BOTTOMp 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.
No pointers to any callee parameters, variables, identifications or local allocations defined in immediately enclosing procedure will be accessed either in the body of p or after the return.
The presence or absence of each of the PROCPROPS
check_stack and untidy, in prcprops will be reflected
in the PROCPROPS of the immediately enclosing procedure.
arg1: EXP x -> EXP BOTTOMarg1 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.
opt_access: OPTION(ACCESS) name_intro: TAG POINTER(alignment(x)) init: EXP x body: EXP y -> EXP yinit 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.
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.
An EXTERNAL defines the classes of external name available
for connecting the internal names inside a CAPSULE to
the world outside the CAPSULE.
s: BYTE_ALIGN TDFIDENT(n) -> EXTERNALstring_extern produces an
EXTERNAL identified
by the TDFIDENT s.
u: BYTE_ALIGN UNIQUE -> EXTERNALunique_extern produces an
EXTERNAL identified
by the UNIQUE u.
s: BYTE_ALIGN TDFIDENT prev: TDFINT -> EXTERNALThis construct is redundant and should not be used.
An auxiliary SORT providing a list of LINKEXTERN.
el: SLIST(LINKEXTERN) -> EXTERN_LINKmake_capsule requires a
SLIST(EXTERN_LINK)
to express the links between the linkable entities and the named (by
EXTERNALs) values outside the CAPSULE.
These describe kinds of floating point number.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> FLOATING_VARIETYThe 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.
control: EXP INTEGER(v) e1: BITSTREAM FLOATING_VARIETY e2: BITSTREAM FLOATING_VARIETY -> FLOATING_VARIETYThe 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.
base: NAT mantissa_digs: NAT min_exponent: NAT max_exponent: NAT -> FLOATING_VARIETYbase 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.
base: NAT mantissa_digs: NAT min_exponent: NAT max_exponent: NAT -> FLOATING_VARIETYA
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.
csh: SHAPE -> FLOATING_VARIETYcsh will be a complex
SHAPE.
Delivers the FLOATING_VARIETY required for the real (or
imaginary) part of a complex SHAPE csh.
fsh: SHAPE -> FLOATING_VARIETYfsh will be a floating
SHAPE.
Delivers FLOATING_VARIETY required for a complex number
whose real (and imaginary) parts have SHAPE fsh.
A GROUP is a list of UNITs with the same
unit identification.
us: SLIST(UNIT) -> GROUPmake_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.
A LABEL marks an EXP in certain constructions,
and is used in jump-like constructions to change the control to the
labelled construction.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> LABEL xThe 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.
labelno: TDFINT -> LABELLabels 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.
A LINK expresses the connection between two variables
of the same SORT.
unit_name: TDFINT capsule_name: TDFINT -> LINKA
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.
A value of SORT LINKEXTERN expresses the connection between
the name by which an object is known inside a CAPSULE
and a name by which it is known outside.
internal: TDFINT ext: EXTERNAL -> LINKEXTERNmake_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.
ls: SLIST(LINK) -> LINKSmake_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.
These are non-negative integers of unlimited size.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> NATThe 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.
control: EXP INTEGER(v) e1: BITSTREAM NAT e2: BITSTREAM NAT -> NATThe 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.
arg: EXP INTEGER(v) -> NATarg will be an install-time non-negative constant. The result is that constant.
err: ERROR_CODE -> NATGives the
NAT corresponding to the ERROR_CODE
err. Each distinct ERROR_CODE will give a different
NAT.
n: TDFINT -> NATn is a non-negative integer of unbounded magnitude.
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).
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> NTESTThe 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.
control: EXP INTEGER(v) e1: BITSTREAM NTEST e2: BITSTREAM NTEST -> NTESTThe 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.
-> NTESTSignifies "equal" test.
-> NTESTSignifies "greater than" test.
-> NTESTSignifies "greater than or equal" test.
-> NTESTSignifies "less than" test.
-> NTESTSignifies "less than or equal" test.
-> NTESTSignifies "not equal" test.
-> NTESTSignifies "not greater than" test.
-> NTESTSignifies "not (greater than or equal)" test.
-> NTESTSignifies "not less than" test.
-> NTESTSignifies "not (less than or equal)" test.
-> NTESTSignifies "less than or greater than" test.
-> NTESTSignifies "not less than and not greater than" test.
-> NTESTSignifies "comparable" test.
With all operands SHAPEs except FLOATING,
this comparison is always true.
-> NTESTSignifies "not comparable" test.
With all operands SHAPEs except FLOATING,
this comparison is always false.
This is a auxilliary SORT used in apply_general_proc.
tgopt: OPTION(TAG x) e: EXP x -> OTAGEXPe 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.
PROCPROPS is a set of properties ascribed to procedure
definitions and calls.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> PROCPROPSThe 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.
control: EXP INTEGER(v) e1: BITSTREAM PROCPROPS e2: BITSTREAM PROCPROPS -> PROCPROPSThe 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.
arg1: PROCPROPS arg2: PROCPROPS -> PROCPROPSDelivers the join of arg1 and arg2.
-> PROCPROPSThe procedure body is required to check for stack overflow.
-> PROCPROPSThe procedure body is a good candidate for inlining at its application.
-> PROCPROPSThe procedure body will contain no label which is the destination of a long_jump.
-> PROCPROPSThe procedure body may be exited using an untidy_return.
-> PROCPROPSApplications of the procedure may have different numbers of actual callee parameters.
-> PROCPROPSApplications of the procedure may have different numbers of actual caller parameters.
PROPS is an assemblage of program information. This
standard offers various ways of constructing a PROPS
- i.e. it defines kinds of information which it is useful to express.
These are:
AL_TAGs standing for ALIGNMENTs;
TAGs standing for EXPs;
EXPs for which TAGs
stand;
TOKENs standing for pieces of TDF
program;
TOKENs
stand;
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.
ROUNDING_MODE specifies the way rounding is to be performed
in floating point arithmetic.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> ROUNDING_MODEThe 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.
control: EXP INTEGER(v) e1: BITSTREAM ROUNDING_MODE e2: BITSTREAM ROUNDING_MODE -> ROUNDING_MODEThe 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.
-> ROUNDING_MODERound as specified by the current state of the machine.
-> ROUNDING_MODESignifies rounding to nearest. The effect when the number lies half-way is not specified.
-> ROUNDING_MODESignifies rounding toward next largest.
-> ROUNDING_MODESignifies rounding toward next smallest.
-> ROUNDING_MODESignifies rounding toward zero.
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.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> SHAPEThe 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.
control: EXP INTEGER(v) e1: BITSTREAM SHAPE e2: BITSTREAM SHAPE -> SHAPEThe 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.
bf_var: BITFIELD_VARIETY -> SHAPEA
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.
-> 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.
sz: EXP OFFSET(x, y) -> SHAPEThe
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.
fv: FLOATING_VARIETY -> SHAPEMost 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.
var: VARIETY -> SHAPEThe 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.
n: NAT s: SHAPE -> SHAPEThe
NOF constructor describes the SHAPE
of a value consisting of an array of n values of the same
SHAPE, s.
arg1: ALIGNMENT arg2: ALIGNMENT -> SHAPEThe
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.
arg: ALIGNMENT -> SHAPEA
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.
-> SHAPE
PROC is the SHAPE which describes pieces
of program.
-> SHAPE
TOP is the SHAPE which describes pieces
of program which return no useful value. assign is an example:
it performs an assignment, but does not deliver any useful value.
These are positive or negative integers of unbounded size.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> SIGNED_NATThe 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.
control: EXP INTEGER(v) e1: BITSTREAM SIGNED_NAT e2: BITSTREAM SIGNED_NAT -> SIGNED_NATThe 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.
arg: EXP INTEGER(v) -> SIGNED_NATarg will be an install-time constant. The result is that constant.
neg: TDFBOOL n: TDFINT -> SIGNED_NATn is a non-negative integer of unbounded magnitude. The result is negative if and only if neg is true.
neg: BOOL n: NAT -> SIGNED_NATThe result is negated if and only if neg is true.
These are the names of the SORTs which can be parameters
of TOKEN definitions.
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAMEThe
SORT of EXP.
-> SORTNAME
foreign_name: STRING(k, n) -> SORTNAMEThis
SORT enables unanticipated kinds of information
to be placed in TDF.
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAME
-> SORTNAMEThe
SORT of TAG.
-> SORTNAME
result: SORTNAME params: LIST(SORTNAME) -> SORTNAMEThe
SORTNAME of a TOKEN. Note that it can
have tokens as parameters, but not as result.
-> SORTNAME
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.
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.
arg1: STRING(k, n) arg2: STRING(k, m) -> STRING(k, n+m)Gives a
STRING which is the concatenation of arg1
with arg2.
arg: TDFSTRING(k, n) -> STRING(k, n)Delivers the
STRING identical to the arg.
These are used to name values and variables in the run time program.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> TAG xThe 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.
tagno: TDFINT -> TAG xmake_tag produces a
TAG identified by tagno.
Constructs a pair of a TAG and an OPTION(ACCESS)
for use in make_proc.
tg: TAG POINTER var_param_alignment acc: OPTION(ACCESS) -> TAGACCConstructs the pair for make_proc.
A TAGDEC declares a TAG for incorporation
into a TAGDEC_PROPS.
t_intro: TDFINT acc: OPTION(ACCESS) signature: OPTION(STRING) x: SHAPE -> TAGDECA
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.
t_intro: TDFINT acc: OPTION(ACCESS) signature: OPTION(STRING) x: SHAPE -> TAGDECA
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.
t_intro: TDFINT acc: OPTION(ACCESS) signature: OPTION(STRING) x: SHAPE -> TAGDECA
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:
COMPOUND(x) and
COMPOUND(y) respectively and a is an initial
segment of b, then b is the maximum. Similarly if b
is an initial segment of a then a is the maximum.
NOF(n, x)
and NOF(m, x) respectively and n
is less than or equal to m, then b is the maximum. Similarly
if m is less than or equal to n then a is the
maximum.
no_labels: TDFINT tds: SLIST(TAGDEC) -> TAGDEC_PROPSno_labels is the number of local
LABELs used in
tds. tds is a list of TAGDECs which declare
the SHAPEs associated with TAGs.
A value of SORT TAGDEF gives the definition of a TAG
for incorporation into a TAGDEF_PROPS.
t: TDFINT signature: OPTION(STRING) e: EXP x -> TAGDEFmake_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.
t: TDFINT opt_access: OPTION(ACCESS) signature: OPTION(STRING) e: EXP x -> TAGDEFmake_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.
t: TDFINT opt_access: OPTION(ACCESS) signature: OPTION(STRING) e: EXP x -> TAGDEFcommon_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:
SHAPE COMPOUND(x)
and COMPOUND(y) respectively and the value produced
by a is an initial segment of the value produced by b,
then b is the maximum. Similarly if b is an initial
segment of a then a is the maximum.
SHAPE NOF(n,
x) and NOF(m, x) respectively and
the value produced by a is an initial segment of the value
produced by
b, then b is the maximum. Similarly if b is an
initial segment of a then a is the maximum.
no_labels: TDFINT tds: SLIST(TAGDEF) -> TAGDEF_PROPSno_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.
sha: SHAPE opt_access: OPTION(ACCESS) tg_intro: TAG -> TAGSHACCThis is an auxiliary construction to make the elements of params_intro in make_proc.
TDFBOOL is the TDF encoding of a boolean. See
Fundamental encoding.
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.
TDFINT is the TDF encoding of an unbounded unsigned
integer constant. See Fundamental encoding.
TDFSTRING(k, n) encodes a sequence of
n unsigned integers of size k bits. See Fundamental
encoding.
A TOKDEC declares a TOKEN for incorporation
into a UNIT.
tok: TDFINT signature: OPTION(STRING) s: SORTNAME -> TOKDECThe 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.
tds: SLIST(TOKDEC) -> TOKDEC_PROPStds is a list of
TOKDECs which gives the sorts
associated with TOKENs.
A TOKDEF gives the definition of a TOKEN
for incorporation into a TOKDEF_PROPS.
tok: TDFINT signature: OPTION(STRING) def: BITSTREAM TOKEN_DEFN -> TOKDEFA
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.
no_labels: TDFINT tds: SLIST(TOKDEF) -> TOKDEF_PROPSno_labels is the number of local
LABELs used in
tds. tds is a list of TOKDEFs which gives
the definitions associated with TOKENs.
These are used to stand for functions evaluated at installation time.
They are represented by TDFINTs.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> TOKENThe 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.
tokno: TDFINT -> TOKENmake_tok constructs a
TOKEN identified by tokno.
tdef: BITSTREAM TOKEN_DEFN -> TOKENtdef is used to supply the definition, as in make_tokdef. Note that
TOKENs are only used in x_apply_token
constructions.
An auxiliary SORT used in make_tokdef and
use_tokdef.
result_sort: SORTNAME tok_params: LIST(TOKFORMALS) body: result_sort -> TOKEN_DEFNMakes 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.
sn: SORTNAME tk: TDFINT -> TOKFORMALSAn auxiliary construction to make up the elements of the lists in token_definition.
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.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> TRANSFER_MODEThe 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.
control: EXP INTEGER(v) e1: BITSTREAM TRANSFER_MODE e2: BITSTREAM TRANSFER_MODE -> TRANSFER_MODEcontrol 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.
md1: TRANSFER_MODE md2: TRANSFER_MODE -> TRANSFER_MODEA 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.
-> TRANSFER_MODEIf 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.
-> TRANSFER_MODEThis
TRANSFER_MODE implies no special properties.
-> TRANSFER_MODEIf 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.
-> TRANSFER_MODEIf 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.
-> TRANSFER_MODEA transfer qualified with complete shall leave the destination unchanged if the evaluation of the value transferred is left with a jump.
These are used to provide world-wide unique names for TOKENs
and TAGs.
This implies a registry for allocating UNIQUE values.
text: SLIST(TDFIDENT) -> UNIQUETwo
UNIQUE values are equal if and only if they were
constructed with equal arguments.
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.
local_vars: SLIST(TDFINT) lks: SLIST(LINKS) properties: BYTESTREAM PROPS -> UNITlocal_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.
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.
token_value: TOKEN token_args: BITSTREAM param_sorts(token_value) -> VARIETYThe 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.
control: EXP INTEGER(v) e1: BITSTREAM VARIETY e2: BITSTREAM VARIETY -> VARIETYThe 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.
lower_bound: SIGNED_NAT upper_bound: SIGNED_NAT -> VARIETYlower_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).
signed_width: BOOL width: NAT -> VARIETYIf 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).
This UNIT gives information about version numbers and
user information.
version_info: SLIST(VERSION) -> VERSION_PROPSContains version information.
major_version: TDFINT minor_version: TDFINT -> VERSIONThe 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.
information: STRING(k, n) -> VERSIONThis is (usually character) information included in the TDF for labelling purposes.
information will be produced by make_string.
Part of the TenDRA Web.
Crown
Copyright © 1998.