Index: doc/theses/andrew_beach_MMath/features.tex
===================================================================
--- doc/theses/andrew_beach_MMath/features.tex	(revision de47a9d90448b4a9998ca306ff8576f8cd4f3369)
+++ doc/theses/andrew_beach_MMath/features.tex	(revision f6106a6aba16b040f4f86fe37774493e2d88df68)
@@ -3,4 +3,8 @@
 This chapter covers the design and user interface of the \CFA
 exception-handling mechanism (EHM). % or exception system.
+
+We will begin with an overview of EHMs in general. It is not a strict
+definition of all EHMs nor an exaustive list of all possible features.
+However it does cover the most common structure and features found in them.
 
 % We should cover what is an exception handling mechanism and what is an
@@ -9,61 +13,75 @@
 \paragraph{Raise / Handle}
 An exception operation has two main parts: raise and handle.
-These are the two parts that the user will write themselves and so
-might be the only two pieces of the EHM that have any syntax.
 These terms are sometimes also known as throw and catch but this work uses
 throw/catch as a particular kind of raise/handle.
+These are the two parts that the user will write themselves and may
+be the only two pieces of the EHM that have any syntax in the language.
 
 \subparagraph{Raise}
-The raise is the starting point for exception handling and usually how
-Some well known examples include the throw statements of \Cpp and Java and
-the raise statement from Python.
-
-For this overview a raise does nothing more kick off the handling of an
-exception, which is called raising the exception. This is inexact but close
-enough for the broad strokes of the overview.
+The raise is the starting point for exception handling. It marks the beginning
+of exception handling by \newterm{raising} an excepion, which passes it to
+the EHM.
+
+Some well known examples include the @throw@ statements of \Cpp and Java and
+the \codePy{raise} statement from Python. In real systems a raise may preform
+some other work (such as memory management) but for the purposes of this
+overview that can be ignored.
 
 \subparagraph{Handle}
-The purpose of most exception operations is to run some sort of handler that
-contains user code.
-The try statement of \Cpp illistrates the common features
-Handlers have three common features: a region of code they apply to, an
-exception label that describes what exceptions they handle and code to run
-when they handle an exception.
-Each handler can handle exceptions raised in that region that match their
-exception label. Different EHMs will have different rules to pick a handler
+The purpose of most exception operations is to run some user code to handle
+that exception. This code is given, with some other information, in a handler.
+
+A handler has three common features: the previously mentioned user code, a
+region of code they cover and an exception label/condition that matches
+certain exceptions.
+Only raises inside the covered region and raising exceptions that match the
+label can be handled by a given handler.
+Different EHMs will have different rules to pick a handler
 if multipe handlers could be used such as ``best match" or ``first found".
+
+The @try@ statements of \Cpp, Java and Python are common examples. All three
+also show another common feature of handlers, they are grouped by the covered
+region.
 
 \paragraph{Propagation}
 After an exception is raised comes what is usually the biggest step for the
-EHM, finding and setting up the handler. This can be broken up into three
-different tasks: searching for a handler, matching against the handler and
-installing the handler.
-
-First the EHM must search for possible handlers that could be used to handle
+EHM: finding and setting up the handler. The propogation from raise to
+handler can be broken up into three different tasks: searching for a handler,
+matching against the handler and installing the handler.
+
+\subparagraph{Searching}
+The EHM begins by searching for handlers that might be used to handle
 the exception. Searching is usually independent of the exception that was
-thrown and instead depends on the call stack, the current function, its caller
-and repeating down the stack.
-
-Second it much match the exception with each handler to see which one is the
-best match and hence which one should be used to handle the exception.
-In languages where the best match is the first match these two are often
-intertwined, a match check is preformed immediately after the search finds
+thrown as it looks for handlers that have the raise site in their covered
+region.
+This includes handlers in the current function, as well as any in callers
+on the stack that have the function call in their covered region.
+
+\subparagraph{Matching}
+Each handler found has to be matched with the raised exception. The exception
+label defines a condition that be use used with exception and decides if
+there is a match or not.
+
+In languages where the first match is used this step is intertwined with
+searching, a match check is preformed immediately after the search finds
 a possible handler.
 
-Third, after a handler is chosen it must be made ready to run.
-What this actually involves can vary widely to fit with the rest of the
+\subparagraph{Installing}
+After a handler is chosen it must be made ready to run.
+The implementation can vary widely to fit with the rest of the
 design of the EHM. The installation step might be trivial or it could be
 the most expensive step in handling an exception. The latter tends to be the
 case when stack unwinding is involved.
 
