{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
-- {-# OPTIONS_GHC -fplugin=LiquidHaskell -fplugin-opt=LiquidHaskell:--verbose #-}

module Bresenham where

{-@

data State = State {
  state_m :: Double,
  state_dx :: {dx':Int | 0 < dx'},
  state_dy :: {dy':Int | 0 <= dy' && dy' <= state_dx && state_m * state_dx == dy'},
  state_x :: {x':Int | x' >= 0},
  state_y :: Int,
  state_d :: Int,
}

@-}
data State = State {
  state_m :: Double,
  state_dx :: Int,
  state_dy :: Int,
  state_x :: Int,
  state_y :: Int,
  state_d :: Int
  }

{-@ measure state_y_correct @-}
state_y_correct :: State -> Bool
state_y_correct (State m _ _ x y _) = (fromIntegral y) - 0.5 <= m * (fromIntegral x) && (fromIntegral y) + 0.5 > m * (fromIntegral x)

{-@ measure state_d_correct @-}
state_d_correct :: State -> Bool
state_d_correct (State _ dx dy x y d) = d == 2 * dy * (x + 1) - (2 * y * dx) - dx

{-@ type ValidState = {st:State | state_y_correct st && state_d_correct st} @-}
type ValidState = State

{-@ step :: st:ValidState -> {st':ValidState | state_x st' == state_x st + 1} @-}
step :: State -> State
step (State m dx dy x y d) =
  if d >= 0
  then
    (State m dx dy (x + 1) (y + 1) (d + ((2 * dy) - (2 * dx))))
  else
    (State m dx dy (x + 1) y (d + (2 * dy)))

{-@ init_state :: m:Double -> {dx:Int | dx > 0} -> {dy:Int | dy < dx && dy > 0 && m * dx == dy} -> ValidState @-}
init_state :: Double -> Int -> Int -> State
init_state m dx dy = State m dx dy x y d
  where
    x = 0
    y = 0
    d = 2 * dy * (x + 1) - (2 * y * dx) - dx


{-@ data Frac = Frac { rate :: Double, numer :: Int, denom :: Int } @-}
data Frac = Frac { rate :: Double, numer :: Int, denom :: Int }

{-@ init_state' :: {dx:Int | dx > 0} -> {dy:Int | dy < dx && dy > 0} -> ValidState @-}
init_state' :: Int -> Int -> ValidState
init_state' dx dy = init_state (rate frac) (numer frac) (denom frac)
  where
    {-@ assume frac :: {v:Frac | (rate v) * (numer v) == (denom v) && (numer v) > 0 && (denom v) < (numer v) && (denom v) > 0} @-}
    frac :: Frac
    frac = Frac ((fromIntegral dy) / (fromIntegral dx)) dx dy