content: {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--short-names"    @-}
  
  module Kmp (search) where
  
  import Language.Haskell.Liquid.Prelude (liquidError)
  
  search pat str = kmpSearch (ofList pat) (ofList str) 
  
  -------------------------------------------------------------
  -- | Do the Search ------------------------------------------
  -------------------------------------------------------------
  
  kmpSearch p@(A m _) s@(A n _) = go 0 0 
    where
      t              = kmpTable p
      go i j
        | j >= m     = i - m
        | i >= n     = (-1)
        | s!i == p!j = go (i+1) (j+1)
        | j == 0     = go (i+1) j
        | otherwise  = go i     (t!j) 
  
  
  -------------------------------------------------------------
  -- | Make Table ---------------------------------------------
  -------------------------------------------------------------
  
  {-@ kmpTable :: (Eq a) => p:Arr a -> {v:DArr Nat | alen v = alen p} @-}
  kmpTable p@(A m _) = go 1 0 t
    where
      t              = new m (\_ -> 0)
      go i j t
        | i >= m - 1 = t
  
        | p!i == p!j = let i' = i + 1
                           j' = j + 1
                           t' = wipe $ set t i' j'
                       in go i' j' t'           
      
        | (j == 0)   = let i' = i + 1
                           t' = wipe $ set t i' 0
                       in go i' j t'
                               
        | otherwise  = let j' = t ! j
                       in go i j' t 
  
  {-@ wipe :: a:DArr Nat -> {v:DArr Nat | alen v = alen a} @-}
  wipe :: Arr Int -> Arr Int
  wipe = undefined
  
  
  {-@ type DArr a = Arr<{\k v -> v <= k}> a @-}
  {-@ type Upto N = {v:Nat | v < N} @-} 
  
  -------------------------------------------------------------
  -- | An Array type ------------------------------------------
  -------------------------------------------------------------
  
  data Arr a = A { alen :: Int
                 , aval :: Int -> a
                 }
  
  {-@ data Arr a <rng :: Int -> a -> Bool>
        = A { alen :: Nat 
            , aval :: i:Upto alen -> a<rng i>
            }
    @-}
  
  
  {-@ new :: forall <p :: Int -> a -> Bool>.
               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!"
              }
  
  {-@ (!) :: forall <p :: Int -> a -> Bool>.
               a:Arr<p> a -> i:Upto (alen a) -> a<p i>
    @-}
  
  (A _ f) ! i = f i
    
  {-@ set :: forall <p :: Int -> a -> Bool>.
               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 }
  
  
  {-@ ofList :: xs:[a] -> {v:Arr a | alen v = len xs} @-} 
  ofList :: [a] -> Arr a
  ofList = undefined
  
  