0 | module Katla.Engine

  2 | import System

  3 | import System.File

  4 | import Core.FC

  5 | import Core.Name

  6 | import Core.Core

  7 | import Core.Context

  8 | import Core.Metadata

  9 | import Libraries.Data.PosMap

 10 | import Libraries.Text.Literate

 11 | import Libraries.Text.Bounded

 12 | import Parser.Unlit

 13 | import Data.List1

 14 | import Data.List

 15 | import Data.Maybe

 16 | import Data.String

 17 | import Data.SnocList

 19 | import Katla.Config

 20 | import Katla.HTML

 21 | import Katla.LaTeX

 22 | import Katla.Markdown

 23 | import Katla.Literate

 32 | pickSmallest : List1 ASemanticDecoration -> Decoration

 33 | pickSmallest ((_, decor, _) ::: []) = decor

 34 | pickSmallest (current ::: candidate :: ds) =

 35 |   let endOf : ASemanticDecoration -> (Int, Int)

 36 |       endOf ((_, (_, end)), _, _) = end

 37 |   in if (endOf candidate < endOf current)

 38 |      then pickSmallest (candidate ::: ds)

 39 |      else pickSmallest (current   ::: ds)

 41 | public export

 42 | Position : Type

 43 | Position = (Int, Int)

 46 | nextRow : Position -> Position

 47 | nextRow (row, _) = (row + 1, 0)

 50 | nextColumn : Position -> Position

 51 | nextColumn (row, col) = (row, col + 1)

 53 | findDecoration : Position -> PosMap ASemanticDecoration -> Maybe Decoration

 54 | findDecoration pos@(row, col) posMap =

 55 |   case dominators ((row, col), (row, col+1)) posMap of

 56 |    []              => Nothing

 57 |    (d :: ds)       => Just $ pickSmallest (d ::: ds)

 59 | toString : SnocList Char -> String

 60 | toString sx = (fastPack $ sx <>> [])

 62 | snocEscape : (escape : Char -> List Char) ->

 63 |              (outputChars : SnocList Char) -> (new : Char) -> SnocList Char

 64 | snocEscape escape sx c = sx <>< escape c

 67 | isNotEndOfLine : List Char -> Maybe (Char, List Char)

 68 | isNotEndOfLine []           = Nothing

 69 | isNotEndOfLine ('\r' :: _ ) = Nothing

 70 | isNotEndOfLine ('\n' :: _ ) = Nothing

 71 | isNotEndOfLine (x    :: xs) = Just (x, xs)

 73 | ship : (output : File) ->

 74 |        Driver ->

 75 |        Maybe Decoration -> (outputChars : SnocList Char) -> IO ()

 76 | ship output driver decor outputChars = when (isSnoc outputChars) $ do

 77 |    let decorated = driver.annotate decor (toString outputChars)

 78 |    ignore $ fPutStr output decorated

 80 | processLine : (output : File)

 81 |            -> (meta : PosMap ASemanticDecoration)

 82 |            -> Driver

 83 |            -> (currentDecor  : Maybe Decoration)

 84 |            -> (currentPos    : Position)

 85 |            -> (endPos : Maybe Position)

 86 |            -> (remainingLine : List Char)

 87 |            -> (currentOutput : SnocList Char)

 88 |            -> IO (Maybe Decoration, Position)

 89 | processLine output meta driver currentDecor currentPos endPos cs currentOutput

 90 |   = case (isNotEndOfLine cs, maybe True (currentPos <) endPos) of

 91 |       -- We've reached the end of the line: output and return

 92 |       (Nothing, _) => do

 93 |         let nextPos = nextRow currentPos

 94 |         ship output driver currentDecor currentOutput

 95 |         ignore $ fPutStrLn output (snd driver.line)

 96 |         pure (currentDecor, nextPos)

 97 |       -- We're past the caller-provided end position: output and return

 98 |       (Just _         , False) => do

 99 |         ship output driver currentDecor currentOutput

100 |         ignore $ fPutStrLn output ""

101 |         pure (currentDecor, currentPos)

102 |       -- We're still in bounds and have found a new character

103 |       -- Assuming decorations may overlap, we need to check whether there is a

104 |       -- new one or whether we can keep munching the line using the same decor.

105 |       -- If we were willing to assume decorations are non-overlapping we could

106 |       -- just return the size of the decorated chunk in `findDecoration` and

