1 | module Goop.Pandoc.HTML

  3 | import Data.List

  4 | import Data.Primitives.Interpolation

  5 | import Data.Set

  6 | import Data.SnocList

  7 | import Data.SortedMap

  8 | import Data.String

  9 | import Derive.Prelude

 11 | import Data.Linear.Ref1

 12 | import Data.Linear.Traverse1

 13 | import Syntax.T1

 15 | import Goop.Pandoc.JSON

 17 | %language ElabReflection

 23 | public export

 24 | Attr : Type

 25 | Attr = (String, List String)

 27 | jsonAttrToAttrs : JAttr -> List Attr

 28 | jsonAttrToAttrs (MkJAttr id classes pairs) =

 29 |   let

 30 |     pairs_map : SortedMap String (List String) =

 31 |       foldl (\acc, (k, v) => insertWith (++) k v acc) empty $

 32 |         map (\(x, y) => (x, (the (List _) [y]))) pairs

 33 |     reduced_pairs = SortedMap.toList pairs_map

 34 |     id_pair = ("id", [id])

 35 |     classes_pair = ("class", classes)

 36 |     all_pairs = id_pair :: classes_pair :: reduced_pairs

 37 |     remove_empty_strings : Attr -> Attr

 38 |     remove_empty_strings (x, ys) = (x, filter (not . null) ys)

 39 |     empty_attr : Attr -> Bool

 40 |     empty_attr (x, []) = True

 41 |     empty_attr (x, (y :: ys)) = False

 42 |   in filter (not . empty_attr) . map remove_empty_strings $ all_pairs

 44 | public export

 45 | data Element : Type where

 46 |   Raw : (contents : String) -> Element

 47 |   Collection : (List Element) -> Element

 48 |   Void : (tag : String) -> Element

 49 |   VoidAttrs : (tag : String) -> (attrs : List Attr) -> Element

 50 |   Normal : (tag : String) -> (contents : List Element) -> Element

 51 |   NormalAttrs : (tag : String) -> (attrs : List Attr) -> (contents : List Element) -> Element

 52 | %runElab derive "Element" [Show]

 77 | namespace GenState

 78 |   public export

 79 |   record State where

 80 |     constructor MkState

 81 |     existing_ids : Set String

 82 |     footnotes : SnocList Element

 84 |   export

 85 |   empty : State

 86 |   empty = MkState empty [<]

 88 |   export

 89 |   insertFootnote : Ref s State -> List Element -> F1 s (String, Nat)

 90 |   insertFootnote state xs = T1.do

 91 |     current_footnotes <- mapF1 footnotes $ read1 state

 92 |     let id = 1 + length current_footnotes

 93 |     let x =

 94 |       NormalAttrs "li"

 95 |          [("id", ["fn\{id}"])]

 96 |          (xs ++ [NormalAttrs "a" [("href", ["#ref-fn\{id}"]), ("class", ["footnote-back"])] [Raw "↩︎"]])

 97 |     mod1 state {footnotes := current_footnotes :< x}

 98 |     pure ("fn\{id}", id)

100 | inlineToHtml : (state : Ref s State) -> Inline -> F1 s Element

101 | blockToHtml : (state : Ref s State) -> Block -> F1 s Element

103 | inlineToHtml _ (Str str) =

104 |   pure $ Raw str

105 | inlineToHtml state (Emph xs) =

106 |   mapF1 (Normal "em") . traverse1 (inlineToHtml state) $ xs

107 | inlineToHtml state (Underline xs) =

108 |   mapF1 (NormalAttrs "span" [("class", ["underline"])]) . traverse1 (inlineToHtml state) $ xs

109 | inlineToHtml state (Strong xs) =

110 |   mapF1 (Normal "strong") . traverse1 (inlineToHtml state) $ xs

111 | inlineToHtml state (Strikeout xs) =

112 |   mapF1 (Normal "s") . traverse1 (inlineToHtml state) $ xs

113 | inlineToHtml state (Superscript xs) =

114 |   mapF1 (Normal "sup") . traverse1 (inlineToHtml state) $ xs

