Differences

This shows you the differences between two versions of the page.

--- language:types [2019/04/18 15:58] – [Refinement] rajit
+++ language:types [2025/04/21 14:32] (current) – [Parameterized types] rajit
@@ Line 23: / Line 23: @@
    * Parameter types
-      * ''pint'', for unsigned integer parameters.
+      * ''pint'', for integer parameters.
-      * ''pints'', for signed integer parameters.
       * ''preal'', for real-valued parameters.
       * ''pbool'', for Boolean-valued parameters.
@@ Line 51: / Line 50: @@
 name followed by a comma-separated list of identifier names.
-<code>
+<code act>
 bool a,b,c,n1,n1x2;
 pint x,y,z;
@@ Line 61: / Line 60: @@
 to have more than one instantiation of a variable in the same scope.
-<code>
+<code act>
 bool a;
 pint a;
+</code>
+<code>
 -[ERROR]-> Duplicate instance for name `a'
 </code>
@@ Line 69: / Line 70: @@
 A parameter instantiation can be accompanied by a single //initializer//
 which initializes the value of a variable.
-<code>
+<code act>
 pint a=5, c=8;
 preal b=8.9;
@@ Line 77: / Line 78: @@
 Using constructs such as
+<code act>
+pint a=c, c=5;
+</code>
 <code>
-pint a=c, c=5;
 -[ERROR]-> The identifier `c' does not exist in the current scope
 </code>
@@ Line 93: / Line 96: @@
 examples of creating arrays are shown below:
-<code>
+<code act>
 int ar1[4]
 preal ar2[7]
@@ Line 108: / Line 111: @@
 specifications, as shown below.
-<code>
+<code act>
 int ar4[5*3]
 preal ar5[7*x+(y%2)-p] // here x, y, and p must be integer parameter types
@@ Line 116: / Line 119: @@
 type. Variables used must always be parameter types (typically ''pint'').
-<code>
+<code act>
 preal a = 4.3;
 bool ar6[7*a+5];
+</code>
+<code>
 -[ERROR]-> Expression must be of type int
 </code>
@@ Line 126: / Line 131: @@
 the example below.
-<code>
+<code act>
 bool x[5,3];
 bool y[1..6][9][2..10];
@@ Line 137: / Line 142: @@
 aforementioned array is shown below.
-<code>
+<code act>
 bool n[4..4], n[6..6];
 </code>
@@ Line 145: / Line 150: @@
 dynamically extended in ACT.
-<code>
+<code act>
 bool n[5];
 bool n[10..12]; // n is now defined at positions 0 to 4, 10 to 12
@@ Line 153: / Line 158: @@
 ''m'' at positions ''[6][5]'', ''[6][6]'', ..., ''[6][10]''.
-<code>
+<code act>
 bool m[6..6][5..10]
 </code>
@@ Line 159: / Line 164: @@
 Note that this is quite different from the statement
-<code>
+<code act>
 bool m[6][5..10];
 </code>
@@ Line 169: / Line 174: @@
 initializers.
-<code>
+<code act>
 bool x[10];
 bool y[10] = x;
+</code>
+<code>
 -[ERROR]-> Connection can only be specified for non-array instances
 </code>
@@ Line 179: / Line 186: @@
 shape of the array in each dimension.
