module TFwH.Chap03
(
floorS
, floor0n
, floor0p
, floor1
, shrink
, choose
, bound
, lower
, upper
, Nat (..)
) where
import Prelude hiding (floor)
import Numeric
lt :: Float -> Integer -> Bool
x `lt` n = x < fromInteger n
leq :: Integer -> Float -> Bool
m `leq` x = fromInteger m <= x
floorS :: Float -> Integer
floorS = read . takeWhile (/= '.') . show
floor0n :: Float -> Integer
floor0n x = until (`leq` x) (subtract 1) (-1)
floor0p :: Float -> Integer
floor0p x = until (x `lt`) (+ 1) 1 - 1
floor0 x = if x < 0
then until (`leq` x) (subtract 1) (-1)
else until (x `lt`) (+ 1) 1 - 1
floor1 :: Float -> Integer
floor1 x = fst (until unit (shrink x) (bound x))
where
unit (m, n) = m + 1 == n
type Interval = (Integer, Integer)
shrink :: Float -> Interval -> Interval
shrink x (m, n) = if p `leq` x then (p, n) else (m, p)
where
p = choose (m, n)
choose :: Interval -> Integer
choose (m, n) = (m + n) `div` 2
bound :: Float -> Interval
bound x = (lower x, upper x)
lower :: Float -> Integer
lower x = until (`leq` x) (* 2) (-1)
upper :: Float -> Integer
upper x = until (x `lt`) (*2) 1
data Nat = Zero | Succ Nat
deriving (Eq, Ord, Show)
instance Num Nat where
m + Zero = m
m + Succ n = Succ (m + n)
m * Zero = Zero
m * Succ n = m * n + m
abs n = n
signum Zero = Zero
signum (Succ n) = Succ Zero
m - Zero = m
Zero - Succ n = Zero
Succ m - Succ n = m - n
fromInteger x
| x <= 0 = Zero
| otherwise = Succ (fromInteger (x - 1))