CLI

app/Commands/Isabelle.hs

@@ -2,6 +2,7 @@ module Commands.Isabelle where
 
 import Commands.Base
 import Commands.Isabelle.Options
+import Data.Text.IO qualified as Text
 import Juvix.Compiler.Backend.Isabelle.Data.Result
 import Juvix.Compiler.Backend.Isabelle.Pretty
 
@@ -13,5 +14,19 @@ runCommand opts = do
   let inputFile = opts ^. isabelleInputFile
   res <- runPipelineNoOptions inputFile upToIsabelle
   let thy = res ^. resultTheory
-  renderStdOut (ppOutDefault thy)
-  putStrLn ""
+  outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
+  if
+      | opts ^. isabelleStdout -> do
+          renderStdOut (ppOutDefault thy)
+          putStrLn ""
+      | otherwise -> do
+          ensureDir outputDir
+          let file :: Path Rel File
+              file =
+                relFile
+                  ( unpack (res ^. resultModuleId . moduleIdPath)
+                      <.> isabelleFileExt
+                  )
+              absPath :: Path Abs File
+              absPath = outputDir <//> file
+          liftIO $ Text.writeFile (toFilePath absPath) (ppPrint thy)

app/Commands/Isabelle/Options.hs

@@ -5,25 +5,25 @@ import CommonOptions
 data IsabelleOptions = IsabelleOptions
   { _isabelleInputFile :: Maybe (AppPath File),
     _isabelleOutputDir :: AppPath Dir,
-    _isabelleRecursive :: Bool
+    _isabelleStdout :: Bool
   }
   deriving stock (Data)
 
 makeLenses ''IsabelleOptions
 
 parseIsabelle :: Parser IsabelleOptions
 parseIsabelle = do
-  _isabelleRecursive <-
-    switch
-      ( long "recursive"
-          <> help "Process imported modules recursively"
-      )
   _isabelleOutputDir <-
     parseGenericOutputDir
       ( value "isabelle"
           <> showDefault
           <> help "Isabelle/HOL output directory"
           <> action "directory"
       )
+  _isabelleStdout <-
+    switch
+      ( long "stdout"
+          <> help "Write the output to stdout instead of a file"
+      )
   _isabelleInputFile <- optional (parseInputFile FileExtJuvix)
   pure IsabelleOptions {..}

src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs

@@ -3,7 +3,8 @@ module Juvix.Compiler.Backend.Isabelle.Data.Result where
 import Juvix.Compiler.Backend.Isabelle.Language
 
 data Result = Result
-  { _resultTheory :: Theory
+  { _resultTheory :: Theory,
+    _resultModuleId :: ModuleId
   }
 
 makeLenses ''Result

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

@@ -110,14 +110,13 @@ instance PrettyCode RecordField where
 instance PrettyCode Theory where
   ppCode Theory {..} = do
     n <- ppCode _theoryName
-    imps <- mapM ppCode _theoryImports
     stmts <- mapM ppCode _theoryStatements
     return $
       kwTheory
         <+> n
           <> line
           <> kwImports
-        <+> hsep ("Main" : imps)
+        <+> "Main"
           <> line
           <> kwBegin
           <> line

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

@@ -28,7 +28,12 @@ fromInternal Internal.InternalTypedResult {..} = do
   go table _resultModule
   where
     go :: Internal.InfoTable -> Internal.Module -> Sem r Result
-    go tab md = return $ Result $ goModule tab md
+    go tab md =
+      return $
+        Result
+          { _resultTheory = goModule tab md,
+            _resultModuleId = md ^. Internal.moduleId
+          }
 
 goModule :: Internal.InfoTable -> Internal.Module -> Theory
 goModule infoTable Internal.Module {..} =

src/Juvix/Data/FileExt.hs

@@ -79,6 +79,9 @@ htmlFileExt = ".html"
 markdownFileExt :: (IsString a) => a
 markdownFileExt = ".md"
 
+isabelleFileExt :: (IsString a) => a
+isabelleFileExt = ".thy"
+
 cFileExt :: (IsString a) => a
 cFileExt = ".c"
 

src/Juvix/Prelude/Prepath.hs

@@ -19,15 +19,19 @@ import Juvix.Prelude.Pretty
 import System.Directory (getHomeDirectory)
 import System.Directory qualified as System
 import System.Environment
+import Prelude (show)
 
 -- | A file/directory path that may contain environmental variables
 newtype Prepath d = Prepath
   { _prepath :: String
   }
-  deriving stock (Show, Eq, Data, Generic)
+  deriving stock (Eq, Data, Generic)
 
 makeLenses ''Prepath
 
+instance Show (Prepath d) where
+  show Prepath {..} = _prepath
+
 type PrepathParts = NonEmpty PrepathPart
 
 data PrepathPart