Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision dc7423120f49721a6d5f3e51bdcfe4b35a1fd58a)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision bfcd3af76db74e3dbbed12a62295035015729a46)
@@ -70,18 +70,119 @@
 As in Section~\ref{s:EnumeratorVisibility}, opening multiple scoped enumerations in a @with@ can result in duplicate enumeration names, but \CFA implicit type resolution and explicit qualification/casting handle ambiguities.
 
-
-\section{Enumeration Pseudo-functions}
-
-Pseudo-functions are function-like operators that do not result in any run-time computations, \ie like @sizeof@, @alignof@, @typeof@.
-A pseudo-function call is often substituted with information extracted from the compilation symbol-table, like storage size or alignment associated with the underlying architecture.
-
-The attributes of an enumerator are accessed by pseudo-functions @posE@, @valueE@, and @labelE@.
-\begin{cfa}
-int jane_pos = @posE@( Names.Jane );   $\C{// 2}$
-char * jane_value = @valueE@( Names.Jane ); $\C{// "JANE"}$
-char * jane_label = @labelE@( Names.Jane ); $\C{// "Jane"}$
-sout | posE( Names.Jane) | labelE( Names.Jane ) | valueE( Names.Jane );
-\end{cfa}
-Note the ability to print all of an enumerator's properties.
+\section{Enumeration Trait}
+
+The header file \lstinline[deletekeywords=enum]{<enum.hfa>} defines the set of traits containing operators and helper functions for @enum@.
+A \CFA enumeration satisfies all of these traits allowing it to interact with runtime features in \CFA.
+Each trait is discussed in detail.
+
+The trait @Bounded@:
+\begin{cfa}
+forall( E ) trait Bounded {
+	E first();
+	E last();
+};
+\end{cfa}
+defines the bounds of the enumeration, where @first()@ returns the first enumerator and @last()@ returns the last, \eg:
+\begin{cfa}
+Workday day = first();					$\C{// Mon}$
+Planet outermost = last();				$\C{// NEPTUNE}$
+\end{cfa}
+@first()@ and @last()@ are overloaded with return types only, so in the example, the enumeration type is found on the left-hand side of the assignment.
+Calling either functions without a context results in a type ambiguity, except in the rare case where the type environment has only one enumeration.
+\begin{cfa}
+@first();@								$\C{// ambiguous Workday and Planet implement Bounded}$
+sout | @last()@;
+Workday day = first();					$\C{// day provides type Workday}$
+void foo( Planet p );
+foo( last() );							$\C{// parameter provides type Planet}$
+\end{cfa}
+
+The trait @Serial@:
+\begin{cfa}
+forall( E | Bounded( E ) ) trait Serial {
+	unsigned fromInstance( E e );
+	E fromInt( unsigned int posn );
+	E succ( E e );
+	E pred( E e );
+};
+\end{cfa}
+is a @Bounded@ trait, where elements can be mapped to an integer sequence.
+A type @T@ matching @Serial@ can project to an unsigned @int@ type, \ie an instance of type T has a corresponding integer value.
+%However, the inverse may not be possible, and possible requires a bound check.
+The mapping from a serial type to integer is defined by @fromInstance@, which returns the enumerator's position.
+The inverse operation is @fromInt@, which performs a bound check using @first()@ and @last()@ before casting the integer into an enumerator.
+Specifically, for enumerator @E@ declaring $N$ enumerators, @fromInt( i )@ returns the $i-1_{th}$ enumerator, if $0 \leq i < N$, or raises the exception @enumBound@.
+
+The @Serial@ trait also requires interface functions @succ( E e )@ and @pred( E e )@ be implemented for a serial type, which imply the enumeration positions are consecutive and ordinal. 
+Specifically, if @e@ is the $i_{th}$ enumerator, @succ( e )@ returns the $i+1_{th}$ enumerator when $e \ne last()$, and @pred( e )@ returns the $i-1_{th}$ enumerator when $e \ne first()$. 
+The exception @enumRange@ is raised if the result of either operation is outside the range of type @E@.
+
+The trait @TypedEnum@:
+\begin{cfa}
+forall( E, T ) trait TypedEnum {
+	T valueE( E e );
+	char * labelE( E e );
+	unsigned int posE( E e );
+};
+\end{cfa}
+captures three basic attributes of an enumeration type: value, label, and position. 
+@TypedEnum@ asserts two types @E@ and @T@, with @T@ being the base type of the enumeration @E@, \eg @enum( T ) E { ... };@.
+Implementing general functions across all enumeration types is possible by asserting @TypeEnum( E, T )@, \eg:
+\begin{cfa}
+forall( E, T | TypeEnum( E, T ) )
+void printEnum( E e ) {
+	sout | "Enum "| labelE( e );
+}
+printEunm( MARS );
+\end{cfa}
+
+Finally, there is an associated trait defining comparison operators among enumerators. 
+\begin{cfa}
+forall( E, T | TypedEnum( E, T ) ) {
+	// comparison
+	int ?==?( E l, E r ); 		$\C{// true if l and r are same enumerators}$
+	int ?!=?( E l, E r ); 		$\C{// true if l and r are different enumerators}$
+	int ?!=?( E l, zero_t ); 	$\C{// true if l is not the first enumerator}$
+	int ?<?( E l, E r ); 		$\C{// true if l is an enumerator before r}$
+	int ?<=?( E l, E r ); 		$\C{// true if l before or the same as r}$
+	int ?>?( E l, E r ); 		$\C{// true if l is an enumerator after r}$
+	int ?>=?( E l, E r ); 		$\C{// true if l after or the same as r}$         
+}
+\end{cfa}
+Note, the overloaded operators are defined only when the header @<enum.hfa>@ is included.
+If not, the compiler converts an enumerator to its value, and applies the operators defined for the value type @E@, \eg:
+\begin{cfa}
+// if not include <enum.hfa>
+enum( int ) Fruits { APPLE = 2, BANANA = 10, CHERRY = 2 };
+APPLE == CHERRY; // true because valueE( APPLE ) == valueE( CHERRY )
+
+#include <enum.hfa>
+APPLE == CHERRY; // false because posE( APPLE ) != posE( CHERRY )
+\end{cfa}
+An enumerator returns its @position@ by default.
+In particular, @printf( ... )@ from @<stdio.h>@ functions provides no context to its parameter type, so it prints @position@. 
+On the other hand, the pipeline operator @?|?( ostream os, E enumType )@ provides type context for type @E@, and \CFA has overwritten this operator to print the enumeration @value@ over @position@.
+\begin{cfa}
+printf( "Position of BANANA is \%d", BANANA ); // Position of BANANA is 1
+sout | "Value of BANANA is " | BANANA; // Value of BANANA is 10
+\end{cfa}
+Programmers can overwrite this behaviour by overloading the pipeline operator themselves.
+\PAB{This needs discussing because including \lstinline{<enum.hfa>} can change the entire meaning of a program.}
+
+
+% \section{Enumeration Pseudo-functions}
+
+% Pseudo-functions are function-like operators that do not result in any run-time computations, \ie like @sizeof@, @alignof@, @typeof@.
+% A pseudo-function call is often substituted with information extracted from the compilation symbol-table, like storage size or alignment associated with the underlying architecture.
+
+% The attributes of an enumerator are accessed by pseudo-functions @posE@, @valueE@, and @labelE@.
+% \begin{cfa}
+% int jane_pos = @posE@( Names.Jane );   $\C{// 2}$
+% char * jane_value = @valueE@( Names.Jane ); $\C{// "JANE"}$
+% char * jane_label = @labelE@( Names.Jane ); $\C{// "Jane"}$
+% sout | posE( Names.Jane) | labelE( Names.Jane ) | valueE( Names.Jane );
+% \end{cfa}
+% Note the ability to print all of an enumerator's properties.
+
 
 
@@ -270,104 +371,15 @@
 
 
-\section{Enumeration Trait}
-
-The header file \lstinline[deletekeywords=enum]{<enum.hfa>} defines the set of traits containing operators and helper functions for @enum@.
-A \CFA enumeration satisfies all of these traits allowing it to interact with runtime features in \CFA.
-Each trait is discussed in detail.
-
-The trait @Bounded@:
-\begin{cfa}
-forall( E ) trait Bounded {
-	E first();
-	E last();
-};
-\end{cfa}
-defines the bounds of the enumeration, where @first()@ returns the first enumerator and @last()@ returns the last, \eg:
-\begin{cfa}
-Workday day = first();					$\C{// Mon}$
-Planet outermost = last();				$\C{// NEPTUNE}$
-\end{cfa}
-@first()@ and @last()@ are overloaded with return types only, so in the example, the enumeration type is found on the left-hand side of the assignment.
-Calling either functions without a context results in a type ambiguity, except in the rare case where the type environment has only one enumeration.
-\begin{cfa}
-@first();@								$\C{// ambiguous Workday and Planet implement Bounded}$
-sout | @last()@;
-Workday day = first();					$\C{// day provides type Workday}$
-void foo( Planet p );
-foo( last() );							$\C{// parameter provides type Planet}$
-\end{cfa}
-
-The trait @Serial@:
-\begin{cfa}
-forall( E | Bounded( E ) ) trait Serial {
-	unsigned fromInstance( E e );
-	E fromInt( unsigned int posn );
-	E succ( E e );
-	E pred( E e );
-};
-\end{cfa}
-is a @Bounded@ trait, where elements can be mapped to an integer sequence.
-A type @T@ matching @Serial@ can project to an unsigned @int@ type, \ie an instance of type T has a corresponding integer value.
-%However, the inverse may not be possible, and possible requires a bound check.
-The mapping from a serial type to integer is defined by @fromInstance@, which returns the enumerator's position.
-The inverse operation is @fromInt@, which performs a bound check using @first()@ and @last()@ before casting the integer into an enumerator.
-Specifically, for enumerator @E@ declaring $N$ enumerators, @fromInt( i )@ returns the $i-1_{th}$ enumerator, if $0 \leq i < N$, or raises the exception @enumBound@.
-
-The @Serial@ trait also requires interface functions @succ( E e )@ and @pred( E e )@ be implemented for a serial type, which imply the enumeration positions are consecutive and ordinal. 
-Specifically, if @e@ is the $i_{th}$ enumerator, @succ( e )@ returns the $i+1_{th}$ enumerator when $e \ne last()$, and @pred( e )@ returns the $i-1_{th}$ enumerator when $e \ne first()$. 
-The exception @enumRange@ is raised if the result of either operation is outside the range of type @E@.
-
-The trait @TypedEnum@:
-\begin{cfa}
-forall( E, T ) trait TypedEnum {
-	T valueE( E e );
-	char * labelE( E e );
-	unsigned int posE( E e );
-};
-\end{cfa}
-captures three basic attributes of an enumeration type: value, label, and position. 
-@TypedEnum@ asserts two types @E@ and @T@, with @T@ being the base type of the enumeration @E@, \eg @enum( T ) E { ... };@.
-Implementing general functions across all enumeration types is possible by asserting @TypeEnum( E, T )@, \eg:
-\begin{cfa}
-forall( E, T | TypeEnum( E, T ) )
-void printEnum( E e ) {
-	sout | "Enum "| labelE( e );
-}
-printEunm( MARS );
-\end{cfa}
-
-Finally, there is an associated trait defining comparison operators among enumerators. 
-\begin{cfa}
-forall( E, T | TypedEnum( E, T ) ) {
-	// comparison
-	int ?==?( E l, E r ); 		$\C{// true if l and r are same enumerators}$
-	int ?!=?( E l, E r ); 		$\C{// true if l and r are different enumerators}$
-	int ?!=?( E l, zero_t ); 	$\C{// true if l is not the first enumerator}$
-	int ?<?( E l, E r ); 		$\C{// true if l is an enumerator before r}$
-	int ?<=?( E l, E r ); 		$\C{// true if l before or the same as r}$
-	int ?>?( E l, E r ); 		$\C{// true if l is an enumerator after r}$
-	int ?>=?( E l, E r ); 		$\C{// true if l after or the same as r}$         
-}
-\end{cfa}
-Note, the overloaded operators are defined only when the header @<enum.hfa>@ is included.
-If not, the compiler converts an enumerator to its value, and applies the operators defined for the value type @E@, \eg:
-\begin{cfa}
-// if not include <enum.hfa>
-enum( int ) Fruits { APPLE = 2, BANANA = 10, CHERRY = 2 };
-APPLE == CHERRY; // true because valueE( APPLE ) == valueE( CHERRY )
-
-#include <enum.hfa>
-APPLE == CHERRY; // false because posE( APPLE ) != posE( CHERRY )
-\end{cfa}
-An enumerator returns its @position@ by default.
-In particular, @printf( ... )@ from @<stdio.h>@ functions provides no context to its parameter type, so it prints @position@. 
-On the other hand, the pipeline operator @?|?( ostream os, E enumType )@ provides type context for type @E@, and \CFA has overwritten this operator to print the enumeration @value@ over @position@.
-\begin{cfa}
-printf( "Position of BANANA is \%d", BANANA ); // Position of BANANA is 1
-sout | "Value of BANANA is " | BANANA; // Value of BANANA is 10
-\end{cfa}
-Programmers can overwrite this behaviour by overloading the pipeline operator themselves.
-\PAB{This needs discussing because including \lstinline{<enum.hfa>} can change the entire meaning of a program.}
-
+
+\section{Enumerated Arrays}
+Enumerated array use an \CFA array as their index.
+\begin{cfa}
+enum() Colour {
+	Red, Orange, Yellow, Green, Blue, Indigo, Violet
+};
+
+string colourCode[Colour] = { "#e81416", "#ffa500", "#ffa500", "#ffa500", "#487de7", "#4b369d", "#70369d" };
+sout | "Colour Code of Orange is " | colourCode[Orange];
+\end{cfa}
 
 \section{Planet Example}