115 | inlineToHtml state (Subscript xs) =

116 |   mapF1 (Normal "sub") . traverse1 (inlineToHtml state) $ xs

117 | inlineToHtml state (SmallCaps xs) =

118 |   mapF1 (NormalAttrs "span" [("class", ["smallcaps"])]) . traverse1 (inlineToHtml state) $ xs

119 | inlineToHtml state (Quoted SingleQuote xs) =

120 |   mapF1 (NormalAttrs "q" [("class", ["single-quote"])]) . traverse1 (inlineToHtml state) $ xs

121 | inlineToHtml state (Quoted DoubleQuote xs) =

122 |   mapF1 (NormalAttrs "q" [("class", ["double-quote"])]) . traverse1 (inlineToHtml state) $ xs

123 | inlineToHtml _ (Code _ str) =

124 |   pure $ Normal "code" [Raw str]

125 | inlineToHtml _ (Space _) = pure $ Raw " "

126 | inlineToHtml _ (SoftBreak _) = pure $ Void "wbr"

127 | inlineToHtml _ (LineBreak _) = pure $ Void "br"

128 | inlineToHtml state (Link _ xs (url, title)) =

129 |   if null title

130 |   then mapF1 (NormalAttrs "a" [("href", [url])]) . traverse1 (inlineToHtml state) $ xs

131 |   else mapF1 (NormalAttrs "a" [("href", [url]), ("title", [title])])

132 |      . traverse1 (inlineToHtml state)

133 |      $ xs

134 | inlineToHtml state (Span x xs) =

135 |   let attrs = jsonAttrToAttrs x

136 |   in if isNil attrs

137 |     then mapF1 (Normal "span") . traverse1 (inlineToHtml state) $ xs

138 |     else mapF1 (NormalAttrs "span" attrs) . traverse1 (inlineToHtml state) $ xs

139 | inlineToHtml state (Note xs) = T1.do

140 |   contents <- traverse1 (blockToHtml state) xs

141 |   (id, id_nat) <- insertFootnote state contents

142 |   pure $ NormalAttrs "a"

143 |                      [("href", [id]), ("class", ["footnote-ref"]), ("id", ["ref-\{id}"])]

144 |                      [Normal "sup" [Raw "\{id_nat}"]]

149 | inlineToHtml state x = ?inlineToHtml_rhs

151 | blockToHtml state (Para xs) =

152 |   mapF1 (Normal "p") . traverse1 (inlineToHtml state) $ xs

153 | blockToHtml state (Plain xs) =

154 |   mapF1 Collection . traverse1 (inlineToHtml state) $ xs

155 | blockToHtml _ (CodeBlock x str) = pure $

156 |   let attrs = jsonAttrToAttrs x

157 |   in if isNil attrs

158 |     then Normal "pre" [Normal "code" [Raw str]]

159 |     else Normal "pre" [NormalAttrs "code" attrs [Raw str]]

160 | blockToHtml state (LineBlock xss) = do

161 |   inner <- traverse1 (traverse1 (inlineToHtml state)) xss

162 |   let children = map (NormalAttrs "span" [("class", ["nonbreaking"])]) inner

163 |   pure $ Collection children

164 | blockToHtml state (BlockQuote xs) =

165 |   mapF1 (Normal "blockquote") . traverse1 (blockToHtml state) $ xs

166 | blockToHtml state (Header k x xs) =

167 |   let attrs = jsonAttrToAttrs x

168 |   in if isNil attrs

169 |     then mapF1 (Normal "h\{k}") . traverse1 (inlineToHtml state) $ xs

170 |     else mapF1 (NormalAttrs "h\{k}" attrs) . traverse1 (inlineToHtml state) $ xs

171 | blockToHtml state (Div x xs) =

172 |   let attrs = jsonAttrToAttrs x

173 |   in if isNil attrs

174 |     then mapF1 (Normal "div") . traverse1 (blockToHtml state) $ xs

175 |     else mapF1 (NormalAttrs "div" attrs) . traverse1 (blockToHtml state) $ xs

