Changeset a03ed29 for doc/theses/jiada_liang_MMath

Timestamp:

Jul 24, 2024, 7:11:32 PM (5 months ago)

Author:

JiadaL <j82liang@…>

Branches:

master

Children:

5aeb1a9

Parents:

e561551 (diff), b6923b17 (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.

Message:

conclude merge

Location:

doc/theses/jiada_liang_MMath

Files:

• CFAenum.tex (modified) (7 diffs)
• background.tex (modified) (8 diffs)
• implementation.tex (modified) (1 diff)
• intro.tex (modified) (5 diffs)

doc/theses/jiada_liang_MMath/CFAenum.tex

@@ -1 +1 @@
 \chapter{\CFA Enumeration}
-
 
 % \CFA supports C enumeration using the same syntax and semantics for backwards compatibility.
@@ -9 +8 @@
 \begin{clang}[identifierstyle=\linespread{0.9}\it]
 $\it enum$-specifier:
-        enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { enumerator-list-noinit }
-        enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { enumerator-list-noinit , }
+        enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { cfa-enumerator-list }
+        enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { cfa-enumerator-list , }
         enum @(type-specifier$\(_{opt}\)$)@ identifier
-enumerator-list-noinit:
+cfa-enumerator-list:
+        cfa-enumerator
+        cfa-enumerator, cfa-enumerator-list
+cfa-enumerator:
         enumeration-constant
-        enumerator-list-noinit , enumeration-constant
+        $\it inline$ identifier
+        enumeration-constant = expression
 \end{clang}
-\CFA enumerations, or \CFA enums, have optional type declaration in a bracket next to the enum keyword.
+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".
@@ -284 +287 @@
 Note, the validity of calls is the same for call-by-reference as for call-by-value, and @const@ restrictions are the same as for other types.
 
-
-
-\section{Enumeration Traits}
-
-\CFA defines the 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@:
-\begin{cfa}
-forall( E ) trait CfaEnum {
-        char * label( E e );
-        unsigned int posn( E e );
-};
-\end{cfa}
-
-describes an enumeration as a named constant with position. And @TypeEnum@
-\begin{cfa}
-forall( E, V ) trait TypeEnum {
-        V value( E e );
-};      
-\end{cfa}
-asserts two types @E@ and @T@, with @T@ being the base type for the enumeration @E@. 
-
-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;
-}
-printEunm( Week.Mon );
-printEnum( RGB.Green );
-\end{cfa}
-
-\CFA does not define attribute functions for C style enumeration. But it is possilbe for users to explicitly implement
-enumeration traits for C enum and any other types.
-
-\begin{cfa}
-enum Fruit { Apple, Bear, Cherry };                     $\C{// C enum}$
-char * label(Fruit f) {
-        switch(f) {
-                case Apple: "A"; break;
-                case Bear: "B"; break;
-                case Cherry: "C"; break;
-        }
-}
-unsigned posn(Fruit f) { return f; }
-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 Enums.
-\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}$
-void foo( Planet p );
-foo( last() );                                                  $\C{// parameter provides type Planet}$
-\end{cfa}
-
-The trait @Serial@:
-\begin{cfa}
-forall( E | Bounded( E ) ) trait Serial {
-        unsigned fromInstance( E e );
-        E fromInt( unsigned int posn );
-        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@.
-
-Finally, there is an associated trait defining comparison operators among enumerators. 
-\begin{cfa}
-forall( E, T | CfaEnum( E, T ) ) {
-        // comparison
-        int ?==?( E l, E r );           $\C{// true if l and r are same enumerators}$
-        int ?!=?( E l, E r );           $\C{// true if l and r are different enumerators}$
-        int ?!=?( E l, zero_t );        $\C{// true if l is not the first enumerator}$
-        int ?<?( E l, E r );            $\C{// true if l is an enumerator before r}$
-        int ?<=?( E l, E r );           $\C{// true if l before or the same as r}$
-        int ?>?( E l, E r );            $\C{// true if l is an enumerator after r}$
-        int ?>=?( E l, E r );           $\C{// true if l after or the same as r}$         
-}
-\end{cfa}
-
-
-
-
-
 \section{Enumerator Control Structures}
 
@@ -433 +295 @@
 
 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.
-\begin{cquote}
-\begin{cfa}
+(For this discussion, ignore the fact that @case@ requires a compile-time constant.)
+\begin{cfa}[belowskip=0pt]
 enum Count { First, Second, Third, Fourth };
 Count e;
 \end{cfa}
-\begin{tabular}{ll}
-\begin{cfa}
+\begin{cquote}
+\setlength{\tabcolsep}{15pt}
+\noindent
+\begin{tabular}{@{}ll@{}}
+\begin{cfa}[aboveskip=0pt]
 
 choose( e ) {
@@ -449 +314 @@
 \end{cfa}
 &
-\begin{cfa}
+\begin{cfa}[aboveskip=0pt]
 // rewrite
 choose( @value@( e ) ) {
@@ -465 +330 @@
 enum Count { First, Second, Third @= First@, Fourth };
 \end{cfa}
-which make @Third == First@ and @Fourth == Second@, causing a compilation error because of duplicate @case@ clauses.
+making @Third == First@ and @Fourth == Second@, causing a compilation error because of duplicate @case@ clauses.
 To better match with programmer intuition, \CFA toggles between value and position semantics depending on the language context.
 For conditional clauses and switch statements, \CFA uses the robust position implementation.
 \begin{cfa}
-choose( @position@( e ) ) {
-        case @position@( First ): ...;
-        case @position@( Second ): ...;
-        case @position@( Third ): ...;
-        case @position@( Fourth ): ...;
-}
-\end{cfa}
-
-\begin{cfa}
-Count variable_a = First, variable_b = Second, variable_c = Third, variable_d = Fourth;
-p(variable_a); // 0
-p(variable_b); // 1
-p(variable_c); // "Third"
-p(variable_d); // 3
-\end{cfa}
-
-\begin{cfa}
-for (d; Workday) { sout | d; }
-for (p; +~=Planet) { sout | p; }
-for (c: -~=Alphabet ) { sout | c; }
-\end{cfa}
-The @range loop@ for enumeration is a syntax sugar that loops over all enumerators and assigns each enumeration to a variable in every iteration.
-The loop control of the range loop consists of two parts: a variable declaration and a @range expression@, with the type of the variable
-can be inferred from the range expression.
-
-The range expression is an enumeration type, optionally prefixed by @+~=@ or @-~=@. Without a prefix, or prefixed with @+~=@, the control
-loop over all enumerators from the first to the last. With a @-~=@ prefix, the control loops backward.
-
-On a side note, the loop syntax
-\begin{cfa}
-for ( typeof(Workday) d; d <= last(); d = succ(d) );
-\end{cfa}
-does not work. When d == last(), the loop control will still attempt to assign succ(d) to d, which causes an @enumBound@ exception.
-
-\CFA reduces conditionals to its "if case" if the predicate is not equal to ( @!=@ ) zero, and the "else case" otherwise.
-Overloading the @!=@ operator with an enumeration type against the zero defines a conceptual conversion from
-enum to boolean, which can be used as predicates.
-
+if ( @posn@( e ) < posn( Third ) ) ...
+choose( @posn@( e ) ) {
+        case @posn@( First ): ...;
+        case @posn@( Second ): ...;
+        case @posn@( Third ): ...;
+        case @posn@( Fourth ): ...;
+}
+\end{cfa}
+
+\CFA provides a special form of for-control for enumerating through an enumeration, where the range is a type.
+\begin{cfa}
+for ( cx; @Count@ ) { sout | cx | nonl; } sout | nl;
+for ( cx; +~= Count ) { sout | cx | nonl; } sout | nl;
+for ( cx; -~= Count ) { sout | cx | nonl; } sout | nl;
+First Second Third Fourth
+First Second Third Fourth
+Fourth Third Second First
+\end{cfa}
+The enumeration type is syntax sugar for looping over all enumerators and assigning each enumerator to the loop index, whose type is inferred from the range type.
+The prefix @+~=@ or @-~=@ iterate forward or backwards through the inclusive enumeration range, where no prefix defaults to @+~=@.
+
+C has an idiom for @if@ and loop predicates of comparing the predicate result ``not equal to 0''.
+\begin{cfa}
+if ( x + y /* != 0 */ ) ...
+while ( p /* != 0 */ ) ...
+\end{cfa}
+This idiom extends to enumerations because there is a boolean conversion in terms of the enumeration value, if and only if such a conversion is available.
+For example, such a conversion exists for all numerical types (integral and floating-point).
+It is possible to explicitly extend this idiom to any typed enumeration by overloading the @!=@ operator.
+\begin{cfa}
+bool ?!=?( Name n, zero_t ) { return n != Fred; }
+Name n = Mary;
+if ( n ) ... // result is true
+\end{cfa}
+Specialize meanings are also possible.
 \begin{cfa}
 enum(int) ErrorCode { Normal = 0, Slow = 1, Overheat = 1000, OutOfResource = 1001 };
-bool ?!=?(ErrorCode lhs, zero_t) { return value(lhs) >= 1000; }
-ErrorCode code = /.../
-if (code) { scream(); }
-\end{cfa}
-
-Incidentally, \CFA does not define boolean conversion for enumeration. If no 
-@?!=?(ErrorCode, zero_t)@ 
-overloading defined,
-\CFA looks for the boolean conversion in terms of its value and gives a compiler error if no such conversion is available.
-
-\begin{cfa}
-enum(int) Weekday { Mon, Tues, Wed, Thurs, Fri, Sat, Sun, };
-enum() Colour { Red, Green, Blue };
-enum(S) Fruit { Apple, Banana, Cherry }
-Weekday w = ...; Colour c = ...; Fruit f = ...;
-if (w) { ... } // w is true if and only if w != Mon, because value(Mon) == 0 (auto initialized)
-if (c) { ... } // error
-if (s) { ... } // depends on ?!=?(S lhs, zero_t ), and error if no such overloading available
-\end{cfa}
-
-As an alternative, users can define the boolean conversion for CfaEnum:
-
-\begin{cfa}
-forall(E | CfaEnum(E))
-bool ?!=?(E lhs, zero_t) {
-        return posn(lhs) != 0;
-}
-\end{cfa}
-which effectively turns the first enumeration as a logical zero and non-zero for others.
-
-\section{Enumerated Arrays}
-Enumerated arrays use an \CFA array as their index.
-\begin{cfa}
-enum() Colour {
-        Red, Orange, Yellow, Green, Blue, Indigo, Violet
-};
-
-string colourCode[Colour] = { "#e81416", "#ffa500", "#ffa500", "#ffa500", "#487de7", "#4b369d", "#70369d" };
-sout | "Colour Code of Orange is " | colourCode[Orange];
-\end{cfa}
+bool ?!=?( ErrorCode ec, zero_t ) { return ec >= Overheat; }
+ErrorCode code = ...;
+if ( code ) { problem(); }
+\end{cfa}
+
+
+\section{Enumeration Dimension}
+
+\VRef{s:EnumeratorTyping} introduced the harmonizing problem between an enumeration and secondary information.
+When possible, using a typed enumeration for the secondary information is the best approach.
+However, there are times when combining these two types is not possible.
+For example, the secondary information might precede the enumeration and/or its type is needed directly to declare parameters of functions.
+In these cases, having secondary arrays of the enumeration size are necessary.
+
+To support some level of harmonizing in these cases, an array dimension can be defined using an enumerator type, and the enumerators used as subscripts.
+\begin{cfa}
+enum E { A, B, C, N }; // possibly predefined
+float H1[N] = { [A] : 3.4, [B] : 7.1, [C] : 0.01 }; // C
+float H2[@E@] = { [A] : 3.4, [B] : 7.1, [C] : 0.01 }; // CFA
+\end{cfa}
+(Note, C uses the symbol, @'='@ for designator initialization, but \CFA had to change to @':'@ because of problems with tuple syntax.)
+This approach is also necessary for a predefined typed enumeration (unchangeable), when additional secondary-information need to be added.
 
 
@@ -568 +412 @@
 \small
 \begin{cfa}
-struct MR { double mass, radius; };
+struct MR { double mass, radius; };                     $\C{// planet definition}$
 enum( @MR@ ) Planet {                                           $\C{// typed enumeration}$
         //                      mass (kg)   radius (km)

doc/theses/jiada_liang_MMath/background.tex

@@ -6 +6 @@
 The following discussion covers C enumerations.
 
-As discussed in \VRef{s:Aliasing}, it is common for C programmers to ``believe'' there are three equivalent forms of named constants.
+As mentioned in \VRef{s:Aliasing}, it is common for C programmers to ``believe'' there are three equivalent forms of named constants.
 \begin{clang}
 #define Mon 0
@@ -33 +33 @@
 C can simulate the aliasing @const@ declarations \see{\VRef{s:Aliasing}}, with static and dynamic initialization.
 \begin{cquote}
-\begin{tabular}{@{}l@{}l@{}}
-\multicolumn{1}{@{}c@{}}{\textbf{static initialization}} &  \multicolumn{1}{c@{}}{\textbf{dynamic intialization}} \\
+\begin{tabular}{@{}ll@{}}
+\multicolumn{1}{@{}c}{\textbf{static initialization}} &  \multicolumn{1}{c@{}}{\textbf{dynamic intialization}} \\
 \begin{clang}
 static const int one = 0 + 1;
@@ -51 +51 @@
         int va[r];
 }
-
-
 \end{clang}
 \end{tabular}
 \end{cquote}
-However, statically initialized identifiers can not appear in constant-expression contexts, \eg @case@.
+However, statically initialized identifiers cannot appear in constant-expression contexts, \eg @case@.
 Dynamically initialized identifiers may appear in initialization and array dimensions in @g++@, which allows variable-sized arrays on the stack.
 Again, this form of aliasing is not an enumeration.
-
 
 \section{C Enumeration}
@@ -129 +126 @@
 
 
-\subsection{Representation}
-
-C standard specifies enumeration \emph{variable} is an implementation-defined integral type large enough to hold all enumerator values.
-In practice, C uses @int@ as the underlying type for enumeration variables, because of the restriction to integral constants, which have type @int@ (unless qualified with a size suffix).
+\subsection{Implementation}
+\label{s:CenumImplementation}
+
+In theory, a C enumeration \emph{variable} is an implementation-defined integral type large enough to hold all enumerator values.
+In practice, C defines @int@~\cite[\S~6.4.4.3]{C11} as the underlying type for enumeration variables, restricting initialization to integral constants, which have type @int@ (unless qualified with a size suffix).
+However, type @int@ is defined as:
+\begin{quote}
+A ``plain'' @int@ object has the natural size suggested by the architecture of the execution environment (large enough to contain any value in the range @INT_MIN@ to @INT_MAX@ as defined in the header @<limits.h>@).~\cite[\S~6.2.5(5)]{C11}
+\end{quote}
+Howeveer, @int@ means a 4 bytes on both 32/64-bit architectures, which does not seem like the ``natural'' size for a 64-bit architecture.
+Whereas, @long int@ means 4 bytes on a 32-bit and 8 bytes on 64-bit architectures, and @long long int@ means 8 bytes on both 32/64-bit architectures, where 64-bit operations are simulated on 32-bit architectures.
+In reality, both @gcc@ and @clang@ partially ignore this specification and type the integral size of an enumerator based its initialization.
+\begin{cfa}
+enum E { IMin = INT_MIN, IMax = INT_MAX,
+                         ILMin = LONG_MIN, ILMax = LONG_MAX,
+                         ILLMin = LLONG_MIN, ILLMax = LLONG_MAX };
+int main() {
+        printf( "%zd %d %d\n%zd %ld %ld\n%zd %ld %ld\n",
+                         sizeof(IMin), IMin, IMax,
+                         sizeof(ILMin), ILMin, ILMax,
+                         sizeof(ILLMin), ILLMin, ILLMax );
+}
+4 -2147483648 2147483647
+8 -9223372036854775808 9223372036854775807
+8 -9223372036854775808 9223372036854775807
+\end{cfa}
+Hence, initialization in the range @INT_MIN@..@INT_MAX@ is 4 bytes, and outside this range is 8 bytes.
 
 \subsection{Usage}
@@ -150 +170 @@
 enum Week { Mon, Tue, Wed, Thu, Fri, Sat, Sun };
 switch ( week ) {
-        case Mon: case Tue: case Wed: case Thu: case Fri:
+        case Mon ... Fri:                               $\C{// gcc case range}$
                 printf( "weekday\n" );
         case Sat: case Sun:
                 printf( "weekend\n" );
 }
-for ( enum Week day = Mon; day <= Sun; day += 1 ) { // step of 1
+for ( enum Week day = Mon; day <= Sun; day += 1 ) { $\C{// step of 1}$
         printf( "day %d\n", day ); // 0-6
 }
@@ -177 +197 @@
 }
 \end{cfa}
-However, for typed enumerations, \see{\VRef{f:EumeratorTyping}}, this idiom fails.
-
-This idiom leads to another C idiom using an enumeration with matching companion information.
+However, for non-integral typed enumerations, \see{\VRef{f:EumeratorTyping}}, this idiom fails.
+
+This idiom is used in another C idiom for matching companion information.
 For example, an enumeration is linked with a companion array of printable strings.
 \begin{cfa}
@@ -196 +216 @@
 
 \bigskip
-While C provides a true enumeration, it is restricted, has unsafe semantics, and does provide useful enumeration features in other programming languages.
+While C provides a true enumeration, it is restricted, has unsafe semantics, and does not provide useful enumeration features in other programming languages.
 
 \section{\CFA Polymorphism}
@@ -238 +258 @@
 \subsection{Constructor and Destructor}
 In \CFA, all objects are initialized by @constructors@ during its allocation, including basic types, 
-which are initialized by constructors default-generated by a compiler.
+which are initialized by auto-generated basic type constructors.
 
 Constructors are overloadable functions with name @?{}@, return @void@, and have at least one parameter, which is a reference

doc/theses/jiada_liang_MMath/implementation.tex

@@ -1 +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@:
+\begin{cfa}
+forall( E ) trait CfaEnum {
+        const char * @label@( E e );
+        unsigned int @posn@( E e );
+};
+\end{cfa}
+asserts an enumeration type @E@ has named enumerator constants (@label@) with positions (@posn@).
+
+The trait @TypedEnum@ extends @CfaEnum@:
+\begin{cfa}
+forall( E, V | CfaEnum( E ) ) trait TypedEnum {
+        V @value@( E e );
+};
+\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}$
+const char * label( Fruit f ) {
+        choose ( f ) {
+                case Apple: return "Apple";
+                case Bear: return "Pear";
+                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.
+\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}$
+void foo( Planet p );
+foo( last() );                                                  $\C{// argument provides type Planet}$
+\end{cfa}
+
+The trait @Serial@:
+\begin{cfa}
+forall( E | Bounded( E ) ) trait Serial {
+        unsigned fromInstance( E e );
+        E fromInt( unsigned int posn );
+        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@.
+
+Finally, there is an associated trait defining comparison operators among enumerators. 
+\begin{cfa}
+forall( E, T | CfaEnum( E, T ) ) {
+        // comparison
+        int ?==?( E l, E r );           $\C{// true if l and r are same enumerators}$
+        int ?!=?( E l, E r );           $\C{// true if l and r are different enumerators}$
+        int ?!=?( E l, zero_t );        $\C{// true if l is not the first enumerator}$
+        int ?<?( E l, E r );            $\C{// true if l is an enumerator before r}$
+        int ?<=?( E l, E r );           $\C{// true if l before or the same as r}$
+        int ?>?( E l, E r );            $\C{// true if l is an enumerator after r}$
+        int ?>=?( E l, E r );           $\C{// true if l after or the same as r}$         
+}
+\end{cfa}
+
+As an alternative, users can define the boolean conversion for CfaEnum:
+
+\begin{cfa}
+forall(E | CfaEnum(E))
+bool ?!=?(E lhs, zero_t) {
+        return posn(lhs) != 0;
+}
+\end{cfa}
+which effectively turns the first enumeration as a logical zero and non-zero for others.
+
+\begin{cfa}
+Count variable_a = First, variable_b = Second, variable_c = Third, variable_d = Fourth;
+p(variable_a); // 0
+p(variable_b); // 1
+p(variable_c); // "Third"
+p(variable_d); // 3
+\end{cfa}
+
+
+\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}

doc/theses/jiada_liang_MMath/intro.tex

@@ -4 +4 @@
 Constants can be overloaded among types, \eg @0@ is a null pointer for all pointer types, and the value zero for integer and floating-point types.
 (In \CFA, the constants @0@ and @1@ can be overloaded for any type.)
-A constant's symbolic name is dictated by language syntax related to types.
+A constant's symbolic name is dictated by language syntax related to types, \eg @5.@ (double), @5.0f@ (float), @5l@ (long double).
 In general, the representation of a constant's value is \newterm{opaque}, so the internal representation can be chosen arbitrarily.
 In theory, there are an infinite set of constant names per type representing an infinite set of values.
@@ -13 +13 @@
 
 Many programming languages capture this important software-engineering capability through a mechanism called \newterm{constant} or \newterm{literal} naming, where a new constant is aliased to an existing constant.
-Its purpose is for readability, replacing a constant name that directly represents a value with a name that is more symbolic and meaningful in the context of the program.
+Its purpose is for readability: replacing a constant name that directly represents a value with a name that is more symbolic and meaningful in the context of the program.
 Thereafter, changing the aliasing of the new constant to another constant automatically distributes the rebinding, preventing errors.
 % and only equality operations are available, \eg @O_RDONLY@, @O_WRONLY@, @O_CREAT@, @O_TRUNC@, @O_APPEND@.
@@ -67 +67 @@
 \label{s:Terminology}
 
-The term \newterm{enumeration} defines a type with a set of new constants, and the term \newterm{enumerator} represents an arbitrary alias name \see{\VRef{s:CEnumeration} for the name derivation}.
-As well, an enumerated type can have three fundamental properties, \newterm{label}, \newterm{order}, and \newterm{value}.
+The term \newterm{enumeration} defines a type with a set of new constants, and the term \newterm{enumerator} represents an arbitrary alias name \see{\VRef{s:CEnumeration} for the name derivations}.
+An enumerated type can have three fundamental properties, \newterm{label} (name), \newterm{order} (position), and \newterm{value} (payload).
 \begin{cquote}
 \sf\setlength{\tabcolsep}{3pt}
@@ -111 +111 @@
 \end{cfa}
 The alias name is logically replaced in the program text by its matching constant.
-It is possible to compare aliases, if the constants allow it, \eg @Size < Pi@;
-whereas \eg @Pi < Name@ might be disallowed depending on the language.
+It is possible to compare aliases, if the constants allow it, \eg @Size < Pi@, whereas @Pi < Name@ might be disallowed depending on the language.
 
 Aliasing is not macro substitution, \eg @#define Size 20@, where a name is replaced by its value \emph{before} compilation, so the name is invisible to the programming language.
@@ -133 +132 @@
 Any reordering of the enumerators requires manual renumbering.
 \begin{cfa}
-const Sun = 1, Mon = 2, Tue = 3, Wed = 4, Thu = 5, Fri = 6, Sat = 7;
+const @Sun = 1@, Mon = 2, Tue = 3, Wed = 4, Thu = 5, Fri = 6, Sat = 7;
 \end{cfa}
 For these reasons, aliasing is sometimes called an enumeration.