liquidhaskell-0.8.10.7: benchmarks/text-0.11.2.3/Data/Text/Lazy/Search.hs
{-@ LIQUID "--pruneunsorted" @-}
{-# LANGUAGE BangPatterns, ScopedTypeVariables #-}
-- |
-- Module : Data.Text.Lazy.Search
-- Copyright : (c) 2009, 2010 Bryan O'Sullivan
--
-- License : BSD-style
-- Maintainer : bos@serpentine.com, rtomharper@googlemail.com,
-- duncan@haskell.org
-- Stability : experimental
-- Portability : GHC
--
-- Fast substring search for lazy 'Text', based on work by Boyer,
-- Moore, Horspool, Sunday, and Lundh. Adapted from the strict
-- implementation.
module Data.Text.Lazy.Search
(
indices
) where
import qualified Data.Text.Array as A
import Data.Int (Int64)
import Data.Word (Word16, Word64)
import qualified Data.Text.Internal as T
import Data.Text.Fusion.Internal (PairS(..))
import Data.Text.Lazy.Internal (Text(..), foldlChunks)
import Data.Bits ((.|.), (.&.))
import Data.Text.UnsafeShift (shiftL)
--LIQUID
-- import qualified Data.Text
-- import Data.Text.Array (Array(..), MArray(..))
-- import qualified Data.Text.Fusion.Internal
-- import qualified Data.Text.Fusion.Size
-- import qualified Data.Text.Internal
-- import qualified Data.Text.Private
-- import qualified Data.Text.Search
-- import qualified Data.Text.Unsafe
import Data.Text.Lazy.Internal (foldrChunks)
import qualified Data.Text.Fusion.Size as TODO_REBARE
import qualified Data.Text as TODO_REBARE
-- import qualified Data.Word
-- import Data.Int (Int32)
import Language.Haskell.Liquid.Prelude
import Language.Haskell.Liquid.Foreign
-- | /O(n+m)/ Find the offsets of all non-overlapping indices of
-- @needle@ within @haystack@.
--
-- This function is strict in @needle@, and lazy (as far as possible)
-- in the chunks of @haystack@.
--
-- In (unlikely) bad cases, this algorithm's complexity degrades
-- towards /O(n*m)/.
{-@ type IdxList a N = [a]<{\ix iy -> (ix+N) <= iy}> @-}
{-@ indices :: pat:Text -> src:Text
-> IdxList {v:Nat64 | v <= ((ltlen src) - (ltlen pat))} (ltlen pat)
@-}
indices :: Text -- ^ Substring to search for (@needle@)
-> Text -- ^ Text to search in (@haystack@)
-> [Int64]
indices needle@(Chunk n ns) _haystack@(Chunk k@(T.Text _ _ klen) ks) =
if nlen <= 0 then []
else if nlen == 1 then indicesOne (nindex 0) _haystack Empty k ks 0
else advance needle _haystack Empty k ks 0 0
where
-- advance x@(T.Text _ _ l) xs = scan
-- where
-- scan !g !i
-- | i >= m = case xs of
-- Empty -> []
-- Chunk y ys -> advance y ys g (i-m)
-- | lackingHay (i + nlen) x xs = []
-- | c == z && candidateMatch 0 = g : scan (g+nlen) (i+nlen)
-- | otherwise = scan (g+delta) (i+delta)
-- where
-- m = fromIntegral l
-- c = hindex (i + nlast)
-- delta | nextInPattern = nlen + 1
-- | c == z = skip + 1
-- | otherwise = 1
-- nextInPattern = mask .&. swizzle (hindex (i+nlen)) == 0
-- candidateMatch !j
-- | j >= nlast = True
-- | hindex (i+j) /= nindex j = False
-- | otherwise = candidateMatch (j+1)
-- hindex = index x xs
nlen = wordLength needle
nlast = nlen - 1
nindex = index n ns
-- z = foldlChunks fin 0 needle
-- --LIQUID fin param needs to be non-empty
-- where fin _ (T.Text farr foff flen) = A.unsafeIndex farr (foff+flen-1)
-- (mask :: Word64) :*: skip = buildTable n ns 0 0 0 (nlen-2)
-- swizzle w = 1 `shiftL` (fromIntegral w .&. 0x3f)
-- buildTable (T.Text xarr xoff xlen) xs = go
-- where
-- go !(g::Int64) !i !msk !skp
-- | i >= xlast = case xs of
-- Empty -> (msk .|. swizzle z) :*: skp
-- Chunk y ys -> buildTable y ys g 0 msk' skp'
-- | otherwise = go (g+1) (i+1) msk' skp'
-- where c = A.unsafeIndex xarr (xoff+i)
-- msk' = msk .|. swizzle c
-- skp' | c == z = nlen - g - 2
-- | otherwise = skp
-- xlast = xlen - 1
-- -- | Check whether an attempt to index into the haystack at the
-- -- given offset would fail.
-- lackingHay q = go 0
-- where
-- go p (T.Text _ _ l) ps = p' < q && case ps of
-- Empty -> True
-- Chunk r rs -> go p' r rs
-- where p' = p + fromIntegral l
indices _ _ = []
{-@ advance :: pat:{v:Text | (ltlen v) > 1}
-> src:LTextNE
-> ts0:LTextLE src
-> x:{v:TextNE | (tlen v) <= (ltlen src)}
-> xs:{v:Text | (((ltlen v) + (tlen x)) = ((ltlen src) - (ltlen ts0)))}
-> i:Nat64
-> g:{v:Int64 | (v - i) = (ltlen ts0)}
-> IdxList {v:Int64 | (BtwnI (v) (g) ((ltlen src) - (ltlen pat)))} (ltlen pat)
@-}
advance :: Text -> Text -> Text -> T.Text -> Text -> Int64 -> Int64 -> [Int64]
advance needle haystack ts0 x xs i g
= advance_scan needle haystack ts0 x xs i g (wordLength haystack - g + 1)
{-@ advance_scan :: pat:{v:Text | (ltlen v) > 1}
-> src:LTextNE
-> ts0:LTextLE src
-> x:{v:TextNE | (tlen v) <= (ltlen src)}
-> xs:{v:Text | (((ltlen v) + (tlen x)) = ((ltlen src) - (ltlen ts0)))}
-> i:Nat64
-> g:{v:Int64 | (v - i) = (ltlen ts0)}
-> {v:Int64 | v = ((ltlen src) - g) + 1}
-> IdxList {v:Int64 | (BtwnI (v) (g) ((ltlen src) - (ltlen pat)))} (ltlen pat)
@-}
{-@ decrease advance_scan 5 8 @-}
advance_scan :: Text -> Text -> Text -> T.Text -> Text -> Int64 -> Int64 -> Int64 -> [Int64]
advance_scan needle@(Chunk n ns) src ts0 x@(T.Text _ _ l) xs !i !g dec =
if i >= m then case xs of
Empty -> []
Chunk y ys -> advance_scan needle src (Chunk x ts0) y ys (i-m) g dec
else if lackingHay (i + nlen) x xs then []
else let d = delta nlen skip c z nextInPattern
c = index x xs (i + nlast)
nextInPattern = mask .&. swizzle (index x xs (i+nlen)) == 0
candidateMatch (d :: Int64) !j
= if j >= nlast then True
else if index x xs (i+j) /= index n ns j then False
else candidateMatch (d-1) (j+1)
--LIQUID candidateMatch !j
--LIQUID | j >= nlast = True
--LIQUID | index x xs (i+j) /= index n ns j = False
--LIQUID | otherwise = candidateMatch (j+1)
in if c == z && candidateMatch nlast 0
then g : advance_scan needle src ts0 x xs (i+nlen) (g+nlen) (dec-nlen)
else advance_scan needle src ts0 x xs (i+d) (g+d) (dec-d)
where
nlen = wordLength needle
nlast = nlen - 1
(mask :: Word64) :*: skip = buildTable z nlen Empty n ns 0 0 0 (nlen-2) nlen
z = foldlChunks fin 0 needle
where fin _ (T.Text farr foff flen) = A.unsafeIndex farr (foff+flen-1)
m = fromIntegral l
-- | Check whether an attempt to index into the haystack at the
-- given offset would fail.
{-@ lackingHay :: q:Nat64 -> t:TextNE -> ts:Text
-> {v:Bool | (v <=> (q > ((tlen t) + (ltlen ts))))}
@-}
lackingHay :: Int64 -> T.Text -> Text -> Bool
lackingHay q t ts = lackingHay_go q 0 t ts
{-@ lackingHay_go :: q:Nat64 -> p:Nat64 -> t:TextNE -> ts:Text
-> {v:Bool | (v <=> (q > (p + (tlen t) + (ltlen ts))))}
@-}
{-@ decrease lackingHay_go 4 @-}
lackingHay_go :: Int64 -> Int64 -> T.Text -> Text -> Bool
lackingHay_go q p (T.Text _ _ l) Empty = q > (p + fromIntegral l)
lackingHay_go q p (T.Text _ _ l) (Chunk r rs) = let p' = p + fromIntegral l
in q > p' && lackingHay_go q p' r rs
{-@ delta :: nlen:{v:Int64 | v > 1} -> skip:{v:Nat64 | v <= nlen}
-> Word16 -> Word16 -> Bool
-> {v:Int64 | (BtwnI v 1 (nlen + 1))}
@-}
delta :: Int64 -> Int64 -> Word16 -> Word16 -> Bool -> Int64
delta nlen skip c z nextInPattern =
if nextInPattern then nlen + 1
else if c == z then skip + 1
else 1
swizzle w = 1 `shiftL` (fromIntegral w .&. 0x3f)
{-@ buildTable :: Word16
-> nlen:{v:Int64 | v > 1}
-> ts0:{v:Text | (BtwnI (ltlen v) 0 nlen)}
-> t:{v:T.Text | (BtwnEI (tlen v) 0 nlen)}
-> ts:{v:Text | (((ltlen v) + (tlen t)) = (nlen - (ltlen ts0)))}
-> i:TValidI t
-> g:{v:Nat64 | v <= ((ltlen ts0) + i)}
-> Word64
-> {v:Nat64 | v < nlen}
-> d:{v:Nat64 | nlen = (i + v)}
-> PairS Word64 {v:Nat64 | v < nlen}
@-}
{-@ decrease buildTable 5 10 @-}
buildTable :: Word16 -> Int64 -> Text -> T.Text -> Text -> Int -> Int64 -> Word64 -> Int64 -> Int64
-> PairS Word64 Int64
buildTable z nlen ts0 t@(T.Text xarr xoff xlen) xs !i !(g::Int64) !msk !skp (d :: Int64) =
if i >= xlast then case xs of
Empty -> (msk .|. swizzle z) :*: skp
Chunk y ys -> let msk' = msk .|. swizzle c
skp' = if c == z then nlen - g - 2 else skp
--LIQUID skp' | c == z = nlen - g - 2
--LIQUID | otherwise = skp
in buildTable z nlen (Chunk t ts0) y ys 0 g msk' skp' nlen
else let msk' = msk .|. swizzle c
skp' = if c == z then nlen - g - 2 else skp
--LIQUID skp' | c == z = nlen - g - 2
--LIQUID | otherwise = skp
in buildTable z nlen ts0 t xs (i+1) (g+1) msk' skp' (d-1)
where c = A.unsafeIndex xarr (xoff+i)
xlast = xlen - 1
-- | Fast index into a partly unpacked 'Text'. We take into account
-- the possibility that the caller might try to access one element
-- past the end.
{-@ index :: t:TextNE -> ts:Text -> i:{v:Nat64 | v <= ((tlen t) + (ltlen ts))}
-> Word16
@-}
{-@ decrease index 2 @-}
index :: T.Text -> Text -> Int64 -> Word16
index (T.Text arr off len) xs !i =
if j < len then A.unsafeIndex arr (off+j)
else case xs of
Empty ->
-- out of bounds, but legal
if j == len then 0
-- should never happen, due to lackingHay above
else liquidError "index"
Chunk c cs -> index c cs (i-fromIntegral len)
where j = fromIntegral i
-- | A variant of 'indices' that scans linearly for a single 'Word16'.
{-@ indicesOne :: Word16
-> t0:Text
-> ts0:LTextLE t0
-> t:TextNE
-> ts:{v:Text | (((ltlen v) + (tlen t)) = ((ltlen t0) - (ltlen ts0)))}
-> i:{v:Int64 | v = (ltlen ts0)}
-> [{v:Int64 | (Btwn (v) (i) (ltlen t0))}]<{\ix iy -> ix < iy}>
@-}
indicesOne :: Word16 -> Text -> Text -> T.Text -> Text -> Int64 -> [Int64]
--LIQUID indicesOne c = chunk
--LIQUID where
--LIQUID chunk !i (T.Text oarr ooff olen) os = go 0
--LIQUID where
--LIQUID go h | h >= olen = case os of
--LIQUID Empty -> []
--LIQUID Chunk y ys -> chunk (i+fromIntegral olen) y ys
--LIQUID | on == c = i + fromIntegral h : go (h+1)
--LIQUID | otherwise = go (h+1)
--LIQUID where on = A.unsafeIndex oarr (ooff+h)
indicesOne c t0 ts0 t@(T.Text _ _ l) os !i = indicesOne_go c t0 ts0 t os i 0 l
{-@ decrease indicesOne_go 5 8 @-}
{-@ indicesOne_go :: Word16
-> t0:Text
-> ts0:LTextLE t0
-> t:{v:TextNE | (tlen v) <= (ltlen t0)}
-> ts:{v:Text | (((ltlen v) + (tlen t)) = ((ltlen t0) - (ltlen ts0)))}
-> i:{v:Int64 | v = (ltlen ts0)}
-> h:{v:Nat | v <= (tlen t)}
-> {v:Int|v = ((tlen t) - h)}
-> [{v:Int64 | (Btwn (v) (i+h) (ltlen t0))}]<{\ix iy -> ix < iy}>
@-}
indicesOne_go :: Word16 -> Text -> Text -> T.Text -> Text -> Int64 -> Int -> Int -> [Int64]
indicesOne_go c t0 ts0 t@(T.Text oarr ooff olen) os !i h d =
if h >= olen then case os of
Empty -> []
Chunk y@(T.Text _ _ l) ys ->
indicesOne_go c t0 (Chunk t ts0) y ys (i+fromIntegral olen) 0 l
else let on = A.unsafeIndex oarr (ooff+h)
in if on == c
then i + fromIntegral h : indicesOne_go c t0 ts0 t os i (h+1) (d-1)
else indicesOne_go c t0 ts0 t os i (h+1) (d-1)
-- | The number of 'Word16' values in a 'Text'.
{-@ wordLength :: t:Text -> {v:Nat64 | v = (ltlen t)} @-}
wordLength :: Text -> Int64
--LIQUID wordLength = foldlChunks sumLength 0
--LIQUID where sumLength i (T.Text _ _ l) = i + fromIntegral l
wordLength = foldrChunks sumLength 0
{-@ sumLength :: ts:Text -> t:T.Text -> i:Int64 -> {v:Int64 | v = ((tlen t) + i)} @-}
sumLength :: Text -> T.Text -> Int64 -> Int64
sumLength _ (T.Text _ _ l) i = i + fromIntegral l
--LIQUID emptyError :: String -> a
--LIQUID emptyError fun = error ("Data.Text.Lazy.Search." ++ fun ++ ": empty input")