Index: doc/theses/jiada_liang_MMath/implementation.tex
===================================================================
--- doc/theses/jiada_liang_MMath/implementation.tex	(revision 10a99d87259c93fc17a6d7791c541fee72559acc)
+++ doc/theses/jiada_liang_MMath/implementation.tex	(revision d1276f834644df5d85a59dd125d428416d44dbed)
@@ -1,3 +1,157 @@
 \chapter{Enumeration Implementation}
+
+
+
+\section{Enumeration Traits}
+
+\CFA defines a 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 @CfaEnum@:
+\begin{cfa}
+forall( E ) trait CfaEnum {
+	const char * @label@( E e );
+	unsigned int @posn@( E e );
+};
+\end{cfa}
+asserts an enumeration type @E@ has named enumerator constants (@label@) with positions (@posn@).
+
+The trait @TypedEnum@ extends @CfaEnum@:
+\begin{cfa}
+forall( E, V | CfaEnum( E ) ) trait TypedEnum {
+	V @value@( E e );
+};
+\end{cfa}
+asserting an enumeration type @E@ can have homogeneous enumerator values of type @V@.
+
+The declarative syntax
+\begin{cfa}
+enum(T) E { A = ..., B = ..., C = ... };
+\end{cfa}
+creates an enumerated type E with @label@, @posn@ and @value@ implemented automatically.
+\begin{cfa}
+void foo( T t ) { ... }
+void bar(E e) {
+	choose ( e ) {
+		case A: printf( "\%d", posn( e) );
+		case B: printf( "\%s", label( e ) );
+		case C: foo( value( e ) );
+	} 
+}
+\end{cfa}
+
+Implementing general functions across all enumeration types is possible by asserting @CfaEnum( E, T )@, \eg:
+\begin{cfa}
+#include <string.hfa>
+forall( E, T | CfaEnum( E, T ) | {unsigned int toUnsigned(T)} )
+string formatEnum( E e ) {
+	unsigned int v = toUnsigned( value( e ) );
+	string out = label(e) + '(' + v +')';
+	return out;
+}
+formatEnum( Week.Mon );
+formatEnum( RGB.Green );
+\end{cfa}
+
+\CFA does not define attribute functions for C-style enumeration.
+But it is possible for users to explicitly implement enumeration traits for C enum and any other types.
+\begin{cfa}
+enum Fruit { Apple, Pear, Cherry };			$\C{// C enum}$
+const char * label( Fruit f ) {
+	choose ( f ) {
+		case Apple: return "Apple";
+		case Bear: return "Pear";
+		case Cherry: return "Cherry";
+	}
+}
+unsigned posn( Fruit f ) { return f; }
+const char * value( Fruit f ) { return ""; } $\C{// value can return any non void type}$
+formatEnum( Apple );						$\C{// Fruit is now a \CFA enum}$
+\end{cfa}
+
+A type that implements trait @CfaEnum@, \ie, a type has no @value@, is called an opaque enum.
+
+% \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}
+
+
+In addition, \CFA implements @Bound@ and @Serial@ for \CFA enumerations.
+\begin{cfa}
+forall( E ) trait Bounded {
+	E first();
+	E last();
+};
+\end{cfa}
+The function @first()@ and @last()@ of enumerated type E return the first and the last enumerator declared in E, respectively. \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 because both Workday and Planet implement Bounded}$
+sout | @last()@;
+Workday day = first();					$\C{// day provides type Workday}$
+void foo( Planet p );
+foo( last() );							$\C{// argument 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 @succ( E e )@ and @pred( E e )@ 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@.
+
+Finally, there is an associated trait defining comparison operators among enumerators. 
+\begin{cfa}
+forall( E, T | CfaEnum( 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}
+
+As an alternative, users can define the boolean conversion for CfaEnum:
+
+\begin{cfa}
+forall(E | CfaEnum(E))
+bool ?!=?(E lhs, zero_t) {
+	return posn(lhs) != 0;
+}
+\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}