-===== User-defined types =====
-User-defined type can be used to create complex circuit structures.  A
-new user-defined type name is introduced by using ''defproc'',
-''defcell'', ''defchan'', or ''deftype''
-statements. All user-defined types have the same basic structure:
-   - a type signature, that provides information about the interface to the type and the ports that are externally visible; and
-   - a //body//, contained in braces, that specifies the detailed definition of the user-defined type.
-The type chosen for each port must be the most specific type used by
-that port in the body (see the implementation relation section).
-User-defined types can also be parameterized, and this is covered in
-detail later.
-==== Processes and cells ====
-A process is a user-defined type that corresponds to a circuit
-entity. Other hardware description languages sometimes call it a module
-or a subcircuit. The basic syntax of a process definition is shown below.
-<code>
-defproc test (bool n, m; bool p, q)
-{
- ...
-}
-</code>
-The definition above creates a new process, called ''test'', that has
-a port list consisting of four ''bool''s. This port list cannot
-contain any parameter types (''pint'', etc).
-If the body of the user-defined type is replaced by a single
-semi-colon or is empty, the statement corresponds to a type
-//declaration//. Declarations are typically used when defining
-mutually recursive types. The declaration corresponding to type
-''test'' is:
-<code>
-defproc test (bool n, m; bool p, q);
-</code>
-If the process is never defined, ACT assumes that it has an empty
-body. If a process declaration is followed by a definition, the type
-signature must match exactly.
-<code>
-defproc test (bool n, m; bool p, q);
-defproc test (bool n, m; bool p) { }
--[ERROR]-> Name `test' previously defined as a different process
-</code>
-A type can only have one definition in a given scope.
-<code>
-defproc test (bool n) { ... }
-defproc test (bool n) { ... }
--[ERROR]-> Process `test': duplicate definition with the same type signature
-</code>
-The body of a process specifies its implementation. This can use a
-combination of instances of other processes, connections, and other
-languages like production rules. Loops and conditional statements can
-also be used to construct a process.
-Port lists have a syntax similar to instantiations. A type
-specifier can be followed by a list of identifiers rather than just a
-single identifier, similar to an instantiation. Semicolons are used
-to separate parameters of differing types, as shown in the example
-below.
-<code>
-defproc test2(bool n,m; d1of2 p,q) { ... }
-</code>
-In this example we assumed that there was a user-defined type (or
-channel) called ''d1of2'' that was used in the port list. Any
-user-defined type in the port list must be either a data or channel
-type. Processes are supposed to correspond to circuit blocks, and so
-cannot be port parameters to other circuit blocks.
-Square brackets can also be used following the identifier names to
-specify array ports. The meaning of these square brackets is identical
-to the ordinary array instantiation. However, the arrays in port lists
-are restricted to be dense arrays indexed at zero. This restriction is
-enforced by syntax, and will be reported as a parse error.
-<code>
-defproc test1 (bool a,b,c, d[10]) { }  // success!
-defproc test2 (bool a,b,c, d[0..9]) { }
--[ERROR]-> Expecting token `]', got `.'
-</code>
-The ports themselves cannot be converted to sparse arrays within the
-body of a definition. This means that the following is illegal:
-<code>
-defproc test1 (bool a, b, c, d[10])
-{
-  bool d[11..12];
-  ...
-}
--[ERROR]-> Array instance for `d': cannot extend a port array
-</code>
-Type names and variable names do not share the same name space.
-Creating a type definition with the same name as an instance variable
-or vice versa is allowed, but deprecated.
-Cells follow the same rules for definition as processes, except the
-keyword ''defcell'' is used in place of ''defproc''. The reason
-for separating cells from processes is that processes are supposed to
-correspond to logical entities that are meaningful semantic
-objects. For example, a process ordinarily has its origins in a CHP
-language description. Cells, on the other hand,
-can be fragments of logical processes. Examples of cells are standard
-gates like C-elements, NAND, or NOR gates, or commonly used circuit
-structures like completion detection logic. Cells are distinguished
-from processes to make it easier to write automation tools.
-==== Data types ====
-A data type is defined using ''deftype''. A data type corresponds
-to an integer or Boolean value, although it could also be a composite
-construct like a record or structure (from software programming
-languages). The syntax is similar to a process, and the constraints
-about declarations/etc. apply here as well.
-Data types have some additional structure that is not required for a
-process. In particular, the body of the data type and its type
-signature provide information that relates a user-defined data type to
-a previously defined or built-in data type. When a user-defined data
-type is specified, a method for setting the value of the data type and
-reading its value must also be specified. If omitted, certain features
-of data types will not be enabled for the defined type.
-The following is a simple example of a datatype that creates a dual-rail
-representation for a Boolean variable. The first line specifies that
-''d1of2'' is a new data type, and it implements the built-in type
-''int<1>''---a one-bit integer.
-<code>
-deftype d1of2 <: int<1> (bool d0,d1)
-{
-  spec {
-    exclhi(d0,d1)
-  }
-}
-</code>
-The body of the type is similar to a process, except it can only contain
-connections, ''spec'' bodies, and special //methods//. The
-following would result in an error:
-<code>
-deftype d1of2 <: int<1> (bool d0,d1)
-{
-  bool p;
-  spec {
-    exclhi(d0,d1)
-  }
-}
--[ERROR]-> Expecting bnf-item `methods_body', got `bool'
-</code>
-There are two methods that can be specified for a data type:
-   - a //set method//, used to write a value to the type;
-   - a //get method//, used to read the value of the type.
-One can think of these as type conversion methods invoked
-automatically to read or write the data type.
-<code>
-deftype d1of2 <: int<1> (bool d0,d1)
-{
-   spec {
-    exclhi(d0,d1)
-   }
-   methods {
-     set {
-       [self=1->d1-;d0+ [] self=0->d0-;d1+]
-     }
-     get {
-       [d0->self:=1 [] d1->self:=0]
-     }
-   }
-}
-</code>
-In the example above, the ''set'' method says that the way to set a
-''d1of2'' data type to the value ''0'' is to set ''d0'' to
-''false'' and ''d1'' to ''true''. The special variable
-''self'' is used to specify the ''int<1>'' value of the type, and
-the methods specify conversion operations.
-The selection statement in the ''get'' method uses the deterministic
-selection operator ''[]'' (see languages). This is an implicit check
-that when the ''get'' method is invoked, signals ''d0'' and ''d1''
-cannot both be ''true''. We have also made this explicit in the
-specification body. Also, if both ''d0'' and ''d1'' are false
-(i.e. an illegal state in which to execute a get operation), the
-variable ''self'' is not assigned; the operation waits for at least
-one of ''d0'' or ''d1'' to be true. This is viewed as an error for a
-data type. (This is different in the case of a channel, where the
-semantics of the channel permit waiting.)
-Port lists for data types can be either built-in data types or
-user-defined data types. Channels (built-in or user-defined) and
-processes are not valid types for ports of a data type, since a data
-type is supposed to represent a circuit structure that is used to
-represent a data value.
-==== Channels ====
-Channels are similar to data types. Instead of relating a user-defined
-channel to built-in data, we relate them to a built-in channel types
-instead. The methods required for supporting the full functionality of
-a channel are operations necessary to send and receive data on the
-channel, rather than a read and write operation on a data value.
-There are six possible methods that can be defined for a channel type:
-   * Methods for sending and receiving values on the channel
-      * ''set'', ''send_rest'': together these two operations implement a send operation on the channel. The send operation consists of two parts: (i) setting the data value to be sent (''set''); and (ii) completing the synchronization operation (''send_rest'').
-      * ''get'', ''recv_rest'': together these two operations implement a receive operation on the channel. The receive operation consists of two parts: (i) getting the value that has been transmitted along the channel (''get''); and (ii) completing the synchronization operation.
-   * Methods for probing a channel to determine if there is synchronization operation being attempted.
-      * ''send_probe'': this is the probe operation for the sending end of the channel. It corresponds to the receiver being ready to communicate.
-      * ''recv_probe'': this is the probe operation for the receiving end of the channel. It corresponds to the sending being ready to communicate.
-The send operation ''X!e'' in the CHP language corresponds to two
-parts: setting the data value, followed by the synchronization
-operation. Setting the data value also indicates that the sender is
-ready to communicate. It is illegal to set the data value multiple
-times without an intervening synchronization operation. Finally,
-attempting to set the data value might block if the previous channel
-operation has not completed as yet. Whether or not this could occur
-depends on the channel protocol.
-The receive operation ''X?v'' in the CHP language corresponds to
-two parts: receiving the data value, followed by the synchronization
-operation. Attempting to get the data value from the channel will
-block if the sender has not provided any value. Once a value has been
-extracted from the channel, the synchronization operation can be
-executed. Prior to the synchronization, multiple get operations can be
-executed; the channel must be designed so that subsequent get
-operations will return the same value as the first one, and will be
-guaranteed not to block. The get operation is used to implement a CHP
-value probe, where the receiver can peek at the value pending in the
-channel without attempting a synchronization operation.
-An example definition of a Boolean channel where the channel has an
-lazy-active send and passive receive is below.
-<code>
-defchan e1of2 <: chan(bool) (bool d0,d1,e)
-{
-   spec {
-    exclhi(d0,d1)
-   }
-   methods {
-    set {
-      [e];[self->d1+[]~self->d0+]
-    }
-    send_rest {
-      [~e];d0-,d1-
-    }
-    get {
-     [d0->self-[]d1->self+]
-    }
-    recv_rest {
-     e-;[~d0&~d1];e+
-    }
-    recv_probe = (d0|d1);
-   }
-}
-</code>
-In the example above, the ''set'' and ''send_rest'' methods
-specify the sequence of operations on the channel variables that are
-invoked for a send action. The ''get'' and ''recv_rest'' methods
-specify the sequence of operations used to perform a receive. The
-special variable ''self'' is used to specify the ''bool'' value
-that is being either sent or received on the channel.
-This channel has an active send and passive receive, and hence probes
-are only supported at the receiver. The ''recv_probe'' method
-expression specifies the Boolean expression corresponding to the probe
-at the receiver end of the channel. A ''send_probe'' can be
-specified in a similar way when the sender is passive and receiver is
-active.
-The ''e1of2'' channel has been specified to perform a four-phase
-handshake protocol. If the channel were to correspond to a two-phase
-protocol, a different sequence of actions can be specified instead.
-Port lists for channel types can be data types (built-in or
-user-defined) or channels. Processes are not valid types for ports of a
-channel type.
-==== Instantiating user-defined types ====
-User-defined type variables can be instantiated in much the same manner
-as ordinary type variables.
-<code>
-defproc test(bool N, n) { ... }
-test x;
-// x.N and x.n refer to the ports of ''x''
-</code>
-The ACT description above creates an instance of type ''test'' named
-''x''. Creating an instance of a type creates instances of all the
-ports listed as well as creating whatever is specified by the body of
-the type definition. The list of ports of a user-defined type can be
-accessed from the scope outside the type definition by using
-dot-notation. These externally visible ports are analogous to the
-//fields// of structures or record types in standard programming
-languages.
-This analogy to records can be used to build complex data types,
-albeit with slightly different syntax compared to traditional
-programming languages. The following is a simple example that
-illustrates this.
-<code>
-deftype mystruct <: int<16> (int<4> f1, f2; int<8> f3)
-{
-  methods {
-   set {
-     f1:=self >> 12;
-     f2:=(self >> 8) & 0xf;
-     f3:=self & 0xff
-   }
-   get {
-     self:=(f1 << 12) | (f2 << 8) | f3
-   }
-  }
-}
-</code>
+===== Parameterized built-in types =====
-===== Parameterized types =====
 Parameterized types give ACT considerable flexibility in type
 definitions. Parameterized types come in two flavors: built-in types,
