Types Module
Module Types implements the data types of the Quartz language.
Types
| Type | Description |
QType represents the data types that are available in the Quartz language. Qbool and Qreal implement booleans and real numbers (NOT floats), respectively. Qbtv, Qnat, and Qint represent bitvectors, natural numbers, and integer numbers that can be bounded or unbounded. The unbounded case is indicated with argument "None", while Qbtv(Some len) denotes bitvectors with "len" bits, and Qnat(Some bl) and Qint(Some bl) represent the numbers {0,...,N-1} {-N,...,N-1}, respectively, where bl is the radix-2 representation of N. Qarr(dim,qty) represents arrays with dimension dim whose elements have type qty, and Qtup tyL represents tuples consisting of elements (e1,...,en) having types tyL=[ty1;...;tyn]. |
Functions and values
| Function or value | Description |
|
get qty of Qarr(dim,qty); fails if applied to other types
|
|
get dim of Qarr(dim,qty); fails if applied to other types
|
|
GetQarrArgs(Qarr(dim,qty)) = (dim,qty), and fails otherwise
|
|
GetQbtvLen(Qbtv len) = len, and fails otherwise
|
|
GetQintRng(Qint rg) = rg, and fails otherwise
|
|
GetQnatRng(Qnat rg) = rg, and fails otherwise
|
|
GetQtupTyL(Qtup tyL) = tyL, and fails otherwise
|
|
Check whether qty1 is a subset of qty2; we identify Qbool with Qbtv(Some 1), view Qnat rg and Qint rg as subsets of Qreal, and embed Qnat rg in Qint rg. Clearly, Qnat rg1 is a subtype of Qnat rg2 if rg1<=rg2, and the same holds for Qint. However, Qbtv(Some 5) is not a subtype of Qbtv(Some 19).
|
|
|
|
check that the given type is not the empty set, i.e., that it contains some elements. This means that bitvectors must have a size>0, and the ranges of finite types Qnat and Qint must also be greater than 0. Moreover, each dimension of an array must be >1, and tuples must consist of more than one type.
|
|
computes the number of bits required to store elements of type qty; returns None if infinitely many are required
|
|
Determine the supremum type of two types if that exists.
|
|
|