Index: doc/proposals/enum.tex
===================================================================
--- doc/proposals/enum.tex	(revision 66d92e3cc3e75781be55e344dbdf9ca4e58f9872)
+++ doc/proposals/enum.tex	(revision 2d373440faae9908ed04cd99e5f056ec1bf18937)
@@ -289,38 +289,42 @@
 \end{lstlisting}
 
-\subsection{Runtime Enumeration}
-
-The companion structure definition is visible to users, and users can create an instance of companion object themselves, which effectively constructs a \textit{Runtime Enumeration}.
-\begin{lstlisting}[ label=lst:runtime_enum ]
-const char values[$\,$] = { "Hello", "World" };
-const char labels[$\,$] = { "First", "Second" };
-Companion(char *) MyEnum = { .values: values, .labels: labels, .length: 2 };
-\end{lstlisting}
-A runtime enumeration can be used to call enumeration functions.
-\begin{lstlisting}[ label=lst:runtime_enum_usage ]
-sout | charatstic_string( MyEnum, 1 );
->>> Label: Second; Value: World
-\end{lstlisting}
-However, a runtime enumeration cannot create an enumeration instance, and it does not support enum-qualified syntax.
-\begin{lstlisting}[ label=lst:runtime_enum_usage ]
-MyEnum e = MyEnum.First; // Does not work: cannot create an enumeration instance e, 
-			            // and MyEnum.First is not recognizable
-\end{lstlisting}
-During the compilation, \CFA adds enumeration declarations to an enumeration symbol table and creates specialized function definitions for \CFA enumeration.
-\CFA does not recognize runtime enumeration during compilation and would not add them to the enumeration symbol table, resulting in a lack of supports for runtime enumeration.
-
-\PAB{Not sure how useful this feature is.}
-
-\section{Enumeration Features}
+% \subsection{Runtime Enumeration}
+
+% The companion structure definition is visible to users, and users can create an instance of companion object themselves, which effectively constructs a \textit{Runtime Enumeration}.
+% \begin{lstlisting}[ label=lst:runtime_enum ]
+% const char values[$\,$] = { "Hello", "World" };
+% const char labels[$\,$] = { "First", "Second" };
+% Companion(char *) MyEnum = { .values: values, .labels: labels, .length: 2 };
+% \end{lstlisting}
+% A runtime enumeration can be used to call enumeration functions.
+% \begin{lstlisting}[ label=lst:runtime_enum_usage ]
+% sout | charatstic_string( MyEnum, 1 );
+% >>> Label: Second; Value: World
+% \end{lstlisting}
+% However, a runtime enumeration cannot create an enumeration instance, and it does not support enum-qualified syntax.
+% \begin{lstlisting}[ label=lst:runtime_enum_usage ]
+% MyEnum e = MyEnum.First; // Does not work: cannot create an enumeration instance e, 
+% 			            // and MyEnum.First is not recognizable
+% \end{lstlisting}
+% During the compilation, \CFA adds enumeration declarations to an enumeration symbol table and creates specialized function definitions for \CFA enumeration.
+% \CFA does not recognize runtime enumeration during compilation and would not add them to the enumeration symbol table, resulting in a lack of supports for runtime enumeration.
+
+% \PAB{Not sure how useful this feature is.}
+
+% \section{Enumeration Features}
 
 A trait is a collection of constraints in \CFA that can be used to describe types.
 The \CFA standard library defines traits to categorize types with related enumeration features.
 
+\section{Enumerator Initialization}
+An enumerator must have a deterministic immutable value, either be explicitly initialized in the enumeration definition, or implicitly initialized by rules.
+
+\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$. 
+
 \subsection{Auto Initializable}
 \label{s:AutoInitializable}
 
-TODO: make the initialization rule a separate section. 
-
-If no explicit initializer is given to an enumeration constant, C initializes the first enumeration constant with value 0, and the next enumeration constant has a value equal to its $predecessor + 1$.
+
 \CFA enumerations have the same rule in enumeration constant initialization.
 However, only \CFA types that have defined traits for @zero_t@, @one_t@, and an addition operator can be automatically initialized by \CFA.