@@ Line 527: / Line 198: @@
 the definition of another one.
-==== Built-in integers and channels ====
 Although we have been describing the types ''int'' and ''chan''
-as simple types, they are in fact paramterized. Omitting the
+as simple types, they are in fact parameterized. Omitting the
 parameters makes ACT use implicit default parameters for both of
 them.
@@ Line 538: / Line 208: @@
 brackets, as shown below:
-<code>
+<code act>
 int<1> x; // x is a one bit integer
 int<37> y; // y is a thirty-seven bit integer
@@ Line 549: / Line 219: @@
 being sent and received on the channel.
-<code>
+<code act>
 chan(bool) x; // x is a Boolean channel
 chan(int<16>) y; // y is a 16-bit integer channel
@@ Line 556: / Line 226: @@
 The default data type for a channel is assumed to be the default
 ''int'', namely ''int<32>''.
+Channels are almost always unidirectional, with data being transferred from sender to receiver.
+In a few cases, it is useful to be able to transfer data from the sender to the receiver, and from the
+receiver to the sender in one channel action. To declare a channel where data are transferred in
+both directions, use:
+<code act>
+// a bool is transferred from sender to receiver, and
+// an int is transferred from the receiver to the sender
+chan(bool,int) x;
+</code>
+These are sometimes called //exchange channels//, since data is exchanged between the sender and receiver.
 Another built-in data type is the //enumeration// type. An
