Isabelle/HOL translation: recursive translation of the whole project

app/App.hs

@@ -255,19 +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 = do
-      args <- askArgs
-      entry <- getEntryPoint' args input_
-      runReader defaultPipelineOptions (runPipelineHtmlEither entry) >>= fromRightJuvixError
+runPipelineHtml bNonRecursive input_ = runPipelineUpTo bNonRecursive () input_ upToInternalTyped
+
+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_
+  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,28 @@ 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 ->
+              renderStdOutLn (ppOutDefault comments thy)
+          | 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

@@ -315,7 +315,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

@@ -69,17 +69,19 @@ fromInternal [email protected] {..} = do
 goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory
 goModule onlyTypes infoTable Internal.Module {..} =
   Theory
-    { _theoryName = overNameText toIsabelleName _moduleName,
-      _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
+    { _theoryName = overNameText toIsabelleTheoryName _moduleName,
+      _theoryImports =
+        map
+          (overNameText toIsabelleTheoryName . (^. Internal.importModuleName))
+          (_moduleBody ^. Internal.moduleImports),
       _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of
         Just (PragmaIsabelleIgnore True) -> []
         _ -> concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
     }
   where
-    toIsabelleName :: Text -> Text
-    toIsabelleName name = case reverse $ filter (/= "") $ T.splitOn "." name of
-      h : _ -> h
-      [] -> impossible
+    toIsabelleTheoryName :: Text -> Text
+    toIsabelleTheoryName name =
+      quote . Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name
 
     isTypeDef :: Statement -> Bool
     isTypeDef = \case
@@ -195,8 +197,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 }
       where
         argnames =
-          map (overNameText quote) $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName (getLoc name) "_") . (^. Internal.argInfoName)) argsInfo
-        name' = overNameText quote name
+          map quoteName $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName (getLoc name) "_") . (^. Internal.argInfoName)) argsInfo
+        name' = quoteName name
         loc = getLoc name
 
     isFunction :: [Name] -> Internal.Expression -> Maybe Internal.Expression -> Bool
@@ -376,18 +378,18 @@ goModule onlyTypes infoTable Internal.Module {..} =
 
     goTypeIden :: Internal.Iden -> Type
     goTypeIden = \case
-      Internal.IdenFunction name -> mkIndType (overNameText quote name) []
+      Internal.IdenFunction name -> mkIndType (quoteName name) []
       Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name)
-      Internal.IdenVar name -> TyVar $ TypeVar (overNameText quote name)
-      Internal.IdenAxiom name -> mkIndType (overNameText quote name) []
-      Internal.IdenInductive name -> mkIndType (overNameText quote name) []
+      Internal.IdenVar name -> TyVar $ TypeVar (quoteName name)
+      Internal.IdenAxiom name -> mkIndType (quoteName name) []
+      Internal.IdenInductive name -> mkIndType (quoteName name) []
 
     goTypeApp :: Internal.Application -> Type
     goTypeApp app = mkIndType name params
       where
         (ind, args) = Internal.unfoldApplication app
         params = map goType (toList args)
-        name = overNameText quote $ case ind of
+        name = quoteName $ case ind of
           Internal.ExpressionIden (Internal.IdenFunction n) -> n
           Internal.ExpressionIden (Internal.IdenAxiom n) -> n
           Internal.ExpressionIden (Internal.IdenInductive n) -> n
@@ -416,8 +418,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
               setNameText "None" name
             Just Internal.BuiltinMaybeJust ->
               setNameText "Some" name
-            _ -> overNameText quote name
-        Nothing -> overNameText quote name
+            _ -> quoteName name
+        Nothing -> quoteName name
 
     getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter]
     getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType
@@ -430,8 +432,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
             Just funInfo ->
               case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of
                 Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name
-                Nothing -> overNameText quote name
-            Nothing -> overNameText quote name
+                Nothing -> quoteName name
+            Nothing -> quoteName name
       x -> x
 
     lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Expression
@@ -490,8 +492,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
               Nothing -> return $ ExprIden (goConstrName name)
           Internal.IdenVar name -> do
             lookupName name
-          Internal.IdenAxiom name -> return $ ExprIden (overNameText quote name)
-          Internal.IdenInductive name -> return $ ExprIden (overNameText quote name)
+          Internal.IdenAxiom name -> return $ ExprIden (quoteName name)
+          Internal.IdenInductive name -> return $ ExprIden (quoteName name)
 
         goApplication :: Internal.Application -> Sem r Expression
         goApplication [email protected] {..}
