Changeset d1276f8 for doc/theses/jiada_liang_MMath

Timestamp:

Jul 24, 2024, 11:25:16 AM (4 months ago)

Author:

Peter A. Buhr <pabuhr@…>

Branches:

master

Children:

35c792f

Parents:

10a99d87

Message:

move enumeration trait material into implementation chapter

File:

• doc/theses/jiada_liang_MMath/implementation.tex (modified) (1 diff)

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}