0 | module Katla.Pandoc

  2 | import Control.Monad.State

  4 | import Data.SortedMap

  5 | import Data.SortedSet

  6 | import Data.String

  8 | import Language.JSON

  9 | import System

 10 | import System.Directory

 11 | import System.Random

 13 | %default total

 15 | updateJSON : String -> (JSON -> JSON) -> JSON -> JSON

 16 | updateJSON key f json = update (\case Nothing => Just (f JNull); Just x => Just (f x)) key json

 18 | findAttr : (key : String) ->

 19 |            (default_ : String) ->

 20 |            List JSON ->

 21 |            String

 22 | findAttr key default_ [] = default_

 23 | findAttr key default_ (JArray [JString k, JString v] :: attrs) =

 24 |     if k == key

 25 |         then v

 26 |         else findAttr key default_ attrs

 27 | findAttr key default_ (_ :: attrs) = findAttr key default_ attrs

 29 | findPackages : JSON -> List String

 30 | findPackages doc = do

 31 |     let Just (JArray packages) = lookup "meta" doc >>= lookup "idris2-packages" >>= lookup "c"

 32 |         | _ => []

 33 |     JObject [("t", JString "MetaInlines"), ("c", JArray [JObject [("t", JString "Str"), ("c", JString package)]])] <- packages

 34 |         | _ => []

 35 |     pure package

 37 | data DisplayType = Block | Inline

 39 | data CodeType = Decls | Expr String

 41 | record Snippet where

 42 |     constructor MkSnippet

 43 |     code : String

 44 |     displayType : DisplayType

 45 |     codeType : CodeType

 46 |     hide : Bool

 47 |     file : String

 48 |     namespace_ : String

 50 | parseSnippet : JSON -> Maybe Snippet

 51 | parseSnippet (JObject [

 52 |     ("t", JString t),

 53 |     ("c", JArray [JArray [_, JArray (JString "idr" :: clss), JArray attrs], JString code])

 54 |   ]) = do

 55 |     displayType <- case t of

 56 |         "CodeBlock" => pure Block

 57 |         "Code" => pure Inline

 58 |         _ => Nothing

 60 |     let codeType = do

 61 |         let exprType = findAttr "type" "?" attrs

 62 |         if elem (JString "decls") clss || elem (JString "decl") clss

 63 |             then Decls

 64 |             else if elem (JString "expr") clss || exprType /= "?"

 65 |               then Expr exprType

 66 |               else case displayType of

 67 |                   Block => Decls

 68 |                   Inline => Expr exprType

 70 |     pure $ MkSnippet

 71 |         code

 72 |         displayType

 73 |         codeType

 74 |         (elem (JString "hide") clss)

 75 |         (findAttr "file" "Main" attrs)

 76 |         (findAttr "namespace" "" attrs)

 77 | parseSnippet json = Nothing

 79 | traverseSnippets : Monad m => (Snippet -> m JSON) -> JSON -> m JSON

 80 | traverseSnippets f json = traverseJSON (\x => maybe (pure x) f (parseSnippet x)) json

 82 | traverseSnippets_ : Monad m => (Snippet -> m ()) -> JSON -> m ()

 83 | traverseSnippets_ f json = traverseJSON_ (\x => maybe (pure ()) f (parseSnippet x)) json

 85 | collateCode : JSON -> SnocList Snippet

 86 | collateCode doc = execState [<] $ traverseSnippets_ (\snippet => modify (:< snippet)) doc

 89 | writeCode : (dir : String) ->

 90 |             (snippets : List Snippet) ->

 91 |             IO (List (Nat, Nat))

 92 | writeCode dir snippets = do

 93 |     (files, ranges) <- runStateT SortedMap.empty $ traverse (\snippet => do

 94 |         let fileName = "\{dir}/\{snippet.file}.idr"

 96 |         let indentDepth = 0

 98 |         indentDepth <- if snippet.namespace_ /= ""

 99 |             then do

100 |                 ignore $ writeBlock fileName indentDepth "namespace \{snippet.namespace_}"

101 |                 pure $ 1 + indentDepth

102 |             else pure indentDepth

104 |         indentDepth <- case snippet.codeType of

105 |             Decls => pure indentDepth

106 |             Expr exprType => do

107 |                 let varName = "x\{show $ cast {to = Bits32} !(randomIO {a = Int32})}"

108 |                 ignore $ writeBlock fileName indentDepth "\{varName} : \{exprType}\n\{varName} ="

109 |                 pure $ 1 + indentDepth

111 |         writeBlock fileName indentDepth snippet.code

112 |       ) snippets

113 |     traverse_ (\(file, _) => closeFile file) files

114 |     pure ranges

115 |   where

116 |     indent : Nat -> List String -> List String

117 |     indent indentDepth block = do

118 |         let indentPrefix = replicate (4 * indentDepth) ' '

119 |         map (\case "" => ""; line => indentPrefix ++ line) block

121 |     getFile : String -> StateT (SortedMap String (File, Nat)) IO (File, Nat)

122 |     getFile fileName = do

123 |         files <- get

124 |         let Nothing = lookup fileName files

125 |             | Just file => pure file

127 |         Right file <- openFile fileName WriteTruncate

128 |             | Left fileError => die "Error writing Idris code to file: \{show fileError}"

130 |         modify $ insert fileName (file, 1)

131 |         pure (file, 1)

133 |     writeBlock : (fileName : String) ->

