Changeset 38e20a80 for doc/theses/jiada_liang_MMath

Timestamp:

Jul 29, 2024, 1:32:10 PM (5 months ago)

Author:

JiadaL <j82liang@…>

Branches:

master

Children:

ce02877

Parents:

5aeb1a9

Message:

update thesis

Location:

doc/theses/jiada_liang_MMath

Files:

• CFAenum.tex (modified) (9 diffs)
• background.tex (modified) (1 diff)
• implementation.tex (modified) (5 diffs)
• uw-ethesis.tex (modified) (1 diff)

doc/theses/jiada_liang_MMath/CFAenum.tex

@@ -6 +6 @@
 % 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 +20 @@
         $\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 +30 @@
 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 +52 @@
 \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 +61 @@
 
 \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 +75 @@
         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 +112 @@
 
 
-\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 +169 @@
 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 +296 @@
 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.

doc/theses/jiada_liang_MMath/background.tex

@@ -401 +401 @@
 
 \subsection{Conversion Cost}
-In C, functions argument and parameter type does not need to be exact match, and the compiler performs an @implicit conversion@ on argument.
-\begin{cfa}
-void foo(double i);
-foo(42);
-\end{cfa}
-The implicit conversion in C is relatively simple because of the abscence of overloading, with the exception of binary operators, for which the 
-compiler needs to find a common type of both operands and the result. The pattern is known as "usual arithmetic conversions".
-
-\CFA generalizes C implicit conversion to function overloading as a concept of @conversion cost@.
-Initially designed by Bilson, conversion cost is a 3-tuple, @(unsafe, poly, safe)@, where unsafe is the number of narrowing conversion,
-poly is the count of polymorphics type binding, and safe is the sum of the degree of widening conversion. Every 
-basic type in \CFA has been assigned with a @distance to Byte@, or @distance@, and the degree of widening conversion is the difference between two distances.
-
-Aaron extends conversion cost to a 7-tuple, 
-@@(unsafe, poly, safe, sign, vars, specialization, reference)@@. The summary of Aaron's cost model is the following:
+\label{s:ConversionCost}
+In C, function call arguments and function parameters do not need to be a exact match. When types mismatch, C performs an \newterm{implicit conversion} 
+on argument to parameter type. The process is trivial with the exception on binary operators;  When types of operands are different, 
+C nees to decide which operands need implicit conversion. C defines the resolution pattern as "usual arithmetic conversion", 
+in which C looks for a \newterm{common type} between operands, and convert either one or both operands to the common type. 
+Loosely defined, a common type is a the smallest type in terms of size of representation that both operands can be converted into without losing their precision.
+Such conversion is called "widening" or "safe conversion".
+
+C binary operators can be restated as 2-arity functions that overloaded with different parameters. "Usual arithmetic conversion" is to find a overloaded 
+instance that for both arguments, the conversion to parameter type is a widening conversion to the smallest type.
+
+\CFA generalizes "usual arithmetic conversion" to \newterm{conversion cost}. In the first design by Bilson, conversion cost is a 3-tuple,
+@(unsafe, poly, safe)@, where @unsafe@ the number of unsafe (narrorow conversion) from argument to parameter, 
+@poly@ is the number of polymorphic function parameter, 
+and @safe@ is sum of degree of safe (widening) conversion.
+Sum of degree is a method to quantify C's integer and floating-point rank. 
+Every pair of widening conversion types has been assigned with a \newterm{distance}, and distance between the two same type is 0.
+For example, the distance from char to int is 2, distance from integer to long is 1, and distance from int to long long int is 2.
+The distance does not mirror C's rank system. For example, the rank of char and signed char are the same in C, but the distance from char to signed char is assigned with 1.
+@safe@ cost is summing all pair of argument to parameter safe conversion distance.
+Among the three in Bilson's model, @unsafe@ is the most significant cost and @safe@ is the least significant one, with an implication that \CFA always choose 
+a candidate with the lowest @unsafe@ if possible.
+
+Assume the overloaded function @foo@ is called with two @int@ parameter. The cost for every overloaded @foo@ has been list along:
+\begin{cfa}
+void foo(char, char);                           // (2, 0, 0)
+void foo(char, int);                            // (1, 0, 0)
+forall(T, V) void foo(T, V);            // (0, 2, 0)
+forall(T)        void foo(T, T);                // (0, 2, 0)
+forall(T)        void foo(T, int);              // (0, 1, 0)
+void foo(long long, long);                      // (0, 0, 3)
+void foo(long, long);                           // (0, 0, 2)
+void foo(int, long);                            // (0, 0, 1)
+
+int i, j; foo(i, j);
+\end{cfa}
+The overloaded instances are ordered from the highest to the lowest cost, and \CFA select the last candidate.
+
+In the later iteration of \CFA, Schluntz and Aaron expanded conversion cost to a 7-tuple with 4 additional categories, 
+@@(unsafe, poly, safe, sign, vars, specialization, reference)@@.
+with interpretation listed below:
 \begin{itemize}
