0 | module Core.Directory

  2 | import Core.Binary

  3 | import Core.Context.Log

  4 | import Core.Options

  6 | import Idris.Version

  8 | import Parser.Unlit

 10 | import Libraries.Data.Version

 11 | import Libraries.Utils.Path

 13 | import Data.SnocList

 15 | import System.Directory

 17 | %default total

 23 | pkgGlobalDirectory : {auto c : Ref Ctxt Defs} -> Core String

 24 | pkgGlobalDirectory =

 25 |   do d <- getDirs

 26 |      pure (prefix_dir d </> "idris2-" ++ showVersion False version)

 29 | pkgLocalDirectory : {auto c : Ref Ctxt Defs} -> Core String

 30 | pkgLocalDirectory =

 31 |   do d <- getDirs

 32 |      Just srcdir <- coreLift currentDir

 33 |        | Nothing => throw (InternalError "Can't get current directory")

 34 |      pure $ srcdir </> depends_dir d

 40 | ttcBuildDirectory : {auto c : Ref Ctxt Defs} -> Core String

 41 | ttcBuildDirectory =

 42 |   do d <- getDirs

 43 |      pure (build_dir d </> "ttc" </> show ttcVersion)

 46 | libInstallDirectory : {auto c : Ref Ctxt Defs} -> String -> Core String

 47 | libInstallDirectory lib =

 48 |   do gbdir <- pkgGlobalDirectory

 49 |      pure (gbdir </> lib)

 52 | ttcInstallDirectory : {auto c : Ref Ctxt Defs} -> String -> Core String

 53 | ttcInstallDirectory lib =

 54 |   do libDir <- libInstallDirectory lib

 55 |      pure (libDir </> show ttcVersion)

 58 | srcInstallDirectory : {auto c : Ref Ctxt Defs} -> String -> Core String

 59 | srcInstallDirectory = libInstallDirectory

 62 | extraSearchDirectories : {auto c : Ref Ctxt Defs} -> Core (List String)

 63 | extraSearchDirectories =

 64 |   do d <- getDirs

 65 |      pure (map (</> show ttcVersion) (extra_dirs d ++ package_dirs d))

 69 | public export

 70 | data IdrSrcExt = E_idr | E_lidr | E_yaff | E_org | E_md

 72 | public export

 73 | Eq IdrSrcExt where

 74 |   E_idr  == E_idr  = True

 75 |   E_lidr == E_lidr = True

 76 |   E_yaff == E_yaff = True

 77 |   E_org  == E_org  = True

 78 |   E_md   == E_md   = True

 79 |   _      == _      = False

 81 | public export

 82 | Show IdrSrcExt where

 83 |   show E_idr  = "idr"

 84 |   show E_lidr = "lidr"

 85 |   show E_yaff = "yaff"

 86 |   show E_org  = "org"

 87 |   show E_md   = "md"

 90 | public export

 91 | listOfExtensions : List IdrSrcExt

 92 | listOfExtensions = [E_idr, E_lidr, E_yaff, E_org, E_md]

 98 | public export

 99 | listOfExtensionsStr : List String

100 | listOfExtensionsStr = listOfExtensionsLiterate ++ [".yaff", ".idr"]

105 | collapseSpecialDirs : SnocList Body -> SnocList Body

106 | collapseSpecialDirs path@(xs :< ParentDir) =

107 |   case collapseSpecialDirs xs of

108 |     xs :< CurDir   => xs

109 |     xs :< Normal _ => xs

110 |     _ => path

111 | collapseSpecialDirs (xs :< CurDir) = collapseSpecialDirs xs

112 | collapseSpecialDirs (xs :< Normal n) = collapseSpecialDirs xs :< Normal n

113 | collapseSpecialDirs [<] = [<]

116 | cleanPath : String -> String

117 | cleanPath = show . the (Path -> Path) { hasTrailSep := False, body $= cast . collapseSpecialDirs . cast } . parse

