Index: doc/proposals/enum.tex
===================================================================
--- doc/proposals/enum.tex	(revision 739495a2dfb9ddf9e1f5cab76d8451ea64d277b3)
+++ doc/proposals/enum.tex	(revision 367725d425be6bcb501fa6d005c7cb8e01598898)
@@ -245,21 +245,5 @@
 
 
-\subsection{Aggressive Inline}
-To avoid allocating memory for enumeration data structures, \CFA inline the result of enumeration attribute pseudo-function whenever it is possible. 
-\begin{lstlisting}[label=lst:enumeration_inline]
-enum(int) OddNumber { A=1, B=3 };
-sout | "A: " | OddNumber.A | "B: " | OddNumber.B | "A+B: " | OddNumber.A + OddNumber.B
-\end{lstlisting}
-Instead of calling pseudo-function @value@ on expression $OddNumber.A$ and $OddNumber.B$, because the result is known statistically, \CFA will inline the constant expression 1 and 3, respectively. Because no runtime lookup for enumeration value is necessary, \CFA will not generate data structure for enumeration OddNumber.
-
-\subsection{Weak Reference}
-\begin{lstlisting}[label=lst:week_ref]
-enum(int) OddNumber { A=1, B=3 };
-enum OddNumber i = ...;
-...
-sout | OddNumber;
-\end{lstlisting}
-In this example, \CFA cannot determine the static value of the enum variable i, and Runtime lookup is necessary. The OddNumber can be referenced in multiple compilations, and allocating the arrays in all compilation units is not desirable. \CFA addresses this by declaring the value array as a weak reference. All compilation units reference OddNumber have weak references to the same enumeration data structure. No extra memory is allocated if more compilation units reference OddNumber, and the OddNumber is initialized once.
-
+\
 \section{Unification}
 
@@ -638,5 +622,48 @@
 \section{Implementation}
 
-\subsection{Compiler Representation (Reworking)}
+\subsection{Static Attribute Expression}
+\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. 
+
+\subsection{Runtime Attribute Expression and Weak Referenced Data}
+\begin{lstlisting}[label=lst:dynamic_attr]
+Colour c;
+...
+value( c ); // or c
+\end{lstlisting}
+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{lstlisting}[label=lst:attr_array]
+const char * Colour_labels [3] = { "Red", "Blue", "Green" };
+const char * Colour_values [3] = { "red", "blue", "green" };
+\end{lstlisting}
+The \CFA compiles transforms the attribute expressions into array access.
+\begin{lstlisting}[label=lst:attr_array_access]
+position( c ) // c; an integer
+value( c ); // Colour_values[c]
+label( c ); // Colour_labels[c]
+\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. 
+
+\subsection{Enum Prelude}
+
+\begin{lstlisting}[label=lst:enum_func_dec]
+forall( T ) {
+    unsigned position( unsigned );
+    T value( unsigned );
+    char * label( unsigned );
+}
+\end{lstlisting}
+\CFA loads the declaration of enumeration function from the enum.hfa.
+
+\subsection{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{lstlisting}[label=lst:EnumDecl]
@@ -667,32 +694,32 @@
 
 
-\subsection{(Rework) Companion Object and Companion Function}
-
-\begin{lstlisting}[caption={Enum Type Functions}, label=lst:cforall_enum_functions]
-forall( T )
-struct Companion {
-	const T * const values;
-        const char * label;
-	int length;
-};
-\end{lstlisting}
-\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{lstlisting}[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{lstlisting}
-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{lstlisting}[label=lst:companion_definition_values_labels]
-Colour.values; // read the Companion's values
-values( Colour ); // same as Colour.values
-\end{lstlisting}
+% \subsection{(Rework) Companion Object and Companion Function}
+
+% \begin{lstlisting}[caption={Enum Type Functions}, label=lst:cforall_enum_functions]
+% forall( T )
+% struct Companion {
+% 	const T * const values;
+%         const char * label;
+% 	int length;
+% };
+% \end{lstlisting}
+% \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{lstlisting}[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{lstlisting}
+% 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{lstlisting}[label=lst:companion_definition_values_labels]
+% Colour.values; // read the Companion's values
+% values( Colour ); // same as Colour.values
+% \end{lstlisting}
 
 \subsection{Companion Traits (experimental)}