-\item Unsafe is the number of argument that implicitly convert to a type with high rank.
-\item Poly accounts for number of polymorphics binding in the function declaration.
-\item Safe is sum of distance (add reference/appendix later).
+\item Unsafe
+\item Poly 
+\item Safe
 \item Sign is the number of sign/unsign variable conversion.
-\item Vars is the number of polymorphics type declared in @forall@.
-\item Specialization is opposite number of function declared in @forall@. More function declared implies more constraint on polymorphics type, and therefore has the lower cost.
-\item Reference is number of lvalue-to-rvalue conversion.
+\item Vars is the number of polymorphics type variable.
+\item Specialization is negative value of the number of type assertion.
+\item Reference is number of reference-to-rvalue conversion.
 \end{itemize}
+The extended conversion cost models looks for candidates that are more specific and less generic.
+@Var@s was introduced by Aaron to disambugate @forall(T, V) void foo(T, V)@ and @forall(T) void foo(T, T)@. The extra type parameter @V@ 
+makes it more generic and less specific. More generic type means less constraints on types of its parameters. \CFA is in favor of candidates with more 
+restrictions on polymorphism so @forall(T) void foo(T, T)@ has lower cost. @Specialization@ is a value that always less than or equal to zero. For every type assertion in @forall@ clause, \CFA subtracts one from 
+@specialization@, starting from zero. More type assertions often means more constraints on argument type, and making the function less generic.
+
+\CFA defines two special cost value: @zero@ and @infinite@ A conversion cost is @zero@ when argument and parameter has exact match, and a conversion cost is @infinite@ when 
+there is no defined conversion between two types. For example, the conversion cost from int to a struct type S is @infinite@. 

doc/theses/jiada_liang_MMath/implementation.tex

@@ -1 @@
-\chapter{Enumeration Implementation}
-
-\section{Enumeration Traits}
-
-\CFA defines a set of traits containing operators and helper functions for @enum@.
-A \CFA enumeration satisfies all of these traits allowing it to interact with runtime features in \CFA.
-Each trait is discussed in detail.
-
-The trait @CfaEnum@:
+\chapter{Enumeration Traits}
+\label{c:trait}
+
+\section{CfaEnum and TypedEnum}
+
+\CFA defines attribute functions @label()@ and @posn()@ for all \CFA enumerations, 
+and therefore \CFA enumerations fulfills the type assertions with the combination. 
+With the observation, we define trait @CfaEnum@:
 \begin{cfa}
 forall( E ) trait CfaEnum {
@@ -14 +13 @@
 };
 \end{cfa}
-asserts an enumeration type @E@ has named enumerator constants (@label@) with positions (@posn@).
-
-The trait @TypedEnum@ extends @CfaEnum@:
+
+% The trait @TypedEnum@ extends @CfaEnum@ with an additional value() assertion:
+Typed enumerations are \CFA enumeration with an additional @value@ attribute. Extending
+CfaEnum traits, TypedEnum is a subset of CFAEnum that implements attribute function @value()@, 
+which includes all typed enumerations. 
 \begin{cfa}
 forall( E, V | CfaEnum( E ) ) trait TypedEnum {
@@ -22 +23 @@
 };
 \end{cfa}
