SIGNATURE SmallReal

-- single precision real numbers

IMPORT  Real    ONLY real

SORT sreal

FUN  0  1  2  3  4  5  6  7  8  9 
    10 11 12 13 14 15 16 17 18 19 
    20 21 22 23 24 25 26 27 28 29 
    30 31 32 
    64 128 256 512 1024
    100 1000 10000 100000 1000000
    min max
    eps         -- smallest number, with 1 + eps > eps
    pi e            : sreal             -- pi/e

FUN + - * /         : sreal**sreal->sreal

FUN pow             : sreal**sreal->sreal       -- power function
    exp sqrt                            -- exponent ex/square root
    ln log          : sreal->sreal      -- natural/decimal logarithm

FUN - abs ceil floor sign: sreal->sreal
                      -- ceil(x)  == min{n in Int|n >=x}
                      -- floor(x) == max{n in Int|n <=x}

FUN min max         : sreal**sreal->sreal
FUN pos? neg? zero? : sreal->bool

FUN <= = >= < > |=  : sreal**sreal->bool

FUN sin cos tan 
    arcsin arccos 
    arctan          : sreal->sreal
    arctan2         : sreal**sreal->sreal
                      -- arcsin(x)==y <=> 
                      -- sin(y)=x and y in [-pi/2,pi/2]   PROVIDED x in [-1,1]
                      -- arccos(x)==y <=> 
                      -- cos(y)=x and y in [0,pi]  PROVIDED x in [-1,1]
                      -- arctan(x)==y <=> tan(y)=x and y in [-pi/2,pi/2]

FUN sinh cosh tanh  : sreal->sreal      
                      -- hyperbolic trigonometric functions

FUN !               : denotation->sreal 
    -- real number denotation
    -- must match regexp [+|-](0|1|..|9)*[.(0|1|..|9)*][e[+|-](0|1|..|9)+]
    -- otherwise undefined

FUN asReal          : sreal -> real

/$ BRACKET RIGHT [+,- : sreal**sreal->sreal] [*,/] $/
/$ BRACKET LEFT [*,/] [+,- : sreal**sreal->sreal] $/
/$ BRACKET LEFT [+,- : sreal**sreal->sreal] [+,- : sreal**sreal->sreal] $/
/$ BRACKET LEFT [*,/] [*,/] $/