Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 35897fb34306b8aedf6e4f502519debba8b7ec7b)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 72713e5bd3cf1fe33bcf6d53d418f97ac9ed6c2c)
@@ -335,6 +335,8 @@
 
 \section{Enum Trait}
-A typed enum comes with traits capture enumeration charastics and helper functions. 
-
+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 {
@@ -343,21 +345,40 @@
 };
 \end{cfa}
-\CFA enums satisfy Bounded trait thanks to the compiler implementing lowerBound() and upperBound(), with 
-lowerBound() returning the first enumerator and upperBound() return the last.
-
+\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}
-
-Because lowerBound() and upperBound() are overloaded with return types only, calling either functions 
-in a null context cause type ambiguity if than one type implementing Bounded traits, including typed enumerations.
-\begin{cfa}
-Workday day1 = lowerBound(); // Okay because rhs hints lowerBound() to return a Workday
+\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's parameter give type hint
-// lowerBound(); // Error because both Planet and Workday implements Bounded
-\end{cfa}
-
+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 {
@@ -368,10 +389,24 @@
 };
 \end{cfa}
-A Serial type can be mapped to a sequnce of integer. For enum types, fromInstance(E e) is equivalent to 
-posE(E e). Enumerations implement fromInt(), succ(), and pred() with bound() check.
-For an enum declares N enumerators, fromInt(i) returns the ith enumerator of type E if $0 \leq i < N$.
-If e is the i-th enumerator, succ(e) returns the i+1-th enumerator if $e != upperBound()$ and pred(e) 
-returns the i-1-th enumerator $e != lowerBound()$. \CFA compile gives an error if bound check fails.
-
+\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 {
@@ -381,8 +416,14 @@
 };
 \end{cfa}
-
-The TypedEnum trait capture three basic attributes of type enums. TypedEnum asserts two types E and T, with T being the base type of enumeration E.
-With an assertion on TypedEnum, we can implement functions for all type enums.
-
+\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))
@@ -392,29 +433,59 @@
 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);
-	int ?!=?(E l, E r);
-	int ?!=?(E l, zero_t);
-	int ?<?(E l, E r);
-	int ?<=?(E l, E r);
-	int ?>?(E l, E r);
-	int ?>=?(E l, E r);
-}
-\end{cfa}
-These overloaded operators are not defined if the file is not included.
-In this case, the compiler converts an enumerator to its value, and applies the operators
-if they are defined for the value type T.
-
+	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=1, CHERRY=2
-};
-APPLE == CHERRY; // True because they have the same Value
+	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.