107 |       -- grab it whole here.

108 |       (Just (c , rest), True) => do

109 |         let nextPos = nextColumn currentPos

110 |             decor   = findDecoration currentPos meta

111 |         if decor == currentDecor

112 |          then let c = snocEscape driver.escape currentOutput c in

113 |               processLine output meta driver currentDecor nextPos endPos rest c

114 |          else do ship output driver currentDecor currentOutput

115 |                  let c = snocEscape driver.escape [<] c

116 |                  processLine output meta driver decor nextPos endPos rest c

118 | processLines : (output : File)

119 |            -> (meta : PosMap ASemanticDecoration)

120 |            -> Driver

121 |            -> (currentDecor  : Maybe Decoration)

122 |            -> (currentPos    : Position)

123 |            -> (remainingLine : List String)

124 |            -> IO (Maybe Decoration, Position)

125 | processLines output meta driver currentDecor currentPos [] = pure (currentDecor, currentPos)

126 | processLines output meta driver currentDecor currentPos (l :: ls) = do

127 |   (nextDecor, nextPos) <- processLine output meta driver currentDecor currentPos Nothing (unpack l) [<]

128 |   processLines output meta driver nextDecor nextPos ls

131 |   : (output : File)

132 |   -> (lineNumberWidth : Nat) -- width of the largest line number e.g. 3 for 999

133 |   -> (meta : PosMap ASemanticDecoration)

134 |   -> Driver

135 |   -> List (WithBounds LitToken)

136 |   -> IO ()

137 | engineLitWithDecor output lineNumberWidth meta driver [] = pure ()

138 | engineLitWithDecor output lineNumberWidth meta driver (t :: ts) = do

139 |   case t.val of

140 |     CodeBlock _ _ src => do

141 |       -- src contains both the opening & closing lines of the code block

142 |       -- we extract the "options" coming after the opening token e.g. "```idris hide"

143 |       -- and the content of the block

144 |       let (opts, content) = case lines src of

145 |                               hd :: tl => (fromMaybe [] (tail' $ words hd), fromMaybe [] (init' tl))

146 |                               [] => ([], [])

147 |       unless ("hide" `elem` opts) $ do

148 |         let (pre, post) = driver.blockMacro

149 |         -- a code block is opened by a keyword + untilEOL

150 |         -- so the start of the code block is the beginning of the next line

151 |         -- TODO: look at `l` to see if there are any options

152 |         ignore $ fPutStrLn output (pre "")

153 |         let pos = bimap (1+) (const 0) (start t)

154 |         ignore $ processLines output meta driver Nothing pos content

155 |         ignore $ fPutStr output post

156 |     Any str => ignore $ fPutStr output str

157 |     CodeLine _ _ => pure () -- not supported for now

158 |   engineLitWithDecor output lineNumberWidth meta driver ts

161 |   : (input, output : File)

162 |   -> (lineNumberWidth : Nat) -- width of the largest line number e.g. 3 for 999

163 |   -> (meta : PosMap ASemanticDecoration)

164 |   -> Driver

165 |   -> Maybe Decoration -> Position -> IO ()

166 | engineWithDecor input output lineNumberWidth meta driver currentDecor currentPos

167 |   = when (not !(fEOF input)) $ do

168 |       Right str <- fGetLine input

169 |         | Left err => pure ()

170 |       -- if we're starting a new line, output the corresponding marker

171 |       when (snd currentPos == 0) $

172 |         ignore $ fPutStr output

173 |                $ fst driver.line lineNumberWidth

174 |                $ cast $ fst currentPos

175 |       -- then process the line

176 |       next <- processLine output meta driver currentDecor currentPos Nothing

177 |                 (fastUnpack str) [<]

178 |       let (nextDecor, nextPos) = next

179 |       engineWithDecor input output lineNumberWidth meta driver nextDecor nextPos

182 | record ListingRange where

183 |   constructor MkListingRange

184 |   startRow, startCol,

185 |   endRow, endCol : Int

188 | RowRangeByOffset : (offset, before, after : Int) -> ListingRange

189 | RowRangeByOffset offset before after = MkListingRange

190 |   { startRow = offset - before

191 |   , endRow = offset + after + 1

192 |   , startCol = 0

193 |   , endCol = 0}

196 | RangeByOffsetAndCols : (offset, after,startCol,endCol : Int) -> ListingRange

