<<>> <> <> <> <> DIRECTORY Ieee USING [SingleReal], Basics32 USING [BITXOR]; <> <<>> <> RealInline: CEDAR DEFINITIONS IMPORTS Basics32 ~ BEGIN OPEN Ieee; <> <<>> Exponent: TYPE = BYTE; oneExponent: Exponent = 127; lastIntExponent: Exponent = oneExponent+BITS[INT]-1; nanExponent: Exponent = Exponent.LAST; realZero: REAL = LOOPHOLE[SingleReal[sign: FALSE, exp: 0, m: 0]]; posZero: REAL = LOOPHOLE[SingleReal[sign: FALSE, exp: 0, m: 0]]; negZero: REAL = LOOPHOLE[SingleReal[sign: TRUE, exp: 0, m: 0]]; posOne: REAL = LOOPHOLE[SingleReal[sign: FALSE, exp: oneExponent, m: 0]]; negOne: REAL = LOOPHOLE[SingleReal[sign: TRUE, exp: oneExponent, m: 0]]; posTwo: REAL = LOOPHOLE[SingleReal[sign: FALSE, exp: oneExponent+1, m: 0]]; negTwo: REAL = LOOPHOLE[SingleReal[sign: TRUE, exp: oneExponent+1, m: 0]]; maxFixable: REAL = LOOPHOLE[SingleReal[sign: FALSE, exp: lastIntExponent, m: 0]]; signBitAsCard: CARD = LOOPHOLE[SingleReal[sign: TRUE, exp: 0, m: 0]]; posInf: REAL = LOOPHOLE[SingleReal[sign: FALSE, exp: nanExponent, m: 0]]; negInf: REAL = LOOPHOLE[SingleReal[sign: TRUE, exp: nanExponent, m: 0]]; <> <<>> MCFix: PROC [REAL] RETURNS [INT] ~ TRUSTED MACHINE CODE { "XR_REAL32_Fix"; }; MCRound: PROC [REAL] RETURNS [INT] ~ TRUSTED MACHINE CODE { "XR_REAL32_Round"; }; MCCeiling: PROC [REAL] RETURNS [INT] ~ TRUSTED MACHINE CODE { "XR_REAL32_Ceiling"; }; MCFloor: PROC [REAL] RETURNS [INT] ~ TRUSTED MACHINE CODE { "XR_REAL32_Floor"; }; <> <<>> IsZero: PROC [r: REAL] RETURNS [BOOL] = INLINE { RETURN [AbsEq[r, realZero]]; }; IsPositive: PROC [r: REAL] RETURNS [BOOL] = INLINE { RETURN [LOOPHOLE[r, INT] > 0]; }; IsFixable: PROC [r: REAL] RETURNS [BOOL] = INLINE { RETURN [AbsLe[r, maxFixable]]; }; IsValid: PROC [r: REAL] RETURNS [BOOL] = INLINE { RETURN [LOOPHOLE[r, SingleReal].exp # nanExponent]; }; Abs: PROC [r: REAL] RETURNS [REAL] = INLINE { RETURN [LOOPHOLE[LOOPHOLE[r, CARD] MOD signBitAsCard, REAL]]; }; Neg: PROC [r: REAL] RETURNS [REAL] = INLINE { RETURN [LOOPHOLE[Basics32.BITXOR[LOOPHOLE[r], signBitAsCard], REAL]]; }; <> <<>> AbsLe: PROC [x, y: REAL] RETURNS [BOOL] = INLINE { RETURN [LOOPHOLE[Abs[x], CARD] <= LOOPHOLE[Abs[y], CARD]]; }; AbsLt: PROC [x, y: REAL] RETURNS [BOOL] = INLINE { RETURN [LOOPHOLE[Abs[x], CARD] < LOOPHOLE[Abs[y], CARD]]; }; AbsGe: PROC [x, y: REAL] RETURNS [BOOL] = INLINE { RETURN [LOOPHOLE[Abs[x], CARD] >= LOOPHOLE[Abs[y], CARD]]; }; AbsGt: PROC [x, y: REAL] RETURNS [BOOL] = INLINE { RETURN [LOOPHOLE[Abs[x], CARD] > LOOPHOLE[Abs[y], CARD]]; }; AbsEq: PROC [x, y: REAL] RETURNS [BOOL] = INLINE { RETURN [LOOPHOLE[Abs[x], CARD] = LOOPHOLE[Abs[y], CARD]]; }; AbsNe: PROC [x, y: REAL] RETURNS [BOOL] = INLINE { RETURN [LOOPHOLE[Abs[x], CARD] # LOOPHOLE[Abs[y], CARD]]; }; AbsMax: PROC [x, y: REAL] RETURNS [REAL] = INLINE { RETURN [LOOPHOLE[MAX[LOOPHOLE[Abs[x], CARD], LOOPHOLE[Abs[y], CARD]]]]; }; AbsMin: PROC [x, y: REAL] RETURNS [REAL] = INLINE { RETURN [LOOPHOLE[MIN[LOOPHOLE[Abs[x], CARD], LOOPHOLE[Abs[y], CARD]]]]; }; END.