176 | blockToHtml _ (HorizontalRule _) =

177 |   pure $ Void "hr"

184 | blockToHtml state x = ?blockToHtml_rhs

186 | combineRawsList : List Element -> List Element

187 | combineRaws : Element -> Element

189 | combineRawsList [] = []

190 | combineRawsList (x :: []) = [combineRaws x]

191 | combineRawsList ((Raw contents_x) :: ((Raw contents_y) :: xs)) =

192 |   combineRawsList $ (Raw (contents_x ++ contents_y)) :: xs

193 | combineRawsList ((Raw contents_x) :: ((Void "wbr") :: xs)) =

194 |   combineRawsList $ (Raw "\{contents_x} ") :: xs

195 | combineRawsList (x :: ((Void "wbr") :: xs)) =

196 |   combineRawsList $ x :: (Raw " ") :: xs

197 | combineRawsList (x :: (y :: xs)) = (combineRaws x) :: combineRawsList (y :: xs)

199 | combineRaws (Collection xs) = Collection $ combineRawsList xs

200 | combineRaws (Normal tag contents) = Normal tag $ combineRawsList contents

201 | combineRaws (NormalAttrs tag attrs contents) = NormalAttrs tag attrs $ combineRawsList contents

202 | combineRaws x = x

209 | attrToString : Attr -> String

210 | attrToString (key, xs) =

211 |   let value = joinBy " " xs

212 |   in "\{key}=\"\{value}\""

214 | attrsToString : List Attr -> String

215 | attrsToString xs = joinBy " " (map attrToString xs)

217 | tagInline : String -> Bool

218 | tagInline "html" = False

219 | tagInline "head" = False

220 | tagInline "body" = False

221 | tagInline "header" = False

222 | tagInline "main" = False

223 | tagInline "article" = False

224 | tagInline "section" = False

225 | tagInline "ol" = False

226 | tagInline "link" = False

227 | tagInline "title" = False

228 | tagInline "meta" = False

229 | tagInline _ = True

232 | data TagRendering = TInline | TSemiInline | TNotInline

234 | tagType : String -> TagRendering

235 | tagType "html" = TNotInline

236 | tagType "head" = TNotInline

237 | tagType "body" = TNotInline

238 | tagType "header" = TNotInline

239 | tagType "main" = TNotInline

240 | tagType "article" = TNotInline

241 | tagType "section" = TNotInline

242 | tagType "ol" = TNotInline

243 | tagType "li" = TNotInline

244 | tagType "link" = TSemiInline

245 | tagType "title" = TSemiInline

246 | tagType "meta" = TSemiInline

247 | tagType "p" = TSemiInline

248 | tagType "h1" = TSemiInline

249 | tagType "h2" = TSemiInline

250 | tagType "h3" = TSemiInline

251 | tagType "h4" = TSemiInline

252 | tagType "h5" = TSemiInline

253 | tagType "h6" = TSemiInline

254 | tagType _ = TInline

256 | indentStr : Nat -> String

257 | indentStr 0 = ""

258 | indentStr (S k) = "  " ++ indentStr k

260 | data LineState = Inline | NewLine

261 | %runElab derive "LineState" [Eq]

263 | record RenderState s where

264 |   constructor MkRS

265 |   indent_level : Ref s Nat

266 |   line_state : Ref s LineState

267 |   buffer : Ref s String

269 | initial : F1 s (RenderState s)

270 | initial = T1.do

271 |   indent_level <- ref1 0

272 |   line_state <- ref1 NewLine

273 |   buffer <- ref1 ""

274 |   pure $ MkRS indent_level line_state buffer

276 | (.indent_string) : RenderState s -> F1 s String

277 | (.indent_string) x = do

278 |   il <- read1 x.indent_level

279 |   pure $ replicate (2 * il) ' '

281 | (.add_component) : RenderState s -> String -> F1' s

282 | (.add_component) x str = do

283 |   ls <- read1 x.line_state

284 |   case ls of

285 |     Inline => mod1 x.buffer (++ str)

286 |     NewLine => do

