Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision d414664b3fcda8f61f1064c2243cd6933479112c)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision d69f71143d903677ae8e0197f438ba2d7efef849)
@@ -155,4 +155,12 @@
 
 
+\section{Enumerator Opaque Type}
+
+\CFA provides a special opaque enumeration type, where the internal representation is chosen by the compiler and only equality operations are available.
+\begin{cfa}
+enum@()@ Planets { MERCURY, VENUS, EARTH, MARS, JUPITER, SATURN, URANUS, NEPTUNE };
+\end{cfa}
+
+
 \section{Enumeration Inheritance}
 
@@ -262,4 +270,105 @@
 
 
+\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{Planet Example}
 
@@ -270,8 +379,8 @@
 Function @surfaceGravity@ uses the @with@ clause to remove @p@ qualification from fields @mass@ and @radius@.
 The program main uses @SizeE@ to obtain the number of enumerators in @Planet@, and safely converts the random value into a @Planet@ enumerator.
-The resulting random orbital body is used in a @choose@ statement.
+The resulting random orbital-body is used in a \CFA @choose@ statement.
 The enumerators in the @case@ clause use position for testing.
-The prints use @labelE@ to print the enumerators label.
-Finally, a loop iterates through the planets computing the weight on each planet for a given earth weight.
+The prints use @labelE@ to print an enumerator's label.
+Finally, a loop iterates through the planets computing the weight on each planet for a given earth mass.
 The print statement does an equality comparison with an enumeration variable and enumerator.
 
