
  0 | module Data.String.Search
  1 | 
  2 | import Data.Buffer
  3 | import Data.List as List
  4 | import System.FFI
  5 | 
  6 | export
  7 | setBytes : Buffer -> Int -> List Bits8 -> IO Unit
  8 | setBytes buf offset [] = pure ()
  9 | setBytes buf offset (x :: xs) = do
 10 |   setBits8 buf offset x
 11 |   setBytes buf (offset + 1) xs
 12 | 
 13 | %foreign "C:string_search_search,libstringsearch-idris"
 14 | prim__search: Buffer -> Int -> Buffer -> Int -> Ptr Int -> PrimIO Int
 15 | 
 16 | search: Buffer -> Int -> Buffer -> Int -> Ptr Int -> IO Int
 17 | search a b c d e = primIO (prim__search a b c d e)
 18 | 
 19 | %foreign "C:string_search_deref_int,libstringsearch-idris"
 20 | prim__derefInt: Ptr Int -> PrimIO Int
 21 | 
 22 | export
 23 | searchBuffer: Buffer -> Buffer -> IO (Maybe Int)
 24 | searchBuffer needle haystack = do
 25 |   needleLen <- rawSize needle
 26 |   haystackLen <- rawSize haystack
 27 |   codePtr <- malloc 4
 28 |   index <- search needle needleLen haystack haystackLen (prim__castPtr codePtr)
 29 |   code <- primIO (prim__derefInt $ prim__castPtr codePtr)
 30 |   free codePtr
 31 |   pure $
 32 |     if code == 1
 33 |        then Just index
 34 |        else Nothing
 35 | 
 36 | export
 37 | splitBits8: List Bits8 -> List Bits8 -> Maybe (List Bits8, List Bits8)
 38 | splitBits8 needle haystack = unsafePerformIO $ do
 39 |   let needleLen  = cast $ List.length needle
 40 |   Just needleBuf <- newBuffer needleLen
 41 |   | Nothing => pure Nothing
 42 |   Just haystackBuf <- newBuffer (cast $ List.length haystack)
 43 |   | Nothing => pure Nothing
 44 |   setBytes needleBuf 0 needle
 45 |   setBytes haystackBuf 0 haystack
 46 |   Just index1 <- searchBuffer needleBuf haystackBuf
 47 |   | Nothing => pure Nothing
 48 |   if index1 == 0
 49 |     -- splitBuffer will return Nothing when it gets a 0,
 50 |     -- so we branch here to avoid this.
 51 |     then do
 52 |       Just (_, after) <- splitBuffer haystackBuf needleLen
 53 |       | Nothing => pure Nothing
 54 |       bits <- bufferData' after
 55 |       pure $ Just ([], bits)
 56 |     else do
 57 |       Just (before, firstBoundaryAndAfter) <- splitBuffer haystackBuf index1
 58 |       | Nothing => pure Nothing
 59 |       Just (_, after) <- splitBuffer firstBoundaryAndAfter needleLen
 60 |       | Nothing => pure Nothing
 61 |       ints <- bufferData' before
 62 |       remainingInts <- bufferData' after
 63 |       pure $ Just ( ints
 64 |                   , remainingInts
 65 |                   )
 66 |