funcompose {X, YB, ZB : TYPE; yb : YB, zb : ZB} : CONTEXT =
BEGIN

%% The extended function context defining additional operations upon partial
%% functions of different types (from type X to type YB; and from type Y to 
%% type ZB).  The domain types X and Y have no bottom value; the range types
%% YB and ZB are extended types containing yb, zb bottom values respectively.
%% Other standard function operations are defined in the function context.  
%% These include constructors for the empty and singleton (maplet) functions.

%% Version revised by A J H Simons on 1 September 2011.

%% Local types - do not export; for internal use within this context only.
%% All First, Second and Composed function types should be declared either 
%% using the cognate Function type defined in the function context, or using
%% the respective underlying base types [X -> YB], [Y -> ZB] or [X -> ZB].

	Y : TYPE = {y : YB | y /= yb};

	First : TYPE = [X -> YB];
	Second : TYPE = [Y -> ZB];
	Composed : TYPE = [X -> ZB];

%% Compose two functions.  The result contains all pairs (x, z) such that
%% some pair (x, y) exists in the first function and some pair (y, z) exists
%% in the second function.  The standard version is the forwards composition 
%% of two functions (Z 'colon' composition).  An alternative is provided for
%% backwards composition (Z 'circle' composition), which is found more often
%% in Z specifications that compose functions.

	compose (funA : First, funB : Second) : Composed =
		LAMBDA (x : X) : LET y : YB = funA(x) IN
			IF y = yb THEN zb ELSE funB(y) ENDIF;

	backCompose(funA : Second, funB : First) : Composed =
		compose(funB, funA);

END