Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
@@ -0,0 +1,274 @@
+\chapter{\CFA-Style Enum}
+
+
+\CFA supports C-Style 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.
+
+
+\section{Enumerator Name Resolution}
+\label{s:EnumeratorNameResolution}
+
+In C, unscoping of enumerators presents 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 of one of the duplicates, which may be impossible.
+
+The \CFA type-system allows extensive overloading, including enumerators.
+Furthermore, \CFA uses the left-hand of assignment in type resolution to pinpoint the best overloaded name.
+Finally, qualification is provided to disambiguate any ambiguous situations.
+\begin{cfa}
+enum C1 { First, Second, Third, Fourth };
+enum C2 { @Fourth@, @Third@, @Second@, @First@ };
+C1 p() { return Third; }				$\C{// correctly resolved duplicate names}$
+C2 p() { return Fourth; }
+void foo() {
+	C1 e1 = First;   C2 e2 = First;
+	e1 = Second;   e2 = Second;
+	e1 = p();   e2 = p();				$\C{// correctly resolved function call}$
+	int i = @C1.@First + @C2.@First;	$\C{// ambiguous without qualification}$
+}
+\end{cfa}
+\CFA overloading allows programmers to use the most meaningful names without fear of unresolvable clashes from included files, which are correctable with qualification.
+
+
+\section{Enumerator Scoping}
+
+An enumeration can be scoped, so the enumerator constants are not projected into the enclosing scope, using @'!'@.
+\begin{cfa}
+enum Weekday @!@ { /* as above */ };
+enum( char * ) Names @!@ { /* as above */ };
+\end{cfa}
+Now the enumerators \emph{must} be qualified with the associated enumeration.
+\begin{cfa}
+Weekday weekday = @Weekday@.Monday;
+Names names = @Names.@Fred;
+names = @Names.@Jane;
+\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}
+Weekday weekday;
+with ( @Weekday@, @Names@ ) {			$\C{// type names}$
+	 Names names = @Fred@;
+	 names = @Jane@;
+	 weekday = Saturday;
+}
+\end{cfa}
+As in Section~\ref{s:EnumeratorNameResolution}, opening multiple unscoped enumerations can result in duplicate enumeration names, but \CFA type resolution and falling back to explicit qualification handles name resolution.
+
+\section{Enumerator Typing}
+
+\CFA extends the enumeration declaration by parameterizing with a type (like a generic type), allowing enumerators to be assigned any values from the declared type.
+Figure~\ref{f:EumeratorTyping} shows a series of examples illustrating that all \CFA types can be use with an enumeration and each type's constants used to set the enumerator constants.
+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 rewritten with @const@.
+A typed enumeration has an implicit (safe) conversion 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}
+\begin{cfa}
+// integral
+	enum( @char@ ) Currency { Dollar = '$\textdollar$', Euro = '$\texteuro$', Pound = '$\textsterling$'  };
+	enum( @signed char@ ) srgb { Red = -1, Green = 0, Blue = 1 };
+	enum( @long long int@ ) BigNum { X = 123_456_789_012_345,  Y = 345_012_789_456_123 };
+// non-integral
+	enum( @double@ ) Math { PI_2 = 1.570796, PI = 3.141597, E = 2.718282 };
+	enum( @_Complex@ ) Plane { X = 1.5+3.4i, Y = 7+3i, Z = 0+0.5i };
+// pointer
+	enum( @char *@ ) Names { Fred = "FRED", Mary = "MARY", Jane = "JANE" };
+	int i, j, k;
+	enum( @int *@ ) ptr { I = &i,  J = &j,  K = &k };
+	enum( @int &@ ) ref { I = i,   J = j,   K = k };
+// tuple
+	enum( @[int, int]@ ) { T = [ 1, 2 ] }; $\C{// new \CFA type}$
+// function
+	void f() {...}   void g() {...}
+	enum( @void (*)()@ ) funs { F = f,  G = g };
+// aggregate
+	struct Person { char * name; int age, height; };
+@***@enum( @Person@ ) friends { @Liz@ = { "ELIZABETH", 22, 170 }, @Beth@ = Liz, Jon = { "JONATHAN", 35, 190 } };
+\end{cfa}
+\caption{Enumerator Typing}
+\label{f:EumeratorTyping}
+\end{figure}
+
+Typed enumerations deals with the \emph{harmonizing} problem between an enumeration and any companion data.
+The following example is from the \CFA compiler, written in \CC.
+\begin{cfa}
+enum integral_types { chr, schar, uschar, sshort, ushort, sint, usint, ..., NO_OF_ITYPES };
+char * integral_names[NO_OF_ITYPES] = {
+	"char", "signed char", "unsigned char",
+	"signed short int", "unsigned short int",
+	"signed int", "unsigned int",
+	...
+};
+\end{cfa}
+The \emph{harmonizing} problem occurs because the enumeration declaration is in one header file and the names are declared in another translation unit.
+It is up to the programmer to ensure changes made in one location are harmonized with the other location (by identifying this requirement within a comment).
+The typed enumeration largely solves this problem by combining and managing the two data types.
+\begin{cfa}
+enum( char * ) integral_types {
+	chr = "char", schar = "signed char", uschar = "unsigned char",
+	sshort = "signed short int", ushort = "unsigned short int",
+	sint = "signed int", usint = "unsigned int",
+	...
+};
+\end{cfa}
+Note, the enumeration type can be a structure (see @Person@ in Figure~\ref{f:EumeratorTyping}), so it is possible to have the equivalent of multiple arrays of companion data using an array of structures.
+
+
+\section{Pure Enumerators}
+
+An empty enumerator type, @enum()@, implies the enumerators are pure symbols without values but set properties;
+hence, there is no default conversion to @int@. 
+
+\begin{cfa}
+enum() Mode { O_RDONLY, O_WRONLY, O_CREAT, O_TRUNC, O_APPEND };
+@***@Mode iomode = O_RDONLY;
+bool b = iomode == O_RDONLY || iomode < O_APPEND;
+int i = iomode;							$\C{\color{red}// disallowed}$
+\end{cfa}
+
+\section{Enumerator Subset}
+
+If follows from enumerator typing that the enumerator type can be another enumerator.
+\begin{cfa}
+enum( @char@ ) Currency { Dollar = '$\textdollar$', Euro = '$\texteuro$', Pound = '$\textsterling$'  };
+enum( @Currency@ ) Europe { Euro = Currency.Euro, Pound = Currency.Pound }; // intersection
+enum( char ) Letter { A = 'A',  B = 'B', C = 'C', ..., Z = 'Z' };
+enum( @Letter@ ) Greek { Alph = A, Beta = B, ..., Zeta = Z }; // intersection
+\end{cfa}
+Subset enumerations may have more or less enumerators than their typed enumeration, but the enumerator values must be from the typed enumeration.
+For example, @Greek@ enumerators are a subset of type @Letter@ and are type compatible with enumeration @Letter@, but @Letter@ enumerators are not type compatible with enumeration @Greek@. 
+\begin{cfa}
+Letter letter = A;
+@***@Greak greek = Beta;
+letter = Beta;							$\C{// allowed, letter == B}$
+greek = A;								$\C{\color{red}// disallowed}$
+\end{cfa}
+
+
+\section{Enumeration Inheritance}
+
+\CFA Plan-9 inheritance may be used with enumerations, where Plan-9 inheritance is containment inheritance with implicit unscoping (like a nested unnamed @struct@/@union@ in C).
+\begin{cfa}
+enum( char * ) Names { /* as above */ };
+enum( char * ) Names2 { @inline Names@, Jack = "JACK", Jill = "JILL" };
+@***@enum /* inferred */ Names3 { @inline Names2@, Sue = "SUE", Tom = "TOM" };
+\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@.
+Note, enumerators must be unique in inheritance but enumerator values may be repeated.
+
+The enumeration type for the inheriting type must be the same as the inherited type;
+hence the enumeration type may be omitted for the inheriting enumeration and it is inferred from the inherited enumeration, as for @Name3@.
+% When inheriting from integral types, automatic numbering may be used, so the inheritance placement left to right is important.
+Specifically, the inheritance relationship for @Names@ is:
+\begin{cfa}
+Names $\(\subset\)$ Names2 $\(\subset\)$ Names3 $\(\subset\)$ const char * $\C{// enum type of Names}$
+\end{cfa}
+For the given function prototypes, the following calls are valid.
+\begin{cquote}
+\begin{tabular}{ll}
+\begin{cfa}
+void f( Names );
+void g( Names2 );
+void h( Names3 );
+void j( const char * );
+\end{cfa}
+&
+\begin{cfa}
+f( Fred );
+g( Fred );   g( Jill );
+h( Fred );   h( Jill );   h( Sue );
+j( Fred );   j( Jill );   j( Sue );   j( "WILL" );
+\end{cfa}
+\end{tabular}
+\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 Pseudo-functions}
+
+Pseudo-functions are function-like operators that do not result in any run-time computations, i.e., like @sizeof@, @offsetof@, @typeof@.
+Often a call to a pseudo-function is substituted with information extracted from the symbol table at compilation time, like storage size or alignment associated with the underlying architecture..
+
+The attributes of an enumerator are accessed by pseudo-functions @position@, @value@, and @label@.
+\begin{cfa}
+@***@int jane_pos = @position@( Names.Jane );   $\C{// 2}$
+@***@char * jane_value = @value@( Names.Jane ); $\C{// "JANE"}$
+@***@char * jane_label = @label@( Names.Jane ); $\C{// "Jane"}$
+sout | @label@( Names.Jane ) | @value@( Names.Jane );
+\end{cfa}
+Note the ability to print both enumerator label and value.
+
+
+\section{Enumerator Position or Value}
+
+Enumerators can be used in multiple contexts.
+In most programming languages, an enumerator is implicitly converted to its value (like a typed macro substitution).
+However, enumerator synonyms and typed enumerations make this implicit conversion to value incorrect in some contexts.
+In these contexts, a programmer's initition assumes an implicit conversion to postion.
+
+For example, an intuitive use of enumerations is with the \CFA @switch@/@choose@ statement, where @choose@ performs an implict @break@ rather than a fall-through at the end of a @case@ clause.
+\begin{cquote}
+\begin{cfa}
+enum Count { First, Second, Third, Fourth };
+Count e;
+\end{cfa}
+\begin{tabular}{ll}
+\begin{cfa}
+
+choose( e ) {
+	case @First@: ...;
+	case @Second@: ...;
+	case @Third@: ...;
+	case @Fourth@: ...;
+}
+\end{cfa}
+&
+\begin{cfa}
+// rewrite
+choose( @value@( e ) ) {
+	case @value@( First ): ...;
+	case @value@( Second ): ...;
+	case @value@( Third ): ...;
+	case @value@( Fourth ): ...;
+}
+\end{cfa}
+\end{tabular}
+\end{cquote}
+Here, the intuitive code on the left is implicitly transformed into the statndard implementation on the right, using the value of the enumeration variable and enumerators.
+However, this implementation is fragile, e.g., if the enumeration is changed to:
+\begin{cfa}
+enum Count { First, Second, Third @= First@, Fourth };
+\end{cfa}
+which make @Third == First@ and @Fourth == Second@, causing a compilation error because of duplicase @case@ clauses.
+To better match with programmer intuition, \CFA toggles between value and position semantics depneding on the language context.
+For conditional clauses and switch statments, \CFA uses the robust position implementation.
+\begin{cfa}
+choose( @position@( e ) ) {
+	case @position@( First ): ...;
+	case @position@( Second ): ...;
+	case @position@( Third ): ...;
+	case @position@( Fourth ): ...;
+}
+\end{cfa}
+
+\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}
Index: doc/theses/jiada_liang_MMath/background.tex
===================================================================
--- doc/theses/jiada_liang_MMath/background.tex	(revision 6bd9f9e171271e7c6ac898b1dbf78fc75e68e592)
+++ doc/theses/jiada_liang_MMath/background.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
@@ -1,1 +1,52 @@
 \chapter{Background}
+
+
+\section{C-Style Enum}
+
+The C-Style enumeration has the following syntax and semantics.
+\begin{cfa}
+enum Weekday { Monday, Tuesday, Wednesday, Thursday@ = 10@, Friday, Saturday, Sunday };
+\end{cfa}
+Enumerators without an explicitly designated constant value are \Newterm{auto-initialized} by the compiler: from left to right, starting at zero or the next explicitly initialized constant, incrementing by @1@.
+For example, @Monday@ to @Wednesday@ are implicitly assigned with constants @0@--@2@, @Thursday@ is explicitly set to constant @10@, and @Friday@ to @Sunday@ are implicitly assigned with constants @11@--@13@.
+Initialization may occur in any order.
+\begin{cfa}
+enum Weekday { Thursday@ = 10@, Friday, Saturday, Sunday, Monday@ = 0@, Tuesday, Wednesday };
+\end{cfa}
+Note, the comma in the enumerator list can be a terminator or a separator, allowing the list to end with a dangling comma.
+\begin{cfa}
+enum Weekday {
+	Thursday = 10, Friday, Saturday, Sunday,
+	Monday = 0, Tuesday, Wednesday@,@ // terminating comma
+};
+\end{cfa}
+This feature allow enumerator lines to be interchanged without moving a comma.\footnote{
+A terminating comma appears in other C syntax, e.g., the initializer list.}
+Finally, C enumerators are \Newterm{unscoped}, i.e., enumerators declared inside of an @enum@ are visible (projected) into the enclosing scope of the @enum@ type.
+
+In theory, a C enumeration \emph{variable} is an implementation-defined integral type large enough to hold all enumerated values.
+In practice, since integral constants are used, which have type @int@ (unless qualified with a size suffix), C uses @int@ as the underlying type for enumeration variables.
+Finally, there is an implicit bidirectional conversion between an enumeration and integral types.
+\begin{cfa}
+{
+	enum Weekday { /* as above */ };	$\C{// enumerators implicitly projected into local scope}$
+	Weekday weekday = Monday;			$\C{// weekday == 0}$
+	weekday = Friday;					$\C{// weekday == 11}$
+	int i = Sunday;						$\C{// implicit conversion to int, i == 13}$
+	weekday = 10000;					$\C{// UNDEFINED! implicit conversion to Weekday}$
+}
+int j = Wednesday;						$\C{// ERROR! Wednesday is not declared in this scope}$
+\end{cfa}
+The implicit conversion from @int@ to an enumeration type is an unnecessary source of error.
+
+It is common for C programmers to ``believe'' there are 3 equivalent forms of constant enumeration.
+\begin{cfa}
+#define Monday 0
+static const int Monday = 0;
+enum { Monday };
+\end{cfa}
+For @#define@, the programmer has to play compiler and explicitly manage the enumeration values;
+furthermore, these are independent constants outside of any language type mechanism.
+The same explicit management is true for @const@ declarations, and the @const@ variable cannot appear in constant-expression locations, like @case@ labels, array dimensions,\footnote{
+C allows variable-length array-declarations (VLA), so this case does work, but it fails in \CC, which does not support VLAs, unless it is \lstinline{g++}.} and immediate operands of assembler instructions.
+Only the @enum@ form is managed by the compiler, is part of the language type-system, and works in all C constant-expression locations.
Index: doc/theses/jiada_liang_MMath/content1.tex
===================================================================
--- doc/theses/jiada_liang_MMath/content1.tex	(revision 6bd9f9e171271e7c6ac898b1dbf78fc75e68e592)
+++ 	(revision )
@@ -1,8 +1,0 @@
-\chapter{Content1}
-\label{c:content1}
-
-This chapter ...
-
-\section{Section 1}
-
-\section{Section 2}
Index: doc/theses/jiada_liang_MMath/content2.tex
===================================================================
--- doc/theses/jiada_liang_MMath/content2.tex	(revision 6bd9f9e171271e7c6ac898b1dbf78fc75e68e592)
+++ 	(revision )
@@ -1,8 +1,0 @@
-\chapter{Content1}
-\label{c:content1}
-
-This chapter ...
-
-\section{Section 1}
-
-\section{Section 2}
Index: doc/theses/jiada_liang_MMath/implementation.tex
===================================================================
--- doc/theses/jiada_liang_MMath/implementation.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
+++ doc/theses/jiada_liang_MMath/implementation.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
@@ -0,0 +1,646 @@
+\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}
+
+\begin{cfa}
+enum(T) E { ... };
+// backing data
+T * E_values;
+char ** E_labels;
+\end{cfa}
+Storing values and labels as arrays can sometimes help support enumeration features.
+However, the data structures are the overhead for the programs. We want to reduce the memory usage for enumeration support by:
+\begin{itemize}
+	\item Only generates the data array if necessary
+	\item The compilation units share the data structures.
+	No extra overhead if the data structures are requested multiple times.
+\end{itemize}
+
+
+\section{Unification}
+
+\section{Enumeration as Value}
+\label{section:enumeration_as_value}
+An \CFA enumeration with base type T can be used seamlessly as T, without explicitly calling the pseudo-function value.
+\begin{cfa}
+char * green_value = Colour.Green; // "G"
+// Is equivalent to
+// char * green_value = value( Color.Green ); "G"
+\end{cfa}
+
+
+\section{Unification Distance}
+
+\begin{cfa}
+T_2 Foo(T1);
+\end{cfa}
+The @Foo@ function expects a parameter with type @T1@. In C, only a value with the exact type T1 can be used as a parameter for @Foo@. In \CFA, @Foo@ accepts value with some type @T3@ as long as @distance(T1, T3)@ is not @Infinite@.
+
+@path(A, B)@ is a compiler concept that returns one of the following:
+\begin{itemize}
+	\item Zero or 0, if and only if $A == B$.
+	\item Safe, if B can be used as A without losing its precision, or B is a subtype of A.
+	\item Unsafe, if B loses its precision when used as A, or A is a subtype of B.
+	\item Infinite, if B cannot be used as A. A is not a subtype of B and B is not a subtype of A.
+\end{itemize}
+
+For example, @path(int, int)==Zero@, @path(int, char)==Safe@, @path(int, double)==Unsafe@, @path(int, struct S)@ is @Infinite@ for @struct S{}@.
+@distance(A, C)@ is the minimum sum of paths from A to C. For example, if @path(A, B)==i@, @path(B, C)==j@, and @path(A, C)=k@, then $$distance(A,C)==min(path(A,B), path(B,C))==i+j$$.
+
+(Skip over the distance matrix here because it is mostly irrelevant for enumeration discussion. In the actual implementation, distance( E, T ) is 1.)
+
+The arithmetic of distance is the following:
+\begin{itemize}
+	\item $Zero + v= v$, for some value v.
+	\item $Safe * k <  Unsafe$, for finite k.
+	\item $Unsafe * k < Infinite$, for finite k.
+	\item $Infinite + v = Infinite$, for some value v.
+\end{itemize}
+
+For @enum(T) E@, @path(T, E)==Safe@ and @path(E,T)==Infinite@. In other words, enumeration type E can be @safely@ used as type T, but type T cannot be used when the resolution context expects a variable with enumeration type @E@.
+
+
+\section{Variable Overloading and Parameter Unification}
+
+\CFA allows variable names to be overloaded. It is possible to overload a variable that has type T and an enumeration with type T.
+\begin{cfa}
+char * green = "Green";
+Colour green = Colour.Green; // "G"
+
+void bar(char * s) { return s; }
+void foo(Colour c) { return value( c ); }
+
+foo( green ); // "G"
+bar( green ); // "Green"
+\end{cfa}
+\CFA's conversion distance helps disambiguation in this overloading. For the function @bar@ which expects the parameter s to have type @char *@, $distance(char *,char *) == Zero$ while $distance(char *, Colour) == Safe$, the path from @char *@ to the enumeration with based type @char *@, \CFA chooses the @green@ with type @char *@ unambiguously. On the other hand, for the function @foo@, @distance(Colour, char *)@ is @Infinite@, @foo@ picks the @green@ with type @char *@.
+
+\section{Function Overloading}
+Similarly, functions can be overloaded with different signatures. \CFA picks the correct function entity based on the distance between parameter types and the arguments.
+\begin{cfa}
+Colour green = Colour.Green;
+void foo(Colour c) { sout | "It is an enum"; } // First foo
+void foo(char * s) { sout | "It is a string"; } // Second foo
+foo( green ); // "It is an enum"
+\end{cfa}
+Because @distance(Colour, Colour)@ is @Zero@ and @distance(char *, Colour)@ is @Safe@, \CFA determines the @foo( green )@ is a call to the first foo.
+
+\section{Attributes Functions}
+The pseudo-function @value()@ "unboxes" the enumeration and the type of the expression is the underlying type. Therefore, in the section~\ref{section:enumeration_as_value} when assigning @Colour.Green@ to variable typed @char *@, the resolution distance is @Safe@, while assigning @value(Color.Green) to @char *) has resolution distance @Zero@.
+
+\begin{cfa}
+int s1;
+\end{cfa}
+The generated code for an enumeration instance is simply an int. It is to hold the position of an enumeration. And usage of variable @s1@ will be converted to return one of its attributes: label, value, or position, concerning the @Unification@ rule
+
+% \section{Unification and Resolution (this implementation will probably not be used, safe as reference for now)}
+
+% \begin{cfa}
+% enum Colour( char * ) { Red = "R", Green = "G", Blue = "B"  };
+% \end{cfa}
+% The @EnumInstType@ is convertible to other types.
+% A \CFA enumeration expression is implicitly \emph{overloaded} with its three different attributes: value, position, and label.
+% The \CFA compilers need to resolve an @EnumInstType@ as one of its attributes based on the current context.
+
+% \begin{cfa}[caption={Null Context}, label=lst:null_context]
+% {
+% 	Colour.Green;
+% }
+% \end{cfa}
+% In example~\ref{lst:null_context}, the environment gives no information to help with the resolution of @Colour.Green@.
+% In this case, any of the attributes is resolvable.
+% According to the \textit{precedence rule}, the expression with @EnumInstType@ resolves as @value( Colour.Green )@.
+% The @EnumInstType@ is converted to the type of the value, which is statically known to the compiler as @char *@.
+% When the compilation reaches the code generation, the compiler outputs code for type @char *@ with the value @"G"@.
+% \begin{cfa}[caption={Null Context Generated Code}, label=lst:null_context]
+% {
+% 	"G";
+% }
+% \end{cfa}
+% \begin{cfa}[caption={int Context}, label=lst:int_context]
+% {
+% 	int g = Colour.Green;
+% }
+% \end{cfa}
+% The assignment expression gives a context for the EnumInstType resolution.
+% The EnumInstType is used as an @int@, and \CFA needs to determine which of the attributes can be resolved as an @int@ type.
+% The functions $Unify( T1, T2 ): bool$ take two types as parameters and determine if one type can be used as another.
+% In example~\ref{lst:int_context}, the compiler is trying to unify @int@ and @EnumInstType@ of @Colour@.
+% $$Unification( int, EnumInstType<Colour> )$$ which turns into three Unification call
+% \begin{cfa}[label=lst:attr_resolution_1]
+% {
+% 	Unify( int, char * ); // unify with the type of value
+% 	Unify( int, int ); // unify with the type of position
+% 	Unify( int, char * ); // unify with the type of label
+% }
+% \end{cfa}
+% \begin{cfa}[label=lst:attr_resolution_precedence]
+% {
+% 	Unification( T1, EnumInstType<T2> ) {
+% 		if ( Unify( T1, T2 ) ) return T2;
+% 		if ( Unify( T1, int ) ) return int;
+% 		if ( Unify( T1, char * ) ) return char *;
+% 		Error: Cannot Unify T1 with EnumInstType<T2>;
+% 	}
+% }
+% \end{cfa}
+% After the unification, @EnumInstType@ is replaced by its attributes.
+
+% \begin{cfa}[caption={Unification Functions}, label=lst:unification_func_call]
+% {
+% 	T2 foo ( T1 ); // function take variable with T1 as a parameter
+% 	foo( EnumInstType<T3> ); // Call foo with a variable has type EnumInstType<T3>
+% 	>>>> Unification( T1, EnumInstType<T3> )
+% }
+% \end{cfa}
+% % The conversion can work backward: in restrictive cases, attributes of can be implicitly converted back to the EnumInstType.
+% Backward conversion:
+% \begin{cfa}[caption={Unification Functions}, label=lst:unification_func_call]
+% {
+% 	enum Colour colour = 1;
+% }
+% \end{cfa}
+
+% \begin{cfa}[caption={Unification Functions}, label=lst:unification_func_call]
+% {
+%	Unification( EnumInstType<Colour>, int ) >>> label
+% }
+% \end{cfa}
+% @int@ can be unified with the label of Colour.
+% @5@ is a constant expression $\Rightarrow$ Compiler knows the value during the compilation $\Rightarrow$ turns it into
+% \begin{cfa}
+% {
+%	enum Colour colour = Colour.Green;
+% }
+% \end{cfa}
+% Steps:
+% \begin{enumerate}
+% \item
+% identify @1@ as a constant expression with type @int@, and the value is statically known as @1@
+% \item
+% @unification( EnumInstType<Colour>, int )@: @position( EnumInstType< Colour > )@
+% \item
+% return the enumeration constant at position 1
+% \end{enumerate}
+% \begin{cfa}
+% {
+% 	enum T (int) { ... } // Declaration
+% 	enum T t = 1;
+% }
+% \end{cfa}
+% Steps:
+% \begin{enumerate}
+% \item
+% identify @1@ as a constant expression with type @int@, and the value is statically known as @1@
+% \item
+% @unification( EnumInstType<Colour>, int )@: @value( EnumInstType< Colour > )@
+% \item
+% return the FIRST enumeration constant that has the value 1, by searching through the values array
+% \end{enumerate}
+% The downside of the precedence rule: @EnumInstType@ $\Rightarrow$ @int ( value )@ $\Rightarrow$ @EnumInstType@ may return a different @EnumInstType@ because the value can be repeated and there is no way to know which one is expected $\Rightarrow$ want uniqueness
+
+% \section{Casting}
+% Casting an EnumInstType to some other type T works similarly to unify the EnumInstType with T. For example:
+% \begin{cfa}
+% enum( int ) Foo { A = 10, B = 100, C = 1000 };
+% (int) Foo.A;
+% \end{cfa}
+% The \CFA-compiler unifies @EnumInstType<int>@ with int, with returns @value( Foo.A )@, which has statically known value 10. In other words, \CFA-compiler is aware of a cast expression, and it forms the context for EnumInstType resolution. The expression with type @EnumInstType<int>@ can be replaced by the compile with a constant expression 10, and optionally discard the cast expression.
+
+% \section{Value Conversion}
+% As discussed in section~\ref{lst:var_declaration}, \CFA only saves @position@ as the necessary information. It is necessary for \CFA to generate intermediate code to retrieve other attributes.
+
+% \begin{cfa}
+% Foo a; // int a;
+% int j = a;
+% char * s = a;
+% \end{cfa}
+% Assume stores a value x, which cannot be statically determined. When assigning a to j in line 2, the compiler @Unify@ j with a, and returns @value( a )@. The generated code for the second line will be
+% \begin{cfa}
+% int j = value( Foo, a )
+% \end{cfa}
+% Similarly, the generated code for the third line is
+% \begin{cfa}
+% char * j = label( Foo, a )
+% \end{cfa}
+
+
+\section{Enumerator Initialization}
+An enumerator must have a deterministic immutable value, either be explicitly initialized in the enumeration definition, or implicitly initialized by rules.
+
+\section{C Enumeration Rule}
+A C enumeration has an integral type. If not initialized, the first enumerator implicitly has the integral value 0, and other enumerators have a value equal to its $predecessor + 1$.
+
+\section{Auto Initializable}
+\label{s:AutoInitializable}
+
+
+\CFA enumerations have the same rule in enumeration constant initialization.
+However, only \CFA types that have defined traits for @zero_t@, @one_t@, and an addition operator can be automatically initialized by \CFA.
+
+Specifically, a type is auto-initializable only if it satisfies the trait @AutoInitializable@:
+\begin{cfa}
+forall(T)
+trait AutoInitializable {
+	void ?()( T & t, zero_t );
+	S ?++( T & t);
+};
+\end{cfa}
+An example of a user-defined @AutoInitializable@ is:
+\begin{cfa}[label=lst:sample_auto_Initializable]
+struct Odd { int i; };
+void ?()( Odd & t, zero_t ) { t.i = 1; };
+Odd ?++( Odd t1 ) { return Odd( t1.i + 2); };
+\end{cfa}
+When the type of an enumeration is @AutoInitializable@, implicit initialization is available.
+\begin{cfa}[label=lst:sample_auto_Initializable_usage]
+enum AutoInitUsage(Odd) {
+	A, B, C = 7, D
+};
+\end{cfa}
+In the example, no initializer is specified for the first enumeration constant @A@, so \CFA initializes it with the value of @zero_t@, which is 1.
+@B@ and @D@ have the values of their $predecessor++$, where @one_t@ has the value 2.
+Therefore, the enumeration is initialized as follows:
+\begin{cfa}[label=lst:sample_auto_Initializable_usage_gen]
+enum AutoInitUsage(Odd) {
+	A = 1, B = 3, C = 7, D = 9
+};
+\end{cfa}
+Note that there is no mechanism to prevent an even value for the direct initialization, such as @C = 6@.
+
+In \CFA, character, integral, float, and imaginary types are all @AutoInitialiable@.
+\begin{cfa}[label=lst:letter]
+enum Alphabet( int ) {
+	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
+};
+print( "%c, %c, %c", Alphabet.F, Alphabet.o, Alphabet.z );
+>>> F, o, z
+\end{cfa}
+\section{Enumeration Features}
+\section{Iteration and Range}
+
+It is convenient to iterate over a \CFA enumeration value, e.g.:
+\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}
+
+
+% \section{Non-uniform Type}
+% TODO: Working in Progress, might need to change other sections. Conflict with the resolution right now.
+
+% \begin{cfa}
+% enum T( int, char * ) {
+%	 a=42, b="Hello World"
+% };
+% \end{cfa}
+% The enum T declares two different types: int and char *. The enumerators of T hold values of one of the declared types.
+
+\section{Enumeration Inheritance}
+
+\begin{cfa}[label=lst:EnumInline]
+enum( char * ) Name { Jack = "Jack", Jill = "Jill" };
+enum /* inferred */ Name2 { inline Name, Sue = "Sue", Tom = "Tom" };
+\end{cfa}
+\lstinline{Inline} allows Enumeration Name2 to inherit enumerators from Name1 by containment, and a Name enumeration is a subtype of enumeration Name2. An enumeration instance of type Name can be used where an instance of Name2 is expected.
+\begin{cfa}[label=lst:EnumInline]
+Name Fred;
+void f( Name2 );
+f( Fred );
+\end{cfa}
+If enumeration A declares @inline B@ in its enumeration body, enumeration A is the "inlining enum" and enumeration B is the "inlined enum".
+
+An enumeration can inline at most one other enumeration. The inline declaration must be placed before the first enumerator of the inlining enum. The inlining enum has all the enumerators from the inlined enum, with the same labels, values, and position.
+\begin{cfa}[label=lst:EnumInline]
+enum /* inferred */ Name2 { inline Name, Sue = "Sue", Tom = "Tom" };
+// is equivalent to enum Name2 { Jack = "Jack", Jill="Jill", Sue = "Sue", Tom = "Tom" };
+\end{cfa}
+Name.Jack is equivalent to Name2.Jack. Their attributes are all identical. Opening both Name and Name2 in the same scope will not introduce ambiguity.
+\begin{cfa}[label=lst:EnumInline]
+with( Name, Name2 ) { Jack; } // Name.Jack and Name2.Jack are equivalent. No ambiguity
+\end{cfa}
+
+\section{Implementation}
+
+\section{Static Attribute Expression}
+\begin{cfa}[label=lst:static_attr]
+enum( char * ) Colour {
+	Red = "red", Blue = "blue", Green = "green"
+};
+\end{cfa}
+An enumerator expression returns its enumerator value as a constant expression with no runtime cost. For example, @Colour.Red@ is equivalent to the constant expression "red", and \CFA finishes the expression evaluation before generating the corresponding C code. Applying a pseudo-function to a constant enumerator expression results in a constant expression as well. @value( Colour.Red )@, @position( Colour. Red )@, and @label( Colour.Red )@ are equivalent to constant expression with char * value "red", int value 0, and char * value "Red", respectively.
+
+\section{Runtime Attribute Expression and Weak Referenced Data}
+\begin{cfa}[label=lst:dynamic_attr]
+Colour c;
+...
+value( c ); // or c
+\end{cfa}
+An enumeration variable c is equivalent to an integer variable with the value of @position( c )@ In Example~\ref{lst:dynamic_attr}, the value of enumeration variable c is unknown at compile time. In this case, the pseudo-function calls are reduced to expression that returns the enumerator values at runtime.
+
+\CFA stores the variables and labels in @const@ arrays to provide runtime lookup for enumeration information.
+
+\begin{cfa}[label=lst:attr_array]
+const char * Colour_labels [3] = { "Red", "Blue", "Green" };
+const char * Colour_values [3] = { "red", "blue", "green" };
+\end{cfa}
+The \CFA compiles transforms the attribute expressions into array access.
+\begin{cfa}[label=lst:attr_array_access]
+position( c ) // c; an integer
+value( c ); // Colour_values[c]
+label( c ); // Colour_labels[c]
+\end{cfa}
+
+To avoid unnecessary memory usage, the labels and values array are only generated as needed, and only generate once across all compilation units. By default, \CFA defers the declaration of the label and value arrays until an call to attribute function with a dynamic value. If an attribute function is never called on a dynamic value of an enumerator, the array will never be allocated. Once the arrays are created, all compilation units share a weak reference to the allocation array.
+
+\section{Enum Prelude}
+
+\begin{cfa}[label=lst:enum_func_dec]
+forall( T ) {
+	unsigned position( unsigned );
+	T value( unsigned );
+	char * label( unsigned );
+}
+\end{cfa}
+\CFA loads the declaration of enumeration function from the enum.hfa.
+
+\section{Internal Representation}
+
+The definition of an enumeration is represented by an internal type called @EnumDecl@. At the minimum, it stores all the information needed to construct the companion object. Therefore, an @EnumDecl@ can be represented as the following:
+\begin{cfa}[label=lst:EnumDecl]
+forall(T)
+class EnumDecl {
+	T* values;
+	char** label;
+};
+\end{cfa}
+
+The internal representation of an enumeration constant is @EnumInstType@.
+An @EnumInstType@ has a reference to the \CFA-enumeration declaration and the position of the enumeration constant.
+\begin{cfa}[label=lst:EnumInstType]
+class EnumInstType {
+	EnumDecl enumDecl;
+	int position;
+};
+\end{cfa}
+In the later discussion, we will use @EnumDecl<T>@ to symbolize a @EnumDecl@ parameterized by type T, and @EnumInstType<T>@ is a declared instance of @EnumDecl<T>@.
+
+\begin{cfa}[caption={Enum Type Functions}, label=lst:cforall_enum_data]
+const T * const values;
+const char * label;
+int length;
+\end{cfa}
+Companion data are necessary information to represent an enumeration. They are stored as standalone pieces, rather than a structure. Those data will be loaded "on demand".
+Companion data are needed only if the according pseudo-functions are called. For example, the value of the enumeration Workday is loaded only if there is at least one compilation that has call $value(Workday)$. Once the values are loaded, all compilations share these values array to reduce memory usage.
+
+
+% \section{(Rework) Companion Object and Companion Function}
+
+% \begin{cfa}[caption={Enum Type Functions}, label=lst:cforall_enum_functions]
+% forall( T )
+% struct Companion {
+% 	const T * const values;
+%		 const char * label;
+% 	int length;
+% };
+% \end{cfa}
+% \CFA generates companion objects, an instance of structure that encloses @necessary@ data to represent an enumeration. The size of the companion is unknown at the compilation time, and it "grows" in size to compensate for the @usage@.
+
+% The companion object is singleton across the compilation (investigation).
+
+% \CFA generates the definition of companion functions.
+% Because \CFA implicitly stores an enumeration instance as its position, the companion function @position@ does nothing but return the position it is passed.
+% Companions function @value@ and @label@ return the array item at the given position of @values@ and @labels@, respectively.
+% \begin{cfa}[label=lst:companion_definition]
+% int position( Companion o, int pos ) { return pos; }
+% T value( Companion o, int pos ) { return o.values[ pos ]; }
+% char * label( Companion o, int pos ) { return o.labels[ pos ]; }
+% \end{cfa}
+% Notably, the @Companion@ structure definition, and all companion objects, are visible to users.
+% A user can retrieve values and labels defined in an enumeration by accessing the values and labels directly, or indirectly by calling @Companion@ functions @values@ and @labels@
+% \begin{cfa}[label=lst:companion_definition_values_labels]
+% Colour.values; // read the Companion's values
+% values( Colour ); // same as Colour.values
+% \end{cfa}
+
+\section{Companion Traits (experimental)}
+Not sure its semantics yet, and it might replace a companion object.
+\begin{cfa}[label=lst:companion_trait]
+forall(T1) {
+	trait Companion(otype T2<otype T1>) {
+		T1 value((otype T2<otype T1> const &);
+		int position(otype T2<otype T1> const &);
+		char * label(otype T2<otype T1> const &);
+	}
+}
+\end{cfa}
+All enumerations implicitly implement the Companion trait, an interface to access attributes. The Companion can be a data type because it fulfills to requirements to have concrete instances, which are:
+
+\begin{enumerate}
+  \item The instance of enumeration has a single polymorphic type.
+  \item Each assertion should use the type once as a parameter.
+\end{enumerate}
+
+\begin{cfa}
+enum(int) Weekday {
+	Monday=10, Tuesday, ...
+};
+
+T value( enum Weekday<T> & this);
+int position( enum Weekday<T> & this )
+char * label( enum Weekday<T> & this )
+
+trait Companion obj = (enum(int)) Workday.Weekday;
+value(obj); // 10
+\end{cfa}
+The enumeration comes with default implementation to the Companion traits functions. The usage of Companion functions would make \CFA allocates and initializes the necessary companion arrays, and return the data at the position represented by the enumeration.
+(...)
+
+\section{User Define Enumeration Functions}
+
+Companion objects make extending features for \CFA enumeration easy.
+\begin{cfa}[label=lst:companion_user_definition]
+char * charastic_string( Companion o, int position ) {
+	return sprintf( "Label: %s; Value: %s", label( o, position ), value( o, position) );
+}
+printf( charactic_string ( Color, 1 ) );
+>>> Label: Green; Value: G
+\end{cfa}
+Defining a function takes a Companion object effectively defines functions for all \CFA enumeration.
+
+The \CFA compiler turns a function call that takes an enumeration instance as a parameter into a function call with a companion object plus a position.
+Therefore, a user can use the syntax with a user-defined enumeration function call:
+\begin{cfa}[label=lst:companion_user_definition]
+charactic_string( Color.Green ); // equivalent to charactic_string( Color, 1 )
+>>> Label: Green; Value: G
+\end{cfa}
+Similarly, the user can work with the enumeration type itself: (see section ref...)
+\begin{cfa}[ label=lst:companion_user_definition]
+void print_enumerators ( Companion o ) {
+	for ( c : Companion o ) {
+		sout | label (c) | value( c ) ;
+	}
+}
+print_enumerators( Colour );
+\end{cfa}
+
+
+\section{Declaration}
+
+The qualified enumeration syntax is dedicated to \CFA enumeration.
+\begin{cfa}[label=lst:range_functions]
+enum (type_declaration) name { enumerator = const_expr, enumerator = const_expr, ... }
+\end{cfa}
+A compiler stores the name, the underlying type, and all enumerators in an @enumeration table@.
+During the $Validation$ pass, the compiler links the type declaration to the type's definition.
+It ensures that the name of an enumerator is unique within the enumeration body, and checks if all values of the enumerator have the declaration type.
+If the declared type is not @AutoInitializable@, \CFA rejects the enumeration definition.
+Otherwise, it attempts to initialize enumerators with the enumeration initialization pattern. (a reference to a future initialization pattern section)
+
+\begin{cfa}[label=lst:init]
+struct T { ... };
+void ?{}( T & t, zero_t ) { ... };
+void ?{}( T & t, one_t ) { ... };
+T ?+?( T & lhs, T & rhs ) { ... };
+
+enum (T) Sample {
+	Zero: 0 /* zero_t */,
+	One: Zero + 1 /* ?+?( Zero, one_t ) */ , ...
+};
+\end{cfa}
+Challenge: \\
+The value of an enumerator, or the initializer, requires @const_expr@.
+While previously getting around the issue by pushing it to the C compiler, it might not work anymore because of the user-defined types, user-defined @zero_t@, @one_t@, and addition operation.
+Might not be able to implement a \emph{correct} static check.
+
+\CFA $autogens$ a Companion object for the declared enumeration.
+\begin{cfa}[label=lst:companion]
+Companion( T ) Sample {
+	.values: { 0, 0+1, 0+1+1, 0+1+1+1, ... }, /* 0: zero_t, 1: one_t, +: ?+?{} */
+	.labels: { "Zero", "One", "Two", "Three", ...},
+	.length: /* number of enumerators */
+};
+\end{cfa}
+\CFA stores values as intermediate expressions because the result of the function call to the function @?+?{}(T&, T&)@ is statically unknown to \CFA.
+But the result is computed at run time, and the compiler ensures the @values@ are not changed.
+
+\section{Qualified Expression}
+
+\CFA uses qualified expression to address the scoping of \CFA-enumeration.
+\begin{cfa}[label=lst:qualified_expression]
+aggregation_name.field;
+\end{cfa}
+The qualified expression is not dedicated to \CFA enumeration.
+It is a feature that is supported by other aggregation in \CFA as well, including a C enumeration.
+When C enumerations are unscoped, the qualified expression syntax still helps to disambiguate names in the context.
+\CFA recognizes if the expression references a \CFA aggregation by searching the presence of @aggregation_name@ in the \CFA enumeration table.
+If the @aggregation_name@ is identified as a \CFA enumeration, the compiler checks if @field@ presents in the declared \CFA enumeration.
+
+\section{Instance Declaration}
+
+
+\begin{cfa}[label=lst:var_declaration]
+enum Sample s1;
+\end{cfa}
+
+The declaration \CFA-enumeration variable has the same syntax as the C-enumeration. Internally, such a variable will be represented as an EnumInstType.
Index: doc/theses/jiada_liang_MMath/intro.tex
===================================================================
--- doc/theses/jiada_liang_MMath/intro.tex	(revision 6bd9f9e171271e7c6ac898b1dbf78fc75e68e592)
+++ doc/theses/jiada_liang_MMath/intro.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
@@ -1,5 +1,28 @@
 \chapter{Introduction}
 
-Testing glossy abbreviations \gls{foo} and \gls{bar}, and glossy definitions \gls{git} and \gls{gulp}.
+Naming values is a common practice in mathematics and engineering, e.g., $\pi$, $\tau$ (2$\pi$), $\phi$ (golden ratio), MHz (1E6), etc.
+Naming is also commonly used to represent many other numerical phenomenon, such as days of the week, months of a year, floors of a building (basement), specific times (noon, New Years).
+Many programming languages capture this important software-engineering capability through a mechanism called an \Newterm{enumeration}.
+An enumeration is similar to other programming-language types by providing a set of constrained values, but adds the ability to name \emph{all} the values in its set.
+Note, all enumeration names must be unique but different names can represent the same value (eight note, quaver), which are synonyms.
 
-And use the glossy abbreviations \gls{foo} and \gls{bar}, and definitions \gls{git} and \gls{gulp} again.
+Specifically, an enumerated type restricts its values to a fixed set of named constants.
+While all types are restricted to a fixed set of values because of the underlying von Neumann architecture, and hence, to a corresponding set of constants, e.g., @3@, @3.5@, @3.5+2.1i@, @'c'@, @"abc"@, etc., these values are not named, other than the programming-language supplied constant names.
+
+Fundamentally, all enumeration systems have an \Newterm{enumeration} type with an associated set of \Newterm{enumerator} names.
+An enumeration has three universal attributes, \Newterm{position}, \Newterm{label}, and \Newterm{value}, as shown by this representative enumeration, where position and value can be different.
+\begin{cquote}
+\small\sf\setlength{\tabcolsep}{3pt}
+\begin{tabular}{rccccccccccc}
+\it\color{red}enumeration & \multicolumn{7}{c}{\it\color{red}enumerators}	\\
+$\downarrow$\hspace*{25pt} & \multicolumn{7}{c}{$\downarrow$}				\\
+@enum@ Weekday \{				& Monday,	& Tuesday,	& Wednesday,	& Thursday,& Friday, 	& Saturday,	& Sunday \}; \\
+\it\color{red}position			& 0			& 1			& 2				& 3				& 4			& 5			& 6			\\
+\it\color{red}label				& Monday	& Tuesday	& Wednesday		& Thursday		& Friday 	& Saturday	& Sunday	\\
+\it\color{red}value				& 0			& 1			& 2				& 3				& 4			& 5		& 6
+\end{tabular}
+\end{cquote}
+Here, the \Newterm{enumeration} @Weekday@ defines the ordered \Newterm{enumerator}s @Monday@, @Tuesday@, @Wednesday@, @Thursday@, @Friday@, @Saturday@ and @Sunday@.
+By convention, the successor of @Tuesday@ is @Monday@ and the predecessor of @Tuesday@ is @Wednesday@, independent of the associated enumerator constant values.
+Because an enumerator is a constant, it cannot appear in a mutable context, e.g. @Mon = Sun@ is meaningless, and an enumerator has no address, it is an \Newterm{rvalue}\footnote{
+The term rvalue defines an expression that can only appear on the right-hand side of an assignment.}.
Index: doc/theses/jiada_liang_MMath/relatedwork.tex
===================================================================
--- doc/theses/jiada_liang_MMath/relatedwork.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
+++ doc/theses/jiada_liang_MMath/relatedwork.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
@@ -0,0 +1,623 @@
+\chapter{Related Work}
+\label{s:RelatedWork}
+
+Enumerations exist in many popular programming languages, e.g., Pascal~\cite{Pascal}, Ada~\cite{Ada}, \Csharp, \CC, Go~\cite{Go}, Java~\cite{Java}, Modula-3~\cite{Modula-3}, Rust~\cite{Rust}, Swift~\cite{Swift}, Python~\cite{Python}, and the algebraic data-type in functional programming.
+There are a large set of overlapping features among these languages, but each language has its own unique restrictions and extensions.
+
+\section{(Free) Pascal}
+
+Free Pascal is a modern object-oriented version of the classic Pascal programming language.
+It allows a C-style enumeration type, where enumerators must be in assigned in ascending numerical order with a constant expression and the range can be non-consecutive.
+\begin{lstlisting}[language=pascal,{moredelim=**[is][\color{red}]{@}{@}}]
+Type EnumType = ( one, two, three, forty @= 40@, fortyone );
+\end{lstlisting}
+Pseudo-functions @Pred@ and @Succ@ can only be used if the range is consecutive.
+The underlying type is an implementation-defined integral type large enough to hold all enumerated values; it does not have to be the smallest possible type.
+The size underlying integral type can be explicitly specified using compiler directive @$PACKENUM@~$N$, where $N$ is the number of bytes, e.g.:
+\begin{lstlisting}[language=pascal,{moredelim=**[is][\color{red}]{@}{@}}]
+Type @{$\color{red}\$$PACKENUM 1}@ SmallEnum = ( one, two, three );
+	    @{$\color{red}\$$PACKENUM 4}@ LargeEnum = ( BigOne, BigTwo, BigThree );
+Var S : SmallEnum; { 1 byte }
+	  L : LargeEnum; { 4 bytes}
+\end{lstlisting}
+
+
+\section{Ada}
+
+An enumeration type is defined as a list of possible values:
+\begin{lstlisting}[language=ada]
+type RGB is (Red, Green, Blue);
+\end{lstlisting}
+Like for numeric types, where e.g., 1 is an integer literal, @Red@, @Green@ and @Blue@ are called the literals of this type.
+There are no other values assignable to objects of this type.
+
+\paragraph{Operators and attributes} ~\newline
+Apart from equality (@"="@), the only operators on enumeration types are the ordering operators: @"<"@, @"<="@, @"="@, @"/="@, @">="@, @">"@, where the order relation is given implicitly by the sequence of literals:
+Each literal has a position, starting with 0 for the first, incremented by one for each successor.
+This position can be queried via the @'Pos@ attribute; the inverse is @'Val@, which returns the corresponding literal. In our example:
+\begin{lstlisting}[language=ada]
+RGB'Pos (Red) = 0
+RGB'Val (0)   = Red
+\end{lstlisting}
+There are two other important attributes: @Image@ and @Value@.
+@Image@ returns the string representation of the value (in capital letters), @Value@ is the inverse:
+\begin{lstlisting}[language=ada]
+RGB'Image ( Red ) = "RED"
+RGB'Value ("Red") =  Red
+\end{lstlisting}
+These attributes are important for simple IO (there are more elaborate IO facilities in @Ada.Text_IO@ for enumeration types).
+Note that, since Ada is case-insensitive, the string given to @'Value@ can be in any case.
+
+\paragraph{Enumeration literals} ~\newline
+Literals are overloadable, i.e. you can have another type with the same literals.
+\begin{lstlisting}[language=ada]
+type Traffic_Light is (Red, Yellow, Green);
+\end{lstlisting}
+Overload resolution within the context of use of a literal normally resolves which @Red@ is meant.
+Only if you have an unresolvable overloading conflict, you can qualify with special syntax which @Red@ is meant:
+\begin{lstlisting}[language=ada]
+RGB'(Red)
+\end{lstlisting}
+Like many other declarative items, enumeration literals can be renamed.
+In fact, such a literal is actually a function, so it has to be renamed as such:
+\begin{lstlisting}[language=ada]
+function Red return P.RGB renames P.Red;
+\end{lstlisting}
+Here, @RGB@ is assumed to be defined in package @P@, which is visible at the place of the renaming declaration.
+Renaming makes @Red@ directly visible without necessity to resort the use-clause.
+
+Note that redeclaration as a function does not affect the staticness of the literal.
+
+\paragraph{Characters as enumeration literals} ~\newline
+Rather unique to Ada is the use of character literals as enumeration literals:
+\begin{lstlisting}[language=ada]
+type ABC is ('A', 'B', 'C');
+\end{lstlisting}
+This literal @'A'@ has nothing in common with the literal @'A'@ of the predefined type @Character@ (or @Wide_Character@).
+
+Every type that has at least one character literal is a character type.
+For every character type, string literals and the concatenation operator @"&"@ are also implicitly defined.
+\begin{lstlisting}[language=ada]
+type My_Character is (No_Character, 'a', Literal, 'z');
+type My_String is array (Positive range <>) of My_Character;
+
+S: My_String := "aa" & Literal & "za" & 'z';
+T: My_String := ('a', 'a', Literal, 'z', 'a', 'z');
+\end{lstlisting}
+In this example, @S@ and @T@ have the same value.
+
+Ada's @Character@ type is defined that way.
+See Ada Programming/Libraries/Standard.
+
+\paragraph{Booleans as enumeration literals} ~\newline
+Also Booleans are defined as enumeration types:
+\begin{lstlisting}[language=ada]
+type Boolean is (False, True);
+\end{lstlisting}
+There is special semantics implied with this declaration in that objects and expressions of this type can be used as conditions.
+Note that the literals @False@ and @True@ are not Ada keywords.
+
+Thus it is not sufficient to declare a type with these literals and then hope objects of this type can be used like so:
+\begin{lstlisting}[language=ada]
+type My_Boolean is (False, True);
+Condition: My_Boolean;
+
+if Condition then -- wrong, won't compile
+\end{lstlisting}
+
+If you need your own Booleans (perhaps with special size requirements), you have to derive from the predefined Boolean:
+\begin{lstlisting}[language=ada]
+type My_Boolean is new Boolean;
+Condition: My_Boolean;
+
+if Condition then -- OK
+\end{lstlisting}
+
+\paragraph{Enumeration subtypes} ~\newline
+You can use range to subtype an enumeration type:
+\begin{lstlisting}[language=ada]
+subtype Capital_Letter is Character range 'A' .. 'Z';
+type Day_Of_Week is (Sunday, Monday, Tuesday, Wednesday, Thursday, Friday, Saturday);
+subtype Working_Day is Day_Of_Week range Monday .. Friday;
+\end{lstlisting}
+
+\paragraph{Using enumerations} ~\newline
+Enumeration types being scalar subtypes, type attributes such as @First@ and @Succ@ will allow stepping through a subsequence of the values.
+\begin{lstlisting}[language=ada]
+case Day_Of_Week'First is
+	when Sunday =>
+	   ISO (False);
+	when Day_Of_Week'Succ(Sunday) =>
+	   ISO (True);
+	when Tuesday .. Saturday =>
+	   raise Program_Error;
+end case;
+\end{lstlisting}
+A loop will automatically step through the values of the subtype's range.
+Filtering week days to include only working days with an even position number:
+\begin{lstlisting}[language=ada]
+	for Day in Working_Day loop
+		if Day_Of_Week'Pos(Day) mod 2 = 0 then
+			Work_In_Backyard;
+		end if;
+	end loop;
+\end{lstlisting}
+Enumeration types can be used as array index subtypes, yielding a table feature:
+\begin{lstlisting}[language=ada]
+type Officer_ID is range 0 .. 50;
+type Schedule is array (Working_Day) of Officer_ID;
+\end{lstlisting}
+
+\begin{lstlisting}[language=ada]
+type Subtype_Name is (Id1, Id2, Id3 ... );
+\end{lstlisting}
+where @Id1@, @Id2@, etc. are identifiers or characters literals.
+In either case, the legal values of the type are referred to as "enumeration literals."
+Each of these values has a "position number" corresponding to its position in the list such that @Id1@ has position 0, @Id2@ has position 1, and the Nth value has position N-1.
+
+\paragraph{Attributes of Enumeration Types} ~\newline
+An enumeration type, @T@, has the following attributes: @T'First@, @T'Last@, @T'Range@, @T'Pred@, @T'Succ@, @T'Min@, @T'Max@, @T'Image@, @T'Wide_Image@, @T'Value@, @T'Wide_Value@, @T'Pos@, and @T'Val@ (pronounced "T tick first", "T tick last", etc.).
+Most of these are illustrated in the example program given below, and most of them produce what you would intuitively expect based on their names.
+
+@T'Image@ and @T'Value@ form a complementary pair of attributes.
+The former takes a value in @T@ and returns a String representation of that value.
+The latter takes a @String@ that is a representation of a value in @T@ and returns that value.
+
+@T'Pos@ and @T'Val@ form another complementary pair.
+The former takes a value in @T@ and returns its position number.
+The latter takes a position number and returns the corresponding value of type @T@.
+
+
+\section{C\raisebox{-0.7ex}{\LARGE$^\sharp$}\xspace} % latex bug: cannot use \relsize{2} so use \LARGE
+
+\lstdefinelanguage{swift}
+{
+  morekeywords={
+    open,catch,@escaping,nil,throws,func,if,then,else,for,in,while,do,switch,case,default,where,break,continue,fallthrough,return,
+    typealias,struct,class,enum,protocol,var,func,let,get,set,willSet,didSet,inout,init,deinit,extension,
+    subscript,prefix,operator,infix,postfix,precedence,associativity,left,right,none,convenience,dynamic,
+    final,lazy,mutating,nonmutating,optional,override,required,static,unowned,safe,weak,internal,
+    private,public,is,as,self,unsafe,dynamicType,true,false,nil,Type,Protocol,
+  },
+  morecomment=[l]{//}, % l is for line comment
+  morecomment=[s]{/*}{*/}, % s is for start and end delimiter
+  morestring=[b]", % defines that strings are enclosed in double quotes
+  breaklines=true,
+  escapeinside={\%*}{*)},
+%  numbers=left,
+  captionpos=b,
+  breakatwhitespace=true,
+  basicstyle=\linespread{0.9}\sf, % https://tex.stackexchange.com/a/102728/129441
+}
+
+Model custom types that define a list of possible values.
+
+An enumeration defines a common type for a group of related values and enables you to work with those values in a type-safe way within your code.
+
+If you are familiar with C, you will know that C enumerations assign related names to a set of integer values.
+Enumerations in Swift are much more flexible, and don't have to provide a value for each case of the enumeration.
+If a value (known as a raw value) is provided for each enumeration case, the value can be a string, a character, or a value of any integer or floating-point type.
+
+Alternatively, enumeration cases can specify associated values of any type to be stored along with each different case value, much as unions or variants do in other languages.
+You can define a common set of related cases as part of one enumeration, each of which has a different set of values of appropriate types associated with it.
+
+Enumerations in Swift are first-class types in their own right.
+They adopt many features traditionally supported only by classes, such as computed properties to provide additional information about the enumeration's current value, and instance methods to provide functionality related to the values the enumeration represents.
+Enumerations can also define initializers to provide an initial case value;
+can be extended to expand their functionality beyond their original implementation; and can conform to protocols to provide standard functionality.
+
+For more about these capabilities, see Properties, Methods, Initialization, Extensions, and Protocols.
+
+\paragraph{Enumeration Syntax}
+
+You introduce enumerations with the @enum@ keyword and place their entire definition within a pair of braces:
+\begin{lstlisting}[language=swift]
+enum SomeEnumeration {
+    // enumeration definition goes here
+}
+\end{lstlisting}
+Here's an example for the four main points of a compass:
+\begin{lstlisting}[language=swift]
+enum CompassPoint {
+    case north
+    case south
+    case east
+    case west
+}
+\end{lstlisting}
+The values defined in an enumeration (such as @north@, @south@, @east@, and @west@) are its enumeration cases.
+You use the @case@ keyword to introduce new enumeration cases.
+
+Note:
+Swift enumeration cases don't have an integer value set by default, unlike languages like C and Objective-C.
+In the CompassPoint example above, @north@, @south@, @east@ and @west@ don't implicitly equal 0, 1, 2 and 3.
+Instead, the different enumeration cases are values in their own right, with an explicitly defined type of CompassPoint.
+
+Multiple cases can appear on a single line, separated by commas:
+\begin{lstlisting}[language=swift]
+enum Planet {
+    case mercury, venus, earth, mars, jupiter, saturn, uranus, neptune
+}
+\end{lstlisting}
+Each enumeration definition defines a new type.
+Like other types in Swift, their names (such as @CompassPoint@ and @Planet@) start with a capital letter.
+Give enumeration types singular rather than plural names, so that they read as self-evident:
+\begin{lstlisting}[language=swift]
+var directionToHead = CompassPoint.west
+\end{lstlisting}
+The type of @directionToHead@ is inferred when it's initialized with one of the possible values of @CompassPoint@.
+Once @directionToHead@ is declared as a @CompassPoint@, you can set it to a different @CompassPoint@ value using a shorter dot syntax:
+\begin{lstlisting}[language=swift]
+directionToHead = .east
+\end{lstlisting}
+The type of @directionToHead@ is already known, and so you can drop the type when setting its value.
+This makes for highly readable code when working with explicitly typed enumeration values.
+
+\paragraph{Matching Enumeration Values with a Switch Statement}
+
+You can match individual enumeration values with a switch statement:
+\begin{lstlisting}[language=swift]
+directionToHead = .south
+switch directionToHead {
+case .north:
+    print("Lots of planets have a north")
+case .south:
+    print("Watch out for penguins")
+case .east:
+    print("Where the sun rises")
+case .west:
+    print("Where the skies are blue")
+}
+// Prints "Watch out for penguins"
+\end{lstlisting}
+You can read this code as:
+\begin{quote}
+"Consider the value of directionToHead.
+In the case where it equals @.north@, print "Lots of planets have a north".
+In the case where it equals @.south@, print "Watch out for penguins"."
+
+...and so on.
+\end{quote}
+As described in Control Flow, a switch statement must be exhaustive when considering an enumeration's cases.
+If the case for @.west@ is omitted, this code doesn't compile, because it doesn't consider the complete list of @CompassPoint@ cases.
+Requiring exhaustiveness ensures that enumeration cases aren't accidentally omitted.
+
+When it isn't appropriate to provide a case for every enumeration case, you can provide a default case to cover any cases that aren't addressed explicitly:
+\begin{lstlisting}[language=swift]
+let somePlanet = Planet.earth
+switch somePlanet {
+case .earth:
+    print("Mostly harmless")
+default:
+    print("Not a safe place for humans")
+}
+// Prints "Mostly harmless"
+\end{lstlisting}
+
+\paragraph{Iterating over Enumeration Cases}
+
+For some enumerations, it's useful to have a collection of all of that enumeration's cases.
+You enable this by writing @CaseIterable@ after the enumeration's name.
+Swift exposes a collection of all the cases as an allCases property of the enumeration type.
+Here's an example:
+\begin{lstlisting}[language=swift]
+enum Beverage: CaseIterable {
+    case coffee, tea, juice
+}
+let numberOfChoices = Beverage.allCases.count
+print("\(numberOfChoices) beverages available")
+// Prints "3 beverages available"
+\end{lstlisting}
+In the example above, you write @Beverage.allCases@ to access a collection that contains all of the cases of the @Beverage@ enumeration.
+You can use @allCases@ like any other collection -- the collection's elements are instances of the enumeration type, so in this case they're Beverage values.
+The example above counts how many cases there are, and the example below uses a for-in loop to iterate over all the cases.
+\begin{lstlisting}[language=swift]
+for beverage in Beverage.allCases {
+    print(beverage)
+}
+// coffee
+// tea
+// juice
+\end{lstlisting}
+The syntax used in the examples above marks the enumeration as conforming to the @CaseIterable@ protocol.
+For information about protocols, see Protocols.
+
+\paragraph{Associated Values}
+The examples in the previous section show how the cases of an enumeration are a defined (and typed) value in their own right.
+You can set a constant or variable to Planet.earth, and check for this value later.
+However, it's sometimes useful to be able to store values of other types alongside these case values.
+This additional information is called an associated value, and it varies each time you use that case as a value in your code.
+
+You can define Swift enumerations to store associated values of any given type, and the value types can be different for each case of the enumeration if needed.
+Enumerations similar to these are known as discriminated unions, tagged unions, or variants in other programming languages.
+
+For example, suppose an inventory tracking system needs to track products by two different types of barcode.
+Some products are labeled with 1D barcodes in UPC format, which uses the numbers 0 to 9.
+Each barcode has a number system digit, followed by five manufacturer code digits and five product code digits.
+These are followed by a check digit to verify that the code has been scanned correctly:
+
+Other products are labeled with 2D barcodes in QR code format, which can use any ISO 8859-1 character and can encode a string up to 2,953 characters long:
+
+It's convenient for an inventory tracking system to store UPC barcodes as a tuple of four integers, and QR code barcodes as a string of any length.
+
+In Swift, an enumeration to define product barcodes of either type might look like this:
+\begin{lstlisting}[language=swift]
+enum Barcode {
+    case upc(Int, Int, Int, Int)
+    case qrCode(String)
+}
+\end{lstlisting}
+This can be read as:
+\begin{quote}
+"Define an enumeration type called Barcode, which can take either a value of upc with an associated value of type @(Int, Int, Int, Int)@, or a value of @qrCode@ with an associated value of type @String@."
+\end{quote}
+This definition doesn't provide any actual @Int@ or @String@ values -- it just defines the type of associated values that Barcode constants and variables can store when they're equal to @Barcode.upc@ or @Barcode.qrCode@.
+
+You can then create new barcodes using either type:
+\begin{lstlisting}[language=swift]
+var productBarcode = Barcode.upc(8, 85909, 51226, 3)
+\end{lstlisting}
+This example creates a new variable called @productBarcode@ and assigns it a value of @Barcode.upc@ with an associated tuple value of @(8, 85909, 51226, 3)@.
+
+You can assign the same product a different type of barcode:
+\begin{lstlisting}[language=swift]
+productBarcode = .qrCode("ABCDEFGHIJKLMNOP")
+\end{lstlisting}
+At this point, the original @Barcode.upc@ and its integer values are replaced by the new @Barcode.qrCode@ and its string value.
+Constants and variables of type Barcode can store either a @.upc@ or a @.qrCode@ (together with their associated values), but they can store only one of them at any given time.
+
+You can check the different barcode types using a switch statement, similar to the example in Matching Enumeration Values with a Switch Statement.
+This time, however, the associated values are extracted as part of the switch statement.
+You extract each associated value as a constant (with the let prefix) or a variable (with the var prefix) for use within the switch case's body:
+\begin{lstlisting}[language=swift][language=swift]
+switch productBarcode {
+case .upc(let numberSystem, let manufacturer, let product, let check):
+    print("UPC: \(numberSystem), \(manufacturer), \(product), \(check).")
+case .qrCode(let productCode):
+    print("QR code: \(productCode).")
+}
+// Prints "QR code: ABCDEFGHIJKLMNOP."
+\end{lstlisting}
+If all of the associated values for an enumeration case are extracted as constants, or if all are extracted as variables, you can place a single let or var annotation before the case name, for brevity:
+\begin{lstlisting}[language=swift]
+switch productBarcode {
+case let .upc(numberSystem, manufacturer, product, check):
+    print("UPC : \(numberSystem), \(manufacturer), \(product), \(check).")
+case let .qrCode(productCode):
+    print("QR code: \(productCode).")
+}
+// Prints "QR code: ABCDEFGHIJKLMNOP."
+\end{lstlisting}
+
+\paragraph{Raw Values}
+
+The barcode example in Associated Values shows how cases of an enumeration can declare that they store associated values of different types.
+As an alternative to associated values, enumeration cases can come prepopulated with default values (called raw values), which are all of the same type.
+
+Here's an example that stores raw ASCII values alongside named enumeration cases:
+\begin{lstlisting}[language=swift]
+enum ASCIIControlCharacter: Character {
+    case tab = "\t"
+    case lineFeed = "\n"
+    case carriageReturn = "\r"
+}
+\end{lstlisting}
+Here, the raw values for an enumeration called ASCIIControlCharacter are defined to be of type Character, and are set to some of the more common ASCII control characters.
+Character values are described in Strings and Characters.
+
+Raw values can be strings, characters, or any of the integer or floating-point number types.
+Each raw value must be unique within its enumeration declaration.
+
+Note
+
+Raw values are not the same as associated values.
+Raw values are set to prepopulated values when you first define the enumeration in your code, like the three ASCII codes above.
+The raw value for a particular enumeration case is always the same.
+Associated values are set when you create a new constant or variable based on one of the enumeration's cases, and can be different each time you do so.
+Implicitly Assigned Raw Values
+
+When you're working with enumerations that store integer or string raw values, you don't have to explicitly assign a raw value for each case.
+When you don't, Swift automatically assigns the values for you.
+
+For example, when integers are used for raw values, the implicit value for each case is one more than the previous case.
+If the first case doesn't have a value set, its value is 0.
+
+The enumeration below is a refinement of the earlier Planet enumeration, with integer raw values to represent each planet's order from the sun:
+
+\begin{lstlisting}[language=swift]
+enum Planet: Int {
+    case mercury = 1, venus, earth, mars, jupiter, saturn, uranus, neptune
+}
+\end{lstlisting}
+In the example above, Planet.mercury has an explicit raw value of 1, Planet.venus has an implicit raw value of 2, and so on.
+
+When strings are used for raw values, the implicit value for each case is the text of that case's name.
+
+The enumeration below is a refinement of the earlier CompassPoint enumeration, with string raw values to represent each direction's name:
+\begin{lstlisting}[language=swift]
+enum CompassPoint: String {
+    case north, south, east, west
+}
+\end{lstlisting}
+In the example above, CompassPoint.south has an implicit raw value of "south", and so on.
+
+You access the raw value of an enumeration case with its rawValue property:
+\begin{lstlisting}[language=swift]
+let earthsOrder = Planet.earth.rawValue
+// earthsOrder is 3
+
+let sunsetDirection = CompassPoint.west.rawValue
+// sunsetDirection is "west"
+\end{lstlisting}
+
+\paragraph{Initializing from a Raw Value}
+
+If you define an enumeration with a raw-value type, the enumeration automatically receives an initializer that takes a value of the raw value's type (as a parameter called rawValue) and returns either an enumeration case or nil.
+You can use this initializer to try to create a new instance of the enumeration.
+
+This example identifies Uranus from its raw value of 7:
+\begin{lstlisting}[language=swift]
+let possiblePlanet = Planet(rawValue: 7)
+// possiblePlanet is of type Planet? and equals Planet.uranus
+\end{lstlisting}
+Not all possible Int values will find a matching planet, however.
+Because of this, the raw value initializer always returns an optional enumeration case.
+In the example above, possiblePlanet is of type Planet?, or "optional Planet."
+Note
+
+The raw value initializer is a failable initializer, because not every raw value will return an enumeration case.
+For more information, see Failable Initializers.
+
+If you try to find a planet with a position of 11, the optional Planet value returned by the raw value initializer will be nil:
+\begin{lstlisting}[language=swift]
+let positionToFind = 11
+if let somePlanet = Planet(rawValue: positionToFind) {
+    switch somePlanet {
+    case .earth:
+        print("Mostly harmless")
+    default:
+        print("Not a safe place for humans")
+    }
+} else {
+    print("There isn't a planet at position \(positionToFind)")
+}
+// Prints "There isn't a planet at position 11"
+\end{lstlisting}
+This example uses optional binding to try to access a planet with a raw value of 11.
+The statement if let somePlanet = Planet(rawValue: 11) creates an optional Planet, and sets somePlanet to the value of that optional Planet if it can be retrieved.
+In this case, it isn't possible to retrieve a planet with a position of 11, and so the else branch is executed instead.
+
+\paragraph{Recursive Enumerations}
+
+A recursive enumeration is an enumeration that has another instance of the enumeration as the associated value for one or more of the enumeration cases.
+You indicate that an enumeration case is recursive by writing indirect before it, which tells the compiler to insert the necessary layer of indirection.
+
+For example, here is an enumeration that stores simple arithmetic expressions:
+\begin{lstlisting}[language=swift]
+enum ArithmeticExpression {
+    case number(Int)
+    indirect case addition(ArithmeticExpression, ArithmeticExpression)
+    indirect case multiplication(ArithmeticExpression, ArithmeticExpression)
+}
+\end{lstlisting}
+You can also write indirect before the beginning of the enumeration to enable indirection for all of the enumeration's cases that have an associated value:
+\begin{lstlisting}[language=swift]
+indirect enum ArithmeticExpression {
+    case number(Int)
+    case addition(ArithmeticExpression, ArithmeticExpression)
+    case multiplication(ArithmeticExpression, ArithmeticExpression)
+}
+\end{lstlisting}
+This enumeration can store three kinds of arithmetic expressions: a plain number, the addition of two expressions, and the multiplication of two expressions.
+The addition and multiplication cases have associated values that are also arithmetic expressions -- these associated values make it possible to nest expressions.
+For example, the expression (5 + 4) * 2 has a number on the right-hand side of the multiplication and another expression on the left-hand side of the multiplication.
+Because the data is nested, the enumeration used to store the data also needs to support nesting -- this means the enumeration needs to be recursive.
+The code below shows the ArithmeticExpression recursive enumeration being created for (5 + 4) * 2:
+\begin{lstlisting}[language=swift]
+let five = ArithmeticExpression.number(5)
+let four = ArithmeticExpression.number(4)
+let sum = ArithmeticExpression.addition(five, four)
+let product = ArithmeticExpression.multiplication(sum, ArithmeticExpression.number(2))
+\end{lstlisting}
+A recursive function is a straightforward way to work with data that has a recursive structure.
+For example, here's a function that evaluates an arithmetic expression:
+\begin{lstlisting}[language=swift]
+func evaluate(_ expression: ArithmeticExpression) -> Int {
+    switch expression {
+    case let .number(value):
+        return value
+    case let .addition(left, right):
+        return evaluate(left) + evaluate(right)
+    case let .multiplication(left, right):
+        return evaluate(left) * evaluate(right)
+    }
+}
+
+print(evaluate(product))
+// Prints "18"
+\end{lstlisting}
+This function evaluates a plain number by simply returning the associated value.
+It evaluates an addition or multiplication by evaluating the expression on the left-hand side, evaluating the expression on the right-hand side, and then adding them or multiplying them.
+
+
+\section{\CC}
+\label{s:C++RelatedWork}
+
+\CC is backwards compatible with C, so it inherited C's enumerations.
+However, the following non-backwards compatible changes have been made.
+\begin{quote}
+7.2 Change: \CC objects of enumeration type can only be assigned values of the same enumeration type.
+In C, objects of enumeration type can be assigned values of any integral type. \\
+Example:
+\begin{lstlisting}[language=c++]
+enum color { red, blue, green };
+color c = 1;			 				$\C{// valid C, invalid C++}$
+\end{lstlisting}
+\textbf{Rationale}: The type-safe nature of C++. \\
+\textbf{Effect on original feature}: Deletion of semantically well-defined feature. \\
+\textbf{Difficulty of converting}: Syntactic transformation. (The type error produced by the assignment can be automatically corrected by applying an explicit cast.) \\
+\textbf{How widely used}: Common.
+\end{quote}
+\begin{quote}
+7.2 Change: In \CC, the type of an enumerator is its enumeration.
+In C, the type of an enumerator is @int@. \\
+Example:
+\begin{lstlisting}[language=c++]
+enum e { A };
+sizeof(A) == sizeof(int)		 		$\C{// in C}$
+sizeof(A) == sizeof(e)		 			$\C{// in C++}$
+/* and sizeof(int) is not necessary equal to sizeof(e) */
+\end{lstlisting}
+\textbf{Rationale}: In C++, an enumeration is a distinct type. \\
+\textbf{Effect on original feature}: Change to semantics of well-defined feature. \\
+\textbf{Difficulty of converting}: Semantic transformation. \\
+\textbf{How widely used}: Seldom. The only time this affects existing C code is when the size of an enumerator is taken.
+Taking the size of an enumerator is not a common C coding practice.
+\end{quote}
+Hence, the values in a \CC enumeration can only be its enumerators (without a cast).
+While the storage size of an enumerator is up to the compiler, there is still an implicit cast to @int@.
+\begin{lstlisting}[language=c++]
+enum E { A, B, C };
+E e = A;
+int i = A;   i = e;	 					$\C{// implicit casts to int}$
+\end{lstlisting}
+\CC{11} added a scoped enumeration, \lstinline[language=c++]{enum class} (or \lstinline[language=c++]{enum struct}), so the enumerators are local to the enumeration and must be accessed using type qualification.
+\begin{lstlisting}[language=c++,{moredelim=**[is][\color{red}]{@}{@}}]
+enum class E { A, B, C };
+E e = @E::@A;	 						$\C{// qualified enumerator}$
+e = B;	 								$\C{// B not in scope}$
+\end{lstlisting}
+\CC{20} supports unscoped access with a \lstinline[language=c++]{using enum} declaration.
+\begin{lstlisting}[language=c++,{moredelim=**[is][\color{red}]{@}{@}}]
+enum class E { A, B, C };
+@using enum E;@
+E e = A;	 							$\C{// direct access}$
+e = B;	 								$\C{// direct access}$
+\end{lstlisting}
+\CC{11} added the ability to explicitly declare the underlying integral type for \lstinline[language=c++]{enum class}.
+\begin{lstlisting}[language=c++,{moredelim=**[is][\color{red}]{@}{@}}]
+enum class RGB @: long@ { Red, Green, Blue };
+enum class rgb @: char@ { Red = 'r', Green = 'g', Blue = 'b' };
+enum class srgb @: signed char@ { Red = -1, Green = 0, Blue = 1 };
+\end{lstlisting}
+There is no implicit conversion from the \lstinline[language=c++]{enum class} type and to its type.
+\begin{lstlisting}[language=c++,{moredelim=**[is][\color{red}]{@}{@}}]
+rgb crgb = rgb::Red;
+char ch = rgb::Red;   ch = crgb;		$\C{// disallowed}$
+\end{lstlisting}
+Finally, there is no mechanism to iterate through an enumeration nor use the enumeration type to declare an array dimension.
+
+
+\section{Go}
+
+\section{Java}
+
+\section{Modula-3}
+
+\section{Rust}
+
+\section{Swift}
+
+\section{Python}
+
+\section{Algebraic Data Type}
Index: doc/theses/jiada_liang_MMath/uw-ethesis-frontpgs.tex
===================================================================
--- doc/theses/jiada_liang_MMath/uw-ethesis-frontpgs.tex	(revision 6bd9f9e171271e7c6ac898b1dbf78fc75e68e592)
+++ doc/theses/jiada_liang_MMath/uw-ethesis-frontpgs.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
@@ -131,5 +131,8 @@
 \begin{center}\textbf{Abstract}\end{center}
 
-Enumerated type ...
+An enumeration is a type defining an ordered set of named constant values, where a name abstracts a value, e.g., @PI@ versus @3.145159@.
+C restrict an enumeration type to the integral type @signed int@, which \CC support , meaning enumeration names bind to integer constants.
+\CFA extends C enumerations to allow all basic and custom types for the enumeration type, like other modern programming languages.
+Furthermore, \CFA adds other useful features for enumerations to support better software-engineering practices and simplify program development.
 
 \cleardoublepage
Index: doc/theses/jiada_liang_MMath/uw-ethesis.tex
===================================================================
--- doc/theses/jiada_liang_MMath/uw-ethesis.tex	(revision 6bd9f9e171271e7c6ac898b1dbf78fc75e68e592)
+++ doc/theses/jiada_liang_MMath/uw-ethesis.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
@@ -211,6 +211,7 @@
 \input{intro}
 \input{background}
-\input{content1}
-\input{content2}
+\input{CFAenum}
+\input{implementation}
+\input{relatedwork}
 \input{performance}
 \input{conclusion}
