{-@ LIQUID "--short-names" @-}
module Point where
-- | Non-negative numbers:
{-@ type NonNeg = {v:Double | v >= 0.0 } @-}
-- | Non-negative, and zero iff X is zero:
{-@ type PosZ X = {v:NonNeg | X == 0.0 <=> v == 0.0 } @-}
-- | The distance function, STATICALLY guaranteed to satisfy "pre/post"
-- or type spec, assuming no run-time checks fail
{-@ dist :: p1:Point -> p2:Point -> {v:NonNeg | v == 0.0 <=> EqPoint p1 p2} @-}
dist (P x1 y1) (P x2 y2) = d
where
d = root (dx + dy)
dx = square (x1 - x2)
dy = square (y1 - y2)
-- | A Data Type for Points
data Point = P { px :: Double, py::Double }
{-@ data Point = P { px :: Double, py :: Double } @-}
-- | When are two points "equal" ?
{-@ predicate EqPoint P1 P2 = (px P1 == px P2 && py P1 == py P2) @-}
-- | Squaring numbers: DYNAMIC checks establish numerical properties
{-@ square :: x:Double -> PosZ x @-}
square :: Double -> Double
square 0 = 0
square x = assume (xx > 0) xx
where
xx = x * x
{-@ root :: x:NonNeg -> PosZ x @-}
root :: Double -> Double
root 0 = 0
root x = assume (rx > 0) rx
where
rx = sqrt x
-- | Run-time Checks
{-@ assume :: b:_ -> a -> {v:a | b} @-}
assume True x = x
assume False _ = error "Failed Dynamic Check!"