197 | RangeByOffsetAndCols offset after startCol endCol =

198 |   let row = offset + after

199 |   in MkListingRange

200 |   { startRow = row

201 |   , startCol = startCol

202 |   , endRow   = row

203 |   , endCol   = endCol

204 |   }

206 | (.start),(.end) : ListingRange -> Position

207 | range.start = (range.startRow, range.startCol)

208 | range.end   = (range.endRow, range.endCol)

212 |   : (input, output : File)

213 |   -> (lineNumberWidth : Nat) -- width of the largest line number e.g. 3 for 999

214 |   -> (meta : PosMap ASemanticDecoration)

215 |   -> Driver

216 |   -> ListingRange

217 |   -> Maybe Decoration -> Position -> IO ()

218 | engineWithRange input output lineNumberWidth meta driver rowRange currentDecor currentPos

219 |   = when (not !(fEOF input)) $ do

220 |       Right str <- fGetLine input

221 |         | Left err => pure ()

222 |       (nextDecor, nextPos) <- (

223 |          -- If the current line in the file intersects with the range

224 |          -- then process the line and otherwise just go to the next one

225 |          if rowRange.startRow <= fst currentPos && currentPos < rowRange.end

226 |          then do

227 |            let (decor, startPos, relevantLine) =

228 |                    if rowRange.startRow == fst currentPos

229 |                      then ( Nothing

230 |                           , (fst currentPos, rowRange.startCol)

231 |                           , drop (cast rowRange.startCol) (fastUnpack str))

232 |                      else (currentDecor, currentPos, fastUnpack str)

233 |            let endPos = Just rowRange.end

234 |            ignore $ fPutStr output

235 |                   $ fst driver.line lineNumberWidth

236 |                   $ cast $ fst currentPos

237 |            processLine output meta driver decor startPos endPos relevantLine [<]

238 |          else pure (Nothing, nextRow currentPos))

239 |       -- stop processing the file as soon as we're beyond the range

240 |       unless (rowRange.end < nextPos) $

241 |         engineWithRange input output lineNumberWidth meta driver rowRange nextDecor nextPos

244 | engine : Backend

245 |        -> Config

246 |        -> (input, output : File)

247 |        -> (lineNumberWidth : Nat)

248 |        -> (meta : PosMap ASemanticDecoration)

249 |        -> Driver

250 |        -> Position

251 |        -> IO ()

252 | engine Markdown cfg input output lnw meta driver pos

253 |   = do Right content <- fRead input

254 |          | Left err => do putStrLn "Error: \{show err}"

255 |                           exitFailure

256 |        let Right ts = lexLiterate styleCMark content

257 |          | Left err => do putStrLn "Error: \{show err}"

258 |                           exitFailure

259 |        engineLitWithDecor output lnw meta driver ts

260 | engine Literate cfg input output lnw meta driver pos

261 |   = do Right content <- fRead input

262 |          | Left err => do putStrLn "Error: \{show err}"

263 |                           exitFailure

264 |        let Right ts = lexLiterate styleTeX content

265 |          | Left err => do putStrLn "Error: \{show err}"

266 |                           exitFailure

267 |        initSty cfg

268 |        engineLitWithDecor output lnw meta driver ts

269 | engine _ _ input output lnw meta driver pos

270 |   = engineWithDecor input output lnw meta driver Nothing pos

272 | record FileHandles where

273 |   constructor MkHandles

274 |   config : Config

275 |   source, output : File

276 |   metadata : PosMap ASemanticDecoration

278 | data Error a = ReportedError | Unreported a

280 | orDie : Core a -> (Error -> String) -> IO a

281 | orDie a k = coreRun a

282 |   (\ err => ignore (fPutStrLn {io = IO} stderr (k err)) >> exitFailure)

283 |   pure

286 | setupFiles : Backend ->

287 |   (mconfig : Maybe String) ->

288 |   (msourcefile, mmetadata : String) ->

289 |   (moutput : Maybe String) ->

290 |   IO FileHandles

291 | setupFiles backend mconfig filename metadata moutput = do

292 |   config <- getConfiguration backend mconfig

293 |   Right source <- openFile filename Read

294 |     | Left err =>

295 |        do ignore $ fPutStrLn stderr

296 |             """

300 |           exitFailure

301 |   fmd <- readMetadata metadata `orDie` \ err =>

302 |           """

306 |   Right output <- maybe