@@ -294,5 +403,5 @@
 enum( double ) { G = 6.6743_E-11 }; $\C{// universal gravitational constant (m3 kg-1 s-2)}$
 static double surfaceGravity( Planet p ) @with( p )@ {
-	return G * mass / ( radius \ 2u ); $\C{// exponentiation}$
+	return G * mass / ( radius \ 2 ); $\C{// exponentiation}$
 }
 static double surfaceWeight( Planet p, double otherMass ) {
@@ -302,5 +411,5 @@
 	if ( argc != 2 ) exit | "Usage: " | argv[0] | "earth-weight";
 	double earthWeight = convert( argv[1] );
-	double mass = earthWeight / surfaceGravity( EARTH );
+	double earthMass = earthWeight / surfaceGravity( EARTH );
 
 	Planet p = @fromInt@( prng( @SizeE@(Planet) ) ); $\C{// select a random orbiting body}$
@@ -315,5 +424,5 @@
 	for ( @p; Planet@ ) {
 		sout | "Your weight on" | (@p == MOON@ ? "the" : "") | labelE(p)
-			   | "is" | wd(1,1, surfaceWeight( p, mass )) | "kg";
+			   | "is" | wd( 1,1, surfaceWeight( p, earthMass ) ) | "kg";
 	}
 }
@@ -333,159 +442,2 @@
 \label{f:PlanetExample}
 \end{figure}
-
-\section{Enum Trait}
-The header file @<enum.hfa>@ defines traits implemented by, and sets of operators and helper functions defined for enum.
-
-\begin{figure}
-\small
-\begin{cfa}
-forall(E) trait Bounded {
-	E lowerBound();
-	E upperBound();
-};
-\end{cfa}
-\caption{f:Bounded Trait}
-\label{f:BoundedTrait}
-\end{figure}
-
-\CFA enums satisfy Bounded trait thanks to the default implemention of @lowerBound()@ and @upperBound()@, with 
-@lowerBound()@ returning the first enumerator and @upperBound()@ returning the last.
-
-\begin{figure}
-\small
-\begin{cfa}
-Workday day1 = lowerBound(); // Monday
-Planet lastPlanet = upperBound(); // NEPTUNE
-\end{cfa}
-\caption{f:Bound Functions}
-\label{f:BoundFunctions}
-\end{figure}
-
-@lowerBound()@ and @upperBound()@ are overloaded with return types only. Calling either functions 
-without a context can result in type ambiguity if more than one types implement the functions from the @Bounded@ traits.
-Because \CFA enum types implements @Bounded@, multiple type enumerations in the same lexical scope will
-cause ambiguity on @lowerBound()@ and @upperBound()@ \see{\VRef{f:BoundFunctions} }.
-
-\begin{figure}
-\small
-\begin{cfa}
-// lowerBound(); // Error because both Planet and Workday implement Bounded
-Workday day1 = lowerBound(); // Okay because type of day1 hints lowerBound() to return a Workday
-void foo(Planet p);
-foo( upperBound() ); Okay because foo expects value with type Planet as parameter
-\end{cfa}
-\caption{Bound Function ambiguity}
-\label{f:BoundAmbiguity}
-\end{figure}
-
-\begin{figure}
-\small
-\begin{cfa}
-forall(E | Bounded(E)) trait Serial {
-	unsigned fromInstance(E e);
-	E fromInt(unsigned i);
-	E succ(E e);
-	E pred(E e);
-};
-\end{cfa}
-\caption{Bounded Trait}
-\label{f:BoundedTrait}
-\end{figure}
-
-A Serial type is a @Bounded@ type where elements can be mapped to an integer sequence.
-A serial type @T@ can project to the integer type: an instance of type T has a corresponding integer value, 
-but the inverse may not be possible, and possible requires a bound check.
-
-The mapping from a serial type to integer is defined as @fromInstance(E e)@.
-For enum types, @fromInstance(E e)@ is equivalent to getting the position of e.
-The inverse of @fromInstance(E e)@ is @fromInt(unsigned i)@ and \CFA implements it with a bound check.
-For an enum @E@ declares N enumerators, @fromInt(i)@ returns the $i-1_{th}$ enumerator if $0 \leq i < N$, or error otherwises.
-
-The Serial trait provides interface functions @succ(E e)@ and @pred(E e)@ as members of a serial type are consecutive and ordinal. 
-If @e@ is the $i_{th}$ enumerator, @succ(e)@ returns the $i+1_{th}$ enumerator when $e != upperBound()$, and @pred(e)@ 
-returns the $i-1_{th}$ enumerator when $e != lowerBound()$. 
-\CFA compiler gives an error if the result of the operation is out the domain of type @T@.
-
-\begin{figure}
-\small
-\begin{cfa}
-forall(E, T) trait TypedEnum {
-	T valueE(E e);
-	char * labelE(E e);
-	unsigned int posE(E e);
-};
-\end{cfa}
-\caption{Type Enum Trait}
-\label{f:TypeEnumTrait}
-\end{figure}
-
-The @TypedEnum@ trait captures three basic attributes of a type enum: value, label, and position. 
-TypedEnum asserts two types @E@ and @T@, with @T@ being the base type of enumeration @E@.
-Implementing functions for general type enums is possible by asserting @TypeEnum(E, T)@.
-
-\begin{figure}
-\small
-\begin{cfa}
-forall( E, T | TypeEnum(E, T))
-void printEnum(E e) {
-	sout | "Enum "| labelE(e);
-}
-printEunm(MARS);
-\end{cfa}
-\caption{Implement Functions for Enums}
-\label{f:ImplementEnumFunction}
-\end{figure}
-
-@<enum.hfa>@ overwrites comparison operators for type enums. 
-\begin{figure}
-\small
-\begin{cfa}
-forall(E, T| TypedEnum(E, T)) {
-	// comparison
-	int ?==?(E l, E r); // returns True if l and r are the same enumerator
-	int ?!=?(E l, E r); // returns True if l and r are the different enumerator
-	int ?!=?(E l, zero_t); // return True if l is not the first enumerator
-	int ?<?(E l, E r); // return True if l is an enuemerator before r
-	int ?<=?(E l, E r); // return True if l==r or l<r
-	int ?>?(E l, E r); // return True if l is an enuemrator after r
-	int ?>=?(E l, E r); // return True if l>r or l==r
-}
-\end{cfa}
-\caption{Enum Operators}
-\label{f:EnumOperators}
-\end{figure}
-The overloaded operators in \ref{f:EnumOperators} are defined when and 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 @T@.
-
-\begin{figure}
-\small
-\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 they are different enumerator
-\end{cfa}
-\caption{Include <enum.hfa>}
-\label{f:IncludeHeader}
-\end{figure}
-
-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 prints enumeration @value@ over @position@.
-\begin{figure}
-\small
-\begin{cfa}
-printf("Position of BANANA is \%d", BANANA); // Postion of BANANA is 1
-sout | "Value of BANANA is " | BANANA; // Value of BANANA is 10
-\end{cfa}
-\caption{Print Enums}
-\label{f:PrintEnum}
-\end{figure}
-
-Programmers can overwrite this behaviour by overloading the pipeline operator themselve.
Index: doc/theses/jiada_liang_MMath/relatedwork.tex
===================================================================
--- doc/theses/jiada_liang_MMath/relatedwork.tex	(revision d414664b3fcda8f61f1064c2243cd6933479112c)
+++ doc/theses/jiada_liang_MMath/relatedwork.tex	(revision d69f71143d903677ae8e0197f438ba2d7efef849)
@@ -218,5 +218,5 @@
 
 \CC has aliasing using @const@ declarations, like C \see{\VRef{s:Cconst}}, with type inferencing, plus static/dynamic initialization.
-(Note, a \CC @constexpr@ declaration is the same @const@ with the restriction that the initialization is a compile-time expression.)
+(Note, a \CC @constexpr@ declaration is the same as @const@ with the restriction that the initialization is a compile-time expression.)
 \begin{c++}
 const @auto@ one = 0 + 1;				$\C{// static initialization}$
@@ -241,5 +241,5 @@
 whereas C @const@ declarations without @static@ are marked @R@.
 
-The following non-backwards compatible changes are made \see{\cite[\S~7.2]{ANSI98:C++}}.
+The following \CC non-backwards compatible changes are made \see{\cite[\S~7.2]{ANSI98:C++}}.
 \begin{cquote}
 Change: \CC objects of enumeration type can only be assigned values of the same enumeration type.