0 | module Text.FC
  1 |
  2 | import Data.ByteString
  3 | import Data.String
  4 | import Derive.Prelude
  5 | import Text.Bounds
  6 |
  7 | %default total
  8 | %language ElabReflection
  9 |
 10 | public export
 11 | data Origin : Type where
 12 |   FileSrc : (path : String) -> Origin
 13 |   Virtual : Origin
 14 |
 15 | %runElab derive "Origin" [Show,Eq]
 16 |
 17 | public export
 18 | Interpolation Origin where
 19 |   interpolate (FileSrc p) = p
 20 |   interpolate Virtual     = "virtual"
 21 |
 22 | public export
 23 | record FileContext where
 24 |   constructor FC
 25 |   origin : Origin
 26 |   bounds : Bounds
 27 |
 28 | public export %inline
 29 | fromBounded : Origin -> Bounded a -> (FileContext, a)
 30 | fromBounded o (B val bounds) = (FC o bounds, val)
 31 |
 32 | public export %inline
 33 | virtualFromBounded : Bounded a -> (FileContext, a)
 34 | virtualFromBounded = fromBounded Virtual
 35 |
 36 | %runElab derive "FileContext" [Show,Eq]
 37 |
 38 | export
 39 | Interpolation FileContext where
 40 |   interpolate (FC o NoBounds) = interpolate o
 41 |   interpolate (FC o b)        = "\{o}: \{b}"
 42 |
 43 | nextRem : Fin 4 -> Bits8 -> Fin 4
 44 | nextRem FZ     m =
 45 |   if      m < 0b1000_0000  then 0
 46 |   else if m < 0b1110_0000  then 1
 47 |   else if m < 0b1111_0000  then 2
 48 |   else                          3
 49 | nextRem (FS x) m = weaken x
 50 |
 51 | ||| Converts an index into a bytestring to a position
 52 | ||| (line and column) in the corresponding UTF-8 string.
 53 | export
 54 | toPosition : Nat -> ByteString -> Position
 55 | toPosition n (BS x bv) = go 0 0 x 0
 56 |   where
 57 |     -- we iterate over a bytestring of UTF-8 encoded characters
 58 |     -- if we are in the middle of a character, we continue until
 59 |     -- the end of character is encountered.
 60 |     go : (l,c : Nat) -> (n : Nat) -> Fin 4 -> (y : Ix n x) => Position
 61 |     go l c 0     _   = P l c
 62 |     go l c (S k) rem =
 63 |       let byte := bv `ix` k
 64 |           nxt  := nextRem rem byte
 65 |        in case nxt of
 66 |             0 => case ixToNat y >= n of
 67 |               True  => P l c
 68 |               False => case byte of
 69 |                 0x0a => go (l+1) 0     k nxt
 70 |                 _    => go l     (c+1) k nxt
 71 |             _ => go l c k nxt
 72 |
 73 | range : Nat -> Nat -> List a -> List a
 74 | range s e = take ((e `minus` s) + 1) . drop s
 75 |
 76 | lineNumbers : SnocList String -> Nat -> Nat -> List String -> SnocList String
 77 | lineNumbers sl _ _    []     = sl
 78 | lineNumbers sl size n (h::t) =
 79 |   let k   := S n
 80 |       pre := padLeft size '0' $ show k
 81 |    in lineNumbers (sl :< " \{pre} | \{h}") size k t
 82 |
 83 | ||| Pretty prints a file context, highlighting the section in the given
 84 | ||| list of source lines.
 85 | |||
 86 | ||| The `FileContext` describes the absolute context (file source and
 87 | ||| bounds) where an error occurred, while `relBounds` is the error's
 88 | ||| position relative to the given list of lines.
 89 | |||
 90 | ||| The above distinction is necessary when streaming large amounts of
 91 | ||| data, where it is not feasible to keep the whole data in memory but
 92 | ||| only the most recent chunk.
 93 | export
 94 | printFC :
 95 |      FileContext
 96 |   -> (relBounds   : Bounds)
 97 |   -> (sourceLines : List String)
 98 |   -> List String
 99 | printFC fc@(FC _ $ BS (P so _) (P eo _)) (BS (P sr sc) (P er ec)) ls =
100 |   let  nsize  := length $ show (eo + 1)
101 |        head   := "\{fc}"
102 |    in case sr == er of
103 |      False =>
104 |        lineNumbers [<"",head] nsize so (range sr (min er $ sr+5) ls) <>> []
105 |      True  =>
106 |        let -- In case of end-of-input errors, we sometimes get `ec == sc`.
107 |            -- We want to make sure we still print at least one emphasis character
108 |            -- in those cases.
109 |            cemph := max 1 $ ec `minus` sc
110 |            emph  := indent (nsize + sc + 4) (replicate cemph '^')
111 |            fr    := er `minus` 4 -- first row
112 |            begin := so `minus` (er `minus` fr)
113 |         in lineNumbers [<"",head] nsize begin (range fr er ls) <>> [emph]
114 | printFC fc _ _  = [interpolate fc]
115 |