liquidhaskell-0.8.10.1: tests/errors/AmbiguousInline.hs
{-@ LIQUID "--scrape-used-imports" @-}
{-@ LIQUID "--short-names" @-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module MatchIdxs where
import qualified Data.ByteString as BS
-- RJ import qualified Data.ByteString.Search as BS
import Data.Char
-- RJ import Data.List.Split(chunksOf)
import Data.Monoid
import Data.Proxy
import Debug.Trace
import GHC.TypeLits
import Language.Haskell.Liquid.Prelude (liquidAssert)
-- FIX import Prelude hiding (min, max)
import Prelude hiding (max)
junk = BS.head
traceMsg msg x = trace (msg ++ show x) x
{-@ chunksBS :: Int -> b:BS.ByteString -> [BS.ByteString] / [(bLength b)] @-}
chunksBS n' xs | BS.null xs = []
| otherwise = x : chunksBS n xs'
where (x,xs') = BS.splitAt (liquidAssert (n > 0) n) xs
n = max 1 n'
bsToString :: BS.ByteString -> String
bsToString = map (chr . fromIntegral) . BS.unpack
stringToBS :: String -> BS.ByteString
stringToBS = BS.pack . map (fromIntegral . ord)
-- | get the (proxied and existentially boxed) type level Symbol for a bytestring
someSymbolValBS :: BS.ByteString -> SomeSymbol
someSymbolValBS = someSymbolVal . bsToString
-- | get the bytestring corresponding to a type level Symbol
mkTarg :: forall t . KnownSymbol t => Proxy t -> BS.ByteString
mkTarg = stringToBS . symbolVal
-- | Naive specification of string matching (from Bird)
{-@ indicesSpec :: t:ByteStringNE -> s:BS.ByteString -> [OkPos t s] @-}
-- indicesSpec targ = map ((BS.length targ -) . BS.length) . filter (targ `BS.isSuffixOf`) . BS.inits
indicesSpec targ s = [ BS.length s' - BS.length targ | s' <- BS.inits s
, targ `BS.isSuffixOf` s' ]
indicesSpec :: BS.ByteString -> BS.ByteString -> [Int]
-- | Datatype to name string matching algorithms; will use it's lifted
-- version put choice in type.
data Alg = BM -- ^ Boyer-Moore from stringsearch package
| Spec -- ^ Naive spec
{-@ indices :: Alg -> t:ByteStringNE -> s:BS.ByteString -> [OkPos t s] @-}
indices BM = assumeIndices -- RJ BS.indices
indices Spec = indicesSpec
-- | Monoid
--
-- 'MatchIdxs alg targ' denotes the result of running string matching
-- algorithm 'alg' search for target 'targ' in some input. In addition
-- to the match indices, information needed to combine this result
-- with similar results on input to the left and right are also
-- included.
--
-- We'd like to prove that the invariants in the comments hold (|x|
-- denotes the length of x).
data MatchIdxs
= Small { targ :: BS.ByteString
, bs :: BS.ByteString
}
| MatchIdxs { targ :: BS.ByteString
, input :: Int
, left :: BS.ByteString
, matches :: [Int]
, right :: BS.ByteString
}
deriving (Eq, Show)
{-@ data MatchIdxs
= Small { targ :: ByteStringNE
, bs :: {v:BS.ByteString | bLength v < bLength targ}
}
| MatchIdxs
{ targ :: ByteStringNE
, input :: {v : Int | v >= bLength targ}
, left :: {v : BS.ByteString | bLength v == bLength targ - 1}
, matches :: [{v:Int | v <= input - bLength targ}]
, right :: {v : BS.ByteString | bLength v == bLength targ - 1}
}
@-}
matchIdxsIs :: MatchIdxs -> [Int]
matchIdxsIs (Small _ _) = []
matchIdxsIs (MatchIdxs _ _ _ is _) = is
-- | create a 'MatchIdxs'
{-@ myIndices :: Alg -> t:ByteStringNE -> BS.ByteString -> MatchIdxsT t @-}
myIndices alg t bs
| BS.length bs > fringeLen = let right1 = BS.drop (BS.length bs - fringeLen) bs in
MatchIdxs t (BS.length bs) left is right1
| otherwise = Small t bs
where
is = indices alg t bs
fringeLen = BS.length t - 1
left = BS.take fringeLen bs
-- right1 = BS.drop (BS.length bs - fringeLen) bs
-- ISSUE: get contextual output with --diff
-- ISSUE: why does lazyvar right1 not work? it drops the output type on right1!
{- lazyvar right1 -}
{-@ type OkPos Targ Str = {v:Nat | v <= bLength Str - bLength Targ} @-}
{-@ type ByteStringNE = {v:BS.ByteString | bLength v > 0 } @-}
{-@ type ByteStringN N = {v:BS.ByteString | bLength v == N} @-}
{-@ type MatchIdxsT T = {v:MatchIdxs | targ v == T} @-}
{-@ assume BS.isSuffixOf :: targ:_ -> s:_ -> {v:_ | v => (bLength targ <= bLength s) } @-}
{-@ assume BS.length :: b:BS.ByteString -> {v:Nat | v == bLength b} @-}
{-@ assume BS.empty :: {v:BS.ByteString | bLength v == 0} @-}
{-@ assume BS.take :: n:Nat -> b:BS.ByteString -> ByteStringN {min n (bLength b)} @-}
{-@ assume BS.drop :: n:Nat -> b:{BS.ByteString | n <= bLength b} -> ByteStringN {bLength b - n} @-}
{-@ assume BS.inits :: b:BS.ByteString -> [{v:BS.ByteString | bLength v <= bLength b}] @-}
{-@ assume BS.append :: b1:BS.ByteString -> b2:BS.ByteString -> ByteStringN {bLength b1 + bLength b2} @-}
{-@ assume BS.null :: b:BS.ByteString -> {v:Bool | v <=> (bLength b == 0)} @-}
{-@ assume BS.splitAt :: n:Nat -> b:BS.ByteString -> (ByteStringN {min n (bLength b)}, ByteStringN {max 0 (bLength b - n)}) @-}
{-@ assume BS.head :: BS.ByteString -> _ @-}
{-@ measure target @-}
target :: MatchIdxs -> BS.ByteString
target (Small t _) = t
target (MatchIdxs t _ _ _ _) = t
{-@ inline min @-}
min :: Int -> Int -> Int
min x y = if x <= y then x else y
{-@ inline max @-}
max :: Int -> Int -> Int
max x y = if x <= y then y else x
-- RJ instance (KnownSymbol t, StringMatch alg) => Monoid (MatchIdxs alg t) where
{-@ mmempty :: t:ByteStringNE -> MatchIdxsT t @-}
mmempty t = Small t BS.empty
{-@ mmconcat :: (Foldable t) => Alg -> tg:ByteStringNE -> t (MatchIdxsT tg) -> (MatchIdxsT tg) @-}
mmconcat alg t = foldr (mmappend alg t) (mmempty t)
{-@ qualif BB(v:Int, n:Int, d:Int, b:BS.ByteString): v <= (n + d) - bLength b @-}
{-@ mmappend :: Alg -> t:ByteStringNE -> MatchIdxsT t -> MatchIdxsT t -> MatchIdxsT t @-}
mmappend alg t mx my =
let fringeLen = BS.length t - 1
idxFun = indices alg t
in
case (mx, my) of
(Small tx x, Small _ y) -> myIndices alg tx (x <> y)
(Small tx x, MatchIdxs _ yLen ly iy rt) -> MatchIdxs tx xyLen lt is rt
where
xyLen = xLen + yLen
xLen = BS.length x
xly = BS.append x ly
lt = BS.take fringeLen xly
is = idxFun xly ++ map (+ xLen) iy
(MatchIdxs tx xLen lt ix rx, Small ty y) -> MatchIdxs tx xyLen lt (ix ++ is) rt
where
xyLen = xLen + yLen
yLen = BS.length y
is = map (+ (xLen - fringeLen)) (idxFun rxy)
rt = BS.drop (BS.length rxy - fringeLen) rxy
rxy = BS.append rx y
(MatchIdxs tx xLen lt ix rx, MatchIdxs ty yLen ly iy rt) -> MatchIdxs tx xyLen lt (ix ++ is) rt
where
xyLen = xLen + yLen
is = ixy ++ map (+ xLen) iy
ixy = map (+ (xLen - fringeLen)) $ idxFun (BS.append rx ly)
-- | Example applications
--
-- The bufLen and chunkSz arguments are there to exercise the monoid,
-- though they also foreshadow a parallel implementation.
{-@ indicesBS' :: Alg -> Int -> Int -> ByteStringNE -> BS.ByteString -> [Int] @-}
indicesBS' alg bufLen chunkSz t bs =
let si = mmconcat alg t . map (mmconcat alg t) . chunksOf bufLen . map (myIndices alg t) $ chunksBS chunkSz bs in
matchIdxsIs si
{-@ indicesBS, indicesNaive :: Int -> Int -> ByteStringNE -> BS.ByteString -> [Int] @-}
indicesBS = indicesBS' BM -- RJ (Proxy :: Proxy BM)
indicesNaive = indicesBS' Spec -- RJ (Proxy :: Proxy Spec)
{-@ isInfixOfBS :: Int -> Int -> ByteStringNE -> BS.ByteString -> Bool @-}
isInfixOfBS bufLen chunkSz t = not . null . indicesBS bufLen chunkSz t
------------------------------------------------------------------------------------------
{-@ invariant {v:BS.ByteString | 0 <= bLength v } @-}
{-@ measure bLength :: BS.ByteString -> Int @-}
{-@ type LNat N = {v:Nat | v < N} @-}
chunksOf :: Int -> [a] -> [[a]]
chunksOf = undefined
{-@ assumeIndices :: t:ByteStringNE -> s:BS.ByteString -> [OkPos t s] @-}
assumeIndices :: BS.ByteString -> BS.ByteString -> [Int]
assumeIndices = undefined