{-@ 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 _ = undefined -- error "Failed Dynamic Check!"