Compact Reals

spec
       CompactReal = 
       BasicReal reveal 
        sort Real, 
        preds __ <= __, __ >= __, __ < __, __ > __, 
        ops __+, __-, __ + __, __ - __, __ * __, __ / __ 

then
       free
              type CompactReal ::= sort Real | posInfinity | negInfinity 
then
       SigOrder with  Elem |-> CompactReal 
then
       var
              r:Real 
       .              negInfinity < posInfinity 
       .              r < posInfinity 
       .              negInfinity < r 
then
       sorts
               PosCompactReal = {x:CompactReal . x > 0 }; 
               NegCompactReal = {x:CompactReal . x < 0 } 

       preds
              isReal, isInfinity: CompactReal 
       ops
               +__, -__: 
                        CompactReal -> CompactReal; 
               __ + __, 
               __ * __: 
                        CompactReal × CompactReal ->? CompactReal, 
                        comm; 
               __ - __, 
               __ / __: 
                        CompactReal × CompactReal ->? CompactReal; 

       vars
               r:Real; 
               p: PosCompactReal; n: NegCompactReal; x,y: CompactReal 

       %%              Defining the sort-predicates: 
       .              isReal(x) <=> x in Real 
       .              isInifinite(x) <=> x=posInfinity \/ x=negInfinity 
       %%              Extending the operations for the new values 
       %%              negInfinity and posInfinity; 
       %%              the results of the terms 
       %%              0/0, infty/infty, 0 * infty, infty-infty 
       %%              are undefined: 
       .              + negInfinity = negInfinity 
       .              + posInfinity = posInfinity 
       .              - negInfinity = posInfinity 
       .              - posInfinity = negInfinity 
       .              r + posInfinity = posInfinity 
       .              r + negInfinity = negInfinity 
       .              posInfinity + posInfinity = posInfinity 
       .              negInfinity + negInfinity = negInfinity 
       .              not def (posInfinity + negInfinity) 
       .              x - y = x + (-y) 
       .              p * posInfinity = posInfinity 
       .              p * negInfinity = negInfinity 
       .              n * posInfinity = negInfinity 
       .              n * negInfinity = posInfinity 
       .              not def (0 * x) if isInfinity(x) 
       .              r / posInfinity =0 
       .              r / negInfinity =0 
       .              not def (x/y) if (isInfinity(x) /\ isInfinity(y)) 
then
       %%cons 
       vars
              x,y: CompactReal 
       .              def (x + y) <=> 
               isReal(x) \/ 
               isReal(y) \/ 
               (x=posInfinity /\ y=posInfinity) \/ 
               (x=negInfinity /\ y=negInfinity) 

       .              def (x - y) <=> 
               isReal(x) \/ 
               isReal(y) \/ 
               (x=posInfinity /\ y=negInfinity) \/ 
               (x=negInfinity /\ y=posInfinity) 

       .              def (x * y) <=> not ((x=0 /\ isInfinity(y)) \/ (y=0 /\ isInfinity(x)) ) 
       .              def (x / y) <=> not (y = 0) /\ (isReal(x) \/ isReal(y)) 
end

view
       TotalOrder_in_CompactReal: 
TotalOrder
       to CompactReal = 
       sort
              Elem |-> CompactReal, 
       pred
              __ <= __ |-> __ <= __ 
end



spec
       ScreenAndRounding = 
       CompactReal 
then
       sort
              CompactS < CompactReal 
       op
              round: CompactReal -> CompactS 
then
       SigOrder with  Elem |-> CompactS 
then
       var
              r: CompactReal 
       %%              CompactS is a screen on CompactReal: 
       .              exists glb: CompactS . (glb <= r /\ forall s: CompactS . (s <= r => s <= glb)) 
       .              exists lub: CompactS . (r <= lub /\ forall s: CompactS . (r <= s => lub <= s)) 
       var
              r, r': CompactReal; s: CompactS 
       %%              round has the projection property: 
       .              round(s) = s 
       %%              round is monotone: 
       .              r <= r' => round(r) <= round(r') 
end

spec
       AbstractExecutableReal 
       [ScreenAndRounding with 
        sort CompactS, 
        preds __ <= __, __ >= __, __<__, __ > __, 
        op round ] 

       given CompactReal = 
       CompactReal 
then
       type
              Screen::= compactSToScreen(screenToCompactS: CompactS) 
       var
              s:Screen 
       .              compactSToScreen (screenToCompactS(s)) = s 
       %%              the other direction - 
       %%              screenToCompactS(compactSToSecreen(x)) = x 
       %%              - is provided by the semantics of the type construct.
       ops
               +__, -__: 
                                     Screen -> Screen; 
               __ + __, __ - __, __ * __: 
                                     Screen × Screen -> Screen; 
               __ / __: 
                                     Screen × Screen ->? Screen; 

       var
              x,y: Screen 
       .              + x = compactSToScreen(round(screenToCompactS(x))) 
       .              - x = compactSToScreen(round(screenToCompactS(x))) 
       .              x + y = 
               compactSToScreen(round( 
               screenToCompactS(x) + screenToCompactS(y))) 

       .              x - y = 
               compactSToScreen(round( 
               screenToCompactS(x) - screenToCompactS(y))) 

       .              x * y = 
               compactSToScreen(round( 
               screenToCompactS(x) * screenToCompactS(y))) 

       .              x / y = 
               compactSToScreen(round( 
               screenToCompactS(x) / screenToCompactS(y))) 

end