Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 175a750ee58bd5b20d6b22913979e43b42ecad4c)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 0bda8d707434c296565beb1edaff2d377450550c)
@@ -136,6 +136,6 @@
 \section{Implementation}
 
-\CFA-cc is is a transpiler translating \CFA code into C, which is compiled by a C compiler.
-During transpilation, \CFA-cc breaks a \CFA enumeration definition into a definition of a C enumeration with the same name and auxiliary arrays: a label and value array for a typed enumeration.
+\CFA-cc is a transpiler translating \CFA code into C, which is compiled by a C compiler.
+During transpiling, \CFA-cc breaks a \CFA enumeration definition into a definition of a C enumeration with the same name and auxiliary arrays: a label and value array for a typed enumeration.
 For example:
 \begin{cfa}
@@ -157,7 +157,7 @@
 Therefore, a \CFA enumeration variable has the same underlying representation as its generated C enumeration.
 This semantics implies a \CFA enumeration variable uses the same storage as a C enumeration variable, that @posn@ can use as its underlying representation, and the label and value arrays take little storage.
-It should be possible to eliminated the two arrays if unused, either by \CFA if local to a translation unit and unused, or by the linker if global but unreferenced.
+It should be possible to eliminate the two arrays if unused, either by \CFA if local to a translation unit and unused, or by the linker if global but unreferenced.
 Also, the label and value arrays are declared @static@ and initialized with constants, so the arrays are allocated in the @.data@ section and initialized before program execution.
-Hence, there is no addition execution cost unless new enumeration features are use, and storage usage is minimal as the number of enumerations in a program is small as is the number of enumerators in an enumeration.
+Hence, there is no additional execution cost unless new enumeration features are used, and storage usage is minimal as the number of enumerations in a program is small as is the number of enumerators in an enumeration.
 
 Along with the enumeration definition, \CFA-cc generates definitions of the attribute functions, @posn@, @label@ and @value@, for each enumeration:
@@ -171,5 +171,5 @@
 Note, the cast to @int@ is actually an internal reinterpreted cast added before type resolution to stop further reduction on the expression by the type resolver \see{\VRef{s:ValueConversion}} and removed in code generation.
 Finally, to further mitigate \CFA enumeration costs, calls to @label@ and @value@ with an enumeration constant are unrolled into the appropriate constant expression, although this could be left to the backend C compiler.
-Hence, in space and time costs, \CFA enumerations follow the C philosophy of only paying for what is used, modulo some future work to convince the linker to remove unaccessed @label@ and @value@ arrays, possibly with @weak@ attributes.
+Hence, in space and time costs, \CFA enumerations follow the C philosophy of only paying for what is used, modulo some future work to convince the linker to remove un-accessed @label@ and @value@ arrays, possibly with @weak@ attributes.
 
 
@@ -258,5 +258,5 @@
 \label{s:CFAInheritance}
 
-\CFA Plan-9 inheritance may be used with \CFA enumerations, where Plan-9 inheritance is containment inheritance with implicit unscoping (like a nested unnamed @struct@/@union@ in C).
+\CFA Plan-9 inheritance may be used with \CFA enumerations, where Plan-9 inheritance is containment inheritance with implicit un-scoping (like a nested unnamed @struct@/@union@ in C).
 Containment is nominative: an enumeration inherits all enumerators from another enumeration by declaring an @inline statement@ in its enumerator lists.
 \begin{cfa}
@@ -280,5 +280,5 @@
 The base type must be consistent between subtype and supertype.
 When an enumeration inherits enumerators from another enumeration, it copies the enumerators' @value@ and @label@, even if the @value@ is auto-initialized.