307 |               (pure $ Right stdout)

308 |               (\output => openFile output WriteTruncate)

309 |               moutput

310 |     | Left err =>

311 |       do ignore $ fPutStrLn stderr

312 |            """

316 |          exitFailure

317 |   -- required because `allSemanticHighlighting` does some logging

318 |   meta <- (do defs <- initDefs

319 |               c <- newRef Ctxt defs

320 |               allSemanticHighlighting fmd)

321 |           `orDie` \ err => "Couldn't assemble metadata: \{show err}"

323 |   pure $ MkHandles

324 |     { config, source, output

325 |     , metadata = meta

326 |     }

328 | public export

329 | data Snippet

330 |   = Raw (Maybe ListingRange)

331 |   | Macro (String, Bool, Maybe ListingRange)

333 | (.listing) : Snippet -> Maybe ListingRange

334 | (Raw mrange          ).listing = mrange

335 | (Macro (_, _, mrange)).listing = mrange

337 | mkDriver : Backend -> (Config -> Driver)

338 | mkDriver HTML = HTML.mkDriver

339 | mkDriver LaTeX = LaTeX.mkDriver

340 | mkDriver Markdown = Markdown.mkDriver

341 | mkDriver Literate = Literate.mkDriver

344 | katla : (backend : Backend) ->

345 |         (snippet : Maybe Snippet) ->

346 |         (mconfig : Maybe String) ->

347 |         (msourcefile, mmetadata, moutput : Maybe String) ->

348 |         -- TODO: would be nice to only specify one of source/metadata

349 |         IO ()

350 | katla _ _       _       Nothing _       _

351 |   = putStrLn "Expecting source file to print."

352 | katla _ _       _       _       Nothing _

353 |   = putStrLn "Expecting metadata file to output."

355 | katla backend Nothing mconfig (Just filename) (Just metadata) moutput = do

356 |   files <- setupFiles backend mconfig filename metadata moutput

358 |   let error : String -> IO ()

359 |       error str = do ignore $ fPutStrLn stderr "Error while \{str}"

360 |                      closeFile files.output

361 |                      exitFailure

363 |   let driver = mkDriver backend files.config

364 |   let (standalonePre, standalonePost) = driver.standalone

366 |   Right _ <- fPutStrLn files.output standalonePre

367 |     | Left err => error "generating preamble: \{show err}"

368 |   Right content <- readFile filename

369 |      | Left err  => error "opening file: \{show err}"

370 |   let lnw = length $ show $ length $ lines content

371 |   engine backend files.config files.source files.output lnw files.metadata driver (0,0)

372 |   Right _ <- fPutStrLn files.output standalonePost

373 |     | Left err => error "generating preamble: \{show err}"

374 |   closeFile files.output

376 | katla backend (Just snippet) mconfig (Just filename) (Just metadata) moutput = do

377 |   files <- setupFiles backend mconfig filename metadata moutput

379 |   let error : String -> IO ()

380 |       error str = do putStrLn "Error while \{str}"

381 |                      closeFile files.output

382 |                      exitFailure

384 |   let driver = mkDriver backend files.config

385 |   case snippet of

386 |     Raw _ => pure ()

387 |     Macro (name, inline, mrange) => do -- TODO: validate macro name, perhaps when parsing

388 |       let (pre, _) = ifThenElse inline driver.inlineMacro driver.blockMacro

389 |       Right _ <- fPutStrLn files.output (pre name)

390 |         | Left err => error "generating macro name \{name}: \{show err}"

391 |       pure ()

392 |   case snippet.listing of

393 |     Nothing    =>

394 |       do Right content <- readFile filename

395 |            | Left err  => error "opening file: \{show err}"

396 |          let lnw = length $ show $ length $ lines content

397 |          engine backend files.config files.source files.output lnw files.metadata driver (0,0)

398 |     Just range =>

399 |       do let lnw = length $ show range.endRow

400 |          engineWithRange files.source files.output lnw files.metadata driver range Nothing (0,0)

401 |   case snippet of

402 |     Raw _ => pure ()

403 |     Macro (name, inline, mrange) => do

404 |       let (_, post) = ifThenElse inline driver.inlineMacro driver.blockMacro

405 |       Right _ <- fPutStrLn files.output post

406 |         | Left err => error "generating macro name \{name}: \{show err}"

407 |       pure ()

409 |   closeFile files.output