use theory names without dots

anoma · May 8, 2024 · e0b0666 · e0b0666
1 parent 96db9ca
commit e0b0666
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
@@ -3,6 +3,7 @@ module Commands.Isabelle where
 import Commands.Base
 import Commands.Isabelle.Options
 import Juvix.Compiler.Backend.Isabelle.Data.Result
+import Juvix.Compiler.Backend.Isabelle.Language
 import Juvix.Compiler.Backend.Isabelle.Pretty
 
 runCommand ::
@@ -23,7 +24,7 @@ runCommand opts = do
           let file :: Path Rel File
               file =
                 relFile
-                  ( unpack (res ^. resultModuleId . moduleIdPath)
+                  ( unpack (thy ^. theoryName . namePretty)
                       <.> isabelleFileExt
                   )
               absPath :: Path Abs File

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -1,6 +1,7 @@
 module Juvix.Compiler.Backend.Isabelle.Translation.FromTyped where
 
 import Data.HashMap.Strict qualified as HashMap
+import Data.Text qualified as T
 import Juvix.Compiler.Backend.Isabelle.Data.Result
 import Juvix.Compiler.Backend.Isabelle.Language
 import Juvix.Compiler.Internal.Data.InfoTable qualified as Internal
@@ -39,11 +40,16 @@ fromInternal Internal.InternalTypedResult {..} = do
 goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory
 goModule onlyTypes infoTable Internal.Module {..} =
   Theory
-    { _theoryName = _moduleName,
+    { _theoryName = over nameText toIsabelleName $ over namePretty toIsabelleName _moduleName,
       _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
       _theoryStatements = concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
     }
   where
+    toIsabelleName :: Text -> Text
+    toIsabelleName name = case reverse $ filter (/= "") $ T.splitOn "." name of
+      h : _ -> h
+      [] -> impossible
+
     isTypeDef :: Statement -> Bool
     isTypeDef = \case
       StmtDefinition {} -> False