    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Primitive System.Direcotry simple bindings to Haskell functions
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --guardedness #-}

    module System.Directory.Primitive where

    open import Agda.Builtin.Unit using (⊤)
    open import Agda.Builtin.Bool using (Bool)
    open import Agda.Builtin.IO using (IO)
    open import Agda.Builtin.List using (List)
    open import Agda.Builtin.Maybe using (Maybe)
    open import Agda.Builtin.Nat using (Nat)
    open import Agda.Builtin.String using (String)
    open import System.FilePath.Posix.Primitive

    {-# FOREIGN GHC import System.Directory #-}
    {-# FOREIGN GHC import Data.Text        #-}

    data XdgDirectory : Set where
      XdgData XdgConfig XdgCache XdgState : XdgDirectory

    data XdgDirectoryList : Set where
      XdgDataDirs XdgConfigDirs : XdgDirectoryList

    {-# COMPILE GHC XdgDirectory     = data XdgDirectory (XdgData|XdgConfig|XdgCache|XdgState) #-}
    {-# COMPILE GHC XdgDirectoryList = data XdgDirectoryList (XdgDataDirs|XdgConfigDirs) #-}

    private
      variable
        m n : Nature

    postulate

      -- 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 m → FilePath n → IO ⊤
      listDirectory            : FilePath n → IO (List RelativePath)
      getDirectoryContents     : FilePath n → IO (List RelativePath)

      -- Current working directory

      getCurrentDirectory  : IO AbsolutePath
      setCurrentDirectory  : FilePath n → IO ⊤
      withCurrentDirectory : ∀ {a} {A : Set 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

      -- Actions 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 Nat
      canonicalizePath               : FilePath n → IO AbsolutePath
      makeAbsolute                   : FilePath n → IO AbsolutePath
      makeRelativeToCurrentDirectory : FilePath n → IO RelativePath

      -- 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))
      exeExtension                 : String

      -- 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

    {-# COMPILE GHC createDirectory          = const createDirectory          #-}
    {-# COMPILE GHC createDirectoryIfMissing = const createDirectoryIfMissing #-}
    {-# COMPILE GHC removeDirectory          = const removeDirectory          #-}
    {-# COMPILE GHC removeDirectoryRecursive = const removeDirectoryRecursive #-}
    {-# COMPILE GHC removePathForcibly       = const removePathForcibly       #-}
    {-# COMPILE GHC renameDirectory          = \ _ _ -> renameDirectory       #-}
    {-# COMPILE GHC listDirectory            = const listDirectory            #-}
    {-# COMPILE GHC getDirectoryContents     = const getDirectoryContents     #-}

    {-# COMPILE GHC getCurrentDirectory  = getCurrentDirectory             #-}
    {-# COMPILE GHC setCurrentDirectory  = const setCurrentDirectory       #-}
    {-# COMPILE GHC withCurrentDirectory = \ _ _ _ -> withCurrentDirectory #-}

    {-# COMPILE GHC getHomeDirectory          = getHomeDirectory          #-}
    {-# COMPILE GHC getXdgDirectory           = getXdgDirectory           #-}
    {-# COMPILE GHC getXdgDirectoryList       = getXdgDirectoryList       #-}
    {-# COMPILE GHC getAppUserDataDirectory   = getAppUserDataDirectory   #-}
    {-# COMPILE GHC getUserDocumentsDirectory = getUserDocumentsDirectory #-}
    {-# COMPILE GHC getTemporaryDirectory     = getTemporaryDirectory     #-}

    {-# COMPILE GHC removeFile                     = const removeFile                     #-}
    {-# COMPILE GHC renameFile                     = \ _ _ -> renameFile                  #-}
    {-# COMPILE GHC renamePath                     = \ _ _ -> renamePath                  #-}
    {-# COMPILE GHC copyFile                       = \ _ _ -> copyFile                    #-}
    {-# COMPILE GHC copyFileWithMetadata           = \ _ _ -> copyFileWithMetadata        #-}
    {-# COMPILE GHC getFileSize                    = const getFileSize                    #-}
    {-# COMPILE GHC canonicalizePath               = const canonicalizePath               #-}
    {-# COMPILE GHC makeAbsolute                   = const makeAbsolute                   #-}
    {-# COMPILE GHC makeRelativeToCurrentDirectory = const makeRelativeToCurrentDirectory #-}

    {-# COMPILE GHC doesPathExist                = const doesPathExist                                  #-}
    {-# COMPILE GHC doesFileExist                = const doesFileExist                                  #-}
    {-# COMPILE GHC doesDirectoryExist           = const doesDirectoryExist                             #-}
    {-# COMPILE GHC findExecutable               = findExecutable . unpack                              #-}
    {-# COMPILE GHC findExecutables              = findExecutables . unpack                             #-}
    {-# COMPILE GHC findExecutablesInDirectories = \ _ fps -> findExecutablesInDirectories fps . unpack #-}
    {-# COMPILE GHC findFile                     = \ _ fps -> findFile fps . unpack                     #-}
    {-# COMPILE GHC findFiles                    = \ _ fps -> findFiles fps . unpack                    #-}
    {-# COMPILE GHC findFileWith                 = \ _ p fps -> findFileWith p fps . unpack             #-}
    {-# COMPILE GHC findFilesWith                = \ _ p fps -> findFilesWith p fps . unpack            #-}
    {-# COMPILE GHC exeExtension                 = pack exeExtension                                    #-}

    {-# COMPILE GHC createFileLink        = \ _ _ -> createFileLink      #-}
    {-# COMPILE GHC createDirectoryLink   = \ _ _ -> createDirectoryLink #-}
    {-# COMPILE GHC removeDirectoryLink   = const removeDirectoryLink    #-}
    {-# COMPILE GHC pathIsSymbolicLink    = const pathIsSymbolicLink     #-}
    {-# COMPILE GHC getSymbolicLinkTarget = const getSymbolicLinkTarget  #-}