Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 5aeb1a9edda09519a06785e0280d3cbe70f6fd15)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 38e20a80ff2d2e0f1bf7fef08b0948ab64d1abf0)
@@ -6,5 +6,7 @@
 % The following sections detail all of my new contributions to enumerations in \CFA.
 \CFA extends the enumeration declaration by parameterizing with a type (like a generic type).
-\begin{clang}[identifierstyle=\linespread{0.9}\it]
+
+
+\begin{cfa}[caption={CFA Enum},captionpos=b,label={l:CFAEnum}]
 $\it enum$-specifier:
 	enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { cfa-enumerator-list }
@@ -18,8 +20,9 @@
 	$\it inline$ identifier
 	enumeration-constant = expression
-\end{clang}
+\end{cfa}
+
 A \newterm{\CFA enumeration}, or \newterm{\CFA enum}, has an optional type declaration in the bracket next to the @enum@ keyword.
-Without optional type declarations, the syntax defines "opaque enums".
-Otherwise, \CFA enum with type declaration are "typed enums".
+Without optional type declarations, the syntax defines \newterm{opaque enums}.
+Otherwise, \CFA enum with type declaration are \newterm{typed enums}.
 
 \section{Opaque Enum}
@@ -27,17 +30,20 @@
 Opaque enum is a special CFA enumeration type, where the internal representation is chosen by the compiler and hidden from users.
 Compared C enum, opaque enums are more restrictive in terms of typing, and cannot be implicitly converted to integers.
-Enumerators of opaque enum cannot have initializer. Declaring initializer in the body of opaque enum results in a syntax error.
+Enumerators of opaque enum cannot have initializer. Declaring initializer in the body of opaque enum results in a compile error.
 \begin{cfa}
 enum@()@ Planets { MERCURY, VENUS, EARTH, MARS, JUPITER, SATURN, URANUS, NEPTUNE };
 
 Planet p = URANUS;
-@int i = VENUS; // Error, VENUS cannot be converted into an integral type@
-\end{cfa}
-Each opage enum has two @attributes@: @position@ and @label@. \CFA auto-generates @attribute functions@ @posn()@ and @label()@ for every \CFA enum to returns the respective attributes.
-\begin{cfa}
-// Auto-generated
-int posn(Planet p);
-char * s label(Planet p);
-\end{cfa}
+int i = VENUS; @// Error, VENUS cannot be converted into an integral type
+\end{cfa}
+% Each opaque enum has two @attributes@: @position@ and @label@. \CFA auto-generates @attribute functions@ @posn()@ and @label()@ for every \CFA enum to returns the respective attributes.
+Opaque enumerations have two defining properties: @label@ (name) and @order@ (position), exposed to users by predefined @attribute functions@ , with the following signatures:
+\begin{cfa}
+forall( E ) {
+	unsigned posn(E e);
+	const char * s label(E e);
+};
+\end{cfa}
+With polymorphic type parameter E being substituted by enumeration types such as @Planet@.
 
 \begin{cfa}
@@ -46,9 +52,8 @@
 \end{cfa}
 
-% \subsection{Representation}
-\CFA uses chooses signed int as the underlying representation of an opaque enum variable, holding the value of enumeration position. Therefore, @posn()@ is in fact a cast that bypassing type system, converting an 
-cfa enum to its integral representation.
-
-Labels information are stored in a global array. @label()@ is a function that maps enum position to an element of the array.
+\subsection{Representation}
+The underlying representation of \CFA enumeration object is its order, saved as an integral type. Therefore, the size of a \CFA enumeration is consistent with C enumeration.
+Attribute function @posn@ performs type substitution on an expression from \CFA type to integral type. 
+Names of enumerators are stored in a global data structure, with @label@ maps \CFA enumeration object to corresponding data.
 
 \section{Typed Enum}
@@ -56,5 +61,5 @@
 
 \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.
+Figure~\ref{f:EumeratorTyping} shows a series of examples illustrating that all \CFA types can be use with an enumeration and each type's values 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 logically rewritten with @const@.
@@ -70,5 +75,5 @@
 	enum( @_Complex@ ) Plane { X = 1.5+3.4i, Y = 7+3i, Z = 0+0.5i };
 // pointer
-	enum( @const char *@ ) Name { Fred = "FRED", Mary = "MARY", Jane = "JANE" };
+	enum( @char *@ ) Name { Fred = "FRED", Mary = "MARY", Jane = "JANE" };
 	int i, j, k;
 	enum( @int *@ ) ptr { I = &i,  J = &j,  K = &k };
