
   0 | module Idrall.FC
   1 | 
   2 | import public Text.PrettyPrint.Prettyprinter
   3 | 
   4 | import Idrall.Path
   5 | 
   6 | import Data.String
   7 | import Data.List
   8 | import System.File
   9 | 
  10 | public export
  11 | FilePos : Type
  12 | FilePos = (Nat, Nat)
  13 | 
  14 | -- does fancy stuff for idris, for now it can just be a Maybe filename
  15 | public export
  16 | OriginDesc : Type
  17 | OriginDesc = Maybe String
  18 | 
  19 | -- TODO use this as a Maybe for MkVirtualFC
  20 | data FCDetails = MkFCDetails OriginDesc FilePos FilePos
  21 | 
  22 | public export
  23 | data FC = MkFC        OriginDesc FilePos FilePos
  24 |         | ||| Virtual FCs are FC attached to desugared/generated code.
  25 |           MkVirtualFC OriginDesc FilePos FilePos
  26 |         | EmptyFC
  27 | %name FC fc
  28 | 
  29 | public export
  30 | interface HasFC a where
  31 |   constructor MkHasFC
  32 |   getFC : a -> FC
  33 | 
  34 | public export
  35 | Show FC where
  36 |   show (MkFC Nothing x y) = "\{show x}-\{show y}"
  37 |   show (MkFC (Just s) x y) = "\{s}:\{show x}-\{show y}"
  38 |   show (MkVirtualFC x y z) = "MkVirtualFCTODO"
  39 |   show EmptyFC = ""
  40 | 
  41 | prettyPairs : (Nat, Nat) -> (Nat, Nat) -> Doc ann
  42 | prettyPairs x y = pretty (show x) <++> pretty "->" <++> pretty (show y)
  43 | 
  44 | public export
  45 | Pretty FC where
  46 |   pretty (MkFC Nothing y z) = prettyPairs y z
  47 |   pretty (MkFC (Just x) y z) = pretty x <++> softline <+> prettyPairs y z
  48 |   pretty (MkVirtualFC Nothing y z) = prettyPairs y z
  49 |   pretty (MkVirtualFC (Just x) y z) = pretty "Virtual File" <++> pretty x <++> softline <+> prettyPairs y z
  50 |   pretty EmptyFC = neutral
  51 | 
  52 | public export
  53 | initFC : FC
  54 | initFC = EmptyFC
  55 | 
  56 | public export
  57 | originFromFC : FC -> OriginDesc
  58 | originFromFC (MkFC x y z) = x
  59 | originFromFC (MkVirtualFC x y z) = x
  60 | originFromFC EmptyFC = Nothing
  61 | 
  62 | export
  63 | fcToVFC : FC -> FC
  64 | fcToVFC (MkFC x y z) = MkVirtualFC x y z
  65 | fcToVFC fc@(MkVirtualFC x y z) = fc
  66 | fcToVFC EmptyFC = EmptyFC
  67 | 
  68 | ex1 : String
  69 | ex1 = """
  70 | 1 some text
  71 | 2 another line that's a bit longer
  72 | 3 again stuff
  73 | """
  74 | 
  75 | printArrows : Nat -> (Nat, Nat) -> (Nat, Nat) -> String
  76 | printArrows max (ln, col) (ln', col') =
  77 |   case (ln <= ln', col <= col') of
  78 |        (True, True) =>
  79 |           let pad = replicate col ' '
  80 |               end = if col' > max then max else col'
  81 |               add1 = if (ln == ln' && col == col') then 1 else 0
  82 |               arrowCount = (minus end col) + add1
  83 |               -- the 1 is for if the span starts and ends on a single char
  84 |               arrows = replicate arrowCount '^'
  85 |           in pack $ pad ++ arrows
  86 |        _ => "^-^-^"
  87 | 
  88 | safePrint : List String -> (Nat, Nat) -> (Nat, Nat) -> Maybe String
  89 | safePrint xs s@(ln, col) e@(ln', col') =
  90 |   case Data.List.inBounds ln xs of
  91 |        (Yes prf) =>
  92 |           let str = index ln xs
  93 |               lineNoPrefix = show ln ++ "| "
  94 |               whitePrefix = pack $ List.replicate (length lineNoPrefix) ' '
  95 |               in
  96 |               Just $ unlines [lineNoPrefix ++ str, whitePrefix ++ printArrows (length str) s e]
  97 |        (No contra) => neutral -- TODO better failure case
  98 | 
  99 | formatSpanSnippet : FC -> String -> Maybe String
 100 | formatSpanSnippet fc str =
 101 |   let ls = lines str
 102 |       startpos' = startpos fc
 103 |       endpos' = endpos fc
 104 |       neutralpos = (0,0)
 105 |       in
 106 |   case (startpos', endpos') of
 107 |        ((Just s), (Just e)) => safePrint ls s e
 108 |        ((Just s), Nothing) => safePrint ls s neutralpos
 109 |        (Nothing, (Just e)) => safePrint ls neutralpos e
 110 |        (Nothing, Nothing) => neutral
 111 | where
 112 |   startpos : FC -> Maybe (Nat, Nat)
 113 |   startpos (MkFC x start _) = Just start
 114 |   startpos (MkVirtualFC x start _) = Just start
 115 |   startpos EmptyFC = Nothing
 116 |   endpos : FC -> Maybe (Nat, Nat)
 117 |   endpos (MkFC x _ end) = Just end
 118 |   endpos (MkVirtualFC x _ end) = Just end
 119 |   endpos EmptyFC = Nothing
 120 | 
 121 | export
 122 | getSpanSnippet : FC -> IO (Maybe String)
 123 | getSpanSnippet fc@(MkFC (Just x) start end) = do
 124 |   Right str <- readFile x | Left e => pure neutral
 125 |   pure $ formatSpanSnippet fc str
 126 | getSpanSnippet fc@(MkVirtualFC (Just x) start end) = do
 127 |   Right str <- readFile x | Left e => pure neutral
 128 |   pure $ formatSpanSnippet fc str
 129 | getSpanSnippet (MkFC Nothing y z) = pure neutral
 130 | getSpanSnippet (MkVirtualFC Nothing y z) = pure neutral
 131 | getSpanSnippet EmptyFC = pure neutral
 132 | 
 133 | doPrint : String -> (Nat, Nat) -> (Nat, Nat) -> IO ()
 134 | doPrint path start end =
 135 |   let fc = MkFC (Just path) start end
 136 |       str = getSpanSnippet fc
 137 |   in
 138 |   case !str of
 139 |        Nothing => putStrLn "error"
 140 |        (Just x) => putStrLn x
 141 |