====== The Implementation relation ======

When types are created using either ''deftype'' or ''defchan'',
they are defined as the implementation of a type. This is also
possible for processes defined using ''defproc''.

==== Implementation ====

The implementation relation is used to specify the precise
implementation of a data or channel type. The most straightforward
mechanism to specify a channel is to say that it is the implementation
of a built-in data type. In the example in the [[language:types2|previous section]], the channel
''e1of2'' is defined to be an implementation of a
''chan(bool)''. The implementation has additional port parameters,
and it specifies the communication protocols for a send and receive
action. The syntax that is used to say that we have an implementation
is the ''<:'' symbol between the name of the type and the parent type
that it is related to.

When a type implements another one, the new type can be used in places
the old type was used. While this is superficially similar to
subtyping in programming languages, it is better viewed as an
implementation relationship. So, if type ''tA'' implements type
''tB'', then ''tA'' has a more detailed description of the
implementation compared to ''tB''. Type ''tB'' is the
//parent type// for type ''tA''. As seen earlier, each data type
or channel type can have a method body that specifies all the
operations that can be performed using the type. These method bodies
relate operations on the type to operations on the parent type
(through ''self'').


Different implementations of the same type are not equivalent or
interchangeable. For example, one can imagine two different
implementations of an ''int<2>'': two dual-rail codes, or a
one-of-four code. Both are implementations, but they are not
equivalent to each other.

A more interesting option is to use the implementation relationship
between two user-defined types. This option is used to create related versions of
an existing type. If type ''foo'' implements ''bar'', then the
basic rule is that one can use ''foo'' instances in all the same
contexts where ''bar'' instances can be used. The meaning of
defining one type to be an implementation of another is discussed in
detail below.

==== Aspects of the implementation relation ====

When a user defined type implements another, there are several items
to consider: (i) the template parameters (if any); (ii) the port
parameters; and the body of the new type. Since the new type is
supposed to implement the old one, ACT defines the template
parameters and port parameters for the new type using the old type as
a starting point.

The port list of the new type consists of the original port list in
the base type plus the additional ports specified in the type
definition---in other words, the new type //extends// the original
port list. As an illustration, consider:

<code act>
defproc type1 (bool a, b) { ... }
defproc type2 <: type1 (bool c) { ... }
</code>

In this case ''type2'' would have ports ''a'', ''b'', and
''c'', since it is an implementation of ''type1''.

Template parameters are handled in a similar fashion, except there is
a complication. In the example below, ''type2'' would have two
template parameters ''N'' and ''M'', as might be expected from
the port list example above.

<code act>
template<pint N>
defproc type1 (bool a, b) { ... }

template<pint M>
defproc type2 <: type1 (bool c) { ... }
</code>

However, we can also define ''type2'' in the following manner:

<code act>
template<pint N>
defproc type1 (bool a, b) { ... }

template<pint M>
defproc type2 <: type1<4> (bool c) { ... }
</code>

In this version, the template parameter from ''type1'' has been
specified in the type definition for ''type2''. To permit this
feature, template parameters for the new type are defined in the
following manner:
   * Template parameters are categorized as //definable parameters// versus //pre-specified parameters//. Fresh template parameters are always definable.
   * Pre-specified parameters are not part of the parameter set that can be specified when a type is created.
   * The value of the pre-specified parameter is computed based on the type signature.
   * The list of parameters accessible in the body of the type and outside the type is the combination of the ones defined by the new type and the parent type.
   * The order of template parameters in the new type corresponds to the new parameters first (in the order specified), followed by any definable parameters left in the parent type.
   
So in the example above, we could create an instance of ''type2''
as follows:

<code act>
type2<5> x;
// x.N, x.M are both accessible!
</code>

The parameter ''N'' for ''x'' will be ''4'', since that has
been pre-specified in the type definition for ''type2''. If instead
we had specified ''type2 <: type1'' as in the earlier example, then
the instance

<code act>
type2<5,7> x;
// x.M=5, x.N=7
</code>

would set ''M'' (the new template parameter) to ''5'', and
''N'' (the parent, still definable parameter) to ''7''. Finally,
the following would be an error:

