Adding mechanism for skipping up-to-date files

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,14 +19,15 @@ 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 )
 import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma )
 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

src/Agda2Hs/Compile/Utils.hs

@@ -10,16 +10,20 @@ 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
 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

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