Add --statements flag to juvix dev latex export (#2946)

This pr adds the `--statements` flag to `juvix dev latex export`. It can
be used like this:
```
juvix dev latex export --statements "List; elem; find" List.juvix
```
All statements are selectable by their 'label'. The label of a statement
is defined as:
1. The function/type/operator/alias/axiom/local_module/fixity/iterator
name being defined.
2. The module name being imported.

## Limitations:
1. Only top statements are allowed. I.e. statements inside local modules
cannot be selected.
1. Open statements are not selectable. Giving `--statements "My.Module"`
will refer to the import statement `import My.Module`.
4. Single constructors are not selectable. Only the whole type
definition.
5. No comments will be printed.

app/Commands/Dev/Latex/Export.hs

@@ -12,21 +12,40 @@ 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 :: forall r. (Members AppEffects r) => ExportOptions -> Sem r ()
 runCommand ExportOptions {..} = do
   res :: Scoper.ScoperResult <- silenceProgressLog (runPipelineNoOptions (Just _exportInputFile) upToScopingEntry)
+  inputAbs :: Path Abs File <- fromAppPathFile _exportInputFile
   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
+      c :: Maybe FileComments = do
+        guard (not _exportNoComments)
+        return (fromJust (Scoper.getScoperResultComments res ^. commentsByFile . at inputAbs))
+  ltx :: Text <- case _exportFilter of
+    ExportFilterNames names -> goNames m names
+    ExportFilterRange ExportRange {..} ->
+      return
+        . Text.unlines
+        . sublist (pred <$> _exportFromLine) (pred <$> _exportToLine)
+        . Text.lines
+        $ concreteToLatex c m
   renderStdOutLn $
     case _exportMode of
       ExportStandalone -> standalone ltx
       ExportRaw -> ltx
       ExportWrap -> verb ltx
+  where
+    goNames :: Module 'Scoped 'ModuleTop -> [Text] -> Sem r Text
+    goNames m ns = do
+      stms :: [Statement 'Scoped] <- mapM getStatement ns
+      return (concreteToLatex Nothing (Statements stms))
+      where
+        getStatement :: Text -> Sem r (Statement 'Scoped)
+        getStatement lbl = case tbl ^. at lbl of
+          Nothing -> exitFailMsg ("The statement " <> lbl <> " does not exist")
+          Just s -> return s
+
+        tbl :: HashMap Text (Statement 'Scoped)
+        tbl = topStatementsByLabel m
 
 verb :: Text -> Text
 verb code =

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

@@ -3,12 +3,22 @@ module Commands.Dev.Latex.Export.Options where
 import CommonOptions
 import Prelude qualified
 
+data ExportFilter
+  = ExportFilterRange ExportRange
+  | ExportFilterNames [Text]
+  deriving stock (Data)
+
+data ExportRange = ExportRange
+  { _exportFromLine :: Maybe Int,
+    _exportToLine :: Maybe Int
+  }
+  deriving stock (Data)
+
 data ExportOptions = ExportOptions
   { _exportInputFile :: AppPath File,
     _exportMode :: ExportMode,
-    _exportNoComments :: Bool,
-    _exportFromLine :: Maybe Int,
-    _exportToLine :: Maybe Int
+    _exportFilter :: ExportFilter,
+    _exportNoComments :: Bool
   }
   deriving stock (Data)
 
@@ -65,7 +75,20 @@ parseExport = do
             <> metavar "LINE"
             <> help "Output until the given line (included)"
         )
-  pure ExportOptions {..}
+  mexportNames <-
+    optional $
+      option
+        readMIdentifierList
+        ( long "statements"
+            <> metavar "[STATEMENT_NAME]"
+            <> help "Export a list of statements. E.g. --statements \"List; foldl; foldr; map\". Comments are not printed"
+        )
+
+  pure $
+    let _exportFilter :: ExportFilter = case mexportNames of
+          Nothing -> ExportFilterRange ExportRange {..}
+          Just names -> ExportFilterNames names
+     in ExportOptions {..}
   where
     readLineNumber :: ReadM Int
     readLineNumber = eitherReader readr

app/CommonOptions.hs

@@ -13,14 +13,18 @@ import Control.Exception qualified as GHC
 import Data.List.NonEmpty qualified as NonEmpty
 import GHC.Conc
 import Juvix.Compiler.Casm.Data.TransformationId.Parser qualified as Casm
+import Juvix.Compiler.Concrete.Translation.FromSource.Lexer
+import Juvix.Compiler.Concrete.Translation.FromSource.ParserResultBuilder
 import Juvix.Compiler.Concrete.Translation.ImportScanner
 import Juvix.Compiler.Core.Data.TransformationId.Parser qualified as Core
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Compiler.Reg.Data.TransformationId.Parser qualified as Reg
 import Juvix.Compiler.Tree.Data.TransformationId.Parser qualified as Tree
 import Juvix.Data.Field
+import Juvix.Data.Keyword.All qualified as Kw
 import Juvix.Prelude
 import Juvix.Prelude as Juvix
+import Juvix.Prelude.Parsing qualified as P
 import Juvix.Prelude.Pretty hiding (group, list)
 import Options.Applicative hiding (helpDoc)
 import Options.Applicative qualified as Opt
@@ -371,3 +375,15 @@ instance EntryPointOptions (EntryPoint -> EntryPoint) where
 
 instance EntryPointOptions () where
   applyOptions () = id
+
+readMParsecS :: ParsecS '[ParserResultBuilder] a -> ReadM a
+readMParsecS p = eitherReader $ \strInput ->
+  run (ignoreParserResultBuilder (P.parseHelperS p (pack strInput)))
+
+readMIdentifier :: ReadM Text
+readMIdentifier = readMParsecS identifier
+
+readMIdentifierList :: ReadM [Text]
+readMIdentifierList =
+  readMParsecS $
+    P.sepEndBy identifier (kw Kw.delimSemicolon)

src/Juvix/Compiler/Backend/Latex/Translation/FromScoped/Source.hs

@@ -1,5 +1,5 @@
 module Juvix.Compiler.Backend.Latex.Translation.FromScoped.Source
-  ( moduleToLatex,
+  ( concreteToLatex,
   )
 where
 
@@ -28,21 +28,19 @@ data LatexColor
   | JuJudoc
   | JuModule
 
-moduleToLatex ::
-  Maybe Comments ->
-  Module 'Scoped 'ModuleTop ->
+concreteToLatex ::
+  (PrettyPrint a) =>
+  Maybe FileComments ->
+  a ->
   Text
-moduleToLatex c = toStrict . Builder.toLazyText . genModuleLatex c
+concreteToLatex c = toStrict . Builder.toLazyText . genLatex c
 
-genModuleLatex ::
-  Maybe Comments ->
-  Module 'Scoped 'ModuleTop ->
-  TextBuilder
-genModuleLatex c =
+genLatex :: (PrettyPrint a) => Maybe FileComments -> a -> TextBuilder
+genLatex c =
   renderTree
     . treeForm
     . layoutPretty defaultLayoutOptions
-    . doc defaultOptions c
+    . docHelper c defaultOptions
 
 renderTree :: SimpleDocTree Ann -> TextBuilder
 renderTree = go

src/Juvix/Compiler/Concrete/Language.hs

@@ -1,8 +1,51 @@
 module Juvix.Compiler.Concrete.Language
   ( module Juvix.Compiler.Concrete.Language.Base,
     module Juvix.Compiler.Concrete.Language.IsApeInstances,
+    module Juvix.Compiler.Concrete.Language,
   )
 where
 
+import Juvix.Compiler.Concrete.Data.ScopedName
 import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Compiler.Concrete.Language.IsApeInstances
+import Juvix.Prelude
+
+symbolTypeLabel :: forall s. (SingI s) => Lens' (SymbolType s) Text
+symbolTypeLabel = case sing :: SStage s of
+  SParsed -> withLocParam
+  SScoped -> nameVerbatim
+
+modulePathTypeLabel :: forall s t. (SingI s, SingI t) => ModulePathType s t -> Text
+modulePathTypeLabel = case (sing :: SStage s, sing :: SModuleIsTop t) of
+  (SParsed, SModuleTop) -> topModulePathToDottedPath
+  (SParsed, SModuleLocal) -> (^. symbolTypeLabel)
+  (SScoped, SModuleTop) -> (^. nameVerbatim)
+  (SScoped, SModuleLocal) -> (^. symbolTypeLabel)
+
+-- | Returns a label for the given statement. Useful so that we can refer to
+-- statements from the CLI. This label may not be unique (e.g. for two import
+-- statements that import the same module).
+statementLabel :: forall s. (SingI s) => Statement s -> Maybe Text
+statementLabel = \case
+  StatementSyntax s -> goSyntax s
+  StatementOpenModule {} -> Nothing
+  StatementProjectionDef {} -> Nothing
+  StatementFunctionDef f -> Just (f ^. signName . symbolTypeLabel)
+  StatementImport i -> Just (i ^. importModulePath . to modulePathTypeLabel)
+  StatementInductive i -> Just (i ^. inductiveName . symbolTypeLabel)
+  StatementModule i -> Just (i ^. modulePath . to modulePathTypeLabel)
+  StatementAxiom a -> Just (a ^. axiomName . symbolTypeLabel)
+  where
+    goSyntax :: SyntaxDef s -> Maybe Text
+    goSyntax = \case
+      SyntaxFixity f -> Just (f ^. fixitySymbol . symbolTypeLabel)
+      SyntaxOperator f -> Just (f ^. opSymbol . symbolTypeLabel)
+      SyntaxIterator f -> Just (f ^. iterSymbol . symbolTypeLabel)
+      SyntaxAlias f -> Just (f ^. aliasDefName . symbolTypeLabel)
+
+-- | Indexes top statements by label
+topStatementsByLabel :: (SingI s) => Module s t -> HashMap Text (Statement s)
+topStatementsByLabel m =
+  hashMap
+    [ (lbl, x) | x <- m ^. moduleBody, Just lbl <- [statementLabel x]
+    ]

src/Juvix/Compiler/Concrete/Language/Base.hs

@@ -280,6 +280,10 @@ data NonDefinition (s :: Stage)
   | NonDefinitionModule (Module s 'ModuleLocal)
   | NonDefinitionOpenModule (OpenModule s 'OpenFull)
 
+newtype Statements (s :: Stage) = Statements
+  { _statements :: [Statement s]
+  }
+
 data Statement (s :: Stage)
   = StatementSyntax (SyntaxDef s)
   | StatementFunctionDef (FunctionDef s)
@@ -2691,6 +2695,7 @@ deriving stock instance Ord (JudocAtom 'Parsed)
 deriving stock instance Ord (JudocAtom 'Scoped)
 
 makeLenses ''SideIfs
+makeLenses ''Statements
 makeLenses ''NamedArgumentFunctionDef
 makeLenses ''NamedArgumentPun
 makeLenses ''IsExhaustive

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -16,7 +16,7 @@ import Juvix.Compiler.Concrete.Extra qualified as Concrete
 import Juvix.Compiler.Concrete.Gen qualified as Gen
 import Juvix.Compiler.Concrete.Keywords
 import Juvix.Compiler.Concrete.Keywords qualified as Kw
-import Juvix.Compiler.Concrete.Language
+import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Compiler.Concrete.MigrateNamedApplication
 import Juvix.Compiler.Concrete.Pretty.Options
 import Juvix.Compiler.Concrete.Translation.ImportScanner.Base
@@ -484,6 +484,9 @@ instance (PrettyPrint a) => PrettyPrint [a] where
     let cs = map ppCode (toList x)
     encloseSep (ppCode @Text "[") (ppCode @Text "]") (ppCode @Text ", ") cs
 
+instance (SingI s) => PrettyPrint (Statements s) where
+  ppCode = ppStatements . (^. statements)
+
 ppStatements :: forall s r. (SingI s, Members '[ExactPrint, Reader Options] r) => [Statement s] -> Sem r ()
 ppStatements ss = paragraphs (ppGroup <$> Concrete.groupStatements (filter shouldBePrinted ss))
   where

src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs

@@ -94,3 +94,9 @@ runParserResultBuilder s =
             { _parsedLoc = getLoc c,
               _parsedTag = ParsedTagComment
             }
+
+ignoreParserResultBuilder :: Sem (ParserResultBuilder ': r) a -> Sem r a
+ignoreParserResultBuilder = interpret $ \case
+  RegisterImport {} -> return ()
+  RegisterItem {} -> return ()
+  RegisterSpaceSpan {} -> return ()

src/Juvix/Compiler/Core/Data/TransformationId/Parser/Base.hs

@@ -20,7 +20,7 @@ completionsString' :: forall t p. (PipelineId' t p) => String -> [String]
 completionsString' = map unpack . completions' @t @p . pack
 
 completions' :: forall t p. (PipelineId' t p) => Text -> [Text]
-completions' = fromRight [] . P.parseHelper (pcompletions @t @p)
+completions' = fromRight [] . P.parseHelper @String (pcompletions @t @p)
 
 transformations :: (PipelineId' t p, MonadParsec e Text m) => m [TransformationLikeId' t p]
 transformations = do

src/Juvix/Parser/Lexer.hs

@@ -1,6 +1,10 @@
 -- | This module contains lexing functions common to all parsers in the pipeline
 -- (Juvix, JuvixCore, JuvixAsm).
-module Juvix.Parser.Lexer where
+module Juvix.Parser.Lexer
+  ( module Juvix.Parser.Lexer,
+    ParsecS,
+  )
+where
 
 import Data.HashSet qualified as HashSet
 import Data.Set qualified as Set
@@ -13,8 +17,6 @@ import Juvix.Prelude
 import Juvix.Prelude.Parsing as P hiding (hspace, space, space1)
 import Text.Megaparsec.Char.Lexer qualified as L
 
-type ParsecS r = ParsecT Void Text (Sem r)
-
 parseFailure :: Int -> String -> ParsecS r a
 parseFailure off str = P.parseError $ P.FancyError off (Set.singleton (P.ErrorFail str))
 

src/Juvix/Prelude/Parsing.hs

@@ -16,7 +16,25 @@ import Juvix.Prelude.Pretty
 import Text.Megaparsec hiding (sepBy1, sepEndBy1, some)
 import Text.Megaparsec.Char
 
-parseHelper :: (TraversableStream txt, VisualStream txt) => Parsec Void txt a -> txt -> Either Text a
-parseHelper p t = case runParser p "<input>" t of
-  Left (err :: ParseErrorBundle txt Void) -> Left (prettyText (errorBundlePretty err))
-  Right r -> return r
+type ParsecS' txt r = ParsecT Void txt (Sem r)
+
+type ParsecS r = ParsecS' Text r
+
+parseHelper ::
+  forall err txt a.
+  (TraversableStream txt, VisualStream txt, IsString err) =>
+  Parsec Void txt a ->
+  txt ->
+  Either err a
+parseHelper p t = mapLeft ppParseErrorBundle (runParser p "<input>" t)
+
+parseHelperS ::
+  forall err txt a r.
+  (TraversableStream txt, VisualStream txt, IsString err) =>
+  ParsecS' txt r a ->
+  txt ->
+  Sem r (Either err a)
+parseHelperS p t = mapLeft ppParseErrorBundle <$> runParserT p "<input>" t
+
+ppParseErrorBundle :: (TraversableStream txt, VisualStream txt, IsString err) => ParseErrorBundle txt Void -> err
+ppParseErrorBundle = prettyIsString . errorBundlePretty

src/Juvix/Prelude/Pretty.hs

@@ -147,10 +147,16 @@ toPlainTextTrim :: (HasTextBackend a) => a -> Text
 toPlainTextTrim = trimText . toPlainText
 
 prettyString :: (Pretty a) => a -> String
-prettyString = renderString . layoutPretty defaultLayoutOptions . pretty
+prettyString = renderString . prettySimpleDoc
+
+prettyIsString :: (Pretty a, IsString str) => a -> str
+prettyIsString = fromString . prettyString
+
+prettySimpleDoc :: (Pretty a) => a -> SimpleDocStream ann
+prettySimpleDoc = layoutPretty defaultLayoutOptions . pretty
 
 prettyText :: (Pretty a) => a -> Text
-prettyText = Text.renderStrict . layoutPretty defaultLayoutOptions . pretty
+prettyText = Text.renderStrict . prettySimpleDoc
 
 hsepSoft' :: (Foldable f) => f (Doc a) -> Doc a
 hsepSoft' = concatWith (\a b -> a <> softline' <> b)