content: {-@ LIQUID "--short-names" @-}
  
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  module AmbiguousInline 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)
  import Prelude hiding (min, 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
  