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.Typst

 23 | import Katla.Markdown

 24 | import Katla.Literate

 33 | pickSmallest : List1 ASemanticDecoration -> Decoration

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

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

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

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

 38 |   in if (endOf candidate < endOf current)

 39 |      then pickSmallest (candidate ::: ds)

 40 |      else pickSmallest (current   ::: ds)

 42 | public export

 43 | Position : Type

 44 | Position = (Int, Int)

 47 | nextRow : Position -> Position

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

 51 | nextColumn : Position -> Position

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

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

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

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

 57 |    []              => Nothing

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

 60 | toString : SnocList Char -> String

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

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

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

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

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

 69 | isNotEndOfLine []           = Nothing

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

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

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

 74 | ship : (output : File) ->

 75 |        Driver ->

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

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

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

 79 |    ignore $ fPutStr output decorated

 81 | processLine : (output : File)

 82 |            -> (meta : PosMap ASemanticDecoration)

 83 |            -> Driver

 84 |            -> (currentDecor  : Maybe Decoration)

 85 |            -> (currentPos    : Position)

 86 |            -> (endPos : Maybe Position)

 87 |            -> (remainingLine : List Char)

 88 |            -> (currentOutput : SnocList Char)

 89 |            -> IO (Maybe Decoration, Position)

 90 | processLine output meta driver currentDecor currentPos endPos cs currentOutput

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

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

 93 |       (Nothing, _) => do

 94 |         let nextPos = nextRow currentPos

 95 |         ship output driver currentDecor currentOutput

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

 97 |         pure (currentDecor, nextPos)

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

 99 |       (Just _         , False) => do

100 |         ship output driver currentDecor currentOutput

101 |         ignore $ fPutStrLn output ""

102 |         pure (currentDecor, currentPos)

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

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

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

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

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

108 |       -- grab it whole here.

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

110 |         let nextPos = nextColumn currentPos

111 |             decor   = findDecoration currentPos meta

112 |         if decor == currentDecor

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

114 |               processLine output meta driver currentDecor nextPos endPos rest c

115 |          else do ship output driver currentDecor currentOutput

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

117 |                  processLine output meta driver decor nextPos endPos rest c

119 | processLines : (output : File)

120 |            -> (meta : PosMap ASemanticDecoration)

121 |            -> Driver

122 |            -> (currentDecor  : Maybe Decoration)

123 |            -> (currentPos    : Position)

124 |            -> (remainingLine : List String)

125 |            -> IO (Maybe Decoration, Position)

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

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

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

129 |   processLines output meta driver nextDecor nextPos ls

132 |   : (output : File)

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

134 |   -> (meta : PosMap ASemanticDecoration)

135 |   -> Driver

136 |   -> List (WithBounds LitToken)

137 |   -> IO ()

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

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

140 |   case t.val of

141 |     CodeBlock _ _ src => do

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

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

144 |       -- and the content of the block

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

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

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

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

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

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

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

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

153 |         ignore $ fPutStrLn output (pre "")

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

155 |         ignore $ processLines output meta driver Nothing pos content

156 |         ignore $ fPutStr output post

157 |     Any str => ignore $ fPutStr output str

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

159 |   engineLitWithDecor output lineNumberWidth meta driver ts

162 |   : (input, output : File)

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

164 |   -> (meta : PosMap ASemanticDecoration)

165 |   -> Driver

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

167 | engineWithDecor input output lineNumberWidth meta driver currentDecor currentPos

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

169 |       Right str <- fGetLine input

170 |         | Left err => pure ()

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

172 |       when (snd currentPos == 0) $

173 |         ignore $ fPutStr output

174 |                $ fst driver.line lineNumberWidth

175 |                $ cast $ fst currentPos

176 |       -- then process the line

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

178 |                 (fastUnpack str) [<]

179 |       let (nextDecor, nextPos) = next

180 |       engineWithDecor input output lineNumberWidth meta driver nextDecor nextPos

183 | record ListingRange where

184 |   constructor MkListingRange

185 |   startRow, startCol,

186 |   endRow, endCol : Int

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

190 | RowRangeByOffset offset before after = MkListingRange

191 |   { startRow = offset - before

192 |   , endRow = offset + after + 1

193 |   , startCol = 0

194 |   , endCol = 0}

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

198 | RangeByOffsetAndCols offset after startCol endCol =

199 |   let row = offset + after

200 |   in MkListingRange

201 |   { startRow = row

202 |   , startCol = startCol

203 |   , endRow   = row

204 |   , endCol   = endCol

205 |   }

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

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

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

213 |   : (input, output : File)

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

215 |   -> (meta : PosMap ASemanticDecoration)

216 |   -> Driver

217 |   -> ListingRange

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

219 | engineWithRange input output lineNumberWidth meta driver rowRange currentDecor currentPos

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

221 |       Right str <- fGetLine input

222 |         | Left err => pure ()

