14.3 Coercions
A name f can be declared as a coercion between a source user-class C with n parameters and a target class D if one of these conditions holds:- D is a user-class, then the type of f must have the form (x1:A1)..(xn:An)(y:(C x1..xn)) (D u1..um) where m is the number of parameters of D.
- D is FUNCLASS, then the type of f must have the form (x1:A1)..(xn:An)(y:(C x1..xn))(x:A)B.
- D is SORTCLASS, then the type of f must have the form (x1:A1)..(xn:An)(y:(C x1..xn))s.
We then write f:C >-> D. The restriction on the type of coercions is called the uniform inheritance condition. Remark that the abstract classes FUNCLASS and SORTCLASS cannot be source classes.
To coerce an object t:(C t1..tn) of C towards D, we have to apply the coercion f to it; the obtained term (f t1..tn t) is then an object of D.
14.3.1 Identity Coercions
Identity coercions are special cases of coercions used to go around the uniform inheritance condition. Let C and D be two classes with respectively n and m parameters and f:(x1:T1)..(xk:Tk)(y:(C u1..un))(D v1..vm) a function which does not verify the uniform inheritance condition. To declare f as coercion, one has first to declare a subclass C' of C:C' := [x1:T1]..[xk:Tk](C u1..un)
We then define an identity coercion between C' and C:
|
We can now declare f as coercion from C' to D, since we can ``cast'' its type as (x1:T1)..(xk:Tk)(y:(C' x1..xk))(D v1..vm).
The identity coercions have a special status: to coerce an object t:(C' t1..tk) of C' towards C, we have not to insert explicitly Id_C'_C since (Id_C'_C t1..tk t) is convertible with t. However we ``rewrite'' the type of t to become an object of C; in this case, it becomes (C u1*..uk*) where each ui* is the result of the substitution in ui of the variables xj by tj.