Index: doc/proposals/enum.tex
===================================================================
--- doc/proposals/enum.tex	(revision d1551a50f54c708e4d86991165a951c6c80fae9b)
+++ doc/proposals/enum.tex	(revision dd1ebb19c6c8f45df1b0b974cfc7f695804381b9)
@@ -7,4 +7,5 @@
 \usepackage{graphics}
 \usepackage{xspace}
+\usepackage{calc}										% latex arithmetic
 
 \makeatletter
@@ -22,4 +23,19 @@
 \newcommand{\@newterm}[2][\@empty]{\lowercase{\def\temp{#2}}{\newtermFontInline{#2}}\ifx#1\@empty\index{\temp}\else\index{#1@{\protect#2}}\fi}
 \newcommand{\@snewterm}[2][\@empty]{{\newtermFontInline{#2}}\ifx#1\@empty\index{#2}\else\index{#1@{\protect#2}}\fi}
+
+\newcommand{\LstBasicStyle}[1]{{\lst@basicstyle{#1}}}
+\newcommand{\LstKeywordStyle}[1]{{\lst@basicstyle{\lst@keywordstyle{#1}}}}
+\newcommand{\LstCommentStyle}[1]{{\lst@basicstyle{\lst@commentstyle{#1}}}}
+\newcommand{\LstStringStyle}[1]{{\lst@basicstyle{\lst@stringstyle{#1}}}}
+\newcommand{\LstNumberStyle}[1]{{\lst@basicstyle{\lst@numberstyle{#1}}}}
+
+\newlength{\gcolumnposn}				% temporary hack because lstlisting does not handle tabs correctly
+\newlength{\columnposn}
+\setlength{\gcolumnposn}{3in}
+\setlength{\columnposn}{\gcolumnposn}
+\newcommand{\setgcolumn}[1]{\global\gcolumnposn=#1\global\columnposn=\gcolumnposn}
+\newcommand{\C}[2][\@empty]{\ifx#1\@empty\else\global\setlength{\columnposn}{#1}\global\columnposn=\columnposn\fi\hfill\makebox[\textwidth-\columnposn][l]{\LstCommentStyle{#2}}}
+\newcommand{\CD}[2][\@empty]{\ifx#1\@empty\else\global\setlength{\columnposn}{#1}\global\columnposn=\columnposn\fi\hfill\makebox[\textwidth-\columnposn][l]{\LstBasicStyle{#2}}}
+\newcommand{\CRT}{\global\columnposn=\gcolumnposn}
 \makeatother
 
@@ -56,5 +72,5 @@
 
 \lstdefinestyle{CStyle}{
-%    backgroundcolor=\color{backgroundColour},   
+%    backgroundcolor=\color{backgroundColour},
 %    commentstyle=\color{mGreen},
 %    keywordstyle=\color{magenta},
@@ -64,15 +80,15 @@
     basicstyle=\small\linespread{0.9}\sf,	% reduce line spacing and use sanserif font
 %   basicstyle=\footnotesize,
-    breakatwhitespace=false,         
-%    breaklines=true,                 
-    captionpos=b,                    
-    keepspaces=true,                 
+    breakatwhitespace=false,
+%    breaklines=true,
+    captionpos=b,
+    keepspaces=true,
 	escapechar=\$,							% LaTeX escape in CFA code
-%    numbers=left,                    
-%    numbersep=5pt,                  
+%    numbers=left,
+%    numbersep=5pt,
 %    numberstyle=\tiny\color{mGray},
-%    showspaces=false,                
+%    showspaces=false,
     showstringspaces=false,
-%    showtabs=false,                  
+%    showtabs=false,
 	showlines=true,							% show blank lines at end of code
     tabsize=5,
@@ -93,21 +109,35 @@
 
 \begin{abstract}
-An enumeration is a type that defines a list of named constant values in C (and other languages).
-C and \CC use an integral type as the underlying representation of an enumeration.
-\CFA extends C enumerations to allow all basic and custom types for the inner representation.
+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 and \CC restrict an enumeration type to the integral type @signed int@, 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.
 \end{abstract}
 
+\section{Background}
+
+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), time (noon, New Years).
+Many programming languages capture this important 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.
+
+Specifically, an enumerated type is a type whose values are restricted to a fixed set of named constants.
+Fundamentally, 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.
+However, the values for basic types are not named, other than the programming-language supplied constants.
+
+
 \section{C-Style Enum}
 
-\CFA supports the C-Style enumeration using the same syntax and semantics.
+The C-Style enumeration has the following syntax and semantics.
 \begin{lstlisting}[label=lst:weekday]
-enum Weekday { Monday, Tuesday, Wednesday, Thursday=10, Friday, Saturday, Sunday };
+enum Weekday { Monday, Tuesday, Wednesday, Thursday@=10@, Friday, Saturday, Sunday };
                 $\(\uparrow\)$                                                                      $\(\uparrow\)$
     ${\rm \newterm{enumeration name}}$                                        ${\rm \newterm{enumerator names}}
 \end{lstlisting}
-The example defines an enumeration type @Weekday@ with ordered enumerators @Monday@, @Tuesday@, @Wednesday@, @Thursday@, @Friday@, @Saturday@ and @Sunday@.
+Here, the enumeration type @Weekday@ defines the ordered \newterm{enumerator}s @Monday@, @Tuesday@, @Wednesday@, @Thursday@, @Friday@, @Saturday@ and @Sunday@.
 The successor of @Tuesday@ is @Monday@ and the predecessor of @Tuesday@ is @Wednesday@.
-A C enumeration is an integral type, with consecutive enumerator values assigned by the compiler starting at zero or the next explicitly initialized value by the programmer.
-For example, @Monday@ to @Wednesday@ have values 0--2 implicitly set by the compiler, @Thursday@ is explicitly set to @10@ by the programmer, and @Friday@ to @Sunday@ have values 11--13 implicitly set by the compiler.
+A C enumeration is implemented by an integral type, with consecutive enumerator values assigned by the compiler starting at zero or the next explicitly initialized value.
+For example, @Monday@ to @Wednesday@ have values 0--2 implicitly set by the compiler, @Thursday@ is explicitly set to @10@, and @Friday@ to @Sunday@ have values 11--13 implicitly set by the compiler.
 
 There are 3 attributes for an enumeration: \newterm{position}, \newterm{label}, and \newterm{value}:
@@ -118,28 +148,37 @@
 \it position		& 0			& 1			& 2				& 3				& 4			& 5			& 6			\\
 \it label			& Monday	& Tuesday	& Wednesday		& Thursday		& Friday 	& Saturday	& Sunday	\\
-\it value			& 0			& 1			& 2				& 10			& 11		& 12		& 13
+\it value			& 0			& 1			& 2				& {\color{red}10}& 11		& 12		& 13
 \end{tabular}
 \end{cquote}
 
 The enumerators of an enumeration are unscoped, i.e., enumerators declared inside of an @enum@ are visible in the enclosing scope of the @enum@ type.
+Furthermore, there is an implicit bidirectional conversion between an enumeration and integral types.
 \begin{lstlisting}[label=lst:enum_scope]
 {
-	enum Weekday { ... };	// enumerators implicitly projected into local scope
+	enum Weekday { ... };				$\C{// enumerators implicitly projected into local scope}$
 	Weekday weekday = Monday;
-	weekday = Friday;
-	int i = Sunday  // i == 13
+	weekday = Friday;					$\C{// weekday == 11}$
+	int i = Sunday						$\C{// i == 13}$
+	weekday = 10000;					$\C{// undefined behaviour}$
 }
-int j = Wednesday; // ERROR! Wednesday is not declared in this scope
+int j = Wednesday;						$\C{// ERROR! Wednesday is not declared in this scope}$
 \end{lstlisting}
 
 \section{\CFA-Style Enum}
 
-A \CFA enumeration is parameterized by a type specifying each enumerator's type.
-\CFA allows any object type for the enumerators, and values assigned to enumerators must be from the declared type.
+\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.
+
+\subsection{Enumerator Typing}
+
+\CFA extends the enumeration by parameterizing the enumeration with a type for the enumerators, allowing enumerators to be assigned any values from the declared type.
 \begin{lstlisting}[label=lst:color]
-enum Colour( @char *@ ) { Red = "R", Green = "G", Blue = "B"  };
-\end{lstlisting}
-The type of @Colour@ is @char *@ and each enumerator is initialized with a C string.
-Only types with a defined ordering can be automatically initialized (see Section~\ref{s:AutoInitializable}).
+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{lstlisting}
+The types of the enumerators are @char@, @double@, and @char *@ and each enumerator is initialized with corresponding type values.
+% Only types with a defined ordering can be automatically initialized (see Section~\ref{s:AutoInitializable}).
 
 % An instance of \CFA-enum (denoted as @<enum_instance>@) is a label for the defined enum name.
@@ -158,44 +197,49 @@
 % $$<qualified\_expression> := <enum\_type>.<enumerator>$$
 \begin{lstlisting}
-Colour colour = @Colour.@Red;	// qualification
+Colour colour = @Colour.@Red;			$\C{// qualification}$
 colour = @Colour.@Blue;
 \end{lstlisting}
 
-\section{Enumeration Pseudo-functions}
+\subsection{Enumeration Pseudo-functions}
 Pseudo-functions are function-like operators that do not result in any run-time computations, i.e., like @sizeof@. Instead, the call to functions will be substituted into other expressions in compilation time.
 
-\subsection{Enumerator Attributes}
-The attributes of an enumerator are accessed by pseudo-functions @position@, @value@, and @label@. 
+\subsubsection{Enumerator Attributes}
+The attributes of an enumerator are accessed by pseudo-functions @position@, @value@, and @label@.
 \begin{lstlisting}
-int green_pos = @position@( Colour.Green );	// 1
-char * green_value = @value@( Colour.Green ); / "G"
-char * green_label = @label@( Colour.Green ); // "Green"
-\end{lstlisting}
-
-\subsection{enumerate()}
+int green_pos = @position@( Colour.Green );	$\C{// 1}$
+char * green_value = @value@( Colour.Green ); $\C{// "G"}$
+char * green_label = @label@( Colour.Green ); $\C{// "Green"}$
+\end{lstlisting}
+
+Enumeration Greek may have more or less enumerators than Letter, but the enumerator values must be from Letter. Therefore, 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. 
+
+\subsubsection{\lstinline{enumerate()}}
+
 \begin{lstlisting}[label=lst:c_switch]
 enum(int) C_ENUM { First, Second, Third = First, Fourth };
-int v(C_ENUM e) { 
-    switch( e ) {
-        case First: return 0; break;
-        case Second: return 1; break;
-        // case Thrid: return 2; break;
-        // case Fourth: return 3; break;
-    };
-};
-\end{lstlisting}
-In the @C_ENUM@ example, @Third@ is an alias of @First@ and @Fourth@ is an alias of @Second@. Programmers cannot make case branches for @Third@ and @Fourth@ because the switch statement matches cases by the enumerator's value. Case First and Third, or Second and Fourth, has duplicate case values. 
-
-@enumerate()@ is a pseudo-function that makes the switch statement match by an enumerator instead. 
+int v( C_ENUM e ) {
+	switch( e ) {
+		case First: return 0; break;
+		case Second: return 1; break;
+		// case Third: return 2; break;
+		// case Fourth: return 3; break;
+	};
+};
+\end{lstlisting}
+In the @C_ENUM@ example, @Third@ is an alias of @First@ and @Fourth@ is an alias of @Second@.
+Programmers cannot make case branches for @Third@ and @Fourth@ because the switch statement matches cases by the enumerator's value.
+Case @First@ and @Third@, or @Second@ and @Fourth@, has duplicate case values.
+
+@enumerate()@ is a pseudo-function that makes the switch statement match by an enumerator instead.
 \begin{lstlisting}[label=lst:c_switch_enumerate]
 enum(double) C_ENUM { First, Second, Third = First, Fourth };
-C_ENUM variable_a = First, variable_b = Second, variable_c = Thrid, variable_d = Fourth;
-int v(C_ENUM e) { 
-    switch( enumeratate( e ) ) {
-        case First: return e; break;
-        case Second: return value( e ); break;
-        case Thrid: return label( e ); break;
-        case Fourth: return position( e ); break;
-    };
+C_ENUM variable_a = First, variable_b = Second, variable_c = Third, variable_d = Fourth;
+int v(C_ENUM e) {
+	switch( enumeratate( e ) ) {
+		case First: return e; break;
+		case Second: return value( e ); break;
+		case Third: return label( e ); break;
+		case Fourth: return position( e ); break;
+	};
 };
 p(variable_a); // 0
@@ -205,5 +249,7 @@
 \end{lstlisting}
 
+
 \section{Enumeration Storage}
+
 
 \subsection{Enumeration Variable}
@@ -228,34 +274,39 @@
 >>> label( Colour, 1) -> char *
 \end{lstlisting}
-@T@ represents the type declared in the \CFA enumeration defined and @char *@ in the example. 
+@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.
 
+
 \subsection{Enumeration Data}
+
 \begin{lstlisting}[label=lst:enumeration_backing_data]
 enum(T) E { ... };
 // backing data
-T* E_values;
-char** E_labels;
-\end{lstlisting}
-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:
+T * E_values;
+char ** E_labels;
+\end{lstlisting}
+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.
+	\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}
 
 \subsection{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. 
+An \CFA enumeration with base type T can be used seamlessly as T, without explicitly calling the pseudo-function value.
 \begin{lstlisting}[label=lst:implicit_conversion]
 char * green_value = Colour.Green; // "G"
-// Is equivalent to 
+// Is equivalent to
 // char * green_value = value( Color.Green ); "G"
 \end{lstlisting}
 
+
 \subsection{Unification Distance}
+
 \begin{lstlisting}[label=lst:unification_distance_example]
 T_2 Foo(T1);
@@ -265,8 +316,8 @@
 @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.
+	\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}
 
@@ -278,8 +329,8 @@
 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.
+	\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}
 
@@ -288,4 +339,5 @@
 
 \subsection{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{lstlisting}[label=lst:variable_overload]
@@ -304,5 +356,5 @@
 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{lstlisting}[label=lst:function_overload]
-Colour green = Colour.Green; 
+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
@@ -326,5 +378,5 @@
 % 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. 
+% The \CFA compilers need to resolve an @EnumInstType@ as one of its attributes based on the current context.
 
 % \begin{lstlisting}[caption={Null Context}, label=lst:null_context]
@@ -379,5 +431,5 @@
 % }
 % \end{lstlisting}
-% % The conversion can work backward: in restrictive cases, attributes of can be implicitly converted back to the EnumInstType. 
+% % The conversion can work backward: in restrictive cases, attributes of can be implicitly converted back to the EnumInstType.
 % Backward conversion:
 % \begin{lstlisting}[caption={Unification Functions}, label=lst:unification_func_call]
@@ -389,12 +441,12 @@
 % \begin{lstlisting}[caption={Unification Functions}, label=lst:unification_func_call]
 % {
-%    Unification( EnumInstType<Colour>, int ) >>> label
+%	Unification( EnumInstType<Colour>, int ) >>> label
 % }
 % \end{lstlisting}
 % @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 
+% @5@ is a constant expression $\Rightarrow$ Compiler knows the value during the compilation $\Rightarrow$ turns it into
 % \begin{lstlisting}
 % {
-%    enum Colour colour = Colour.Green; 
+%	enum Colour colour = Colour.Green;
 % }
 % \end{lstlisting}
@@ -411,5 +463,5 @@
 % {
 % 	enum T (int) { ... } // Declaration
-% 	enum T t = 1; 
+% 	enum T t = 1;
 % }
 % \end{lstlisting}
@@ -423,5 +475,5 @@
 % 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 
+% 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
 
 % \subsection{Casting}
@@ -431,5 +483,5 @@
 % (int) Foo.A;
 % \end{lstlisting}
-% 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. 
+% 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.
 
 % \subsection{Value Conversion}
@@ -445,5 +497,5 @@
 % int j = value( Foo, a )
 % \end{lstlisting}
-% Similarly, the generated code for the third line is 
+% Similarly, the generated code for the third line is
 % \begin{lstlisting}
 % char * j = label( Foo, a )
@@ -455,5 +507,5 @@
 
 \subsection{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$. 
+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$.
 
 \subsection{Auto Initializable}
@@ -478,5 +530,5 @@
 Odd ?++( Odd t1 ) { return Odd( t1.i + 2); };
 \end{lstlisting}
-When the type of an enumeration is @AutoInitializable@, implicit initialization is available. 
+When the type of an enumeration is @AutoInitializable@, implicit initialization is available.
 \begin{lstlisting}[label=lst:sample_auto_Initializable_usage]
 enum AutoInitUsage(Odd) {
@@ -514,5 +566,5 @@
 @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: 
+\textbullet\ \CFA offers a shorthand for iterating all enumeration constants:
 \begin{lstlisting}[label=lst:range_functions]
 for ( Alphabet alph ) { sout | alph; }
@@ -567,5 +619,5 @@
 >>> 10 11 12 13 14 15 16 17 18
 \end{lstlisting}
-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 
+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{lstlisting}[label=lst:range_function_stepping_converted]
 for ( typeof( value(Sequence.A) ) s=value( Sequence.A ); s <= Sequence.D; s+=1  ) { sout | alph; }
@@ -579,5 +631,5 @@
 for ( char * alph; Alphabet )
 \end{lstlisting}
-This for-loop implicitly iterates every label of the enumeration, because a label is the only valid resolution to the ch with type @char *@ in this case.
+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{lstlisting}[label=lst:range_functions_label_implicit]
@@ -591,8 +643,8 @@
 % \begin{lstlisting}
 % enum T( int, char * ) {
-%     a=42, b="Hello World"
+%	 a=42, b="Hello World"
 % };
 % \end{lstlisting}
-% The enum T declares two different types: int and char *. The enumerators of T hold values of one of the declared types. 
+% The enum T declares two different types: int and char *. The enumerators of T hold values of one of the declared types.
 
 \subsection{Enumeration Inheritance}
@@ -602,5 +654,5 @@
 enum /* inferred */ Name2 { inline Name, Sue = "Sue", Tom = "Tom" };
 \end{lstlisting}
-\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. 
+\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{lstlisting}[label=lst:EnumInline]
 Name Fred;
@@ -610,5 +662,5 @@
 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. 
+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{lstlisting}[label=lst:EnumInline]
 enum /* inferred */ Name2 { inline Name, Sue = "Sue", Tom = "Tom" };
@@ -625,8 +677,8 @@
 \begin{lstlisting}[label=lst:static_attr]
 enum( char * ) Colour {
-    Red = "red", Blue = "blue", Green = "green"  
-};
-\end{lstlisting}
-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. 
+	Red = "red", Blue = "blue", Green = "green"
+};
+\end{lstlisting}
+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.
 
 \subsection{Runtime Attribute Expression and Weak Referenced Data}
@@ -638,5 +690,5 @@
 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. 
+\CFA stores the variables and labels in @const@ arrays to provide runtime lookup for enumeration information.
 
 \begin{lstlisting}[label=lst:attr_array]
@@ -651,5 +703,5 @@
 \end{lstlisting}
 
-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. 
+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.
 
 \subsection{Enum Prelude}
@@ -657,7 +709,7 @@
 \begin{lstlisting}[label=lst:enum_func_dec]
 forall( T ) {
-    unsigned position( unsigned );
-    T value( unsigned );
-    char * label( unsigned );
+	unsigned position( unsigned );
+	T value( unsigned );
+	char * label( unsigned );
 }
 \end{lstlisting}
@@ -670,6 +722,6 @@
 forall(T)
 class EnumDecl {
-    T* values;
-    char** label;
+	T* values;
+	char** label;
 };
 \end{lstlisting}
@@ -679,6 +731,6 @@
 \begin{lstlisting}[label=lst:EnumInstType]
 class EnumInstType {
-    EnumDecl enumDecl;
-    int position;
+	EnumDecl enumDecl;
+	int position;
 };
 \end{lstlisting}
@@ -700,5 +752,5 @@
 % struct Companion {
 % 	const T * const values;
-%         const char * label;
+%		 const char * label;
 % 	int length;
 % };
@@ -706,5 +758,5 @@
 % \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).  
+% The companion object is singleton across the compilation (investigation).
 
 % \CFA generates the definition of companion functions.
@@ -727,9 +779,9 @@
 \begin{lstlisting}[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 &);
-    }
+	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{lstlisting}
@@ -743,5 +795,5 @@
 \begin{lstlisting}
 enum(int) Weekday {
-    Monday=10, Tuesday, ...
+	Monday=10, Tuesday, ...
 };
 
@@ -758,8 +810,8 @@
 \subsection{User Define Enumeration Functions}
 
-Companion objects make extending features for \CFA enumeration easy. 
+Companion objects make extending features for \CFA enumeration easy.
 \begin{lstlisting}[label=lst:companion_user_definition]
-char * charastic_string( Companion o, int position ) { 
-	return sprintf( "Label: %s; Value: %s", label( o, position ), value( o, position) ); 
+char * charastic_string( Companion o, int position ) {
+	return sprintf( "Label: %s; Value: %s", label( o, position ), value( o, position) );
 }
 printf( charactic_string ( Color, 1 ) );
@@ -776,8 +828,8 @@
 Similarly, the user can work with the enumeration type itself: (see section ref...)
 \begin{lstlisting}[ label=lst:companion_user_definition]
-void print_enumerators ( Companion o ) { 
+void print_enumerators ( Companion o ) {
 	for ( c : Companion o ) {
 		sout | label (c) | value( c ) ;
-	} 
+	}
 }
 print_enumerators( Colour );
@@ -795,5 +847,5 @@
 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) 
+Otherwise, it attempts to initialize enumerators with the enumeration initialization pattern. (a reference to a future initialization pattern section)
 
 \begin{lstlisting}[label=lst:init]
@@ -803,6 +855,6 @@
 T ?+?( T & lhs, T & rhs ) { ... };
 
-enum (T) Sample { 
-	Zero: 0 /* zero_t */, 
+enum (T) Sample {
+	Zero: 0 /* zero_t */,
 	One: Zero + 1 /* ?+?( Zero, one_t ) */ , ...
 };
@@ -826,5 +878,5 @@
 \subsection{Qualified Expression}
 
-\CFA uses qualified expression to address the scoping of \CFA-enumeration. 
+\CFA uses qualified expression to address the scoping of \CFA-enumeration.
 \begin{lstlisting}[label=lst:qualified_expression]
 aggregation_name.field;
@@ -837,4 +889,5 @@
 
 \subsection{\lstinline{with} Clause/Statement}
+
 Instead of qualifying an enumeration expression every time, the @with@ can be used to expose enumerators to the current scope, making them directly accessible.
 \begin{lstlisting}[label=lst:declaration]
@@ -842,6 +895,6 @@
 enum Animal( int ) { Cat=10, Dog=20 };
 with ( Color, Animal ) {
-    char * red_string = Red; // value( Color.Red )
-    int cat = Cat; // value( Animal.Cat )
+	char * red_string = Red; // value( Color.Red )
+	int cat = Cat; // value( Animal.Cat )
 }
 \end{lstlisting}
@@ -851,5 +904,5 @@
 enum RGB( int ) { Red=0, Green=1, Blue=2 };
 with ( Color, RGB ) {
-    // int red = Red; 
+	// int red = Red;
 }
 \end{lstlisting}
@@ -864,4 +917,6 @@
 
 The declaration \CFA-enumeration variable has the same syntax as the C-enumeration. Internally, such a variable will be represented as an EnumInstType.
+
+\section{Related Work}
 
 