287 |       is <- x.indent_string

288 |       mod1 x.buffer (++ "\{is}\{str}")

289 |       write1 x.line_state Inline

291 | (.newline) : (rs : RenderState s) -> F1' s

292 | (.newline) rs = do

293 |   Inline <- read1 rs.line_state

294 |     | NewLine => pure ()

295 |   is <- rs.indent_string

296 |   mod1 rs.buffer (++ "\n")

297 |   write1 rs.line_state NewLine

299 | (.indent) : (rs : RenderState s) -> F1' s -> F1' s

300 | (.indent) rs f = T1.do

301 |   orig <- read1 rs.indent_level

302 |   mod1 rs.indent_level (+ 1)

303 |   f

304 |   write1 rs.indent_level orig

306 | renderElement : (rs : RenderState s) -> Element -> F1' s

307 | (.add_type) : (rs : RenderState s) -> (start, close : String) -> TagRendering -> List Element -> F1' s

309 | (.add_type) rs start close TInline xs = T1.do

310 |   rs.add_component start

311 |   traverse1_ (renderElement rs) xs

312 |   rs.add_component close

313 | (.add_type) rs start close TSemiInline xs = T1.do

314 |   rs.newline

315 |   rs.add_component start

316 |   traverse1_ (renderElement rs) xs

317 |   rs.add_component close

318 |   rs.newline

319 | (.add_type) rs start close TNotInline xs = T1.do

320 |   rs.newline

321 |   rs.add_component start

322 |   rs.newline

323 |   rs.indent $

324 |     traverse1_ (renderElement rs) xs

325 |   rs.newline

326 |   rs.add_component close

327 |   rs.newline

329 | renderElement rs (Raw contents) = rs.add_component contents

330 | renderElement rs (Collection xs) = traverse1_ (renderElement rs) xs

331 | renderElement rs (Void tag) =

332 |   let str = "<\{tag} />"

333 |   in case tagType tag of

334 |     TInline => rs.add_component str

335 |     _ => T1.do

336 |       rs.newline

337 |       rs.add_component str

338 |       rs.newline

339 | renderElement rs (VoidAttrs tag attrs) =

340 |   let str = "<\{tag} \{attrsToString attrs} />"

341 |   in case tagType tag of

342 |     TInline => rs.add_component str

343 |     _ => T1.do

344 |       rs.newline

345 |       rs.add_component str

346 |       rs.newline

347 | renderElement rs (Normal tag contents) =

348 |   let start = "<\{tag}>"

349 |       close = "</\{tag}>"

350 |   in rs.add_type start close (tagType tag) contents

351 | renderElement rs (NormalAttrs tag attrs contents) =

352 |   let start = "<\{tag} \{attrsToString attrs}>"

353 |       close = "</\{tag}>"

354 |   in rs.add_type start close (tagType tag) contents

357 | render : Element -> String

358 | render x = run1 $ T1.do

359 |   rs <- initial

360 |   renderElement rs x

361 |   read1 rs.buffer

368 | article : List Element -> Element

369 | article = Normal "article"

372 | header : List Element -> Element

373 | header = Normal "header"

376 | body : List Element -> Element

377 | body = Normal "body"

380 | head : List Element -> Element

381 | head = Normal "head"

384 | h : Nat -> List Element -> Element

385 | h k xs = Normal "h\{k}" xs

388 | stylesheet : String -> Element

389 | stylesheet path =

390 |   VoidAttrs "link" [("rel", ["stylesheet"]), ("type", ["text/css"]), ("href", [path])]

393 | document : List Element -> String

394 | document xs = "<!DOCTYPE html>\n" ++ render (NormalAttrs "html" [("lang", ["en"])] xs)

397 | walkTree : (f : Element -> Maybe Element) -> Element -> Element

398 | walkTree f x =

399 |   -- Try applying to this node first

400 |   let x' = maybe x id $ f x

401 |   -- Then recurse

402 |   in case x' of

403 |     Collection xs => Collection (map (walkTree f) xs)