-As an alternate third step if no appropriate handler is found then some sort
-of recovery has to be preformed. This is only required with unchecked
-exceptions as checked exceptions can promise that a handler is found. It also
-is also installing a handler but it is a special default that may be
-installed differently.
+If a matching handler is not guarantied to be found the EHM will need a
+different course of action here in the cases where no handler matches.
+This is only required with unchecked exceptions as checked exceptions
+(such as in Java) can make than guaranty.
+This different action can also be installing a handler but it is usually an
+implicat and much more general one.
 
 \subparagraph{Hierarchy}
-In \CFA the EHM uses a hierarchial system to organise its exceptions.
-This stratagy is borrowed from object-orientated languages where the
+A common way to organize exceptions is in a hierarchical structure.
+This is especially true in object-orientated languages where the
 exception hierarchy is a natural extension of the object hierarchy.
 
@@ -88,5 +106,5 @@
 A handler labelled with any given exception can handle exceptions of that
 type or any child type of that exception. The root of the exception hierarchy
-(here \texttt{exception}) acts as a catch-all, leaf types catch single types
+(here \codeC{exception}) acts as a catch-all, leaf types catch single types
 and the exceptions in the middle can be used to catch different groups of
 related exceptions.
@@ -94,6 +112,7 @@
 This system has some notable advantages, such as multiple levels of grouping,
 the ability for libraries to add new exception types and the isolation
-between different sub-hierarchies. So the design was adapted for a
-non-object-orientated language.
+between different sub-hierarchies.
+This design is used in \CFA even though it is not a object-orientated
+language using different tools to create the hierarchy.
 
 % Could I cite the rational for the Python IO exception rework?
@@ -101,33 +120,29 @@
 \paragraph{Completion}
 After the handler has finished the entire exception operation has to complete
-and continue executing somewhere else. This step is usually very simple
-both logically and in its implementation as the installation of the handler
-usually does the heavy lifting.
-
-The EHM can return control to many different places.
-However, the most common is after the handler definition and the next most
-common is after the raise.
+and continue executing somewhere else. This step is usually simple,
+both logically and in its implementation, as the installation of the handler
+is usually set up to do most of the work.
+
+The EHM can return control to many different places,
+the most common are after the handler definition and after the raise.
 
 \paragraph{Communication}
