------------------------------------------------------------------------
-- The Agda standard library
--
-- Posix filepaths
------------------------------------------------------------------------

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

module System.FilePath.Posix where

open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.List using (List)
open import Agda.Builtin.String using (String)
open import IO.Base using (IO; lift)
open import Data.Maybe.Base using (Maybe)
open import Data.Product.Base using (_×_)
open import Data.Sum.Base using (_⊎_)

open import Foreign.Haskell.Coerce

open import System.FilePath.Posix.Primitive as Prim
  public
  -- Some of these functions are not directly re-exported because their
  -- respective types mentions FFI-friendly versions of the stdlib's types
  -- e.g. `Pair` instead of `_×_`.
  -- A wrapper is systematically defined below using Foreign.Haskell.Coerce's
  -- zero-cost coercion to expose a more useful function to users.
  using ( module Nature
        ; Nature
        ; FilePath
        ; mkFilePath
        ; getFilePath
        ; AbsolutePath
        ; RelativePath
        ; SomePath
        ; Extension
        ; mkExtension
        ; getExtension
     -- Separator predicates
        ; pathSeparator
        ; pathSeparators
        ; isPathSeparator
        ; searchPathSeparator
        ; isSearchPathSeparator
        ; extSeparator
        ; isExtSeparator
     -- $PATH methods
        ; splitSearchPath
     -- ; getSearchPath see below: lift needed
     -- Extension functions
     -- ; splitExtension see below: coerce needed
        ; takeExtension
        ; replaceExtension
        ; dropExtension
        ; addExtension
        ; hasExtension
        ; takeExtensions
        ; replaceExtensions
        ; dropExtensions
        ; isExtensionOf
     -- ; stripExtension see below: coerce needed
     -- Filename/directory functions
     -- ; splitFileName see below: coerce needed
        ; takeFileName
        ; replaceFileName
        ; dropFileName
        ; takeBaseName
        ; replaceBaseName
        ; takeDirectory
        ; replaceDirectory
        ; combine
        ; splitPath
        ; joinPath
        ; splitDirectories
      -- Trailing slash functions
        ; hasTrailingPathSeparator
        ; addTrailingPathSeparator
        ; dropTrailingPathSeparator
     -- File name manipulations
        ; normalise
        ; equalFilePath
        ; makeRelative
     -- ; checkFilePath see below: coerce needed
        ; isRelative
        ; isAbsolute
        ; isValid
        ; makeValid
        )

private
  variable
    m n : Nature

-- singleton type for Nature
data KnownNature : Nature → Set where
  instance
    absolute : KnownNature Nature.absolute
    relative : KnownNature Nature.relative

currentDirectory : SomePath
currentDirectory = mkFilePath "."

splitExtension  : FilePath n → FilePath n × Extension
splitExtension = coerce Prim.splitExtension

splitExtensions : FilePath n → FilePath n × Extension
splitExtensions = coerce Prim.splitExtensions

stripExtension : Extension → FilePath n → Maybe (FilePath n)
stripExtension = coerce Prim.stripExtension

getSearchPath : IO (List SomePath)
getSearchPath = lift Prim.getSearchPath

splitFileName : FilePath n → FilePath n × RelativePath
splitFileName = coerce Prim.splitFileName

checkFilePath : FilePath n → RelativePath ⊎ AbsolutePath
checkFilePath = coerce Prim.checkFilePath