From 3af8bb41f515b2e15a7c16f8509ab8730a279dcc Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 24 Apr 2024 15:45:58 +0200 Subject: [PATCH] CLI --- app/Commands/Isabelle.hs | 19 +++++++++++++++++-- app/Commands/Isabelle/Options.hs | 12 ++++++------ .../Compiler/Backend/Isabelle/Data/Result.hs | 3 ++- .../Compiler/Backend/Isabelle/Pretty/Base.hs | 3 +-- .../Backend/Isabelle/Translation/FromTyped.hs | 7 ++++++- src/Juvix/Data/FileExt.hs | 3 +++ src/Juvix/Prelude/Prepath.hs | 6 +++++- 7 files changed, 40 insertions(+), 13 deletions(-) diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs index b076846a4c..999dc745f1 100644 --- a/app/Commands/Isabelle.hs +++ b/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) diff --git a/app/Commands/Isabelle/Options.hs b/app/Commands/Isabelle/Options.hs index ca14968d44..34c057e9a6 100644 --- a/app/Commands/Isabelle/Options.hs +++ b/app/Commands/Isabelle/Options.hs @@ -5,7 +5,7 @@ import CommonOptions data IsabelleOptions = IsabelleOptions { _isabelleInputFile :: Maybe (AppPath File), _isabelleOutputDir :: AppPath Dir, - _isabelleRecursive :: Bool + _isabelleStdout :: Bool } deriving stock (Data) @@ -13,11 +13,6 @@ makeLenses ''IsabelleOptions parseIsabelle :: Parser IsabelleOptions parseIsabelle = do - _isabelleRecursive <- - switch - ( long "recursive" - <> help "Process imported modules recursively" - ) _isabelleOutputDir <- parseGenericOutputDir ( value "isabelle" @@ -25,5 +20,10 @@ parseIsabelle = do <> 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 {..} diff --git a/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs b/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs index d11fbb4325..3c13082b6c 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs +++ b/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 diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs index 5cd2a24af9..d4902d83f6 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/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 diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index d7958f5d5c..5e9384244d 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/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 {..} = diff --git a/src/Juvix/Data/FileExt.hs b/src/Juvix/Data/FileExt.hs index bc43f107aa..78307a7d73 100644 --- a/src/Juvix/Data/FileExt.hs +++ b/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" diff --git a/src/Juvix/Prelude/Prepath.hs b/src/Juvix/Prelude/Prepath.hs index b3e0731e9f..b94765d9d4 100644 --- a/src/Juvix/Prelude/Prepath.hs +++ b/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