content: {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--short-names"    @-}
  
  module KmpVec (search) where
  
  import Language.Haskell.Liquid.Prelude (liquidError)
  import Data.Vector
  import Data.Vector.Mutable (write)
  import Prelude hiding (length, replicate)
  
  {-@ type Idx X = {v:Nat | v < vlen X} @-}
  
  
  search pat str = kmpSearch (fromList pat) (fromList str) 
  
  -------------------------------------------------------------
  -- | Do the Search ------------------------------------------
  -------------------------------------------------------------
  
  kmpSearch p s      = go 0 0 
    where
      t              = kmpTable p
      m              = length p
      n              = length s
      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:Vector a -> {v:Vector Nat | vlen v = vlen p} @-}
  kmpTable p         = go 1 0 t
    where
      m              = length p
      t              = replicate m 0 
      go i j t
        | i >= m - 1 = t
  
        | p!i == p!j = let i' = i + 1
                           j' = j + 1
                           t' = set t i' j'
                       in go i' j' t'           
      
        | (j == 0)   = let i' = i + 1
                           t' = set t i' 0
                       in go i' j t'
                               
        | otherwise  = let j' = t ! j
                       in go i j' t 
  
  
  {-@ type Upto N = {v:Nat | v < N} @-} 
  
  {-@ set :: a:Vector a -> i:Idx a -> a -> {v:Vector a | vlen v = vlen a} @-}
  set :: Vector a -> Int -> a -> Vector a
  set = undefined
  
  