123 | splitIdrisFileName : String -> Maybe (String, String)

124 | splitIdrisFileName fname

125 |     = hasLitFileExt fname <|> isPureCode

127 |   where

128 |     isPureCode : Maybe (String, String)

129 |     isPureCode

130 |       = let (bname, ext) = splitFileName fname in

131 |         do guard (ext == "idr")

132 |            pure (bname, ".idr")

138 | firstAvailable : {auto c : Ref Ctxt Defs} ->

139 |                  List String -> Core (Maybe String)

140 | firstAvailable [] = pure Nothing

141 | firstAvailable (f :: fs)

142 |     = do log "import.file" 30 $ "Attempting to read " ++ f

143 |          Right ok <- coreLift $ openFile f Read

144 |                | Left err => firstAvailable fs

145 |          coreLift $ closeFile ok

146 |          pure (Just f)

150 | findDataFile : {auto c : Ref Ctxt Defs} ->

151 |                String -> Core String

152 | findDataFile fname

153 |     = do d <- getDirs

154 |          let fs = map (\p => cleanPath $ p </> fname) (data_dirs d)

155 |          Just f <- firstAvailable fs

156 |             | Nothing => throw (InternalError ("Can't find data file " ++ fname ++

157 |                                                " in any of " ++ show fs))

158 |          pure f

162 | readDataFile : {auto c : Ref Ctxt Defs} ->

163 |                String -> Core String

164 | readDataFile fname

165 |     = do f <- findDataFile fname

166 |          Right d <- coreLift $ readFile f

167 |             | Left err => throw (FileErr f err)

168 |          pure d

174 | findLibraryFile : {auto c : Ref Ctxt Defs} ->

175 |                   String -> Core String

176 | findLibraryFile fname

177 |     = do d <- getDirs

178 |          let packageLibs = libDirs (package_dirs d)

179 |          let extraLibs = libDirs (extra_dirs d)

180 |          let fs = map (\p => cleanPath $ p </> fname)

181 |                       (lib_dirs d ++ packageLibs ++ extraLibs)

182 |          Just f <- firstAvailable fs

183 |             | Nothing => throw (InternalError ("Can't find library " ++ fname))

184 |          pure f

185 |     where

186 |       libDirs : List String -> List String

187 |       libDirs = map (\x => x </> "lib")

192 | nsToPath : {auto c : Ref Ctxt Defs} ->

193 |            FC -> ModuleIdent -> Core (Either Error String)

194 | nsToPath loc ns

195 |     = do bdir <- ttcBuildDirectory

196 |          ttcs <- extraSearchDirectories

197 |          let fnameBase = ModuleIdent.toPath ns

198 |          let fs = map (\p => cleanPath $ p </> fnameBase <.> "ttc") (bdir :: ttcs)

199 |          Just f <- firstAvailable fs

200 |             | Nothing => pure (Left (ModuleNotFound loc ns))

201 |          pure (Right f)

206 | nsToSource : {auto c : Ref Ctxt Defs} ->

207 |              FC -> ModuleIdent -> Core String

208 | nsToSource loc ns

209 |     = do d <- getDirs

210 |          let fnameOrig = ModuleIdent.toPath ns

211 |          let fnameBase = cleanPath $ maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)

212 |          let fs = map ((fnameBase ++)) listOfExtensionsStr

213 |          Just f <- firstAvailable fs

214 |             | Nothing => throw (ModuleNotFound loc ns)

215 |          pure f

221 | mbPathToNS : String -> Maybe String -> String -> Maybe ModuleIdent

222 | mbPathToNS wdir sdir fname =

223 |   let

224 |     sdir = fromMaybe "" sdir

225 |     base = if isAbsolute fname then wdir </> sdir else sdir

226 |   in

227 |     unsafeFoldModuleIdent . reverse . splitPath . Path.dropExtensions

228 |       <$> (Path.dropBase `on` cleanPath) base fname