134 |                  (indentDepth : Nat) ->

135 |                  (block : String) ->

136 |                  StateT (SortedMap String (File, Nat)) IO (Nat, Nat)

137 |     writeBlock fileName indentDepth block = do

138 |         let ls = indent indentDepth $ lines block

139 |         let lineCount = length ls

140 |         (file, start) <- getFile fileName

142 |         -- Round trip of `unlines . lines` not identiy

143 |         -- This might introduce a new trailing newline

144 |         -- Trailing newline important for consistency of line counting

145 |         Right () <- fPutStrLn file $ unlines ls

146 |             | Left fileError => die "Error writing Idris code to file: \{show fileError}"

148 |         modify $ updateExisting (mapSnd (1 + lineCount +)) fileName

149 |         pure (start, minus lineCount 1)

152 | checkCode : (dir : String) ->

153 |             (packages : List String) ->

154 |             (snippets : List Snippet) ->

155 |             IO ()

156 | checkCode dir packages snippets = do

157 |     let fileNames = SortedSet.fromList $ map file snippets

158 |     for_ fileNames $ \fileName => do

159 |         (_, 0) <- run $ ["idris2", "-c", "\{dir}/\{fileName}.idr"] ++ (packages >>= (\package => ["-p", package]))

160 |             | (msg, err) => die $ "Error checking Idris code (exit code: \{show err})\n" ++ msg

161 |         pure ()

164 | addKatlaHeader : JSON -> IO JSON

165 | addKatlaHeader doc = do

166 |     (katlaHeader, 0) <- run "katla latex preamble"

167 |         | (_, err) => die "Error getting Katla header (exit code: \{show err})"

169 |     let pandocKatlaHeader = JObject [

170 |         ("t", JString "MetaBlocks"),

171 |         ("c", JArray [JObject [

172 |             ("t", JString "RawBlock"),

173 |             ("c", JArray [JString "tex", JString katlaHeader])

174 |         ]])

175 |     ]

177 |     pure $ update (Just . update (Just . update (Just . (\case

178 |           JArray xs => JArray $ pandocKatlaHeader :: xs

179 |           json => json) .

180 |           maybe (JArray []) id) "c" .

181 |           maybe (JObject [("t", JString "MetaList")]) id) "header-includes" .

182 |           maybe (JObject []) id) "meta" doc

185 | formatSnippet : (dir : String) -> Snippet -> (start : Nat) -> (len : Nat) -> IO JSON

186 | formatSnippet dir snippet start len = do

187 |     let False = snippet.hide

188 |         | True => pure $ JObject [("t", JString "Para"), ("c", JArray [])]

190 |     let katlaCmd = case snippet.displayType of

191 |           Block => "katla latex macro KatlaSnippet \{dir}/\{snippet.file}.idr build/ttc/*/\{dir}/\{snippet.file}.ttm \{show start} 0 \{show len}"

192 |           Inline => "katla latex macro inline KatlaSnippet \{dir}/\{snippet.file}.idr build/ttc/*/\{dir}/\{snippet.file}.ttm \{show start} 0 \{show $ 1 + len} \{show $ 8 + length snippet.code}"

193 |     (out, 0) <- run katlaCmd

194 |         | (_, err) => die "Error running Katla (exit code: \{show err})"

196 |     let out = if snippet.namespace_ /= "" then dedent out else out

197 |     let out = case snippet.codeType of

198 |           Decls => out

199 |           Expr _ => dedent out

201 |     pure $ JObject [

202 |         ("t", JString $ case snippet.displayType of Block => "RawBlock"; Inline => "RawInline"),

203 |         ("c", JArray [

204 |             JString "tex",

205 |             JString $ "\\let\\KatlaSnippet\\relax{}" ++ out ++ "\\KatlaSnippet{}"

206 |         ])

207 |     ]

208 |   where

209 |     katlaIndent : String

210 |     katlaIndent = "\\KatlaSpace{}\\KatlaSpace{}\\KatlaSpace{}\\KatlaSpace{}"

212 |     katlaIndentLen : Nat

213 |     katlaIndentLen = length katlaIndent

215 |     dedent : String -> String

216 |     dedent block = unlines $

217 |         map (\line => if isPrefixOf katlaIndent line

218 |             then substr katlaIndentLen (minus (length line) katlaIndentLen) line

219 |             else line

220 |         ) $

221 |         lines block

224 | addKatlaSnippets : (dir : String) -> List Snippet -> List (Nat, Nat) -> JSON -> IO JSON

225 | addKatlaSnippets dir snippets ranges json = do

226 |     evalStateT ranges $ traverseSnippets (\snippet => do

227 |         Just (start, len) <- gets head'

228 |             | Nothing => die "katla-pandoc internal error"

229 |         modify (\case [] => []; _ :: xs => xs)

230 |         lift $ formatSnippet dir snippet start len

231 |       ) json

234 | main : IO ()

235 | main = do

236 |     doc <- getLine

237 |     let Just doc = parse doc

238 |         | Nothing => pure ()

240 |     let snippets = cast $ collateCode doc

241 |     let packages = findPackages doc

243 |     let dir = "build/katla"

244 |     ignore $ createDir "build"

245 |     ignore $ createDir dir

247 |     ranges <- writeCode dir snippets

248 |     checkCode dir packages snippets

249 |     doc <- addKatlaHeader doc

250 |     doc <- addKatlaSnippets dir snippets ranges doc

252 |     printLn doc