content: {-# LANGUAGE FlexibleContexts, LambdaCase #-}
  
  module HsToCoq.ProcessFiles (ProcessingMode(..), processFiles) where
  
  import Control.Lens
  
  import Data.Foldable
  import Control.Monad
  import Control.Monad.IO.Class
  
  import qualified Data.Set as S
  
  import System.Directory
  
  import GHC
  
  import HsToCoq.ConvertHaskell.Monad
  import HsToCoq.Util.GHC.Deriving
  
  --------------------------------------------------------------------------------
  
  data ProcessingMode = Recursive | NonRecursive
                      deriving (Eq, Ord, Enum, Bounded, Show, Read)
  
  processFiles :: GlobalMonad r m => ProcessingMode -> [FilePath] -> m (Maybe [TypecheckedModule])
  processFiles mode files = do
    initForDeriving
    traverse_ (addTarget <=< (guessTarget ?? Nothing)) files
    load LoadAllTargets >>= \case
      Succeeded -> Just <$> do
        filterModules <- case mode of
          Recursive    -> pure pure
          NonRecursive -> do
            let canonicalizePaths trav = traverse (liftIO . canonicalizePath) trav
            filePaths <- S.fromList . map Just <$> canonicalizePaths files
            let moduleFile = canonicalizePaths . ml_hs_file . ms_location
            pure . filterM $ fmap (`S.member` filePaths) . moduleFile
        traverse (addDerivedInstances <=< typecheckModule <=< parseModule)
          =<< skipModulesBy ms_mod_name
          =<< filterModules . mgModSummaries
          =<< getModuleGraph
      Failed ->
        pure Nothing
  