<code act>
template<pint N> defproc type1 (bool a, b) { ... }
template<pint N> defproc type2 <: type1 (bool c) { ... }
</code>
<code>
-[ERROR]-> Duplicate meta-parameter name in port list: `N'
           Conflict occurs due to parent type: type1
</code>
since the name of the template parameter is repeated.

The body of the new type is the union of the original type definition
and the new body. As an example to illustrate how this might be used,
consider the following example: 

<code act>
defproc buffer (e1of2? l, e1of2! r)
{
   bool x;

   chp {
     *[ l?x;r!x ]
   }
}
</code>

''buffer'' specifies the CHP description for a one-place FIFO. This
can be implemented using a variety of circuits, and hence we could
define a specific implementation as follows:

<code act>
defproc wchb <: buffer ()
{
   prs {
     ...
   }
}
</code>

The process ''wchb'' is a specific implementation of the buffer
(without any extra ports) that contains a particular production-rule
implementation of the same buffer.

==== Overrides ====

Consider the buffer example above. A better and more abstract
specification for a buffer at the CHP level of abstraction would be:

<code act>
defproc buffer (chan?(bool) l, chan!(bool) r)
{
   bool x;

   chp {
     *[ l?x;r!x ]
   }
}
</code>

The production rules for this buffer use the fact that the Boolean
channel for ''l'' and ''r'' is in fact an ''e1of2''
channel. Because an ''e1of2'' channel implements a
''chan(bool)'', ACT provides a mechanism to say that an
implementation of a process also replaces existing types with new
implementations of the same type. This mechanism is called an
//override//, because old types can be //overridden// with new
ones that implement them.

Variables in the port list as well as the body of a type can be
overridden. For this to be sound, the new type must be an
implementation of the original. The syntax for this is shown below:

<code act>
defproc wchb <: buffer()
+{ e1of2 l, r; } // override block
{
   prs {
     ...
   }
}
</code>

In this version, the original process implements a buffer with
channels, and the ''wchb'' specifies that the channel is a
''e1of2''.  The first abstract buffer can be used with different
handshake protocols on channels, or with different circuits.

The ''+{ ... }'' indicates the override block. The override
block uses the instantiation syntax to specify override types. The
only syntax permited is of the form within an override block is

<code act>
+{
    type list-of-ids;
    ...
 }
</code>

The identifiers cannot contain array specifiers, and the types 
cannot have any direction flags. Furthermore, the types must also
be user-defined types. The identifier names must match names in the
parent type (either in the port list or in the body of the type). If
the original identifier was declared as an array, the entire array
will be overridden. Direction flags from the parent type will be
inherited by the overridden type.

Implementation relations introduced should be handled with care. For
example, suppose one has two definitions of a buffer: one using the
CHP language, and the other using the PRS language (as above), and
consider the variable ''x''. Now this internal variable which is in
the CHP language may not be part of the PRS for the WCHB
reshuffling. In other words, the ''wchb'' process will not have any
internal variable that corresponds to ''x'' in the CHP language!
Similarly, the ''wchb'' PRS language will contain additional
variables that are not present in the CHP language. The relation
between such variables is unspecified by the implementation
relationship.

An additional complication arises if the process ''wchb'' ends up
introducing a state variable ''x'' in the PRS language that does
correspond to the ''bool x'' in the CHP language. In this case, one
should override ''x'' as well with the appropriate detailed
representation of the Boolean variable.

=== Overriding conditional instances and templated types ===

An instance created in a type definition may be created only under certain circumstances. 
This can occur in templated types, where template parameters can affect the instances within the type.
The override block has the simple syntax shown above. However, to account for conditional instances,
the override block directives implicitly check if the instance exists before applying the override. (Note that
ACT does not permit different types for the same instance name under different conditions.)

When a type is being overridden by another, the new implementation may have additional template parameters.
The override syntax above requires the complete list of template parameters to be specified. Instead, we also
provide a single extension override syntax

<code act>
+{
    type<param1,param2,...,paramN>+ id;   // single ID only
    ...
 }
</code>
The ''+'' indicates that these are //extra// template parameter(s) that should be added to the existing ones that have already been specified for the instance ''id'' in the original type definition.