@@ -356,5 +360,5 @@
 };
 \end{lstlisting}
-Note, there is no mechanism to prevent an even value for the direct initialization, such as @C = 6@.
+Note that there is no mechanism to prevent an even value for the direct initialization, such as @C = 6@.
 
 In \CFA, character, integral, float, and imaginary types are all @AutoInitialiable@.
@@ -367,50 +371,75 @@
 >>> F, o, z
 \end{lstlisting}
-
+\section{Enumeration Features}
 \subsection{Iteration and Range}
 
-It is convenient to iterate over a \CFA enumeration, e.g.:
+It is convenient to iterate over a \CFA enumeration value, e.g.:
 \begin{lstlisting}[label=lst:range_functions]
-for ( Alphabet alph; Alphabet ) {
-	printf( "%d ", alph );
-}
->>> A B C ...
+for ( Alphabet alph; Alphabet ) { sout | alph; }
+>>> A B C ... D
 \end{lstlisting}
 The for-loop uses the enumeration type @Alphabet@ its range, and iterates through all enumerators in the order defined in the enumeration.
 @alph@ is the iterating enumeration object, which returns the value of an @Alphabet@ in this context according to the precedence rule.
 
-\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 ) {
-	printf( "%d ", alph );
-}
->>> A B C ...
-\end{lstlisting}
-The following different loop-control syntax is supported:
-\begin{lstlisting}[label=lst:range_functions]
-for ( Alphabet.D )
-for ( alph; Alphabet.g ~ Alphabet.z )
-for ( Alphabet alph; Alphabet.R ~ Alphabet.X ~ 2 )
-\end{lstlisting}
-\PAB{Explain what each loop does.}
-Notably, the meaning of ``step'' for an iteration has changed for enumeration.
-Consider the following example:
-\begin{lstlisting}[label=lst:range_functions]
-enum(int) Sequence {
-	A = 10, B = 12, C = 14;  
-}
-for ( s; Sequence.A ~ Sequence.C ) {
-	printf( "%d ", s ); 
-}
->>> 10 12 14
-
-for ( s; Sequence.A ~ Sequence.A ~ 2 ) {
-	printf( "%d ", s ); 
-}
->>> 10 14
-\end{lstlisting}
-The range iteration of enumeration does not return the @current_value++@ until it reaches the upper bound.
-The semantics is to return the next enumeration constant.
-If a stepping is specified, 2 for example, it returns the 2 enumeration constant after the current one, rather than the @current+2@.
+for ( Alphabet alph ) { sout | alph; }
+>>> A B C ... D
+\end{lstlisting}
+
+The following are examples for constructing for-control using an enumeration. Note that the type declaration of the iterating variable is optional, because \CFA can infer the type as EnumInstType based on the range expression, and possibly convert it to one of its attribute types.
+
+\textbullet\ H is implicit up-to exclusive range [0, H).
+\begin{lstlisting}[label=lst:range_function_1]
+for ( alph; Alphabet.D ) { sout | alph; }
+>>> A B C
+\end{lstlisting}
+
+\textbullet\ ~= H is implicit up-to inclusive range [0,H].
+\begin{lstlisting}[label=lst:range_function_2]
+for ( alph; ~= Alphabet.D ) { sout | alph; }
+>>> A B C D
+\end{lstlisting}
+
+\textbullet\ L ~ H is explicit up-to exclusive range [L,H).
+\begin{lstlisting}[label=lst:range_function_3]
+for ( alph; Alphabet.B ~ Alphabet.D  ) { sout | alph; }
+// for ( Alphabet alph = Alphabet.B; alph < Alphabet.D; alph += 1  ); 1 is one_t
+>>> B C
+\end{lstlisting}
+
+\textbullet\ L ~= H is explicit up-to inclusive range [L,H].
+\begin{lstlisting}[label=lst:range_function_4]
+for ( alph; Alphabet.B ~= Alphabet.D  ) { sout | alph; }
+>>> B C D
+\end{lstlisting}
+
+\textbullet\ L -~ H is explicit down-to exclusive range [H,L), where L and H are implicitly interchanged to make the range down-to.
+\begin{lstlisting}[label=lst:range_function_5]
+for ( alph; Alphabet.D -~ Alphabet.B  ) { sout | alph; }
+>>> D C
+\end{lstlisting}
+
+\textbullet\ L -~= H is explicit down-to exclusive range [H,L], where L and H are implicitly interchanged to make the range down-to.
+\begin{lstlisting}[label=lst:range_function_6]
+for ( alph; Alphabet.D -~= Alphabet.B  ) { sout | alph; }
+>>> D C B
+\end{lstlisting}
+
+A user can specify the ``step size'' of an iteration. There are two different stepping schemes of enumeration for-loop.
+\begin{lstlisting}[label=lst:range_function_stepping]
+enum(int) Sequence { A = 10, B = 12, C = 14, D = 16, D  = 18 };
+for ( s; Sequence.A ~= Sequence.D ~ 1  ) { sout | alph; }
+>>> 10 12 14 16 18
+for ( s; Sequence.A ~= Sequence.D; s+=1  ) { sout | alph; }
+>>> 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 
+\begin{lstlisting}[label=lst:range_function_stepping_converted]
+for ( typeof( value(Sequence.A) ) s=value( Sequence.A ); s <= Sequence.D; s+=1  ) { sout | alph; }
+>>> 10 11 12 13 14 15 16 17 18
+\end{lstlisting}
+
+% \PAB{Explain what each loop does.}
 
 It is also possible to iterate over an enumeration's labels, implicitly or explicitly:
