Index: doc/theses/jiada_liang_MMath/intro.tex
===================================================================
--- doc/theses/jiada_liang_MMath/intro.tex	(revision c4d6c900fd47e0fbd91cc0e4ab14450e327e9618)
+++ doc/theses/jiada_liang_MMath/intro.tex	(revision c03af3175878c32c0de8ee068d13afa9e559f1b0)
@@ -299,13 +299,13 @@
 \begin{enumerate}
 \item
-overloading:
-\item
-scoping
-\item
-typing
-\item
-subseting
-\item
-inheritance
+overloading: provides a pattern to overload functions, literal, and variable for polymorphic enumerations.
+\item
+scoping: adds name space for enumerations.
+\item
+safety: defines a safe enumeration conversion scheme.
+\item
+harmonization: allows enumeration to be mapped with data.
+\item
+inheritance: implements containment inheritance for enumerations.
 \end{enumerate}
 
Index: doc/theses/jiada_liang_MMath/rangeLoops.cfa
===================================================================
--- doc/theses/jiada_liang_MMath/rangeLoops.cfa	(revision c03af3175878c32c0de8ee068d13afa9e559f1b0)
+++ doc/theses/jiada_liang_MMath/rangeLoops.cfa	(revision c03af3175878c32c0de8ee068d13afa9e559f1b0)
@@ -0,0 +1,50 @@
+#include <enum.hfa>
+#include <fstream.hfa>
+
+enum() Chars{A, B, C, D};
+forall(E | CfaEnum(E) | Serial(E)) void baz(E) {
+    for (e; E) {
+        sout | label(e);
+    }
+}
+
+void foo() {
+    for (unsigned i = 0; i < countof(Chars); i++) {
+        sout | label((Chars)fromInt(i));
+    }
+    sout | nl;
+    for (Chars e = lowerBound();; e = succ(e)) {
+        sout | label(e);
+        if (e == upperBound()) break;
+    }
+    sout | nl;
+    for (Chars e; A ~ = D) {
+        sout | label(e);
+    }
+    sout | nl;
+    for (e; A ~ = D) {
+        sout | label(e);
+    }
+    sout | nl;
+    for (Chars e; A - ~ = D) {
+        sout | label(e);
+    }
+    sout | nl;
+    for (e; A - ~ = D ~2) {
+        sout | label(e);
+    }
+    sout | nl;
+    for (e; Chars) {
+        sout | label(e);
+    }
+    sout | nl;
+    baz(A);
+}
+
+void bar() {
+    for (unsigned i = countof(Chars) - 1; i >= 0; i--) {}
+    for (Chars e = lowerBound(); e <= upperBound(); e = succ(e)) {}
+    for (Chars e = upperBound(); e >= lowerBound(); e = pred(e)) {}
+}
+
+int main() { foo(); }
Index: doc/theses/jiada_liang_MMath/trait.tex
===================================================================
--- doc/theses/jiada_liang_MMath/trait.tex	(revision c4d6c900fd47e0fbd91cc0e4ab14450e327e9618)
+++ doc/theses/jiada_liang_MMath/trait.tex	(revision c03af3175878c32c0de8ee068d13afa9e559f1b0)
@@ -185,6 +185,6 @@
 \begin{cfa}
 enum RGB {Red, Green, Blue};
-countof( RGB ); // (1)
-countof( Red ); // (2)
+countof( RGB );
+countof( Red );
 \end{cfa}
 Both expressions from the previous example are converted to constant expression @3@ with no function call at runtime. 
@@ -201,32 +201,108 @@
 \end{enumerate}
 