404 |     Normal tag contents => Normal tag (map (walkTree f) contents)

405 |     NormalAttrs tag attrs contents => NormalAttrs tag attrs (map (walkTree f) contents)

406 |     _ => x'

408 | unwrapParagraph : Element -> Maybe Element

409 | unwrapParagraph (Normal "p" contents) = Just $ Collection contents

410 | unwrapParagraph (NormalAttrs "p" attrs contents) = Just $ Collection contents

411 | unwrapParagraph _ = Nothing

414 | filterTree : (f : Element -> Bool) -> Element -> Maybe Element

415 | filterTree f x =

416 |   if f x

417 |   then case x of

418 |     Collection xs =>

419 |       let xs' = catMaybes $ map (filterTree f) xs

420 |       in if isNil xs' then Nothing else Just (Collection xs')

421 |     Normal tag contents =>

422 |       let contents' = catMaybes $ map (filterTree f) contents

423 |       in if isNil contents' then Nothing else Just (Normal tag contents')

424 |     NormalAttrs tag attrs contents =>

425 |       let contents' = catMaybes $ map (filterTree f) contents

426 |       in if isNil contents' then Nothing else Just (NormalAttrs tag attrs contents')

427 |     x => Just x

428 |   else Nothing

430 | lookupAttr : String -> List Attr -> Maybe String

431 | lookupAttr str [] = Nothing

432 | lookupAttr str ((x, ys) :: xs) =

433 |   if str == x

434 |     then Just $ joinBy " " ys

435 |     else lookupAttr str xs

437 | replaceAttr : (key, value : String) -> List Attr -> List Attr

438 | replaceAttr key value [] = []

439 | replaceAttr key value ((x, ys) :: xs) =

440 |   if key == x

441 |     then (x, [value]) :: xs

442 |     else (x, ys) :: replaceAttr key value xs

445 | processLinks : (fn : String -> Either err String) -> Element -> Either err Element

446 | processLinks fn (Collection xs) = do

447 |   xs <- traverse (processLinks fn) xs

448 |   pure $ Collection xs

449 | processLinks fn (Normal tag contents) = do

450 |   contents <- traverse (processLinks fn) contents

451 |   pure $ Normal tag contents

452 | processLinks fn (NormalAttrs "a" attrs contents) =

453 |   case lookupAttr "href" attrs of

454 |     Nothing => do

455 |       contents <- traverse (processLinks fn) contents

456 |       pure $ NormalAttrs "a" attrs contents

457 |     Just x => do

458 |       x' <- fn x

459 |       let attrs' = replaceAttr "href" x' attrs

460 |       pure $ NormalAttrs "a" attrs' contents

461 | processLinks fn (NormalAttrs tag attrs contents) = do

462 |   contents <- traverse (processLinks fn) contents

463 |   pure $ NormalAttrs tag attrs contents

464 | processLinks fn e = Right e

470 | namespace Inline

471 |   export

472 |   toHtml' : Ref s State -> Inline -> F1 s Element

473 |   toHtml' state = mapF1 combineRaws . inlineToHtml state

475 |   export

476 |   toHtml : Inline -> Element

477 |   toHtml x = run1 $ T1.do

478 |     state : Ref _ State <- ref1 empty

479 |     toHtml' state x

481 | namespace Block

482 |   export

483 |   toHtml' : Ref s State -> Block -> F1 s Element

484 |   toHtml' state = mapF1 combineRaws . blockToHtml state

486 |   export

487 |   toHtml : List Block -> (List Element, Element)

488 |   toHtml xs = run1 $ T1.do

489 |     state : Ref _ State <- ref1 empty

490 |     output <- traverse1 (toHtml' state) xs

491 |     footnotes <- mapF1 (toList . footnotes) $ read1 state

492 |     let section =

493 |          NormalAttrs "section" [("id", ["footnotes"]), ("class", ["footnotes"])]

494 |                      [ h 3 [Raw "Footnotes"]

495 |                      , Normal "ol" footnotes

496 |                      ]

497 |     pure (output, combineRaws . walkTree unwrapParagraph $ section)