Add Pandoc mode

CONTRIBUTORS

@@ -1,3 +1,4 @@
 Ohad Kammar
 Guillaume Allais
 Jan de Muijnck-Hughes
+Robert Wright

Makefile

@@ -5,8 +5,12 @@ project:build/exec/katla
 build/exec/katla: .PHONY
 	idris2 --build katla.ipkg
 
-install: build/exec/katla
+build/exec/katla-pandoc: .PHONY
+	idris2 --build katla-pandoc.ipkg
+
+install: build/exec/katla build/exec/katla-pandoc
 	idris2 --install katla.ipkg
+	idris2 --install katla-pandoc.ipkg
 	cp -R build/exec/* ~/.idris2/bin/
 
 test: .PHONY

katla-pandoc.ipkg

@@ -0,0 +1,13 @@
+package katla-pandoc
+
+authors = "Robert Wright"
+
+depends = contrib
+
+modules
+  = Katla.Pandoc
+
+main = Katla.Pandoc
+
+executable = katla-pandoc
+sourcedir = "src"

src/Katla/Pandoc.idr

@@ -0,0 +1,253 @@
+module Katla.Pandoc
+
+import Control.Monad.State
+
+import Data.SortedMap
+import Data.SortedSet
+import Data.String
+
+import Language.JSON
+import System
+import System.Directory
+import System.Random
+
+%default total
+
+updateJSON : String -> (JSON -> JSON) -> JSON -> JSON
+updateJSON key f json = update (\case Nothing => Just (f JNull); Just x => Just (f x)) key json
+
+findAttr : (key : String) ->
+           (default_ : String) ->
+           List JSON ->
+           String
+findAttr key default_ [] = default_
+findAttr key default_ (JArray [JString k, JString v] :: attrs) =
+    if k == key
+        then v
+        else findAttr key default_ attrs
+findAttr key default_ (_ :: attrs) = findAttr key default_ attrs
+
+findPackages : JSON -> List String
+findPackages doc = do
+    let Just (JArray packages) = lookup "meta" doc >>= lookup "idris2-packages" >>= lookup "c"
+        | _ => []
+    JObject [("t", JString "MetaInlines"), ("c", JArray [JObject [("t", JString "Str"), ("c", JString package)]])] <- packages
+        | _ => []
+    pure package
+
+data DisplayType = Block | Inline
+
+data CodeType = Decls | Expr String
+
+record Snippet where
+    constructor MkSnippet
+    code : String
+    displayType : DisplayType
+    codeType : CodeType
+    hide : Bool
+    file : String
+    namespace_ : String
+
+parseSnippet : JSON -> Maybe Snippet
+parseSnippet (JObject [
+    ("t", JString t),
+    ("c", JArray [JArray [_, JArray (JString "idr" :: clss), JArray attrs], JString code])
+  ]) = do
+    displayType <- case t of
+        "CodeBlock" => pure Block
+        "Code" => pure Inline
+        _ => Nothing
+
+    let codeType = do
+        let exprType = findAttr "type" "?" attrs
+        if elem (JString "decls") clss || elem (JString "decl") clss
+            then Decls
+            else if elem (JString "expr") clss || exprType /= "?"
+              then Expr exprType
+              else case displayType of
+                  Block => Decls
+                  Inline => Expr exprType
+
+    pure $ MkSnippet
+        code
+        displayType
+        codeType
+        (elem (JString "hide") clss)
+        (findAttr "file" "Main" attrs)
+        (findAttr "namespace" "" attrs)
+parseSnippet json = Nothing
+
+traverseSnippets : Monad m => (Snippet -> m JSON) -> JSON -> m JSON
+traverseSnippets f json = traverseJSON (\x => maybe (pure x) f (parseSnippet x)) json
+
+traverseSnippets_ : Monad m => (Snippet -> m ()) -> JSON -> m ()
+traverseSnippets_ f json = traverseJSON_ (\x => maybe (pure ()) f (parseSnippet x)) json
+
+collateCode : JSON -> SnocList Snippet
+collateCode doc = execState [<] $ traverseSnippets_ (\snippet => modify (:< snippet)) doc
+
+covering
+writeCode : (dir : String) ->
+            (snippets : List Snippet) ->
+            IO (List (Nat, Nat))
+writeCode dir snippets = do
+    (files, ranges) <- runStateT SortedMap.empty $ traverse (\snippet => do
+        let fileName = "\{dir}/\{snippet.file}.idr"
+
+        let indentDepth = 0
+
+        indentDepth <- if snippet.namespace_ /= ""
+            then do
+                ignore $ writeBlock fileName indentDepth "namespace \{snippet.namespace_}"
+                pure $ 1 + indentDepth
+            else pure indentDepth
+
+        indentDepth <- case snippet.codeType of
+            Decls => pure indentDepth
+            Expr exprType => do
+                let varName = "x\{show $ cast {to = Bits32} !(randomIO {a = Int32})}"
+                ignore $ writeBlock fileName indentDepth "\{varName} : \{exprType}\n\{varName} ="
+                pure $ 1 + indentDepth
+
+        writeBlock fileName indentDepth snippet.code
+      ) snippets
+    traverse_ (\(file, _) => closeFile file) files
+    pure ranges
+  where
+    indent : Nat -> List String -> List String
+    indent indentDepth block = do
+        let indentPrefix = replicate (4 * indentDepth) ' '
+        map (\case "" => ""; line => indentPrefix ++ line) block
+
+    getFile : String -> StateT (SortedMap String (File, Nat)) IO (File, Nat)
+    getFile fileName = do
+        files <- get
+        let Nothing = lookup fileName files
+            | Just file => pure file
+
+        Right file <- openFile fileName WriteTruncate
+            | Left fileError => die "Error writing Idris code to file: \{show fileError}"
+
+        modify $ insert fileName (file, 1)
+        pure (file, 1)
+
+    writeBlock : (fileName : String) ->
+                 (indentDepth : Nat) ->
+                 (block : String) ->
+                 StateT (SortedMap String (File, Nat)) IO (Nat, Nat)
+    writeBlock fileName indentDepth block = do
+        let ls = indent indentDepth $ lines block
+        let lineCount = length ls
+        (file, start) <- getFile fileName
+
+        -- Round trip of `unlines . lines` not identiy
+        -- This might introduce a new trailing newline
+        -- Trailing newline important for consistency of line counting
+        Right () <- fPutStrLn file $ unlines ls
+            | Left fileError => die "Error writing Idris code to file: \{show fileError}"
+
+        modify $ updateExisting (mapSnd (1 + lineCount +)) fileName
+        pure (start, minus lineCount 1)
+
+covering
+checkCode : (dir : String) ->
+            (packages : List String) ->
+            (snippets : List Snippet) ->
+            IO ()
+checkCode dir packages snippets = do
+    let fileNames = SortedSet.fromList $ map file snippets
+    for_ fileNames $ \fileName => do
+        (_, 0) <- run $ ["idris2", "-c", "\{dir}/\{fileName}.idr"] ++ (packages >>= (\package => ["-p", package]))
+            | (msg, err) => die $ "Error checking Idris code (exit code: \{show err})\n" ++ msg
+        pure ()
+
+covering
+addKatlaHeader : JSON -> IO JSON
+addKatlaHeader doc = do
+    (katlaHeader, 0) <- run "katla latex preamble"
+        | (_, err) => die "Error getting Katla header (exit code: \{show err})"
+
+    let pandocKatlaHeader = JObject [
+        ("t", JString "MetaBlocks"),
+        ("c", JArray [JObject [
+            ("t", JString "RawBlock"),
+            ("c", JArray [JString "tex", JString katlaHeader])
+        ]])
+    ]
+
+    pure $ update (Just . update (Just . update (Just . (\case
+          JArray xs => JArray $ pandocKatlaHeader :: xs
+          json => json) .
+          maybe (JArray []) id) "c" .
+          maybe (JObject [("t", JString "MetaList")]) id) "header-includes" .
+          maybe (JObject []) id) "meta" doc
+
+covering
+formatSnippet : (dir : String) -> Snippet -> (start : Nat) -> (len : Nat) -> IO JSON
+formatSnippet dir snippet start len = do
+    let False = snippet.hide
+        | True => pure $ JObject [("t", JString "Para"), ("c", JArray [])]
+
+    let katlaCmd = case snippet.displayType of
+          Block => "katla latex macro KatlaSnippet \{dir}/\{snippet.file}.idr build/ttc/*/\{dir}/\{snippet.file}.ttm \{show start} 0 \{show len}"
+          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}"
+    (out, 0) <- run katlaCmd
+        | (_, err) => die "Error running Katla (exit code: \{show err})"
+
+    let out = if snippet.namespace_ /= "" then dedent out else out
+    let out = case snippet.codeType of
+          Decls => out
+          Expr _ => dedent out
+
+    pure $ JObject [
+        ("t", JString $ case snippet.displayType of Block => "RawBlock"; Inline => "RawInline"),
+        ("c", JArray [
+            JString "tex",
+            JString $ "\\let\\KatlaSnippet\\relax{}" ++ out ++ "\\KatlaSnippet{}"
+        ])
+    ]
+  where
+    katlaIndent : String
+    katlaIndent = "\\KatlaSpace{}\\KatlaSpace{}\\KatlaSpace{}\\KatlaSpace{}"
+
+    katlaIndentLen : Nat
+    katlaIndentLen = length katlaIndent
+
+    dedent : String -> String
+    dedent block = unlines $
+        map (\line => if isPrefixOf katlaIndent line
+            then substr katlaIndentLen (minus (length line) katlaIndentLen) line
+            else line
+        ) $
+        lines block
+
+covering
+addKatlaSnippets : (dir : String) -> List Snippet -> List (Nat, Nat) -> JSON -> IO JSON
+addKatlaSnippets dir snippets ranges json = do
+    evalStateT ranges $ traverseSnippets (\snippet => do
+        Just (start, len) <- gets head'
+            | Nothing => die "katla-pandoc internal error"
+        modify (\case [] => []; _ :: xs => xs)
+        lift $ formatSnippet dir snippet start len
+      ) json
+
+covering
+main : IO ()
+main = do
+    doc <- getLine
+    let Just doc = parse doc
+        | Nothing => pure ()
+
+    let snippets = cast $ collateCode doc
+    let packages = findPackages doc
+
+    let dir = "build/katla"
+    ignore $ createDir "build"
+    ignore $ createDir dir
+
+    ranges <- writeCode dir snippets
+    checkCode dir packages snippets
+    doc <- addKatlaHeader doc
+    doc <- addKatlaSnippets dir snippets ranges doc
+
+    printLn doc

