recursive translation

app/App.hs

@@ -255,22 +255,37 @@ runPipeline opts input_ =
   runPipelineLogger opts input_
     . inject
 
+runPipelineUpTo ::
+  (Members '[App, EmbedIO, Logger, TaggedLock] r, EntryPointOptions opts) =>
+  Bool ->
+  opts ->
+  Maybe (AppPath File) ->
+  Sem (PipelineEff r) a ->
+  Sem r (a, [a])
+runPipelineUpTo bNonRecursive opts input_ a
+  | bNonRecursive = do
+      r <- runPipeline opts input_ a
+      return (r, [])
+  | otherwise = runPipelineUpToRecursive opts input_ a
+
 runPipelineHtml ::
   (Members '[App, EmbedIO, Logger, TaggedLock] r) =>
   Bool ->
   Maybe (AppPath File) ->
   Sem r (InternalTypedResult, [InternalTypedResult])
-runPipelineHtml bNonRecursive input_
-  | bNonRecursive = do
-      r <- runPipelineNoOptions input_ upToInternalTyped
-      return (r, [])
-  | otherwise = runPipelineRecursive input_
+runPipelineHtml bNonRecursive input_ = runPipelineUpTo bNonRecursive () input_ upToInternalTyped
 
-runPipelineRecursive :: (Members '[App, EmbedIO, Logger, TaggedLock] r) => Maybe (AppPath File) -> Sem r (InternalTypedResult, [InternalTypedResult])
-runPipelineRecursive input_ = do
+runPipelineUpToRecursive ::
+  (Members '[App, EmbedIO, Logger, TaggedLock] r, EntryPointOptions opts) =>
+  opts ->
+  Maybe (AppPath File) ->
+  Sem (PipelineEff r) a ->
+  Sem r (a, [a])
+runPipelineUpToRecursive opts input_ a = do
   args <- askArgs
   entry <- getEntryPoint' args input_
-  runReader defaultPipelineOptions (runPipelineRecursiveEither entry) >>= fromRightJuvixError
+  let entry' = applyOptions opts entry
+  runReader defaultPipelineOptions (runPipelineRecursiveEither entry' (inject a)) >>= fromRightJuvixError
 
 runPipelineOptions :: (Members '[App] r) => Sem (Reader PipelineOptions ': r) a -> Sem r a
 runPipelineOptions m = do

app/Commands/Isabelle.hs

@@ -12,22 +12,29 @@ runCommand ::
   Sem r ()
 runCommand opts = do
   let inputFile = opts ^. isabelleInputFile
-  res <- runPipeline opts inputFile upToIsabelle
-  let thy = res ^. resultTheory
-      comments = res ^. resultComments
-  outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
-  if
-      | opts ^. isabelleStdout -> do
-          renderStdOut (ppOutDefault comments thy)
-          putStrLn ""
-      | otherwise -> do
-          ensureDir outputDir
-          let file :: Path Rel File
-              file =
-                relFile
-                  ( unpack (thy ^. theoryName . namePretty)
-                      <.> isabelleFileExt
-                  )
-              absPath :: Path Abs File
-              absPath = outputDir <//> file
-          writeFileEnsureLn absPath (ppPrint comments thy <> "\n")
+  (r, rs) <- runPipelineUpTo (opts ^. isabelleNonRecursive) opts inputFile upToIsabelle
+  let pkg = r ^. resultModuleId . moduleIdPackage
+  mapM_ (translateTyped opts pkg) (r : rs)
+
+translateTyped :: (Members AppEffects r) => IsabelleOptions -> Text -> Result -> Sem r ()
+translateTyped opts pkg res
+  | res ^. resultModuleId . moduleIdPackage == pkg = do
+      let thy = res ^. resultTheory
+          comments = res ^. resultComments
+      outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
+      if
+          | opts ^. isabelleStdout -> do
+              renderStdOut (ppOutDefault comments thy)
+              putStrLn ""
+          | otherwise -> do
+              ensureDir outputDir
+              let file :: Path Rel File
+                  file =
+                    relFile
+                      ( unpack (thy ^. theoryName . namePretty)
+                          <.> isabelleFileExt
+                      )
+                  absPath :: Path Abs File
+                  absPath = outputDir <//> file
+              writeFileEnsureLn absPath (ppPrint comments thy <> "\n")
+  | otherwise = return ()

app/Commands/Isabelle/Options.hs

@@ -4,7 +4,8 @@ import CommonOptions
 import Juvix.Compiler.Pipeline.EntryPoint
 
 data IsabelleOptions = IsabelleOptions
-  { _isabelleInputFile :: Maybe (AppPath File),
+  { _isabelleNonRecursive :: Bool,
+    _isabelleInputFile :: Maybe (AppPath File),
     _isabelleOutputDir :: AppPath Dir,
     _isabelleStdout :: Bool,
     _isabelleOnlyTypes :: Bool
@@ -15,6 +16,11 @@ makeLenses ''IsabelleOptions
 
 parseIsabelle :: Parser IsabelleOptions
 parseIsabelle = do
+  _isabelleNonRecursive <-
+    switch
+      ( long "non-recursive"
+          <> help "Do not process imported modules recursively"
+      )
   _isabelleOutputDir <-
     parseGenericOutputDir
       ( value "isabelle"

src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs

@@ -312,7 +312,7 @@ instance PrettyCode RecordField where
 
 ppImports :: [Name] -> Sem r [Doc Ann]
 ppImports ns =
-  return $ map (dquotes . pretty) $ filter (not . Text.isPrefixOf "Stdlib/") $ map (Text.replace "." "/" . (^. namePretty)) ns
+  return $ map pretty $ filter (not . Text.isPrefixOf "Stdlib_" . (^. namePretty)) ns
 
 instance PrettyCode Theory where
   ppCode Theory {..} = do

src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs

@@ -51,59 +51,36 @@ fromInternal res@Internal.InternalTypedResult {..} = do
       itab' = Internal.insertInternalModule itab md
       table :: Internal.InfoTable
       table = Internal.computeCombinedInfoTable itab'
-      moduleNames :: [Name]
-      moduleNames = map (^. Internal.internalModuleName) (HashMap.elems (itab' ^. Internal.internalModuleTable))
       comments :: [Comment]
       comments = allComments (Internal.getInternalTypedResultComments res)
-  go onlyTypes comments moduleNames table _resultModule
+  go onlyTypes comments table _resultModule
   where
-    go :: Bool -> [Comment] -> [Name] -> Internal.InfoTable -> Internal.Module -> Sem r Result
-    go onlyTypes comments moduleNames tab md =
+    go :: Bool -> [Comment] -> Internal.InfoTable -> Internal.Module -> Sem r Result
+    go onlyTypes comments tab md =
       return $
         Result
-          { _resultTheory = goModule onlyTypes moduleNames tab md,
+          { _resultTheory = goModule onlyTypes tab md,
             _resultModuleId = md ^. Internal.moduleId,
             _resultComments = filter (\c -> c ^. commentInterval . intervalFile == file) comments
           }
       where
         file = getLoc md ^. intervalFile
 
-goModule :: Bool -> [Name] -> Internal.InfoTable -> Internal.Module -> Theory
-goModule onlyTypes moduleNames infoTable Internal.Module {..} =
+goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory
+goModule onlyTypes infoTable Internal.Module {..} =
   Theory
-    { _theoryName = lookupTheoryName _moduleName,
+    { _theoryName = overNameText toIsabelleTheoryName _moduleName,
       _theoryImports =
-        map lookupTheoryName $
+        map (overNameText toIsabelleTheoryName) $
           map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
       _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of
         Just (PragmaIsabelleIgnore True) -> []
         _ -> concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
     }
   where
     toIsabelleTheoryName :: Text -> Text
-    toIsabelleTheoryName name = case reverse $ filter (/= "") $ T.splitOn "." name of
-      h : _ -> h
-      [] -> impossible
-
-    moduleNameMap :: HashMap Name Name
-    moduleNameMap =
-      HashMap.fromList $ concatMap mapGroup groups
-      where
-        groups = groupSortOn (toIsabelleTheoryName . (^. nameText)) moduleNames
-
-        mapGroup :: NonEmpty Name -> [(Name, Name)]
-        mapGroup (name :| names) =
-          (name, overNameText toIsabelleTheoryName name) : names'
-          where
-            names' =
-              zipWith
-                (\n (idx :: Int) -> (n, overNameText (<> "_" <> show idx) n))
-                names
-                [0 ..]
-
-    lookupTheoryName :: Name -> Name
-    lookupTheoryName name =
-      fromMaybe (error "lookupTheoryName") $ HashMap.lookup name moduleNameMap
+    toIsabelleTheoryName name =
+      Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name
 
     isTypeDef :: Statement -> Bool
     isTypeDef = \case

src/Juvix/Compiler/Pipeline/Driver.hs

@@ -11,7 +11,7 @@ module Juvix.Compiler.Pipeline.Driver
     processFileUpToParsing,
     processModule,
     processImport,
-    processRecursiveUpToTyped,
+    processRecursiveUpTo,
     processImports,
     processModuleToStoredCore,
   )
@@ -30,12 +30,12 @@ import Juvix.Compiler.Core.Data.Module qualified as Core
 import Juvix.Compiler.Core.Translation.FromInternal.Data.Context qualified as Core
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as InternalTyped
-import Juvix.Compiler.Internal.Translation.FromInternal.Data (InternalTypedResult)
 import Juvix.Compiler.Pipeline
 import Juvix.Compiler.Pipeline.Driver.Data
 import Juvix.Compiler.Pipeline.JvoCache
 import Juvix.Compiler.Pipeline.Loader.PathResolver
 import Juvix.Compiler.Pipeline.ModuleInfoCache
+import Juvix.Compiler.Pipeline.Package.Loader.EvalEff (EvalFileEff)
 import Juvix.Compiler.Store.Core.Extra
 import Juvix.Compiler.Store.Extra qualified as Store
 import Juvix.Compiler.Store.Language
@@ -132,8 +132,8 @@ processProject = do
   nodes <- toList <$> asks (importTreeProjectNodes rootDir)
   forWithM nodes (mkEntryIndex >=> processModule)
 
-processRecursiveUpToTyped ::
-  forall r.
+processRecursiveUpTo ::
+  forall a r.
   ( Members
       '[ Reader EntryPoint,
          TopModuleNameChecker,
@@ -142,35 +142,37 @@ processRecursiveUpToTyped ::
          Error JuvixError,
          Files,
          PathResolver,
-         ModuleInfoCache
+         ModuleInfoCache,
+         EvalFileEff
        ]
       r
   ) =>
-  Sem r (InternalTypedResult, [InternalTypedResult])
-processRecursiveUpToTyped = do
+  Sem (Reader Parser.ParserResult ': Reader Store.ModuleTable ': NameIdGen ': r) a ->
+  Sem r (a, [a])
+processRecursiveUpTo a = do
   entry <- ask
   PipelineResult {..} <- processFileUpToParsing entry
   let imports = HashMap.keys (_pipelineResultImports ^. Store.moduleTable)
   ms <- forM imports $ \imp ->
     withPathFile imp goImport
   let pkg = entry ^. entryPointPackage
   mid <- runReader pkg (getModuleId (_pipelineResult ^. Parser.resultModule . modulePath . to topModulePathKey))
-  a <-
+  r <-
     evalTopNameIdGen mid
       . runReader _pipelineResultImports
       . runReader _pipelineResult
-      $ upToInternalTyped
-  return (a, ms)
+      $ a
+  return (r, ms)
   where
-    goImport :: ImportNode -> Sem r InternalTypedResult
+    goImport :: ImportNode -> Sem r a
     goImport node = do
       entry <- ask
       let entry' =
             entry
               { _entryPointStdin = Nothing,
                 _entryPointModulePath = Just (node ^. importNodeAbsFile)
               }
-      (^. pipelineResult) <$> runReader entry' (processFileUpTo upToInternalTyped)
+      (^. pipelineResult) <$> local (const entry') (processFileUpTo a)
 
 processImport ::
   forall r.

src/Juvix/Compiler/Pipeline/Run.hs

@@ -52,13 +52,14 @@ runPipelineHighlight ::
 runPipelineHighlight entry = fmap fst . runIOEitherHelper entry
 
 runPipelineRecursiveEither ::
-  forall r.
+  forall a r.
   (Members PipelineAppEffects r) =>
   EntryPoint ->
-  Sem r (Either JuvixError (Typed.InternalTypedResult, [Typed.InternalTypedResult]))
-runPipelineRecursiveEither entry = do
+  Sem (PipelineEff r) a ->
+  Sem r (Either JuvixError (a, [a]))
+runPipelineRecursiveEither entry a = do
   x <- runIOEitherPipeline' entry $ do
-    processRecursiveUpToTyped
+    processRecursiveUpTo a
   return . mapRight snd $ snd x
 
 runIOEitherHelper ::