{-|
Module      : Idris.Imports
Description : Code to handle import declarations.

License     : BSD3
Maintainer  : The Idris Community.
-}
module Idris.Imports(
    IFileType(..), findIBC, findImport, findInPath, findPkgIndex
  , ibcPathNoFallback, installedPackages, pkgIndex
  , PkgName, pkgName, unPkgName, unInitializedPkgName
  ) where

import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Error
import IRTS.System (getIdrisLibDir)

import Control.Monad
import Control.Monad.State.Strict
import Data.Char (isAlpha, isDigit, toLower)
import Data.List (isSuffixOf)
import System.Directory
import System.FilePath

data IFileType = IDR FilePath | LIDR FilePath | IBC FilePath IFileType
    deriving (Int -> IFileType -> ShowS
[IFileType] -> ShowS
IFileType -> FilePath
(Int -> IFileType -> ShowS)
-> (IFileType -> FilePath)
-> ([IFileType] -> ShowS)
-> Show IFileType
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IFileType -> ShowS
showsPrec :: Int -> IFileType -> ShowS
$cshow :: IFileType -> FilePath
show :: IFileType -> FilePath
$cshowList :: [IFileType] -> ShowS
showList :: [IFileType] -> ShowS
Show, Eq IFileType
Eq IFileType =>
(IFileType -> IFileType -> Ordering)
-> (IFileType -> IFileType -> Bool)
-> (IFileType -> IFileType -> Bool)
-> (IFileType -> IFileType -> Bool)
-> (IFileType -> IFileType -> Bool)
-> (IFileType -> IFileType -> IFileType)
-> (IFileType -> IFileType -> IFileType)
-> Ord IFileType
IFileType -> IFileType -> Bool
IFileType -> IFileType -> Ordering
IFileType -> IFileType -> IFileType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: IFileType -> IFileType -> Ordering
compare :: IFileType -> IFileType -> Ordering
$c< :: IFileType -> IFileType -> Bool
< :: IFileType -> IFileType -> Bool
$c<= :: IFileType -> IFileType -> Bool
<= :: IFileType -> IFileType -> Bool
$c> :: IFileType -> IFileType -> Bool
> :: IFileType -> IFileType -> Bool
$c>= :: IFileType -> IFileType -> Bool
>= :: IFileType -> IFileType -> Bool
$cmax :: IFileType -> IFileType -> IFileType
max :: IFileType -> IFileType -> IFileType
$cmin :: IFileType -> IFileType -> IFileType
min :: IFileType -> IFileType -> IFileType
Ord)

instance Eq IFileType where
    IDR FilePath
x == :: IFileType -> IFileType -> Bool
== IDR FilePath
y = FilePath
x FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
y
    LIDR FilePath
x == LIDR FilePath
y = FilePath
x FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
y
    IBC FilePath
x IFileType
_ == IBC FilePath
y IFileType
_ = FilePath
x FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
y
    IFileType
_ == IFileType
_ = Bool
False

newtype PkgName = PkgName String

unPkgName :: PkgName -> String
unPkgName :: PkgName -> FilePath
unPkgName (PkgName FilePath
s) = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower FilePath
s

instance Show PkgName where
    show :: PkgName -> FilePath
show (PkgName FilePath
pkg) = FilePath
pkg
instance Eq PkgName where
    PkgName
a == :: PkgName -> PkgName -> Bool
== PkgName
b = PkgName -> FilePath
unPkgName PkgName
a FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== PkgName -> FilePath
unPkgName PkgName
b

unInitializedPkgName :: PkgName
unInitializedPkgName :: PkgName
unInitializedPkgName = FilePath -> PkgName
PkgName FilePath
""

pkgName :: String -> Either String PkgName
pkgName :: FilePath -> Either FilePath PkgName
pkgName FilePath
""      = FilePath -> Either FilePath PkgName
forall a b. a -> Either a b
Left FilePath
"empty package name"
pkgName s :: FilePath
s@(Char
f:FilePath
l)
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Char -> Bool
isAlpha Char
f =
        FilePath -> Either FilePath PkgName
