Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision d93b8131b6d6f864fdf457bb174840310cb9dfd1)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision dcfcf368f79594eb9cffea05e52b6e6ca5967954)
@@ -71,4 +71,6 @@
 char * s = label( O_TRUNC );			$\C{// "O\_TRUNC"}$
 int open = posn( O_WRONLY );			$\C{// 1}$
+s = label( mode );						$\C{// "O\_RDONLY"}$
+int open = posn( mode );				$\C{// 0}$
 \end{cfa}
 Equality and relational operations are available.
@@ -131,40 +133,33 @@
 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.
+
+\CFA-cc is is a transpiler translating \CFA code into C, which is compiled by a C compiler.
+During transpilation, \CFA-cc breaks a \CFA enumeration definition into a definition of a C enumeration with the same name and auxiliary arrays: a label and value array for a typed enumeration.
 For example:
 \begin{cfa}
-// CFA (source):
-enum(T) E { E1=t1, E2=t2, E3=t3 };
+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 resemble \CFA enumerator positions thanks to C's auto-initialization scheme.
-A \CFA enumeration variable definition is same in \CFA and C, before or after the transpilation.
-For example:
+static const char * E_labels[3] = { "E1", "E2", "E3" };
+static const T E_values[3] = { t1, t2, t3 };
+\end{cfa}
+The generated C enumeration has enumerator values that match \CFA enumerator positions because of C's auto-initialization.
+A \CFA enumeration variable definition is the same in \CFA as C, \eg:
 \begin{cfa}
 enum E e = E1;
-e;
-\end{cfa}
-These two expressions will not change by \CFA-cc. A \CFA enumeration variable will always have the same underlying representation as its generated 
-C enumeration. This implies \CFA enumeration variable does not take up extra memory and \CFA enumeration use @posn@ as its underlying representation.
-
-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@: 
+e = E2;
+\end{cfa}
+so these expressions remain unchanged by \CFA-cc.
+Therefore, a \CFA enumeration variable has the same underlying representation as its generated C enumeration.
+This semantics implies a \CFA enumeration variable does not use memory, that @posn@ can use its underlying representation, and the label and value arrays take little storage.
+It should be possible to eliminated the two arrays if unused, either by \CFA if local to a translation unit and unused, or by the linker if global but unreferenced.
+Also, the label and value arrays are declared @static@ and initialized with constants, so the arrays are allocated in the @.data@ section and initialized before program execution.
+Hence, there is no addition execution cost unless new enumeration features are use, and storage usage is minimal as the number of enumerations in a program is small as is the number of enumerators in an enumeration.
+
+Along with the enumeration definition, \CFA-cc generates definitions of the attribute functions, @posn@, @label@ and @value@, for each enumeration:
 \begin{cfa}
 inline int posn( E e ) { return (int) e; }
@@ -172,14 +167,10 @@
 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.
+where the function calls are normally inlined by the backend C compiler into a few instructions.
+These functions simplify the job of getting the enumerations types through the type system in the same way as normal functions and calls.
+Note, the cast to @int@ is actually an internal reinterpreted cast added before type resolution to stop further reduction on the expression by the type resolver \see{\VRef{s:ValueConversion}} and removed in code generation.
+Finally, to further mitigate \CFA enumeration costs, calls to @label@ and @value@ with an enumeration constant are unrolled into the appropriate constant expression, although this could be left to the backend C compiler.
+Hence, in space and time costs, \CFA enumerations follow the C philosophy of only paying for what is used, modulo some future work to convince the linker to remove unaccessed @label@ and @value@ arrays, possibly with @weak@ attributes.
+
 
 \section{Value Conversion}
@@ -214,5 +205,5 @@
 % \begin{cfa}
 % forall(T | @CfaEnum(T)@) void bar(T);
-% 
+%
 % bar(a);					$\C{// (3), with cost (0, 0, 1, 0, 0, 0, 0, 0)}$
 % \end{cfa}
@@ -236,7 +227,7 @@
 \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 
+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.
 
@@ -249,5 +240,5 @@
 \end{cfa}
 Enumeration @Greek@ may have more or less enumerators than @Letter@, but its enumerator values \emph{must} be from @Letter@.
-Therefore, the set of @Greek@ enumerator values in a subset of the @Letter@ enumerator values. 
+Therefore, the set of @Greek@ enumerator values in a subset of the @Letter@ enumerator values.
 @Letter@ is type compatible with enumeration @Letter@ because value conversions are inserted whenever @Letter@ is used in place of @Greek@.
 \begin{cfa}
@@ -291,5 +282,5 @@
 However, the position of the underlying representation is the order of the enumerator in the new enumeration.
 \begin{cfa}
-enum() E1 { B };									$\C{// B}$						
+enum() E1 { B };									$\C{// B}$
 enum() E2 { C, D };						$\C{// C D}$
 enum() E3 { inline E1, inline E2, E };	$\C{// {\color{red}[\(_{E1}\)} B {\color{red}]} {\color{red}[\(_{E2}\)} C D {\color{red}]} E}$
@@ -298,7 +289,7 @@
 In the example, @B@ is at position 0 in @E1@ and @E3@, but position 1 in @E4@ as @A@ takes position 0 in @E4@.
 @C@ is at position 0 in @E2@, 1 in @E3@, and 2 in @E4@.
-@D@ is at position 1 in @E2@, 2 in @E3@, and 3 in @E4@. 
-
-A subtype enumeration can be casted, or implicitly converted into its supertype, with a @safe@ cost, called \newterm{enumeration conversion}. 
+@D@ is at position 1 in @E2@, 2 in @E3@, and 3 in @E4@.
+
+A subtype enumeration can be casted, or implicitly converted into its supertype, with a @safe@ cost, called \newterm{enumeration conversion}.
 \begin{cfa}
 enum E2 e2 = C;
