
{-# LANGUAGE QuasiQuotes #-}
{-@ LIQUID "--no-termination "@-}
{-@ LIQUID "--short-names "@-}
{-@ LIQUID "--diff "@-}



import LiquidHaskell


import Language.Haskell.Liquid.Prelude (liquidError)
import Data.IORef
import Control.Applicative ((<$>))
import qualified Data.Map as M

[lq| type Upto N = {v:Nat | v < N} |]

---------------------------------------------------------------------------
[lq| search :: String -> str:String -> Maybe (Upto (len str)) |]
---------------------------------------------------------------------------
search :: String -> String -> Maybe Int
search pat str = kmpSearch (ofList pat) (ofList str)


-------------------------------------------------------------
-- | Do the Search ------------------------------------------
-------------------------------------------------------------

[lq| kmpSearch :: (Eq a) => p:Arr a -> s:Arr a -> Maybe (Upto (alen s)) |]
kmpSearch p@(A m _) s@(A n _) = go 0 0
  where
    t              = kmpTable p
    go i j
      | i >= n     = Nothing
      | j >= m     = Just (i - m)
      | s!i == p!j = go (i+1) (j+1)
      | j == 0     = go (i+1) j
      | otherwise  = go i     (t!j)


-------------------------------------------------------------
-- | Make Table ---------------------------------------------
-------------------------------------------------------------

kmpTable p@(A m _) = go t 1 0
  where
    t              = new m (\_ -> 0)
    go t i j
      | i >= m - 1 = t

      | p!i == p!j = let i' = i + 1
                         j' = j + 1
                         t' = set t i' j'
                     in go t' i' j'

      | (j == 0)   = let i' = i + 1
                         t' = set t i' 0
                     in go t' i' j

      | otherwise  = let j' = t ! j
                     in go t i j'


-------------------------------------------------------------
-- | A Pure Array -------------------------------------------
-------------------------------------------------------------

data Arr a   = A { alen :: Int
                 , aval :: Int -> a
                 }

[lq| data Arr a <p :: Int -> a -> Prop>
             = A { alen :: Nat
                 , aval :: i:Upto alen -> a<p i>
                 }
  |]


[lq| new :: forall <p :: Int -> a -> Prop>.
             n:Nat -> (i:Upto n -> a<p i>) -> {v: Arr<p> a | alen v = n}
  |]
new n v = A { alen = n
            , aval = \i -> if (0 <= i && i < n)
                             then v i
                             else liquidError "Out of Bounds!"
            }

[lq| (!) :: forall <p :: Int -> a -> Prop>.
             a:Arr<p> a -> i:Upto (alen a) -> a<p i>
  |]

(A _ f) ! i = f i

[lq| set :: forall <p :: Int -> a -> Prop>.
             a:Arr<p> a -> i:Upto (alen a) -> a<p i> -> {v:Arr<p> a | alen v = alen a}
  |]
set a@(A _ f) i v = a { aval = \j -> if (i == j) then v else f j }


[lq| ofList :: xs:[a] -> {v:Arr a | alen v = len xs} |]
ofList xs = new n f
  where
    n     = length xs
    m     = M.fromList $ zip [0..] xs
    f i   = (M.!) m i

[lq| map :: (a -> b) -> a:Arr a -> {v:Arr b | alen v = alen a} |]
map f a@(A n z) = A n (f . z)



-------------------------------------------------------------
-- | An Imperative Array ------------------------------------
-------------------------------------------------------------

data IOArr a = IOA { size :: Int
                   , pntr :: IORef (Arr a)
                   }

[lq| data IOArr a <p :: Int -> a -> Prop>
      = IOA { size :: Nat
            , pntr :: IORef ({v:Arr<p> a | alen v = size})
            }
  |]


[lq| newIO :: forall <p :: Int -> a -> Prop>.
               n:Nat -> (i:Upto n -> a<p i>) -> IO ({v: IOArr<p> a | size v = n})
  |]
newIO n f = IOA n <$> newIORef (new n f)

[lq| getIO :: forall <p :: Int -> a -> Prop>.
              a:IOArr<p> a -> i:Upto (size a) -> IO (a<p i>)
  |]
getIO a@(IOA sz p) i
  = do arr   <- readIORef p
       return $ (arr ! i)

[lq| setIO :: forall <p :: Int -> a -> Prop>.
              a:IOArr<p> a -> i:Upto (size a) -> a<p i> -> IO ()
  |]
setIO a@(IOA sz p) i v
  = do arr     <- readIORef p
       let arr' = set arr i v
       writeIORef p arr'