223 |       (nextDecor, nextPos) <- (

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

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

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

227 |          then do

228 |            let (decor, startPos, relevantLine) =

229 |                    if rowRange.startRow == fst currentPos

230 |                      then ( Nothing

231 |                           , (fst currentPos, rowRange.startCol)

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

233 |                      else (currentDecor, currentPos, fastUnpack str)

234 |            let endPos = Just rowRange.end

235 |            ignore $ fPutStr output

236 |                   $ fst driver.line lineNumberWidth

237 |                   $ cast $ fst currentPos

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

239 |          else pure (Nothing, nextRow currentPos))

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

241 |       unless (rowRange.end < nextPos) $

242 |         engineWithRange input output lineNumberWidth meta driver rowRange nextDecor nextPos

245 | engine : Backend

246 |        -> Config

247 |        -> (input, output : File)

248 |        -> (lineNumberWidth : Nat)

249 |        -> (meta : PosMap ASemanticDecoration)

250 |        -> Driver

251 |        -> Position

252 |        -> IO ()

253 | engine Typst cfg input output lnw meta driver pos

254 |   = do Right content <- fRead input

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

256 |                           exitFailure

257 |        let Right ts = lexLiterate styleCMark content

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

259 |                           exitFailure

260 |        engineLitWithDecor output lnw meta driver ts

261 | engine Markdown cfg input output lnw meta driver pos

262 |   = do Right content <- fRead input

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

264 |                           exitFailure

265 |        let Right ts = lexLiterate styleCMark content

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

267 |                           exitFailure

268 |        engineLitWithDecor output lnw meta driver ts

269 | engine Literate cfg input output lnw meta driver pos

270 |   = do Right content <- fRead input

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

272 |                           exitFailure

273 |        let Right ts = lexLiterate styleTeX content

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

275 |                           exitFailure

276 |        initSty cfg

277 |        engineLitWithDecor output lnw meta driver ts

278 | engine _ _ input output lnw meta driver pos

279 |   = engineWithDecor input output lnw meta driver Nothing pos

281 | record FileHandles where

282 |   constructor MkHandles

283 |   config : Config

284 |   source, output : File

285 |   metadata : PosMap ASemanticDecoration

287 | data Error a = ReportedError | Unreported a

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

290 | orDie a k = coreRun a

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

292 |   pure

295 | setupFiles : Backend ->

296 |   (mconfig : Maybe String) ->

297 |   (msourcefile, mmetadata : String) ->

298 |   (moutput : Maybe String) ->

299 |   IO FileHandles

300 | setupFiles backend mconfig filename metadata moutput = do

301 |   config <- getConfiguration backend mconfig

302 |   Right source <- openFile filename Read

303 |     | Left err =>

304 |        do ignore $ fPutStrLn stderr

305 |             """

309 |           exitFailure

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

311 |           """

315 |   Right output <- maybe

316 |               (pure $ Right stdout)

317 |               (\output => openFile output WriteTruncate)

318 |               moutput

319 |     | Left err =>

320 |       do ignore $ fPutStrLn stderr

321 |            """

325 |          exitFailure

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

327 |   meta <- (do defs <- initDefs

328 |               c <- newRef Ctxt defs

329 |               allSemanticHighlighting fmd)

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

332 |   pure $ MkHandles

333 |     { config, source, output

334 |     , metadata = meta

335 |     }

337 | public export

338 | data Snippet

339 |   = Raw (Maybe ListingRange)

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

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

343 | (Raw mrange          ).listing = mrange

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

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

347 | mkDriver HTML = HTML.mkDriver

348 | mkDriver LaTeX = LaTeX.mkDriver

349 | mkDriver Typst = Typst.mkDriver

350 | mkDriver Markdown = Markdown.mkDriver

351 | mkDriver Literate = Literate.mkDriver

354 | katla : (backend : Backend) ->

355 |         (snippet : Maybe Snippet) ->

356 |         (mconfig : Maybe String) ->

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

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

359 |         IO ()

360 | katla _ _       _       Nothing _       _

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

362 | katla _ _       _       _       Nothing _

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

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

366 |   files <- setupFiles backend mconfig filename metadata moutput

368 |   let error : String -> IO ()

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

370 |                      closeFile files.output

371 |                      exitFailure

373 |   let driver = mkDriver backend files.config

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

376 |   Right _ <- fPutStrLn files.output standalonePre

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

378 |   Right content <- readFile filename

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

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

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

382 |   Right _ <- fPutStrLn files.output standalonePost

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

384 |   closeFile files.output

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

387 |   files <- setupFiles backend mconfig filename metadata moutput

389 |   let error : String -> IO ()

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

391 |                      closeFile files.output

392 |                      exitFailure

394 |   let driver = mkDriver backend files.config

395 |   case snippet of

396 |     Raw _ => pure ()

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

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

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

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

401 |       pure ()

402 |   case snippet.listing of

403 |     Nothing    =>

404 |       do Right content <- readFile filename

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

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

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

408 |     Just range =>

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

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

411 |   case snippet of

412 |     Raw _ => pure ()

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

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

415 |       Right _ <- fPutStrLn files.output post

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

417 |       pure ()

419 |   closeFile files.output