forall a b. a -> Either a b
Left FilePath
"package name need to start by a letter"
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Char
c -> Char -> Bool
isAlpha Char
c Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> FilePath -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FilePath
"-_") FilePath
l =
        FilePath -> Either FilePath PkgName
forall a b. a -> Either a b
Left FilePath
"package name need to contain only letter, digits, and -_"
    | Bool
otherwise = PkgName -> Either FilePath PkgName
forall a b. b -> Either a b
Right (PkgName -> Either FilePath PkgName)
-> PkgName -> Either FilePath PkgName
forall a b. (a -> b) -> a -> b
$ FilePath -> PkgName
PkgName FilePath
s

-- | Get the index file name for a package name
pkgIndex :: PkgName -> FilePath
pkgIndex :: PkgName -> FilePath
pkgIndex PkgName
s = FilePath
"00" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ PkgName -> FilePath
unPkgName PkgName
s FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"-idx.ibc"

srcPath :: FilePath -> FilePath
srcPath :: ShowS
srcPath FilePath
fp = let (FilePath
_, FilePath
ext) = FilePath -> (FilePath, FilePath)
splitExtension FilePath
fp in
                 case FilePath
ext of
                    FilePath
".idr" -> FilePath
fp
                    FilePath
_ -> FilePath
fp FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
".idr"

lsrcPath :: FilePath -> FilePath
lsrcPath :: ShowS
lsrcPath FilePath
fp = let (FilePath
_, FilePath
ext) = FilePath -> (FilePath, FilePath)
splitExtension FilePath
fp in
                  case FilePath
ext of
                     FilePath
".lidr" -> FilePath
fp
                     FilePath
_ -> FilePath
fp FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
".lidr"

-- Get name of byte compiled version of an import
ibcPath :: FilePath -> Bool -> FilePath -> FilePath
ibcPath :: FilePath -> Bool -> ShowS
ibcPath FilePath
ibcsd Bool
use_ibcsd FilePath
fp = let (FilePath
d_fp, FilePath
n_fp) = FilePath -> (FilePath, FilePath)
splitFileName FilePath
fp
                                 d :: FilePath
d = if (Bool -> Bool
not Bool
use_ibcsd) Bool -> Bool -> Bool
|| FilePath
ibcsd FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
""
                                     then FilePath
d_fp
                                     else FilePath
ibcsd FilePath -> ShowS
</> FilePath
d_fp
                                 n :: FilePath
n = ShowS
dropExtension FilePath
n_fp
                             in FilePath
d FilePath -> ShowS
</> FilePath
n FilePath -> ShowS
<.> FilePath
"ibc"

ibcPathWithFallback :: FilePath -> FilePath -> IO FilePath
ibcPathWithFallback :: FilePath -> FilePath -> IO FilePath
ibcPathWithFallback FilePath
ibcsd FilePath
fp = do let ibcp :: FilePath
ibcp = FilePath -> Bool -> ShowS
ibcPath FilePath
ibcsd Bool
True FilePath
fp
                                  Bool
ibc <- FilePath -> IO Bool
doesFileExist' FilePath
ibcp
                                  FilePath -> IO FilePath
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Bool
ibc
                                          then FilePath
ibcp
                                          else FilePath -> Bool -> ShowS
ibcPath FilePath
ibcsd Bool
False FilePath
fp)

ibcPathNoFallback :: FilePath -> FilePath -> FilePath
ibcPathNoFallback :: FilePath -> ShowS
ibcPathNoFallback FilePath
ibcsd FilePath
fp = FilePath -> Bool -> ShowS
ibcPath FilePath
ibcsd Bool
True FilePath
fp

