(*
 * Union ops:
 *
 *	isa		tag interrogation
 *	.		field selection (projection)
 *	{} or typename	construction (injection)
 *
 *
 * obj union =  tagged_field*
 *    ops: "_?._"(union, fieldname)->boolean;
 *	   "_._"(union, fieldname)->field;
 *         "{_}(fieldtype}->union
 *
 * Tuple ops:
 *
 *	
 *	.		field selection (projection)
 *	{} or typename	construction (injection)
 *
 * obj tuple =  field*
 *     ops: "_._"(union, fieldname)->boolean;
 *         "{...}"(fieldtype}->union	-- sort of
 *
 * Concrete prototypical examples:
 *
 * obj Union =  a:A or b:B or c:C
 *     ops: SelectA(Union)->A;		-- u.a
 *	    SelectB(Union)->B;		-- u.b
 *	    SelectC(Union)->B;		-- u.c
 *	    CheckA(Union)->boolean	-- u?.a
 *	    CheckB(Union)->boolean;	-- u?.b
 *	    CheckC(Union)->boolean;	-- u?.c
 *	    Union(A)->Union;		-- {aval}
 *	    Union(B)->Union;		-- {bval}
 *	    Union(C)->Union;		-- {cval}
 * end;
 *
 * obj Tuple =  a:A and b:B and c:C
 *     ops: SelectA(Tuple)->A;		-- u.a
 *	    SelectB(Tuple)->B;		-- u.b
 *	    SelectC(Tuple)->B;		-- u.c
 *	    Tuple(A,B,C)->Tuple;	-- {aval,bval,cval}
 * end;
 *
 *
 * On the necessary type inference and/or structural type equivalencing.
 *
 *     * The type of {x} is a tagged value of the form {x, typeof(x)}, suitable
 *	 for binding to a variable of type (typeof(x) or ...).
 *
 *     * The type of {x,y,z} is a tuple value of the form {x, y, z}, suitable
 *	 for binding to a variable of type (typeof(x) and typeof(y) and
 *	 typeof(z)).
 *
 *)
object Union =  a:A or b:B or c:C;
object A;
object B;
object C;

operation u1(u:Union, a:A, b:B, c:C)->(u':Union, a':A, b':B, c':C)
    pre: if u?.a then u.a = a else false;
    post: u' = {a};	(* ERROR: { ... } is not a union constructor in new
			   semantics.  24mar04: This comment, from 7jun00, is
		           not longer true.  There s a 24mar04 LOG message
			   about it. *)
end u1;

operation u2
    components: ;
    inputs: x:Union, y:Union;
    outputs: z: Union;
    description: (*
	x
    *);
end u2;