content: {-@ LIQUID "--short-names"    @-}
  
  module PointDist 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!"
  
  
  