-asserting an enumeration type @E@ can have homogeneous enumerator values of type @V@.
-
-The declarative syntax
-\begin{cfa}
-enum(T) E { A = ..., B = ..., C = ... };
-\end{cfa}
-creates an enumerated type E with @label@, @posn@ and @value@ implemented automatically.
-\begin{cfa}
-void foo( T t ) { ... }
-void bar(E e) {
-        choose ( e ) {
-                case A: printf( "\%d", posn( e) );
-                case B: printf( "\%s", label( e ) );
-                case C: foo( value( e ) );
-        } 
-}
-\end{cfa}
-
-Implementing general functions across all enumeration types is possible by asserting @CfaEnum( E, T )@, \eg:
-\begin{cfa}
-#include <string.hfa>
-forall( E, T | CfaEnum( E, T ) | {unsigned int toUnsigned(T)} )
-string formatEnum( E e ) {
-        unsigned int v = toUnsigned( value( e ) );
-        string out = label(e) + '(' + v +')';
-        return out;
-}
-formatEnum( Week.Mon );
-formatEnum( RGB.Green );
-\end{cfa}
-
-\CFA does not define attribute functions for C-style enumeration.
-But it is possible for users to explicitly implement enumeration traits for C enum and any other types.
-\begin{cfa}
-enum Fruit { Apple, Pear, Cherry };                     $\C{// C enum}$
+Type parameter V of TypedEnum trait binds to return type of @value()@, which is also the base 
+type for typed enumerations. CfaEnum and TypedEnum triats constitues a CfaEnum function interfaces, as well a way to define functions
+over all CfaEnum enumerations.
+\begin{cfa}
+// for all type E that implements value() to return type T, where T is a type that convertible to string
+forall(  E, T | TypedEnum( E, T ) | { ?{}(string &, T ); } ) 
+string format_enum( E e ) { return label(E) + "(" + string(value(e)) + ")"; }
+
+// int is convertible to string; implemented in the standard library
+enum(int) RGB { Red = 0xFF0000, Green = 0x00FF00, Blue = 0x0000FF };
+
+struct color_code { int R; int G; int B }; 
+// Implement color_code to string conversion
+?{}(string & this, struct color_code p ) {
+        this = string(p.R) + ',' + string(p.G) + ',' + string(p.B);
+}
+enum(color_code) Rainbow {
+        Red = {255, 0, 0}, Orange = {255, 127, 0}, Yellow = {255, 255, 0}, Green = {0, 255, 0},
+        Blue = {0, 0, 255}, Indigo = {75, 0, 130}, Purple = {148, 0, 211}
+};
+
+format_enum(RGB.Green); // "Green(65280)"
+format_enum(Rainbow.Green); // "Green(0,255,0)"
+\end{cfa}
+
+
+% Not only CFA enumerations can be used with CfaEnum trait, other types that satisfy 
+% CfaEnum assertions are all valid. 
+Types does not need be defined as \CFA enumerations to work with CfaEnum traits. CfaEnum applies to any type 
+with @label()@ and @value()@ being properly defined. 
+Here is an example on how to extend a C enumeration to comply CfaEnum traits:
+\begin{cfa}
+enum Fruit { Apple, Banana, Cherry };                   $\C{// C enum}$
 const char * label( Fruit f ) {
-        choose ( f ) {
+        choose( f ) {
                 case Apple: return "Apple";
-                case Bear: return "Pear";
+                case Banana: return "Banana";
                 case Cherry: return "Cherry";
         }
 }
-unsigned posn( Fruit f ) { return f; }
-const char * value( Fruit f ) { return ""; } $\C{// value can return any non void type}$
-formatEnum( Apple );                                            $\C{// Fruit is now a \CFA enum}$
-\end{cfa}
-
-A type that implements trait @CfaEnum@, \ie, a type has no @value@, is called an opaque enum.
-
-% \section{Enumerator Opaque Type}
-
-% \CFA provides a special opaque enumeration type, where the internal representation is chosen by the compiler and only equality operations are available.
-\begin{cfa}
-enum@()@ Planets { MERCURY, VENUS, EARTH, MARS, JUPITER, SATURN, URANUS, NEPTUNE };
-\end{cfa}
-
-
-In addition, \CFA implements @Bound@ and @Serial@ for \CFA enumerations.
+unsigned posn( Fruit f ) { return f; } 
+char value( Fruit f ) { 
+        choose(f)  {
+                case Apple: return 'a';
+                case Banana: return 'b';
+                case Cherry: return 'c';
+        }
+}
+
+format_enum(Cherry); // "Cherry(c)"
+\end{cfa}
+
+\subsection{Bounded and Serial}
+A bounded type defines a lower bound and a upper bound.
 \begin{cfa}
 forall( E ) trait Bounded {
-        E first();
-        E last();
-};
-\end{cfa}
-The function @first()@ and @last()@ of enumerated type E return the first and the last enumerator declared in E, respectively. \eg:
-\begin{cfa}
-Workday day = first();                                  $\C{// Mon}$
-Planet outermost = last();                              $\C{// NEPTUNE}$
-\end{cfa}
-@first()@ and @last()@ are overloaded with return types only, so in the example, the enumeration type is found on the left-hand side of the assignment.
-Calling either functions without a context results in a type ambiguity, except in the rare case where the type environment has only one enumeration.
-\begin{cfa}
-@first();@                                                              $\C{// ambiguous because both Workday and Planet implement Bounded}$
-sout | @last()@;
-Workday day = first();                                  $\C{// day provides type Workday}$
+        E lowerBound();
+        E lowerBound();
+};
+
+\end{cfa}
+Both Bounded functions are implement for \CFA enumerations, with @lowerBound()@ returning the first enumerator and @upperBound()@ returning 
+the last enumerator.
+\begin{cfa}
+Workday day = lowerBound();                                     $\C{// Mon}$
+Planet outermost = upperBound();                                $\C{// NEPTUNE}$
+\end{cfa}
+
+The lowerBound() and upperBound() are functions overloaded on return type only, means their type resolution solely depend on the outer context, 
+including expected type as a function argument, or the left hand size of an assignment expression. 
+Calling either function without a context results in a type ambiguity, except in the rare case where the type environment has only one 
+type overloads the functions, including \CFA enumerations, which has Bounded functions automatic defined.
+\begin{cfa}
+@lowerBound();@                 $\C{// ambiguous as both Workday and Planet implement Bounded}$
+sout | @lowerBound()@;
+Workday day = first();          $\C{// day provides type Workday}$
 void foo( Planet p );
-foo( last() );                                                  $\C{// argument provides type Planet}$
-\end{cfa}
-
-The trait @Serial@:
+foo( last() );                      $\C{// argument provides type Planet}$
+\end{cfa}
+
+@Serial@ is a subset of @Bounded@, with functions maps elements against integers, as well implements a sequential order between members.
 \begin{cfa}
 forall( E | Bounded( E ) ) trait Serial {
         unsigned fromInstance( E e );
-        E fromInt( unsigned int posn );
+        E fromInt( unsigned int i );
         E succ( E e );
         E pred( E e );
-};
-\end{cfa}
-is a @Bounded@ trait, where elements can be mapped to an integer sequence.
-A type @T@ matching @Serial@ can project to an unsigned @int@ type, \ie an instance of type T has a corresponding integer value.
-%However, the inverse may not be possible, and possible requires a bound check.
-The mapping from a serial type to integer is defined by @fromInstance@, which returns the enumerator's position.
-The inverse operation is @fromInt@, which performs a bound check using @first()@ and @last()@ before casting the integer into an enumerator.
-Specifically, for enumerator @E@ declaring $N$ enumerators, @fromInt( i )@ returns the $i-1_{th}$ enumerator, if $0 \leq i < N$, or raises the exception @enumBound@.
-
-The @succ( E e )@ and @pred( E e )@ imply the enumeration positions are consecutive and ordinal. 
-Specifically, if @e@ is the $i_{th}$ enumerator, @succ( e )@ returns the $i+1_{th}$ enumerator when $e \ne last()$, and @pred( e )@ returns the $i-1_{th}$ enumerator when $e \ne first()$. 
-The exception @enumRange@ is raised if the result of either operation is outside the range of type @E@.
+        unsigned Countof( E e );
+};
+\end{cfa}
+
+% A Serail type can project to an unsigned @int@ type, \ie an instance of type T has a corresponding integer value.
+Function @fromInstance()@ projects a @Bounded@ member to a number and @fromInt@ is the inverser. Function @succ()@ take an element, returns the "next" 
+member in sequential order and @pred()@ returns the "last" member.
+
+A Serial type E may not be having a one-to-one mapping to integer because of bound. An integer that cannot be mapping to a member of E is called the member \newterm{out of bound}. 
+Calling @succ()@ on @upperBound@ or @pred()@ on @lowerBound()@ results in out of bound.
+
+\CFA implements Serial interface for CFA enumerations with \newterm{bound check} on @fromInt()@, @succ()@ and @pred()@, and abort the program if the function call results in out of bound.
+Unlike a cast, conversion between \CFA enumeration and integer with @Serial@ interface is type safe.
+Specifically for @fromInt@, \CFA abort if input i smaller than @fromInstance(lowerBound())@ or greater than @fromInstance(upperBound())@
+
+Function @Countof@ takes an object as a parameter and returns the number of elements in the Serial type, which is @fromInstance( upper ) - fromInstance( lower ) + 1@.
+@Countof@ does not use its arugment as procedural input; it needs 
+an argument to anchor its polymorphic type T. 
+
+\CFA has an expression @countof@ (lower case) that returns the number of enumerators defined for enumerations. 
+\begin{cfa}
+enum RGB {Red, Green, Blue};
+countof( RGB ); // (1)
+countof( Red ); // (2)
+\end{cfa}
+Both expressions from the previous example are converted to constant expression @3@ with no function call at runtime. 
+@countof@ also works for any type T that defines @Countof@ and @lowerBound@, for which it turns into 
+a function call @Countof( T )@. The resolution step on expression @countof(e)@ works as the following with priority ordered:
+\begin{enumerate}
+\item Looks for an enumeration named e, such as @enum e {... }@. 
+If such an enumeration e exists, \CFA replace @countof(e)@  with constant expression with number of enumerator of e.
+\item Looks for a non-enumeration type named e that defines @Countof@ and @lowerBound@, including e being a polymorphic type, such as @forall(e)@. 
+If type e exists, \CFA replaces it with @Countof(lowerBound())@, where lowerBound() is bounded to type e.  
+\item Looks for an enumerator e that defined in enumeration E. If such an enumeration e exists, \CFA replace @countof(e)@ with constant expression with number of enumerator of E.
+\item Looks for a name e in the context with expression type E. If such name e exists, \CFA replace @countof(e)@ with function call @Countof(e)@.
+\item If 1-4 fail, \CFA reports a type error on expression @countof(e)@.
+\end{enumerate}
+
+With the @Bounded@ and @Serial@, a loop over enumeration can be implemented in the following ways:
+\begin{cfa}
+enum() E { ... }
+for( unsigned i = 0; i < countof(E); i++ ) { ... }
+for( E e = lowerBound(); ; e = succ(e) ) { ...; if (e == upperBound()) break; }
+
+forall( T ) {
+        for( unsigned i = 0; i < countof(T); i++ ) { ... }
+        for( T e = lowerBound(); ; e = succ(e) ) { ...; if (e == upperBound()) break; }
+}
+\end{cfa}
 
 Finally, there is an associated trait defining comparison operators among enumerators. 
@@ -154 +193 @@
 
 
-\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 Initialization}
-
-C auto-initialization works for the integral type @int@ with constant expressions.
-\begin{cfa}
-enum Alphabet ! {
-        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
-};
-\end{cfa}
-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}
-
-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.
-
-
-\section{Enumeration Features}
-
-
 \section{Iteration and Range}
 
@@ -541 +273 @@
 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 {
-        Mon = 10, Tue, ...
-};
-
-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.

doc/theses/jiada_liang_MMath/uw-ethesis.tex

@@ -226 +226 @@
 \input{intro}
 \input{background}
+\input{CEnum}
 \input{CFAenum}
 \input{implementation}
 \input{relatedwork}
-\input{performance}
 \input{conclusion}