------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive System.FilePath.Posix simple bindings to Haskell functions
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --guardedness #-}
module System.FilePath.Posix.Primitive where
open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.Char using (Char)
open import Agda.Builtin.List using (List)
open import Agda.Builtin.Maybe using (Maybe)
open import Agda.Builtin.String using (String)
open import Foreign.Haskell as FFI using (Pair; Either)
open import IO.Primitive.Core using (IO)
-- A filepath has a nature: it can be either relative or absolute.
-- We postulate this nature rather than defining it as an inductive
-- type so that the user cannot inspect it. The only way to cast an
-- arbitrary filepath nature @n@ to either @relative@ or @absolute@
-- is to use @checkFilePath@.
module Nature where
postulate
Nature : Set
relative absolute unknown : Nature
-- In the Haskell backend these @natures@ are simply erased as the
-- libraries represent all filepaths in the same way.
{-# FOREIGN GHC import Data.Kind #-}
{-# COMPILE GHC Nature = type Type #-}
{-# COMPILE GHC relative = type () #-}
{-# COMPILE GHC absolute = type () #-}
{-# COMPILE GHC unknown = type () #-}
open Nature using (Nature) public
private
variable
m n : Nature
postulate
FilePath : Nature → Set
getFilePath : FilePath n → String
Extension : Set
mkExtension : String → Extension
getExtension : Extension → String
{-# FOREIGN GHC import Data.Text #-}
{-# FOREIGN GHC import System.FilePath.Posix #-}
{-# FOREIGN GHC type AgdaFilePath n = FilePath #-}
{-# COMPILE GHC FilePath = type AgdaFilePath #-}
{-# COMPILE GHC getFilePath = const pack #-}
{-# COMPILE GHC Extension = type String #-}
{-# COMPILE GHC mkExtension = unpack #-}
{-# COMPILE GHC getExtension = pack #-}
-- We provide convenient short names for the two types of filepaths
AbsolutePath = FilePath Nature.absolute
RelativePath = FilePath Nature.relative
SomePath = FilePath Nature.unknown
-- In order to prevent users from picking whether a string gets
-- converted to a @relative@ or an @absolute@ path we have:
-- * a postulated @unknown@ nature
-- * a function @mkFilePath@ producing filepaths of this postulated nature
postulate
mkFilePath : String → SomePath
{-# COMPILE GHC mkFilePath = unpack #-}
postulate
-- Separator predicates
pathSeparator : Char
pathSeparators : List Char
isPathSeparator : Char → Bool
searchPathSeparator : Char
isSearchPathSeparator : Char → Bool
extSeparator : Char
isExtSeparator : Char → Bool
-- $PATH methods
splitSearchPath : String → List SomePath
getSearchPath : IO (List SomePath)
-- Extension functions
splitExtension : FilePath n → Pair (FilePath n) Extension
takeExtension : FilePath n → Extension
replaceExtension : FilePath n → Extension → FilePath n
dropExtension : FilePath n → FilePath n
addExtension : FilePath n → Extension → FilePath n
hasExtension : FilePath n → Bool
splitExtensions : FilePath n → Pair (FilePath n) Extension
takeExtensions : FilePath n → Extension
replaceExtensions : FilePath n → Extension → FilePath n
dropExtensions : FilePath n → FilePath n
isExtensionOf : Extension → FilePath n → Bool
stripExtension : Extension → FilePath n → Maybe (FilePath n)
-- Filename/directory functions
splitFileName : FilePath n → Pair (FilePath n) RelativePath
takeFileName : FilePath n → String
replaceFileName : FilePath n → String → FilePath n
dropFileName : FilePath n → FilePath n
takeBaseName : FilePath n → String
replaceBaseName : FilePath n → String → FilePath n
takeDirectory : FilePath n → FilePath n
replaceDirectory : FilePath m → FilePath n → FilePath n
combine : FilePath n → RelativePath → FilePath n
splitPath : FilePath n → List RelativePath
joinPath : List RelativePath → RelativePath
splitDirectories : FilePath n → List RelativePath
-- Drive functions
splitDrive : FilePath n → Pair (FilePath n) RelativePath
joinDrive : FilePath n → RelativePath → FilePath n
takeDrive : FilePath n → FilePath n
hasDrive : FilePath n → Bool
dropDrive : FilePath n → RelativePath
isDrive : FilePath n → Bool
-- Trailing slash functions
hasTrailingPathSeparator : FilePath n → Bool
addTrailingPathSeparator : FilePath n → FilePath n
dropTrailingPathSeparator : FilePath n → FilePath n
-- File name manipulations
normalise : FilePath n → FilePath n
equalFilePath : FilePath m → FilePath n → Bool
makeRelative : FilePath m → FilePath n → RelativePath
checkFilePath : FilePath n → Either RelativePath AbsolutePath
isRelative : FilePath n → Bool
isAbsolute : FilePath n → Bool
isValid : FilePath n → Bool
makeValid : FilePath n → FilePath n
{-# FOREIGN GHC
checkFilePath fp
| isRelative fp = Left fp
| otherwise = Right fp
#-}
{-# COMPILE GHC pathSeparator = pathSeparator #-}
{-# COMPILE GHC pathSeparators = pathSeparators #-}
{-# COMPILE GHC isPathSeparator = isPathSeparator #-}
{-# COMPILE GHC searchPathSeparator = searchPathSeparator #-}
{-# COMPILE GHC isSearchPathSeparator = isSearchPathSeparator #-}
{-# COMPILE GHC extSeparator = extSeparator #-}
{-# COMPILE GHC isExtSeparator = isExtSeparator #-}
{-# COMPILE GHC splitSearchPath = splitSearchPath . unpack #-}
{-# COMPILE GHC getSearchPath = getSearchPath #-}
{-# COMPILE GHC splitExtension = const splitExtension #-}
{-# COMPILE GHC takeExtension = const takeExtension #-}
{-# COMPILE GHC replaceExtension = const replaceExtension #-}
{-# COMPILE GHC dropExtension = const dropExtension #-}
{-# COMPILE GHC addExtension = const addExtension #-}
{-# COMPILE GHC hasExtension = const hasExtension #-}
{-# COMPILE GHC splitExtensions = const splitExtensions #-}
{-# COMPILE GHC takeExtensions = const takeExtensions #-}
{-# COMPILE GHC replaceExtensions = const replaceExtensions #-}
{-# COMPILE GHC dropExtensions = const dropExtensions #-}
{-# COMPILE GHC isExtensionOf = const isExtensionOf #-}
{-# COMPILE GHC stripExtension = const stripExtension #-}
{-# COMPILE GHC splitFileName = const splitFileName #-}
{-# COMPILE GHC takeFileName = const $ pack . takeFileName #-}
{-# COMPILE GHC replaceFileName = const $ fmap (. unpack) replaceFileName #-}
{-# COMPILE GHC dropFileName = const dropFileName #-}
{-# COMPILE GHC takeBaseName = const $ pack . takeBaseName #-}
{-# COMPILE GHC replaceBaseName = const $ fmap (. unpack) replaceBaseName #-}
{-# COMPILE GHC takeDirectory = const takeDirectory #-}
{-# COMPILE GHC replaceDirectory = \ _ _ -> replaceDirectory #-}
{-# COMPILE GHC combine = const combine #-}
{-# COMPILE GHC splitPath = const splitPath #-}
{-# COMPILE GHC joinPath = joinPath #-}
{-# COMPILE GHC splitDirectories = const splitDirectories #-}
{-# COMPILE GHC splitDrive = const splitDrive #-}
{-# COMPILE GHC joinDrive = const joinDrive #-}
{-# COMPILE GHC takeDrive = const takeDrive #-}
{-# COMPILE GHC hasDrive = const hasDrive #-}
{-# COMPILE GHC dropDrive = const dropDrive #-}
{-# COMPILE GHC isDrive = const isDrive #-}
{-# COMPILE GHC hasTrailingPathSeparator = const hasTrailingPathSeparator #-}
{-# COMPILE GHC addTrailingPathSeparator = const addTrailingPathSeparator #-}
{-# COMPILE GHC dropTrailingPathSeparator = const dropTrailingPathSeparator #-}
{-# COMPILE GHC normalise = const normalise #-}
{-# COMPILE GHC equalFilePath = \ _ _ -> equalFilePath #-}
{-# COMPILE GHC makeRelative = \ _ _ -> makeRelative #-}
{-# COMPILE GHC isRelative = const isRelative #-}
{-# COMPILE GHC isAbsolute = const isAbsolute #-}
{-# COMPILE GHC checkFilePath = const checkFilePath #-}
{-# COMPILE GHC isValid = const isValid #-}
{-# COMPILE GHC makeValid = const makeValid #-}
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