Export Juvix source code to latex (#2917)

This pr adds two new commands related to latex.
1. `juvix dev latex getJuvixSty`. This command prints the contents of
the `juvix.sty` latex package to stdout. It has no options and the
expected usage is `juvix dev latex getJuvixSty > juvix.sty`.
2. `juvix dev latex export`. Expects a .juvix file as an argument and
outputs to stdout the highlighted module in latex format. Optional flags
`--from LINE`, `--to LINE` to output only the specified line range.
There is a `--mode` flag to choose how you want the output.
   ```
   • standalone: Output a ready to compile LaTeX file
   • wrap: Wrap the code in a Verbatim environment
   • raw: Output only the code (default: standalone)
   ```
4. As shown in the standalone output, one is allowed to choose the theme
when importing the juvix package like this: `\usepackage[theme =
latte]{juvix}`. Available themes are `latte`, `frappe`, `macchiato`,
`mocha`.

Examples:
To generate the following output I ran these commands:
```
cd examples/milestones/HelloWorld
mkdir latex
juvix dev latex getJuvixSty > latex/juvix.sty
juvix dev latex export HelloWorld.juvix > latex/main.tex
cd latex
xelatex main.tex
open main.pdf
```
1. with `\usepackage[theme = latte]{juvix}`:

![image](https://github.com/user-attachments/assets/200c212f-cc18-4dac-95fe-b3828346e7fa)
1. with `\usepackage[theme = frappe]{juvix}`:

![image](https://github.com/user-attachments/assets/a71d07aa-8adc-485c-a41d-3ea62dc2c5a3)
1. with `\usepackage[theme = macchiato]{juvix}`:

![image](https://github.com/user-attachments/assets/e7e878cf-3c2b-4497-a06c-0e8a445b5116)
1. with `\usepackage[theme = mocha]{juvix}`:

![image](https://github.com/user-attachments/assets/79a4c82c-c90e-4844-baf4-f107d8b8ae20)

app/App.hs

@@ -11,9 +11,6 @@ import Juvix.Compiler.Pipeline.Run
 import Juvix.Data.Error qualified as Error
 import Juvix.Extra.Paths.Base hiding (rootBuildDir)
 import Juvix.Parser.Error
-import Juvix.Prelude.Pretty hiding
-  ( Doc,
-  )
 import System.Console.ANSI qualified as Ansi
 
 data App :: Effect where

app/Commands/Compile/CStage.hs

@@ -3,7 +3,6 @@ module Commands.Compile.CStage where
 
 import CommonOptions
 import Juvix.Prelude as Juvix
-import Juvix.Prelude.Pretty
 import Prelude (show)
 
 data CStage

app/Commands/Dev.hs

@@ -13,6 +13,7 @@ import Commands.Dev.DisplayRoot qualified as DisplayRoot
 import Commands.Dev.Highlight qualified as Highlight
 import Commands.Dev.ImportTree qualified as ImportTree
 import Commands.Dev.Internal qualified as Internal
+import Commands.Dev.Latex qualified as Latex
 import Commands.Dev.MigrateJuvixYaml qualified as MigrateJuvixYaml
 import Commands.Dev.Nockma qualified as Nockma
 import Commands.Dev.Options
@@ -27,6 +28,7 @@ import Commands.Repl qualified as Repl
 runCommand :: (Members AppEffects r) => DevCommand -> Sem r ()
 runCommand = \case
   ImportTree opts -> ImportTree.runCommand opts
+  Latex opts -> Latex.runCommand opts
   Highlight opts -> Highlight.runCommand opts
   DevCompile opts -> DevCompile.runCommand opts
   Parse opts -> Parse.runCommand opts

app/Commands/Dev/Asm/Compile.hs

@@ -10,7 +10,6 @@ import Juvix.Compiler.Backend.C qualified as C
 import Juvix.Compiler.Casm.Data.Result qualified as Casm
 import Juvix.Compiler.Casm.Pretty qualified as Casm
 import Juvix.Compiler.Reg.Pretty qualified as Reg
-import Juvix.Prelude.Pretty
 
 runCommand :: forall r. (Members '[EmbedIO, App, TaggedLock] r) => AsmCompileOptions -> Sem r ()
 runCommand opts = do

app/Commands/Dev/Core/Compile/Base.hs

@@ -16,7 +16,6 @@ import Juvix.Compiler.Core.Data.Module qualified as Core
 import Juvix.Compiler.Core.Data.TransformationId qualified as Core
 import Juvix.Compiler.Reg.Pretty qualified as Reg
 import Juvix.Compiler.Tree.Pretty qualified as Tree
-import Juvix.Prelude.Pretty
 
 data PipelineArg = PipelineArg
   { _pipelineArgOptions :: CompileOptions,

app/Commands/Dev/Latex.hs

@@ -0,0 +1,11 @@
+module Commands.Dev.Latex where
+
+import Commands.Base
+import Commands.Dev.Latex.Export qualified as Export
+import Commands.Dev.Latex.GetJuvixSty qualified as GetJuvixSty
+import Commands.Dev.Latex.Options
+
+runCommand :: (Members AppEffects r) => LatexCommand -> Sem r ()
+runCommand = \case
+  Export m -> Export.runCommand m
+  GetJuvixSty m -> GetJuvixSty.runCommand m

app/Commands/Dev/Latex/Export.hs

@@ -0,0 +1,60 @@
+module Commands.Dev.Latex.Export
+  ( module Commands.Dev.Latex.Export,
+    module Commands.Dev.Latex.Export.Options,
+  )
+where
+
+import Commands.Base
+import Commands.Dev.Latex.Export.Options
+import Data.String.Interpolate (__i)
+import Data.Text qualified as Text
+import Juvix.Compiler.Backend.Latex.Translation.FromScoped.Source
+import Juvix.Compiler.Concrete.Language
+import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
+
+runCommand :: (Members AppEffects r) => ExportOptions -> Sem r ()
+runCommand ExportOptions {..} = do
+  res :: Scoper.ScoperResult <- silenceProgressLog (runPipelineNoOptions (Just _exportInputFile) upToScopingEntry)
+  let m :: Module 'Scoped 'ModuleTop = res ^. Scoper.resultModule
+      c :: Maybe Comments = guard (not _exportNoComments) $> Scoper.getScoperResultComments res
+      ltx :: Text =
+        Text.unlines
+          . sublist (pred <$> _exportFromLine) (pred <$> _exportToLine)
+          . Text.lines
+          $ moduleToLatex c m
+  renderStdOutLn $
+    case _exportMode of
+      ExportStandalone -> standalone ltx
+      ExportRaw -> ltx
+      ExportWrap -> verb ltx
+
+verb :: Text -> Text
+verb code =
+  [__i|
+  \\begin{tcolorbox}[colback=ju-base, colframe=ju-crust]
+  \\begin{Verbatim}[commandchars=\\\\\\{\\}]
+  #{code}
+  \\end{Verbatim}
+  \\end{tcolorbox}
+  |]
+
+standalone :: Text -> Text
+standalone code =
+  [__i|
+  \\documentclass{article}
+  \\usepackage{tcolorbox}
+  \\usepackage{fvextra}
+  \\usepackage[theme=latte]{juvix}
+  \\begin{document}
+  #{verb code}
+  \\end{document}
+ |]
+
+sublist :: Maybe Int -> Maybe Int -> [a] -> [a]
+sublist mfromIx mtoIx l =
+  take
+    (toIx + 1 - fromIx)
+    (drop fromIx l)
+  where
+    fromIx = fromMaybe 0 mfromIx
+    toIx = fromMaybe (length l - 1) mtoIx

app/Commands/Dev/Latex/Export/Options.hs

@@ -0,0 +1,83 @@
+module Commands.Dev.Latex.Export.Options where
+
+import CommonOptions
+import Prelude qualified
+
+data ExportOptions = ExportOptions
+  { _exportInputFile :: AppPath File,
+    _exportMode :: ExportMode,
+    _exportNoComments :: Bool,
+    _exportFromLine :: Maybe Int,
+    _exportToLine :: Maybe Int
+  }
+  deriving stock (Data)
+
+data ExportMode
+  = ExportStandalone
+  | ExportWrap
+  | ExportRaw
+  deriving stock (Enum, Bounded, Ord, Eq, Data, Generic)
+
+instance Show ExportMode where
+  show = \case
+    ExportWrap -> "wrap"
+    ExportStandalone -> "standalone"
+    ExportRaw -> "raw"
+
+makeLenses ''ExportOptions
+
+exportModeHelp :: ExportMode -> AnsiDoc
+exportModeHelp = \case
+  ExportWrap -> "Wrap the code in a Verbatim environment"
+  ExportStandalone -> "Output a ready to compile LaTeX file"
+  ExportRaw -> "Output only the code"
+
+parseExport :: Parser ExportOptions
+parseExport = do
+  _exportInputFile <- parseInputFiles (pure FileExtJuvix)
+  _exportNoComments <-
+    switch
+      ( long "no-comments"
+          <> help "Do not print comments"
+      )
+  _exportMode <-
+    option
+      (enumReader Proxy)
+      ( long "mode"
+          <> helpDoc ("How to deliver the output:\n" <> enumHelp exportModeHelp)
+          <> showDefault
+          <> completer (enumCompleter @ExportMode Proxy)
+          <> value ExportStandalone
+      )
+  _exportFromLine <-
+    optional $
+      option
+        readLineNumber
+        ( long "from"
+            <> metavar "LINE"
+            <> help "Output from the given line onwards"
+        )
+  _exportToLine <-
+    optional $
+      option
+        readLineNumber
+        ( long "to"
+            <> metavar "LINE"
+            <> help "Output until the given line (included)"
+        )
+  pure ExportOptions {..}
+  where
+    readLineNumber :: ReadM Int
+    readLineNumber = eitherReader readr
+      where
+        readr :: String -> Either String Int
+        readr inputStr = do
+          num <- readEither inputStr
+          when
+            (num <= 0)
+            $ Left
+              ( "Invalid line number "
+                  <> show num
+                  <> ". Line number must be at least 1"
+              )
+          return num

app/Commands/Dev/Latex/GetJuvixSty.hs

@@ -0,0 +1,8 @@
+module Commands.Dev.Latex.GetJuvixSty where
+
+import Commands.Base
+import Commands.Dev.Latex.GetJuvixSty.Options
+import Juvix.Extra.Paths
+
+runCommand :: (Members AppEffects r) => GetJuvixStyOptions -> Sem r ()
+runCommand _ = renderStdOutRaw juvixSty

app/Commands/Dev/Latex/GetJuvixSty/Options.hs

@@ -0,0 +1,11 @@
+module Commands.Dev.Latex.GetJuvixSty.Options where
+
+import CommonOptions
+
+data GetJuvixStyOptions = GetJuvixStyOptions
+  deriving stock (Data)
+
+makeLenses ''GetJuvixStyOptions
+
+parseGetJuvixSty :: Parser GetJuvixStyOptions
+parseGetJuvixSty = pure GetJuvixStyOptions

app/Commands/Dev/Latex/Options.hs

@@ -0,0 +1,41 @@
+module Commands.Dev.Latex.Options
+  ( module Commands.Dev.Latex.Options,
+    module Commands.Dev.Latex.Export.Options,
+    module Commands.Dev.Latex.GetJuvixSty.Options,
+  )
+where
+
+import Commands.Dev.Latex.Export.Options
+import Commands.Dev.Latex.GetJuvixSty.Options
+import CommonOptions
+
+data LatexCommand
+  = Export ExportOptions
+  | GetJuvixSty GetJuvixStyOptions
+  deriving stock (Data)
+
+parseLatex :: Parser LatexCommand
+parseLatex =
+  hsubparser $
+    mconcat
+      [ commandExport,
+        commandGetJuvixSty
+      ]
+  where
+    commandExport :: Mod CommandFields LatexCommand
+    commandExport = command "export" minfo
+      where
+        minfo :: ParserInfo LatexCommand
+        minfo =
+          info
+            (Export <$> parseExport)
+            (progDesc "Export a Juvix module to LaTeX")
+
+    commandGetJuvixSty :: Mod CommandFields LatexCommand
+    commandGetJuvixSty = command "getJuvixSty" minfo
+      where
+        minfo :: ParserInfo LatexCommand
+        minfo =
+          info
+            (GetJuvixSty <$> parseGetJuvixSty)
+            (progDesc "Print juvix.sty to stdout")

app/Commands/Dev/Options.hs

@@ -2,6 +2,7 @@ module Commands.Dev.Options
   ( module Commands.Dev.Options,
     module Commands.Dev.Asm.Options,
     module Commands.Dev.Core.Options,
+    module Commands.Dev.Latex.Options,
     module Commands.Dev.Internal.Options,
     module Commands.Dev.Parse.Options,
     module Commands.Dev.Highlight.Options,
@@ -19,6 +20,7 @@ import Commands.Dev.DisplayRoot.Options
 import Commands.Dev.Highlight.Options
 import Commands.Dev.ImportTree.Options
 import Commands.Dev.Internal.Options
+import Commands.Dev.Latex.Options
 import Commands.Dev.MigrateJuvixYaml.Options
 import Commands.Dev.Nockma.Options
 import Commands.Dev.Parse.Options
@@ -34,6 +36,7 @@ import CommonOptions
 data DevCommand
   = DisplayRoot RootOptions
   | ImportTree ImportTreeCommand
+  | Latex LatexCommand
   | Highlight HighlightOptions
   | Internal InternalCommand
   | DevCompile DevCompileCommand
@@ -71,10 +74,18 @@ parseDevCommand =
           commandTermination,
           commandJuvixDevRepl,
           commandMigrateJuvixYaml,
+          commandLatex,
           commandNockma
         ]
     )
 
+commandLatex :: Mod CommandFields DevCommand
+commandLatex =
+  command "latex" $
+    info
+      (Latex <$> parseLatex)
+      (progDesc "Subcommands related to LaTeX")
+
 commandImportTree :: Mod CommandFields DevCommand
 commandImportTree =
   command "import-tree" $

app/Commands/Dev/Reg/Compile.hs

@@ -9,7 +9,6 @@ import Juvix.Compiler.Backend.C qualified as C
 import Juvix.Compiler.Casm.Data.Result qualified as Casm
 import Juvix.Compiler.Casm.Pretty qualified as Casm
 import Juvix.Compiler.Reg.Translation.FromSource qualified as Reg
-import Juvix.Prelude.Pretty
 
 runCommand :: forall r. (Members '[EmbedIO, App, TaggedLock] r) => CompileOptions -> Sem r ()
 runCommand opts = do

app/Commands/Dev/Scope.hs

@@ -5,7 +5,6 @@ import Commands.Dev.Scope.Options
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Print qualified as Print
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
-import Juvix.Prelude.Pretty
 
 runCommand :: (Members AppEffects r) => ScopeOptions -> Sem r ()
 runCommand opts = do

app/Commands/Dev/Termination/CallGraph.hs

@@ -7,7 +7,6 @@ import Juvix.Compiler.Internal.Pretty qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination qualified as Termination
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal
 import Juvix.Compiler.Store.Extra qualified as Stored
-import Juvix.Prelude.Pretty
 
 runCommand :: (Members AppEffects r) => CallGraphOptions -> Sem r ()
 runCommand CallGraphOptions {..} = do

app/Commands/Dev/Tree/CompileOld/Base.hs

@@ -13,7 +13,6 @@ import Juvix.Compiler.Nockma.Pretty qualified as Nockma
 import Juvix.Compiler.Nockma.Translation.FromTree qualified as Nockma
 import Juvix.Compiler.Reg.Pretty qualified as Reg
 import Juvix.Compiler.Tree.Data.InfoTable qualified as Tree
-import Juvix.Prelude.Pretty
 
 data PipelineArg = PipelineArg
   { _pipelineArgOptions :: CompileOptions,

app/Commands/Dev/Tree/Eval/Options.hs

@@ -1,7 +1,6 @@
 module Commands.Dev.Tree.Eval.Options where
 
 import CommonOptions
-import Juvix.Prelude.Pretty
 import Prelude (show)
 
 data Evaluator

app/Commands/Repl.hs

@@ -34,7 +34,6 @@ import Juvix.Data.NameKind
 import Juvix.Extra.Paths qualified as P
 import Juvix.Extra.Stdlib
 import Juvix.Extra.Version
-import Juvix.Prelude.Pretty
 import Juvix.Prelude.Pretty qualified as P
 import System.Console.ANSI qualified as Ansi
 import System.Console.Haskeline