Index: doc/theses/mike_brooks_MMath/array.tex
===================================================================
--- doc/theses/mike_brooks_MMath/array.tex	(revision ad9f5931463621e55b660fd57101ba749263b146)
+++ doc/theses/mike_brooks_MMath/array.tex	(revision c3e41cda7b7a639338faa16c005b96ed95202da9)
@@ -2,13 +2,17 @@
 \label{c:Array}
 
+Arrays in C are possibly the single most misunderstood and incorrectly used feature in the language, resulting in the largest proportion of runtime errors and security violations.
+This chapter describes the new \CFA language and library features that introduce a length-checked array type, @array@, to the \CFA standard library~\cite{Cforall}.
+
+Offering the @array@ type, as a distinct alternative to the C array, is consistent with \CFA's goal of backwards compatibility, \ie virtually all existing C (@gcc@) programs can be compiled by \CFA with only a small number of changes, similar to \CC (@g++@).
+However, a few compatibility-breaking changes to the behaviour of the C array are necessary, both as an implementation convenience and to fix C's lax treatment of arrays.
+Hence, the @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features, making it unnecessary to deal with every inherited complexity of the C array.
+
 
 \section{Introduction}
 \label{s:ArrayIntro}
 
-Arrays in C are possibly the single most misunderstood and incorrectly used feature in the language, resulting in the largest proportion of runtime errors and security violations.
-This chapter describes the new \CFA language and library features that introduce a length-checked array type to the \CFA standard library~\cite{Cforall}.
-
-Specifically, a new \CFA array is declared by instantiating the generic @array@ type,
-much like instantiating any other standard-library generic type (such as @dlist@),
+The new \CFA array is declared by instantiating the generic @array@ type,
+much like instantiating any other standard-library generic type (such as \CC @vector@),
 though using a new style of generic parameter.
 \begin{cfa}
@@ -16,8 +20,8 @@
 \end{cfa}
 Here, the arguments to the @array@ type are @float@ (element type) and @99@ (length).