@@ -424,7 +453,63 @@
 \end{lstlisting}
 
+
+% \subsection{Non-uniform Type}
+% TODO: Working in Progress, might need to change other sections. Conflict with the resolution right now.
+
+% \begin{lstlisting}
+% enum T( int, char * ) {
+%     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. 
+
+\subsection{Enumeration Inheritance}
+
+\begin{lstlisting}[label=lst:EnumInline]
+enum( char * ) Name { Jack = "Jack", Jill = "Jill" };
+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. 
+\begin{lstlisting}[label=lst:EnumInline]
+Name Fred;
+void f( Name2 );
+f( Fred );
+\end{lstlisting}
+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. 
+\begin{lstlisting}[label=lst:EnumInline]
+enum /* inferred */ Name2 { inline Name, Sue = "Sue", Tom = "Tom" };
+// is equivalent to enum Name2 { Jack = "Jack", Jill="Jill", Sue = "Sue", Tom = "Tom" };
+\end{lstlisting}
+Name.Jack is equivalent to Name2.Jack. Their attributes are all identical. Opening both Name and Name2 in the same scope will not introduce ambiguity.
+\begin{lstlisting}[label=lst:EnumInline]
+with( Name, Name2 ) { Jack; } // Name.Jack and Name2.Jack are equivalent. No ambiguity
+\end{lstlisting}
+
 \section{Implementation}
 
-\CFA places the definition of Companion structure and non-parameterized Companion functions in the prelude, visible globally.
+\subsection{Compiler 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]
+forall(T)
+class EnumDecl {
+    T* values;
+    char** label;
+};
+\end{lstlisting}
+
+The internal representation of an enumeration constant is @EnumInstType@.
+An @EnumInstType@ has a reference to the \CFA-enumeration declaration and the position of the enumeration constant.
+\begin{lstlisting}[label=lst:EnumInstType]
+class EnumInstType {
+    EnumDecl enumDecl;
+    int position;
+};
+\end{lstlisting}
+In the later discussion, we will use @EnumDecl<T>@ to symbolize a @EnumDecl@ parameterized by type T, and @EnumInstType<T>@ is a declared instance of @EnumDecl<T>@.
+
+% \subsection{Preluede}
+% \CFA places the definition of Companion structure and non-parameterized Companion functions in the prelude, visible globally.
 
 \subsection{Declaration}
@@ -479,43 +564,39 @@
 If the @aggregation_name@ is identified as a \CFA enumeration, the compiler checks if @field@ presents in the declared \CFA enumeration.
 
-\subsection{\lstinline{with} Statement}
-
-\emph{Work in Progress}
-
+\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]
+enum Color( char * ) { Red="R", Green="G", Blue="B" };
+enum Animal( int ) { Cat=10, Dog=20 };
+with ( Color, Animal ) {
+    char * red_string = Red; // value( Color.Red )
+    int cat = Cat; // value( Animal.Cat )
+}
+\end{lstlisting}
+The \lstinline{with} might introduce ambiguity to a scope. Consider the example:
+\begin{lstlisting}[label=lst:declaration]
+enum Color( char * ) { Red="R", Green="G", Blue="B" };
+enum RGB( int ) { Red=0, Green=1, Blue=2 };
+with ( Color, RGB ) {
+    // int red = Red; 
+}
+\end{lstlisting}
+\CFA will not try to resolve the expression with ambiguity. It would report an error. In this case, it is necessary to qualify @Red@ even inside of the \lstinline{with} clause.
 
 \subsection{Instance Declaration}
 