findImport :: [FilePath] -> FilePath -> FilePath -> Idris IFileType
findImport :: [FilePath] -> FilePath -> FilePath -> Idris IFileType
findImport []     FilePath
ibcsd FilePath
fp = Err -> Idris IFileType
forall a. Err -> Idris a
ierror (Err -> Idris IFileType)
-> (FilePath -> Err) -> FilePath -> Idris IFileType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Err
forall t. FilePath -> Err' t
Msg (FilePath -> Idris IFileType) -> FilePath -> Idris IFileType
forall a b. (a -> b) -> a -> b
$ FilePath
"Can't find import " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
fp
findImport (FilePath
d:[FilePath]
ds) FilePath
ibcsd FilePath
fp = do let fp_full :: FilePath
fp_full = FilePath
d FilePath -> ShowS
</> FilePath
fp
                                FilePath
ibcp <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO FilePath
ibcPathWithFallback FilePath
ibcsd FilePath
fp_full
                                let idrp :: FilePath
idrp = ShowS
srcPath FilePath
fp_full
                                let lidrp :: FilePath
lidrp = ShowS
lsrcPath FilePath
fp_full
                                Bool
ibc <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Bool
doesFileExist' FilePath
ibcp
                                Bool
idr  <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Bool
doesFileExist' FilePath
idrp
                                Bool
lidr <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Bool
doesFileExist' FilePath
lidrp
                                let isrc :: IFileType
isrc = if Bool
lidr
                                           then FilePath -> IFileType
LIDR FilePath
lidrp
                                           else FilePath -> IFileType
IDR FilePath
idrp
                                if Bool
ibc
                                  then IFileType -> Idris IFileType
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> IFileType -> IFileType
IBC FilePath
ibcp IFileType
isrc)
                                  else if (Bool
idr Bool -> Bool -> Bool
|| Bool
lidr)
                                       then IFileType -> Idris IFileType
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IFileType
isrc
                                       else [FilePath] -> FilePath -> FilePath -> Idris IFileType
findImport [FilePath]
ds FilePath
ibcsd FilePath
fp

-- Only look for IBCs and not source
findIBC :: [FilePath] -> FilePath -> FilePath -> Idris (Maybe FilePath)
findIBC :: [FilePath] -> FilePath -> FilePath -> Idris (Maybe FilePath)
findIBC [] FilePath
_ FilePath
fp = Maybe FilePath -> Idris (Maybe FilePath)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FilePath
forall a. Maybe a
Nothing
findIBC (FilePath
d:[FilePath]
ds) FilePath
ibcsd FilePath
fp = do let fp_full :: FilePath
fp_full = FilePath
d FilePath -> ShowS
</> FilePath
fp
                             FilePath
ibcp <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO FilePath
ibcPathWithFallback FilePath
ibcsd FilePath
fp_full
                             Bool
ibc <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Bool
doesFileExist' FilePath
ibcp
                             if Bool
ibc
                                then Maybe FilePath -> Idris (Maybe FilePath)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath -> Idris (Maybe FilePath))
