Defines an interface for a hardware module (see section
5.13). An
interface is essentially a struct, but its components are restricted
to those things that have a physical interpretation as wires in and out
of a circuit. The types of fields in an interface are more likely to
involve Action's (see section
5.11),
which are typically interpreted as "enable signals" into a circuit. The
fields of an interface are also known as methods (not to be confused
with methods of a class, described in Sections
2.1 and
4.5).
topDefn ::= interface typeId {tyVarId }= { { fieldDef ; }}
Example:
interface Stack a =
This describes a circuit that implements a stack (a LIFO) of items. This
polymorphic definition does not specify the type of the contents of the
stack, just that they have some type "a". Corresponding to the push
method, the circuit will have input wires to carry a value of type
"a", and a "push-enable" input wire that specifies when the value
present on the input wires should be pushed on the stack. Corresponding
to the pop component, the circuit will have a "pop-enable" input wire
that specifies when a value should be popped off the stack.
Corresponding to the top component, the circuit will have a set of
output wires: if the stack is empty, the wires will represent the value
Nothing, and if the stack is non-empty and $v$ is the value at the top
of the stack, the wires will represent Maybe $v$.