{-|
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.Applicative ((<$>))
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 -> String
(Int -> IFileType -> ShowS)
-> (IFileType -> String)
-> ([IFileType] -> ShowS)
-> Show IFileType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IFileType] -> ShowS
$cshowList :: [IFileType] -> ShowS
show :: IFileType -> String
$cshow :: IFileType -> String
showsPrec :: Int -> IFileType -> ShowS
$cshowsPrec :: Int -> 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
min :: IFileType -> IFileType -> IFileType
$cmin :: IFileType -> IFileType -> IFileType
max :: IFileType -> IFileType -> IFileType
$cmax :: IFileType -> IFileType -> IFileType
>= :: IFileType -> IFileType -> Bool
$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
compare :: IFileType -> IFileType -> Ordering
$ccompare :: IFileType -> IFileType -> Ordering
$cp1Ord :: Eq IFileType
Ord)

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

newtype PkgName = PkgName String

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

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

unInitializedPkgName :: PkgName
unInitializedPkgName :: PkgName
unInitializedPkgName = String -> PkgName
PkgName ""

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

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

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

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

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

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

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

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

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


-- find a specific filename somewhere in a path

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

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


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


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

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

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