tests/Main.idr

@@ -14,6 +14,7 @@ tests = MkTestPool "Examples using Katla" [] Nothing
   , "init"
   , "markdown"
   , "literate"
+  , "pandoc"
   ]
 
 main : IO ()

tests/examples/pandoc/Source.md

@@ -0,0 +1,89 @@
+---
+title: Writing an Idris2 PDF file with katla-pandoc
+idris2-packages:
+  - contrib
+colorlinks: true # Workaround for conflict between Katla and pandoc default latex template
+---
+
+Using [katla](https://github.com/idris-community/katla)'s pandoc backend we can produce PDF documents containing semantically highlighted Idris2 code.
+
+The file you are currently reading is the rendered version of a literate markdown/idris2 file. It is called `Source.md` and contains fenced `idr` blocks.
+
+# Basic Usage
+
+We can hide uninteresting code blocks by adding the `hide` attribute. We hide an import of `Data.Vect` here. We won't see anything in the output PDF.
+
+```{.idr .hide}
+import Data.Vect
+```
+
+We can use all Idris 2 features. Here's an example code block:
+
+```idr
+x : Nat
+x = 1 + 2
+```
+
+We can use namespaces by adding the `namespace` attribute, such as to provide alternate definitions for functions. Consider this function signature:
+
+```{.idr namespace="A"}
+f : Vect n a -> Vect (n + n) a
+```
+
+Here's one implementation for `f`{.idr namespace="A" type="Vect 1 Nat -> ?"}:
+
+```{.idr namespace="A"}
+f xs = xs ++ xs
+```
+
+By repeating the signature in a different namespace, in a hidden code block, I can give an alternate definition:
+
+```{.idr .hide namespace="B"}
+f : Vect n a -> Vect (n + n) a
+```
+
+```{.idr namespace="B"}
+f xs = xs ++ reverse xs
+```
+
+# Inline Code
+
+As well as block code, we can have inline code, like `the Nat 3`{.idr}. Here's another: `1 + 2`{.idr}. We can also call the function we previously defined: `f [1, 2, 3]`{.idr namespace="A"}.
+
+By default, a code block is interpreted as top-level Idris 2 declarations, while inline code is interpreted as an expression. But we can switch it up if we wish.
+
+By using the `decls` class, we can write an inline declaration: `g : Nat -> Nat`{.idr .decls}.
+
+By using the `expr` class, we can write a block expression:
+
+```{.idr .expr type="List Nat"}
+[
+    1,
+    2,
+    3
+]
+```
+
+# Types
+
+Sometimes, Idris 2 cannot infer the type of an expression. Is `[1, 2, 3]`{.idr type="List Nat"} a `List Nat`{.idr}, or a `Vect 3 Integer`{.idr}? We can use the `type` attribute to tell Idris 2 which one it should be.
+
+# Multiple Files
+
+If you need an import to *not* be available, namespaces are not enough. We can use the `file` attribute to put snippets in separate files. For example, the signature of `f`{.idr namespace="A" type="Vect 1 Nat -> ?"} fails to compile if we use a new file, that hasn't imported `Vect`{.idr}.
+
+```{.idr file="Another"}
+failing "Undefined name Vect."
+    f : Vect n a -> Vect (n + n) a
+```
+
+# Packages
+
+We can add Idris 2 packages to the YAML metadata of the Markdown file, using the `idris2-packages` key. For example, adding `contrib` allows us to use the `Language.JSON` module.
+
+```{.idr file="Package"}
+import Language.JSON
+
+x : Maybe JSON
+x = parse #"{"x": 1, "y": 2}"#
+```

tests/examples/pandoc/run

@@ -0,0 +1,8 @@
+rm -rf temp build
+
+mkdir temp
+
+# Test Katla pandoc
+pandoc ./Source.md --filter "$1-pandoc" -o temp/source.tex
+pandoc ./Source.md --filter "$1-pandoc" -o temp/source.pdf
+diff source-expected.tex temp/source.tex >> output