@@ Line 561: / Line 243: @@
 restricted range.
-<code>
+<code act>
 enum<5> x; // x can take on values 0, 1, 2, 3, 4
 </code>
@@ Line 568: / Line 250: @@
 of expressions. Also, enumerations that have power-of-two ranges are
 type-equivalent to the approprate ''int'' type. For instance,
-''enum<2>''@ is equivalent to ''int<1>''. Enumerations are
+''enum<2>'' is equivalent to ''int<1>''. Enumerations are
 useful when specifying a data value that is a one-hot code.
-==== User-defined types ====
-Processes, channels, and datatypes created using ''defproc'',
-''defchan'', and ''deftype'' all support
-parameterization. Parameters are specified using the ''template''
-keyword.
-Since the syntax for all three is the same, we use a process
-definition to illustrate this. To create a parameterized type, the
-definition of the type is preceeded by a template specifier as shown
-below.
-<code>
-// A generic adder block
-template<pint N>
-defproc adder (e1of2 a[N], b[N]; e1of2 s[N])
-{
-  ...
-}
-</code>
-This example defines an ''adder'' that takes ''N'' as a
-parameter. Note that the value of ''N'' determines the size of the
-arrays in the port list for the process. Instances of this
-''adder'' can be created in the following way:
-<code>
-adder<4> a1;  // a1 is a 4-bit adder
-adder<16> a2; // a2 is a 16-bit adder
-</code>
-The value of ''a1.N'' is 4, while the value of ''a2.N'' is
-. To illustrate how one might define this adder block, assume we
-have processes ''fulladder'', ''zerosource'', and
-''bitbucket'' already defined that implement a full-adder, a
-constant source of zeros, and a constant sink respectively. One
-possible definition of the adder would be:
-<code>
-template<pint N>
-defproc adder (e1of2 a[N], b[N]; e1of2 s[N])
-{
-   fulladder fa[N];
-   ( i : N-1 : fa[i].a = a[i]; fa[i].b = b[i]; fa[i].s = s[i];
-                fa[i].co = fa[i+1].ci; )
-   zerosource z;
-   bitbucket w;
-   fa[0].ci=z.x;
-   fa[N-1].co = w.x;
-}
-</code>
-This creates a parameterized ripple-carry adder. Notice the use of
-loops and arrays to connect the carry chain for the adder, and the
-inputs and outputs of the process to the ''fulladder'' ports.
-As shown in the example above, the arguments in the template parameter
-list are specified by listing them next to the type name.  Trailing
-arguments can be omitted from the parameter list attached to the type
-as shown in the example below.
-<code>
-template<pint N; preal w[N]>
-defproc test (bool n[N]) { ... }
-test<5> x;
-</code>
-Channels and data types can also be parameterized in the same way. For
-example, the following might be an N-bit dual rail definition.
-<code>
-template<pint N>
-deftype d1of2 <: int<N> (bool d0[N], d1[N]) { ... }
-</code>
-Since the body of the type can use loops and selection statements in
-arbitrary ways, changing the parameters for the type can completely
-change the structure of the circuit. It can also change the ports for
-the type. Hence, when checking for type compatibility, the values of
-parameters are also taken into account. Hence, the full type for
-instance ''a2'' above is in fact ''adder<5>'', not just
-''adder''. Types such as ''fulladder'' that do not have
-parameters are more completely specified as ''fulladder<>'',
-although the angle brackets can be omitted. Arrays can only correspond
-to instances of the same type---so an array cannot contain a three-bit
-adder and five-bit adder.
 ===== Directional types =====
