
  0 | module System.UV.Util
  1 | 
  2 | import Data.ByteString
  3 | import Data.ByteVect
  4 | import Data.IORef
  5 | 
  6 | %default total
  7 | 
  8 | public export
  9 | idris_uv : String -> String
 10 | idris_uv fn = "C:" ++ fn ++ ",libuv-idris"
 11 | 
 12 | export %inline
 13 | boolToInt32 : Bool -> Int32
 14 | boolToInt32 False = 0
 15 | boolToInt32 True  = 1
 16 | 
 17 | export %inline
 18 | int32ToBool : Int32 -> Bool
 19 | int32ToBool 0 = False
 20 | int32ToBool _ = True
 21 | 
 22 | --------------------------------------------------------------------------------
 23 | -- Accumulating Lines: TODO: This should probably go to idris2-bytestring
 24 | --------------------------------------------------------------------------------
 25 | 
 26 | ls :  SnocList ByteString
 27 |    -> (n : Nat)
 28 |    -> ByteVect n
 29 |    -> (SnocList ByteString, ByteString)
 30 | ls sb n bs =
 31 |   case breakNL bs of
 32 |     MkBreakRes l1 0      b1 _  prf => (sb, BS l1 b1)
 33 |     MkBreakRes l1 (S l2) b1 b2 prf =>
 34 |       ls (sb :< BS l1 b1) (assert_smaller n l2) (tail b2)
 35 | 
 36 | lss :  SnocList ByteString
 37 |     -> ByteString
 38 |     -> List ByteString
 39 |     -> (List ByteString, ByteString)
 40 | lss sx x []          = (sx <>> [], x)
 41 | lss sx x (BS n bs :: bss) =
 42 |   case breakNL bs of
 43 |     MkBreakRes l1 0      b1 _  prf => lss sx (x <+> BS l1 b1) bss
 44 |     MkBreakRes l1 (S l2) b1 b2 prf =>
 45 |       let (sx2,x2) := ls (sx :< (x <+> BS l1 b1)) l2 (tail b2)
 46 |        in lss sx2 x2 bss
 47 | 
 48 | export %inline
 49 | accumLines : (rem, next : ByteString) -> (List ByteString, ByteString)
 50 | accumLines rem bs = lss [<] rem [bs]
 51 | 
 52 | export %inline
 53 | accumLinesN :
 54 |      (rem : ByteString)
 55 |   -> List ByteString
 56 |   -> (List ByteString, ByteString)
 57 | accumLinesN = lss [<]
 58 |