theory names

app/App.hs

@@ -264,10 +264,13 @@ runPipelineHtml bNonRecursive input_
   | bNonRecursive = do
       r <- runPipelineNoOptions input_ upToInternalTyped
       return (r, [])
-  | otherwise = do
-      args <- askArgs
-      entry <- getEntryPoint' args input_
-      runReader defaultPipelineOptions (runPipelineHtmlEither entry) >>= fromRightJuvixError
+  | otherwise = runPipelineRecursive input_
+
+runPipelineRecursive :: (Members '[App, EmbedIO, Logger, TaggedLock] r) => Maybe (AppPath File) -> Sem r (InternalTypedResult, [InternalTypedResult])
+runPipelineRecursive input_ = do
+  args <- askArgs
+  entry <- getEntryPoint' args input_
+  runReader defaultPipelineOptions (runPipelineRecursiveEither entry) >>= fromRightJuvixError
 
 runPipelineOptions :: (Members '[App] r) => Sem (Reader PipelineOptions ': r) a -> Sem r a
 runPipelineOptions m = do

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

@@ -51,36 +51,60 @@ fromInternal [email protected] {..} = 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 table _resultModule
+  go onlyTypes comments moduleNames table _resultModule
   where
-    go :: Bool -> [Comment] -> Internal.InfoTable -> Internal.Module -> Sem r Result
-    go onlyTypes comments tab md =
+    go :: Bool -> [Comment] -> [Name] -> Internal.InfoTable -> Internal.Module -> Sem r Result
+    go onlyTypes comments moduleNames tab md =
       return $
         Result
-          { _resultTheory = goModule onlyTypes tab md,
+          { _resultTheory = goModule onlyTypes moduleNames tab md,
             _resultModuleId = md ^. Internal.moduleId,
             _resultComments = filter (\c -> c ^. commentInterval . intervalFile == file) comments
           }
       where
         file = getLoc md ^. intervalFile
 
-goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory
-goModule onlyTypes infoTable Internal.Module {..} =
+goModule :: Bool -> [Name] -> Internal.InfoTable -> Internal.Module -> Theory
+goModule onlyTypes moduleNames infoTable Internal.Module {..} =
   Theory
-    { _theoryName = overNameText toIsabelleName _moduleName,
-      _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
+    { _theoryName = lookupTheoryName _moduleName,
+      _theoryImports =
+        map lookupTheoryName $
+          map (^. 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
+    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
+
     isTypeDef :: Statement -> Bool
     isTypeDef = \case
       StmtDefinition {} -> False

src/Juvix/Compiler/Pipeline/Run.hs

@@ -51,12 +51,12 @@ runPipelineHighlight ::
   Sem r HighlightInput
 runPipelineHighlight entry = fmap fst . runIOEitherHelper entry
 
-runPipelineHtmlEither ::
+runPipelineRecursiveEither ::
   forall r.
   (Members PipelineAppEffects r) =>
   EntryPoint ->
   Sem r (Either JuvixError (Typed.InternalTypedResult, [Typed.InternalTypedResult]))
-runPipelineHtmlEither entry = do
+runPipelineRecursiveEither entry = do
   x <- runIOEitherPipeline' entry $ do
     processRecursiveUpToTyped
   return . mapRight snd $ snd x