diff --git a/docs/Cryptol.pdf b/docs/Cryptol.pdf new file mode 100644 index 00000000..52081e8a Binary files /dev/null and b/docs/Cryptol.pdf differ diff --git a/docs/CryptolPrims.md b/docs/CryptolPrims.md index 1134b147..f8f26ad6 100644 --- a/docs/CryptolPrims.md +++ b/docs/CryptolPrims.md @@ -20,6 +20,7 @@ Comparisons and Ordering instance (Cmp a, Cmp b) => Cmp (a, b) instance (Cmp a, Cmp b) => Cmp { x : a, y : b } instance Cmp Integer + instance Cmp Rational Signed Comparisons --------------------- @@ -41,30 +42,50 @@ Signed Comparisons Arithmetic ---------- - (+) : {a} (Arith a) => a -> a -> a - (-) : {a} (Arith a) => a -> a -> a - (*) : {a} (Arith a) => a -> a -> a - (/) : {a} (Arith a) => a -> a -> a - (%) : {a} (Arith a) => a -> a -> a - (^^) : {a} (Arith a) => a -> a -> a - (/$) : {a} (Arith a) => a -> a -> a - (%$) : {a} (Arith a) => a -> a -> a - lg2 : {a} (Arith a) => a -> a - negate : {a} (Arith a) => a -> a + (+) : {a} (Ring a) => a -> a -> a + (-) : {a} (Ring a) => a -> a -> a + (*) : {a} (Ring a) => a -> a -> a + negate : {a} (Ring a) => a -> a + + (/) : {a} (Integral a) => a -> a -> a + (%) : {a} (Integral a) => a -> a -> a + + (/.) : {a} (Field a) => a -> a -> a + recip : {a} (Field a) => a -> a + + floor : {a} (Round a) => a -> Integer + ceiling : {a} (Round a) => a -> Integer + trunc : {a} (Round a) => a -> Integer + round : {a} (Round a) => a -> Integer + + (^^) : {a, n} (Ring a, fin n) => a -> [n] -> a + (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + lg2 : {n} (fin n) => [n] -> [n] The prefix notation `- x` is syntactic sugar for `negate x`. // No instance for `Bit`. - instance (fin n) => Arith ([n]Bit) - instance (Arith a) => Arith ([n]a) - instance (Arith b) => Arith (a -> b) - instance (Arith a, Arith b) => Arith (a, b) - instance (Arith a, Arith b) => Arith { x : a, y : b } - instance Arith Integer + instance (fin n) => Ring ([n]Bit) + instance (Ring a) => Ring ([n]a) + instance (Ring b) => Ring (a -> b) + instance (Ring a, Ring b) => Ring (a, b) + instance (Ring a, Ring b) => Ring { x : a, y : b } + instance Ring Integer + instance (fin n, n>=1) => Ring (Z n) + instance Ring Rational -Note that because there is no instance for `Arith Bit` +Note that because there is no instance for `Ring Bit` the top two instances do not actually overlap. + instance Integral Integer + instance (fin n) => Integral ([n]Bit) + instance (fin n, n>=1) => Integral (Z n) + + instance Field Rational + + instance Round Rational + Boolean ------- @@ -100,14 +121,14 @@ Sequences reverse : {n,a} (fin n) => [n]a -> [n]a transpose : {n,m,a} [n][m]a -> [m][n]a - (@) : {n,a,m} [n]a -> [m] -> a - (@@) : {n,a,m,i} [n]a -> [m][i] -> [m]a - (!) : {n,a,m} (fin n) => [n]a -> [m] -> a - (!!) : {n,a,m,i} (fin n) => [n]a -> [m][i] -> [m]a - update : {n,a,m} (fin m) => [n]a -> [m] -> a -> [n]a - updateEnd : {n,a,m} (fin n, fin m) => [n]a -> [m] -> a -> [n]a - updates : {n,a,m,d} (fin m, fin d) => [n]a -> [d][m] -> [d]a -> [n]a - updatesEnd : {n,a,m,d} (fin n, fin m, fin d) => [n]a -> [d][m] -> [d]a -> [n]a + (@) : {n,a,ix} (Integral ix) => [n]a -> ix -> a + (@@) : {n,k,ix,a} (Integral ix) => [n]a -> [k]ix -> [k]a + (!) : {n,a,ix} (fin n, Integral ix) => [n]a -> ix -> a + (!!) : {n,k,ix,a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a + update : {n,a,ix} (Integral ix) => [n]a -> ix -> a -> [n]a + updateEnd : {n,a,ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a + updates : {n,k,ix,a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + updatesEnd : {n,k,ix,d} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a take : {front,back,elem} (fin front) => [front + back]elem -> [front]elem drop : {front,back,elem} (fin front) => [front + back]elem -> [back]elem @@ -123,13 +144,13 @@ in a different order. Shift And Rotate ---------------- - (<<) : {n,a,m} (fin n, Zero a) => [n]a -> [m] -> [n]a - (>>) : {n,a,m} (fin n, Zero a) => [n]a -> [m] -> [n]a - (<<<) : {n,a,m} (fin n) => [n]a -> [m] -> [n]a - (>>>) : {n,a,m} (fin n) => [n]a -> [m] -> [n]a + (<<) : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (>>) : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + (<<<) : {n,ix,a} (fin n, Integral ix) => [n]a -> ix -> [n]a + (>>>) : {n,ix,a} (fin n, Integral ix) => [n]a -> ix -> [n]a // Arithmetic shift only for bitvectors - (>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n] + (>>$) : {n,ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n] Random Values ------------- diff --git a/docs/CryptolPrims.pdf b/docs/CryptolPrims.pdf index e6e84af0..7971d6e4 100644 Binary files a/docs/CryptolPrims.pdf and b/docs/CryptolPrims.pdf differ diff --git a/docs/ProgrammingCryptol.pdf b/docs/ProgrammingCryptol.pdf index ca0c30aa..52081e8a 100644 Binary files a/docs/ProgrammingCryptol.pdf and b/docs/ProgrammingCryptol.pdf differ diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index 249c42d1..2bb53617 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -33,17 +33,18 @@ time. \section{Basic data types} \label{sec:basic-data-types} -Cryptol provides five basic data types: bits, sequences, integers, -tuples, and records. Words (i.e., $n$-bit numbers) are a special case -of sequences. Note that, aside from bits and integers, all other +Cryptol provides seven basic data types: bits, sequences, integers, +integers-modulo-n, rationals, tuples, and records. +Words (i.e., $n$-bit numbers) are a special case +of sequences. Note that, aside from the base types (like bits and integers), Cryptol types can be nested as deep as you like. That is, we can have records of sequences containing tuples made up of other records, etc., giving us a rich type-system for precisely describing the shapes of data our programs manipulate. While Cryptol is statically typed, it uses type inference to supply -unspecified types. That is, the user does {\em not} have to write the -types of all expressions; they will be automatically inferred by the +unspecified types. That is, the user usually does {\em not} have to +write the types of all expressions; they will be automatically inferred by the type-inference engine. Of course, in certain contexts the user might choose to supply a type explicitly. The notation is simple: we simply put the expression, followed by {\tt :} and the type. For instance, @@ -117,8 +118,8 @@ Here is the response from Cryptol, in order: A word is simply a numeric value with some number of bits, corresponding to the usual notion of binary numbers.\indTheWordType To match our observation of how cryptographers use binary numbers, -Cryptol only supports non-negative ($\geq 0$) word values (i.e., no -floating point or negative numbers).\indFloatingPoint However, words +Cryptol defaults to interpreting words as non-negative ($\geq 0$) +values (i.e., no negative numbers). However, words can be arbitrarily large: There is no predefined maximum number of bits that we are limited to.\indArbitraryPrecision The type of $n$-bit words is written \texttt{[n]}; e.g. \texttt{[8]} is the 8-bit word type. @@ -206,15 +207,16 @@ override this by giving an explicit type signature.\indSignature %===================================================================== \sectionWithAnswers{Integers: Unbounded numbers}{sec:integer} -The type \texttt{Integer} represents mathematical integers of -unlimited size. To write an integer value in Cryptol, simply write the -number in decimal, optionally annotated with \texttt{:Integer} to -disambiguate the type. Numbers written in base 2, 8, or 16 are always -$n$-bit words, and never have type \texttt{Integer}. However, they can -be converted to unbounded integers using \texttt{toInteger}. For -example, \texttt{toInteger 0xff} represents the integer 255. To write -a negative integer, simply negate the result: For example, -\texttt{-12} and \texttt{- toInteger 0xc} represent the integer $-12$. +The type \texttt{Integer}\indTheIntegerType represents mathematical +integers of unlimited size. To write an integer value in Cryptol, +simply write the number in decimal, optionally annotated with +\texttt{:Integer} to disambiguate the type. Numbers written in base 2, +8, or 16 are always $n$-bit words, and never have type +\texttt{Integer}. However, they can be converted to unbounded integers +using \texttt{toInteger}. For example, \texttt{toInteger 0xff} +represents the integer 255. To write a negative integer, simply negate +the result: For example, \texttt{-12} and \texttt{- toInteger 0xc} +represent the integer $-12$. \begin{Exercise}\label{ex:int:1} Compare the results of evaluating the expressions \texttt{0x8 + 0x9} @@ -235,6 +237,56 @@ is 17. The final result is also due to wraparound: \texttt{- 0x5} evaluates to \texttt{0xb} or 11, which is $-5 + 16$. \end{Answer} +In addition to the unbounded \texttt{Integer} type, there are also a +collection of bounded integer types: \texttt{Z n} for each finite +positive \texttt{n}. \texttt{Z n} represents the ring of integers modulo \texttt{n}. +Just like with fixed-width bitvector values, arithmetic in +\texttt{Z n} will ``wrap around'' (i.e., be reduced modulo \texttt{n}) +when values get too large. +\begin{Exercise}\label{ex:int:2} + Compare the results of evaluating \texttt{ (5 : Z 7) + (6 : Z 7) } + with \texttt{ toInteger (5 : Z 7) + toInteger (6 : Z 7) }. + What is the result of \texttt{ -3 : Z 7 }? + Were the results what you expected? +\end{Exercise} +\begin{Answer}\ansref{ex:int:2} +Here are Cryptol's responses: +\begin{Verbatim} + 4 + 11 + 4 +\end{Verbatim} +\end{Answer} + +%===================================================================== +\section{Rationals} +\label{sec:rational} + +The type \texttt{Rational}\indTheRationalType represents the rational number subset +of the real line: that is, those numbers that can be represented +a ratio of integers. You can explicitly create rational values using +the \texttt{ratio} function, which accepts the numerator and denominator +as integer values, or you can create a rational value from an +integer using the \texttt{fromInteger} function. Rational values can +also be created directly from literals the same way as for +\texttt{Integer}. + +For example, all of the following expression create the same +value representing one half: +\begin{Verbatim} + ratio 1 2 + ratio 2 4 + (1 /. 2) : Rational + (recip 2) : Rational + (fromInteger (-1) /. fromInteger (-2)) : Rational +\end{Verbatim} + +Note, the division operation on \texttt{Rational} is +written \texttt{/.}, and should not be confused with +\texttt{/}, which is the division operation on for words +and integers. + + %===================================================================== % \section{Tuples: Heterogeneous collections} % \label{sec:tuple} @@ -463,7 +515,7 @@ $2\times 3 = 6$ elements. \end{Answer} \begin{Exercise}\label{ex:seq:5}\indParallel\indComp - A comprehension with multiple branchess is called a \emph{parallel + A comprehension with multiple branches is called a \emph{parallel comprehension}. We can have any number of parallel branches. The contents of each branch will be \emph{zipped} to obtain the results. Experiment with the following expressions: @@ -1235,14 +1287,19 @@ Here are Cryptol's responses: Before proceeding further, we have to take a detour and talk briefly about one of the most useful values in Cryptol: {\tt zero}.\indZero -The value {\tt zero} inhabits every type in Cryptol, and stands for -the value that consists of all {\tt False}\indFalse bits. The -following examples should illustrate the idea: +The value {\tt zero} inhabits every type in Cryptol. +The following examples should illustrate the idea: \begin{Verbatim} Cryptol> zero : Bit False Cryptol> zero : [8] 0 + Cryptol> zero : Integer + 0 + Cryptol> zero : Z 19 + 0 + Cryptol> zero : Rational + (ratio 0 1) Cryptol> zero : ([8], Bit) (0, False) Cryptol> zero : [8][3] @@ -1301,8 +1358,10 @@ Cryptol supports the usual binary arithmetic operators {\tt +}, {\tt division), {\tt \%} (integer modulus), along with \emph{ceiling} base-2 logarithm {\tt lg2} and binary {\tt min} and {\tt max}. -The important thing to remember is that all arithmetic in Cryptol is -modular,\indModular with respect to the underlying word size. As a +It is important thing to remember is that all arithmetic in Cryptol is +carried out according to the type of the values being computed; +for word types in particular, arithmetic is modular,\indModular +with respect to the underlying word size. As a consequence, there is no such thing as an overflow/underflow in Cryptol, as the result will be always guaranteed to fit in the resulting word size. While this is very handy for most applications of @@ -1353,7 +1412,6 @@ Try out the following expressions:\indEq\indNeq 2 % 0 3 + (if 3 == 2+1 then 12 else 2/0) 3 + (if 3 != 2+1 then 12 else 2/0) - lg2 (-25) : Integer lg2 (-25) : [_] \end{Verbatim} In the last expression, remember that unary minus will\indUnaryMinus @@ -1363,9 +1421,7 @@ operation? \begin{Answer}\ansref{ex:arith:4} The first, second, and fourth examples give a ``division by 0'' error message. In the third example, the division by zero occurs - only in an unreachable branch, so the result is not an error. The - logarithm at type \texttt{Integer} gives a ``logarithm of negative'' - error. + only in an unreachable branch, so the result is not an error. In the last expression, the number \texttt{25} fits in 5 bits, so the modulus is $2^5 = 32$. The unary minus yields \texttt{7}, hence @@ -1374,7 +1430,7 @@ operation? \end{Answer} \begin{Exercise}\label{ex:arith:5:1} -Division truncates down. Try out the following expressions:\indDiv\indMod +Integral division truncates down. Try out the following expressions:\indDiv\indMod \begin{Verbatim} (6 / 3, 6 % 3) (7 / 3, 7 % 3) @@ -1603,6 +1659,18 @@ sequence of bits. Hence, an equivalent (but verbose) way to write the type {\tt [17]} is {\tt [17]Bit}, which we would say in English as ``a sequence of length 17, whose elements are Bits.'' +\paragraph*{Integers}\indTheIntegerType The type \texttt{Integer} +represents the unbounded mathematical integers. Arithmetic on this +type will not overflow. + +\paragraph*{Modular integers} The type \texttt{Z n} represents +the subset of the integers from 0 to \texttt{n} (not including \texttt{n}). +Arithmetic on these types is done modulo \texttt{n}. + +\paragraph*{Rationals}\indTheRationalType The type \texttt{Rational} represents +the subset of the real line that can be represented as a ratio of integers. +As with the integers, arithmetic on this type does not overflow. + \paragraph*{Tuples}\indTheTupleType A tuple is a heterogeneous collection of arbitrary number of elements. Just like we write a tuple value by enclosing it in @@ -2862,11 +2930,12 @@ takes two objects of any single type that can be compared and returns a Bit.'' Cryptol defines a collection of basic type classes: \texttt{Logic}, -\texttt{Zero}, \texttt{Cmp}, \texttt{SignedCmp}, \texttt{Arith}, and +\texttt{Zero}, \texttt{Cmp}, \texttt{SignedCmp}, \texttt{Ring}, +\texttt{Integral}, \texttt{Field}, \texttt{Round}, and \texttt{Literal}. These appear in the type signature of operators and functions that require them. If a function you define calls, for example, \texttt{+}, on two arguments both of type \texttt{a}, the -type constraints for \texttt{a} will include \texttt{(Arith a)}. +type constraints for \texttt{a} will include \texttt{(Ring a)}. \begin{itemize} \item @@ -2898,14 +2967,38 @@ operators \texttt{<\$}, \texttt{>\$}, \texttt{<=\$}, and \texttt{>=\$}. These are like \texttt{<}, \texttt{>}, \texttt{<=}, and \texttt{>=}, except that they interpret bitvectors as \emph{signed} 2's complement numbers, whereas the \texttt{Cmp} operations use the -\emph{unsigned} ordering. +\emph{unsigned} ordering. \texttt{SignedCmp} does not contain the +other atomic numeric types in Cryptol, just bitvectors. \item -The \texttt{Arith} typeclass includes the binary operators \texttt{+}, -\texttt{-}, \texttt{*}, \texttt{/}, \verb+%+, and \verb+^^+, as well -as the unary operators \texttt{lg2} and \texttt{-}, and the function -\texttt{fromInteger}. Infinite sequence enumerations \texttt{[x ...]} -and \texttt{[x, y ...]} are also defined for class \texttt{Arith}. +The \texttt{Ring} typeclass includes the binary operators \texttt{+}, +\texttt{-}, \texttt{*}, and the unary operators \texttt{negate} +and \texttt{fromInteger}. All the numeric types in Cryptol +are members of \texttt{Ring}. + +\item +The \texttt{Integral} typeclass represents values that are ``like +integers''. It inclues the integral division and modulus operators +\texttt{/} and \texttt{\%}, and the \texttt{toInteger} casting function. +The sequence indexing, update and shifting operations +take index arguments that can be of any \texttt{Integral} type. +Infinite sequence enumerations \texttt{[x ...]} +and \texttt{[x, y ...]} are also defined for class \texttt{Integral}. +Bitvectors, integers, and moduluar integers are members of \texttt{Integral}. + +\item +The \texttt{Field} typeclass represents values that, in addition to +being a \texttt{Ring} posess a multiplictive inverses. +It includes the field division operation \texttt{/.} and the +\texttt{recip} operation for computing the reciprocol of a value. +Currently, only type \texttt{Rational} is a member of this class. + +\item + The \texttt{Round} typeclass contains types that can be + rounded to integers. It includes \texttt{floor}, \texttt{ceiling}, + \texttt{trunc} and \texttt{round} operations, which are all different + ways of rounding values to integers. +Currently, only type \texttt{Rational} is a member of this class. \item The \texttt{Literal} typeclass includes numeric literals. @@ -2915,17 +3008,17 @@ The \texttt{Literal} typeclass includes numeric literals. Without including an explicit type declaration, define a function that Cryptol infers has the following type: \begin{Verbatim} - cmpArith : {a,b} (Cmp a, Arith b) => a -> a -> b -> b + cmpRing : {a,b} (Cmp a, Ring b) => a -> a -> b -> b \end{Verbatim} \end{Exercise} \begin{Answer}\ansref{ex:tvar:1} This code: \begin{code} - cmpArith x y z = if x == y then z else z+z + cmpRing x y z = if x == y then z else z+z \end{code} yields the inferred type: \begin{Verbatim} - cmpArith : {a, b} (Arith b, Cmp a) => a -> a -> b -> b + cmpRing : {a, b} (Cmp a, Ring b) => a -> a -> b -> b \end{Verbatim} \end{Answer} diff --git a/docs/ProgrammingCryptol/prims/Primitives.tex b/docs/ProgrammingCryptol/prims/Primitives.tex index 5b9c7c7b..d3393c53 100644 --- a/docs/ProgrammingCryptol/prims/Primitives.tex +++ b/docs/ProgrammingCryptol/prims/Primitives.tex @@ -23,9 +23,26 @@ primsPlaceHolder=1; \end{Verbatim} \paragraph*{Arithmetic} \begin{Verbatim} - +, -, *, /, %, ^^ : {a} (Arith a) => a -> a -> a - negate, lg2 : {a} (Arith a) => a -> a - fromInteger : {a} (Arith a) => Integer -> a + +, -, * : {a} (Ring a) => a -> a -> a + negate : {a} (Ring a) => a -> a + fromInteger : {a} (Ring a) => Integer -> a + ^^ : {a} (Ring a, fin n) => a -> [n] -> a + abs : {a} (Cmp a, Ring a) => a -> a + /, % : {a} (Integral a) => a -> a -> a + toInteger : {a} (Integral a) => a -> Integer + lg2 : {n} (fin n) => [n] -> [n] + /$, %$ : {n} (fin n, n >= 1) => [n] -> [n] -> [n] + carry : {n} (fin n) => [n] -> [n] -> Bit + scarry, sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + zext : {m, n} (fin m, m >= n) => [n] -> [m] + sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] + ratio : Integer -> Integer -> Rational + /. : {a} (Field a) => a -> a -> a + recip : {a} (Field a) => a -> a + floor : {a} (Round a) => a -> Integer + ceiling : {a} (Round a) => a -> Integer + trunc : {a} (Round a) => a -> Integer + round : {a} (Round a) => a -> Integer \end{Verbatim} \paragraph*{Polynomial arithmetic} \begin{Verbatim} @@ -49,20 +66,20 @@ primsPlaceHolder=1; \end{Verbatim} \paragraph*{Indexing, updates} \begin{Verbatim} - @ : {n, a, ix} (fin ix) => [n]a -> [ix] -> a - ! : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a - @@ : {n, k, ix, a} (fin ix) => [n]a -> [k][ix] -> [k]a - !! : {n, k, ix, a} (fin n, fin ix) => [n]a -> [k][ix] -> [k]a + @ : {n, a, ix} (Integral ix) => [n]a -> ix -> a + ! : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a + @@ : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a + !! : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a update : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a - updateEnd : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a -> [n]a - updates : {n, k, ix, a} (fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a - updatesEnd : {n, k, ix, a} (fin n, fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a + updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a + updates : {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a + updatesEnd : {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a \end{Verbatim} \paragraph*{Shifting, rotating} \begin{Verbatim} - >>>, <<< : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a - >>, << : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a - >>$ : {n, ix} (fin n, n >= 1, fin ix) => [n] -> [ix] -> [n] + >>>, <<< : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a + >>, << : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a + >>$ : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n] \end{Verbatim} \paragraph*{Functional programming} \begin{Verbatim} diff --git a/docs/ProgrammingCryptol/utils/Indexes.tex b/docs/ProgrammingCryptol/utils/Indexes.tex index 7a37ea4e..622d69df 100644 --- a/docs/ProgrammingCryptol/utils/Indexes.tex +++ b/docs/ProgrammingCryptol/utils/Indexes.tex @@ -48,6 +48,8 @@ \newcommand{\indTheBitType}{\index{bit}\xspace} \newcommand{\indTheTupleType}{\index{tuple}\xspace} \newcommand{\indTheWordType}{\index{word}\xspace} +\newcommand{\indTheIntegerType}{\index{integer}\xspace} +\newcommand{\indTheRationalType}{\index{rational}\xspace} \newcommand{\indTheSequenceType}{\index{sequence}\xspace} \newcommand{\indTheRecordType}{\index{record}\xspace} \newcommand{\indTheStringType}{\index{string}\xspace} diff --git a/docs/Semantics.pdf b/docs/Semantics.pdf index 0ec56ff2..926a949a 100644 Binary files a/docs/Semantics.pdf and b/docs/Semantics.pdf differ