-With the @Bounded@ and @Serial@, a loop over enumeration can be implemented in the following ways:
-\begin{cfa}
-enum() E { ... }
-for( unsigned i = 0; i < countof(E); i++ ) { ... }
-for( E e = lowerBound(); ; e = succ(e) ) { ...; if (e == upperBound()) break; }
-
-forall( T ) {
-	for( unsigned i = 0; i < countof(T); i++ ) { ... }
-	for( T e = lowerBound(); ; e = succ(e) ) { ...; if (e == upperBound()) break; }
-}
-\end{cfa}
-
-Finally, there is an associated trait defining comparison operators among enumerators. 
-\begin{cfa}
-forall( E, T | CfaEnum( E, T ) ) {
+\section{Iterating Over An Enumeration}
+An fundamental aspect of an enumerated type is to be able to enumerate over its enumerators. \CFA supports \newterm{for} loops,
+\newterm{while} loop, and \newterm{range} loop. This section covers @for@ loops and @range@ loops for 
+enumeration, but the concept transition to @while@ loop.
+
+\subsection{For Loop}
+A for loop is constitued by a loop control and a loop body.
+A loop control is often a 3-tuple, separated by semicolons: initializers, condition, and an expression. It is a common practice to declare 
+a variable, often in initializers, that be used in the condition and updated in the expression or loop body. Such variable is called \newterm{index}.
+
+% With implemented @Bounded@ and @Serial@ interface for \CFA enumeration, a @for@ loop that iterates over \CFA enumeration can be implemented as the following:
+A @for@ loop iterates an enumeration can be written with functions from @Bounded@ and @Serial@ interfaces:
+\begin{cfa}
+enum() Chars { A, B, C, D };
+for( unsigned i = 0; i < countof(E); i++ ) { sout | label(e); }		$\C{// (1) A B C D}$
+for( Chars e = lowerBound(); ; e = succ(e) ) { $\C{// (2)}$
+	sout |label((Chars)fromInt(i)) |' '; 
+	if (e == upperBound()) break; 
+}
+\end{cfa}
+
+A caveat in writing loop using finite number as index is that the number can unintentionally be out the range:
+\begin{cfa}
+for( unsigned i = countof(Chars) - 1; i >= 0; i-- ) {}				$\C{// 3}$
+for( Chars e = lowerBound(); e <= upperBound(); e = succ(e) ) {}	$\C{// 4}$
+for( Chars e = upperBound(); e >= lowerBound(); e = pred(e) ) {}	$\C{// 5}$
+\end{cfa}
+Loop (3) is a value underflow: when @i@ reaches to @0@, decrement statement will still execute and cause 
+the @unsigned int@ value @i@ wraps to @UINT_MAX@, which fails to loop test and the loop cannot terminate.
+
+In loop (4) and (5), when @e@ is at the @Bound@ (@upperBound@/@lowerBound@) and @succ@/@pred@ will result in @out of bounded@, \CFA 
+aborts its execution. Therefore, it is necessary to implement the condtional break within the loop body.
+
+
+\subsection{Range Loop}
+Instead of specifying condition, \CFA supports @range loops@, for which a user specifies a range of values. 
+\begin{cfa}[label=lst:range_functions_2]
+for ( Chars e; A ~= D ) { sout | label(e); }		$\C{// (6)}$
+for ( e; A ~= D ) { sout | label(e); }				$\C{// (7)}$
+for ( Chars e; A -~= D ) { sout | label(e); }		$\C{// (8) D C B A}$
+for ( e; A -~=D ~ 2 ) { sout | label(e); }		$\C{// (9) D B }$
+\end{cfa}
+Every range loop above has an index declaration, and a @range@ bounded by \newterm{left bound} @A@ and \newterm{right bound} @D@. 
+An index declaration can have an optional type declaration, without which \CFA 
+implicitly declares index variable to be the type of the bounds (@typeof(A)@). 
+If a range is joined by @~=@ (range up equal) operator, the index variable will be initialized by 
+the @left bound@, and change incrementally until its position exceeds @right bound@.
+On the other hand, if a range is defined with @-~=@ (range down equal) operation, the index variable will
+have the value of the @right bound@. It change decrementally until its position is less than the @left bound@. 
+A range can be suffixed by an positive integal \newterm{step}, joined by @~@. The loop @(9)@ declares a step size of 2 so that 
+e updates @pred(pred(e))@ in every iteration.
+
+\CFA manipulates the position of the index variable and breaks the loop if an index update can result in @out of range@. 
+
+\CFA provides a shorthand for range loop over a \CFA enumeration or a @Serial@:
+\begin{cfa}[label=lst:range_functions_2]
+for ( e; Chars ) { sout | label(e); }		$\C{// (10) A B C D}$
+for ( e; E ) {								$\C{// forall(E | CfaEnum(E) | Serial(E)) }$
+    sout | label(e);
+}
+\end{cfa}
+The shorthand syntax has a type name expression (@Char@ and @E@) as its range. If the range expression does not name 
+a \CFA enumeration or a @Serial@, \CFA reports a compile time error. When type name as range is a \CFA enumeration, 
+it turns into a loop that iterates all enumerators of the type. If the type name is a @Serial@, the index variable 
+will be initialized as the @lowerBound@. The loop control checks the index's position against the position of @upperBound@, 
+and terminate the loop when the index has a position greater than the @upperBound@. \CFA does not update the index with 
+@succ@ but manipulate its position directly to avoid @out of bound@.
+
+\section{Overload Operators}
+% Finally, there is an associated trait defining comparison operators among enumerators. 
+\CFA preemptively overloads comparison operators for \CFA enumeration with @Serial@ and @CfaEnum@. 
+They defines that two enumerators are equal only if the are the same enumerator, and compartors are 
+define for order comparison.
+\begin{cfa}
+forall( E | CfaEnum( E ) | Serial( E ) ) {
 	// 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}
-
-As an alternative, users can define the boolean conversion for CfaEnum:
-
+	int ?>=?( E l, E r ); 		$\C{// true if l after or the same as r}$
+}
+\end{cfa}
+
+\CFA implements few arithmetic operators for @CfaEnum@. Unlike update functions in @Serial@, these 
+operator does not have bound checks, which rely on @upperBound@ and @lowerBound@. These operators directly manipulate 
+position, the underlying representation of a \CFA enumeration.
+\begin{cfa}
+forall( E | CfaEnum( E ) | Serial( E ) ) {
+	// comparison
+	E ++?( E & l );
+	E --?( E & l );
+	E ?+=? ( E & l, one_t );
+	E ?-=? ( E & l, one_t );
+	E ?+=? ( E & l, int i );
+	E ?-=? ( E & l, int i );
+	E ?++( E & l );
+	E ?--( E & l );
+}
+\end{cfa}
+
+Lastly, \CFA does not define @zero_t@ for \CFA enumeration. Users can define the boolean false for 
+\CFA enumerations on their own. Here is an example:
 \begin{cfa}
 forall(E | CfaEnum(E))
@@ -235,93 +311,97 @@
 }
 \end{cfa}
-which effectively turns the first enumeration as a logical zero and non-zero for others.
-
-\begin{cfa}
-Count variable_a = First, variable_b = Second, variable_c = Third, variable_d = Fourth;
-p(variable_a); // 0
-p(variable_b); // 1
-p(variable_c); // "Third"
-p(variable_d); // 3
-\end{cfa}
-
-
-\section{Iteration and Range}
-
-It is convenient to iterate over a \CFA enumeration value, \eg:
-\begin{cfa}[label=lst:range_functions]
-for ( Alphabet alph; Alphabet ) { sout | alph; }
->>> A B C ... D
-\end{cfa}
-The for-loop uses the enumeration type @Alphabet@ its range, and iterates through all enumerators in the order defined in the enumeration.
-@alph@ is the iterating enumeration object, which returns the value of an @Alphabet@ in this context according to the precedence rule.
-
-\textbullet\ \CFA offers a shorthand for iterating all enumeration constants:
-\begin{cfa}[label=lst:range_functions]
-for ( Alphabet alph ) { sout | alph; }
->>> A B C ... D
-\end{cfa}
-
-The following are examples for constructing for-control using an enumeration. Note that the type declaration of the iterating variable is optional, because \CFA can infer the type as EnumInstType based on the range expression, and possibly convert it to one of its attribute types.
-
-\textbullet\ H is implicit up-to exclusive range [0, H).
-\begin{cfa}[label=lst:range_function_1]
-for ( alph; Alphabet.D ) { sout | alph; }
->>> A B C
-\end{cfa}
-
-\textbullet\ ~= H is implicit up-to inclusive range [0,H].
-\begin{cfa}[label=lst:range_function_2]
-for ( alph; ~= Alphabet.D ) { sout | alph; }
->>> A B C D
-\end{cfa}
-
-\textbullet\ L ~ H is explicit up-to exclusive range [L,H).
-\begin{cfa}[label=lst:range_function_3]
-for ( alph; Alphabet.B ~ Alphabet.D  ) { sout | alph; }
-// for ( Alphabet alph = Alphabet.B; alph < Alphabet.D; alph += 1  ); 1 is one_t
->>> B C
-\end{cfa}
-
-\textbullet\ L ~= H is explicit up-to inclusive range [L,H].
-\begin{cfa}[label=lst:range_function_4]
-for ( alph; Alphabet.B ~= Alphabet.D  ) { sout | alph; }
->>> B C D
-\end{cfa}
-
-\textbullet\ L -~ H is explicit down-to exclusive range [H,L), where L and H are implicitly interchanged to make the range down-to.
-\begin{cfa}[label=lst:range_function_5]
-for ( alph; Alphabet.D -~ Alphabet.B  ) { sout | alph; }
->>> D C
-\end{cfa}
-
-\textbullet\ L -~= H is explicit down-to exclusive range [H,L], where L and H are implicitly interchanged to make the range down-to.
-\begin{cfa}[label=lst:range_function_6]
-for ( alph; Alphabet.D -~= Alphabet.B  ) { sout | alph; }
->>> D C B
-\end{cfa}
-
-A user can specify the ``step size'' of an iteration. There are two different stepping schemes of enumeration for-loop.
-\begin{cfa}[label=lst:range_function_stepping]
-enum(int) Sequence { A = 10, B = 12, C = 14, D = 16, D  = 18 };
-for ( s; Sequence.A ~= Sequence.D ~ 1  ) { sout | alph; }
->>> 10 12 14 16 18
-for ( s; Sequence.A ~= Sequence.D; s+=1  ) { sout | alph; }
->>> 10 11 12 13 14 15 16 17 18
-\end{cfa}
-The first syntax is stepping to the next enumeration constant, which is the default stepping scheme if not explicitly specified. The second syntax, on the other hand, is to call @operator+=@ @one_type@ on the @value( s )@. Therefore, the second syntax is equivalent to
-\begin{cfa}[label=lst:range_function_stepping_converted]
-for ( typeof( value(Sequence.A) ) s=value( Sequence.A ); s <= Sequence.D; s+=1  ) { sout | alph; }
->>> 10 11 12 13 14 15 16 17 18
-\end{cfa}
-
-% \PAB{Explain what each loop does.}
-
-It is also possible to iterate over an enumeration's labels, implicitly or explicitly:
-\begin{cfa}[label=lst:range_functions_label_implicit]
-for ( char * alph; Alphabet )
-\end{cfa}
-This for-loop implicitly iterates every label of the enumeration, because a label is the only valid resolution to @ch@ with type @char *@ in this case.
-If the value can also be resolved as the @char *@, you might iterate the labels explicitly with the array iteration.
-\begin{cfa}[label=lst:range_functions_label_implicit]
-for ( char * ch; labels( Alphabet ) )
-\end{cfa}
+which effectively turns the first enumeration as a logical false and true for others.
+
+% \begin{cfa}
+% Count variable_a = First, variable_b = Second, variable_c = Third, variable_d = Fourth;
+% p(variable_a); // 0
+% p(variable_b); // 1
+% p(variable_c); // "Third"
+% p(variable_d); // 3
+% \end{cfa}
+
+
+% \section{Iteration and Range}
+
+
+
+% % It is convenient to iterate over a \CFA enumeration value, \eg:
+% \CFA implements \newterm{range loop} for \CFA enumeration using the enumerated traits. The most basic form of @range loop@ is the follows:
+% \begin{cfa}[label=lst:range_functions]
+% for ( Alphabet alph; Alphabet ) { sout | alph; }
+% >>> A B C ... D
+% \end{cfa}
+% % The @range loops@ iterates through all enumerators in the order defined in the enumeration.
+% % @alph@ is the iterating enumeration object, which returns the value of an @Alphabet@ in this context according to the precedence rule.
+% Enumerated @range loop@ extends the \CFA grammar as it allows a type name @Alphabet@ 
+
+% \textbullet\ \CFA offers a shorthand for iterating all enumeration constants:
+% \begin{cfa}[label=lst:range_functions]
+% for ( Alphabet alph ) { sout | alph; }
+% >>> A B C ... D
+% \end{cfa}
+
+% The following are examples for constructing for-control using an enumeration. Note that the type declaration of the iterating variable is optional, because \CFA can infer the type as EnumInstType based on the range expression, and possibly convert it to one of its attribute types.
+
+% \textbullet\ H is implicit up-to exclusive range [0, H).
+% \begin{cfa}[label=lst:range_function_1]
+% for ( alph; Alphabet.D ) { sout | alph; }
+% >>> A B C
+% \end{cfa}
+
+% \textbullet\ ~= H is implicit up-to inclusive range [0,H].
+% \begin{cfa}[label=lst:range_function_2]
+% for ( alph; ~= Alphabet.D ) { sout | alph; }
+% >>> A B C D
+% \end{cfa}
+
+% \textbullet\ L ~ H is explicit up-to exclusive range [L,H).
+% \begin{cfa}[label=lst:range_function_3]
+% for ( alph; Alphabet.B ~ Alphabet.D  ) { sout | alph; }
+% // for ( Alphabet alph = Alphabet.B; alph < Alphabet.D; alph += 1  ); 1 is one_t
+% >>> B C
+% \end{cfa}
+
+% \textbullet\ L ~= H is explicit up-to inclusive range [L,H].
+% \begin{cfa}[label=lst:range_function_4]
+% for ( alph; Alphabet.B ~= Alphabet.D  ) { sout | alph; }
+% >>> B C D
+% \end{cfa}
+
+% \textbullet\ L -~ H is explicit down-to exclusive range [H,L), where L and H are implicitly interchanged to make the range down-to.
+% \begin{cfa}[label=lst:range_function_5]
+% for ( alph; Alphabet.D -~ Alphabet.B  ) { sout | alph; }
+% >>> D C
+% \end{cfa}
+
+% \textbullet\ L -~= H is explicit down-to exclusive range [H,L], where L and H are implicitly interchanged to make the range down-to.
+% \begin{cfa}[label=lst:range_function_6]
+% for ( alph; Alphabet.D -~= Alphabet.B  ) { sout | alph; }
+% >>> D C B
+% \end{cfa}
+
+% A user can specify the ``step size'' of an iteration. There are two different stepping schemes of enumeration for-loop.
+% \begin{cfa}[label=lst:range_function_stepping]
+% enum(int) Sequence { A = 10, B = 12, C = 14, D = 16, D  = 18 };
+% for ( s; Sequence.A ~= Sequence.D ~ 1  ) { sout | alph; }
+% >>> 10 12 14 16 18
+% for ( s; Sequence.A ~= Sequence.D; s+=1  ) { sout | alph; }
+% >>> 10 11 12 13 14 15 16 17 18
+% \end{cfa}
+% The first syntax is stepping to the next enumeration constant, which is the default stepping scheme if not explicitly specified. The second syntax, on the other hand, is to call @operator+=@ @one_type@ on the @value( s )@. Therefore, the second syntax is equivalent to
+% \begin{cfa}[label=lst:range_function_stepping_converted]
+% for ( typeof( value(Sequence.A) ) s=value( Sequence.A ); s <= Sequence.D; s+=1  ) { sout | alph; }
+% >>> 10 11 12 13 14 15 16 17 18
+% \end{cfa}
+
+% % \PAB{Explain what each loop does.}
+
+% It is also possible to iterate over an enumeration's labels, implicitly or explicitly:
+% \begin{cfa}[label=lst:range_functions_label_implicit]
+% for ( char * alph; Alphabet )
+% \end{cfa}
+% This for-loop implicitly iterates every label of the enumeration, because a label is the only valid resolution to @ch@ with type @char *@ in this case.
+% If the value can also be resolved as the @char *@, you might iterate the labels explicitly with the array iteration.
+% \begin{cfa}[label=lst:range_functions_label_implicit]
+% for ( char * ch; labels( Alphabet ) )
+% \end{cfa}