@@ -1217,9 +1219,40 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives))
                 ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
 
+    quoteName :: Name -> Name
+    quoteName name = overNameText goNameText name
+      where
+        goNameText :: Text -> Text
+        goNameText txt
+          | Text.elem '.' txt =
+              let idenName = snd $ Text.breakOnEnd "." txt
+                  modulePath = name ^. nameId . nameIdModuleId . moduleIdPath
+                  modulePathText = Text.intercalate "." (modulePath ^. modulePathKeyDir ++ [modulePath ^. modulePathKeyName])
+                  moduleName' = toIsabelleTheoryName modulePathText
+                  idenName' = quote idenName
+               in moduleName' <> "." <> idenName'
+          | otherwise = quote txt
+
     quote :: Text -> Text
-    quote = quote' . Text.filter isLatin1 . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
+    quote txt0
+      | Text.elem '.' txt0 = moduleName' <> "." <> idenName'
+      | otherwise = quote'' txt0
       where
+        (moduleName, idenName) = Text.breakOnEnd "." txt0
+        moduleName' = toIsabelleTheoryName (removeLastDot moduleName)
+        idenName' = quote'' idenName
+
+        removeLastDot :: Text -> Text
+        removeLastDot txt
+          | Text.last txt == '.' = Text.init txt
+          | otherwise = txt
+
+        quote'' :: Text -> Text
+        quote'' =
+          quote'
+            . Text.filter isLatin1
+            . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
+
         quote' :: Text -> Text
         quote' txt
           | HashSet.member txt reservedNames = quote' (prime txt)

src/Juvix/Compiler/Pipeline/Driver.hs

@@ -12,7 +12,7 @@ module Juvix.Compiler.Pipeline.Driver
     processFileUpToParsing,
     processModule,
     processImport,
-    processRecursiveUpToTyped,
+    processRecursiveUpTo,
     processImports,
     processModuleToStoredCore,
   )
@@ -32,12 +32,13 @@ 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 (readGlobalPackage)
+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
@@ -280,8 +281,8 @@ processProject = do
   nodes <- toList <$> asks (importTreeProjectNodes rootDir)
   forWithM nodes (mkEntryIndex >=> processModule)
 
-processRecursiveUpToTyped ::
-  forall r.
+processRecursiveUpTo ::
+  forall a r.
   ( Members
       '[ Reader EntryPoint,
          TopModuleNameChecker,
@@ -290,35 +291,42 @@ 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 ^. entryPointPackageId
   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
+      pkgInfo <- fromJust . HashMap.lookup (node ^. importNodePackageRoot) <$> getPackageInfos
+      pkg <- case pkgInfo ^. packagePackage of
+        PackageReal p -> return p
+        _ -> readGlobalPackage
       entry <- ask
       let entry' =
             entry
-              { _entryPointStdin = Nothing,
+              { _entryPointPackage = pkg,
+                _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

@@ -51,14 +51,15 @@ runPipelineHighlight ::
   Sem r HighlightInput
 runPipelineHighlight entry = fmap fst . runIOEitherHelper entry
 
-runPipelineHtmlEither ::
-  forall r.
+runPipelineRecursiveEither ::
+  forall a r.
   (Members PipelineAppEffects r) =>
   EntryPoint ->
-  Sem r (Either JuvixError (Typed.InternalTypedResult, [Typed.InternalTypedResult]))
-runPipelineHtmlEither 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 ::

src/Juvix/Parser/Error.hs

@@ -178,7 +178,7 @@ instance ToGenericError StdinOrFileError where
   genericError StdinOrFileError =
     return
       GenericError
-        { _genericErrorLoc = singletonInterval (mkInitialLoc formatStdinPath),
+        { _genericErrorLoc = singletonInterval (mkInitialLoc noFile),
           _genericErrorMessage = prettyError "Neither JUVIX_FILE_OR_PROJECT nor --stdin option is chosen",
           _genericErrorIntervals = []
         }

tests/positive/Isabelle/M/Main.juvix

@@ -0,0 +1,6 @@
+module M.Main;
+
+import Stdlib.Prelude open;
+import M.N open;
+
+f (a : Nat) : Nat := g a;

tests/positive/Isabelle/M/N.juvix

@@ -0,0 +1,5 @@
+module M.N;
+
+import Stdlib.Prelude open;
+
+g (a : Nat) : Nat := a + 1;

tests/positive/Isabelle/N.juvix

@@ -0,0 +1,5 @@
+module N;
+
+import Stdlib.Prelude open;
+
+g (a : Nat) : Nat := a * 2;