Index: doc/theses/jiada_liang_MMath/trait.tex
===================================================================
--- doc/theses/jiada_liang_MMath/trait.tex	(revision bd686f0a4193bec9130edec2ddc51e8bbb5df7e5)
+++ doc/theses/jiada_liang_MMath/trait.tex	(revision 8cb2ff633d154e6819fdc26b163cfc2247eac230)
@@ -2,31 +2,38 @@
 \label{c:trait}
 
-% Despite parametric polymorphism being a pivotal feature of \CFA, for a long time, there was not 
-% a technique to write functions being polymorphic over enumerated types. 
-\CC introduced @std::is_enum@ trait on \CC{11} and @concepts@ on \CC{20}; with the combination, users can 
-write function polymorphic over enumerated type in \CC:
-\begin{cfa}
+\CC introduced the @std::is_enum@ trait in \CC{11} and concept feature in \CC{20}.
+With this combination, it is possible to write a polymorphic function over an enumerated type.
+\begin{c++}
 #include <type_traits>
-
-template<typename T>
-@concept Enumerable = std::is_enum<T>::value;@
-
-template<@Enumerable@ T>
-void f(T) {}
-\end{cfa}
-The @std::is_enum@ and other \CC @traits@ are a compile-time interfaces to query type information. 
-While named the same as @trait@, it is orthogonal to \CFA trait, as the latter being defined as 
-a collection of assertion to be satisfied by a polymorphic type.
-
-\CFA provides @CfaEnum@ and @TypedEnum@ traits to supports polymorphic functions for \CFA enumeration:
-\begin{cfa}
-forall(T | @CfaEnum(T)@)
-void f(T) {}
-\end{cfa}
-
-\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@:
+template<typename T>  @concept Enumerable@  =  std::is_enum<T>::value;
+template<@Enumerable@ E>  E  f( E e ) {	$\C{// constrainted type}$
+	E w = e;							$\C{// alloction and copy}$
+	cout << e << ' ' << w << endl;		$\C{// value}$
+	return w;							$\C{// copy}$
+}
+int main() {
+	enum E { A = 42, B, C } e = C;
+	e = f( e );
+}
+44 44
+\end{c++}
+The @std::is_enum@ and other \CC @traits@ are a compile-time interfaces to query type information.
+While named the same as @trait@ in other programming languages, it is orthogonal to the \CFA trait, with the latter being defined as a collection of assertion to be satisfied by a polymorphic type.
+
+The following sections cover the underlying implementation features I created to generalize and restrict enumerations in the \CFA type-system using the @trait@ mechanism.
+
+
+\section{Traits \lstinline{CfaEnum} and \lstinline{TypedEnum}}
+
+Traits @CfaEnum@ and @TypedEnum@ define the enumeration attributes: @label@, @posn@, @value@, and @Countof@.
+These traits support polymorphic functions for \CFA enumeration, \eg:
+\begin{cfa}
+forall( E ) | @CfaEnum( E )@ )
+void f( E e ) {
+	// access enumeration properties for e
+}
+\end{cfa}
+
+Trait @CfaEnum@ defines attribute functions @label@ and @posn@ for all \CFA enumerations, and internally \CFA enumerations fulfills this assertion.
 \begin{cfa}
 forall( E ) trait CfaEnum {
@@ -35,9 +42,7 @@
 };
 \end{cfa}
-
-% 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. 
+This trait covers opaque enumerations that do not have an explicit @value@.
+
+The trait @TypedEnum@ extends @CfaEnum@ with the @value@ assertion for typed enumerations.
 \begin{cfa}
 forall( E, V | CfaEnum( E ) ) trait TypedEnum {
@@ -45,89 +50,85 @@
 };
 \end{cfa}
-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);
-}
+Here, the associate type-parameter @V@ is the base type of the typed enumeration, and hence, the return type of @value@.
+These two traits provide a way to define functions over all \CFA enumerations.
+
+For example, \VRef[Figure]{f:GeneralizedEnumerationFormatter} shows a generalized enumeration formatter for any enumeration type.
+The formatter prints an enumerator name and its value in the form @"label( value )"@.
+The trait for @format_enum@ requires a function named @str@ for printing the value (payload) of the enumerator.
+Hence, enumeration defines how its value appear and @format_enum@ displays this value within the label name.
+
+\begin{figure}
+\begin{cfa}
+forall( @E, V | TypedEnum( E, V )@ | { string str( V ); } ) $\C{// format any enumeration}$
+string format_enum( E e ) {
+	return label( e ) + '(' + str( value( e ) ) + ')'; $\C{// "label( value )"}$
+}
+enum(size_t) RGB { Red = 0xFF0000, Green = 0x00FF00, Blue = 0x0000FF };
+// string library has conversion function str from size_t to string
+
+struct color_code { int R, G, 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 ) {
-		case Apple: return "Apple";
-		case Banana: return "Banana";
-		case Cherry: return "Cherry";
-	}
-}
-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}
-
-\section{Discussion: Static Type Information}
-@CfaEnum@ and @TypedEnum@ are approximations to \CFA Enumerations and Typed Enumerations: they are not 
-assertions on a type being an enumerated type, 
-but rather types being shared an interfaces with \CFA enumerations.
-\CC's @type_traits@ is fundamentally different than \CFA's traits: \CC's @type_traits@ are descriptions 
-of compile time type information
-\footnote{Concepts can check if a \CC class implement a certain method, 
-but it is to probe a static type information of a class having a such member.}
-, while \CFA's trait describe how a type can be used, 
-which is a closer paradigm to a trait system in languages such as Scala and Rust. 
-However, Scala and Rust's traits are nominative: 
-a type explicitly declare a named traits to be of its type; while in \CFA, 
-type implements all functions declares in a trait to implicitly be of the trait type.
-
-If to support static type information, \CFA needs new piece of syntax to distinguish static type 
-query from function calls, for example:
-\begin{cfa}
-forall(T | { T::is_enum; });
-\end{cfa}
-When to call a polymorphic function @foo(T)@ with assertions set @S@ and function call argument @a@, \CFA 
-determines if there is an overloaded name @a@ that has non-zero conversion cost to all assertions in @S@.
-As a consequence, @is_enum@ can be a \CFA directive that immediately trim down the search space of @a@ to 
-be some enumerated types. In fact, because \CFA stores symbols maps to enumeration in a standalone data structure. 
-Limiting search space to enumeration improve on \CFA resolution speed.
-
-While assertion on static type information seems improvement on expressivity, it is a challenge to 
-extend its capability without a fully functional pre-processsor that evaluate constant expression as \CC 
-compilers does. The described @is_enum@ manipulate compiler behaviour, which cannot be easily extended to 
-other usage cases. Therefore, \CFA currently does not support @is_enum@ and utalizes traits as a workaround.
+	Red = {255, 0, 0}, Orange = {255, 127, 0}, Yellow = {255, 255, 0}, Green = {0, 255, 0}, // ...
+};
+string str( color_code cc ) with( cc ) {	$\C{// format payload, "ddd,ddd,ddd"}$
+	return str( R ) + ',' + str( G ) + ',' + str( B ); $\C{// "R,G,B"}$
+}
+int main() {
+	sout | format_enum( RGB.Green );		$\C{// "Green(65280)"}$
+	sout | format_enum( Rainbow.Green );	$\C{// "Green(0,255,0)"}$
+}
+\end{cfa}
+\caption{Generalized Enumeration Formatter}
+\label{f:GeneralizedEnumerationFormatter}
+\end{figure}
+
+Other types may work with traits @CfaEnum@ and @TypedEnum@, by supplying appropriate @label@, @posn@, and @value@ functions.
+For example, \VRef[Figure]{f:GeneralizedEnumerationFormatter} extends a (possibly predefined) C enumeration to work with all the \CFA extensions.
+
+\begin{figure}
+\begin{cfa}
+enum Fruit { Apple, Banana, Cherry };		$\C{// C enum}$
+const char * @label@( Fruit f ) {
+	static const char * labels[] = { "Apple", "Banana", "Cherry" };
+	return labels[f];
+}
+int @posn@( Fruit f ) { return f; }
+int @value@( Fruit f ) {
+	static const char values[] = { 'a', 'b', 'c' };
+	return values[f];
+}
+sout | format_enum( Cherry );				$\C{// "Cherry(c)"}$
+\end{cfa}
+\caption{Generalized Enumeration Formatter}
+\label{f:GeneralizedEnumerationFormatter}
+\end{figure}
+
+
+\section{Discussion: Genericity}
+
+At the start of this chapter, the \CC concept is introduced to constraint template types, \eg:
+\begin{c++}
+concept Enumerable = std::is_enum<T>::value;
+\end{c++}
+Here, @concept@ is referring directly to types with kind @enum@;
+other @concept@s can refer to all types with kind @int@ with @long@ or @long long@ qualifiers, \etc.
+Hence, the @concept@ is a first level of restriction allowing only the specified kinds of types and rejecting others.
+The template expansion is the second level of restriction verifying if the type passing the @concept@ test provides the necessary functionality.
+Hence, a @concept@ is querying precise aspects of the programming language set of types.
+
+Alternatively, languages using traits, like \CFA, Scala, Go, and Rust, are defining a restriction based on a set of operations, variables, or structure fields that must exist to match with usages in a function or aggregate type.
+Hence, the \CFA enumeration traits never connected with the specific @enum@ kind.
+Instead, anything that can look like the @enum@ kind is considered an enumeration (duck typing).
+However, Scala, Go, and Rust traits are nominative: a type explicitly declares a named traits to be of its type, while in \CFA, the type implements all functions declared in a trait to implicitly satisfy a polymorphic function/type needs.
+
+One of the key differences between concepts and traits, which is leveraged heavily by \CFA, is the ability to apply new \CFA features to C legacy code.
+For example, \VRef[Figure]{f:GeneralizedEnumerationFormatter} shows that pre-existing C enumerations can be upgraded to work and play with new \CFA enumeration facilities.
+Another example is adding constructors and destructors to pre-existing C types by simply declaring them for the old C type.
+\CC fails at certain levels of legacy extension because many of the new \CC features must appear \emph{within} an aggregate definition, where it is impossible to change legacy library types.
 
 
 \section{Bounded and Serial}
-A bounded type defines a lower bound and a upper bound.
+
+A bounded trait defines a lower and upper bound for a type.
 \begin{cfa}
 forall( E ) trait Bounded {
@@ -135,145 +136,142 @@
 	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}
-
-@Serial@ is a subset of @Bounded@, with functions maps elements against integers, as well implements a sequential order between members.
+\end{cfa}
+Both functions are necessary for the implementation of \CFA enumeration, with @lowerBound@ returning the first enumerator and @upperBound@ returning the last enumerator.
+\begin{cfa}
+enum(int) Week { Mon, Tue, Wed, Thu, Fri, Sat, Sun };
+enum(int) Fruit { Apple, Banana, Cherry };
+Week first_day = lowerBound();				$\C{// Mon}$
+Fruit last_fruit = upperBound();			$\C{// Cherry}$
+\end{cfa}
+The @lowerBound@ and @upperBound@ are functions overloaded on return type only, meaning their type resolution depends solely on the call-site context, such as the parameter type for a function argument or the left hand size of an assignment expression.
+Calling either function without a context results in a type ambiguity, unless the type environment has only one type overloading the functions.
+\begin{cfa}
+sout | @lowerBound()@;      $\C[2.5in]{// ambiguous as Week and Fruit implement Bounded}$
+void foo( Fruit );
+foo( lowerBound() );		$\C{// parameter provides type Fruit}$
+Week day = upperBound();	$\C{// day provides type Week}\CRT$
+\end{cfa}
+
+Trait @Serial@ is a subset of @Bounded@, with functions mapping enumerators to integers, and implementing a sequential order between enumerators.
 \begin{cfa}
 forall( E | Bounded( E ) ) trait Serial {
-	unsigned fromInstance( E e );
+	int fromInstance( E e );
 	E fromInt( unsigned int i );
+	E pred( E e );
 	E succ( E e );
-	E pred( E 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 );
-countof( Red );
-\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:
+	unsigned Countof( E );
+};
+\end{cfa}
+Function @fromInstance@ projects a @Bounded@ member to a number and @fromInt@ is the inverse.
+Function @pred@ takes an enumerator and returns the previous enumerator, if there is one, in sequential order, and @succ@ returns the next enumerator.
+\begin{cfa}
+sout | fromInstance( Wed ) | fromInt( 2 ) | succ( Wed ) | pred( Wed );
+2 Wed Thu Tue
+\end{cfa}
+Bound checking is provided for @fromInt@, @pred@, and @succ@, and the program is terminated if the lower or upper bound is exceeded, \eg:
+\begin{cfa}
+fromInt( 100 );
+Cforall Runtime error: call to fromInt has index 100 outside of enumeration range 0-6.
+\end{cfa}
+Function @fromInstance@ or a position cast using @(int)@ is always safe, \ie within the enumeration range.
+
+Function @Countof@ is the generic counterpart to the builtin pseudo-function @countof@.
+@countof@ only works on enumeration types and instances, so it is locked into the language type system;
+as such, @countof( enum-type)@ becomes a compile-time constant.
+@Countof@ works on an any type that matches the @Serial@ trait.
+Hence, @Countof@ does not use its argument;
+only the parameter type is needed to compute the range size.
+\begin{cfa}
+int Countof( E ) {
+	E upper = upperBound();
+	E lower = lowerBound();
+	return fromInstance( upper ) + fromInstance( lower ) + 1;
+}
+\end{cfa}
+
+@countof@ also works for any type @E@ that defines @Countof@ and @lowerBound@, becoming a call to @Countof( E )@.
+The resolution step on expression @countof( E )@ are:
 \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)@.
+\item Look for an enumeration named @E@, such as @enum E {... }@.
+If such an enumeration @E@ exists, replace @countof( E )@  with the number of enumerators.
+\item Look 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, replaces it with @Countof(lowerBound())@, where @lowerBound@ is defined for type @E@.
+\item Look for an enumerator @A@ defined in enumeration @E@.
+If such an enumerator @A@ exists, replace @countof( A )@ with the number of enumerators in @E@.
+\item Look for a name @A@ in the lexical context with type @E@.
+If such name @A@ exists, replace @countof( A )@ with function call @Countof( E )@.
+\item If 1-4 fail, report a type error on expression @countof( E )@.
 \end{enumerate}
 
-\section{Iterating Over An Enumeration}
-An fundamental aspect of an enumerated type is to be able to enumerate over its enumerators. \CFA supports \newterm{for} loops,
-\newterm{while} loop, and \newterm{range} loop. This section covers @for@ loops and @range@ loops for 
-enumeration, but the concept transition to @while@ loop.
+
+\section{Enumerating}
+
+The fundamental aspect of an enumeration type is the ability to enumerate over its enumerators.
+\CFA supports \newterm{for} loops, \newterm{while} loop, and \newterm{range} loop. This section covers @for@ loops and @range@ loops for enumeration, but the concept transition to @while@ loop.
+
 
 \subsection{For Loop}
-A for loop is constitued by a loop control and a loop body.
-A loop control is often a 3-tuple, separated by semicolons: initializers, condition, and an expression. It is a common practice to declare 
-a variable, often in initializers, that be used in the condition and updated in the expression or loop body. Such variable is called \newterm{index}.
-
-% With implemented @Bounded@ and @Serial@ interface for \CFA enumeration, a @for@ loop that iterates over \CFA enumeration can be implemented as the following:
-A @for@ loop iterates an enumeration can be written with functions from @Bounded@ and @Serial@ interfaces:
-\begin{cfa}
-enum() Chars { A, B, C, D };
-for( unsigned i = 0; i < countof(E); i++ ) { sout | label(e); }		$\C{// (1) A B C D}$
-for( Chars e = lowerBound(); ; e = succ(e) ) { $\C{// (2)}$
-	sout |label((Chars)fromInt(i)) |' '; 
-	if (e == upperBound()) break; 
-}
-\end{cfa}
-
-A caveat in writing loop using finite number as index is that the number can unintentionally be out the range:
-\begin{cfa}
-for( unsigned i = countof(Chars) - 1; i >= 0; i-- ) {}				$\C{// 3}$
-for( Chars e = lowerBound(); e <= upperBound(); e = succ(e) ) {}	$\C{// 4}$
-for( Chars e = upperBound(); e >= lowerBound(); e = pred(e) ) {}	$\C{// 5}$
-\end{cfa}
-Loop (3) is a value underflow: when @i@ reaches to @0@, decrement statement will still execute and cause 
-the @unsigned int@ value @i@ wraps to @UINT_MAX@, which fails to loop test and the loop cannot terminate.
-
-In loop (4) and (5), when @e@ is at the @Bound@ (@upperBound@/@lowerBound@) and @succ@/@pred@ will result in @out of bounded@, \CFA 
-aborts its execution. Therefore, it is necessary to implement the condtional break within the loop body.
+
+A for-loop consists of loop control and body.
+The loop control is often a 3-tuple: initializers, stopping condition, and advancement.
+It is a common practice to declare one or more loop-index variables in initializers, checked these variables for stopping iteration, and updated the variables in advancement.
+Such a variable is called an \newterm{index} and is available for reading and writing within the loop body.
+(Some languages make the index read-only in the loop body.)
+This style of iteration can be written for an enumeration using functions from the @Bounded@ and @Serial@ traits:
+\begin{cfa}
+enum() E { A, B, C, D };
+for ( unsigned int i = 0; i < countof(E); i += 1 ) $\C{// (1)}$
+	sout | label( fromInt( i ) ) | nonl;
+sout | nl;
+for ( E e = lowerBound(); ; e = succ(e) ) {	$\C{// (2)}$
+	sout | label(e) | nonl;
+  if (e == upperBound()) break;
+}
+sout | nl;
+A B C D
+A B C D
+\end{cfa}
+
+A caveat in writing loop control using @pred@ and @succ@ is unintentionally exceeding the range.
+\begin{cfa}
+for ( E e = upperBound(); e >= lowerBound(); e = pred( e ) ) {}
+for ( E e = lowerBound(); e <= upperBound(); e = succ( e ) ) {}
+\end{cfa}
+Both of these loops look correct but fail because these is an additional bound check within the advancement \emph{before} the conditional test to stop the loop, resulting in a failure at the endpoints of the iteration.
+These loops must be restructured by moving the loop test to the end of the loop (@do-while@), as in loop (2) above, which is safe because an enumeration always at least one enumerator.
 
 
 \subsection{Range Loop}
-Instead of specifying condition, \CFA supports @range loops@, for which a user specifies a range of values. 
-\begin{cfa}[label=lst:range_functions_2]
-for ( Chars e; A ~= D ) { sout | label(e); }		$\C{// (6)}$
-for ( e; A ~= D ) { sout | label(e); }				$\C{// (7)}$
-for ( Chars e; A -~= D ) { sout | label(e); }		$\C{// (8) D C B A}$
-for ( e; A -~=D ~ 2 ) { sout | label(e); }		$\C{// (9) D B }$
-\end{cfa}
-Every range loop above has an index declaration, and a @range@ bounded by \newterm{left bound} @A@ and \newterm{right bound} @D@. 
-An index declaration can have an optional type declaration, without which \CFA 
-implicitly declares index variable to be the type of the bounds (@typeof(A)@). 
-If a range is joined by @~=@ (range up equal) operator, the index variable will be initialized by 
-the @left bound@, and change incrementally until its position exceeds @right bound@.
-On the other hand, if a range is defined with @-~=@ (range down equal) operation, the index variable will
-have the value of the @right bound@. It change decrementally until its position is less than the @left bound@. 
-A range can be suffixed by an positive integal \newterm{step}, joined by @~@. The loop @(9)@ declares a step size of 2 so that 
-e updates @pred(pred(e))@ in every iteration.
-
-\CFA manipulates the position of the index variable and breaks the loop if an index update can result in @out of range@. 
-
-\CFA provides a shorthand for range loop over a \CFA enumeration or a @Serial@:
-\begin{cfa}[label=lst:range_functions_2]
-for ( e; Chars ) { sout | label(e); }		$\C{// (10) A B C D}$
-for ( e; E ) {								$\C{// forall(E | CfaEnum(E) | Serial(E)) }$
-    sout | label(e);
-}
-\end{cfa}
-The shorthand syntax has a type name expression (@Char@ and @E@) as its range. If the range expression does not name 
-a \CFA enumeration or a @Serial@, \CFA reports a compile time error. When type name as range is a \CFA enumeration, 
-it turns into a loop that iterates all enumerators of the type. If the type name is a @Serial@, the index variable 
-will be initialized as the @lowerBound@. The loop control checks the index's position against the position of @upperBound@, 
-and terminate the loop when the index has a position greater than the @upperBound@. \CFA does not update the index with 
-@succ@ but manipulate its position directly to avoid @out of bound@.
+
+Instead of writing the traditional 3-tuple loop control, \CFA supports a \newterm{range loop}.
+\begin{cfa}
+for ( @E e; A ~= D@ ) { sout | label( e ) | nonl; } sout | nl;
+for ( @e; A ~= D@ ) { sout | label( e ) | nonl; } sout | nl;
+for ( @E e; A -~= D@ ) { sout | label( e ) | nonl; } sout | nl;
+for ( @e; A -~= D ~ 2@ ) { sout | label( e ) | nonl; } sout | nl;
+\end{cfa}
+Every range loop above has an index declaration and a @range@ bounded by \newterm{left bound} @A@ and \newterm{right bound} @D@.
+If the index declaration-type is omitted, the index type is the type of the lower bound (@typeof( A )@).
+If a range is joined by @~=@ (range up equal) operator, the index variable is initialized by the left bound and advanced by 1 until it is greater than the right bound.
+If a range is joined by @-~=@ (range down equal) operator, the index variable is initialized by the right bound and advanced by -1 until it is less than the left bound.
+(Note, functions @pred@ and @succ@ are not used for advancement, so the advancement problem does not occur.)
+A range can be suffixed by a positive \newterm{step}, \eg @~ 2@, so advancement is incremented/decremented by step.
+
+Finally, a shorthand for enumerating over the entire set of enumerators (the most common case) is using the enumeration type for the range.
+\begin{cfa}
+for ( e; @E@ ) sout | label( e ) | nonl; sout | nl; $\C{// A B C D}$
+for ( e; @-~= E@ ) sout | label( e ) | nonl; sout | nl; $\C{// D C B A}$
+\end{cfa}
+For a \CFA enumeration, the loop enumerates over all enumerators of the enumeration.
+For a type matching the @Serial@ trait: the index variable is initialized to @lowerBound@ and loop control checks the index's value for greater than the @upperBound@.
+If the range type is not a \CFA enumeration or does not match trait @Serial@, it is compile-time error.
+
 
 \section{Overload Operators}
-% Finally, there is an associated trait defining comparison operators among enumerators. 
-\CFA preemptively overloads comparison operators for \CFA enumeration with @Serial@ and @CfaEnum@. 
-They defines that two enumerators are equal only if the are the same enumerator, and compartors are 
-define for order comparison.
-\begin{cfa}
-forall( E | CfaEnum( E ) | Serial( E ) ) {
+
+\CFA overloads the comparison operators for \CFA enumeration satisfying traits @Serial@ and @CfaEnum@.
+These definitions require the operand types be the same and the appropriate comparison is made using the the positions of the operands.
+\begin{cfa}
+forall( E | CfaEnum( E ) | Serial( E ) ) @{@ $\C{// distribution block}$
 	// comparison
 	int ?==?( E l, E r ); 		$\C{// true if l and r are same enumerators}$
@@ -283,12 +281,13 @@
 	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}
-
-\CFA implements few arithmetic operators for @CfaEnum@. Unlike update functions in @Serial@, these 
-operator does not have bound checks, which rely on @upperBound@ and @lowerBound@. These operators directly manipulate 
-position, the underlying representation of a \CFA enumeration.
-\begin{cfa}
-forall( E | CfaEnum( E ) | Serial( E ) ) {
+@}@
+\end{cfa}
+(Note, all the function prototypes are wrapped in a distribution block, where all qualifiers preceding the block are distributed to each declaration with the block, which eliminated tedious repeated qualification.
+Distribution blocks can be nested.)
+
+\CFA implements a few arithmetic operators for @CfaEnum@.
+Unlike advancement functions in @Serial@, these operators perform direct arithmetic, so there is no implicit bound checks.
+\begin{cfa}
+forall( E | CfaEnum( E ) | Serial( E ) ) { $\C{// distribution block}$
 	// comparison
 	E ++?( E & l );
@@ -303,105 +302,11 @@
 \end{cfa}
 
-Lastly, \CFA does not define @zero_t@ for \CFA enumeration. Users can define the boolean false for 
-\CFA enumerations on their own. Here is an example:
-\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 false and true 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{Iteration and Range}
-
-
-
-% % It is convenient to iterate over a \CFA enumeration value, \eg:
-% \CFA implements \newterm{range loop} for \CFA enumeration using the enumerated traits. The most basic form of @range loop@ is the follows:
-% \begin{cfa}[label=lst:range_functions]
-% for ( Alphabet alph; Alphabet ) { sout | alph; }
-% >>> A B C ... D
-% \end{cfa}
-% % The @range loops@ iterates through all enumerators in the order defined in the enumeration.
-% % @alph@ is the iterating enumeration object, which returns the value of an @Alphabet@ in this context according to the precedence rule.
-% Enumerated @range loop@ extends the \CFA grammar as it allows a type name @Alphabet@ 
-
-% \textbullet\ \CFA offers a shorthand for iterating all enumeration constants:
-% \begin{cfa}[label=lst:range_functions]
-% for ( Alphabet alph ) { sout | alph; }
-% >>> A B C ... D
-% \end{cfa}
-
-% The following are examples for constructing for-control using an enumeration. Note that the type declaration of the iterating variable is optional, because \CFA can infer the type as EnumInstType based on the range expression, and possibly convert it to one of its attribute types.
-
-% \textbullet\ H is implicit up-to exclusive range [0, H).
-% \begin{cfa}[label=lst:range_function_1]
-% for ( alph; Alphabet.D ) { sout | alph; }
-% >>> A B C
-% \end{cfa}
-
-% \textbullet\ ~= H is implicit up-to inclusive range [0,H].
-% \begin{cfa}[label=lst:range_function_2]
-% for ( alph; ~= Alphabet.D ) { sout | alph; }
-% >>> A B C D
-% \end{cfa}
-
-% \textbullet\ L ~ H is explicit up-to exclusive range [L,H).
-% \begin{cfa}[label=lst:range_function_3]
-% for ( alph; Alphabet.B ~ Alphabet.D  ) { sout | alph; }
-% // for ( Alphabet alph = Alphabet.B; alph < Alphabet.D; alph += 1  ); 1 is one_t
-% >>> B C
-% \end{cfa}
-
-% \textbullet\ L ~= H is explicit up-to inclusive range [L,H].
-% \begin{cfa}[label=lst:range_function_4]
-% for ( alph; Alphabet.B ~= Alphabet.D  ) { sout | alph; }
-% >>> B C D
-% \end{cfa}
-
-% \textbullet\ L -~ H is explicit down-to exclusive range [H,L), where L and H are implicitly interchanged to make the range down-to.
-% \begin{cfa}[label=lst:range_function_5]
-% for ( alph; Alphabet.D -~ Alphabet.B  ) { sout | alph; }
-% >>> D C
-% \end{cfa}
-
-% \textbullet\ L -~= H is explicit down-to exclusive range [H,L], where L and H are implicitly interchanged to make the range down-to.
-% \begin{cfa}[label=lst:range_function_6]
-% for ( alph; Alphabet.D -~= Alphabet.B  ) { sout | alph; }
-% >>> D C B
-% \end{cfa}
-
-% A user can specify the ``step size'' of an iteration. There are two different stepping schemes of enumeration for-loop.
-% \begin{cfa}[label=lst:range_function_stepping]
-% enum(int) Sequence { A = 10, B = 12, C = 14, D = 16, D  = 18 };
-% for ( s; Sequence.A ~= Sequence.D ~ 1  ) { sout | alph; }
-% >>> 10 12 14 16 18
-% for ( s; Sequence.A ~= Sequence.D; s+=1  ) { sout | alph; }
-% >>> 10 11 12 13 14 15 16 17 18
-% \end{cfa}
-% The first syntax is stepping to the next enumeration constant, which is the default stepping scheme if not explicitly specified. The second syntax, on the other hand, is to call @operator+=@ @one_type@ on the @value( s )@. Therefore, the second syntax is equivalent to
-% \begin{cfa}[label=lst:range_function_stepping_converted]
-% for ( typeof( value(Sequence.A) ) s=value( Sequence.A ); s <= Sequence.D; s+=1  ) { sout | alph; }
-% >>> 10 11 12 13 14 15 16 17 18
-% \end{cfa}
-
-% % \PAB{Explain what each loop does.}
-
-% It is also possible to iterate over an enumeration's labels, implicitly or explicitly:
-% \begin{cfa}[label=lst:range_functions_label_implicit]
-% for ( char * alph; Alphabet )
-% \end{cfa}
-% This for-loop implicitly iterates every label of the enumeration, because a label is the only valid resolution to @ch@ with type @char *@ in this case.
-% If the value can also be resolved as the @char *@, you might iterate the labels explicitly with the array iteration.
-% \begin{cfa}[label=lst:range_functions_label_implicit]
-% for ( char * ch; labels( Alphabet ) )
-% \end{cfa}
+Lastly, \CFA does not define @zero_t@ for \CFA enumeration.
+Users can define the boolean @false@ for \CFA enumerations on their own, \eg:
+\begin{cfa}
+forall( E | CfaEnum( E ) )
+int ?!=?( E lhs, zero_t ) {
+	return posn( lhs ) != 0;
+}
+\end{cfa}
+which effectively turns the first enumeration to a logical @false@ and @true@ for the others.
