------------------------------------------------------------------------
-- 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 #-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4