content: {-@ LIQUID "--pruneunsorted" @-}
  
  {-# LANGUAGE BangPatterns, ScopedTypeVariables #-}
  
  -- |
  -- Module      : Data.Text.Search
  -- Copyright   : (c) Bryan O'Sullivan 2009
  --
  -- License     : BSD-style
  -- Maintainer  : bos@serpentine.com, rtomharper@googlemail.com,
  --               duncan@haskell.org
  -- Stability   : experimental
  -- Portability : GHC
  --
  -- Fast substring search for 'Text', based on work by Boyer, Moore,
  -- Horspool, Sunday, and Lundh.
  --
  -- References:
  --
  -- * R. S. Boyer, J. S. Moore: A Fast String Searching Algorithm.
  --   Communications of the ACM, 20, 10, 762-772 (1977)
  --
  -- * R. N. Horspool: Practical Fast Searching in Strings.  Software -
  --   Practice and Experience 10, 501-506 (1980)
  --
  -- * D. M. Sunday: A Very Fast Substring Search Algorithm.
  --   Communications of the ACM, 33, 8, 132-142 (1990)
  --
  -- * F. Lundh: The Fast Search Algorithm.
  --   <http://effbot.org/zone/stringlib.htm> (2006)
  
  module Data.Text.Search
      (
        indices
      --LIQUID
      , T(..)
      ) where
  
  import qualified Data.Text.Array as A
  import Data.Word (Word64)
  import Data.Text.Internal (Text(..))
  import Data.Bits ((.|.), (.&.))
  import Data.Text.UnsafeShift (shiftL)
  
  --LIQUID
  import Data.Word (Word16)
  -- import Language.Haskell.Liquid.Prelude
  
  --LIQUID FIXME: we don't currently parse the `:*` syntax used originally
  data T = {-# UNPACK #-} !Word64 `T` {-# UNPACK #-} !Int
  
  {-@ qualif Foo(v:int,x:int): v <= x + 1 @-}
  {-@ qualif Diff(v:int,l:int,d:int): v = (l - d) + 1 @-}
  
  {-@ measure tskip :: T -> Int
        tskip (T mask skip) = skip
    @-}
  
  -- | /O(n+m)/ Find the offsets of all non-overlapping indices of
  -- @needle@ within @haystack@.  The offsets returned represent
  -- locations in the low-level array.
  --
  -- In (unlikely) bad cases, this algorithm's complexity degrades
  -- towards /O(n*m)/.
  {-@ indices :: needle:Text -> haystack:Text
              -> [(TValidIN haystack (tlen needle))]<{\ix iy -> (ix+(tlen needle)) <= iy}>
    @-}
  indices :: Text                -- ^ Substring to search for (@needle@)
          -> Text                -- ^ Text to search in (@haystack@)
          -> [Int]
  indices _needle@(Text narr noff nlen) _haystack@(Text harr hoff hlen)
      --LIQUID switched first two guards, need to consider whether this is problematic..
      = if      nlen <= 0 || ldiff < 0 then []
        else if nlen == 1              then scanOne (index _needle 0)
        else
          --LIQUID pushing definitions in to prove safety!
               {- LIQUID WITNESS -}
          let scan (d :: Int) !i
                = if i > ldiff then []
                  else
                    let nlast = nlen - 1
                        z     = index _needle nlast
                        c = index _haystack (i + nlast)
                        {- LIQUID WITNESS -}
                        candidateMatch (d :: Int) !j
                            = if j >= nlast               then True
                              else if index _haystack (i+j) /= index _needle j then False
                              else candidateMatch (d-1) (j+1)
                        delta = if nextInPattern then nlen + 1
                                else if c == z   then skip + 1
                                else 1
                              where nextInPattern = mask .&. swizzle (index' _haystack (i+nlen)) == 0
                                    !(mask `T` skip)       = buildTable (nlen-1) _needle 0 0 (nlen-2)
                     in if c == z && candidateMatch nlast 0
                        then i : scan (d-nlen) (i + nlen)
                        else scan (d-delta) (i + delta)
          in scan (hlen+1) 0
    where
      ldiff    = hlen - nlen
      -- nlast    = nlen - 1
      -- z        = nindex nlast
      -- nindex k = A.unsafeIndex narr (noff+k)
      -- hindex k = A.unsafeIndex harr (hoff+k)
      -- hindex' k | k == hlen  = 0
      --           | otherwise = A.unsafeIndex harr (hoff+k)
      -- buildTable !i !msk !skp
      --     | i >= nlast           = (msk .|. swizzle z) :* skp
      --     | otherwise            = buildTable (i+1) (msk .|. swizzle c) skp'
      --     where c                = nindex i
      --           skp' | c == z    = nlen - i - 2
      --                | otherwise = skp
      -- swizzle k = 1 `shiftL` (fromIntegral k .&. 0x3f)
      -- scan !i
      --     | i > ldiff                  = []
      --     | c == z && candidateMatch 0 = i : scan (i + nlen)
      --     | otherwise                  = scan (i + delta)
      --     where c = hindex (i + nlast)
      --           candidateMatch !j
      --                 | j >= nlast               = True
      --                 | hindex (i+j) /= nindex j = False
      --                 | otherwise                = candidateMatch (j+1)
      --           delta | nextInPattern = nlen + 1
      --                 | c == z        = skip + 1
      --                 | otherwise     = 1
      --             where nextInPattern = mask .&. swizzle (hindex' (i+nlen)) == 0
      --           !(mask :* skip)       = buildTable 0 0 (nlen-2)
      scanOne c = loop hlen 0
        {- LIQUID WITNESS -}
          where loop (d :: Int) !i = if i >= hlen     then []
                                     else if index _haystack i == c then i : loop (d-1) (i+1)
                                     else loop (d-1) (i+1)
  {- INLINE indices #-}
  
  {-@ buildTable :: d:Nat
                 -> pat:{v:Text | (tlen v) > 1}
                 -> i:{v:Nat | ((v < (tlen pat)) && (v = (tlen pat) - 1 - d))}
                 -> Word64
                 -> skp:{v:Nat | v < (tlen pat)}
                 -> {v:T | (Btwn (tskip v) 0 (tlen pat))}
    @-}
  buildTable :: Int -> Text -> Int -> Word64 -> Int -> T
  buildTable d pat@(Text narr noff nlen) !i !msk !skp
      = if i >= nlast          then (msk .|. swizzle z) `T` skp
        else                   let skp' = if c == z    then nlen - i - 2
                                          else skp
                               in buildTable (d-1) pat (i+1) (msk .|. swizzle c) skp'
      where nlast            = nlen - 1
            z                = index pat nlast
            c                = index pat i
  
  swizzle k = 1 `shiftL` (fromIntegral k .&. 0x3f)
  
  {-@ index :: t:Text -> k:TValidI t -> Word16 @-}
  index :: Text -> Int -> Word16
  index (Text arr off len) k = A.unsafeIndex arr (off+k)
  
  {-@ index' :: t:Text -> k:{v:Nat | v <= (tlen t)} -> Word16 @-}
  index' (Text arr off len) k
      = if k == len then 0
        else A.unsafeIndex arr (off+k)
  