-However, the position of the underlying representation is the order of the enumerator in the new enumeration.
+However, the underlying representation's position is the enumerator's order in the new enumeration.
 \begin{cfa}
 enum() E1 { B };									$\C{// B}$
@@ -287,5 +287,5 @@
 enum() E4 { A, inline E3, F};			$\C{// A {\color{blue}[\(_{E3}\)} {\color{red}[\(_{E1}\)} B {\color{red}]} {\color{red}[\(_{E2}\)} C D {\color{red}]} E {\color{blue}]} F}$
 \end{cfa}
-In the example, @B@ is at position 0 in @E1@ and @E3@, but position 1 in @E4@ as @A@ takes position 0 in @E4@.
+In this example, @B@ is at position 0 in @E1@ and @E3@, but position 1 in @E4@ as @A@ takes position 0 in @E4@.
 @C@ is at position 0 in @E2@, 1 in @E3@, and 2 in @E4@.
 @D@ is at position 1 in @E2@, 2 in @E3@, and 3 in @E4@.
@@ -331,5 +331,5 @@
 
 As discussed in \VRef{s:OpaqueEnum}, \CFA chooses position as a representation of a \CFA enumeration variable.
-When a cast or implicit conversion moves an enumeration from subtype to supertype, the position can be unchanged or increase.
+When a cast or implicit conversion moves an enumeration from subtype to supertype, the position can be unchanged or increased.
 \CFA determines the position offset with an \newterm{offset calculation} function.
 
@@ -368,5 +368,5 @@
 The algorithm iterates over the members in @dst@ to find @src@.
 If a member is an enumerator of @dst@, the positions of all subsequent members are incremented by one.
-If the current member is @dst@, the function returns true indicating \emph{found} and the accumulated offset.
+If the current member is @dst@, the function returns true, indicating \emph{found} and the accumulated offset.
 Otherwise, the algorithm recurses into the current @CFAEnum@ @m@ to check if its @src@ is convertible to @m@.
 If @src@ is convertible to the current member @m@, this means @src@ is a subtype-of-subtype of @dst@.
@@ -378,8 +378,8 @@
 \section{Control Structures}
 
-Enumerators can be used in multiple contexts.
+Enumerators are used in various contexts.
 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 intuition assumes an implicit conversion to position.
+However, in some contexts, enumerator synonyms and typed enumerations make this implicit conversion to value incorrect.
+A programmer's intuition assumes an implicit conversion to position in these contexts.
 
 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.
@@ -442,5 +442,5 @@
 \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 @+~=@.
+The prefix @+~=@ or @-~=@ iterate forward or backward 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''.
@@ -449,5 +449,5 @@
 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.
+This idiom extends to enumerations because there is a boolean conversion regarding 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.
@@ -482,5 +482,5 @@
 \end{cfa}
 \footnotetext{C uses symbol \lstinline{'='} for designator initialization, but \CFA changes it to \lstinline{':'} 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.
+This approach is also necessary for a predefined typed enumeration (unchangeable) when additional secondary information needs to be added.
 The array subscript operator, namely @?[?]@, is overloaded so that when a \CFA enumerator is used as an array index, it implicitly converts to its position over value to sustain data harmonization.
 This behaviour can be reverted by explicit overloading:
Index: doc/theses/jiada_liang_MMath/Cenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/Cenum.tex	(revision 175a750ee58bd5b20d6b22913979e43b42ecad4c)
+++ doc/theses/jiada_liang_MMath/Cenum.tex	(revision 0bda8d707434c296565beb1edaff2d377450550c)
@@ -3,5 +3,5 @@
 \CFA supports legacy C enumeration using the same syntax for backward compatibility.
 A C-style enumeration in \CFA is called a \newterm{C Enum}.
-The semantics of the C Enum is mostly consistent with C with some restrictions.
+The semantics of the C Enum are mostly consistent with C with some restrictions.
 The following sections detail all of my new contributions to enumerations in C.
 
@@ -52,5 +52,5 @@
 enum RGB @!@ { Red, Green, Blue };
 \end{cfa}
-Now the enumerators \emph{must} be qualified with the associated enumeration type.
+Now, the enumerators \emph{must} be qualified with the associated enumeration type.
 \begin{cfa}
 Week week = @Week.@Mon;
Index: doc/theses/jiada_liang_MMath/relatedwork.tex
===================================================================
--- doc/theses/jiada_liang_MMath/relatedwork.tex	(revision 175a750ee58bd5b20d6b22913979e43b42ecad4c)
+++ doc/theses/jiada_liang_MMath/relatedwork.tex	(revision 0bda8d707434c296565beb1edaff2d377450550c)
@@ -497,7 +497,6 @@
 
 To indirectly enumerate, \Csharp's Enum library provides @Enum.GetValues@, 
-% a pseudo-method that retrieves an array of the enumeration constants for looping over an enumeration type or variable (expensive operation).
 a static member of abstract Enum type that return a reference to an array of all enumeration constants.
-Internally, a Enum type has a static member called @fieldInfoHash@ -- a @Hashtable@ that stores enumerators information.
+Internally, an Enum type has a static member called @fieldInfoHash@ -- a @Hashtable@ that stores information about enumerators.
 The field is populated on-demand: it only contains information if a @reflection@ like @GetValues@ is called.
 As an optimization, this information is cached, so the cost of reflection is paid once throughout the lifetime of a program.
@@ -539,5 +538,5 @@
 const V = 3.1;  const W = 3.1;
 \end{Go}
-Since these declarations are immutable variables, they are unscoped and Go has no overloading. If no type declaration provided, Go infers 
+These declarations defined immutable and unscoped variables, and Go has no naming overloading. If no type declaration is provided, Go infers 
 type from the initializer expression.
 
@@ -552,5 +551,5 @@
 subsequent identifiers can be implicitly or explicitly initialized.
 Implicit initialization always uses the \emph{previous} (predecessor) constant expression initializer.
-A constant block can still use explicit declarations, and following constants inherit that type.
+A constant block can still use explicit declarations, and the following constants inherit that type.
 \begin{Go}
 type BigInt int64
@@ -559,6 +558,6 @@
 const ( S @int@ = 0; T; USA @string@ = "USA"; U; V @float32@ = 3.1; W )
 \end{Go}
-Typing the first constant and implicit initializing is still not a enumeration because there is no unique type for the constant block;
-nothing stops other constant blocks from having the same type. 
+Typing the first constant and implicit initializing is still not an enumeration because there is no unique type for the constant block;
+Nothing stops other constant blocks from being of the same type. 
 
 Each @const@ declaration provides an implicit \emph{compile-time} integer counter starting at @0@, called \lstinline[language=Go]{iota}, which is post-incremented after each constant declaration.
@@ -643,5 +642,5 @@
 Week day = Week.Sat;
 \end{Java}
-The enumerator's members are scoped requiring qualification.
+The enumerator's members are scoped, requiring qualification.
 The value of an enumeration instance is restricted to its enumerators.
 
@@ -722,5 +721,5 @@
 @EnumSet@ is enumerable because it extends @AbstractSet@ interfaces and thus supports direct enumerating via @forEach@.
 It also has subset operation @range@ and it is possible to add to and remove from members of the set. 
-@EnumSet@ supports more enumeration features, but it is not an enumeration type: it is a set of enumerators from a pre-define enum. 
+@EnumSet@ supports more enumeration features, but it is not an enumeration type; it is a set of enumerators from a pre-defined enum. 
 
 An enumeration type cannot declare an array dimension nor can an enumerator be used as a subscript.
@@ -841,5 +840,5 @@
 % However, there is no mechanism to iterate through an enumeration without casting to integral and positions versus values is not handled.
 Like C/\CC, there is no mechanism to iterate through an enumeration.
-It can only be approximated by a loop over a range of enumerator and only works if the enumerator values are a sequence of natural numbers.
+It can only be approximated by a loop over a range of enumerators and only works if the enumerator values are a sequence of natural numbers.
 \begin{c++}
 for d in Week::Mon as isize ..= Week::Sun as isize {
@@ -913,5 +912,5 @@
 % for integral types, there is auto-incrementing.
 As well, it is possible to type associated values of enumeration cases with a common type. 
-When enumeration cases are typed with a common integral type, Swift auto-initialize enumeration cases following the same initialization scheme as C language.
+When enumeration cases are typed with a common integral type, Swift auto-initializes enumeration cases following the same initialization scheme as C language.
 If an enumeration is typed with @string@, its cases are auto-initialized to case names (labels).
 \begin{cquote}
@@ -965,5 +964,5 @@
 \end{cquote}
 Enumerating is accomplished by inheriting from @CaseIterable@ protocol, which has a static @enum.@ @allCases@ property that returns a collection of all the cases for looping over an enumeration type or variable.
-Like \CFA, Swift's default enumerator output is the case name (label). An enumerator of a typed enumeration has attribute 
+Like \CFA, Swift's default enumerator output is the case name (label). An enumerator of a typed enumeration has an attribute 
 @rawValue@ that return its case value.
 \begin{swift}
@@ -1015,5 +1014,5 @@
 % Conversion from @rawValue@ to enumerator may fail (bad lookup), so the result is an optional value.
 In the previous example, the initialization of @opt@ fails if there is no enumeration value equal to 0, resulting in a @nil@ value.
-Initialization from a raw value is considered a expensive operation because it requires a value lookup.
+Initialization from a raw value is considered an expensive operation because it requires a value lookup.
 
 
@@ -1040,5 +1039,5 @@
 Mon : 1 Tue : 2 Wed : 3 Thu : 10 Fri : !11! Sat : 4 Sun : !12!
 \end{python}
-@auto@ is controlled by member @_generate_next_value_()@, which by default return one plus the highest value among enumerators, and can be overridden:
+@auto@ is controlled by member @_generate_next_value_()@, which by default returns one plus the highest value among enumerators, and can be overridden:
 \begin{python}
 @staticmethod
@@ -1061,5 +1060,5 @@
 it is not an ADT because the enumerator names are not constructors.
 
-An enumerator initialized with the same value is an alias and invisible at the enumeration level, \ie the alias is substituted for its aliasee.
+An enumerator initialized with the same value is an alias and invisible at the enumeration level, \ie the alias is substituted for its aliases.
 \begin{python}
 class WeekD(Enum): Mon = 1; Tue = 2; Wed = 3; Thu = !10!; Fri = !10!; Sat = !10!; Sun = !10!
Index: doc/theses/jiada_liang_MMath/trait.tex
===================================================================
--- doc/theses/jiada_liang_MMath/trait.tex	(revision 175a750ee58bd5b20d6b22913979e43b42ecad4c)
+++ doc/theses/jiada_liang_MMath/trait.tex	(revision 0bda8d707434c296565beb1edaff2d377450550c)
@@ -18,6 +18,6 @@
 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 @std::is_enum@ and other \CC @traits@ are 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 assertions 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.
@@ -35,5 +35,5 @@
 \end{cfa}
 \newpage
-Trait @CfaEnum@ defines attribute functions @label@ and @posn@ for all \CFA enumerations, and internally \CFA enumerations fulfills this assertion.
+Trait @CfaEnum@ defines attribute functions @label@ and @posn@ for all \CFA enumerations, and internally \CFA enumerations fulfill this assertion.
 \begin{cfa}
 forall( E ) trait CfaEnum {
@@ -55,6 +55,6 @@
 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.
+The trait for @format_enum@ requires a function named @str@ to print the value (payload) of the enumerator.
+Hence, enumeration defines how its value appears, and @format_enum@ displays this value within the label name.
 
 \begin{figure}
@@ -113,10 +113,10 @@
 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.
+Hence, the @concept@ is the 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.
+Hence, the \CFA enumeration traits are never connected with the specific @enum@ kind.
 Instead, anything that can look like the @enum@ kind is considered an enumeration (static structural typing).
 However, Scala, Go, and Rust traits are nominative: a type explicitly declares a named trait to be of its type, while in \CFA, any type implementing all requirements declared in a trait implicitly satisfy its restrictions.
@@ -144,5 +144,5 @@
 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.
+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 side 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}
@@ -177,8 +177,8 @@
 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@.
+Function @Countof@ is the generic counterpart to the built-in 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.
+@Countof@ works on 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.
@@ -197,9 +197,9 @@
 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@.
+If type @E@ exists, replace 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 Look for a name @A@ in the lexical context with the type @E@.
+If the name @A@ exists, replace @countof( A )@ with a function call @Countof( E )@.
 \item If 1-4 fail, report a type error on expression @countof( E )@.
 \end{enumerate}
@@ -209,5 +209,5 @@
 
 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.
+\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 transitions to @while@ loop.
 
 
@@ -216,5 +216,5 @@
 A for-loop consists of loop control and body.
 The loop control is often a 3-tuple: initializers, looping condition, and advancement.
-It is a common practice to declare one or more loop-index variables in initializers, determines whether the variables satisfy the loop condition, and update the variables in advancement.
+It is a common practice to declare one or more loop-index variables in initializers,  whether the variables satisfy the loop condition, and update 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.)
@@ -239,5 +239,5 @@
 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.
+Both of these loops look correct but fail because there 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 has at least one enumerator.
 
@@ -272,5 +272,5 @@
 
 \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.
+These definitions require the operand types to 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}$
@@ -284,10 +284,10 @@
 @}@
 \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.
+(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 eliminates 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.
-Bound checks are added to these operations to ensure the outputs fulfills the @Bounded@ invariant.
+Bound checks are added to these operations to ensure the outputs fulfill the @Bounded@ invariant.
 \begin{cfa}
 forall( E | CfaEnum( E ) | Serial( E ) ) { $\C{// distribution block}$
@@ -312,3 +312,3 @@
 }
 \end{cfa}
-which effectively turns the first enumeration to a logical @false@ and @true@ for the others.
+which effectively turns the first enumeration into a logical @false@ and @true@ for the others.