1 | module Text.ILex.Internal.Runner

 3 | import Data.Array.Index

 4 | import Data.Buffer

 5 | import Data.Buffer.Core

 6 | import Data.Buffer.Indexed

 7 | import Data.ByteString

 8 | import Data.Linear.Ref1

 9 | import Data.Maybe0

10 | import Data.Nat.BSExtra

12 | import Text.Bounds

13 | import Text.ParseError

14 | import Text.FC

15 | import Text.ILex.Lexer

16 | import Text.ILex.RExp

18 | %default total

21 | offsetToIx : (o : Nat) -> Ix s (o+s)

22 | offsetToIx 0     = IZ

23 | offsetToIx (S k) = rewrite plusSuccRightSucc k s in IS (offsetToIx k)

25 | export %inline

26 | toBS :

27 |      IBuffer n

28 |   -> (from        : Ix m n)

29 |   -> (0    till   : Nat)

30 |   -> {auto ix     : Ix till n}

31 |   -> {auto 0  lte : LTE (ixToNat from) (ixToNat ix)}

32 |   -> ByteString

33 | toBS buf from till =

34 |  let bv := fromIBuffer buf

35 |   in BS _ $ substringFromTill (ixToNat from) (ixToNat ix) {lt2 = ixLTE ix} bv

38 | toBSP :

39 |      ByteString

40 |   -> IBuffer n

41 |   -> (from        : Ix m n)

42 |   -> (0    till   : Nat)

43 |   -> {auto ix     : Ix till n}

44 |   -> {auto 0  lte : LTE (ixToNat from) (ixToNat ix)}

45 |   -> ByteString

46 | toBSP (BS 0 _) buf from till = toBS buf from till

47 | toBSP prev     buf from till =

48 |  let bv := fromIBuffer buf

49 |      bs := BS _ $ substringFromTill (ixToNat from) (ixToNat ix) {lt2 = ixLTE ix} bv

50 |   in prev <+> bs