module System.Directory where

open import Level
open import Codata.IO
open import Data.Unit
open import Data.Bool.Base
open import Data.List.Base
open import Data.Maybe.Base
open import Data.Nat.Base
open import Data.String.Base
open import Foreign.Haskell.Coerce
open import Function
open import System.FilePath.Posix hiding (makeRelative)

open import System.Directory.Primitive as Prim
  using ( XdgDirectory
        ; XdgData
        ; XdgConfig
        ; XdgCache
        ; XdgDirectoryList
        ; XdgDataDirs
        ; XdgConfigDirs
        ; exeExtension
        ) public

variable
    : Level
  m n : Nature

-- Actions on directories

createDirectory           : FilePath n  IO  
createDirectoryIfMissing  : Bool  FilePath n  IO  
removeDirectory           : FilePath n  IO  
removeDirectoryRecursive  : FilePath n  IO  
removePathForcibly        : FilePath n  IO  
renameDirectory           : FilePath n  FilePath n  IO  
listDirectory             : FilePath n  IO  (List RelativePath)

-- Current working directory

getDirectoryContents      : FilePath n  IO  (List RelativePath)
getCurrentDirectory       : IO  AbsolutePath
setCurrentDirectory       : FilePath n  IO  
withCurrentDirectory      :  {a} {A : Set a}  {{a ≤ˡ }}  FilePath n  IO  A  IO  A

-- Pre-defined directories

getHomeDirectory          : IO  AbsolutePath
getXdgDirectory           : XdgDirectory  RelativePath  IO  AbsolutePath
getXdgDirectoryList       : XdgDirectoryList  IO  (List AbsolutePath)
getAppUserDataDirectory   : RelativePath  IO  AbsolutePath
getUserDocumentsDirectory : IO  AbsolutePath
getTemporaryDirectory     : IO  AbsolutePath

-- Action on files
removeFile           : FilePath m  IO  
renameFile           : FilePath m  FilePath n  IO  
renamePath           : FilePath m  FilePath n  IO  
copyFile             : FilePath m  FilePath n  IO  
copyFileWithMetadata : FilePath m  FilePath n  IO  
getFileSize          : FilePath n  IO  
canonicalizePath     : FilePath n  IO  AbsolutePath
makeAbsolute         : FilePath n  IO  AbsolutePath
makeRelative         : FilePath n  IO  RelativePath

toKnownNature : KnownNature m  FilePath n  IO  (FilePath m)
toKnownNature absolute = makeAbsolute
toKnownNature relative = makeRelative

relativeToKnownNature : KnownNature n  RelativePath  IO  (FilePath n)
absoluteToKnownNature : KnownNature n  AbsolutePath  IO  (FilePath n)

relativeToKnownNature absolute = makeAbsolute
relativeToKnownNature relative = pure

absoluteToKnownNature absolute = pure
absoluteToKnownNature relative = makeRelative

-- Existence tests

doesPathExist                : FilePath n -> IO  Bool
doesFileExist                : FilePath n -> IO  Bool
doesDirectoryExist           : FilePath n -> IO  Bool
findExecutable               : String  IO  (Maybe AbsolutePath)
findExecutables              : String  IO  (List AbsolutePath)
findExecutablesInDirectories : List (FilePath n)  String  IO  (List (FilePath n))
findFile                     : List (FilePath n)  String  IO  (Maybe (FilePath n))
findFiles                    : List (FilePath n)  String  IO  (List (FilePath n))
findFileWith                 : (FilePath n  IO  Bool)  List (FilePath n)  String  IO  (Maybe (FilePath n))
findFilesWith                : (FilePath n  IO  Bool)  List (FilePath n)  String  IO  (List (FilePath n))

-- Symbolic links

createFileLink        : FilePath m  FilePath n  IO  
createDirectoryLink   : FilePath m  FilePath n  IO  
removeDirectoryLink   : FilePath n  IO  
pathIsSymbolicLink    : FilePath n  IO  Bool
getSymbolicLinkTarget : FilePath n  IO  SomePath





createDirectory          = lift ∘′ Prim.createDirectory
createDirectoryIfMissing = λ b  lift ∘′ Prim.createDirectoryIfMissing b
removeDirectory          = lift ∘′ Prim.removeDirectory
removeDirectoryRecursive = lift ∘′ Prim.removeDirectoryRecursive
removePathForcibly       = lift ∘′ Prim.removePathForcibly
renameDirectory          = λ fp  lift ∘′ Prim.renameDirectory fp
listDirectory            = lift ∘′ Prim.listDirectory
getDirectoryContents     = lift ∘′ Prim.getDirectoryContents

getCurrentDirectory  = lift Prim.getCurrentDirectory
setCurrentDirectory  = lift ∘′ Prim.setCurrentDirectory
withCurrentDirectory = λ fp ma  lift (Prim.withCurrentDirectory fp (run ma))

getHomeDirectory          = lift Prim.getHomeDirectory
getXdgDirectory           = λ d fp  lift (Prim.getXdgDirectory d fp)
getXdgDirectoryList       = lift ∘′ Prim.getXdgDirectoryList
getAppUserDataDirectory   = lift ∘′ Prim.getAppUserDataDirectory
getUserDocumentsDirectory = lift Prim.getUserDocumentsDirectory
getTemporaryDirectory     = lift Prim.getTemporaryDirectory

removeFile           = lift ∘′ Prim.removeFile
renameFile           = λ a b  lift (Prim.renameFile a b)
renamePath           = λ a b  lift (Prim.renamePath a b)
copyFile             = λ a b  lift (Prim.copyFile a b)
copyFileWithMetadata = λ a b  lift (Prim.copyFileWithMetadata a b)
getFileSize          = lift ∘′ Prim.getFileSize
canonicalizePath     = lift ∘′ Prim.canonicalizePath
makeAbsolute         = lift ∘′ Prim.makeAbsolute
makeRelative         = lift ∘′ Prim.makeRelativeToCurrentDirectory

doesPathExist                = lift ∘′ Prim.doesPathExist
doesFileExist                = lift ∘′ Prim.doesFileExist
doesDirectoryExist           = lift ∘′ Prim.doesDirectoryExist
findExecutable               = lift ∘′ coerce ∘′ Prim.findExecutable
findExecutables              = lift ∘′ Prim.findExecutables
findExecutablesInDirectories = λ fps str  lift (Prim.findExecutablesInDirectories fps str)
findFile                     = λ fps str  lift (coerce Prim.findFile fps str)
findFiles                    = λ fps str  lift (Prim.findFiles fps str)
findFileWith                 = λ p fps str  lift (coerce Prim.findFileWith (run ∘′ p) fps str)
findFilesWith                = λ p fps str  lift (Prim.findFilesWith (run ∘′ p) fps str)

createFileLink        = λ fp  lift ∘′ Prim.createFileLink fp
createDirectoryLink   = λ fp  lift ∘′ Prim.createDirectoryLink fp
removeDirectoryLink   = lift ∘′ Prim.removeDirectoryLink
pathIsSymbolicLink    = lift ∘′ Prim.pathIsSymbolicLink
getSymbolicLinkTarget = lift ∘′ Prim.getSymbolicLinkTarget