Index: doc/theses/jiada_liang_MMath/implementation.tex
===================================================================
--- doc/theses/jiada_liang_MMath/implementation.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
+++ doc/theses/jiada_liang_MMath/implementation.tex	(revision 956299bfb54cdd0289b10d4a75fecc95d3dea2c8)
@@ -0,0 +1,646 @@
+\chapter{Enumeration Implementation}
+
+
+\section{Enumeration Variable}
+
+Although \CFA enumeration captures three different attributes, an enumeration instance does not store all this information.
+The @sizeof@ a \CFA enumeration instance is always 4 bytes, the same size as a C enumeration instance (@sizeof( int )@).
+It comes from the fact that:
+\begin{enumerate}
+\item
+a \CFA enumeration is always statically typed;
+\item
+it is always resolved as one of its attributes regarding real usage.
+\end{enumerate}
+When creating an enumeration instance @colour@ and assigning it with the enumerator @Color.Green@, the compiler allocates an integer variable and stores the position 1.
+The invocations of $positions()$, $value()$, and $label()$ turn into calls to special functions defined in the prelude:
+\begin{cfa}
+position( green );
+>>> position( Colour, 1 ) -> int
+value( green );
+>>> value( Colour, 1 ) -> T
+label( green );
+>>> label( Colour, 1) -> char *
+\end{cfa}
+@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.
+
+
+\section{Enumeration Data}
+
+\begin{cfa}
+enum(T) E { ... };
+// backing data
+T * E_values;
+char ** E_labels;
+\end{cfa}
+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.
+\end{itemize}
+
+
+\section{Unification}
+
+\section{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.
+\begin{cfa}
+char * green_value = Colour.Green; // "G"
+// Is equivalent to
+// char * green_value = value( Color.Green ); "G"
+\end{cfa}
+
+
+\section{Unification Distance}
+
+\begin{cfa}
+T_2 Foo(T1);
+\end{cfa}
+The @Foo@ function expects a parameter with type @T1@. In C, only a value with the exact type T1 can be used as a parameter for @Foo@. In \CFA, @Foo@ accepts value with some type @T3@ as long as @distance(T1, T3)@ is not @Infinite@.
+
+@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.
+\end{itemize}
+
+For example, @path(int, int)==Zero@, @path(int, char)==Safe@, @path(int, double)==Unsafe@, @path(int, struct S)@ is @Infinite@ for @struct S{}@.
+@distance(A, C)@ is the minimum sum of paths from A to C. For example, if @path(A, B)==i@, @path(B, C)==j@, and @path(A, C)=k@, then $$distance(A,C)==min(path(A,B), path(B,C))==i+j$$.
+
+(Skip over the distance matrix here because it is mostly irrelevant for enumeration discussion. In the actual implementation, distance( E, T ) is 1.)
+
+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.
+\end{itemize}
+
+For @enum(T) E@, @path(T, E)==Safe@ and @path(E,T)==Infinite@. In other words, enumeration type E can be @safely@ used as type T, but type T cannot be used when the resolution context expects a variable with enumeration type @E@.
+
+
+\section{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{cfa}
+char * green = "Green";
+Colour green = Colour.Green; // "G"
+
+void bar(char * s) { return s; }
+void foo(Colour c) { return value( c ); }
+
+foo( green ); // "G"
+bar( green ); // "Green"
+\end{cfa}
+\CFA's conversion distance helps disambiguation in this overloading. For the function @bar@ which expects the parameter s to have type @char *@, $distance(char *,char *) == Zero$ while $distance(char *, Colour) == Safe$, the path from @char *@ to the enumeration with based type @char *@, \CFA chooses the @green@ with type @char *@ unambiguously. On the other hand, for the function @foo@, @distance(Colour, char *)@ is @Infinite@, @foo@ picks the @green@ with type @char *@.
+
+\section{Function Overloading}
+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{cfa}
+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
+foo( green ); // "It is an enum"
+\end{cfa}
+Because @distance(Colour, Colour)@ is @Zero@ and @distance(char *, Colour)@ is @Safe@, \CFA determines the @foo( green )@ is a call to the first foo.
+
+\section{Attributes Functions}
+The pseudo-function @value()@ "unboxes" the enumeration and the type of the expression is the underlying type. Therefore, in the section~\ref{section:enumeration_as_value} when assigning @Colour.Green@ to variable typed @char *@, the resolution distance is @Safe@, while assigning @value(Color.Green) to @char *) has resolution distance @Zero@.
+
+\begin{cfa}
+int s1;
+\end{cfa}
+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, concerning the @Unification@ rule
+
+% \section{Unification and Resolution (this implementation will probably not be used, safe as reference for now)}
+
+% \begin{cfa}
+% enum Colour( char * ) { Red = "R", Green = "G", Blue = "B"  };
+% \end{cfa}
+% 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.
+
+% \begin{cfa}[caption={Null Context}, label=lst:null_context]
+% {
+% 	Colour.Green;
+% }
+% \end{cfa}
+% In example~\ref{lst:null_context}, the environment gives no information to help with the resolution of @Colour.Green@.
+% In this case, any of the attributes is resolvable.
+% According to the \textit{precedence rule}, the expression with @EnumInstType@ resolves as @value( Colour.Green )@.
+% The @EnumInstType@ is converted to the type of the value, which is statically known to the compiler as @char *@.
+% When the compilation reaches the code generation, the compiler outputs code for type @char *@ with the value @"G"@.
+% \begin{cfa}[caption={Null Context Generated Code}, label=lst:null_context]
+% {
+% 	"G";
+% }
+% \end{cfa}
+% \begin{cfa}[caption={int Context}, label=lst:int_context]
+% {
+% 	int g = Colour.Green;
+% }
+% \end{cfa}
+% The assignment expression gives a context for the EnumInstType resolution.
+% The EnumInstType is used as an @int@, and \CFA needs to determine which of the attributes can be resolved as an @int@ type.
+% The functions $Unify( T1, T2 ): bool$ take two types as parameters and determine if one type can be used as another.
+% In example~\ref{lst:int_context}, the compiler is trying to unify @int@ and @EnumInstType@ of @Colour@.
+% $$Unification( int, EnumInstType<Colour> )$$ which turns into three Unification call
+% \begin{cfa}[label=lst:attr_resolution_1]
+% {
+% 	Unify( int, char * ); // unify with the type of value
+% 	Unify( int, int ); // unify with the type of position
+% 	Unify( int, char * ); // unify with the type of label
+% }
+% \end{cfa}
+% \begin{cfa}[label=lst:attr_resolution_precedence]
+% {
+% 	Unification( T1, EnumInstType<T2> ) {
+% 		if ( Unify( T1, T2 ) ) return T2;
+% 		if ( Unify( T1, int ) ) return int;
+% 		if ( Unify( T1, char * ) ) return char *;
+% 		Error: Cannot Unify T1 with EnumInstType<T2>;
+% 	}
+% }
+% \end{cfa}
+% After the unification, @EnumInstType@ is replaced by its attributes.
+
+% \begin{cfa}[caption={Unification Functions}, label=lst:unification_func_call]
+% {
+% 	T2 foo ( T1 ); // function take variable with T1 as a parameter
+% 	foo( EnumInstType<T3> ); // Call foo with a variable has type EnumInstType<T3>
+% 	>>>> Unification( T1, EnumInstType<T3> )
+% }
+% \end{cfa}
+% % The conversion can work backward: in restrictive cases, attributes of can be implicitly converted back to the EnumInstType.
+% Backward conversion:
+% \begin{cfa}[caption={Unification Functions}, label=lst:unification_func_call]
+% {
+% 	enum Colour colour = 1;
+% }
+% \end{cfa}
+
+% \begin{cfa}[caption={Unification Functions}, label=lst:unification_func_call]
+% {
+%	Unification( EnumInstType<Colour>, int ) >>> label
+% }
+% \end{cfa}
+% @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
+% \begin{cfa}
+% {
+%	enum Colour colour = Colour.Green;
+% }
+% \end{cfa}
+% Steps:
+% \begin{enumerate}
+% \item
+% identify @1@ as a constant expression with type @int@, and the value is statically known as @1@
+% \item
+% @unification( EnumInstType<Colour>, int )@: @position( EnumInstType< Colour > )@
+% \item
+% return the enumeration constant at position 1
+% \end{enumerate}
+% \begin{cfa}
+% {
+% 	enum T (int) { ... } // Declaration
+% 	enum T t = 1;
+% }
+% \end{cfa}
+% Steps:
+% \begin{enumerate}
+% \item
+% identify @1@ as a constant expression with type @int@, and the value is statically known as @1@
+% \item
+% @unification( EnumInstType<Colour>, int )@: @value( EnumInstType< Colour > )@
+% \item
+% 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
+
+% \section{Casting}
+% Casting an EnumInstType to some other type T works similarly to unify the EnumInstType with T. For example:
+% \begin{cfa}
+% enum( int ) Foo { A = 10, B = 100, C = 1000 };
+% (int) Foo.A;
+% \end{cfa}
+% 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.
+
+% \section{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{cfa}
+% Foo a; // int a;
+% int j = a;
+% char * s = a;
+% \end{cfa}
+% 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{cfa}
+% int j = value( Foo, a )
+% \end{cfa}
+% Similarly, the generated code for the third line is
+% \begin{cfa}
+% char * j = label( Foo, a )
+% \end{cfa}
+
+
+\section{Enumerator Initialization}
+An enumerator must have a deterministic immutable value, either be explicitly initialized in the enumeration definition, or implicitly initialized by rules.
+
+\section{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$.
+
+\section{Auto Initializable}
+\label{s:AutoInitializable}
+
+
+\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.
+
+Specifically, a type is auto-initializable only if it satisfies the trait @AutoInitializable@:
+\begin{cfa}
+forall(T)
+trait AutoInitializable {
+	void ?()( T & t, zero_t );
+	S ?++( T & t);
+};
+\end{cfa}
+An example of a user-defined @AutoInitializable@ is:
+\begin{cfa}[label=lst:sample_auto_Initializable]
+struct Odd { int i; };
+void ?()( Odd & t, zero_t ) { t.i = 1; };
+Odd ?++( Odd t1 ) { return Odd( t1.i + 2); };
+\end{cfa}
+When the type of an enumeration is @AutoInitializable@, implicit initialization is available.
+\begin{cfa}[label=lst:sample_auto_Initializable_usage]
+enum AutoInitUsage(Odd) {
+	A, B, C = 7, D
+};
+\end{cfa}
+In the example, no initializer is specified for the first enumeration constant @A@, so \CFA initializes it with the value of @zero_t@, which is 1.
+@B@ and @D@ have the values of their $predecessor++$, where @one_t@ has the value 2.
+Therefore, the enumeration is initialized as follows:
+\begin{cfa}[label=lst:sample_auto_Initializable_usage_gen]
+enum AutoInitUsage(Odd) {
+	A = 1, B = 3, C = 7, D = 9
+};
+\end{cfa}
+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@.
+\begin{cfa}[label=lst:letter]
+enum Alphabet( int ) {
+	A = 'A', B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z,
+	a = 'a', b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z
+};
+print( "%c, %c, %c", Alphabet.F, Alphabet.o, Alphabet.z );
+>>> F, o, z
+\end{cfa}
+\section{Enumeration Features}
+\section{Iteration and Range}
+
+It is convenient to iterate over a \CFA enumeration value, e.g.:
+\begin{cfa}[label=lst:range_functions]
+for ( Alphabet alph; Alphabet ) { sout | alph; }
+>>> A B C ... D
+\end{cfa}
+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.
+
+\textbullet\ \CFA offers a shorthand for iterating all enumeration constants:
+\begin{cfa}[label=lst:range_functions]
+for ( Alphabet alph ) { sout | alph; }
+>>> A B C ... D
+\end{cfa}
+
+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{cfa}[label=lst:range_function_1]
+for ( alph; Alphabet.D ) { sout | alph; }
+>>> A B C
+\end{cfa}
+
+\textbullet\ ~= H is implicit up-to inclusive range [0,H].
+\begin{cfa}[label=lst:range_function_2]
+for ( alph; ~= Alphabet.D ) { sout | alph; }
+>>> A B C D
+\end{cfa}
+
+\textbullet\ L ~ H is explicit up-to exclusive range [L,H).
+\begin{cfa}[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{cfa}
+
+\textbullet\ L ~= H is explicit up-to inclusive range [L,H].
+\begin{cfa}[label=lst:range_function_4]
+for ( alph; Alphabet.B ~= Alphabet.D  ) { sout | alph; }
+>>> B C D
+\end{cfa}
+
+\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{cfa}[label=lst:range_function_5]
+for ( alph; Alphabet.D -~ Alphabet.B  ) { sout | alph; }
+>>> D C
+\end{cfa}
+
+\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{cfa}[label=lst:range_function_6]
+for ( alph; Alphabet.D -~= Alphabet.B  ) { sout | alph; }
+>>> D C B
+\end{cfa}
+
+A user can specify the ``step size'' of an iteration. There are two different stepping schemes of enumeration for-loop.
+\begin{cfa}[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{cfa}
+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{cfa}[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{cfa}
+
+% \PAB{Explain what each loop does.}
+
+It is also possible to iterate over an enumeration's labels, implicitly or explicitly:
+\begin{cfa}[label=lst:range_functions_label_implicit]
+for ( char * alph; Alphabet )
+\end{cfa}
+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{cfa}[label=lst:range_functions_label_implicit]
+for ( char * ch; labels( Alphabet ) )
+\end{cfa}
+
+
+% \section{Non-uniform Type}
+% TODO: Working in Progress, might need to change other sections. Conflict with the resolution right now.
+
+% \begin{cfa}
+% enum T( int, char * ) {
+%	 a=42, b="Hello World"
+% };
+% \end{cfa}
+% The enum T declares two different types: int and char *. The enumerators of T hold values of one of the declared types.
+
+\section{Enumeration Inheritance}
+
+\begin{cfa}[label=lst:EnumInline]
+enum( char * ) Name { Jack = "Jack", Jill = "Jill" };
+enum /* inferred */ Name2 { inline Name, Sue = "Sue", Tom = "Tom" };
+\end{cfa}
+\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{cfa}[label=lst:EnumInline]
+Name Fred;
+void f( Name2 );
+f( Fred );
+\end{cfa}
+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{cfa}[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{cfa}
+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{cfa}[label=lst:EnumInline]
+with( Name, Name2 ) { Jack; } // Name.Jack and Name2.Jack are equivalent. No ambiguity
+\end{cfa}
+
+\section{Implementation}
+
+\section{Static Attribute Expression}
+\begin{cfa}[label=lst:static_attr]
+enum( char * ) Colour {
+	Red = "red", Blue = "blue", Green = "green"
+};
+\end{cfa}
+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.
+
+\section{Runtime Attribute Expression and Weak Referenced Data}
+\begin{cfa}[label=lst:dynamic_attr]
+Colour c;
+...
+value( c ); // or c
+\end{cfa}
+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{cfa}[label=lst:attr_array]
+const char * Colour_labels [3] = { "Red", "Blue", "Green" };
+const char * Colour_values [3] = { "red", "blue", "green" };
+\end{cfa}
+The \CFA compiles transforms the attribute expressions into array access.
+\begin{cfa}[label=lst:attr_array_access]
+position( c ) // c; an integer
+value( c ); // Colour_values[c]
+label( c ); // Colour_labels[c]
+\end{cfa}
+
+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.
+
+\section{Enum Prelude}
+
+\begin{cfa}[label=lst:enum_func_dec]
+forall( T ) {
+	unsigned position( unsigned );
+	T value( unsigned );
+	char * label( unsigned );
+}
+\end{cfa}
+\CFA loads the declaration of enumeration function from the enum.hfa.
+
+\section{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{cfa}[label=lst:EnumDecl]
+forall(T)
+class EnumDecl {
+	T* values;
+	char** label;
+};
+\end{cfa}
+
+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{cfa}[label=lst:EnumInstType]
+class EnumInstType {
+	EnumDecl enumDecl;
+	int position;
+};
+\end{cfa}
+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>@.
+
+\begin{cfa}[caption={Enum Type Functions}, label=lst:cforall_enum_data]
+const T * const values;
+const char * label;
+int length;
+\end{cfa}
+Companion data are necessary information to represent an enumeration. They are stored as standalone pieces, rather than a structure. Those data will be loaded "on demand".
+Companion data are needed only if the according pseudo-functions are called. For example, the value of the enumeration Workday is loaded only if there is at least one compilation that has call $value(Workday)$. Once the values are loaded, all compilations share these values array to reduce memory usage.
+
+
+% \section{(Rework) Companion Object and Companion Function}
+
+% \begin{cfa}[caption={Enum Type Functions}, label=lst:cforall_enum_functions]
+% forall( T )
+% struct Companion {
+% 	const T * const values;
+%		 const char * label;
+% 	int length;
+% };
+% \end{cfa}
+% \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{cfa}[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{cfa}
+% 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{cfa}[label=lst:companion_definition_values_labels]
+% Colour.values; // read the Companion's values
+% values( Colour ); // same as Colour.values
+% \end{cfa}
+
+\section{Companion Traits (experimental)}
+Not sure its semantics yet, and it might replace a companion object.
+\begin{cfa}[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 &);
+	}
+}
+\end{cfa}
+All enumerations implicitly implement the Companion trait, an interface to access attributes. The Companion can be a data type because it fulfills to requirements to have concrete instances, which are:
+
+\begin{enumerate}
+  \item The instance of enumeration has a single polymorphic type.
+  \item Each assertion should use the type once as a parameter.
+\end{enumerate}
+
+\begin{cfa}
+enum(int) Weekday {
+	Monday=10, Tuesday, ...
+};
+
+T value( enum Weekday<T> & this);
+int position( enum Weekday<T> & this )
+char * label( enum Weekday<T> & this )
+
+trait Companion obj = (enum(int)) Workday.Weekday;
+value(obj); // 10
+\end{cfa}
+The enumeration comes with default implementation to the Companion traits functions. The usage of Companion functions would make \CFA allocates and initializes the necessary companion arrays, and return the data at the position represented by the enumeration.
+(...)
+
+\section{User Define Enumeration Functions}
+
+Companion objects make extending features for \CFA enumeration easy.
+\begin{cfa}[label=lst:companion_user_definition]
+char * charastic_string( Companion o, int position ) {
+	return sprintf( "Label: %s; Value: %s", label( o, position ), value( o, position) );
+}
+printf( charactic_string ( Color, 1 ) );
+>>> Label: Green; Value: G
+\end{cfa}
+Defining a function takes a Companion object effectively defines functions for all \CFA enumeration.
+
+The \CFA compiler turns a function call that takes an enumeration instance as a parameter into a function call with a companion object plus a position.
+Therefore, a user can use the syntax with a user-defined enumeration function call:
+\begin{cfa}[label=lst:companion_user_definition]
+charactic_string( Color.Green ); // equivalent to charactic_string( Color, 1 )
+>>> Label: Green; Value: G
+\end{cfa}
+Similarly, the user can work with the enumeration type itself: (see section ref...)
+\begin{cfa}[ label=lst:companion_user_definition]
+void print_enumerators ( Companion o ) {
+	for ( c : Companion o ) {
+		sout | label (c) | value( c ) ;
+	}
+}
+print_enumerators( Colour );
+\end{cfa}
+
+
+\section{Declaration}
+
+The qualified enumeration syntax is dedicated to \CFA enumeration.
+\begin{cfa}[label=lst:range_functions]
+enum (type_declaration) name { enumerator = const_expr, enumerator = const_expr, ... }
+\end{cfa}
+A compiler stores the name, the underlying type, and all enumerators in an @enumeration table@.
+During the $Validation$ pass, the compiler links the type declaration to the type's definition.
+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)
+
+\begin{cfa}[label=lst:init]
+struct T { ... };
+void ?{}( T & t, zero_t ) { ... };
+void ?{}( T & t, one_t ) { ... };
+T ?+?( T & lhs, T & rhs ) { ... };
+
+enum (T) Sample {
+	Zero: 0 /* zero_t */,
+	One: Zero + 1 /* ?+?( Zero, one_t ) */ , ...
+};
+\end{cfa}
+Challenge: \\
+The value of an enumerator, or the initializer, requires @const_expr@.
+While previously getting around the issue by pushing it to the C compiler, it might not work anymore because of the user-defined types, user-defined @zero_t@, @one_t@, and addition operation.
+Might not be able to implement a \emph{correct} static check.
+
+\CFA $autogens$ a Companion object for the declared enumeration.
+\begin{cfa}[label=lst:companion]
+Companion( T ) Sample {
+	.values: { 0, 0+1, 0+1+1, 0+1+1+1, ... }, /* 0: zero_t, 1: one_t, +: ?+?{} */
+	.labels: { "Zero", "One", "Two", "Three", ...},
+	.length: /* number of enumerators */
+};
+\end{cfa}
+\CFA stores values as intermediate expressions because the result of the function call to the function @?+?{}(T&, T&)@ is statically unknown to \CFA.
+But the result is computed at run time, and the compiler ensures the @values@ are not changed.
+
+\section{Qualified Expression}
+
+\CFA uses qualified expression to address the scoping of \CFA-enumeration.
+\begin{cfa}[label=lst:qualified_expression]
+aggregation_name.field;
+\end{cfa}
+The qualified expression is not dedicated to \CFA enumeration.
+It is a feature that is supported by other aggregation in \CFA as well, including a C enumeration.
+When C enumerations are unscoped, the qualified expression syntax still helps to disambiguate names in the context.
+\CFA recognizes if the expression references a \CFA aggregation by searching the presence of @aggregation_name@ in the \CFA enumeration table.
+If the @aggregation_name@ is identified as a \CFA enumeration, the compiler checks if @field@ presents in the declared \CFA enumeration.
+
+\section{Instance Declaration}
+
+
+\begin{cfa}[label=lst:var_declaration]
+enum Sample s1;
+\end{cfa}
+
+The declaration \CFA-enumeration variable has the same syntax as the C-enumeration. Internally, such a variable will be represented as an EnumInstType.