-When this type is used as a function parameter, the type-system requires that a call's argument matches, down to the length.
+When this type is used as a function parameter, the type-system requires that a call's argument is a perfect match.
 \begin{cfa}
 void f( @array( float, 42 )@ & p ) {}	$\C{// p accepts 42 floats}$
-f( x );									$\C{// statically rejected: types are different, 99 != 42}$
+f( x );									$\C{// statically rejected: type lengths are different, 99 != 42}$
 
 test2.cfa:3:1 error: Invalid application of existing declaration(s) in expression.
@@ -25,9 +29,7 @@
 \end{cfa}
 Here, the function @f@'s parameter @p@ is declared with length 42.
-The call @f( x )@, with the argument being the previously-declared object, is invalid, because the @array@ lengths @99@ and @42@ do not match.
-
-A function declaration can be polymorphic over these @array@ arguments by using the @forall@ declaration prefix.
-This function @g@'s takes arbitrary type parameter @T@ (familiar) and \emph{dimension parameter} @N@ (new).
-A dimension paramter represents a to-be-determined count of elements, managed by the type system.
+However, the call @f( x )@ is invalid, because @x@'s length is @99@, which does not match @42@.
+
+A function declaration can be polymorphic over these @array@ arguments by using the \CFA @forall@ declaration prefix.
 \begin{cfa}
 forall( T, @[N]@ )
@@ -40,16 +42,26 @@
 Cforall Runtime error: subscript 1000 exceeds dimension range [0,99) $for$ array 0x555555558020.
 \end{cfa}
+Function @g@ takes an arbitrary type parameter @T@ and a \emph{dimension parameter} @N@.
+A dimension parameter represents a to-be-determined count of elements, managed by the type system.
 The call @g( x, 0 )@ is valid because @g@ accepts any length of array, where the type system infers @float@ for @T@ and length @99@ for @N@.
-Inferring values for @T@ and @N@ is implicit, without programmer involvement.
+Inferring values for @T@ and @N@ is implicit.
 Furthermore, in this case, the runtime subscript @x[0]@ (parameter @i@ being @0@) in @g@ is valid because 0 is in the dimension range $[0,99)$ of argument @x@.
-The call @g( x, 1000 )@ is also accepted through compile time;
+However, the call @g( x, 1000 )@ is also accepted through compile time;
 however, this case's subscript, @x[1000]@, generates an error, because @1000@ is outside the dimension range $[0,99)$ of argument @x@.
+In general, the @forall( ..., [N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and within a function.
+The syntactic form is chosen to parallel other @forall@ forms:
+\begin{cfa}
+forall( @[N]@ ) ...	$\C[1.5in]{// dimension}$
+forall( T ) ...		$\C{// value datatype (formerly, "otype")}$
+forall( T & ) ...	$\C{// opaque datatype (formerly, "dtype")}\CRT$
+\end{cfa}
+% The notation @array(thing, N)@ is a single-dimensional case, giving a generic type instance.
 
 The generic @array@ type is comparable to the C array type, which \CFA inherits from C.
 Their runtime characteristics are often identical, and some features are available in both.
-For example, assume a caller instantiates @N@ with 42 (discussion about how to follow) in:
+For example, assume a caller has an argument that instantiates @N@ with 42.
 \begin{cfa}
 forall( [N] )
-void declDemo() {
+void declDemo( ... ) {
 	float x1[N];						$\C{// built-in type ("C array")}$
 	array(float, N) x2;					$\C{// type from library}$
@@ -59,16 +71,11 @@
 The two variables have identical size and layout; they both encapsulate 42-float stack allocations, with no additional ``bookkeeping'' allocations or headers.
 Providing this explicit generic approach requires a significant extension to the \CFA type system to support a full-feature, safe, efficient (space and time) array-type, which forms the foundation for more complex array forms in \CFA.
-
-Admittedly, the @array@ library type (type for @x2@) is syntactically different from its C counterpart.
-A future goal (TODO xref) is to provide the new features upon a built-in type whose syntax approaches C's (declaration style of @x1@).
+In all following discussion, ``C array'' means the types like that of @x@ and ``\CFA array'' means the standard-library @array@ type (instantiations), like the type of @x2@.
+
+Admittedly, the @array@ library type for @x2@ is syntactically different from its C counterpart.
+A future goal (TODO xref) is to provide the new @array@ features with syntax approaching C's (declaration style of @x1@).
 Then, the library @array@ type could be removed, giving \CFA a largely uniform array type.
-At present, the C-syntax array gets partial support for the new features, so the generic @array@ is used exclusively when introducing features;
+At present, the C-syntax @array@ is only partially supported, so the generic @array@ is used exclusively in the thesis;
 feature support and C compatibility are revisited in Section ? TODO.
-
-Offering the @array@ type, as a distinct alternative to the C array, is consistent with \CFA's goal of backwards compatibility, \ie virtually all existing C (@gcc@) programs can be compiled by \CFA with only a small number of changes, similar to \CC (@g++@).
-However, a few compatibility-breaking changes to the behaviour of the C array are necessary, both as an implementation convenience and to fix C's lax treatment of arrays.
-Hence, the @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features, making it unnecessary to deal with every inherited complexity of the C array.
-
-In all discussion following, ``C array'' means the types like that of @x@ and ``\CFA array'' means the standard-library @array@ type (instantiations), like the type of @x2@.
 
 My contributions in this chapter are:
@@ -83,12 +90,7 @@
 
 
-\section{Definitions and design considerations}
-
-
-\subsection{Dependent typing}
-
-
-
-General dependent typing allows the type system to encode arbitrary predicates (e.g. behavioural specifications for functions),
+\section{Dependent typing}
+
+General dependent typing allows the type system to encode arbitrary predicates (\eg behavioural specifications for functions),
 which is an anti-goal for my work.
 Firstly, this application is strongly associated with pure functional languages,
@@ -101,5 +103,4 @@
 
 
-
 \section{Features added}
 
@@ -109,18 +110,18 @@
 By declaring type variables at the front of object declarations, an array dimension is lexically referenceable where it is needed.
 For example, a declaration can share one length, @N@, among a pair of parameters and the return,
-meaning that it requires both input arrays to be of the same length, and guarantees that the result with be of that length as well.
+meaning that it requires both input arrays to be of the same length, and guarantees that the result is of that length as well.
 \lstinput{10-17}{hello-array.cfa}
-This function @f@ does a pointwise comparison of its two input arrays, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated @bool@ array.
-The dynamic allocation of the @ret@ array by preexisting @alloc@ uses the parameterized dimension information implicitly within its @sizeof@ determination, and casts the return type.
-Note that alloc only sees one whole type for its @T@ (which is @f@'s @array(bool, N)@); this type's size is a computation based on @N@.
-\begin{cfa}
-// simplification
-static inline forall( T & | sized(T) )
+Function @f@ does a pointwise comparison of its two input arrays, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated @bool@ array.
+The dynamic allocation of the @ret@ array, by the library @alloc@ function,
+\begin{cfa}
+forall( T & | sized(T) )
 T * alloc() {
-	return (T *)malloc( sizeof(T) );
-}
-\end{cfa}
-This example illustrates how the new @array@ type plugs into existing \CFA behaviour by implementing necessary @sized@ assertions needed by other types.
-(@sized@ implies a concrete \vs abstract type with a runtime-available size, exposed as @sizeof@.)
+	return @(T *)@malloc( @sizeof(T)@ );
+}
+\end{cfa}
+uses the parameterized dimension information implicitly within its @sizeof@ determination, and casts the return type.
+Note that @alloc@ only sees one whole type for its @T@ (which is @f@'s @array(bool, N)@); this type's size is a computation based on @N@.
+This example illustrates how the new @array@ type plugs into existing \CFA behaviour by implementing necessary \emph{sized} assertions needed by other types.
+(\emph{sized} implies a concrete \vs abstract type with a runtime-available size, exposed as @sizeof@.)
 As a result, there is significant programming safety by making the size accessible and implicit, compared with C's @calloc@ and non-array supporting @memalign@, which take an explicit length parameter not managed by the type system.
 
@@ -142,12 +143,4 @@
 The result is a significant improvement in safety and usability.
 
-In general, the @forall( ..., [N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and within a function.
-The syntactic form is chosen to parallel other @forall@ forms:
-\begin{cfa}
-forall( @[N]@ ) ...	$\C[1.5in]{// dimension}$
-forall( T & ) ...	$\C{// opaque datatype (formerly, "dtype")}$
-forall( T ) ...		$\C{// value datatype (formerly, "otype")}\CRT$
-\end{cfa}
-% The notation @array(thing, N)@ is a single-dimensional case, giving a generic type instance.
 In summary:
 \begin{itemize}
@@ -168,5 +161,5 @@
 % agreed, though already said
 \item
-\CC does not allow a template function to be nested, while \CFA lests its polymorphic functions to be nested.
+\CC does not allow a template function to be nested, while \CFA lets its polymorphic functions to be nested.
 % why is this important?
 \item
@@ -227,15 +220,15 @@
 \end{cfa}
 \end{tabular}
-\caption{\lstinline{N}-style paramters, for \CC template \vs \CFA generic type }
+\caption{\lstinline{N}-style parameters, for \CC template \vs \CFA generic type }
 \label{f:TemplateVsGenericType}
 \end{figure}
 
 Just as the first example in \VRef[Section]{s:ArrayIntro} shows a compile-time rejection of a length mismatch,
-so are length mismatches stopped when they invlove dimension parameters.
+so are length mismatches stopped when they involve dimension parameters.
 While \VRef[Figure]{f:fHarness} shows successfully calling a function @f@ expecting two arrays of the same length,
 \begin{cfa}
 array( bool, N ) & f( array( float, N ) &, array( float, N ) & );
 \end{cfa}
-a static rejection occurs when attempting to call @f@ with arrays of potentially differing lengths.
+a static rejection occurs when attempting to call @f@ with arrays of differing lengths.
 \lstinput[tabsize=1]{70-74}{hello-array.cfa}
 When the argument lengths themselves are statically unknown,
@@ -252,5 +245,5 @@
 Orthogonally, the \CFA array type works within generic \emph{types}, \ie @forall@-on-@struct@.
 The same argument safety and the associated implicit communication of array length occurs.
-Preexisting \CFA allowed aggregate types to be generalized with type parameters, enabling parameterizing for element types.
+Preexisting \CFA allowed aggregate types to be generalized with type parameters, enabling parameterizing of element types.
 Now, \CFA also allows parameterizing them by length.
 Doing so gives a refinement of C's ``flexible array member'' pattern[TODO: cite ARM 6.7.2.1 pp18]\cite{arr:gnu-flex-mbr}.
@@ -259,18 +252,9 @@
 This flexibility, in turn, allows for multiple array members.
 \lstinput{10-15}{hello-accordion.cfa}
-This structure's layout has the starting offset of @studentIds@ varying according to the generic parameter @C@, and the offset of @preferences@ varying according to both generic parameters.
-
-The school example has the data structure capturing many students' course-preference forms.
-It has course- and student-level metadata (their respective display names) and a position-based preferecens' matrix.
-The input files in \VRef[Figure]{f:checkHarness} give example data.
-
-When a function operates on a @School@ structure, the type system handles its memory layout transparently.
-\lstinput{30-37}{hello-accordion.cfa}
-In the running example, this @getPref@ function answers,
-for the student at position @sIx@, what is the position of its @pref@\textsuperscript{th}-favoured class?
-
-\VRef[Figure]{f:checkHarness} shows the @School@ harness and results with different array sizes.
-This example program prints the courses in each student's preferred order, all using the looked-up display names.
-Note the declaration of the @school@ variable.
+The structure has course- and student-level metatdata (their respective field names) and a position-based preferences' matrix.
+Its layout has the starting offset of @studentIds@ varying according to the generic parameter @C@, and the offset of @preferences@ varying according to both generic parameters.
+
+\VRef[Figure]{f:checkHarness} shows a program main using @School@ and results with different array sizes.
+The @school@ variable holds many students' course-preference forms.
 It is on the stack and its initialization does not use any casting or size arithmetic.
 Both of these points are impossible with a C flexible array member.
@@ -280,41 +264,32 @@
 \end{cfa}
 This ability to avoid casting and size arithmetic improves safety and usability over C flexible array members.
-
+Finally, inputs and outputs are given at the bottom for different sized schools.
+The example program prints the courses in each student's preferred order, all using the looked-up display names.
 
 \begin{figure}
-% super hack to get this to line up
-\begin{tabular}{@{}ll@{\hspace{25pt}}l@{}}
-\begin{tabular}{@{}p{3.25in}@{}}
+\begin{cquote}
 \lstinput{50-55}{hello-accordion.cfa}
-\vspace*{-3pt}
 \lstinput{90-98}{hello-accordion.cfa}
-\end{tabular}
-&
-\raisebox{0.32\totalheight}{%
-}%
-&
-\end{tabular}
-
-TODO: Get Peter's layout help
-
-\$ cat school1
-
+\ \\
+@$ cat school1@
 \lstinput{}{school1}
 
-\$ ./a.out < school1
-
+@$ ./a.out < school1@
 \lstinput{}{school1.out}
 
-\$ cat school2
-
+@$ cat school2@
 \lstinput{}{school2}
 
-\$ ./a.out < school2
-
+@$ ./a.out < school2@
 \lstinput{}{school2.out}
+\end{cquote}
 
 \caption{\lstinline{School} harness, input and output}
 \label{f:checkHarness}
 \end{figure}
+
+When a function operates on a @School@ structure, the type system handles its memory layout transparently.
+\lstinput{30-37}{hello-accordion.cfa}
+In the example, this @getPref@ function answers, for the student at position @is@, what is the position of its @pref@\textsuperscript{th}-favoured class?
 
 
@@ -333,17 +308,17 @@
 But simplifications close enough for the present discussion are:
 \begin{cfa}
-	forall( [N] )
-	struct array_1d_float {
-		float items[N];
-	};
-	forall( T, [N] )
-	struct array_1d {
-		T items[N];
-	};
-\end{cfa}
-This structure pattern, plus a subscript operator, is all that @array@ provides.
+forall( [N] )
+struct array_1d_float {
+	float items[N];
+};
+forall( T, [N] )
+struct array_1d_T {
+	T items[N];
+};
+\end{cfa}
+These two structure patterns, plus a subscript operator, is all that @array@ provides.
 
 My main work is letting a programmer define
-such a structre (one whose type is parameterized by @[N]@)
+such a structure (one whose type is parameterized by @[N]@)
 and functions that operate on it (these being similarly parameterized).
 
@@ -351,12 +326,11 @@
 \begin{itemize}
 \item
-	The resolver, providing values for a used declaration's type-system variables,
+	Resolver provided values for a used declaration's type-system variables,
 	gathered from type information in scope at the usage site.
-
 \item
 	The box pass, encoding information about type parameters
 	into ``extra'' regular parameters/arguments on declarations and calls.
 	Notably, it conveys the size of a type @foo@ as a @__sizeof_foo@ parameter,
-	and rewrites the @sizeof(foo)@ expression as @__sizeof_foo@, i.e. a use of the parameter.
+	and rewrites the @sizeof(foo)@ expression as @__sizeof_foo@, \ie a use of the parameter.
 \end{itemize}
 
@@ -364,17 +338,17 @@
 This work is detailed in \VRef[Section]{s:ArrayTypingC}.
 However, the resolution--boxing scheme, in its preexisting state, was already equipped to work on (desugared) dimension parameters.
-The discussion following explains the desugaring and how correct lowered code results.
-
-An even simpler structure, and a toy function on it, demonstrate what's needed for the encoding.
-\begin{cfa}
-	forall( [@N@] ) { // [1]
-		struct thing {};
-		void f( thing(@N@) ) { sout | @N@; } // [2], [3]
-	}
-	int main() {
-		thing( @10@ ) x;  f(x);  // prints 10, [4]
-		thing( 100 ) y;  f(y);  // prints 100
-		return 0;
-	}
+The following discussion explains the desugaring and how correctly lowered code results.
+
+A simpler structure, and a toy function on it, demonstrate what is needed for the encoding.
+\begin{cfa}
+forall( [@N@] ) { $\C{// [1]}$
+	struct thing {};
+	void f( thing(@N@) ) { sout | @N@; } $\C{// [2], [3]}$
+}
+int main() {
+	thing( @10@ ) x;  f( x );  $\C{// prints 10, [4]}$
+	thing( 100 ) y;  f( y );  $\C{// prints 100}$
+	return 0;
+}
 \end{cfa}
 This example has:
@@ -389,5 +363,5 @@
 	A value like 10 being used as an argument to the parameter @N@.
 \end{enumerate}
-The chosen solution being to encode the value @N@ \emph{as a type}, items 1 and 2 are immediately available for free.
+The chosen solution is to encode the value @N@ \emph{as a type}, so items 1 and 2 are immediately available for free.
 Item 3 needs a way to recover the encoded value from a (valid) type (and to reject invalid types occurring here).
 Item 4 needs a way to produce a type that encodes the given value.
@@ -400,5 +374,5 @@
 \item
 	Given a dimension expression $e$, produce type @char[@$e$@]@ to represent it.
-	If $e$ evaluates to $n$ then the endoded type has size $n$.
+	If $e$ evaluates to $n$ then the encoded type has size $n$.
 \item
 	Given a type $T$ (produced by these rules), recover the value that it represents with the expression @sizeof(@$T$@)@.
@@ -410,13 +384,13 @@
 The running example is lowered to:
 \begin{cfa}
-	forall( @N*@ ) { // [1]
-		struct thing {};
-		void f( thing(@N@) ) { sout | @sizeof(N)@; } // [2], [3]
-	}
-	int main() {
-		thing( char[@10@] ) x;  f(x);  // prints 10, [4]
-		thing( char[100] ) y;  f(y);  // prints 100
-		return 0;
-	}
+forall( @N *@ ) { $\C{// [1]}$
+	struct thing {};
+	void f( thing(@N@) ) { sout | @sizeof(N)@; } $\C{// [2], [3]}$
+}
+int main() {
+	thing( char[@10@] ) x;  f( x );  $\C{// prints 10, [4]}$
+	thing( char[100] ) y;  f( y );  $\C{// prints 100}$
+	return 0;
+}
 \end{cfa}
 Observe:
@@ -430,18 +404,17 @@
 	The @sout...@ expression (being an application of the @?|?@ operator) has a second argument that is an ordinary expression.
 \item
-	The type of variable @x@ is another @thing(-)@ type;  the argument to the generic @thing@ is a type (array type).
+	The type of variable @x@ is another @thing(-)@ type; the argument to the generic @thing@ is a type (array type of bytes, @char@).
 \end{enumerate}
 
 From this point, preexisting \CFA compilation takes over lowering it the rest of the way to C.
-Inspecting the result shows what the above translation achieves.
-A form that shows only the relevant changes of the box pass (as informed by the resolver), leaving the rest unadulterated, is:
-\begin{cfa}
-	// [1]
-	void f( size_t __sizeof_N, @void *@ ) { sout | @__sizeof_N@; } // [2], [3]
-	int main() {
-		struct __conc_thing_10 {} x;  f(@10@, &x);  // prints 10, [4]
-		struct __conc_thing_100 {} y;  f(@100@, &y);  // prints 100
-		return 0;
-	}
+Here the result shows only the relevant changes of the box pass (as informed by the resolver), leaving the rest unadulterated:
+\begin{cfa}
+// [1]
+void f( size_t __sizeof_N, @void *@ ) { sout | @__sizeof_N@; } $\C{// [2], [3]}$
+int main() {
+	struct __conc_thing_10 {} x;  f( @10@, &x );  $\C{// prints 10, [4]}$
+	struct __conc_thing_100 {} y;  f( @100@, &y );  $\C{// prints 100}$
+	return 0;
+}
 \end{cfa}
 Observe:
@@ -452,13 +425,13 @@
 	The type @thing(N)@ is (replaced by @void *@, but thereby effectively) gone.
 \item
-	The @sout...@ expression (being an application of the @?|?@ operator) has a second argument that is a regular variable (parameter) usage.
+	The @sout...@ expression (being an application of the @?|?@ operator) has a regular variable (parameter) usage for its second argument.
 \item
 	Information about the particular @thing@ instantiation (value 10) has moved, from the type, to a regular function-call argument.
 \end{enumerate}
-At the end of the desugaring and downstream processing, the original C idiom of ``pass both a pointer and a length parameter'' has been reconstructed.
-In the programmer-written form, only the thing is passed.
+At the end of the desugaring and downstream processing, the original C idiom of ``pass both a length parameter and a pointer'' has been reconstructed.
+In the programmer-written form, only the @thing@ is passed.
 The compiler's action produces the more complex form, which if handwritten, would be error-prone.
 
-Back at the very front end, the parsing changes, AST schema extensions, and validation rules for enabling the sugared user input are:
+Back at the compiler front end, the parsing changes AST schema extensions and validation rules for enabling the sugared user input.
 \begin{itemize}
 \item
@@ -467,5 +440,5 @@
 	Have the new brand of type-variable, \emph{Dimension}, in the AST form of a type-variable, to represent one parsed from @[-]@.
 \item
-	Allow a type variable to occur in expression position.  Validate (after parsing) that only dimension-branded type variables are used here.
+	Allow a type variable to occur in an expression.  Validate (after parsing) that only dimension-branded type variables are used here.
 \item
 	Allow an expression to occur in type-argument position.  Brand the resulting type argument as a dimension.
@@ -473,6 +446,7 @@
 	Validate (after parsing), on a generic-type usage, \eg the type part of the declaration
 	\begin{cfa}
-		@array_1d( foo, bar ) x;@
+	array_1d( foo, bar ) x;
 	\end{cfa}
+	\vspace*{-10pt}
 	that the brands on the generic arguments match the brands of the declared type variables.
 	Here, that @foo@ is a type and @bar@ is a dimension.
@@ -488,13 +462,12 @@
 from one party who knows it, to another who is willing to work with any given length.
 For scenarios where the concern is a mishandled length,
-the interaction is between two parties who both claim to know (something about) it.
-Such a scenario occurs in this pure C fragment, wich today's C compilers accept:
-\begin{cfa}
-	int n = @42@;
-	float x[n];
-	float (*xp)[@999@] = &x;
-	(*xp)[@500@];  // in "bound"?
-\end{cfa}
-
+the interaction is between two parties who both claim to know something about it.
+Such a scenario occurs in this pure C fragment, which today's C compilers accept:
+\begin{cfa}
+int n = @42@;
+float x[n];
+float (*xp)[@999@] = &x;
+(*xp)[@500@]; $\C{// in "bound"?}$
+\end{cfa}
 Here, the array @x@ has length 42, while a pointer to it (@xp@) claims length 999.
 So, while the subscript of @xp@ at position 500 is out of bound of its referent @x@,
@@ -505,22 +478,17 @@
 The \CFA new-array rejects the analogous case:
 \begin{cfa}
-	int n = @42@;
-	array(float, n) x;
-	array(float, 999) * xp = x; // static rejection here
-	(*xp)[@500@]; // runtime check vs len 999
-\end{cfa}
-
-% TODO: kill the vertical whitespace around these lists
-% nothing from https://stackoverflow.com/questions/1061112/eliminate-space-before-beginitemize is working
-
-The way the \CFA array is implemented,
-the type analysis of this \CFA case reduces to a case similar to the earlier C version.
+int n = @42@;
+array(float, n) x;
+array(float, 999) * xp = x; $\C{// static rejection here}$
+(*xp)[@500@]; $\C{// runtime check vs len 999}$
+\end{cfa}
+The way the \CFA array is implemented, the type analysis of this case reduces to a case similar to the earlier C version.
 The \CFA compiler's compatibility analysis proceeds as:
-\begin{itemize}[noitemsep,partopsep=-\parskip,parsep=0pt,leftmargin=4em]
+\begin{itemize}[parsep=0pt]
 \item
 	Is @array(float, 999)@ type-compatible with @array(float, n)@?
 \item
-	Is @arrayX(float, char[999])@ type-compatible with @arrayX(float, char[n])@?
-	\footnote{Here, \lstinline{arrayX} represents the type that results
+	Is @arrayX(float, char[999])@ type-compatible with @arrayX(float, char[n])@?\footnote{
+		Here, \lstinline{arrayX} represents the type that results
 		from desugaring the \lstinline{array} type
 		into a type whose generic parameters are all types.
@@ -531,9 +499,5 @@
 	Is @char[999]@ type-compatible with @char[n]@?
 \end{itemize}
-
-I chose to achieve the necessary rejection of the \CFA case
-by adding a rejection of the corresponding C case.
-
-This decision is not backward compatible.
+To achieve the necessary \CFA rejections meant rejecting the corresponding C case, which is not backward compatible.
 There are two complementary mitigations for this incompatibility.
 
@@ -542,9 +506,9 @@
 This situation might arise if @n@ were known to be 999,
 rather than 42, as in the introductory examples.
-The programmer can add a cast, as in:
-\begin{cfa}
-	xp = ( float (*)[999] ) & x;
-\end{cfa}
-This addition causes \CFA to accept, beacause now, the programmer has accepted blame.
+The programmer can add a cast in the \CFA code.
+\begin{cfa}
+xp = @(float (*)[999])@ &x;
+\end{cfa}
+This addition causes \CFA to accept, because now, the programmer has accepted blame.
 This addition is benign in plain C, because the cast is valid, just unnecessary there.
 Moreover, the addition can even be seen as appropriate ``eye candy,''
@@ -556,15 +520,14 @@
 Second, the incompatibility only affects types like pointer-to-array,
 which are are infrequently used in C.
-The more common C idiom for aliasing an array is to use the pointer-to-first-element type,
-which does not participate in the \CFA array's length checking.
-\footnote{Notably, the desugaring of the \lstinline{array@} type,
-	avoids letting any \lstinline{-[-]} type decay,
-	in order to preserve the length information that powers runtime bound checking.}
-Therefore, the frequency of needing to upgrade wild C code (as discussed in the first mitigation)
+The more common C idiom for aliasing an array is to use a pointer-to-first-element type,
+which does not participate in the \CFA array's length checking.\footnote{
+	Notably, the desugaring of the \lstinline{array} type avoids letting any \lstinline{-[-]} type decay,
+	in order to preserve the length information that powers runtime bound-checking.}
+Therefore, the frequency of needing to upgrade legacy C code (as discussed in the first mitigation)
 is anticipated to be low.
 
 Because the incompatibility represents a low cost to a \CFA onboarding effort
 (with a plausible side benefit of linting the original code for a missing annotation),
-I elected not to add special measures to retain the compatibility.
+no special measures were added to retain the compatibility.
 It would be possible to flag occurrences of @-[-]@ types that come from @array@ desugaring,
 treating those with stricter \CFA rules, while treating others with classic C rules.
@@ -573,10 +536,10 @@
 
 Having allowed that both the initial C example's check
-\begin{itemize}[noitemsep,partopsep=-\parskip,parsep=0pt,leftmargin=4em]
+\begin{itemize}
 	\item
 		Is @float[999]@ type-compatible with @float[n]@?
 \end{itemize}
-and the second \CFA exmple's induced check
-\begin{itemize}[noitemsep,partopsep=-\parskip,parsep=0pt,leftmargin=4em]
+and the second \CFA example's induced check
+\begin{itemize}
 	\item
 		Is @char[999]@ type-compatible with @char[n]@?
@@ -587,11 +550,11 @@
 To implement the new \CFA rules, I took the syntactic recursion a step further, obtaining,
 in both cases:
-\begin{itemize}[noitemsep,partopsep=-\parskip,parsep=0pt,leftmargin=4em]
+\begin{itemize}
 	\item
-		Is @999@ TBD-compatible with @n@?
+		Is @999@ compatible with @n@?
 \end{itemize}
-This compatibility question applies to a pair of expressions, where the earlier ones were to types.
+This compatibility question applies to a pair of expressions, where the earlier implementation were to types.
 Such an expression-compatibility question is a new addition to the \CFA compiler.
-These questions only arise in the context of dimension expressions on (C) array types.
+Note, these questions only arise in the context of dimension expressions on (C) array types.
 
 TODO: ensure these compiler implementation matters are treated under \CFA compiler background:
@@ -600,6 +563,5 @@
 GenPoly.
 
-The relevant technical component of the \CFA compiler is,
-within the type resolver, the type unification procedure.
+The relevant technical component of the \CFA compiler is the type unification procedure within the type resolver.
 I added rules for continuing this unification into expressions that occur within types.
 It is still fundamentally doing \emph{type} unification
@@ -607,5 +569,4 @@
 and not participating in binding any variables that stand in for expression fragments
 (for there is no such sort of variable in \CFA's analysis.)
-
 An unfortunate fact about the \CFA compiler's preexisting implementation is that
 type unification suffers from two forms of duplication.
@@ -613,13 +574,12 @@
 The first duplication has (many of) the unification rules stated twice.
 As a result, my additions for dimension expressions are stated twice.
-The extra statement of the rules occurs in the GenPoly module,
+The extra statement of the rules occurs in the @GenPoly@ module,
 where concrete types like @array(int, 5)@\footnote{
 	Again, the presentation is simplified
-	by leaving the \lstinline{array} macro unexpanded}
+	by leaving the \lstinline{array} macro unexpanded.}
 are lowered into corresponding C types @struct __conc_array_1234@ (the suffix being a generated index).
-In this case, the struct's definition gives fields that hardcode the argument values of @float@ and @5@.
-The next time an @array(-,-)@ concrete instance is encountered,
-is the previous @struct __conc_array_1234@ suitable for it?
-Yes, for another occurrance of @array(int, 5)@;
+In this case, the struct's definition contains fields that hardcode the argument values of @float@ and @5@.
+The next time an @array(-,-)@ concrete instance is encountered, it checks if the previous @struct __conc_array_1234@ is suitable for it.
+Yes, for another occurrence of @array(int, 5)@;
 no, for either @array(rational(int), 5)@ or @array(int, 42)@.
 By the last example, this phase must ``reject''
@@ -630,13 +590,13 @@
 In the program
 \begin{cfa}
-	void f( double );
-	forall( T & ) void f( T & );
-	void g( int n ) {
-		array( float, n + 1 ) x;
-		f(x);
-	}
-\end{cfa}
-when resolving the function call, the first unification stage
-compares the types @T@, of the parameter, with @array( float, n + 1 )@, of the argument.
+void @f@( double );
+forall( T & ) void @f@( T & );
+void g( int n ) {
+	array( float, n + 1 ) x;
+	f(x);   // overloaded
+}
+\end{cfa}
+when resolving the function call, @g@, the first unification stage
+compares the type @T@ of the parameter with @array( float, n + 1 )@, of the argument.
 TODO: finish.
 
@@ -647,12 +607,11 @@
 	TODO: Deal with directionality, that I'm doing exact-match, no ``at least as long as,'' no subtyping.
 	Should it be an earlier scoping principle?  Feels like it should matter in more places than here.}
-So, a ``yes'' answer must represent a guarantee that both expressions will evaluate the
-same result, while a ``no'' can tolerate ``they might, but we're not sure,'
+So, a ``yes'' answer must represent a guarantee that both expressions evaluate the
+same result, while a ``no'' can tolerate ``they might, but we're not sure'',
 provided that practical recourses are available
-to let programmers express their better knowledge.
-The specific rule-set that I offer with the current release is, in fact, extremely conservative.
+to let programmers express better knowledge.
+The new rule-set in the current release is, in fact, extremely conservative.
 I chose to keep things simple,
-and allow real future needs do drive adding additional complexity,
-within the framework that I laid out.
+and allow future needs to drive adding additional complexity, within the new framework.
 
 For starters, the original motivating example's rejection
@@ -662,81 +621,82 @@
 Rather, the analysis assumes a variable's value can be anything,
 and so there can be no guarantee that its value is 999.
-So, a variable use and a literal can never match.
+So, a variable and a literal can never match.
 
 Two occurrences of the same literal value are obviously a fine match.
-For two occurrences of the same varialbe, more information is needed.
+For two occurrences of the same variable, more information is needed.
 For example, this one is fine
 \begin{cfa}
-	void f( const int n ) {
-		float x[n];
-		float (*xp)[n] = x; // accept
-	}
+void f( const int n ) {
+	float x[n];
+	float (*xp)[n] = x;   // accept
+}
 \end{cfa}
 while this one is not:
 \begin{cfa}
-	void f() {
-		int n = 42;
-		float x[n];
-		n = 999;
-		float (*xp)[n] = x; // reject
-	}
+void f() {
+	int n = 42;
+	float x[n];
+	n = 999;
+	float (*xp)[n] = x;   // reject
+}
 \end{cfa}
 Furthermore, the fact that the first example sees @n@ as @const@
-is not actually a sufficent basis.
+is not actually sufficient.
 In this example, @f@'s length expression's declaration is as @const@ as it can be,
 yet its value still changes between the two invocations:
-\begin{cfa}
-	// compile unit 1
-	void g();
-	void f( const int & const nr ) {
-		float x[nr];
-		g();
-		float (*xp)[nr] = x; // reject
-	}
-	// compile unit 2
-	static int n = 42;
-	void g() {
-		n = 99;
-	}
-	void f( const int & );
-	int main () {
-		f(n);
-		return 0;
-	}
-\end{cfa}
-The issue in this last case is,
-just because you aren't able to change something doesn't mean someone else can't.
-
-My rule set also respects a feature of the C tradition.
-In spite of the several limitations of the C rules
+\begin{cquote}
+\setlength{\tabcolsep}{15pt}
+\begin{tabular}{@{}ll@{}}
+\begin{cfa}
+// compile unit 1
+void g();
+void f( const int & const nr ) {
+	float x[nr];
+	g();    // change n
+	@float (*xp)[nr] = x;@   // reject
+}
+\end{cfa}
+&
+\begin{cfa}
+// compile unit 2
+static int n = 42;
+void g() {
+	n = 99;
+}
+
+f( n );
+\end{cfa}
+\end{tabular}
+\end{cquote}
+The issue here is that knowledge needed to make a correct decision is hidden by separate compilation.
+Even within a translation unit, static analysis might not be able to provide all the information.
+
+My rule set also respects a traditional C feature: In spite of the several limitations of the C rules
 accepting cases that produce different values, there are a few mismatches that C stops.
-C is quite precise when working with two static values:
-\begin{cfa}
-	enum { fortytwo = 42 };
-	float x[fortytwo];
-	float (*xp1)[42] = &x; // accept
-	float (*xp2)[999] = &x; // reject
+C is quite precise when working with two static values.
+\begin{cfa}
+enum { fortytwo = 42 };
+float x[fortytwo];
+float (*xp1)[42] = &x;    // accept
+float (*xp2)[999] = &x;   // reject
 \end{cfa}
 My \CFA rules agree with C's on these cases.
 
-My rules classify expressions into three groups:
+In summary, the new rules classify expressions into three groups:
 \begin{description}
 \item[Statically Evaluable]
 	Expressions for which a specific value can be calculated (conservatively)
 	at compile-time.
-	A preexisting \CFA compiler module defines which expressions qualify,
+	A preexisting \CFA compiler module defines which literals, enumerators, and expressions qualify,
 	and evaluates them.
-	Includes literals and enumeration values.
 \item[Dynamic but Stable]
-	The value of a variable declared as @const@.
-	Includes a @const@ parameter.
+	The value of a variable declared as @const@, including a @const@ parameter.
 \item[Potentially Unstable]
 	The catch-all category.  Notable examples include:
-	any function-call result (@float x[foo()];@),
-	the particular function-call result that is a pointer dereference (@void f(const int * n) { float x[*n]; }@), and
+	any function-call result, @float x[foo()];@,
+	the particular function-call result that is a pointer dereference, @void f(const int * n)@ @{ float x[*n]; }@, and
 	any use of a reference-typed variable.
 \end{description}
-
-My \CFA rules are:
+Within these groups, my \CFA rules are:
 \begin{itemize}
 \item
@@ -744,11 +704,9 @@
 	Notably, this rule allows a literal to match with an enumeration value, based on the value.
 \item
-	Accept a Dynamic but Stable pair, if both expressions are written out the same, e.g. refers to same variable declaration.
+	Accept a Dynamic but Stable pair, if both expressions are written out the same, \eg refers to the same variable declaration.
 \item
 	Otherwise, reject.
-	Notably, reject all pairs from the Potentially Unstable group.
-	Notably, reject all pairs that cross groups.
+	Notably, reject all pairs from the Potentially Unstable group and all pairs that cross groups.
 \end{itemize}
-
 The traditional C rules are:
 \begin{itemize}
@@ -759,10 +717,10 @@
 \end{itemize}
 
-
-\newcommand{\falsealarm}{{\color{orange}\small{*}}}
-\newcommand{\allowmisuse}{{\color{red}\textbf{!}}}
-\newcommand{\cmark}{\ding{51}} % from pifont
-\newcommand{\xmark}{\ding{55}}
 \begin{figure}
+	\newcommand{\falsealarm}{{\color{blue}\small{*}}}
+	\newcommand{\allowmisuse}{{\color{red}\textbf{!}}}
+	\newcommand{\cmark}{\ding{51}} % from pifont
+	\newcommand{\xmark}{\ding{55}}
+
 	\begin{tabular}{@{}l@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c}
 	 & \multicolumn{2}{c}{\underline{Values Equal}}
@@ -778,18 +736,19 @@
 	\end{tabular}
 
-	\vspace{12pt}
-	\noindent\textbf{Legend:}
-	\begin{itemize}
+	\medskip
+	\noindent\textbf{Legend}
+	\begin{itemize}[leftmargin=*]
 	\item
 		Each row gives the treatment of a test harness of the form
 		\begin{cfa}
-			float x[ expr1 ];
-			float (*xp)[ expr2 ] = &x;
+		float x[ expr1 ];
+		float (*xp)[ expr2 ] = &x;
 		\end{cfa}
-		where \lstinline{expr1} and \lstinline{expr2} are metavariables varying according to the row's Case.
+		\vspace*{-10pt}
+		where \lstinline{expr1} and \lstinline{expr2} are meta-variables varying according to the row's Case.
 		Each row's claim applies to other harnesses too, including,
 		\begin{itemize}
 		\item
-			calling a function with a paramter like \lstinline{x} and an argument of the \lstinline{xp} type,
+			calling a function with a parameter like \lstinline{x} and an argument of the \lstinline{xp} type,
 		\item
 			assignment in place of initialization,
@@ -801,8 +760,8 @@
 	\item
 		Each case's claim is symmetric (swapping \lstinline{expr1} with \lstinline{expr2} has no effect),
-		even though most test harnesses are asymetric.
+		even though most test harnesses are asymmetric.
 	\item
 		The table treats symbolic identity (Same/Different on rows)
-		apart from value eqality (Equal/Unequal on columns).
+		apart from value equality (Equal/Unequal on columns).
 		\begin{itemize}
 		\item
@@ -819,6 +778,6 @@
 		while every Accept under Values Unequal is an allowed misuse (\allowmisuse).
 	\end{itemize}
-	\caption{Case comparison for array type compatibility, given pairs of dimension expressions.
-		TODO: get Peter's LaTeX help on overall appearance, probably including column spacing/centering and bullet indentation.}
+
+	\caption{Case comparison for array type compatibility, given pairs of dimension expressions.}
 	\label{f:DimexprRuleCompare}
 \end{figure}
@@ -826,6 +785,6 @@
 
 Figure~\ref{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
-It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafely.
-It also shows that C-incompatibilities only occur in cases that C treats unsafely.
+It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafe.
+It also shows that C-incompatibilities only occur in cases that C treats unsafe.
 
 
@@ -837,25 +796,25 @@
 whose reuses are rejected by the blunt current-state rules:
 \begin{cfa}
-	void f( int & nr, const int nv ) {
-		float x[nr];
-		float (*xp)[nr] = & x; // reject: nr varying (no references)
-		float y[nv + 1];
-		float (*yp)[nv + 1] = & y; // reject: ?+? unpredicable (no functions)
-	}
+void f( int & nr, const int nv ) {
+	float x[nr];
+	float (*xp)[nr] = &x;   // reject: nr varying (no references)
+	float y[nv + 1];
+	float (*yp)[nv + 1] = &y;   // reject: ?+? unpredictable (no functions)
+}
 \end{cfa}
 Yet, both dimension expressions are reused safely.
-(The @nr@ reference is never written, not volatile
+The @nr@ reference is never written, not volatile
 and control does not leave the function between the uses.
-The name @?+?@ resolves to a function that is quite predictable.)
-The programmer here can add the constant declarations:
-\begin{cfa}
-	void f( int & nr, const int nv ) {
-		@const int nx@ = nr;
-		float x[nx];
-		float (*xp)[nx] = & x; // acept
-		@const int ny@ = nv + 1;
-		float y[ny];
-		float (*yp)[ny] = & y; // accept
-	}
+The name @?+?@ resolves to a function that is quite predictable.
+Here, the programmer can add the constant declarations (cast does not work):
+\begin{cfa}
+void f( int & nr, const int nv ) {
+	@const int nx@ = nr;
+	float x[nx];
+	float (*xp)[nx] = & x;   // accept
+	@const int ny@ = nv + 1;
+	float y[ny];
+	float (*yp)[ny] = & y;   // accept
+}
 \end{cfa}
 The result is the originally intended semantics,
@@ -863,8 +822,8 @@
 
 The snapshotting trick is also used by the translation, though to achieve a different outcome.
-Rather obviously, every array must be subscriptable, even a bizzarre one:
-\begin{cfa}
-	array( float, rand(10) ) x;
-	x[0];  // 10% chance of bound-check failure
+Rather obviously, every array must be subscriptable, even a bizarre one:
+\begin{cfa}
+array( float, rand(10) ) x;
+x[0];  // 10% chance of bound-check failure
 \end{cfa}
 Less obvious is that the mechanism of subscripting is a function call,
@@ -874,175 +833,33 @@
 Adjusting the example to make the function's use of length more explicit:
 \begin{cfa}
-	forall ( T * )
-	void f( T * x ) { sout | sizeof(*x); }
-	float x[ rand(10) ];
-	f( x );
+forall ( T * )
+void f( T * x ) { sout | sizeof(*x); }
+float x[ rand(10) ];
+f( x );
 \end{cfa}
 Considering that the partly translated function declaration is, loosely,
 \begin{cfa}
-	void f( size_t __sizeof_T, void * x ) { sout | __sizeof_T; }
-\end{cfa}
-the translated call must not go like:
-\begin{cfa}
-	float x[ rand(10) ];
-	f( rand(10), &x );
-\end{cfa}
-Rather, its actual translation is like:
-\begin{cfa}
-	size_t __dim_x = rand(10);
-	float x[ __dim_x ];
-	f( __dim_x, &x );
-\end{cfa}
-The occurrence of this dimension hoisting during translation was present in the preexisting \CFA compiler.
-But its cases were buggy, particularly with determining, ``Can hoisting be skipped here?''
-For skipping this hoisting is clearly desirable in some cases,
-not the least of which is when the programmer has already done so manually.
-My work includes getting these cases right, harmonized with the accept/reject criteria, and tested.
-
-
+void f( size_t __sizeof_T, void * x ) { sout | __sizeof_T; }
+\end{cfa}
+the translation must call the dimension argument twice:
+\begin{cfa}
+float x[ rand(10) ];
+f( rand(10), &x );
+\end{cfa}
+Rather, the translation is:
+\begin{cfa}
+size_t __dim_x = rand(10);
+float x[ __dim_x ];
+f( __dim_x, &x );
+\end{cfa}
+The occurrence of this dimension hoisting during translation was in the preexisting \CFA compiler.
+But its cases were buggy, particularly with determining, ``Can hoisting the expression be skipped here?'', for skipping this hoisting is clearly desirable in some cases.
+For example, when the programmer has already done so manually. \PAB{I don't know what this means.}
+In the new implementation, these cases are correct, harmonized with the accept/reject criteria.
 
 TODO: Discuss the interaction of this dimension hoisting with the challenge of extra unification for cost calculation
 
 
-\section{Multidimensional Arrays}
-\label{toc:mdimpl}
-
-% TODO: introduce multidimensional array feature and approaches
-
-When working with arrays, \eg linear algebra, array dimensions are referred to as ``rows'' and ``columns'' for a matrix, adding ``planes'' for a cube.
-(There is little terminology for higher dimensional arrays.)
-For example, an acrostic poem\footnote{A type of poetry where the first, last or other letters in a line spell out a particular word or phrase in a vertical column.}
-can be treated as a grid of characters, where the rows are the text and the columns are the embedded keyword(s).
-Within a poem, there is the concept of a \newterm{slice}, \eg a row is a slice for the poem text, a column is a slice for a keyword.
-In general, the dimensioning and subscripting for multidimensional arrays has two syntactic forms: @m[r,c]@ or @m[r][c]@.
-
-Commonly, an array, matrix, or cube, is visualized (especially in mathematics) as a contiguous row, rectangle, or block.
-This conceptualization is reenforced by subscript ordering, \eg $m_{r,c}$ for a matrix and $c_{p,r,c}$ for a cube.
-Few programming languages differ from the mathematical subscript ordering.
-However, computer memory is flat, and hence, array forms are structured in memory as appropriate for the runtime system.
-The closest representation to the conceptual visualization is for an array object to be contiguous, and the language structures this memory using pointer arithmetic to access the values using various subscripts.
-This approach still has degrees of layout freedom, such as row or column major order, \ie juxtaposed rows or columns in memory, even when the subscript order remains fixed.
-For example, programming languages like MATLAB, Fortran, Julia and R store matrices in column-major order since they are commonly used for processing column-vectors in tabular data sets but retain row-major subscripting.
-In general, storage layout is hidden by subscripting, and only appears when passing arrays among different programming languages or accessing specific hardware.
-
-\VRef[Figure]{f:FixedVariable} shows two C90 approaches for manipulating a contiguous matrix.
-Note, C90 does not support VLAs.
-The fixed-dimension approach (left) uses the type system;
-however, it requires all dimensions except the first to be specified at compile time, \eg @m[][6]@, allowing all subscripting stride calculations to be generated with constants.
-Hence, every matrix passed to @fp1@ must have exactly 6 columns but the row size can vary.
-The variable-dimension approach (right) ignores (violates) the type system, \ie argument and parameters types do not match, and subscripting is performed manually using pointer arithmetic in the macro @sub@.
-
-\begin{figure}
-\begin{tabular}{@{}l@{\hspace{40pt}}l@{}}
-\multicolumn{1}{c}{\textbf{Fixed Dimension}} & \multicolumn{1}{c}{\textbf{Variable Dimension}} \\
-\begin{cfa}
-
-void fp1( int rows, int m[][@6@] ) {
-	...  printf( "%d ", @m[r][c]@ );  ...
-}
-int fm1[4][@6@], fm2[6][@6@]; // no VLA
-// initialize matrixes
-fp1( 4, fm1 ); // implicit 6 columns
-fp1( 6, fm2 );
-\end{cfa}
-&
-\begin{cfa}
-#define sub( m, r, c ) *(m + r * sizeof( m[0] ) + c)
-void fp2( int rows, int cols, int *m ) {
-	...  printf( "%d ", @sub( m, r, c )@ );  ...
-}
-int vm1[@4@][@4@], vm2[@6@][@8@]; // no VLA
-// initialize matrixes
-fp2( 4, 4, vm1 );
-fp2( 6, 8, vm2 );
-\end{cfa}
-\end{tabular}
-\caption{C90 Fixed \vs Variable Contiguous Matrix Styles}
-\label{f:FixedVariable}
-\end{figure}
-
-Many languages allow multidimensional arrays-of-arrays, \eg in Pascal or \CC.
-\begin{cquote}
-\begin{tabular}{@{}ll@{}}
-\begin{pascal}
-var m : array[0..4, 0..4] of Integer;  (* matrix *)
-type AT = array[0..4] of Integer;  (* array type *)
-type MT = array[0..4] of AT;  (* array of array type *)
-var aa : MT;  (* array of array variable *)
-m@[1][2]@ := 1;   aa@[1][2]@ := 1 (* same subscripting *)
-\end{pascal}
-&
-\begin{c++}
-int m[5][5];
-
-typedef vector< vector<int> > MT;
-MT vm( 5, vector<int>( 5 ) );
-m@[1][2]@ = 1;  aa@[1][2]@ = 1;
-\end{c++}
-\end{tabular}
-\end{cquote}
-The language decides if the matrix and array-of-array are laid out the same or differently.
-For example, an array-of-array may be an array of row pointers to arrays of columns, so the rows may not be contiguous in memory nor even the same length (triangular matrix).
-Regardless, there is usually a uniform subscripting syntax masking the memory layout, even though a language could differentiated between the two forms using subscript syntax, \eg @m[1,2]@ \vs @aa[1][2]@.
-Nevertheless, controlling memory layout can make a difference in what operations are allowed and in performance (caching/NUMA effects).
-
-C also provides non-contiguous arrays-of-arrays.
-\begin{cfa}
-int m[5][5];							$\C{// contiguous}$
-int * aa[5];							$\C{// non-contiguous}$
-\end{cfa}
-both with different memory layout using the same subscripting, and both with different degrees of issues.
-The focus of this work is on the contiguous multidimensional arrays in C.
-The reason is that programmers are often forced to use the more complex array-of-array form when a contiguous array would be simpler, faster, and safer.
-Nevertheless, the C array-of-array form is still important for special circumstances.
-
-\VRef[Figure]{f:ContiguousNon-contiguous} shows the extensions made in C99 for manipulating contiguous \vs non-contiguous arrays.\footnote{C90 also supported non-contiguous arrays.}
-First, VLAs are supported.
-Second, for contiguous arrays, C99 conjoins one or more of the parameters as a downstream dimension(s), \eg @cols@, implicitly using this parameter to compute the row stride of @m@.
-If the declaration of @fc@ is changed to:
-\begin{cfa}
-void fc( int rows, int cols, int m[@rows@][@cols@] ) ...
-\end{cfa}
-it is possible for C to perform bound checking across all subscripting, but it does not.
-While this contiguous-array capability is a step forward, it is still the programmer's responsibility to manually manage the number of dimensions and their sizes, both at the function definition and call sites.
-That is, the array does not automatically carry its structure and sizes for use in computing subscripts.
-While the non-contiguous style in @faa@ looks very similar to @fc@, the compiler only understands the unknown-sized array of row pointers, and it relies on the programmer to traverse the columns in a row correctly with a correctly bounded loop index.
-Specifically, there is no requirement that the rows are the same length, like a poem with different length lines.
-
-\begin{figure}
-\begin{tabular}{@{}ll@{}}
-\multicolumn{1}{c}{\textbf{Contiguous}} & \multicolumn{1}{c}{\textbf{ Non-contiguous}} \\
-\begin{cfa}
-void fc( int rows, @int cols@, int m[ /* rows */ ][@cols@] ) {
-	...  printf( "%d ", @m[r][c]@ );  ...
-}
-int m@[5][5]@;
-for ( int r = 0; r < 5; r += 1 ) {
-
-	for ( int c = 0; c < 5; c += 1 )
-		m[r][c] = r + c;
-}
-fc( 5, 5, m );
-\end{cfa}
-&
-\begin{cfa}
-void faa( int rows, int cols, int * m[ @/* cols */@ ] ) {
-	...  printf( "%d ", @m[r][c]@ );  ...
-}
-int @* aa[5]@;  // row pointers
-for ( int r = 0; r < 5; r += 1 ) {
-	@aa[r] = malloc( 5 * sizeof(int) );@ // create rows
-	for ( int c = 0; c < 5; c += 1 )
-		aa[r][c] = r + c;
-}
-faa( 5, 5, aa );
-\end{cfa}
-\end{tabular}
-\caption{C99 Contiguous \vs Non-contiguous Matrix Styles}
-\label{f:ContiguousNon-contiguous}
-\end{figure}
-
-
-\subsection{Multidimensional array implementation}
+\section{Multidimensional array implementation}
 \label{s:ArrayMdImpl}
 
@@ -1221,5 +1038,5 @@
 	S & | sized(S),			$\C{// masquerading-as}$
 	Timmed &,				$\C{// immediate element, often another array}$
-	Tbase &					$\C{// base element, e.g. float, never array}$
+	Tbase &					$\C{// base element, \eg float, never array}$
 ) { // distribute forall to each element
 	struct arpk {
Index: doc/theses/mike_brooks_MMath/background.tex
===================================================================
--- doc/theses/mike_brooks_MMath/background.tex	(revision ad9f5931463621e55b660fd57101ba749263b146)
+++ doc/theses/mike_brooks_MMath/background.tex	(revision c3e41cda7b7a639338faa16c005b96ed95202da9)
@@ -178,5 +178,5 @@
 \lstinput{34-34}{bkgd-carray-arrty.c}
 The inspection begins by using @sizeof@ to provide program semantics for the intuition of an expression's type.
-An architecture with 64-bit pointer size is used, to keep irrelevant details fixed.
+An architecture with 64-bit pointer size is used, to remove irrelevant details.
 \lstinput{35-36}{bkgd-carray-arrty.c}
 Now consider the @sizeof@ expressions derived from @ar@, modified by adding pointer-to and first-element (and including unnecessary parentheses to avoid any confusion about precedence).
@@ -215,5 +215,5 @@
 
 My observation is recognizing:
-\begin{itemize}[leftmargin=*,topsep=0pt,itemsep=0pt]
+\begin{itemize}[leftmargin=*,itemsep=0pt]
 	\item There is value in using a type that knows its size.
 	\item The type pointer to the (first) element does not.
@@ -302,5 +302,5 @@
 
 In summary, when a function is written with an array-typed parameter,
-\begin{itemize}[leftmargin=*,topsep=0pt]
+\begin{itemize}[leftmargin=*]
 	\item an appearance of passing an array by value is always an incorrect understanding,
 	\item a dimension value, if any is present, is ignored,
@@ -532,31 +532,34 @@
 \subsection{Array Parameter Declaration}
 
-Passing an array along with a function call is obviously useful.
-Let us say that a parameter is an array parameter when the called function intends to subscript it.
-This section asserts that a more satisfactory/formal characterization does not exist in C, surveys the ways that C API authors communicate ``@p@ has zero or more @T@s,'' and calls out the minority cases where the C type system is using or verifying such claims.
-
-A C function's parameter declarations look different, from the caller's and callee's perspectives.
+Passing an array as an argument to a function is necessary.
+Assume a parameter is an array when the function intends to subscript it.
+This section asserts that a more satisfactory/formal characterization does not exist in C, surveys the ways that C API authors communicate ``@p@ has zero or more dimensions'' and calls out the minority cases where the C type system is using or verifying such claims.
+
+A C parameter declarations look different, from the caller's and callee's perspectives.
 Both perspectives consist of the text read by a programmer and the semantics enforced by the type system.
-The caller's perspecitve is available from a mere function declaration (which allow definition-before-use and separate compilation), but can also be read from (the non-body part of) a function definition.
+The caller's perspective is available from a function declaration, which allow definition-before-use and separate compilation, but can also be read from (the non-body part of) a function definition.
 The callee's perspective is what is available inside the function.
 \begin{cfa}
-	int foo( int, float, char );				$\C{// declaration, names optional}$
-	int bar( int i, float f, char c ) { 		$\C{// definition, names mandatory}$
-		$/* caller's perspective of foo's; callee's perspective of bar's */$
-		...
-	}
-	$/* caller's persepectives of foo's and bar's */$
-\end{cfa}
-The caller's perspective is more limited.
-The example shows, so far, that parameter names (by virtue of being optional) are really comments in the caller's perspective, while they are semantically significant in the callee's perspective.
+int foo( int, float, char );				$\C{// declaration, names optional}$
+int bar( int i, float f, char c ) { 		$\C{// definition, names mandatory}$
+	// caller's perspective of foo; callee's perspective of bar
+}
+// caller's perspectives of foo's and bar's
+\end{cfa}
+In caller's perspective, the parameter names (by virtue of being optional) are really comments;
+in the callee's perspective, parameter names are semantically significant.
 Array parameters introduce a further, subtle, semantic difference and considerable freedom to comment.
 
-At the semantic level, there is no such thing as an array parameter, except for one case (@T[static 5]@) discussed shortly.
+At the semantic level, there is no such thing as an array parameter, except for one case (@T [static 5]@) discussed shortly.
 Rather, there are only pointer parameters.
-This fact probably shares considerable responsibility for the common sense of ``an array is just a pointer,'' wich has been refuted in non-parameter contexts.
+This fact probably shares considerable responsibility for the common sense of ``an array is just a pointer,'' which has been refuted in non-parameter contexts.
 This fact holds in both the caller's and callee's perspectives.
-However, a parameter's type can include ``array of.''
-For example, the type ``pointer to array of 5 ints'' (@T(*)[5]@) is a pointer type, a fully meaningful parameter type (in the sense that this description does not contain any information that the type system ignores), and a type that appears the same in the caller's \vs callee's perspectives.
-The outermost type constructor (syntactically first dimension) is really the one that determines the flavour of parameter.
+However, a parameter's type can include ``array of.'', \eg the type ``pointer to array of 5 ints'' (@T (*)[5]@) is a pointer type.
+This type is fully meaningful in the sense that its description does not contain any information that the type system ignores, and the type appears the same in the caller's \vs callee's perspectives.
+In fact, the outermost type constructor (syntactically first dimension) is really the one that determines the flavour of parameter.
+
+Yet, C allows array syntax for the outermost type constructor, from which comes the freedom to comment.
+An array parameter declaration can specify the outermost dimension with a dimension value, @[10]@ (which is ignored), an empty dimension list, @[ ]@, or a pointer, @*@, as seen in \VRef[Figure]{f:ArParmEquivDecl}.
+The rationale for rejecting the first ``invalid'' row follows shortly, while the second ``invalid'' row is simple nonsense, included to complete the pattern; its syntax hints at what the final row actually achieves.
 
 \begin{figure}
@@ -596,20 +599,30 @@
 \end{tabular}
 \end{cquote}
-\caption{Multiple ways to declare an arrray parameter.  Across a valid row, every declaration is equivalent.  Each column gives a declaration style.  Really, the style can be read from the first row only.  The second row shows how the style extends to multiple dimensions, with the rows thereafter providing context for the choice of which second-row \lstinline{[]}receives the column-style variation.}
+\caption{Multiple ways to declare an array parameter.
+Across a valid row, every declaration is equivalent.
+Each column gives a declaration style, where the style for that column is read from the first row.
+The second row begins the style for multiple dimensions, with the rows thereafter providing context for the choice of which second-row \lstinline{[]} receives the column-style variation.}
 \label{f:ArParmEquivDecl}
 \end{figure}
 
-Yet, C allows array syntax for the outermost type constructor, from which comes the freedom to comment.
-An array parameter declaration can specify the outermost dimension with a dimension value, @[10]@ (which is ignored), an empty dimension list, @[ ]@, or a pointer, @*@, as seen in \VRef[Figure]{f:ArParmEquivDecl}.  The rationale for rejecting the first ``invalid'' row follows shortly, while the second ``invalid'' row is simple nonsense, included to complete the pattern; its syntax hints at what the final row actually achieves.
-
-In the lefmost style, the typechecker ignores the actual value in most practical cases.
-This value is allowed to be a dynamic expression, so it is \emph{possible} to use the leftmost style in many practical cases.
+In the leftmost style, the typechecker ignores the actual value in most practical cases.
+This value is allowed to be a dynamic expression, and then it has practical cases.
+\begin{cfa}
+void foo( int @n@ ) {
+	float _42( float @a[n]@ ) {    // nested function
+		a[0] = 42;
+	}
+	float b[n];
+	_42( b );
+}
+\end{cfa}
+
 
 % To help contextualize the matrix part of this example, the syntaxes @float [5][]@, @float [][]@ and @float (*)[]@ are all rejected, for reasons discussed shortly.
 % So are @float[5]*@, @float[]*@ and @float (*)*@.  These latter ones are simply nonsense, though they hint at ``1d array of pointers'', whose equivalent syntax options are, @float *[5]@, @float *[]@, and @float **@.
 
-It is a matter of taste as to whether a programmer should use a form as far left as possible (getting the most out of syntactically integrated comments), sticking to the right (avoiding false comfort from suggesting the typechecker is checking more than it is), or compromising in the middle (reducing unchecked information, yet clearly stating, ``I will subscript this one'').
-
-Note that this equivalence of pointer and array declarations is special to paramters.
+It is a matter of taste as to whether a programmer should use a form as far left as possible (getting the most out of possible subscripting and dimension sizes), sticking to the right (avoiding false comfort from suggesting the typechecker is checking more than it is), or compromising in the middle (reducing unchecked information, yet clearly stating, ``I will subscript).
+
+Note that this equivalence of pointer and array declarations is special to parameters.
 It does not apply to local variables, where true array declarations are possible.
 \begin{cfa}
@@ -626,5 +639,5 @@
 float sum( float v[] );
 float arg = 3.14;
-sum( &arg );								$\C{// accepted, v := \&arg}$
+sum( &arg );								$\C{// accepted, v = \&arg}$
 \end{cfa}
 
@@ -674,4 +687,5 @@
 The last observation is a fact of the callee's perspective.
 There is little type-system checking, in the caller's perspective, that what is being passed, matches.
+\PAB{I do not understand}
 \begin{cfa}
 void f( float [][10] );
@@ -680,8 +694,22 @@
 f(&a); // reject
 f(&b); // accept
+
+void foo() {
+	void f( float [][10] );
+	int n = 100;
+	float a[100], b[3][12], c[n], d[n][n];
+	f( a );    // reject
+	f( b );    // reject
+	f( c );    // reject
+	f( d );    // accept
+	f( &a );   // reject
+	f( &b );   // reject
+	f( &c );   // accept
+	f( &d );   // reject
+}
 \end{cfa}
 This size is therefore, a callee's assumption.
 
-Finally, to handle higher-dimensional VLAs, C repurposed the @*@ \emph{within} the dimension in a declaration to mean that the callee will have make an assumption about the size here, but no (unchecked, possibly wrong) information about this assumption is included for the caller-programmer's benefit/overconfidence.
+Finally, to handle higher-dimensional VLAs, C repurposed the @*@ \emph{within} the dimension in a declaration to mean that the callee has make an assumption about the size, but no (unchecked, possibly wrong) information about this assumption is included for the caller-programmer's benefit/over-confidence.
 \begin{cquote}
 @[@ \textit{type-qualifier-list$_{opt}$} @* ]@
Index: doc/theses/mike_brooks_MMath/programs/hello-accordion.cfa
===================================================================
--- doc/theses/mike_brooks_MMath/programs/hello-accordion.cfa	(revision ad9f5931463621e55b660fd57101ba749263b146)
+++ doc/theses/mike_brooks_MMath/programs/hello-accordion.cfa	(revision c3e41cda7b7a639338faa16c005b96ed95202da9)
@@ -30,9 +30,9 @@
 forall( [C], [S] )
 int getPref( @School( C, S ) & school@, int is, int pref ) {
-    for ( ic; C ) {
-        int curPref = @school.preferences@[ic][is];   $\C{// offset calculation implicit}$
+	for ( ic; C ) {
+		int curPref = @school.preferences@[ic][is];   $\C{// offset calculation implicit}$
 		if ( curPref == pref ) return ic;
 	}
-    assert( false );
+	assert( false );
 }
 
@@ -59,24 +59,24 @@
 
 	{	string sv;
-        int iv;
-        // headers' row
-        sin | "\nc\\s";
-        for ( is ; ns ) {
-            // column label
-            sin | sv;
-            school.student_ids[is] = sv;
-        }
-        // body rows
-        for ( ic ; nc ) {
-            // row label
-            sin | sv;
-            school.course_codes[ic] = sv;
-            for ( is ; ns ) {
-                // matrix item
-                sin | iv;
-                school.preferences[ic][is] = iv;
-            }
-        }
-    }
+		int iv;
+		// headers' row
+		sin | "\nc\\s";
+		for ( is ; ns ) {
+			// column label
+			sin | sv;
+			school.student_ids[is] = sv;
+		}
+		// body rows
+		for ( ic ; nc ) {
+			// row label
+			sin | sv;
+			school.course_codes[ic] = sv;
+			for ( is ; ns ) {
+				// matrix item
+				sin | iv;
+				school.preferences[ic][is] = iv;
+			}
+		}
+	}
 
 
@@ -91,6 +91,6 @@
 		sout | school.student_ids[is] | ": " | nonl;
 		for ( pref; 1 ~= nc ) {
-            int ic = getPref(school, is, pref);
-            sout | school.course_codes[ ic ] | nonl;
+			int ic = getPref(school, is, pref);
+			sout | school.course_codes[ ic ] | nonl;
 		}
 		sout | nl;
Index: doc/theses/mike_brooks_MMath/programs/hello-array.cfa
===================================================================
--- doc/theses/mike_brooks_MMath/programs/hello-array.cfa	(revision ad9f5931463621e55b660fd57101ba749263b146)
+++ doc/theses/mike_brooks_MMath/programs/hello-array.cfa	(revision c3e41cda7b7a639338faa16c005b96ed95202da9)
@@ -114,5 +114,5 @@
 	f( y, y );		$\C{// ok}$
 	if ( M == N )
-		f( x, @(array( float, M ) &)@y ); $\C{// ok}$
+		f( x, @(array( float, M ) &)@y ); $\C{// ok}\CRT$
 }
 
Index: doc/theses/mike_brooks_MMath/programs/sharing-demo.cfa
===================================================================
--- doc/theses/mike_brooks_MMath/programs/sharing-demo.cfa	(revision ad9f5931463621e55b660fd57101ba749263b146)
+++ doc/theses/mike_brooks_MMath/programs/sharing-demo.cfa	(revision c3e41cda7b7a639338faa16c005b96ed95202da9)
@@ -108,6 +108,6 @@
 	assert( s2 == "bbb" );
 	sout | xstr(S2bbb) | "\t& " | s1 | "\t& " | s1a | "\t& " | s2 | "\t\\\\";
-      
-    #define S2S1a s2  = s1a
+
+	#define S2S1a s2  = s1a
 	S2S1a;
 	assert( s1 == "aaa" );
@@ -122,5 +122,5 @@
 	assert( s2 == "ccc" );
 	sout | xstr(S2ccc) | "\t& " | s1 | "\t& " | s1a | "\t& " | s2 | "\t\\\\";
-      
+
 	#define S1xxx s1  = "xxx"
 	S1xxx;
@@ -149,5 +149,5 @@
 
 	#define D2_s2_s1 string s2     = s1(1,2)
-	D2_s2_s1;      
+	D2_s2_s1;
 	assert( s1 == "abcd" );
 	assert( s1_mid == "bc" );
@@ -157,5 +157,5 @@
 	sout | "\\par\\noindent";
 
-    sout | "Again, @`shareEdits@ passes changes in both directions; copy does not.  Note the difference in index values, with the \\emph{b} position being 1 in the longer string and 0 in the shorter strings.  In the case of s1 aliasing with @s1_mid@, the very same character is being accessed by different postitions.";
+	sout | "Again, @`shareEdits@ passes changes in both directions; copy does not.  Note the difference in index values, with the \\emph{b} position being 1 in the longer string and 0 in the shorter strings.  In the case of s1 aliasing with @s1_mid@, the very same character is being accessed by different postitions.";
 	sout | "\\par\\noindent";
 	sout | "\\begin{tabular}{llll}";
@@ -176,6 +176,6 @@
 	assert( s2 == "bc" );
 	sout | xstr(D2_s1mid_minus) | "\t& " | s1 | "\t& " | s1_mid | "\t& " | s2 | "\t\\\\";
-      
-    #define D2_s2_pipe s2    [0] = '|'
+
+	#define D2_s2_pipe s2    [0] = '|'
 	D2_s2_pipe;
 	assert( s1 == "a-cd" );
@@ -186,5 +186,5 @@
 	sout | "\\par\\noindent";
 
-    sout | "Once again, assignment of a value is a modificiation that flows through the aliasing relationship, without affecting its structure.";
+	sout | "Once again, assignment of a value is a modificiation that flows through the aliasing relationship, without affecting its structure.";
 	sout | "\\par\\noindent";
 	sout | "\\begin{tabular}{llll}";
@@ -198,5 +198,5 @@
 	assert( s2 == "|c" );
 	sout | xstr(D2_s1mid_ff) | "\t& " | s1 | "\t& " | s1_mid | "\t& " | s2 | "\t\\\\";
-      
+
 	#define D2_s2_gg s2     = "gg"
 	D2_s2_gg;
@@ -208,9 +208,9 @@
 	sout | "\\par\\noindent";
 
-    sout | "In the \\emph{ff} step, which is a positive example of flow across an aliasing relationship, the result is straightforward to accept because the flow direction is from contained (small) to containing (large).  The following rules for edits through aliasing substrings will guide how to flow in the opposite direction.";
+	sout | "In the \\emph{ff} step, which is a positive example of flow across an aliasing relationship, the result is straightforward to accept because the flow direction is from contained (small) to containing (large).  The following rules for edits through aliasing substrings will guide how to flow in the opposite direction.";
 	sout | "\\par";
 
 
-    sout | "Growth and shrinkage are natural extensions.  An empty substring is a real thing, at a well-defined location, whose meaning is extrapolated from the examples so far.  The intended metaphor is to operating a GUI text editor.  Having an aliasing substring is like using the mouse to select a few words.  Assigning onto an aliasign substring is like typing from having a few words selected:  depending how much you type, the file being edited can get shorter or longer.";
+	sout | "Growth and shrinkage are natural extensions.  An empty substring is a real thing, at a well-defined location, whose meaning is extrapolated from the examples so far.  The intended metaphor is to operating a GUI text editor.  Having an aliasing substring is like using the mouse to select a few words.  Assigning onto an aliasign substring is like typing from having a few words selected:  depending how much you type, the file being edited can get shorter or longer.";
 	sout | "\\par\\noindent";
 	sout | "\\begin{tabular}{lll}";
@@ -219,5 +219,5 @@
 
 	assert( s1 == "affd" );
-//	assert( s1_mid == "fc" );                                                     // ????????? bug?
+//	assert( s1_mid == "fc" );													 // ????????? bug?
 	sout | xstr(D2_s2_gg) | "\t& " | s1 | "\t& " | s1_mid | "\t\\\\";
 
@@ -227,5 +227,5 @@
 	assert( s1_mid == "hhhh" );
 	sout  | xstr(D2_s1mid_hhhh)  | "\t& " | s1 | "\t& " | s1_mid | "\t\\\\";
-      
+
 	#define D2_s1mid_i s1_mid = "i"
 	D2_s1mid_i;
@@ -248,5 +248,5 @@
 	sout | "\\par\\noindent";
 
-    sout | "Multiple portions can be aliased.  When there are several aliasing substrings at once, the text editor analogy becomes an online multi-user editor.  I should be able to edit a paragraph in one place (changing the document's length), without my edits affecting which letters are within a mouse-selection that you had made previously, somewhere else.";
+	sout | "Multiple portions can be aliased.  When there are several aliasing substrings at once, the text editor analogy becomes an online multi-user editor.  I should be able to edit a paragraph in one place (changing the document's length), without my edits affecting which letters are within a mouse-selection that you had made previously, somewhere else.";
 	sout | "\\par\\noindent";
 	sout | "\\begin{tabular}{lllll}";
@@ -264,5 +264,5 @@
 	assert( s1_end == "d" );
 	sout  | xstr(D2_s1end_s1)  | "\t& " | s1 | "\t& " | s1_bgn | "\t& " | s1_mid | "\t& " | s1_end | "\t\\\\";
-      
+
 	#define D1_s1bgn_zzz s1_bgn = "zzzz"
 	D1_s1bgn_zzz;
@@ -275,5 +275,5 @@
 	sout | "\\par\\noindent";
 
-    sout | "When an edit happens on an aliasing substring that overlaps another, an effect is unavoidable.  Here, the passive party sees its selection shortened, to exclude the characters that were not part of the original selection.";
+	sout | "When an edit happens on an aliasing substring that overlaps another, an effect is unavoidable.  Here, the passive party sees its selection shortened, to exclude the characters that were not part of the original selection.";
 	sout | "\\par\\noindent";
 	sout | "\\begin{tabular}{llllll}";
@@ -286,5 +286,5 @@
 	assert( s1_crs == "zj" );
 	assert( s1_mid == "jj" );
-	assert( s1_end == "d" );  
+	assert( s1_end == "d" );
 	sout  | xstr(D2_s1crs_s1)  | "\t& " | s1 | "\t& " | s1_bgn | "\t& " | s1_crs | "\t& " | s1_mid | "\t& " | s1_end | "\t\\\\";
 
@@ -301,5 +301,5 @@
 	sout | "TODO: finish typesetting the demo";
 
-    // "This shortening behaviour means that a modification has to occur entirely inside a substring, to show up in that substring.  Sharing changes through the intersection of partially overlapping aliases is still possible, so long as the receiver's boundary is not inside the edit."
+	// "This shortening behaviour means that a modification has to occur entirely inside a substring, to show up in that substring.  Sharing changes through the intersection of partially overlapping aliases is still possible, so long as the receiver's boundary is not inside the edit."
 
 	string word = "Phi";
@@ -309,5 +309,5 @@
 	assert( consonants == "Ph" );
 	assert( miniscules == "hi" );
-      
+
 	consonants[1] = 's';
 	assert( word == "Psi" );
@@ -321,10 +321,10 @@
 	string greet_bgn = all(10,1)`shareEdits;
 	string greet_end = all(14,1)`shareEdits;
-      
+
 	assert( all == "They said hello again" );
 	assert( greet == "hello" );
 	assert( greet_bgn == "h" );
 	assert( greet_end == "o" );
-      
+
 
 	greet = "sup";
@@ -333,42 +333,42 @@
 	// assert( greet_bgn == "" );    ------ Should be so, but fails
 	// assert( greet_end == "" );
-      
-
-  
-
-  
-    /* As in the earlier step where \emph{aj} becomes \emph{ajjd}, such empty substrings maintain their places in the total string, and can be used for filling it.  Because @greet_bgn@ was orginally at the start of the edit, in the outcome, the empty @greet_bgn@ sits just before the written value.  Similarly @greed_end@ goes after.  Though not shown, an overwritten substring at neither side goes arbitrarily to the before side. */
-  
-
-  
-
-	greet_bgn = "what"; 
-      
-      
+
+
+
+
+
+	/* As in the earlier step where \emph{aj} becomes \emph{ajjd}, such empty substrings maintain their places in the total string, and can be used for filling it.  Because @greet_bgn@ was orginally at the start of the edit, in the outcome, the empty @greet_bgn@ sits just before the written value.  Similarly @greed_end@ goes after.  Though not shown, an overwritten substring at neither side goes arbitrarily to the before side. */
+
+
+
+
+	greet_bgn = "what";
+
+
 	assert( all == "They said whatsup again" );
-      
+
 	assert( greet == "sup" );
-      
+
 	assert( greet_bgn == "what" );
 	// assert( greet_end == "" );    ------ Should be so, but fails
-      
-
-	greet_end = "..."; 
-      
-      
+
+
+	greet_end = "...";
+
+
 	assert( all == "They said whatsup... again" );
-      
+
 	assert( greet == "sup" );
-      
+
 	assert( greet_bgn == "what" );
-      
+
 	assert( greet_end == "..." );
-      
-
-  
-
-  
-    /* Though these empty substrings hold their places in the total string, an empty string only belongs to bigger strings when it occurs completely inside them.  There is no such state as including an empty substring at an edge.  For this reason, @word@ gains the characters added by assigning to @greet_bgn@ and @greet_end@, but the string @greet@ does not. */
-  
+
+
+
+
+
+	/* Though these empty substrings hold their places in the total string, an empty string only belongs to bigger strings when it occurs completely inside them.  There is no such state as including an empty substring at an edge.  For this reason, @word@ gains the characters added by assigning to @greet_bgn@ and @greet_end@, but the string @greet@ does not. */
+
 
 }
@@ -377,6 +377,6 @@
 int main(int argc, char ** argv) {
 
-    demo1();
-    demo2();
-    printf("%% %s done running\n", argv[0]);
+	demo1();
+	demo2();
+	printf("%% %s done running\n", argv[0]);
 }
Index: doc/theses/mike_brooks_MMath/uw-ethesis.tex
===================================================================
--- doc/theses/mike_brooks_MMath/uw-ethesis.tex	(revision ad9f5931463621e55b660fd57101ba749263b146)
+++ doc/theses/mike_brooks_MMath/uw-ethesis.tex	(revision c3e41cda7b7a639338faa16c005b96ed95202da9)
@@ -102,4 +102,5 @@
 \input{common}
 %\usepackage{common}
+
 \CFAStyle						% CFA code-style
 \lstset{language=cfa,belowskip=-1pt} % set default language to CFA