liquidhaskell-0.8.10.7: benchmarks/text-0.11.2.3/Data/Text/Fusion.hs
{-@ LIQUID "--prune-unsorted" @-}
{-@ LIQUID "--eliminate=none" @-}
{-# LANGUAGE BangPatterns, MagicHash #-}
-- |
-- Module : Data.Text.Fusion
-- Copyright : (c) Tom Harper 2008-2009,
-- (c) Bryan O'Sullivan 2009-2010,
-- (c) Duncan Coutts 2009
--
-- License : BSD-style
-- Maintainer : bos@serpentine.com, rtomharper@googlemail.com,
-- duncan@haskell.org
-- Stability : experimental
-- Portability : GHC
--
-- Text manipulation functions represented as fusible operations over
-- streams.
module Data.Text.Fusion
(
-- * Types
Stream(..)
, Step(..)
-- * Creation and elimination
, stream
, unstream
, reverseStream
, length
-- * Transformations
, reverse
-- * Construction
-- ** Scans
, reverseScanr
-- ** Accumulating maps
, mapAccumL
-- ** Generation and unfolding
, unfoldrN
-- * Indexing
, index
, findIndex
, countChar
) where
-- REBARE import Prelude (undefined, Bool(..), Char, Maybe(..), Monad(..), Int, Num(..), Ord(..), ($), (&&), fromIntegral, otherwise)
import Prelude hiding (reverse, length)
import Data.Bits ((.&.))
import Data.Text.Internal (Text(..))
import Data.Text.Private (runText)
import Data.Text.UnsafeChar (ord, unsafeChr, unsafeWrite)
import Data.Text.UnsafeShift (shiftL, shiftR)
import qualified Data.Text.Array as A
import qualified Data.Text.Fusion.Common as S
import Data.Text.Fusion.Internal
import Data.Text.Fusion.Size
import qualified Data.Text.Internal as I
import qualified Data.Text.Encoding.Utf16 as U16
--LIQUID
import GHC.ST (runST)
import Language.Haskell.Liquid.Prelude
default(Int)
{-@ q_ltplus :: a:Int -> b:Int -> {v:Int | v < (a+b)} @-}
q_ltplus :: Int -> Int -> Int
q_ltplus = undefined
{-@ q_lteplus :: a:Int -> b:Int -> {v:Int | (v+a) <= b} @-}
q_lteplus :: Int -> Int -> Int
q_lteplus = undefined
{-@ qualOrd1 :: x:Char -> {v:Int |
((((ordP x) < 65536) => (v = 0))
&& (((ordP x) >= 65536) => (v = 1))) } -> ()
@-}
qualOrd1 :: Char -> Int -> ()
qualOrd1 _ _ = ()
{-@ qualOrd2 :: x:Char -> i:Int -> {v:Int |
((((ordP x) < 65536) => (v = i))
&& (((ordP x) >= 65536) => (v = (i + 1))))} -> ()
@-}
qualOrd2 :: Char -> Int -> Int -> ()
qualOrd2 _ _ _ = ()
{-@ qualOrd3 :: x:Char -> {v:Int |
((((ordP x) < 65536) => (v >= 0))
&& (((ordP x) >= 65536) => (v >= 1))) } -> ()
@-}
qualOrd3 :: Char -> Int -> ()
qualOrd3 _ _ = ()
{-@ qualif MALenLE(v:int, a:A.MArray s): v <= (malen a) @-}
{-@ qualif ALenLE(v:int, a:A.Array): v <= (alen a) @-}
{-@ qualif_Foo1 :: Num b => a:A.MArray a -> {v:(Int, b) | snd v <= maLen a} @-}
qualif_Foo1 :: Num b => A.MArray a -> (Int, b)
qualif_Foo1 = undefined
{-@ qualif_Foo2 :: Num b => a:A.Array -> {v:(Int, b) | snd v <= aLen a} @-}
qualif_Foo2 :: Num b => A.Array -> (Int, b)
qualif_Foo2 = undefined
{-@ qualif Foo(v:int): v >= -1 @-}
{-@ qualif Foo(v:int): v >= 4 @-}
-- | /O(n)/ Convert a 'Text' into a 'Stream Char'.
{-@ assume stream :: t:Data.Text.Internal.Text
-> {v:Data.Text.Fusion.Internal.Stream Char | slen v = tlength t }
@-}
stream :: Text -> Stream Char
stream (Text arr off len) = Stream next off (maxSize len)
where
!end = off+len
next !i
| i >= end = Done
| otherwise =
let n = A.unsafeIndexF arr off len i
in if n >= 0xD800 && n <= 0xDBFF
then let n2 = A.unsafeIndex arr (i + 1)
in Yield (U16.chr2 n n2) (i + 2)
else Yield (unsafeChr n) (i + 1)
--LIQUID | n >= 0xD800 && n <= 0xDBFF = Yield (U16.chr2 n n2) (i + 2)
--LIQUID | otherwise = Yield (unsafeChr n) (i + 1)
--LIQUID where
--LIQUID n = A.unsafeIndex arr i
--LIQUID n2 = A.unsafeIndex arr (i + 1)
{-# INLINE [0] stream #-}
-- | /O(n)/ Convert a 'Text' into a 'Stream Char', but iterate
-- backwards.
{-@ assume reverseStream :: t:Data.Text.Internal.Text
-> {v:Data.Text.Fusion.Internal.Stream Char | (slen v) = (tlength t)}
@-}
reverseStream :: Text -> Stream Char
reverseStream (Text arr off len) = Stream next (off+len-1) (maxSize len)
where
{-# INLINE next #-}
next !i
| i < off = Done
| otherwise =
let n = A.unsafeIndexB arr off len i
in if n >= 0xDC00 && n <= 0xDFFF
then let n2 = A.unsafeIndex arr (i - 1)
in Yield (U16.chr2 n2 n) (i - 2)
else Yield (unsafeChr n) (i - 1)
--LIQUID | n >= 0xDC00 && n <= 0xDFFF = Yield (U16.chr2 n2 n) (i - 2)
--LIQUID | otherwise = Yield (unsafeChr n) (i - 1)
--LIQUID where
--LIQUID n = A.unsafeIndex arr i
--LIQUID n2 = A.unsafeIndex arr (i - 1)
{-# INLINE [0] reverseStream #-}
-- | /O(n)/ Convert a 'Stream Char' into a 'Text'.
--LIQUID FIXME: we should be able to prove these streaming functions terminating
-- but that requires giving a refined Stream type, which requires
-- handling existential types.
{-@ assume unstream :: s:Data.Text.Fusion.Internal.Stream Char
-> {v:Data.Text.Internal.Text | (tlength v) = (slen s)}
@-}
{-@ lazy unstream @-}
unstream :: Stream Char -> Text
unstream (Stream next0 s0 len) = runText $ \done -> do
let mlen = upperBound 4 len
arr0 <- A.new mlen
let outer arr top = loop
where
loop !s !i =
case next0 s of
Done -> done arr i
Skip s' -> loop s' i
Yield x s'
| j >= top -> {-# SCC "unstream/resize" #-} do
let top' = (top + 1) * 2 --LIQUID `shiftL` 1
arr' <- A.new top'
A.copyM arr' 0 arr 0 top
outer arr' top' s i
| otherwise -> do d <- unsafeWrite arr i x
loop s' (i+d)
where j | ord x < 0x10000 = i
| otherwise = i + 1
outer arr0 mlen s0 0
{-# INLINE [0] unstream #-}
{-# RULES "STREAM stream/unstream fusion" forall s. stream (unstream s) = s #-}
-- ----------------------------------------------------------------------------
-- * Basic stream functions
{-@ assume length :: s:Data.Text.Fusion.Internal.Stream Char
-> {v:GHC.Types.Int | v = (slen s)}
@-}
length :: Stream Char -> Int
length = S.lengthI
{-# INLINE[0] length #-}
-- | /O(n)/ Reverse the characters of a string.
{-@ assume reverse :: s:Data.Text.Fusion.Internal.Stream Char
-> {v:Data.Text.Internal.Text | (tlength v) = (slen s)}
@-}
{-@ lazy reverse @-}
reverse :: Stream Char -> Text
reverse (Stream next s len0)
| isEmpty len0 = I.empty
| otherwise = I.textP arr (liquidAssume (off' <= A.aLen arr) off')
(liquidAssume (off' + len' <= A.aLen arr) len')
where
upper k (Exact n) = max k n
upper k (Max n) = max k n
upper k _ = k
len0' = upper 4 len0 --LIQUID INLINE upperBound 4 (larger len0 4)
-- (arr, (off', len'))
arr = fst bloink
off' = fst (snd bloink)
len' = snd (snd bloink)
bloink = A.run2 (A.new len0' >>= loop s (len0'-1) len0')
loop !s0 !i !len marr =
case next s0 of
Done -> return (marr, (j, len-j))
where j = i + 1
Skip s1 -> loop s1 i len marr
Yield x s1 | i < least -> {-# SCC "reverse/resize" #-} do
let newLen = len * 2 --LIQUID `shiftL` 1
marr' <- A.new newLen
A.copyM marr' (newLen-len) marr 0 len
write s1 (len+i) newLen marr'
| otherwise -> write s1 i len marr
where n = ord x
least | n < 0x10000 = 0
| otherwise = 1
m = n - 0x10000
lo = fromIntegral $ (m `shiftR` 10) + 0xD800
hi = fromIntegral $ (m .&. 0x3FF) + 0xDC00
-- TODO: figure out why this is deemed unsafe on ghc-7.10
write _ _ _ _ = undefined
write t j l mar
| n < 0x10000 = do
A.unsafeWrite mar j (fromIntegral n)
loop t (j-1) l mar
| otherwise = do
A.unsafeWrite mar (j-1) lo
A.unsafeWrite mar j hi
loop t (j-2) l mar
{-# INLINE [0] reverse #-}
-- | /O(n)/ Perform the equivalent of 'scanr' over a list, only with
-- the input and result reversed.
reverseScanr :: (Char -> Char -> Char) -> Char -> Stream Char -> Stream Char
reverseScanr f z0 (Stream next0 s0 len) = Stream next (S1 :*: z0 :*: s0) (len+1) -- HINT maybe too low
where
{-# INLINE next #-}
next (S1 :*: z :*: s) = Yield z (S2 :*: z :*: s)
next (S2 :*: z :*: s) = case next0 s of
Yield x s' -> let !x' = f x z
in Yield x' (S2 :*: x' :*: s')
Skip s' -> Skip (S2 :*: z :*: s')
Done -> Done
{-# INLINE reverseScanr #-}
-- | /O(n)/ Like 'unfoldr', 'unfoldrN' builds a stream from a seed
-- value. However, the length of the result is limited by the
-- first argument to 'unfoldrN'. This function is more efficient than
-- 'unfoldr' when the length of the result is known.
unfoldrN :: Int -> (a -> Maybe (Char,a)) -> a -> Stream Char
unfoldrN n = S.unfoldrNI n
{-# INLINE [0] unfoldrN #-}
-------------------------------------------------------------------------------
-- ** Indexing streams
-- | /O(n)/ stream index (subscript) operator, starting from 0.
index :: Stream Char -> Int -> Char
index = S.indexI
{-# INLINE [0] index #-}
-- | The 'findIndex' function takes a predicate and a stream and
-- returns the index of the first element in the stream
-- satisfying the predicate.
{-@ assume findIndex :: (GHC.Types.Char -> GHC.Types.Bool)
-> s:Data.Text.Fusion.Internal.Stream Char
-> Maybe {v:Nat | v < slen s}
@-}
findIndex :: (Char -> Bool) -> Stream Char -> Maybe Int
findIndex = S.findIndexI
{-# INLINE [0] findIndex #-}
-- | /O(n)/ The 'count' function returns the number of times the query
-- element appears in the given stream.
countChar :: Char -> Stream Char -> Int
countChar = S.countCharI
{-# INLINE [0] countChar #-}
-- | /O(n)/ Like a combination of 'map' and 'foldl''. Applies a
-- function to each element of a 'Text', passing an accumulating
-- parameter from left to right, and returns a final 'Text'.
{- fst :: (a, b) -> a @-}
-- fst :: (a, b) -> a
-- fst = undefined
{- snd :: (a, b) -> b @-}
-- snd :: (a, b) -> b
-- snd = undefined
{-@ assume mapAccumL
:: (a -> GHC.Types.Char -> (a,GHC.Types.Char))
-> a
-> s:Data.Text.Fusion.Internal.Stream Char
-> (a, {v:Data.Text.Internal.Text | (tlength v) = (slen s)})
@-}
{-@ lazy mapAccumL @-}
mapAccumL :: (a -> Char -> (a,Char)) -> a -> Stream Char -> (a, Text)
mapAccumL f z0 (Stream next0 s0 len) = (nz, I.textP na 0 nl)
where
mlen = upperBound 4 len
--LIQUID INLINE (na,(nz,nl)) = A.run2 (A.new mlen >>= \arr -> outer arr mlen z0 s0 0)
(na, (nz, nl))
= runST $ do arr0 <- A.new mlen
(marr,x) <- outer arr0 mlen z0 s0 0
arr <- A.unsafeFreeze marr
return (arr,x)
-- where mlen = upperBound 4 len
outer arr top = loop
where
loop !z !s !i =
case next0 s of
Done -> return (arr, (z,i))
Skip s' -> loop z s' i
Yield x s'
| j >= top -> {-# SCC "mapAccumL/resize" #-} do
let top' = (top + 1) * 2 --LIQUID `shiftL` 1
arr' <- A.new top'
A.copyM arr' 0 arr 0 top
outer arr' top' z s i
--LIQUID BUG | otherwise -> do let (z',c) = f z x
--LIQUID BUG d <- unsafeWrite arr i c
--LIQUID BUG loop z' s' (i+d)
--LIQUID BUG where j | ord x < 0x10000 = i
--LIQUID BUG | otherwise = i + 1
--LIQUID this needs to be `ord c` because `f` may return a Char
--LIQUID that takes 2 slots in the array. see LIQUID.txt for details
| otherwise -> do d <- unsafeWrite arr i c
loop z' s' (i+d)
where z' = fst blob1
c = snd blob1
blob1 = f z x
j | ord c < 0x10000 = i
| otherwise = i + 1
{-# INLINE [0] mapAccumL #-}