Add support for Literate Juvix Markdown (#2448)

This PR adds an initial support for Literate Juvix Markdown files, files
with the extension `.juvix.md`.

Here is a small example of such a file: `Test.juvix.md`.

<pre>
# This is a heading
Lorem ...

```juvix
module Test;

type A := a;

fun : A -> A 
 | _ := a;
```
Other text
</pre>


This initial support enables users to execute common commands such as
typechecking, compilation, and HTML generation. Additionally, a new
command called `markdown` has been introduced. This command replaces
code blocks marked with the juvix attribute with their respective HTML
output, much like the output we obtain when running `juvix html`. In
this version, comments are ignored in the output, including judoc
blocks.

- We intend to use this new feature in combination with this Python
plugin (https://github.com/anoma/juvix-mkdocs) to enhance our
documentation site.



https://github.com/anoma/juvix/assets/1428088/a0c17f36-3d76-42cc-a571-91f885866874


## Future work

Open as issues once this PR is merged, we can work on the following:

- Support imports of Juvix Markdown modules (update the path resolver to
support imports of Literate Markdown files)
- Support (Judoc) comments in md Juvix blocks
- Support Markdown in Judoc blocks
- Update Text editor support, vscode extension and emacs mode (the
highlighting info is a few characters off in the current state)



- Closes #1839 
- Closes #1719

.gitignore

@@ -90,3 +90,4 @@ hie.yaml
 /.shake/
 /.benchmark-results/
 docs/assets/**
+.repos

app/Commands/Compile/Options.hs

@@ -15,4 +15,4 @@ parseMainCompileOptions :: Parser CompileOptions
 parseMainCompileOptions =
   parseCompileOptions
     supportedTargets
-    (parseInputFile FileExtJuvix)
+    (parseInputFiles (NonEmpty.fromList [FileExtJuvix, FileExtJuvixMarkdown]))

app/Commands/Eval/Options.hs

@@ -1,6 +1,7 @@
 module Commands.Eval.Options where
 
 import CommonOptions
+import Data.List.NonEmpty qualified as NonEmpty
 import Evaluator qualified as Eval
 import Juvix.Compiler.Core.Pretty.Options qualified as Core
 
@@ -29,7 +30,7 @@ instance CanonicalProjection EvalOptions Eval.EvalOptions where
 
 parseEvalOptions :: Parser EvalOptions
 parseEvalOptions = do
-  _evalInputFile <- parseInputFile FileExtJuvix
+  _evalInputFile <- parseInputFiles (NonEmpty.fromList [FileExtJuvix, FileExtJuvixMarkdown])
   _evalSymbolName <-
     optional $
       strOption

app/Commands/Html/Options.hs

@@ -1,6 +1,7 @@
 module Commands.Html.Options where
 
 import CommonOptions
+import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Backend.Html.Data.Options hiding (HtmlOptions)
 
 data HtmlOptions = HtmlOptions
@@ -91,7 +92,7 @@ parseHtml = do
       ( long "open"
           <> help "Open the documentation after generating it"
       )
-  _htmlInputFile <- parseInputFile FileExtJuvix
+  _htmlInputFile <- parseInputFiles (NonEmpty.fromList [FileExtJuvix, FileExtJuvixMarkdown])
   pure HtmlOptions {..}
   where
     allThemes :: [Theme]

app/Commands/Markdown.hs

@@ -0,0 +1,54 @@
+module Commands.Markdown where
+
+import Commands.Base
+import Commands.Markdown.Options
+import Data.Text.IO qualified as Text
+import Juvix.Compiler.Backend.Markdown.Translation.FromTyped.Source
+import Juvix.Compiler.Backend.Markdown.Translation.FromTyped.Source qualified as MK
+import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
+import Juvix.Compiler.Concrete.Language qualified as Concrete
+import Juvix.Compiler.Concrete.Pretty qualified as Concrete
+import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
+import Juvix.Extra.Assets (writeAssets)
+
+runCommand ::
+  (Members '[Embed IO, App] r) =>
+  MarkdownOptions ->
+  Sem r ()
+runCommand opts = do
+  let inputFile = opts ^. markdownInputFile
+  scopedM <- runPipeline inputFile upToScoping
+  let m = head (scopedM ^. Scoper.resultModules)
+  outputDir <- fromAppPathDir (opts ^. markdownOutputDir)
+  md :: Text <-
+    MK.fromJuvixMarkdown
+      ProcessJuvixBlocksArgs
+        { _processJuvixBlocksArgsConcreteOpts = Concrete.defaultOptions,
+          _processJuvixBlocksArgsUrlPrefix = opts ^. markdownUrlPrefix,
+          _processJuvixBlocksArgsIdPrefix =
+            opts ^. markdownIdPrefix,
+          _processJuvixBlocksArgsNoPath =
+            opts ^. markdownNoPath,
+          _processJuvixBlocksArgsComments = scopedM ^. Scoper.comments,
+          _processJuvixBlocksArgsModule = m,
+          _processJuvixBlocksArgsOutputDir = outputDir
+        }
+  if
+      | opts ^. markdownStdout -> liftIO . putStrLn $ md
+      | otherwise -> do
+          ensureDir outputDir
+          when (opts ^. markdownWriteAssets) $
+            liftIO $
+              writeAssets outputDir
+
+          let mdFile :: Path Rel File
+              mdFile =
+                relFile
+                  ( Concrete.topModulePathToDottedPath
+                      (m ^. Concrete.modulePath . S.nameConcrete)
+                      <.> markdownFileExt
+                  )
+              absPath :: Path Abs File
+              absPath = outputDir <//> mdFile
+
+          liftIO $ Text.writeFile (toFilePath absPath) md

app/Commands/Markdown/Options.hs

@@ -0,0 +1,56 @@
+module Commands.Markdown.Options where
+
+import CommonOptions
+
+data MarkdownOptions = MarkdownOptions
+  { _markdownInputFile :: AppPath File,
+    _markdownOutputDir :: AppPath Dir,
+    _markdownUrlPrefix :: Text,
+    _markdownIdPrefix :: Text,
+    _markdownNoPath :: Bool,
+    _markdownStdout :: Bool,
+    _markdownWriteAssets :: Bool
+  }
+  deriving stock (Data)
+
+makeLenses ''MarkdownOptions
+
+parseJuvixMarkdown :: Parser MarkdownOptions
+parseJuvixMarkdown = do
+  _markdownUrlPrefix :: Text <-
+    strOption
+      ( value mempty
+          <> long "prefix-url"
+          <> help "Prefix used for inner Juvix hyperlinks"
+      )
+  _markdownIdPrefix :: Text <-
+    strOption
+      ( value mempty
+          <> long "prefix-id"
+          <> showDefault
+          <> help "Prefix used for HTML element IDs"
+      )
+  _markdownInputFile <- parseInputFile FileExtJuvixMarkdown
+  _markdownOutputDir <-
+    parseGenericOutputDir
+      ( value "markdown"
+          <> showDefault
+          <> help "Markdown output directory"
+          <> action "directory"
+      )
+  _markdownNoPath <-
+    switch
+      ( long "no-path"
+          <> help "Do not include the path to the input file in the HTML id hyperlinks"
+      )
+  _markdownWriteAssets <-
+    switch
+      ( long "write-assets"
+          <> help "Write the CSS/JS assets to the output directory"
+      )
+  _markdownStdout <-
+    switch
+      ( long "stdout"
+          <> help "Write the output to stdout instead of a file"
+      )
+  pure MarkdownOptions {..}

app/Commands/Typecheck/Options.hs

@@ -2,6 +2,7 @@ module Commands.Typecheck.Options where
 
 import Commands.Dev.Internal.Typecheck.Options qualified as Internal
 import CommonOptions
+import Data.List.NonEmpty qualified as NonEmpty
 
 newtype TypecheckOptions = TypecheckOptions
   { _typecheckInputFile :: AppPath File
@@ -12,7 +13,7 @@ makeLenses ''TypecheckOptions
 
 parseTypecheck :: Parser TypecheckOptions
 parseTypecheck = do
-  _typecheckInputFile <- parseInputFile FileExtJuvix
+  _typecheckInputFile <- parseInputFiles (NonEmpty.fromList [FileExtJuvix, FileExtJuvixMarkdown])
   pure TypecheckOptions {..}
 
 instance CanonicalProjection TypecheckOptions Internal.InternalTypeOptions where

app/TopCommand.hs

@@ -10,6 +10,7 @@ import Commands.Eval qualified as Eval
 import Commands.Format qualified as Format
 import Commands.Html qualified as Html
 import Commands.Init qualified as Init
+import Commands.Markdown qualified as Markdown
 import Commands.Repl qualified as Repl
 import Commands.Typecheck qualified as Typecheck
 import Juvix.Extra.Version
@@ -37,6 +38,7 @@ runTopCommand = \case
   Clean opts -> runFilesIO (Clean.runCommand opts)
   Eval opts -> Eval.runCommand opts
   Html opts -> Html.runCommand opts
+  Markdown opts -> Markdown.runCommand opts
   JuvixRepl opts -> Repl.runCommand opts
   JuvixFormat opts -> runFilesIO (Format.runCommand opts)
   Dependencies opts -> Dependencies.runCommand opts

app/TopCommand/Options.hs

@@ -9,6 +9,7 @@ import Commands.Eval.Options
 import Commands.Format.Options
 import Commands.Html.Options
 import Commands.Init.Options
+import Commands.Markdown.Options
 import Commands.Repl.Options
 import Commands.Typecheck.Options
 import CommonOptions hiding (Doc)
@@ -25,6 +26,7 @@ data TopCommand
   | Clean CleanOptions
   | Eval EvalOptions
   | Html HtmlOptions
+  | Markdown MarkdownOptions
   | Dev Dev.DevCommand
   | Doctor DoctorOptions
   | Init InitOptions
@@ -188,6 +190,13 @@ commandHtml =
       (Html <$> parseHtml)
       (progDesc "Generate HTML for a Juvix file")
 
+commandMarkdown :: Mod CommandFields TopCommand
+commandMarkdown =
+  command "markdown" $
+    info
+      (Markdown <$> parseJuvixMarkdown)
+      (progDesc "Translate Juvix code blocks in a Markdown file to Markdown")
+
 commandDev :: Mod CommandFields TopCommand
 commandDev =
   command "dev" $
@@ -204,7 +213,8 @@ parseCompilerCommand =
           commandCheck,
           commandCompile,
           commandEval,
-          commandHtml
+          commandHtml,
+          commandMarkdown
         ]
     )
 

package.yaml

@@ -60,6 +60,8 @@ dependencies:
   - language-c == 0.9.*
   - libyaml == 0.1.*
   - megaparsec == 9.3.*
+  - commonmark == 0.2.*
+  - parsec == 3.1.*
   - microlens-platform == 0.4.*
   - parser-combinators == 1.3.*
   - path == 0.9.*

src/Juvix/Compiler/Backend/Html/Data/Options.hs

@@ -16,6 +16,21 @@ data HtmlOptions = HtmlOptions
     _htmlOptionsNoFooter :: Bool
   }
 
+defaultHtmlOptions :: HtmlOptions
+defaultHtmlOptions =
+  HtmlOptions
+    { _htmlOptionsKind = HtmlDoc,
+      _htmlOptionsAssetsPrefix = "",
+      _htmlOptionsUrlPrefix = "",
+      _htmlOptionsIdPrefix = "",
+      _htmlOptionsOnlyCode = False,
+      _htmlOptionsNoPath = False,
+      _htmlOptionsOutputDir = $(mkAbsDir "/tmp"),
+      _htmlOptionsParamBase = "",
+      _htmlOptionsTheme = Nord,
+      _htmlOptionsNoFooter = False
+    }
+
 data Theme
   = Nord
   | Ayu

src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs

@@ -292,6 +292,18 @@ juColor = Attr.class_ . toStr
       JuVar -> "ju-var"
       JuNumber -> "ju-number"
 
+juKindColor :: S.NameKind -> CssColor
+juKindColor = \case
+  S.KNameConstructor -> JuConstructor
+  S.KNameInductive -> JuInductive
+  S.KNameFunction -> JuFunction
+  S.KNameLocal -> JuVar
+  S.KNameAxiom -> JuAxiom
+  S.KNameLocalModule -> JuVar
+  S.KNameAlias -> JuVar
+  S.KNameTopModule -> JuVar
+  S.KNameFixity -> JuFixity
+
 putTag :: forall r. (Members '[Reader HtmlOptions] r) => Ann -> Html -> Sem r Html
 putTag ann x = case ann of
   AnnKind k -> return (tagKind k x)
@@ -330,18 +342,7 @@ putTag ann x = case ann of
 
     tagKind k =
       Html.span
-        ! juColor
-          ( case k of
-              S.KNameConstructor -> JuConstructor
-              S.KNameInductive -> JuInductive
-              S.KNameFunction -> JuFunction
-              S.KNameLocal -> JuVar
-              S.KNameAxiom -> JuAxiom
-              S.KNameLocalModule -> JuVar
-              S.KNameAlias -> JuVar
-              S.KNameTopModule -> JuVar
-              S.KNameFixity -> JuFixity
-          )
+        ! juColor (juKindColor k)
 
 nameIdAttr :: (Members '[Reader HtmlOptions] r) => S.NameId -> Sem r AttributeValue
 nameIdAttr (S.NameId k) = do