Multiple Representation and Coercion

This example illustrates how sort constraints and retracts can be used to provide multiple representations for a single abstract type, with coercions that change representation automatically when needed. The example used is Cartesian and polar representations of points (or vectors from the origin) in the plane. The keyword mb declares a sort constraint, following the syntax of Maude; it is implemented as in the example Meta-programming and Sort Constraints, and is here used to define subsorts for angles and non-negative floating point numbers. Distance and sum (d and +, respectively) are only defined on the Cartesian representation, but the three reductions below the first spec apply these functions to varous combinations of representations that are not all Cartesian. The second spec defines a rotation function on polar points and then uses that to define a negation function for addition, as a rotation by pi, i.e., by 180 degrees; since both points are Cartesian, this reduction requires two coercions on the second argument before the addition can be done; the result is zero (up to round off error), just as it should be.

1. BOBJ Source Code

obj POINT is pr FLOAT . sorts NNeg Point Cart Polar Angle . subsorts Angle < NNeg < Float . var N : NNeg . var A : Angle . var F : Float . mb F : NNeg if F >= 0 . op _**2 : Float -> NNeg [prec 2]. eq F **2 = F * F . mb F : Angle if 0 <= F and F < 2 * pi . subsorts Cart Polar < Point . op <_,_> : Float Float -> Cart . op _+_ : Cart Cart -> Cart . vars F1 F2 F3 F4 : Float . eq < F1, F2 > + < F3, F4 > = < F1 + F3, F2 + F4 > . op [_,_] : Angle NNeg -> Polar . eq r:Point>Cart([A, N]) = <N * cos(A), N * sin(A)> if N > 0 . eq r:Point>Cart([A, N]) = <0, 0> if N == 0 . eq r:Point>Polar(<F1, F2>) = [atan(F2 / F1), sqrt(F1 **2 + F2 **2)] if F1 =/= 0 . op d : Cart Cart -> NNeg . eq d(<F1, F2>, <F3, F4>) = sqrt((F1 - F3)**2 + (F2 - F4)**2). end red d(<1, 1 >, [pi / 3, 3]). red <1, 1 > + [pi / 3, 3]. red [pi / 2, 2] + [pi / 3, 3]. obj ROTATE is pr POINT . op r : Polar Angle -> Polar . vars A A' : Angle . var N : NNeg . var P : Polar . eq r([A, N], A') = [A + A', N] . op -_ : Polar -> Polar [prec 2]. eq - P = r(P, pi). end red <1, 1 > + - <1, 1 > .

2. BOBJ Output

% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.255 built: Tue Nov 29 16:53:20 PST 2005 University of California, San Diego Fri Feb 03 12:51:18 PST 2006 BOBJ> in point ========================================== obj POINT ========================================== reduce in POINT : d(< 1 , 1 >, [(pi / 3) , 3]) result Angle: 1.6744693419986432 rewrite time: 752ms parse time: 11ms Warning: non-termination corrected ========================================== reduce in POINT : (< 1 , 1 >) + ([(pi / 3) , 3]) result Cart: < 2.5000000000000004 , 3.598076211353316 > rewrite time: 1305ms parse time: 19ms Warning: non-termination corrected ========================================== reduce in POINT : ([(pi / 2) , 2]) + ([(pi / 3) , 3]) result Cart: < 1.5000000000000007 , 4.598076211353316 > rewrite time: 2358ms parse time: 13ms Warning: non-termination corrected ========================================== obj ROTATE ========================================== reduce in ROTATE : (< 1 , 1 >) + (- (< 1 , 1 >)) result Cart: < -2.220446049250313E-16 , 0.0 > rewrite time: 2493ms parse time: 43ms Warning: non-termination corrected BOBJ> q Bye. %

To BOBJ examples homepage
To Tatami project homepage

Maintained by Joseph Goguen
Last modified: Sat Feb 4 19:49:16 PST 2006