
  0 | ||| Some utilities mainly for internal use
  1 | module Text.ILex.Internal.Runner
  2 | 
  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
 11 | 
 12 | import Text.Bounds
 13 | import Text.ParseError
 14 | import Text.FC
 15 | import Text.ILex.Lexer
 16 | import Text.ILex.RExp
 17 | 
 18 | %default total
 19 | 
 20 | export
 21 | offsetToIx : (o : Nat) -> Ix s (o+s)
 22 | offsetToIx 0     = IZ
 23 | offsetToIx (S k) = rewrite plusSuccRightSucc k s in IS (offsetToIx k)
 24 | 
 25 | export %inline
 26 | writeBS :
 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 |   -> Ref q ByteString
 33 |   -> F1' q
 34 | writeBS buf from till ref t =
 35 |  let bv := fromIBuffer buf
 36 |      bs := BS _ $ substringFromTill (ixToNat from) (ixToNat ix) {lt2 = ixLTE ix} bv
 37 |   in write1 ref bs t
 38 | 
 39 | export
 40 | writeBSP :
 41 |      ByteString
 42 |   -> IBuffer n
 43 |   -> (from        : Ix m n)
 44 |   -> (0    till   : Nat)
 45 |   -> {auto ix     : Ix till n}
 46 |   -> {auto 0  lte : LTE (ixToNat from) (ixToNat ix)}
 47 |   -> Ref q ByteString
 48 |   -> F1' q
 49 | writeBSP (BS 0 _) buf from till ref t = writeBS buf from till ref t
 50 | writeBSP prev     buf from till ref t =
 51 |  let bv := fromIBuffer buf
 52 |      bs := BS _ $ substringFromTill (ixToNat from) (ixToNat ix) {lt2 = ixLTE ix} bv
 53 |   in write1 ref (prev <+> bs) t
 54 |