@@ -107,30 +112,49 @@
 
 
-\subsection{Implicit Conversion}
+\subsection{Value Conversion}
 C has an implicit type conversion from an enumerator to its base type @int@.
-Correspondingly, \CFA has an implicit (safe) conversion from a typed enumerator to its base type.
+Correspondingly, \CFA has an implicit conversion from a typed enumerator to its base type.
 \begin{cfa}
 char currency = Dollar;
-string fred = Fred;						$\C{// implicit conversion from char * to \CFA string type}$
-Person student = Beth;
-\end{cfa}
-
-% The implicit conversion is accomplished by the compiler adding @value()@ function calls as a candidate with safe cost. Therefore, the expression
-% \begin{cfa}
-% char currency = Dollar;
-% \end{cfa}
-% is equivalent to
-% \begin{cfa}
-% char currency = value(Dollar);
-% \end{cfa}
-% Such conversion an @additional@ safe 
-
-The implicit conversion is accomplished by the resolver adding call to @value()@ functions as a resolution candidate with a @implicit@ cost.
-Implicit cost is an additional category to Aaron's cost model. It is more signicant than @unsafe@ to have
-the compiler choosing implicit conversion over the narrowing conversion; It is less signicant to @poly@ 
-so that function overloaded with enum traits will be selected over the implicit. @Enum trait@ will be discussed in the chapter.
-
-Therefore, \CFA conversion cost is 8-tuple
-@@(unsafe, implicit, poly, safe, sign, vars, specialization, reference)@@
+void foo( char * );
+foo( Fred );
+\end{cfa}
+% \CFA enumeration being resolved as its base type because \CFA inserts an implicit @value()@ call on an \CFA enumeration.
+During the resolution of expression e with \CFA enumeration type, \CFA adds @value(e)@ as an additional candidate with an extra \newterm{value} cost.
+For expression @char currency = Dollar@, the is no defined conversion from Dollar (\CFA enumeration) type to basic type and the conversion cost is @infinite@, 
+thus the only valid candidate is @value(Dollar)@.
+
+@Value@ is a new category in \CFA's conversion cost model. It is defined to be a more significant factor than a @unsafe@ but weight less than @poly@.
+The resultin g conversion cost is a 8-tuple:
+@@(unsafe, value, poly, safe, sign, vars, specialization, reference)@@.
+
+\begin{cfa}
+void bar(int);
+enum(int) Month !{ 
+	January=31, February=29, March=31, April=30, May=31, June-30,
+	July=31, August=31, September=30, October=31, November=30, December=31
+};
+
+Month a = Februrary;	// (1), with cost (0, 1, 0, 0, 0, 0, 0, 0)
+double a = 5.5;			// (2), with cost (1, 0, 0, 0, 0, 0, 0, 0)
+
+bar(a);
+\end{cfa}
+In the previous example, candidate (1) has an value cost to parameter type int, with is lower than (2) as an unsafe conversion from double to int.
+\CFA chooses value cost over unsafe cost and therefore @a@ of @bar(a)@ is resolved as an @Month@.
+
+\begin{cfa}
+forall(T | @CfaEnum(T)@) void bar(T);
+
+bar(a);					// (3), with cost (0, 0, 1, 0, 0, 0, 0, 0)
+\end{cfa}
+% @Value@ is designed to be less significant than @poly@ to allow function being generic over \CFA enumeration (see ~\ref{c:trait}). 
+Being generic over @CfaEnum@ traits (a pre-defined interface for \CFA enums) is a practice in \CFA to implement functions over \CFA enumerations, as will see in chapter~\ref{c:trait}.
+@Value@ is a being a more significant cost than @poly@ implies if a overloaeded function defined for @CfaEnum@ (and other generic type), \CFA always 
+try to resolve it as a @CfaEnum@, rather to insert a @value@ conversion.
+
+\subsection{Coercion}
+While implicit conversion from a \CFA enumeration has been disabled, a explicit coercion cast to basic type is still possible to be consistent with C. In which case, 
+\CFA converts a \CFA enumeration variable as a basic type, with the value of the @position@ of the variable.
 
 \section{Auto Initialization} 
@@ -145,43 +169,23 @@
 The complexity of the constant expression depends on the level of runtime computation the compiler implements, \eg \CC \lstinline[language={[GNU]C++}]{constexpr} provides complex compile-time computation across multiple types, which blurs the compilation/runtime boundary.
 
-% The notion of auto-initialization can be generalized in \CFA through the trait @AutoInitializable@.
-% \begin{cfa}
-% forall(T) @trait@ AutoInitializable {
-% 	void ?{}( T & o, T v );				$\C{// initialization}$
-% 	void ?{}( T & t, zero_t );			$\C{// 0}$
-% 	T ?++( T & t);						$\C{// increment}$
-% };
-% \end{cfa}
-% In addition, there is an implicit enumeration counter, @ecnt@ of type @T@, managed by the compiler.
-% For example, the type @Odd@ satisfies @AutoInitializable@:
-% \begin{cfa}
-% struct Odd { int i; };
-% void ?{}( Odd & o, int v ) { if ( v & 1 ) o.i = v; else /* error not odd */ ; };
-% void ?{}( Odd & o, zero_t ) { o.i = 1; };
-% Odd ?++( Odd o ) { return (Odd){ o.i + 2 }; };
-% \end{cfa}
-% and implicit initialization is available.
-% \begin{cfa}
-% enum( Odd ) { A, B, C = 7, D };			$\C{// 1, 3, 7, 9}$
-% \end{cfa}
-% where the compiler performs the following transformation and runs the code.
-% \begin{cfa}
-% enum( Odd ) {
-% 	?{}( ecnt, @0@ }  ?{}( A, ecnt },	?++( ecnt )  ?{}( B, ecnt ),
-% 	?{}( ecnt, 7 )  ?{}( C, ecnt ),	?++( ecnt )  ?{}( D, ecnt )
-% };
-% \end{cfa}
-
-The notion of auto-initialization is generalized in \CFA enum in the following way:
-Enumerator e is the first enumerator of \CFA enumeration E with base type T. If e declares no no initializer, e is auto-initialized by the $zero\_t$ constructor of T.
-\CFA reports a compile time error if T has no $zero\_t$ constructor.
-Enumerator e is an enumerator of base-type T enumeration E that position i, where $i \neq 0$. And d is the enumerator with position @i-1@, e is auto-initialized with 
-the result of @value(d)++@. If operator @?++@ is not defined for type T, \CFA reports a compile time error.
-
-Unfortunately, auto-initialization is not implemented because \CFA is only a transpiler, relying on generated C code to perform the detail work.
+% The notion of auto-initialization is generalized in \CFA enumertation E with base type T in the following way:
+When an enumerator @e@ does not have a initializer, if @e@ has enumeration type @E@ with base type @T@, \CFA auto-initialize @e@ with the following scheme:
+\begin{enumerate}
+% \item Enumerator e is the first enumerator of \CFA enumeration E with base type T. If e declares no no initializer, e is auto-initialized by the $zero\_t$ constructor of T.
+\item if e is first enumerator, e is initialized with T's @zero_t@.
+\item otherwise, if d is the enumerator defined just before e, with d has has been initialized with expression @l@ (@l@ can also be an auto-generated), e is initialized with @l++@. 
+% \CFA reports a compile time error if T has no $zero\_t$ constructor.
+% Enumerator e is an enumerator of base-type T enumeration E that position i, where $i \neq 0$. And d is the enumerator with position @i-1@, e is auto-initialized with 
+% the result of @value(d)++@. If operator @?++@ is not defined for type T, \CFA reports a compile time error.
+
+% Unfortunately, auto-initialization is not implemented because \CFA is only a transpiler, relying on generated C code to perform the detail work.
+% C does not have the equivalent of \CC \lstinline[language={[GNU]C++}]{constexpr}, and it is currently beyond the scope of the \CFA project to implement a complex runtime interpreter in the transpiler.
+% Nevertheless, the necessary language concepts exist to support this feature.
+\end{enumerate}
+while @?++( T )@ can be explicitly overloaded or implicitly overloaded with properly defined @one_t@ and @?+?(T, T)@.
+
+Unfortunately, auto-initialization with only constant expression is not enforced because \CFA is only a transpiler, relying on generated C code to perform the detail work.
 C does not have the equivalent of \CC \lstinline[language={[GNU]C++}]{constexpr}, and it is currently beyond the scope of the \CFA project to implement a complex runtime interpreter in the transpiler.
 Nevertheless, the necessary language concepts exist to support this feature.
-
-
 
 \section{Enumeration Inheritance}
@@ -292,5 +296,5 @@
 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 position.
+In these contexts, a programmer's intuition assumes an implicit conversion to position.
 
 For example, an intuitive use of enumerations is with the \CFA @switch@/@choose@ statement, where @choose@ performs an implicit @break@ rather than a fall-through at the end of a @case@ clause.
