Module documentation

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -54,8 +54,6 @@ means the value {\tt 12} has type {\tt [8]}, i.e., it is an 8-bit
 word. We shall see other examples of this in the following discussion.
 
 %=====================================================================
-\section{Bits: Booleans}
-\label{sec:bits}
 \sectionWithAnswers{Bits: Booleans}{sec:bits}
 
 The type {\tt Bit}\indTheBitType represents a single bit of
@@ -107,8 +105,6 @@ Here is the response from Cryptol, in order:
 \end{tip}
 
 %=====================================================================
-\section{Words: Numbers}
-\label{sec:words}
 \sectionWithAnswers{Words: Numbers}{sec:words}
 
 A word is simply a numeric value, corresponding to the usual notion of
@@ -188,8 +184,8 @@ the same value, so {\tt a} and {\tt A} both represent 10.
   Section~\ref{sec:words2}, after we learn about sequences.}
 
 %=====================================================================
-\section{Tuples: Heterogeneous collections}
-\label{sec:tuple}
+% \section{Tuples: Heterogeneous collections}
+% \label{sec:tuple}
 \sectionWithAnswers{Tuples: Heterogeneous collections}{sec:tuple}
 
 A tuple is a simple collection of arbitrary ordered values of
@@ -281,8 +277,8 @@ The required expression would be:
 \end{tip}
 
 %=====================================================================
-\section{Sequences: Homogeneous collections}
-\label{sec:sequences}
+% \section{Sequences: Homogeneous collections}
+% \label{sec:sequences}
 \sectionWithAnswers{Sequences: Homogeneous collections}{sec:sequences}
 
 While tuples contain heterogeneous data, sequences are used for
@@ -464,6 +460,7 @@ Comprehensions may be nested.\indNestedComp In this pattern, the
 element value expression of the outer nesting is a sequence
 comprehension (which may refer to values generated by the outer
 generator). The pattern looks like this:
