Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 3ac5fd8bcb3728ce8676e2b55b9fd4f691a06719)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 02101a45a08b3935b33cad46118592615c09f3a2)
@@ -53,11 +53,4 @@
 enum E { A, B, C, D, @N@ };  // N == 4
 \end{cfa}
-
-The underlying representation of \CFA enumeration object is its position, saved as an integral type.
-Therefore, the size of a \CFA enumeration is consistent with a C enumeration.
-Attribute function @posn@ performs type substitution on an expression from \CFA type to an integral type.
-The label and value of an enumerator are stored in a global data structure for each enumeration, where attribute functions @label@/@value@ map an \CFA enumeration object to the corresponding data.
-These operations do not apply to C Enums because backward compatibility means the necessary backing data structures cannot be supplied.
-
 
 \section{Opaque Enumeration}
@@ -138,7 +131,48 @@
 calling constructors happens at runtime (dynamic).
 
+\section{Implementation}
+\CFA-cc is is a transpiler that translates \CFA code into C, which can later be compiled by a C compiler.
+
+During the transpilation, \CFA-cc breaks a \CFA enumeration definition into a definition of a C enumeration with the same name and auxiliary arrays: a label array and a value array for a typed enumeration.
+For example:
+\begin{cfa}
+// CFA (source):
+enum(T) E { E1=t1, E2=t2, E3=t3 };
+\end{cfa}
+is compiled into:
+\begin{cfa}
+// C (transpiled by cfa-cc):
+enum E { E1, E2, E3 };
+const char * E_labels[3] = { "E1", "E2", "E3" };
+const T E_values [3] = { t1, t2, t3 };
+\end{cfa}
+The generated C enumeration will have enumerator values equals to their positions thanks to C's auto-initialization scheme. Notice that value and label arrays are dynamically allocated data structures that take up 
+memory. If an enumeration is globally defined, the arrays are allocated in the @.data@ section and will be initialized before the program execution.
+Otherwise, if an enumeration has its definition in a local scope, these arrays will be allocated on the stack and be initialized when the program counter 
+reaches the code location of the enumeration definition.
+
+% This bring a considerable overhead to the program, in terms of both execution time and storage. 
+% An opaque enumeration has no overhead 
+% for values, and it has been suggested as a future work to leave as an option to not generate the label array.
+
+Alongs with the enumeration defintion, \CFA-cc adds defintions of attribute functions: @posn@, @label@ and @value@: 
+\begin{cfa}
+inline int posn( E e ) { return (int) e; }
+inline const * label( E e ) { return E_labels[ (int) e ]; }
+inline const * E_value( E e ) { return E_values[ (int) e ]; }
+\end{cfa}
+These functions are not implemented in \CFA code: they are Abstract Syntax Tree (AST) nodes appends to the Abstract Syntax Tree (AST).
+Notably, the AST subnode for the "cast to @int@" expression inside the functions is annotated as reinterpreted casts.
+In order words, the effect of a case is only to change the type of an expression, and it stops further reduction on the expression \see{\VRef{s:ValueConversion}}.
+
+Consequently, \CFA enumeration comes with space and runtime overhead, both for enumeration definition and function call to attribute functions. \CFA made efforts to reduce the runtime 
+overhead on function calls by aggressively reducing @label()@ and @value()@ function calls on an enumeration constant to a constant expression. The interpreted casts are extraneous 
+after type checking and removed in later steps. A @label()@ and @value()@ call on an enumeration variable is a lookup of an element of an array of constant values, and it is up to the 
+C compiler to optimize its runtime. While OpaqueEnum is effectively an "opt-out" of the value overhead, it has been suggested that an option to "opt-out" from labels be added as well.
+A @label()@ function definition is still necessary to accomplish enumeration traits. But it will return an empty string for an enumeration label when "opt-out" or the enumerator name 
+when it is called on an enumeration constant. It will allow a user not to pay the overhead for labels when the enumerator names of a particular enumerated type are not helpful.
 
 \section{Value Conversion}
-
+\label{s:ValueConversion}
 C has an implicit type conversion from an enumerator to its base type @int@.
 Correspondingly, \CFA has an implicit conversion from a typed enumerator to its base type, allowing typed enumeration to be seamlessly used as the value of its base type
@@ -191,4 +225,9 @@
 enum(S) E { A, B, C, D };
 \end{cfa}
+
+The restriction on C's enumeration initializers being constant expression is relaxed on \CFA enumeration. 
+Therefore, an enumerator initializer allows function calls like @?+?( S & s, one_t )@ and @?{}( S & s, zero_t )@. 
+It is because the values of \CFA enumerators are not stored in the compiled enumeration body but in the @value@ array, which 
+allows dynamic initialization.
 
 \section{Subset}
@@ -520,5 +559,5 @@
 The enumerators in the @case@ clause use the enumerator position for testing.
 The prints use @label@ to print an enumerator's name.
-Finally, a loop enumerates through the planets computing the weight on each planet for a given earth mass.
+Finally, a loop enumerates through the planets computing the weight on each planet for a given Earth mass.
 The print statement does an equality comparison with an enumeration variable and enumerator (@p == MOON@).
 