-For effective exception handling, additional information is usually required
-as this base model only communicates the exception's identity. Common
-additional methods of communication are putting fields on an exception and
-allowing a handler to access the lexical scope it is defined in (usually
-a function's local variables).
-
-\paragraph{Other Features}
-Any given exception handling mechanism is free at add other features on top
-of this. This is an overview of the base that all EHMs use but it is not an
-exaustive list of everything an EHM can do.
+For effective exception handling, additional information is usually passed
+from the raise to the handler.
+So far only communication of the exceptions' identity has been covered.
+A common method is putting fields into the exception instance and giving the
+handler access to them.
 
 \section{Virtuals}
-Virtual types and casts are not part of the exception system nor are they
-required for an exception system. But an object-oriented style hierarchy is a
-great way of organizing exceptions so a minimal virtual system has been added
-to \CFA.
+Virtual types and casts are not part of \CFA's EHM nor are they required for
+any EHM. But \CFA uses a hierarchial system of exceptions and this feature
+is leveraged to create that.
+
+% Maybe talk about why the virtual system is so minimal.
+% Created for but not a part of the exception system.
 
 The virtual system supports multiple ``trees" of types. Each tree is
 a simple hierarchy with a single root type. Each type in a tree has exactly
-one parent - except for the root type which has zero parents - and any
+one parent -- except for the root type which has zero parents -- and any
 number of children.
 Any type that belongs to any of these trees is called a virtual type.
@@ -139,30 +154,33 @@
 Every virtual type also has a list of virtual members. Children inherit
 their parent's list of virtual members but may add new members to it.
-It is important to note that these are virtual members, not virtual methods.
-However as function pointers are allowed they can be used to mimic virtual
-methods as well.
-
-The unique id for the virtual type and all the virtual members are combined
+It is important to note that these are virtual members, not virtual methods
+of object-orientated programming, and can be of any type.
+However, since \CFA has function pointers and they are allowed, virtual
+members can be used to mimic virtual methods.
+
+Each virtual type has a unique id.
+This unique id and all the virtual members are combined
 into a virtual table type. Each virtual type has a pointer to a virtual table
 as a hidden field.
 
-Up until this point the virtual system is a lot like ones found in object-
-orientated languages but this where they diverge. Objects encapsulate a
+Up until this point the virtual system is similar to ones found in
+object-orientated languages but this where \CFA diverges. Objects encapsulate a
 single set of behaviours in each type, universally across the entire program,
 and indeed all programs that use that type definition. In this sense the
 types are ``closed" and cannot be altered.
 
-However in \CFA types do not encapsulate any behaviour. Traits are local and
+In \CFA types do not encapsulate any behaviour. Traits are local and
 types can begin to statify a trait, stop satifying a trait or satify the same
-trait in a different way with each new definition. In this sense they are
-``open" as they can change at any time. This means it is implossible to pick
-a single set of functions that repersent the type.
-
-So we don't try to have a single value. The user can define virtual tables
-which are filled in at their declaration and given a name. Anywhere you can
-see that name you can use that virtual table; even if it is defined locally
-inside a function, although in that case you must respect its lifetime.
-
-An object of a virtual type is ``bound" to a virtual table instance which
+trait in a different way at any lexical location in the program.
+In this sense they are ``open" as they can change at any time. This means it
+is implossible to pick a single set of functions that repersent the type's
+implementation across the program.
+
+\CFA side-steps this issue by not having a single virtual table for each
+type. A user can define virtual tables which are filled in at their
+declaration and given a name. Anywhere that name is visible, even if it was
+defined locally inside a function (although that means it will not have a
+static lifetime), it can be used.
+Specifically, a virtual type is ``bound" to a virtual table which
 sets the virtual members for that object. The virtual members can be accessed
 through the object.
@@ -196,9 +214,11 @@
 \end{cfa}
 The trait is defined over two types, the exception type and the virtual table
-type. This should be one-to-one, each exception type has only one virtual
+type. This should be one-to-one: each exception type has only one virtual
 table type and vice versa. The only assertion in the trait is
 @get_exception_vtable@, which takes a pointer of the exception type and
 returns a reference to the virtual table type instance.
 
+% TODO: This section, and all references to get_exception_vtable, are
+% out-of-data. Perhaps wait until the update is finished before rewriting it.
 The function @get_exception_vtable@ is actually a constant function.
 Regardless of the value passed in (including the null pointer) it should
@@ -214,7 +234,5 @@
 % similar system I know of (except Agda's I guess) so I took it out.
 
-There are two more traits for exceptions @is_termination_exception@ and
-@is_resumption_exception@. They are defined as follows:
-
+There are two more traits for exceptions defined as follows:
 \begin{cfa}
 trait is_termination_exception(
@@ -228,24 +246,22 @@
 };
 \end{cfa}
-
-In other words they make sure that a given type and virtual type is an
-exception and defines one of the two default handlers. These default handlers
-are used in the main exception handling operations \see{Exception Handling}
-and their use will be detailed there.
-
-However all three of these traits can be tricky to use directly.
-There is a bit of repetition required but
+Both traits ensure a pair of types are an exception type and its virtual table
+and defines one of the two default handlers. The default handlers are used
+as fallbacks and are discussed in detail in \VRef{s:ExceptionHandling}.
+
+However, all three of these traits can be tricky to use directly.
+While there is a bit of repetition required,
 the largest issue is that the virtual table type is mangled and not in a user
-facing way. So there are three macros that can be used to wrap these traits
-when you need to refer to the names:
+facing way. So these three macros are provided to wrap these traits to
+simplify referring to the names:
 @IS_EXCEPTION@, @IS_TERMINATION_EXCEPTION@ and @IS_RESUMPTION_EXCEPTION@.
 
-All take one or two arguments. The first argument is the name of the
-exception type. Its unmangled and mangled form are passed to the trait.
+All three take one or two arguments. The first argument is the name of the
+exception type. The macro passes its unmangled and mangled form to the trait.
 The second (optional) argument is a parenthesized list of polymorphic
-arguments. This argument should only with polymorphic exceptions and the
-list will be passed to both types.
-In the current set-up the base name and the polymorphic arguments have to
-match so these macros can be used without losing flexibility.
+arguments. This argument is only used with polymorphic exceptions and the
+list is be passed to both types.
+In the current set-up, the two types always have the same polymorphic
+arguments so these macros can be used without losing flexibility.
 
 For example consider a function that is polymorphic over types that have a
@@ -257,50 +273,56 @@
 
 \section{Exception Handling}
-\CFA provides two kinds of exception handling, termination and resumption.
-These twin operations are the core of the exception handling mechanism and
-are the reason for the features of exceptions.
+\label{s:ExceptionHandling}
+\CFA provides two kinds of exception handling: termination and resumption.
+These twin operations are the core of \CFA's exception handling mechanism.
 This section will cover the general patterns shared by the two operations and
 then go on to cover the details each individual operation.
 
-Both operations follow the same set of steps to do their operation. They both
-start with the user preforming a throw on an exception.
-Then there is the search for a handler, if one is found than the exception
-is caught and the handler is run. After that control returns to normal
-execution.
-
+Both operations follow the same set of steps.
+Both start with the user preforming a raise on an exception.
+Then the exception propogates up the stack.
+If a handler is found the exception is caught and the handler is run.
+After that control returns to normal execution.
 If the search fails a default handler is run and then control
-returns to normal execution immediately. That is where the default handlers
-@defaultTermiationHandler@ and @defaultResumptionHandler@ are used.
+returns to normal execution after the raise.
+
+This general description covers what the two kinds have in common.
+Differences include how propogation is preformed, where exception continues
+after an exception is caught and handled and which default handler is run.
 
 \subsection{Termination}
 \label{s:Termination}
-
-Termination handling is more familiar kind and used in most programming
+Termination handling is the familiar kind and used in most programming
 languages with exception handling.
-It is dynamic, non-local goto. If a throw is successful then the stack will
-be unwound and control will (usually) continue in a different function on
-the call stack. They are commonly used when an error has occurred and recovery
-is impossible in the current function.
+It is dynamic, non-local goto. If the raised exception is matched and
+handled the stack is unwound and control will (usually) continue the function
+on the call stack that defined the handler.
+Termination is commonly used when an error has occurred and recovery is
+impossible locally.
 
 % (usually) Control can continue in the current function but then a different
 % control flow construct should be used.
 
-A termination throw is started with the @throw@ statement:
+A termination raise is started with the @throw@ statement:
 \begin{cfa}
 throw EXPRESSION;
 \end{cfa}
 The expression must return a reference to a termination exception, where the
-termination exception is any type that satisfies @is_termination_exception@
-at the call site.
-Through \CFA's trait system the functions in the traits are passed into the
-throw code. A new @defaultTerminationHandler@ can be defined in any scope to
+termination exception is any type that satisfies the trait
+@is_termination_exception@ at the call site.
+Through \CFA's trait system the trait functions are implicity passed into the
+throw code and the EHM.
+A new @defaultTerminationHandler@ can be defined in any scope to
 change the throw's behavior (see below).
 
-The throw will copy the provided exception into managed memory. It is the
-user's responsibility to ensure the original exception is cleaned up if the
-stack is unwound (allocating it on the stack should be sufficient).
-
-Then the exception system searches the stack using the copied exception.
-It starts starts from the throw and proceeds to the base of the stack,
+The throw will copy the provided exception into managed memory to ensure
+the exception is not destroyed if the stack is unwound.
+It is the user's responsibility to ensure the original exception is cleaned
+up wheither the stack is unwound or not. Allocating it on the stack is
+usually sufficient.
+
+Then propogation starts with the search. \CFA uses a ``first match" rule so
+matching is preformed with the copied exception as the search continues.
+It starts from the throwing function and proceeds to the base of the stack,
 from callee to caller.
 At each stack frame, a check is made for resumption handlers defined by the
@@ -309,45 +331,47 @@
 try {
 	GUARDED_BLOCK
-} catch (EXCEPTION_TYPE$\(_1\)$ * NAME$\(_1\)$) {
+} catch (EXCEPTION_TYPE$\(_1\)$ * [NAME$\(_1\)$]) {
 	HANDLER_BLOCK$\(_1\)$
-} catch (EXCEPTION_TYPE$\(_2\)$ * NAME$\(_2\)$) {
+} catch (EXCEPTION_TYPE$\(_2\)$ * [NAME$\(_2\)$]) {
 	HANDLER_BLOCK$\(_2\)$
 }
 \end{cfa}
-When viewed on its own a try statement will simply execute the statements in
-@GUARDED_BLOCK@ and when those are finished the try statement finishes.
+When viewed on its own, a try statement will simply execute the statements
+in @GUARDED_BLOCK@ and when those are finished the try statement finishes.
 
 However, while the guarded statements are being executed, including any
-functions they invoke, all the handlers following the try block are now
-or any functions invoked from those
-statements, throws an exception, and the exception
-is not handled by a try statement further up the stack, the termination
-handlers are searched for a matching exception type from top to bottom.
-
-Exception matching checks the representation of the thrown exception-type is
-the same or a descendant type of the exception types in the handler clauses. If
-it is the same of a descendant of @EXCEPTION_TYPE@$_i$ then @NAME@$_i$ is
+invoked functions, all the handlers in the statement are now on the search
+path. If a termination exception is thrown and not handled further up the
+stack they will be matched against the exception.
+
+Exception matching checks the handler in each catch clause in the order
+they appear, top to bottom. If the representation of the thrown exception type
+is the same or a descendant of @EXCEPTION_TYPE@$_i$ then @NAME@$_i$
+(if provided) is
 bound to a pointer to the exception and the statements in @HANDLER_BLOCK@$_i$
 are executed. If control reaches the end of the handler, the exception is
 freed and control continues after the try statement.
 
-If no handler is found during the search then the default handler is run.
+If no termination handler is found during the search then the default handler
+(@defaultTerminationHandler@) is run.
 Through \CFA's trait system the best match at the throw sight will be used.
 This function is run and is passed the copied exception. After the default
 handler is run control continues after the throw statement.
 
-There is a global @defaultTerminationHandler@ that cancels the current stack
-with the copied exception. However it is generic over all exception types so
-new default handlers can be defined for different exception types and so
-different exception types can have different default handlers.
+There is a global @defaultTerminationHandler@ that is polymorphic over all
+exception types. Since it is so general a more specific handler can be
+defined and will be used for those types, effectively overriding the handler
+for particular exception type.
+The global default termination handler performs a cancellation
+\see{\VRef{s:Cancellation}} on the current stack with the copied exception.
 
 \subsection{Resumption}
 \label{s:Resumption}
 
-Resumption exception handling is a less common form than termination but is
-just as old~\cite{Goodenough75} and is in some sense simpler.
-It is a dynamic, non-local function call. If the throw is successful a
-closure will be taken from up the stack and executed, after which the throwing
-function will continue executing.
+Resumption exception handling is less common than termination but is
+just as old~\cite{Goodenough75} and is simpler in many ways.
+It is a dynamic, non-local function call. If the raised exception is
+matched a closure will be taken from up the stack and executed,
+after which the raising function will continue executing.
 These are most often used when an error occurred and if the error is repaired
 then the function can continue.
@@ -357,15 +381,17 @@
 throwResume EXPRESSION;
 \end{cfa}
-The semantics of the @throwResume@ statement are like the @throw@, but the
-expression has return a reference a type that satisfies the trait
-@is_resumption_exception@. The assertions from this trait are available to
+It works much the same way as the termination throw.
+The expression must return a reference to a resumption exception,
+where the resumption exception is any type that satisfies the trait
+@is_resumption_exception@ at the call site.
+The assertions from this trait are available to
 the exception system while handling the exception.
 
-At run-time, no copies are made. As the stack is not unwound the exception and
+At run-time, no exception copy is made.
+As the stack is not unwound the exception and
 any values on the stack will remain in scope while the resumption is handled.
 
-Then the exception system searches the stack using the provided exception.
-It starts starts from the throw and proceeds to the base of the stack,
-from callee to caller.
+The EHM then begins propogation. The search starts from the raise in the
+resuming function and proceeds to the base of the stack, from callee to caller.
 At each stack frame, a check is made for resumption handlers defined by the
 @catchResume@ clauses of a @try@ statement.
@@ -373,23 +399,30 @@
 try {
 	GUARDED_BLOCK
-} catchResume (EXCEPTION_TYPE$\(_1\)$ * NAME$\(_1\)$) {
+} catchResume (EXCEPTION_TYPE$\(_1\)$ * [NAME$\(_1\)$]) {
 	HANDLER_BLOCK$\(_1\)$
-} catchResume (EXCEPTION_TYPE$\(_2\)$ * NAME$\(_2\)$) {
+} catchResume (EXCEPTION_TYPE$\(_2\)$ * [NAME$\(_2\)$]) {
 	HANDLER_BLOCK$\(_2\)$
 }
 \end{cfa}
-If the handlers are not involved in a search this will simply execute the
-@GUARDED_BLOCK@ and then continue to the next statement.
-Its purpose is to add handlers onto the stack.
-(Note, termination and resumption handlers may be intermixed in a @try@
-statement but the kind of throw must be the same as the handler for it to be
-considered as a possible match.)
-
-If a search for a resumption handler reaches a try block it will check each
-@catchResume@ clause, top-to-bottom.
-At each handler if the thrown exception is or is a child type of
-@EXCEPTION_TYPE@$_i$ then the a pointer to the exception is bound to
-@NAME@$_i$ and then @HANDLER_BLOCK@$_i$ is executed. After the block is
-finished control will return to the @throwResume@ statement.
+% I wonder if there would be some good central place for this.
+Note that termination handlers and resumption handlers may be used together
+in a single try statement, intermixing @catch@ and @catchResume@ freely.
+Each type of handler will only interact with exceptions from the matching
+type of raise.
+When a try statement is executed it simply executes the statements in the
+@GUARDED_BLOCK@ and then finishes.
+
+However, while the guarded statements are being executed, including any
+invoked functions, all the handlers in the statement are now on the search
+path. If a resumption exception is reported and not handled further up the
+stack they will be matched against the exception.
+
+Exception matching checks the handler in each catch clause in the order
+they appear, top to bottom. If the representation of the thrown exception type
+is the same or a descendant of @EXCEPTION_TYPE@$_i$ then @NAME@$_i$
+(if provided) is bound to a pointer to the exception and the statements in
+@HANDLER_BLOCK@$_i$ are executed.
+If control reaches the end of the handler, execution continues after the
+the raise statement that raised the handled exception.
 
 Like termination, if no resumption handler is found, the default handler
@@ -397,14 +430,13 @@
 call sight according to \CFA's overloading rules. The default handler is
 passed the exception given to the throw. When the default handler finishes
-execution continues after the throw statement.
+execution continues after the raise statement.
 
 There is a global @defaultResumptionHandler@ is polymorphic over all
 termination exceptions and preforms a termination throw on the exception.
-The @defaultTerminationHandler@ for that throw is matched at the original
-throw statement (the resumption @throwResume@) and it can be customized by
+The @defaultTerminationHandler@ for that raise is matched at the original
+raise statement (the resumption @throwResume@) and it can be customized by
 introducing a new or better match as well.
 
-% \subsubsection?
-
+\subsubsection{Resumption Marking}
 A key difference between resumption and termination is that resumption does
 not unwind the stack. A side effect that is that when a handler is matched
@@ -432,11 +464,10 @@
 can form with multiple handlers and different exception types.
 
-To prevent all of these cases we mask sections of the stack, or equivalently
-the try statements on the stack, so that the resumption search skips over
-them and continues with the next unmasked section of the stack.
-
-A section of the stack is marked when it is searched to see if it contains
-a handler for an exception and unmarked when that exception has been handled
-or the search was completed without finding a handler.
+To prevent all of these cases we mark try statements on the stack.
+A try statement is marked when a match check is preformed with it and an
+exception. The statement will be unmarked when the handling of that exception
+is completed or the search completes without finding a handler.
+While a try statement is marked its handlers are never matched, effectify
+skipping over it to the next try statement.
 
 % This might need a diagram. But it is an important part of the justification
@@ -457,16 +488,15 @@
 \end{verbatim}
 
-The rules can be remembered as thinking about what would be searched in
-termination. So when a throw happens in a handler; a termination handler
-skips everything from the original throw to the original catch because that
-part of the stack has been unwound, a resumption handler skips the same
-section of stack because it has been masked.
-A throw in a default handler will preform the same search as the original
-throw because; for termination nothing has been unwound, for resumption
-the mask will be the same.
-
-The symmetry with termination is why this pattern was picked. Other patterns,
-such as marking just the handlers that caught, also work but lack the
-symmetry which means there is more to remember.
+These rules mirror what happens with termination.
+When a termination throw happens in a handler the search will not look at
+any handlers from the original throw to the original catch because that
+part of the stack has been unwound.
+A resumption raise in the same situation wants to search the entire stack,
+but it will not try to match the exception with try statements in the section
+that would have been unwound as they are marked.
+
+The symmetry between resumption termination is why this pattern was picked.
+Other patterns, such as marking just the handlers that caught, also work but
+lack the symmetry means there are less rules to remember.
 
 \section{Conditional Catch}
@@ -474,5 +504,5 @@
 condition to further control which exceptions they handle:
 \begin{cfa}
-catch (EXCEPTION_TYPE * NAME ; CONDITION)
+catch (EXCEPTION_TYPE * [NAME] ; CONDITION)
 \end{cfa}
 First, the same semantics is used to match the exception type. Second, if the
@@ -482,22 +512,28 @@
 matches. Otherwise, the exception search continues as if the exception type
 did not match.
+
+The condition matching allows finer matching by allowing the match to check
+more kinds of information than just the exception type.
 \begin{cfa}
 try {
-	f1 = open( ... );
-	f2 = open( ... );
+	handle1 = open( f1, ... );
+	handle2 = open( f2, ... );
+	handle3 = open( f3, ... );
 	...
 } catch( IOFailure * f ; fd( f ) == f1 ) {
-	// only handle IO failure for f1
+	// Only handle IO failure for f1.
+} catch( IOFailure * f ; fd( f ) == f3 ) {
+	// Only handle IO failure for f3.
 }
-\end{cfa}
-Note, catching @IOFailure@, checking for @f1@ in the handler, and re-raising the
-exception if not @f1@ is different because the re-raise does not examine any of
-remaining handlers in the current try statement.
-
-\section{Rethrowing}
-\colour{red}{From Andrew: I recomend we talk about why the language doesn't
-have rethrows/reraises instead.}
-
-\label{s:Rethrowing}
+// Can't handle a failure relating to f2 here.
+\end{cfa}
+In this example the file that experianced the IO error is used to decide
+which handler should be run, if any at all.
+
+\begin{comment}
+% I know I actually haven't got rid of them yet, but I'm going to try
+% to write it as if I had and see if that makes sense:
+\section{Reraising}
+\label{s:Reraising}
 Within the handler block or functions called from the handler block, it is
 possible to reraise the most recently caught exception with @throw@ or
@@ -518,8 +554,60 @@
 is part of an unwound stack frame. To prevent this problem, a new default
 handler is generated that does a program-level abort.
+\end{comment}
+
+\subsection{Comparison with Reraising}
+A more popular way to allow handlers to match in more detail is to reraise
+the exception after it has been caught if it could not be handled here.
+On the surface these two features seem interchangable.
+
+If we used @throw;@ to start a termination reraise then these two statements
+would have the same behaviour:
+\begin{cfa}
+try {
+    do_work_may_throw();
+} catch(exception_t * exc ; can_handle(exc)) {
+    handle(exc);
+}
+\end{cfa}
+
+\begin{cfa}
+try {
+    do_work_may_throw();
+} catch(exception_t * exc) { 
+    if (can_handle(exc)) {
+        handle(exc);
+    } else {
+        throw;
+    }
+}
+\end{cfa}
+If there are further handlers after this handler only the first version will
+check them. If multiple handlers on a single try block could handle the same
+exception the translations get more complex but they are equivilantly
+powerful.
+
+Until stack unwinding comes into the picture. In termination handling, a
+conditional catch happens before the stack is unwound, but a reraise happens
+afterwards. Normally this might only cause you to loose some debug
+information you could get from a stack trace (and that can be side stepped
+entirely by collecting information during the unwind). But for \CFA there is
+another issue, if the exception isn't handled the default handler should be
+run at the site of the original raise.
+
+There are two problems with this: the site of the original raise doesn't
+exist anymore and the default handler might not exist anymore. The site will
+always be removed as part of the unwinding, often with the entirety of the
+function it was in. The default handler could be a stack allocated nested
+function removed during the unwind.
+
+This means actually trying to pretend the catch didn't happening, continuing
+the original raise instead of starting a new one, is infeasible.
+That is the expected behaviour for most languages and we can't replicate
+that behaviour.
 
 \section{Finally Clauses}
+\label{s:FinallyClauses}
 Finally clauses are used to preform unconditional clean-up when leaving a
-scope. They are placed at the end of a try statement:
+scope and are placed at the end of a try statement after any handler clauses:
 \begin{cfa}
 try {
@@ -537,23 +625,26 @@
 
 Execution of the finally block should always finish, meaning control runs off
-the end of the block. This requirement ensures always continues as if the
-finally clause is not present, \ie finally is for cleanup not changing control
-flow. Because of this requirement, local control flow out of the finally block
+the end of the block. This requirement ensures control always continues as if
+the finally clause is not present, \ie finally is for cleanup not changing
+control flow.
+Because of this requirement, local control flow out of the finally block
 is forbidden. The compiler precludes any @break@, @continue@, @fallthru@ or
 @return@ that causes control to leave the finally block. Other ways to leave
 the finally block, such as a long jump or termination are much harder to check,
-and at best requiring additional run-time overhead, and so are mealy
+and at best requiring additional run-time overhead, and so are only
 discouraged.
 
-Not all languages with exceptions have finally clauses. Notably \Cpp does
+Not all languages with unwinding have finally clauses. Notably \Cpp does
 without it as descructors serve a similar role. Although destructors and
 finally clauses can be used in many of the same areas they have their own
 use cases like top-level functions and lambda functions with closures.
 Destructors take a bit more work to set up but are much easier to reuse while
-finally clauses are good for once offs and can include local information.
+finally clauses are good for one-off uses and
+can easily include local information.
 
 \section{Cancellation}
+\label{s:Cancellation}
 Cancellation is a stack-level abort, which can be thought of as as an
-uncatchable termination. It unwinds the entirety of the current stack, and if
+uncatchable termination. It unwinds the entire current stack, and if
 possible forwards the cancellation exception to a different stack.
 
@@ -561,61 +652,62 @@
 There is no special statement for starting a cancellation; instead the standard
 library function @cancel_stack@ is called passing an exception. Unlike a
-throw, this exception is not used in matching only to pass information about
+raise, this exception is not used in matching only to pass information about
 the cause of the cancellation.
-(This also means matching cannot fail so there is no default handler either.)
-
-After @cancel_stack@ is called the exception is copied into the exception
-handling mechanism's memory. Then the entirety of the current stack is
+(This also means matching cannot fail so there is no default handler.)
+
+After @cancel_stack@ is called the exception is copied into the EHM's memory
+and the current stack is
 unwound. After that it depends one which stack is being cancelled.
 \begin{description}
 \item[Main Stack:]
 The main stack is the one used by the program main at the start of execution,
-and is the only stack in a sequential program. Even in a concurrent program
-the main stack is only dependent on the environment that started the program.
-Hence, when the main stack is cancelled there is nowhere else in the program
-to notify. After the stack is unwound, there is a program-level abort.
+and is the only stack in a sequential program.
+After the main stack is unwound there is a program-level abort. 
+
+There are two reasons for this. The first is that it obviously had to do this
+in a sequential program as there is nothing else to notify and the simplicity
+of keeping the same behaviour in sequential and concurrent programs is good.
+Also, even in concurrent programs there is no stack that an innate connection
+to, so it would have be explicitly managed.
 
 \item[Thread Stack:]
-A thread stack is created for a @thread@ object or object that satisfies the
-@is_thread@ trait. A thread only has two points of communication that must
-happen: start and join. As the thread must be running to perform a
-cancellation, it must occur after start and before join, so join is used
-for communication here.
-After the stack is unwound, the thread halts and waits for
-another thread to join with it. The joining thread checks for a cancellation,
-and if present, resumes exception @ThreadCancelled@.
-
-There is a subtle difference between the explicit join (@join@ function) and
-implicit join (from a destructor call). The explicit join takes the default
-handler (@defaultResumptionHandler@) from its calling context, which is used if
-the exception is not caught. The implicit join does a program abort instead.
-
-This semantics is for safety. If an unwind is triggered while another unwind
-is underway only one of them can proceed as they both want to ``consume'' the
-stack. Letting both try to proceed leads to very undefined behaviour.
-Both termination and cancellation involve unwinding and, since the default
-@defaultResumptionHandler@ preforms a termination that could more easily
-happen in an implicate join inside a destructor. So there is an error message
-and an abort instead.
-\todo{Perhaps have a more general disucssion of unwind collisions before
-this point.}
-
-The recommended way to avoid the abort is to handle the initial resumption
-from the implicate join. If required you may put an explicate join inside a
-finally clause to disable the check and use the local
-@defaultResumptionHandler@ instead.
-
-\item[Coroutine Stack:] A coroutine stack is created for a @coroutine@ object
-or object that satisfies the @is_coroutine@ trait. A coroutine only knows of
-two other coroutines, its starter and its last resumer. Of the two the last
-resumer has the tightest coupling to the coroutine it activated and the most
-up-to-date information.
-
-Hence, cancellation of the active coroutine is forwarded to the last resumer
-after the stack is unwound. When the resumer restarts, it resumes exception
-@CoroutineCancelled@, which is polymorphic over the coroutine type and has a
-pointer to the cancelled coroutine.
-
-The resume function also has an assertion that the @defaultResumptionHandler@
-for the exception. So it will use the default handler like a regular throw.
+A thread stack is created for a \CFA @thread@ object or object that satisfies
+the @is_thread@ trait.
+After a thread stack is unwound there exception is stored until another
+thread attempts to join with it. Then the exception @ThreadCancelled@,
+which stores a reference to the thread and to the exception passed to the
+cancellation, is reported from the join.
+There is one difference between an explicit join (with the @join@ function)
+and an implicit join (from a destructor call). The explicit join takes the
+default handler (@defaultResumptionHandler@) from its calling context while
+the implicit join provides its own which does a program abort if the
+@ThreadCancelled@ exception cannot be handled.
+
+Communication is done at join because a thread only has to have to points of
+communication with other threads: start and join.
+Since a thread must be running to perform a cancellation (and cannot be
+cancelled from another stack), the cancellation must be after start and
+before the join. So join is the one that we will use.
+
+% TODO: Find somewhere to discuss unwind collisions.
+The difference between the explicit and implicit join is for safety and
+debugging. It helps prevent unwinding collisions by avoiding throwing from
+a destructor and prevents cascading the error across multiple threads if
+the user is not equipped to deal with it.
+Also you can always add an explicit join if that is the desired behaviour.
+
+\item[Coroutine Stack:]
+A coroutine stack is created for a @coroutine@ object or object that
+satisfies the @is_coroutine@ trait.
+After a coroutine stack is unwound control returns to the resume function
+that most recently resumed it. The resume statement reports a
+@CoroutineCancelled@ exception, which contains a references to the cancelled
+coroutine and the exception used to cancel it.
+The resume function also takes the @defaultResumptionHandler@ from the
+caller's context and passes it to the internal report.
+
+A coroutine knows of two other coroutines, its starter and its last resumer.
+The starter has a much more distant connection while the last resumer just
+(in terms of coroutine state) called resume on this coroutine, so the message
+is passed to the latter.
 \end{description}
Index: doc/theses/andrew_beach_MMath/uw-ethesis.tex
===================================================================
--- doc/theses/andrew_beach_MMath/uw-ethesis.tex	(revision de47a9d90448b4a9998ca306ff8576f8cd4f3369)
+++ doc/theses/andrew_beach_MMath/uw-ethesis.tex	(revision f6106a6aba16b040f4f86fe37774493e2d88df68)
@@ -217,4 +217,10 @@
 \pdfstringdefDisableCommands{\def\Cpp{C++}}
 
+% Wrappers for inline code snippits.
+\newrobustcmd*\codeCFA[1]{\lstinline[language=CFA]{#1}}
+\newrobustcmd*\codeC[1]{\lstinline[language=C]{#1}}
+\newrobustcmd*\codeCpp[1]{\lstinline[language=C++]{#1}}
+\newrobustcmd*\codePy[1]{\lstinline[language=Python]{#1}}
+
 % Colour text, formatted in LaTeX style instead of TeX style.
 \newcommand*\colour[2]{{\color{#1}#2}}