@@ Line 665: / Line 260: @@
 type can be defined, and they are shown below:
-<code>
+<code act>
 bool x;  // Boolean that may be read or written
 bool! y; // Boolean that must be written, and may be read
@@ Line 680: / Line 275: @@
 output on ''c''.
-<code>
+<code act>
 defcell nand2 (bool? a, b; bool! c) { ... }
 </code>
@@ Line 687: / Line 282: @@
 different.
-<code>
+<code act>
 chan(int) x;  // Sends or receives are permitted
 chan!(int) y; // Only sends permitted
@@ Line 696: / Line 291: @@
 constructs are useful in libraries for additional error checking, and
 conveying more information to the user of the library.
-==== Interaction with user-defined types ====
-Direction specifications can be used for built-in data and channel
-types, as well as user-defined types. Consider the ''e1of2''
-user-defined channel type that we saw earlier:
-<code>
-defchan e1of2 <: chan(bool) (bool d0,d1,e)
-{
-   spec {
-    exclhi(d0,d1)
-   }
-   methods {
-    set {
-      [e];[self->d1+[]~self->d0+]
-    }
-    send_rest {
-      [~e];d0-,d1-
-    }
-    get {
-     [d0->self-[]d1->self+]
-    }
-    recv_rest {
-     e-;[~d0&~d1];e+
-    }
-    recv_probe = (d0|d1);
-   }
-}
-</code>
-When we use ''e1of2?'' or ''e1of2!'', we need some mechanism to
-specify the access permissions for the //port parameters// of the
-user-defined type. The convention used is that there are five possible
-ways to specify any constraints on access to port parameters. For our
-example, we can use one of the following variations in the port parameter list:
-<code>
-bool d0; // No constraints; this port could be read or written
-bool! d0; // Both e1of2? and e1of2! have bool! permissions
-bool? d0; // Both e1of2? and e1of2! have bool? permissions
-bool?! d0; // e1of2? has bool? permissions, and e1of2! has bool! permissions
-bool!? d0; // e1of2? has bool! permissions, and e1of2! has bool? permissions
-</code>
-Hence, a better definition of an ''e1of2'' channel would more
-completely specify the access permissions for the port parameters in
-the following way.
-<code>
-defchan e1of2 <: chan(bool) (bool?! d0,d1; bool!? e) { ... }
-</code>
-A careful examination of the type signature reveals that the sender
-and receiver have the appropriate permissions. There is a subtle
-interaction between connections and directional types in ACT, and this
-is detailed in the section on connections.
-===== 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 above, 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 a
-refinement 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 refinement between two
-user-defined types. Refinement 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.
-==== Refinement ====
-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>
-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>
-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>
-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>
-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>
-type2<5,7> x;
-// x.M=5, x.N=7
-</code>
-would set ''N'' (the new template parameter) to ''5'', and
-''M'' (the parent, still definable parameter) to ''7''. Finally,
-the following would be an error:
-<code>
-template<pint N> defproc type1 (bool a, b) { ... }
-template<pint N> defproc type2 <: type1 (bool c) { ... }
--[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>
-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>
-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>
-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>
-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>
-+{
-    @var{type} @var{list-of-ids};
-    ...
- }
-</code>
-The identifiers cannot contain array specifiers, and the types canot
-have any direction flags. 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.
-Implemetation 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.
-**XXX: test this**
-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.
-===== The ptype =====