Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 18d7aafd7ba06df826cfd83e2f922f66fd91126b)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision e561551d00f8e4e32d358a64ece5a41b29a8501b)
@@ -2,214 +2,50 @@
 
 
-\CFA supports C enumeration using the same syntax and semantics for backwards compatibility.
-\CFA also extends C-Style enumeration by adding a number of new features that bring enumerations inline with other modern programming languages.
-Any enumeration extensions must be intuitive to C programmers both in syntax and semantics.
-The following sections detail all of my new contributions to enumerations in \CFA.
-
-\begin{comment}
-	Not support. 
-\end{comment}
-% \section{Aliasing}
-
-% C already provides @const@-style aliasing using the unnamed enumerator \see{\VRef{s:TypeName}}, even if the name @enum@ is misleading (@const@ would be better).
-% Given the existence of this form, it is straightforward to extend it with types other than @int@.
-% \begin{cfa}
-% enum E { Size = 20u, PI = 3.14159L, Jack = L"John" };
-% \end{cfa}
-% which matches with @const@ aliasing in other programming languages.
-% Here, the type of the enumerator is the type of the initialization constant, \eg @typeof(20u)@ for @Size@ implies @unsigned int@.
-% Auto-initialization is restricted to the case where all constants are @int@, matching with C.
-% As seen in \VRef{s:EnumeratorTyping}, this feature is just a shorthand for multiple typed-enumeration declarations.
-
-
-\section{Enumerator Visibility}
-\label{s:EnumeratorVisibility}
-
-In C, unscoped enumerators present a \newterm{naming problem} when multiple enumeration types appear in the same scope with duplicate enumerator names.
-There is no mechanism in C to resolve these naming conflicts other than renaming one of the duplicates, which may be impossible if the conflict comes from system include files.
-
-The \CFA type-system allows extensive overloading, including enumerators.
-Furthermore, \CFA uses the environment, such as the left-had of assignment and function parameter, to pinpoint the best overloaded name. 
-% Furthermore, \CFA uses the left-hand of assignment in type resolution to pinpoint the best overloaded name.
-Finally, qualification and casting are provided to disambiguate any ambiguous situations.
-\begin{cfa}
-enum E1 { First, Second, Third, Fourth };
-enum E2 { @Fourth@, @Third@, @Second@, @First@ }; $\C{// same enumerator names}$
-E1 f() { return Third; }				$\C{// overloaded functions, different return types}$
-E2 f() { return Fourth; }
-void g(E1 e);
-void h(E2 e);
-void foo() {
-	E1 e1 = First;   E2 e2 = First;		$\C{// initialization}$
-	e1 = Second;   e2 = Second;			$\C{// assignment}$
-	e1 = f();   e2 = f();				$\C{// function return}$
-	g(First); h(First);					$\C{// function parameter}$
-	int i = @E1.@First + @E2.@First;	$\C{// disambiguate with qualification}$
-	int j = @(E1)@First + @(E2)@First;	$\C{// disambiguate with cast}$
-}
-\end{cfa}
-\CFA overloading allows programmers to use the most meaningful names without fear of name clashes within a program or from external sources, like include files.
-Experience from \CFA developers is that the type system implicitly and correctly disambiguates the majority of overloaded names, \ie it is rare to get an incorrect selection or ambiguity, even among hundreds of overloaded variables and functions.
-Any ambiguity can be resolved using qualification or casting.
-
-
-\section{Enumerator Scoping}
-
-An enumeration can be scoped, using @'!'@, so the enumerator constants are not projected into the enclosing scope.
-\begin{cfa}
-enum Week @!@ { Mon, Tue, Wed, Thu = 10, Fri, Sat, Sun };
-enum RGB @!@ { Red, Green, Blue };
-\end{cfa}
-Now the enumerators \emph{must} be qualified with the associated enumeration type.
-\begin{cfa}
-Week week = @Week.@Mon;
-week = @Week.@Sat;
-RGB rgb = @RGB.@Red;
-rgb = @RGB.@Blue;
-\end{cfa}
-It is possible to toggle back to unscoping using the \CFA @with@ clause/statement (see also \CC \lstinline[language=c++]{using enum} in Section~\ref{s:C++RelatedWork}).
-\begin{cfa}
-with ( @Week@, @RGB@ ) {				$\C{// type names}$
-	 week = @Sun@;						$\C{// no qualification}$
-	 rgb = @Green@;
-}
-\end{cfa}
-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 this localized scenario.
-
-
-\section{Enumeration Traits}
-
-\CFA 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 @CfaEnum@:
-\begin{cfa}
-forall( E ) trait CfaEnum {
-	char * label( E e );
-	unsigned int posn( E e );
-};
-\end{cfa}
-
-describes an enumeration as a named constant with position. And @TypeEnum@
-\begin{cfa}
-forall( E, V ) trait TypeEnum {
-	V value( E e );
-};	
-\end{cfa}
-asserts two types @E@ and @T@, with @T@ being the base type for the enumeration @E@. 
-
-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;
-}
-printEunm( Week.Mon );
-printEnum( RGB.Green );
-\end{cfa}
-
-\CFA does not define attribute functions for C style enumeration. But it is possilbe for users to explicitly implement
-enumeration traits for C enum and any other types.
-
-\begin{cfa}
-enum Fruit { Apple, Bear, Cherry };			$\C{// C enum}$
-char * label(Fruit f) {
-	switch(f) {
-		case Apple: "A"; break;
-		case Bear: "B"; break;
-		case Cherry: "C"; break;
-	}
-}
-unsigned posn(Fruit f) { return f; }
-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.
+% \CFA supports C enumeration using the same syntax and semantics for backwards compatibility.
+% \CFA also extends C-Style enumeration by adding a number of new features that bring enumerations inline with other modern programming languages.
+% Any enumeration extensions must be intuitive to C programmers both in syntax and semantics.
+% The following sections detail all of my new contributions to enumerations in \CFA.
+\CFA extends the enumeration declaration by parameterizing with a type (like a generic type).
+\begin{clang}[identifierstyle=\linespread{0.9}\it]
+$\it enum$-specifier:
+	enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { enumerator-list-noinit }
+	enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { enumerator-list-noinit , }
+	enum @(type-specifier$\(_{opt}\)$)@ identifier
+enumerator-list-noinit:
+	enumeration-constant
+	enumerator-list-noinit , enumeration-constant
+\end{clang}
+\CFA enumerations, or \CFA enums, have optional type declaration in a bracket next to the enum keyword.
+Without optional type declarations, the syntax defines "opaque enums".
+Otherwise, \CFA enum with type declaration are "typed enums".
+
+\section{Opaque Enum}
+\label{s:OpaqueEnum}
+Opaque enum is a special CFA enumeration type, where the internal representation is chosen by the compiler and hidden from users.
+Compared C enum, opaque enums are more restrictive in terms of typing, and cannot be implicitly converted to integers.
+Enumerators of opaque enum cannot have initializer. Declaring initializer in the body of opaque enum results in a syntax error.
 \begin{cfa}
 enum@()@ Planets { MERCURY, VENUS, EARTH, MARS, JUPITER, SATURN, URANUS, NEPTUNE };
-\end{cfa}
-
-
-In addition, \CFA implements @Bound@ and @Serial@ for \CFA Enums.
-\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{// 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 @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}
+
+Planet p = URANUS;
+@int i = VENUS; // Error, VENUS cannot be converted into an integral type@
+\end{cfa}
+Each opage enum has two @attributes@: @position@ and @label@. \CFA auto-generates @attribute functions@ @posn()@ and @label()@ for every \CFA enum to returns the respective attributes.
+\begin{cfa}
+// Auto-generated
+int posn(Planet p);
+char * s label(Planet p);
+\end{cfa}
+
+\begin{cfa}
+unsigned i = posn(VENUS); // 1
+char * s = label(MARS); // "MARS"
+\end{cfa}
+
+% \subsection{Representation}
+\CFA uses chooses signed int as the underlying representation of an opaque enum variable, holding the value of enumeration position. Therefore, @posn()@ is in fact a cast that bypassing type system, converting an 
+cfa enum to its integral representation.
+
+Labels information are stored in a global array. @label()@ is a function that maps enum position to an element of the array.
 
 \section{Typed Enum}
@@ -220,21 +56,4 @@
 Note, the synonyms @Liz@ and @Beth@ in the last declaration.
 Because enumerators are constants, the enumeration type is implicitly @const@, so all the enumerator types in Figure~\ref{f:EumeratorTyping} are logically rewritten with @const@.
-
-C has an implicit type conversion from an enumerator to its base type @int@.
-Correspondingly, \CFA has an implicit (safe) conversion from a typed enumerator to its base type.
-\begin{cfa}
-char currency = Dollar;
-string fred = Fred;						$\C{// implicit conversion from char * to \CFA string type}$
-Person student = Beth;
-\end{cfa}
-
-% \begin{cfa}
-% struct S { int i, j; };
-% enum( S ) s { A = { 3,  4 }, B = { 7,  8 } };
-% enum( @char@ ) Currency { Dollar = '$\textdollar$', Euro = '$\texteuro$', Pound = '$\textsterling$'  };
-% enum( @double@ ) Planet { Venus = 4.87, Earth = 5.97, Mars = 0.642  }; // mass
-% enum( @char *@ ) Colour { Red = "red", Green = "green", Blue = "blue"  };
-% enum( @Currency@ ) Europe { Euro = '$\texteuro$', Pound = '$\textsterling$' }; // intersection
-% \end{cfa}
 
 \begin{figure}
@@ -281,4 +100,86 @@
 calling constructors happens at runtime (dynamic).
 
+@value@ is an @attribute@ that defined for typed enum along with position and label. @values@ of a typed enum are stored in a global array of declared typed, initialized with 
+value of enumerator initializers. @value()@ functions maps an enum to an elements of the array.
+
+
+\subsection{Implicit Conversion}
+C has an implicit type conversion from an enumerator to its base type @int@.
+Correspondingly, \CFA has an implicit (safe) conversion from a typed enumerator to its base type.
+\begin{cfa}
+char currency = Dollar;
+string fred = Fred;						$\C{// implicit conversion from char * to \CFA string type}$
+Person student = Beth;
+\end{cfa}
+
+% The implicit conversion is accomplished by the compiler adding @value()@ function calls as a candidate with safe cost. Therefore, the expression
+% \begin{cfa}
+% char currency = Dollar;
+% \end{cfa}
+% is equivalent to
+% \begin{cfa}
+% char currency = value(Dollar);
+% \end{cfa}
+% Such conversion an @additional@ safe 
+
+The implicit conversion is accomplished by the resolver adding call to @value()@ functions as a resolution candidate with a @implicit@ cost.
+Implicit cost is an additional category to Aaron's cost model. It is more signicant than @unsafe@ to have
+the compiler choosing implicit conversion over the narrowing conversion; It is less signicant to @poly@ 
+so that function overloaded with enum traits will be selected over the implicit. @Enum trait@ will be discussed in the chapter.
+
+Therefore, \CFA conversion cost is 8-tuple
+@@(unsafe, implicit, poly, safe, sign, vars, specialization, reference)@@
+
+\section{Auto Initialization} 
+
+C auto-initialization works for the integral type @int@ with constant expressions.
+\begin{cfa}
+enum Alphabet ! {
+	A = 'A', B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z,
+	a = 'a', b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z
+};
+\end{cfa}
+The complexity of the constant expression depends on the level of runtime computation the compiler implements, \eg \CC \lstinline[language={[GNU]C++}]{constexpr} provides complex compile-time computation across multiple types, which blurs the compilation/runtime boundary.
+
+% The notion of auto-initialization can be generalized in \CFA through the trait @AutoInitializable@.
+% \begin{cfa}
+% forall(T) @trait@ AutoInitializable {
+% 	void ?{}( T & o, T v );				$\C{// initialization}$
+% 	void ?{}( T & t, zero_t );			$\C{// 0}$
+% 	T ?++( T & t);						$\C{// increment}$
+% };
+% \end{cfa}
+% In addition, there is an implicit enumeration counter, @ecnt@ of type @T@, managed by the compiler.
+% For example, the type @Odd@ satisfies @AutoInitializable@:
+% \begin{cfa}
+% struct Odd { int i; };
+% void ?{}( Odd & o, int v ) { if ( v & 1 ) o.i = v; else /* error not odd */ ; };
+% void ?{}( Odd & o, zero_t ) { o.i = 1; };
+% Odd ?++( Odd o ) { return (Odd){ o.i + 2 }; };
+% \end{cfa}
+% and implicit initialization is available.
+% \begin{cfa}
+% enum( Odd ) { A, B, C = 7, D };			$\C{// 1, 3, 7, 9}$
+% \end{cfa}
+% where the compiler performs the following transformation and runs the code.
+% \begin{cfa}
+% enum( Odd ) {
+% 	?{}( ecnt, @0@ }  ?{}( A, ecnt },	?++( ecnt )  ?{}( B, ecnt ),
+% 	?{}( ecnt, 7 )  ?{}( C, ecnt ),	?++( ecnt )  ?{}( D, ecnt )
+% };
+% \end{cfa}
+
+The notion of auto-initialization is generalized in \CFA enum in the following way:
+Enumerator e is the first enumerator of \CFA enumeration E with base type T. If e declares no no initializer, e is auto-initialized by the $zero\_t$ constructor of T.
+\CFA reports a compile time error if T has no $zero\_t$ constructor.
+Enumerator e is an enumerator of base-type T enumeration E that position i, where $i \neq 0$. And d is the enumerator with position @i-1@, e is auto-initialized with 
+the result of @value(d)++@. If operator @?++@ is not defined for type T, \CFA reports a compile time error.
+
+Unfortunately, auto-initialization is not implemented because \CFA is only a transpiler, relying on generated C code to perform the detail work.
+C does not have the equivalent of \CC \lstinline[language={[GNU]C++}]{constexpr}, and it is currently beyond the scope of the \CFA project to implement a complex runtime interpreter in the transpiler.
+Nevertheless, the necessary language concepts exist to support this feature.
+
+
+
 \section{Enumeration Inheritance}
 
@@ -291,5 +192,5 @@
 \end{cfa}
 
-Enumeration @Name2@ inherits all the enumerators and their values from enumeration @Names@ by containment, and a @Names@ enumeration is a subtype of enumeration @Name2@.
+Enumeration @Name2@ inherits all the enumerators and their values from enumeration @Names@ by containment, and a @Names@ enumeration is a @subtype@ of enumeration @Name2@.
 Note, that enumerators must be unique in inheritance but enumerator values may be repeated.
 
@@ -301,10 +202,66 @@
 Names $\(\subset\)$ Names2 $\(\subset\)$ Names3 $\C{// enum type of Names}$
 \end{cfa}
-A subtype can be cast to its supertype, assigned to a supertype variable, or be used as a function argument that expects the supertype.
-\begin{cfa}
-Names fred = Name.Fred;
-(Names2) fred; (Names3) fred; (Name3) Names.Jack;  $\C{// cast to super type}$
-Names2 fred2 = fred; Names3 fred3 = fred2; $\C{// assign to super type}$
-\end{cfa}
+
+Inlined from \CFA enumeration @O@, new enumeration @N@ copies all enumerators from @O@, including those @O@ obtains through inheritance. Enumerators inherited from @O@
+keeps same @label@ and @value@, but @position@ may shift to the right if other enumerators or inline enumeration declared in prior of @inline A@.
+\begin{cfa}
+enum() Phynchocephalia { Tuatara };
+enum() Squamata { Snake, Lizard };
+enum() Lepidosauromorpha { inline Phynchocephalia, inline Squamata, Kuehneosauridae };
+\end{cfa}
+Snake, for example, has the position 0 in Squamata, but 1 in Lepidosauromorpha as Tuatara inherited from Phynchocephalia is position 0 in Lepidosauromorpha.
+
+A subtype enumeration can be casted, or implicitly converted into its supertype, with a safe cost.
+\begin{cfa}
+enum Squamata squamata_lizard = Lizard;
+posn(quamata_lizard); // 1
+enum Lepidosauromorpha lepidosauromorpha_lizard = squamata_lizard;
+posn(lepidosauromorpha_lizard); // 2
+void foo( Lepidosauromorpha l );
+foo( squamata_lizard );
+posn( (Lepidosauromorpha) squamata_lizard ); // 2
+
+Lepidosauromorpha s = Snake;
+\end{cfa}
+The last expression in the preceding example is umabigious. While both @Squamata.Snake@ and @Lepidosauromorpha.Snake@ are valid candidate, @Squamata.Snake@ has
+an associated safe cost and \CFA select the zero cost candidate @Lepidosauromorpha.Snake@. 
+
+As discussed in \VRef{s:OpaqueEnum}, \CFA chooses position as a representation of \CFA enum. Conversion involves both change of typing
+and possibly @position@.
+
+When converting a subtype to a supertype, the position can only be a larger value. The difference between the position in subtype and in supertype is an "offset".
+\CFA runs a the following algorithm to determine the offset for an enumerator to a super type. 
+% In a summary, \CFA loops over members (include enumerators and inline enums) of the supertype.
+% If the member is the matching enumerator, the algorithm returns its position.
+% If the member is a inline enumeration, the algorithm trys to find the enumerator in the inline enumeration. If success, it returns the position of enumerator in the inline enumeration, plus 
+% the position in the current enumeration. Otherwises, it increase the offset by the size of inline enumeration.
+
+\begin{cfa}
+struct Enumerator;
+struct CFAEnum {
+	vector<variant<CFAEnum, Enumerator>> members;
+};
+pair<bool, int> calculateEnumOffset( CFAEnum dst, Enumerator e ) {
+	int offset = 0;
+	for( auto v: dst.members ) {
+		if ( v.holds_alternative<Enumerator>() ) {
+			auto m = v.get<Enumerator>();
+			if ( m == e ) return make_pair( true, 0 );
+			offset++;
+		} else {
+			auto p = calculateEnumOffset( v, e );
+			if ( p.first ) return make_pair( true, offset + p.second );
+			offset += p.second;
+		}
+	}
+	return make_pair( false, offset );
+}
+\end{cfa}
+
+% \begin{cfa}
+% Names fred = Name.Fred;
+% (Names2) fred; (Names3) fred; (Name3) Names.Jack;  $\C{// cast to super type}$
+% Names2 fred2 = fred; Names3 fred3 = fred2; $\C{// assign to super type}$
+% \end{cfa}
 For the given function prototypes, the following calls are valid.
 \begin{cquote}
@@ -326,4 +283,145 @@
 \end{cquote}
 Note, the validity of calls is the same for call-by-reference as for call-by-value, and @const@ restrictions are the same as for other types.
+
+
+
+\section{Enumeration Traits}
+
+\CFA 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 @CfaEnum@:
+\begin{cfa}
+forall( E ) trait CfaEnum {
+	char * label( E e );
+	unsigned int posn( E e );
+};
+\end{cfa}
+
+describes an enumeration as a named constant with position. And @TypeEnum@
+\begin{cfa}
+forall( E, V ) trait TypeEnum {
+	V value( E e );
+};	
+\end{cfa}
+asserts two types @E@ and @T@, with @T@ being the base type for the enumeration @E@. 
+
+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;
+}
+printEunm( Week.Mon );
+printEnum( RGB.Green );
+\end{cfa}
+
+\CFA does not define attribute functions for C style enumeration. But it is possilbe for users to explicitly implement
+enumeration traits for C enum and any other types.
+
+\begin{cfa}
+enum Fruit { Apple, Bear, Cherry };			$\C{// C enum}$
+char * label(Fruit f) {
+	switch(f) {
+		case Apple: "A"; break;
+		case Bear: "B"; break;
+		case Cherry: "C"; break;
+	}
+}
+unsigned posn(Fruit f) { return f; }
+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 Enums.
+\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{// 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 @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}
+
+
+
+
 
 \section{Enumerator Control Structures}
Index: doc/theses/jiada_liang_MMath/background.tex
===================================================================
--- doc/theses/jiada_liang_MMath/background.tex	(revision 18d7aafd7ba06df826cfd83e2f922f66fd91126b)
+++ doc/theses/jiada_liang_MMath/background.tex	(revision e561551d00f8e4e32d358a64ece5a41b29a8501b)
@@ -129,9 +129,8 @@
 
 
-\subsection{Implementation}
-
-In theory, a C enumeration \emph{variable} is an implementation-defined integral type large enough to hold all enumerator values.
+\subsection{Representation}
+
+C standard specifies enumeration \emph{variable} is an implementation-defined integral type large enough to hold all enumerator values.
 In practice, C uses @int@ as the underlying type for enumeration variables, because of the restriction to integral constants, which have type @int@ (unless qualified with a size suffix).
-
 
 \subsection{Usage}
@@ -198,2 +197,210 @@
 \bigskip
 While C provides a true enumeration, it is restricted, has unsafe semantics, and does provide useful enumeration features in other programming languages.
+
+\section{\CFA Polymorphism}
+\subsection{Function Overloading}
+Function overloading is programming languages feature wherein functions may share the same name, but with different function signatures. In both C++ and \CFA, function names can be overloaded 
+with different entities as long as they are different in terms of the number and type of parameters.
+
+\begin{cfa}
+void f(); // (1)
+void f(int); // (2); Overloaded on the number of parameters
+void f(char); // (3); Overloaded on parameter type
+
+f('A');
+\end{cfa}
+In this case, the name f is overloaded with a nullity function and two arity functions with different parameters types. Exactly which precedures being executed
+is determined based on the passing arguments. The last expression of the preceding example calls f with one arguments, narrowing the possible candidates down to (2) and (3).
+Between those, function argument 'A' is an exact match to the parameter expected by (3), while needing an @implicit conversion@ to call (2). The compiler determines (3) is the better candidates among
+and procedure (3) is being executed.
+
+\begin{cfa}
+int f(int); // (4); Overloaded on return type
+[int, int] f(int); // (5) Overloaded on the number of return value
+\end{cfa}
+The function declarations (4) and (5) show the ability of \CFA functions overloaded with different return value, a feature that is not shared by C++.
+
+
+\subsection{Operator Overloading}
+Operators in \CFA are specialized function and are overloadable by with specially-named functions represents the syntax used to call the operator.
+% For example, @bool ?==?T(T lhs, T rhs)@ overloads equality operator for type T, where @?@ is the placeholders for operands for the operator.
+\begin{cfa}
+enum Weekday { Monday, Tuesday, Wednesday, Thursday, Friday, Saturday, Sunday };
+bool ?<?(const Weekday a, const Weekday b) {
+	return ((int)a + 1);
+}
+Monday < Sunday; // False
+?<?( Monday, Sunday ); // Equivalent syntax
+\end{cfa}
+Unary operators are functions that takes one argument and have name @operator?@ or @?operator@, where @?@ is the placeholders for operands.
+Binary operators are function with two parameters. They are overloadable with function name @?operator?@.
+
+\subsection{Constructor and Destructor}
+In \CFA, all objects are initialized by @constructors@ during its allocation, including basic types, 
+which are initialized by constructors default-generated by a compiler.
+
+Constructors are overloadable functions with name @?{}@, return @void@, and have at least one parameter, which is a reference
+to the object being constructored (Colloquially referred to "this" or "self" in other language).
+
+\begin{cfa}
+struct Employee {
+	const char * name;
+	double salary;
+};
+
+void ?{}( Employee& this, const char * name, double salary ) {
+    this.name = name;
+    this.salary = salary;
+}
+
+Employee Sara { "Sara Schmidt", 20.5 };
+\end{cfa}
+Like Python, the "self" reference is implicitly passed to a constructor. The Employee constructors takes two additional arugments used in its
+field initialization.
+
+A destructor in \CFA is a function that has name @^?{}@. It returns void, and take only one arugment as its "self".
+\begin{cfa}
+void ^?{}( Employee& this ) {
+    free(this.name);
+    this.name = 0p;
+    this.salary = 0;
+}
+\end{cfa}
+Destructor can be explicitly evoked as a function call, or implicitly called at the end of the block in which the object is delcared.
+\begin{cfa}
+{
+^Sara{};
+Sara{ "Sara Craft", 20 };
+} // ^Sara{}
+\end{cfa}
+
+\subsection{Variable Overloading}
+C and C++ disallow more than one variable declared in the same scope with the same name. When a variable declare in a inner scope has the same name as 
+a variable in an outer scope, the outer scope variable is "shadowed" by the inner scope variable and cannot be accessed directly. 
+
+\CFA has variable overloading: multiple variables can share the same name in the same scope, as long as they have different type. Name shadowing only 
+happens when the inner scope variable and the outer scope ones have the same type.
+\begin{cfa}
+double i = 6.0;
+int i = 5;
+void foo( double i ) { sout | i; } // 6.0
+\end{cfa}
+
+\subsection{Special Literals}
+Literal 0 has special meanings within different contexts: it can means "nothing" or "empty", an additive identity in arithmetic, a default value as in C (null pointer), 
+or an initial state.
+Awaring of its significance, \CFA provides a special type for the 0 literal, @zero_t@, to define the logical @zero@ for custom types.
+\begin{cfa}
+struct S { int i, j; };
+void ?{}( S & this, @zero_t@ ) { this.i = 0; this.j = 0; } // zero_t, no parameter name allowed
+S s0 = @0@;
+\end{cfa}
+Overloading @zero_t@ for S provides new definition for @zero@ of type S.
+
+According to the C standard, @0@ is the @only@ false value. Any values compares equals to @0@ is false, and not euqals @0@ is true. As a consequence, control structure 
+such as @if()@ and @while()@ only runs it true clause when its predicate @not equals@ to @0@. 
+
+\CFA generalizes this concept and allows to logically overloads the boolean value for any type by overloading @not equal@ comparison against @zero_t@.
+\begin{cfa}
+int ?@!=@?( S this, @zero_t@ ) { return this.i != 0 && this.j != 0; }
+\end{cfa}
+
+% In C, the literal 0 represents the Boolean value false. The expression such as @if (x)@ is equivalent to @if (x != 0)@ .
+% \CFA allows user to define the logical zero for a custom type by overloading the @!=@ operation against a special type, @zero_t@, 
+% so that an expression with the custom type can be used as a predicate without the need of conversion to the literal 0.
+% \begin{cfa}
+% struct S s;
+% int ?!=?(S, zero_t);
+% if (s) {}
+% \end{cfa}
+Literal 1 is also special. Particularly in C, the pre-increment operator and post-increment operator can be interpreted in terms of @+= 1@.
+The logical @1@ in \CFA is represented by special type @one_t@.
+\begin{cfa}
+void ?{}( S & this, one_t ) { this.i = 1; this.j = 1; }	// one_t, no parameter name allowed
+S & ?+=?( S & this, one_t ) { this.i += 1; this.j += 1; return op; }
+\end{cfa}
+Without explictly overloaded by a user, \CFA uses the user-defined @+=(S&, one_t)@ to interpret @?++@ and @++?@, as both are polymorphic functions in \CFA.
+
+\subsection{Polymorphics Functions}
+Parametric-Polymorphics functions are the functions that applied to all types. \CFA functions are parametric-polymorphics when 
+they are written with the @forall@ clause.
+
+\begin{cfa}
+forall(T)
+T identity(T x) { return x; }
+identity(42);
+\end{cfa}
+The identity function accepts a value from any type as an arugment, and the type parameter @T@ is bounded to @int@ when the function
+is called with 42. 
+
+The forall clause can takes @type assertions@ that restricts the polymorphics type. 
+\begin{cfa}
+forall( T | { void foo(T); } )
+void bar(T t) { foo(t); }
+
+struct S {} s;
+void foo(struct S);
+
+bar(s);
+\end{cfa}
+The assertion on @T@ restricts the range of types for bar to only those implements foo with the matching a signature, so that bar() 
+can call @foo@ in its body with type safe.
+Calling on type with no mathcing @foo()@ implemented, such as int, causes a compile time type assertion error. 
+
+A @forall@ clause can asserts on multiple types and with multiple asserting functions. A common practice in \CFA is to group
+the asserting functions in to a named @trait@ . 
+
+\begin{cfa}
+trait Bird(T) {
+	int days_can_fly(T i);
+	void fly(T t);
+};
+
+forall(B | Bird(B)) {
+	void bird_fly(int days_since_born, B bird) {
+		if (days_since_born > days_can_fly(bird)) {
+			fly(bird);
+		}
+	}
+}
+
+struct Robin {} r;
+int days_can_fly(Robin r) { return 23; }
+void fly(Robin r) {}
+
+bird_fly( r );
+\end{cfa}
+
+Grouping type assertions into named trait effectively create a reusable interface for parametrics polymorphics types.
+
+\section{Expression Resolution}
+
+The overloading feature poses a challenge in \CFA expression resolution. Overloadeded identifiers can refer multiple 
+candidates, with multiples being simultaneously valid. The main task of \CFA resolver is to identity a best candidate that
+involes less implicit conversion and polymorphism.
+
+\subsection{Conversion Cost}
+In C, functions argument and parameter type does not need to be exact match, and the compiler performs an @implicit conversion@ on argument.
+\begin{cfa}
+void foo(double i);
+foo(42);
+\end{cfa}
+The implicit conversion in C is relatively simple because of the abscence of overloading, with the exception of binary operators, for which the 
+compiler needs to find a common type of both operands and the result. The pattern is known as "usual arithmetic conversions".
+
+\CFA generalizes C implicit conversion to function overloading as a concept of @conversion cost@.
+Initially designed by Bilson, conversion cost is a 3-tuple, @(unsafe, poly, safe)@, where unsafe is the number of narrowing conversion,
+poly is the count of polymorphics type binding, and safe is the sum of the degree of widening conversion. Every 
+basic type in \CFA has been assigned with a @distance to Byte@, or @distance@, and the degree of widening conversion is the difference between two distances.
+
+Aaron extends conversion cost to a 7-tuple, 
+@@(unsafe, poly, safe, sign, vars, specialization, reference)@@. The summary of Aaron's cost model is the following:
+\begin{itemize}
+\item Unsafe is the number of argument that implicitly convert to a type with high rank.
+\item Poly accounts for number of polymorphics binding in the function declaration.
+\item Safe is sum of distance (add reference/appendix later).
+\item Sign is the number of sign/unsign variable conversion.
+\item Vars is the number of polymorphics type declared in @forall@.
+\item Specialization is opposite number of function declared in @forall@. More function declared implies more constraint on polymorphics type, and therefore has the lower cost.
+\item Reference is number of lvalue-to-rvalue conversion.
+\end{itemize}
Index: doc/theses/jiada_liang_MMath/implementation.tex
===================================================================
--- doc/theses/jiada_liang_MMath/implementation.tex	(revision 18d7aafd7ba06df826cfd83e2f922f66fd91126b)
+++ doc/theses/jiada_liang_MMath/implementation.tex	(revision e561551d00f8e4e32d358a64ece5a41b29a8501b)
@@ -1,29 +1,3 @@
 \chapter{Enumeration Implementation}
-
-
-\section{Enumeration Variable}
-
-Although \CFA enumeration captures three different attributes, an enumeration instance does not store all this information.
-The @sizeof@ a \CFA enumeration instance is always 4 bytes, the same size as a C enumeration instance (@sizeof( int )@).
-It comes from the fact that:
-\begin{enumerate}
-\item
-a \CFA enumeration is always statically typed;
-\item
-it is always resolved as one of its attributes regarding real usage.
-\end{enumerate}
-When creating an enumeration instance @colour@ and assigning it with the enumerator @Color.Green@, the compiler allocates an integer variable and stores the position 1.
-The invocations of $positions()$, $value()$, and $label()$ turn into calls to special functions defined in the prelude:
-\begin{cfa}
-position( green );
->>> position( Colour, 1 ) -> int
-value( green );
->>> value( Colour, 1 ) -> T
-label( green );
->>> label( Colour, 1) -> char *
-\end{cfa}
-@T@ represents the type declared in the \CFA enumeration defined and @char *@ in the example.
-These generated functions are $Companion Functions$, they take an $companion$ object and the position as parameters.
-
 
 \section{Enumeration Data}