Index: doc/proposals/exceptions-pab.md
===================================================================
--- doc/proposals/exceptions-pab.md	(revision cea0d0c1f38dd62a244e585e64531b78242825f3)
+++ doc/proposals/exceptions-pab.md	(revision cea0d0c1f38dd62a244e585e64531b78242825f3)
@@ -0,0 +1,232 @@
+# Exception Handling Changes
+
+This proposal changes the C∀ exception handling mechanism from matching an object type to a function type.
+Using functions fits with function overloading in the C∀ type system.
+
+The following shows a resumption example.
+
+```
+exception int resumpt( int, double );		// return result, no stack unwinding
+try {
+	i = resumpt( 3, 3.5 );					// exception raise
+} catch( int resumpt( int i, double d ) {	// i = 3, d = 3.5
+	... return 42;		 					// return value to raise point
+}
+```
+
+The following shows a termination example.
+
+```
+exception void termin( double );			// void return, stack unwinding
+try {
+	termin( 3.5 );							// exception raise
+} catch( void termin( int i, double d ) {	// i = 3, d = 3.5
+	...										// fall through to lexical block
+}
+```
+
+There is no explicit *raise* statement.
+(See Mesa Language Manual page 135, footnote)
+The compiler knows a function is an exception, so it does a search call (propagation) instead of a branch call.
+
+An exception function is denoted by the `exception` keyword to differentiate it from a regular function.
+An exception function is defined in a `catch` clause, which is a local, inline implementation of the exception function.
+The catch clause must specify the exception-function name and type for matching, and arbitrary parameter names to access the raise arguments.
+Data is carried from the raise call to the `catch` body via the argument/parameter mechanism, and data can be returned to the raise call via function return.
+An exception function cannot be passed as a function pointer nor can a raise use a pointer to an exception function.
+
+Overloading of the exception raise occurs among existing exception functions.
+
+```
+exception int fix( int, double );
+exception double fix( int, double );
+exception double fix( double );
+try {
+	int i = fix ( 3, 3.5 );					// choose best overloading
+} catch( int fix( int i, double d ) ) {		// match with exact catch body
+} catch( double fix( int i, double d ) ) {
+} catch( double fix( double d ) ) {
+}
+```
+
+Normal overload resolution occur at the raise point, where the best fit *exception* function is chosen based on arguments and left-hand side.
+Matching between raise and catch is exact, as for function pointers, with the selected overload chosen at the raise point (compare mangled names dynamically)
+
+An exception function has a *kind*: return, noreturn, or dual, denoting resumption, termination, or both.
+An exception function cannot be overloaded on the exception kind.
+A return exception function must return a type, a noreturn exception function must return `void`, a dual exception function must return a type.
+A dual exception function is specified using the quasi-keyword `dual`.
+
+```
+exception int dual( int, double ) dual;		// Dual, return result or exit handler block, no initial stack unwinding
+```
+
+Within the handler for kind return (stack not unwound), the handler *must* return a value as for any value returning function;
+any other control-flow statement or fallthrough is an error, like `break` or fallthrough on a value returning function.
+
+```
+	} catch( int fix( int i, float j ) ) {	// stack not unwound, i and j accessible, must return
+		return 42;							// implies return to fix call, not return of nested function
+		break;								// syntax error => must return
+		// fallthrough => syntax error
+	}
+```
+
+Within the handler for kind noreturn (stack unwound), `break` or fallthrough ⇒ exit handler, like in the `case` clause of a switch statement;
+any other control-flow statement works on the lexical context outside the handler.
+
+```
+	} catch( void recover( int i ) ) {		// stack unwound, cannot return
+		break;								// implies exit catch routine
+		return;								// implies return from lexical function
+		// fallthrough => implies break
+	}
+```
+
+Within the handler for kind dual (stack not unwound), `break` or fallthrough ⇒ exit handler and unwind stack, or return a value to the raise at top of the stack.
+
+```
+	} catch( int dual( int i, float j ) ) {	// stack not unwound, can return
+		return 42;							// implies return to fix call, not return of nested function
+		break;								// implies exit catch body
+		// fallthrough => implies break
+	}
+```
+
+In all cases, a handler can raise another exception.
+
+An exception function can have a static body, which define the action if the exception is not caught.
+If no body is specified, there are default actions added.
+This matches with `defaultResume` and `defaultTerminate` in current C∀/μC++.
+Here a parameter name is necessary to access the raise argument(s).
+
+Resumption default:
+
+```
+exception int resumpt( int i ) {			// called if no handler found
+	// return default correction or abort or raise another exception
+	// default if not specified is to call UnhandledException at resumer or joiner.
+}
+```
+
+Termination default:
+
+```
+exception void termin( double d ) {			// called if no handler found
+	// abort or raise another exception
+	// default if not specified is to call UnhandledException at resumer or joiner.
+}
+```
+
+Dual default is the same as termination default, as having a default correction action is unlikely.
+
+A `throws` clause can be added to a regular function to indicate alternate outcomes.
+
+```
+int foo(...) throws( int ex( int ), float ex( int ), char ex( double, double ) );
+```
+
+The `throws` clause is *not* part of the function type, and hence, is not used for overloading.
+Functions with a `throws` clause cause are handled by a separate type-checking pass, which examines the statically call structure to determine if calls to `foo` are nested directly or indirectly within guarded blocks with matching catch clauses, e.g.:
+
+```
+int bar( int i ) throws( int fixup( int ) );
+
+void foo(...) {
+	... i = bar( 3 ); ...					// call statically nested within handler for fixup
+}
+void baz() {
+	try {
+		foo(...);
+	} catch( int fixup( int ) ) {
+		... return 42;
+	}
+}
+```
+
+If this type check fails, a warning is given, and a dynamic check is wrapped around the call to verify only the specified exception functions are raised.
+This dual approach allows all forms of reuse to exist, and is similar to checked/unchecked exceptions in Java.
+
+Resumption example:
+
+```
+exception int fix( int i, float f );
+
+void foo() {
+	try {
+		for () {
+			if ( ... ) x = fix( 3, 5.4 );
+		}
+	} catch( int fix( int i, float j ) ) {
+		... return 42;						// fix up problem and return to raise
+	}
+}
+```
+
+Termination example:
+
+```
+exception void end_of_file( ifstream is );
+
+void foo() {
+	int i;
+	try {
+		for () {
+			sin | i;  // internally, does a call end_of_file( is ), which implicitly throws exception
+			sout | i;
+		}
+	} catch( end_of_file( ifstream is ) && is == sin ) { // "is" used in predicate selection
+		// close file
+	}
+}
+```
+
+Dual example:
+
+```
+exception int dual( int i, float f ) dual;
+
+void baz() {
+	try {
+		for () {
+			if ( ... ) x = dual( 3, 5.4 );
+		}
+	} catch( int dual( int i, float j ) ) {
+		if ( ... ) return 42;				// return to raise calls
+		if ( ... ) break;					// exit catch body
+		// fallthrough						// implies break
+	}
+}
+```
+
+I'm not sure this polymorphism is doing anything, except suggesting a common pattern.
+A catch clause cannot be polymorphic because there is no RTTI matching.
+
+```
+forall( T ) exception void arithmetic( T op1, T op2, int retcode ) noreturn;
+
+enum FloatExceptions ! { Invalid, ZeroDiv, Overflow, Underflow, Inexact };
+exception double arithmetic( double op1, double op2, int retcode ) {
+	// default abort
+}
+enum IntExceptions ! { ZeroDiv, Overflow, Underflow };
+exception double arithmetic( int op1, int op2, int retcode ) {
+	// default abort
+}
+
+void xxx() {
+	double x = 3.5;
+	try {
+		x = x / 0.0;
+	} catch( arithmetic( double op1, double op2, int retcode ) ) {
+		if ( retcode == FloatExceptions.ZeroDiv ) ...
+	}
+
+	int i = 3;
+	try {
+		i = i / 0;
+	} catch( arithmetic( int op1, int op2, int retcode ) ) {
+		if ( retcode == IntExceptions.ZeroDiv ) ...
+	}
+}
+```