
   0 | ||| Conversion of the bounds of a byte sequence to an text
   1 | ||| sequence plus absolute and relative bounds for pretty printing
   2 | ||| errors when streaming large files.
   3 | module Text.ByteRange
   4 | 
   5 | import Debug.Trace
   6 | import Derive.Prelude
   7 | import public Data.ByteString
   8 | import public Text.ByteBounds
   9 | 
  10 | %default total
  11 | %language ElabReflection
  12 | 
  13 | MIN_LINES : Nat
  14 | MIN_LINES = 5
  15 | 
  16 | ||| A non-empty chunk of bytes in a sequence or stream of bytes
  17 | ||| wrapped up with some counters.
  18 | public export
  19 | record Chunk where
  20 |   constructor CH
  21 |   ||| The current chunk of bytes
  22 |   bytes       : ByteString
  23 | 
  24 |   ||| Absolute byte position of the first byte in `bytes`
  25 |   first       : BytePos
  26 | 
  27 |   ||| Number of line breaks encountered before this chunk
  28 |   linesBefore : Nat
  29 | 
  30 |   ||| Number of line breaks in this chunk
  31 |   lines       : Nat
  32 | 
  33 |   {auto 0 prf : IsSucc bytes.size}
  34 | 
  35 | %runElab derive "Chunk" [Show]
  36 | 
  37 | %inline
  38 | lineCount : ByteString -> Nat
  39 | lineCount = flip foldr Z $ \b,n => case b of {0xa => S n; _   => n}
  40 | 
  41 | ||| Absolute position of the last byte in the given `Chunk`.
  42 | export
  43 | (.last) : Chunk -> BytePos
  44 | b.last = incLen b.bytes.size b.first
  45 | 
  46 | ||| Absolute position of the first byte of the next chunk after this one.
  47 | export
  48 | (.next) : Chunk -> BytePos
  49 | b.next = BP (b.first.pos + b.bytes.size)
  50 | 
  51 | ||| Number of linebreaks up to and including the given chunk.
  52 | export
  53 | (.linesIncluding) : Chunk -> Nat
  54 | b.linesIncluding = b.linesBefore + b.lines
  55 | 
  56 | ||| Given an optional previous chunk plus a non-empty byte vector,
  57 | ||| computes the stats of the current chunk.
  58 | export
  59 | nextChunk : Maybe Chunk -> (bs : ByteString) -> (0 p : IsSucc bs.size) => Chunk
  60 | nextChunk Nothing  bs = CH bs 0 0 (lineCount bs)
  61 | nextChunk (Just c) bs = CH bs c.next c.linesIncluding (lineCount bs)
  62 | 
  63 | dropPartialLine : Chunk -> SnocList Chunk
  64 | dropPartialLine c =
  65 |  let (pre, BS (S $ S k) pst) := break (0xa ==) c.bytes | _ => [<]
  66 |      p         := BP $ c.first.pos + pre.size + 1
  67 |   in [<CH (BS (S k) $ tail pst) p (S c.linesBefore) (pred c.lines)]
  68 | 
  69 | ||| A sequence of chunks, describing if it holds some start
  70 | ||| and end position.
  71 | public export
  72 | data ByteRange : Type where
  73 |   Prefix : SnocList Chunk -> ByteRange
  74 |   Start  : SnocList Chunk -> ByteRange
  75 |   End    : SnocList Chunk -> ByteRange
  76 |   Done   : SnocList Chunk -> ByteRange
  77 |   None   : ByteRange
  78 | 
  79 | %runElab derive "ByteRange" [Show]
  80 | 
  81 | export %inline
  82 | isDone : ByteRange -> Bool
  83 | isDone (Done _) = True
  84 | isDone _        = False
  85 | 
  86 | containsEnd : ByteRange -> Bool
  87 | containsEnd (End _) = True
  88 | containsEnd r       = isDone r
  89 | 
  90 | export
  91 | chunks : ByteRange -> SnocList Chunk
  92 | chunks (Prefix sx) = sx
  93 | chunks (Start sx)  = sx
  94 | chunks (End sx)    = sx
  95 | chunks (Done sx)   = sx
  96 | chunks None        = [<]
  97 | 
  98 | lastChunk : SnocList Chunk -> Maybe Chunk
  99 | lastChunk [<]    = Nothing
 100 | lastChunk (_:<c) = Just c
 101 | 
 102 | pre : List Chunk -> SnocList Chunk -> Nat -> ByteRange
 103 | pre cs [<] _     = Prefix ([<] <>< cs)
 104 | pre cs (sc:<c) n =
 105 |   case n `minus` c.lines of
 106 |     0 => Start (dropPartialLine c <>< cs)
 107 |     n => pre (c::cs) sc n
 108 | 
 109 | ||| Given a start and end position, appends a chunk of bytes to
 110 | ||| range of bytes, making sure that the range will contain
 111 | ||| enough lines before the start byte and enough lines after the
 112 | ||| end byte.
 113 | export
 114 | appendChunk : (s,e : BytePos) -> ByteRange -> ByteString -> ByteRange
 115 | appendChunk _ _ r@(Done _) _               = r
 116 | appendChunk _ _ r          (BS 0 _)        = r
 117 | appendChunk s e r          bs@(BS (S _) _) =
 118 |  let cs  := chunks r
 119 |      c   := nextChunk (lastChunk cs) bs
 120 |      cs2 := cs:< c
 121 |      -- cs2 := cs:< trace "Current: \{show c}" c
 122 |   in case c.last >= e of
 123 |        True  => if containsEnd r && c.lines > 0 then Done cs2 else End cs2
 124 |        False => case c.last >= s of
 125 |          True  => Start cs2
 126 |          False => pre [] cs2 MIN_LINES
 127 | 
 128 | ||| Given a sequence (or stream) of byte vectors, we want to find
 129 | ||| a minimal chunk fully enclosing a given byte range, so that we
 130 | ||| can pretty print that byte range.
 131 | |||
 132 | ||| The chunk should fulfill the following prerequisites:
 133 | |||  * fully contain all bytes given in the byte range
 134 | |||  * contain the last five line breaks before the first
 135 | |||    byte in the byte range, or - if there are not as many line breaks before
 136 | |||    the first byte - contain the first byte of the whole byte stream
 137 | |||    so that we can print the whole line where - for instance -
 138 | |||    an error occurred
 139 | |||  * contain at least the next line-break *after* the last position (if any)
 140 | export %inline
 141 | enclosingBytes : Foldable f => (s,e : BytePos) -> f ByteString -> ByteRange
 142 | enclosingBytes s e = foldl (appendChunk s e) None
 143 | 
 144 | ||| Absolute and relative text bounds in a stream of byte vectors
 145 | public export
 146 | record TextBounds where
 147 |   constructor TB
 148 |   ||| An excerpt of the byte stream large enough to fully contain
 149 |   ||| a given byte sequence
 150 |   content  : String
 151 | 
 152 |   ||| Absolute bounds of the start and end position of the given
 153 |   ||| byte sequence.
 154 |   absolute : Bounds
 155 | 
 156 |   ||| Relative bounds of the start and end position of the given
 157 |   ||| byte sequence.
 158 |   relative : Bounds
 159 | 
 160 | %runElab derive "TextBounds" [Show,Eq]
 161 | 
 162 | bounds : (line : Nat) -> ByteBounds -> ByteString -> TextBounds
 163 | bounds line bb bs =
 164 |  let ini := P line 0
 165 |      m   := bytePositionMapFrom ini bs
 166 |      abs := toBounds bb
 167 |   in TB (toString bs) abs (relativeTo abs ini)
 168 | 
 169 | ||| Given a byte range that is supposed to contain the
 170 | ||| byte sequence corresponding to the given byte bounds,
 171 | ||| returns the proper text bounds - or `Nothing` if
 172 | ||| something went wrong.
 173 | export
 174 | textBounds : (start, end : BytePos) -> ByteRange -> Maybe TextBounds
 175 | textBounds s e r =
 176 |   case containsEnd r of
 177 |     False => Nothing
 178 |     True  =>
 179 |      let c::cs := chunks r <>> [] | _ => Nothing
 180 |          bs    := fastConcat (map bytes $ c::cs)
 181 |          o     := c.first
 182 |       in Just $ bounds c.linesBefore (BB (offsetTo o s) (offsetTo o e)) bs
 183 | 
 184 | export %inline
 185 | toFCErr : ByteError e -> TextBounds -> FCErr e
 186 | toFCErr (BE o _ _ x) (TB c a r) = PE o a r (Just c) x
 187 |