From 88fed7e0ab90186f3acfd212670e3381caaac2f4 Mon Sep 17 00:00:00 2001 From: viktorcsimma Date: Sun, 3 Mar 2024 18:06:29 +0100 Subject: [PATCH] Adding mechanism for skipping up-to-date files --- src/Agda2Hs/Compile.hs | 23 +++++++++++++++++------ src/Agda2Hs/Compile/Utils.hs | 10 ++++++++++ src/Agda2Hs/Render.hs | 11 ++--------- 3 files changed, 29 insertions(+), 15 deletions(-) diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs index 7039d62c..63d830fe 100644 --- a/src/Agda2Hs/Compile.hs +++ b/src/Agda2Hs/Compile.hs @@ -1,7 +1,7 @@ module Agda2Hs.Compile where import Control.Monad.Trans.RWS.CPS ( evalRWST ) -import Control.Monad.State ( gets ) +import Control.Monad.State ( gets, liftIO ) import Control.Arrow ((>>>)) import Data.Functor import Data.List ( isPrefixOf ) @@ -10,6 +10,7 @@ import qualified Data.Map as M import Agda.Compiler.Backend import Agda.Compiler.Common ( curIF ) +import Agda.Utils.FileName ( isNewerThan ) import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName ) import Agda.Syntax.Common.Pretty ( prettyShow ) import Agda.TypeChecking.Pretty @@ -18,6 +19,7 @@ import Agda.Utils.Null import Agda.Utils.Monad ( whenM, anyM ) import qualified Language.Haskell.Exts.Extension as Hs +import qualified Language.Haskell.Exts.Syntax as Hs import Agda2Hs.Compile.ClassInstance ( compileInstance ) import Agda2Hs.Compile.Data ( compileData ) @@ -25,7 +27,7 @@ import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlin import Agda2Hs.Compile.Postulate ( compilePostulate ) import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma ) import Agda2Hs.Compile.Types -import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, primModules, isClassName ) +import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, primModules, isClassName, moduleFileName ) import Agda2Hs.Pragma @@ -46,13 +48,22 @@ runC :: TopLevelModuleName -> SpecialRules -> C a -> TCM (a, CompileOutput) runC tlm rewrites c = evalRWST c (initCompileEnv tlm rewrites) initCompileState moduleSetup :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath -> TCM (Recompile ModuleEnv ModuleRes) -moduleSetup _ _ m _ = do +moduleSetup opts _ m mifile = do -- we never compile primitive modules if any (`isPrefixOf` prettyShow m) primModules then pure $ Skip () else do - reportSDoc "agda2hs.compile" 3 $ text "Compiling module: " <+> prettyTCM m - setScope . iInsideScope =<< curIF - return $ Recompile m + -- check whether the file needs to be recompiled + uptodate <- case mifile of + Nothing -> pure False + Just ifile -> let ofile = moduleFileName opts m in + liftIO =<< isNewerThan <$> ofile <*> pure ifile + if uptodate then do + reportSDoc "agda2hs.compile" 3 $ text "Module " <+> prettyTCM m <+> text " is already up-to-date" + return $ Skip () + else do + reportSDoc "agda2hs.compile" 3 $ text "Compiling module: " <+> prettyTCM m + setScope . iInsideScope =<< curIF + return $ Recompile m -- Main compile function diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs index 6d785463..de2017a2 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/src/Agda2Hs/Compile/Utils.hs @@ -10,9 +10,12 @@ import Control.Monad.State ( put, modify ) import Data.Maybe ( isJust ) import qualified Data.Map as M +import System.FilePath ( () ) + import qualified Language.Haskell.Exts as Hs import Agda.Compiler.Backend hiding ( Args ) +import Agda.Compiler.Common ( compileDir ) import Agda.Syntax.Common import qualified Agda.Syntax.Concrete.Name as C @@ -20,6 +23,7 @@ import Agda.Syntax.Internal import Agda.Syntax.Position ( noRange ) import Agda.Syntax.Scope.Base import Agda.Syntax.Scope.Monad ( bindVariable, freshConcreteName, isDatatypeModule ) +import Agda.Syntax.TopLevelModuleName import Agda.Syntax.Common.Pretty ( prettyShow ) import qualified Agda.Syntax.Common.Pretty as P @@ -192,6 +196,12 @@ dropClassModule m@(MName ns) = isClassModule m >>= \case True -> dropClassModule $ MName $ init ns False -> return m +-- Gets the path of the Haskell file to be generated +moduleFileName :: Options -> TopLevelModuleName -> TCM FilePath +moduleFileName opts name = do + outDir <- compileDir + return $ fromMaybe outDir (optOutDir opts) moduleNameToFileName name "hs" + moduleParametersToDrop :: ModuleName -> C Telescope moduleParametersToDrop mod = do reportSDoc "agda2hs.moduleParameters" 25 $ text "Getting telescope for" <+> prettyTCM mod diff --git a/src/Agda2Hs/Render.hs b/src/Agda2Hs/Render.hs index 4cd979d2..ab8dc4f3 100644 --- a/src/Agda2Hs/Render.hs +++ b/src/Agda2Hs/Render.hs @@ -9,7 +9,7 @@ import Data.Maybe ( fromMaybe, isNothing ) import Data.Set ( Set ) import qualified Data.Set as Set -import System.FilePath ( takeDirectory, () ) +import System.FilePath ( takeDirectory ) import System.Directory ( createDirectoryIfMissing ) import qualified Language.Haskell.Exts.SrcLoc as Hs @@ -19,7 +19,6 @@ import qualified Language.Haskell.Exts.ExactPrint as Hs import qualified Language.Haskell.Exts.Extension as Hs import Agda.Compiler.Backend -import Agda.Compiler.Common ( compileDir ) import Agda.TypeChecking.Pretty import qualified Agda.Syntax.Concrete.Name as C @@ -32,7 +31,7 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) import Agda2Hs.Compile import Agda2Hs.Compile.Types import Agda2Hs.Compile.Imports -import Agda2Hs.Compile.Utils ( primModules ) +import Agda2Hs.Compile.Utils ( primModules, moduleFileName ) import Agda2Hs.HsUtils import Agda2Hs.Pragma ( getForeignPragmas ) @@ -71,12 +70,6 @@ codeBlocks code = [(r, [uncurry Hs.exactPrint $ moveToTop $ noPragmas mcs]) | (r -- Generating the files ------------------------------------------------------- -moduleFileName :: Options -> TopLevelModuleName -> TCM FilePath -moduleFileName opts name = do - outDir <- compileDir - return $ fromMaybe outDir (optOutDir opts) moduleNameToFileName name "hs" - - ensureDirectory :: FilePath -> IO () ensureDirectory = createDirectoryIfMissing True . takeDirectory