summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Monad/Options.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Monad/Options.hs')
-rw-r--r--src/full/Agda/TypeChecking/Monad/Options.hs29
1 files changed, 17 insertions, 12 deletions
diff --git a/src/full/Agda/TypeChecking/Monad/Options.hs b/src/full/Agda/TypeChecking/Monad/Options.hs
index c7821d5..be45881 100644
--- a/src/full/Agda/TypeChecking/Monad/Options.hs
+++ b/src/full/Agda/TypeChecking/Monad/Options.hs
@@ -1,19 +1,21 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
module Agda.TypeChecking.Monad.Options where
+import Prelude hiding (mapM)
+
import Control.Applicative
-import Control.Monad.Reader
-import Control.Monad.State
+import Control.Monad.Reader hiding (mapM)
+import Control.Monad.State hiding (mapM)
+
import Data.Maybe
+import Data.Traversable
+
import Text.PrettyPrint
import System.Directory
import System.FilePath
-import Paths_Agda (getDataFileName)
--- NB: find Paths_Agda.hs in dist/build/autogen/
-
import Agda.Syntax.Concrete
import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.Base
@@ -25,6 +27,7 @@ import Agda.Interaction.Response
import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.FileName
+import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Lens
import Agda.Utils.List
@@ -182,7 +185,7 @@ setIncludeDirs incs relativeTo = do
incs <- return $ map (mkAbsolute . (filePath root </>)) incs
-- Andreas, 2013-10-30 Add default include dir
- libdir <- liftIO $ getDataFileName ("lib")
+ libdir <- liftIO $ defaultLibDir
-- NB: This is an absolute file name, but
-- Agda.Utils.FilePath wants to check absoluteness anyway.
let primdir = mkAbsolute $ libdir </> "prim"
@@ -216,11 +219,13 @@ setInputFile file =
-- | Should only be run if 'hasInputFile'.
getInputFile :: TCM AbsolutePath
-getInputFile =
- do mf <- optInputFile <$> commandLineOptions
- case mf of
- Just file -> liftIO $ absolute file
- Nothing -> __IMPOSSIBLE__
+getInputFile = fromMaybeM __IMPOSSIBLE__ $
+ getInputFile'
+
+-- | Return the 'optInputFile' as 'AbsolutePath', if any.
+getInputFile' :: TCM (Maybe AbsolutePath)
+getInputFile' = mapM (liftIO . absolute) =<< do
+ optInputFile <$> commandLineOptions
hasInputFile :: TCM Bool
hasInputFile = isJust <$> optInputFile <$> commandLineOptions