-\emph{Work in Progress}
-
-\begin{lstlisting}[label=lst:declaration]
+
+\begin{lstlisting}[label=lst:var_declaration]
 enum Sample s1;
-Sample s2;
-\end{lstlisting}
-A declaration of \CFA enumeration instance that has no difference than a C enumeration or other \CFA aggregation.
-The compiler recognizes the type of a variable declaration by searching the name in all possible types.
-The @enum@ keyword is not necessary but helps to disambiguate types (questionable).
-The generated code for a \CFA enumeration declaration is utterly an integer, which is meant to store the position.
-\begin{lstlisting}[label=lst:declaration]
+\end{lstlisting}
+
+The declaration \CFA-enumeration variable has the same syntax as the C-enumeration. Internally, such a variable will be represented as an EnumInstType.
+\begin{lstlisting}[label=lst:declaration_code]
 int s1;
-int s2;
-\end{lstlisting}
-
-\subsection{Compiler Representation}
-
-\emph{Work in Progress}
-
-The internal representation of an enumeration constant is @EnumInstType@.
-The minimum information an @EnumInstType@ stores is a reference to the \CFA-enumeration declaration and the position of the enumeration constant.
-\begin{lstlisting}[label=lst:EnumInstType]
-class EnumInstType {
-	EnumDecl enumDecl;
-	int position;
-};
-\end{lstlisting}
+\end{lstlisting}
+The generated code for an enumeration instance is simply an int. It is to hold the position of an enumeration. And usage of variable @s1@ will be converted to return one of its attributes: label, value, or position, with respect to the @Unification@ rule
 
 \subsection{Unification and Resolution }
 
-\emph{Work in Progress}
 
 \begin{lstlisting}
@@ -604,5 +685,5 @@
 @unification( EnumInstType<Colour>, int )@: @position( EnumInstType< Colour > )@
 \item
-return the enumeration constant at the position 1
+return the enumeration constant at position 1
 \end{enumerate}
 \begin{lstlisting}
@@ -623,4 +704,29 @@
 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}
+Casting an EnumInstType to some other type T works similarly to unify the EnumInstType with T. For example:
+\begin{lstlisting}
+enum( int ) Foo { A = 10, B = 100, C = 1000 };
+(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. 
+
+\subsection{Value Conversion}
+As discussed in section~\ref{lst:var_declaration}, \CFA only saves @position@ as the necessary information. It is necessary for \CFA to generate intermediate code to retrieve other attributes.
+
+\begin{lstlisting}
+Foo a; // int a;
+int j = a;
+char * s = a;
+\end{lstlisting}
+Assume stores a value x, which cannot be statically determined. When assigning a to j in line 2, the compiler @Unify@ j with a, and returns @value( a )@. The generated code for the second line will be
+\begin{lstlisting}
+int j = value( Foo, a )
+\end{lstlisting}
+Similarly, the generated code for the third line is 
+\begin{lstlisting}
+char * j = label( Foo, a )
+\end{lstlisting}
+
 \end{document}