+
 \begin{minipage}{\textwidth}  %% trying to avoid splitting this across pages
 \begin{Verbatim}
   [  [ <expr with x & y>  //                   \
@@ -900,8 +897,8 @@ Here are Cryptol's responses:
 \end{Answer}
 
 %=====================================================================
-\section{Words revisited}
-\label{sec:words2}
+% \section{Words revisited}
+% \label{sec:words2}
 \sectionWithAnswers{Words revisited}{sec:words2}
 
 In Section~\ref{sec:words} we have introduced numbers as a distinct
@@ -1153,8 +1150,8 @@ operations on them; including arithmetic:
 \end{Verbatim}
 
 %=====================================================================
-\section{Records: Named collections}
-\label{sec:records}
+% \section{Records: Named collections}
+% \label{sec:records}
 \sectionWithAnswers{Records: Named collections}{sec:records}
 
 In Cryptol, records are simply collections of named fields. In this
@@ -1218,8 +1215,8 @@ Here are Cryptol's responses:
   functionality in our current study.}
 
 %=====================================================================
-\section{\texorpdfstring{The {\tt zero}}{The zero}}
-\label{sec:zero}
+% \section{\texorpdfstring{The {\tt zero}}{The zero}}
+% \label{sec:zero}
 \sectionWithAnswers{\texorpdfstring{The {\tt zero}}{The zero}}{sec:zero}
 
 Before proceeding further, we have to take a detour and talk briefly
@@ -1244,7 +1241,7 @@ following examples should illustrate the idea:
 
 \noindent On the other extreme, the value {\tt zero} combined with the
 complement operator {\tt \Verb|~|}\indComplement gives us values that
-consist of all all {\tt True}\indTrue bits:
+consist of all {\tt True}\indTrue bits:
 \begin{Verbatim}
   Cryptol> ~zero : Bit
   True
@@ -1281,8 +1278,8 @@ The {\tt zero} function returns {\tt 0}, ignoring its argument.
 \end{Answer}
 
 %=====================================================================
-\section{Arithmetic}
-\label{sec:arithmetic}
+% \section{Arithmetic}
+% \label{sec:arithmetic}
 \sectionWithAnswers{Arithmetic}{sec:arithmetic}
 
 Cryptol supports the usual binary arithmetic operators {\tt +}, {\tt
@@ -1537,8 +1534,8 @@ element is at least $4$-bits wide.
 \end{Answer}
 
 %=====================================================================
-\section{Types}
-\label{sec:types}
+% \section{Types}
+% \label{sec:types}
 \sectionWithAnswers{Types}{sec:types}
 
 Cryptol's type system is one of its key features\footnote{The Cryptol
@@ -1996,8 +1993,8 @@ bit-precise programming problems it has been designed
 for~\cite{lewis2003}.
 
 %=====================================================================
-\section{Defining functions}
-\label{sec:funcs}
+% \section{Defining functions}
+% \label{sec:funcs}
 \sectionWithAnswers{Defining functions}{sec:funcs}
 
 So far, we used Cryptol as a calculator: we typed in expressions and
@@ -2281,8 +2278,8 @@ empty sequence that can satisfy the predicate.
 \end{Answer}
 
 %=====================================================================
-\section{Recursion and recurrences}
-\label{sec:recandrec}
+% \section{Recursion and recurrences}
+% \label{sec:recandrec}
 \sectionWithAnswers{Recursion and recurrences}{sec:recandrec}
 
 \todo[inline]{This section represents a big opportunity to emphasize sequence
@@ -2630,8 +2627,8 @@ arithmetic.\indModular
 \end{Answer}
 
 %=====================================================================
-\section{Stream equations}
-\label{sec:streameq}
+% \section{Stream equations}
+% \label{sec:streameq}
 \sectionWithAnswers{Stream equations}{sec:streameq}
 
 Most cryptographic algorithms are described in terms of operations on
@@ -2690,8 +2687,8 @@ The Cryptol code corresponding to this stream equation is:
 \end{Answer}
 
 %=====================================================================
-\section{Type synonyms}
-\label{sec:tsyn}
+% \section{Type synonyms}
+% \label{sec:tsyn}
 \sectionWithAnswers{Type synonyms}{sec:tsyn}\indTypSynonym
 
 \todo[inline]{Motivate type synonyms better; NQueens with nice
@@ -3031,6 +3028,64 @@ Here is a more interesting example:
 \todo[inline]{Why is this more interesting?  What are the reflections the
   reader should have?}
 
+%=====================================================================
+\section{Program structure with modules}
+
+When a cryptographic specification gets very large it can make sense
+to decompose its functions into modules. Doing this well encourages
+code re-use, so it's a generally good thing to do. Cryptol's module
+system is simple and easy to use. Here's a quick overview:
+
+A module's name should be the same as the filename the module is
+defined in. For example, the \verb+utilities+ module should be
+defined in a file called \verb+utilities.cry+. To specify that a file
+defines a module, its first non-commented line should be:
+
+\begin{verbatim}
+  module utilities where
+\end{verbatim}
+
+After that the variables and functions you define will be contained
+(in this example) in the {\it utilities} module.
+
+In the code where you want to use a module, you \verb+import+ it like this:
+\begin{verbatim}
+  import utilities
+\end{verbatim}
+
+Cryptol will look for the file \verb+utilities.cry+ in the current directory. Once you've imported a module, all of its variables and functions are available to use in your code.
+
+If you're writing a module that has both {\it private} and {\it public}
+definitions, you can hide the ones that shouldn't be exported to modules
+that include it by using the \verb+private+ keyword, like this:
+
+\begin{code}
+  private internalDouble x = x + x
+  exportedDouble = x * 2
+\end{code}
+
+As you can tell, by default definitions are exported to including modules.
+
+Finally, if you're importing a module that defines something with
+a name that you would like to define in your code, you can do a
+{\it qualified} import of that module like this:
+
+\begin{verbatim}
+  import utilities as util
+\end{verbatim}
+
+Now, instead of all the definitions being available in your module,
+they are qualified with the name you provided, in this case \verb+util+.
+This means you will prefix those names with \verb+util::+ when you call them,
+and the unqualified names are able to be defined in your own code.
+
+\begin{verbatim}
+  import utilities as util
+  // let's say utililities.cry defines "all", and we want to use
+  // it in our refined definition of all:
+  all xs = util::all xs && (width xs) > 0
+\end{verbatim}
+
 %=====================================================================
 \section{The road ahead}
 \label{sec:road-ahead}