231 | corePathToNS : String -> Maybe String -> String -> Core ModuleIdent

232 | corePathToNS wdir sdir fname = do

233 |   let err = UserError $

234 |           "Source file "

235 |        ++ show (cleanPath fname)

236 |        ++ " is not in the source directory "

237 |        ++ show (cleanPath (wdir </> fromMaybe "" sdir))

238 |   maybe (throw err) pure (mbPathToNS wdir sdir fname)

241 | ctxtPathToNS : {auto c : Ref Ctxt Defs} -> String -> Core ModuleIdent

242 | ctxtPathToNS fname = do

243 |   defs <- get Ctxt

244 |   let wdir = defs.options.dirs.working_dir

245 |   let sdir = defs.options.dirs.source_dir

246 |   corePathToNS wdir sdir fname

248 | dirExists : String -> IO Bool

249 | dirExists dir = do Right d <- openDir dir

250 |                        | Left _ => pure False

251 |                    closeDir d

252 |                    pure True

257 | mkdirAll : String -> IO (Either FileError ())

258 | mkdirAll dir = if parse dir == emptyPath

259 |                   then pure (Right ())

260 |                   else do exist <- dirExists dir

261 |                           if exist

262 |                              then pure (Right ())

263 |                              else do Right () <- case parent dir of

264 |                                           Just parent => mkdirAll parent

265 |                                           Nothing => pure (Right ())

266 |                                         | err => pure err

267 |                                      createDir dir

273 | makeBuildDirectory : {auto c : Ref Ctxt Defs} ->

274 |                      ModuleIdent -> Core ()

275 | makeBuildDirectory ns

276 |     = do bdir <- ttcBuildDirectory

277 |          let ns = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns -- first item is file name

278 |          let ndir = joinPath ns

279 |          Right _ <- coreLift $ mkdirAll (bdir </> ndir)

280 |             | Left err => throw (FileErr (bdir </> ndir) err)

281 |          pure ()

285 | ensureDirectoryExists : String -> Core ()

286 | ensureDirectoryExists dir

287 |     = do Right _ <- coreLift $ mkdirAll dir

288 |             | Left err => throw (FileErr dir err)

289 |          pure ()

293 | getTTCFileName : {auto c : Ref Ctxt Defs} ->

294 |                  String -> String -> Core String

295 | getTTCFileName inp ext

296 |     = do -- Get its namespace from the file relative to the working directory

297 |          -- and generate the ttc file from that

298 |          ns <- ctxtPathToNS inp

299 |          let fname = ModuleIdent.toPath ns <.> ext

300 |          bdir <- ttcBuildDirectory

301 |          pure $ bdir </> fname

306 | getObjFileName : {auto c : Ref Ctxt Defs} ->

307 |                  String -> String -> Core String

308 | getObjFileName inp ext

309 |     = do -- Get its namespace from the file relative to the working directory

310 |          -- and generate the ttc file from that

311 |          ns <- ctxtPathToNS inp

312 |          let fname = ModuleIdent.toPath ns <.> ext

313 |          pure $ fname

317 | getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String

318 | getExecFileName efile

319 |     = do d <- getDirs

320 |          pure $ build_dir d </> efile

327 | findIpkgFile : IO (Maybe (String, String, String))

329 |     = do Just dir <- currentDir

330 |               | Nothing => pure Nothing

331 |          res <- findIpkgFile' dir ""

332 |          pure res

333 |   where

334 |     covering

335 |     findIpkgFile' : String -> String -> IO (Maybe (String, String, String))

336 |     findIpkgFile' dir up

337 |         = do Right files <- listDir dir

338 |                  | Left err => pure Nothing

339 |              let Just f = find (\f => extension f == Just "ipkg") files

340 |                  | Nothing => case splitParent dir of

341 |                                    Just (parent, end) => findIpkgFile' parent (end </> up)

342 |                                    Nothing => pure Nothing

343 |              pure $ Just (dir, f, up)