-> Maybe FilePath -> Idris (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
ibcp
                                else [FilePath] -> FilePath -> FilePath -> Idris (Maybe FilePath)
findIBC [FilePath]
ds FilePath
ibcsd FilePath
fp


-- find a specific filename somewhere in a path

findInPath :: [FilePath] -> FilePath -> IO FilePath
findInPath :: [FilePath] -> FilePath -> IO FilePath
findInPath [] FilePath
fp = FilePath -> IO FilePath
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"Can't find file " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
fp
findInPath (FilePath
d:[FilePath]
ds) FilePath
fp = do let p :: FilePath
p = FilePath
d FilePath -> ShowS
</> FilePath
fp
                          Bool
e <- FilePath -> IO Bool
doesFileExist' FilePath
p
                          if Bool
e then FilePath -> IO FilePath
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
p else [FilePath] -> FilePath -> IO FilePath
findInPath [FilePath]
ds FilePath
fp

findPkgIndex :: PkgName -> Idris FilePath
findPkgIndex :: PkgName -> Idris FilePath
findPkgIndex PkgName
p = do let idx :: FilePath
idx = PkgName -> FilePath
pkgIndex PkgName
p
                    [FilePath]
ids <- Idris [FilePath]
allImportDirs
                    IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath -> IO FilePath
findInPath [FilePath]
ids FilePath
idx


installedPackages :: IO [String]
installedPackages :: IO [FilePath]
installedPackages = do
  FilePath
idir <- IO FilePath
getIdrisLibDir
  (FilePath -> IO Bool) -> [FilePath] -> IO [FilePath]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (FilePath -> FilePath -> IO Bool
goodDir FilePath
idir) ([FilePath] -> IO [FilePath]) -> IO [FilePath] -> IO [FilePath]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO [FilePath]
dirContents FilePath
idir
  where
  allFilesInDir :: FilePath -> FilePath -> IO [FilePath]
allFilesInDir FilePath
base FilePath
fp = do
    let fullpath :: FilePath
fullpath = FilePath
base FilePath -> ShowS
</> FilePath
fp
    Bool
isDir <- FilePath -> IO Bool
doesDirectoryExist' FilePath
fullpath
    if Bool
isDir
      then ([[FilePath]] -> [FilePath]) -> IO [[FilePath]] -> IO [FilePath]
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[FilePath]] -> [FilePath]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((FilePath -> IO [FilePath]) -> [FilePath] -> IO [[FilePath]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FilePath -> FilePath -> IO [FilePath]
allFilesInDir FilePath
fullpath) ([FilePath] -> IO [[FilePath]]) -> IO [FilePath] -> IO [[FilePath]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO [FilePath]
dirContents FilePath
fullpath)
      else [FilePath] -> IO [FilePath]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [FilePath
fp]
  dirContents :: FilePath -> IO [FilePath]
dirContents = ([FilePath] -> [FilePath]) -> IO [FilePath] -> IO [FilePath]
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FilePath -> Bool) -> [FilePath] -> [FilePath]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath
".", FilePath
".."]))) (IO [FilePath] -> IO [FilePath])
-> (FilePath -> IO [FilePath]) -> FilePath -> IO [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO [FilePath]
getDirectoryContents
  goodDir :: FilePath -> FilePath -> IO Bool
goodDir FilePath
idir FilePath
d = (FilePath -> Bool) -> [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath
".ibc" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf`) ([FilePath] -> Bool) -> IO [FilePath] -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> FilePath -> IO [FilePath]
allFilesInDir FilePath
idir FilePath
d


-- | Case sensitive file existence check for Mac OS X.
doesFileExist' :: FilePath -> IO Bool
doesFileExist' :: FilePath -> IO Bool
doesFileExist' = (FilePath -> IO Bool) -> FilePath -> IO Bool
caseSensitive FilePath -> IO Bool
doesFileExist

-- | Case sensitive directory existence check for Mac OS X.
doesDirectoryExist' :: FilePath -> IO Bool
doesDirectoryExist' :: FilePath -> IO Bool
doesDirectoryExist' = (FilePath -> IO Bool) -> FilePath -> IO Bool
caseSensitive FilePath -> IO Bool
doesDirectoryExist

caseSensitive :: (FilePath -> IO Bool) -> FilePath -> IO Bool
caseSensitive :: (FilePath -> IO Bool) -> FilePath -> IO Bool
caseSensitive FilePath -> IO Bool
existsCheck FilePath
name =
  do Bool
exists <- FilePath -> IO Bool
existsCheck FilePath
name
     if Bool
exists
        then do [FilePath]
contents <- FilePath -> IO [FilePath]
getDirectoryContents (ShowS
takeDirectory FilePath
name)
                Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ (ShowS
takeFileName FilePath
name) FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
contents
        else Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False