{-|
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
                                  ibc <- FilePath -> IO Bool
doesFileExist' FilePath
ibcp
                                  return (if ibc
                                          then ibcp
                                          else ibcPath ibcsd False 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
                                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 = ShowS
srcPath FilePath
fp_full
                                let lidrp = ShowS
lsrcPath FilePath
fp_full
                                ibc <- runIO $ doesFileExist' ibcp
                                idr  <- runIO $ doesFileExist' idrp
                                lidr <- runIO $ doesFileExist' lidrp
                                let isrc = if Bool
lidr
                                           then FilePath -> IFileType
LIDR FilePath
lidrp
                                           else FilePath -> IFileType
IDR FilePath
idrp
                                if ibc
                                  then return (IBC ibcp isrc)
                                  else if (idr || lidr)
                                       then return isrc
                                       else findImport ds ibcsd 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
                             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
                             ibc <- runIO $ doesFileExist' ibcp
                             if ibc
                                then return $ Just ibcp
                                else findIBC ds ibcsd 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
                          e <- FilePath -> IO Bool
doesFileExist' FilePath
p
                          if e then return p else findInPath ds fp

findPkgIndex :: PkgName -> Idris FilePath
findPkgIndex :: PkgName -> Idris FilePath
findPkgIndex PkgName
p = do let idx :: FilePath
idx = PkgName -> FilePath
pkgIndex PkgName
p
                    ids <- Idris [FilePath]
allImportDirs
                    runIO $ findInPath ids idx


installedPackages :: IO [String]
installedPackages :: IO [FilePath]
installedPackages = do
  idir <- IO FilePath
getIdrisLibDir
  filterM (goodDir idir) =<< dirContents idir
  where
  allFilesInDir :: FilePath -> FilePath -> IO [FilePath]
allFilesInDir FilePath
base FilePath
fp = do
    let fullpath :: FilePath
fullpath = FilePath
base FilePath -> ShowS
</> FilePath
fp
    isDir <- FilePath -> IO Bool
doesDirectoryExist' FilePath
fullpath
    if isDir
      then fmap concat (mapM (allFilesInDir fullpath) =<< dirContents fullpath)
      else return [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 exists <- FilePath -> IO Bool
existsCheck FilePath
name
     if exists
        then do contents <- getDirectoryContents (takeDirectory name)
                return $ (takeFileName name) `elem` contents
        else return False